-qed.
-
-(*
-lemma sem_eclose_star: ∀S:DeqSet.∀i:pitem S.
- \sem{〈i^*,true〉} =1 \sem{〈i,false〉}·\sem{|i|}^* ∪ {ϵ}.
-/2/ qed.
-*)
-
-(* theorem 16: 1 → 3 *)
-lemma odot_dot_aux : ∀S.∀e1:pre S.∀i2:pitem S.
- \sem{•i2} =1 \sem{i2} ∪ \sem{|i2|} →
- \sem{e1 ▹ i2} =1 \sem{e1} · \sem{|i2|} ∪ \sem{i2}.
-#S * #i1 #b1 #i2 cases b1
- [2:#th >odot_false >sem_pre_false >sem_pre_false >sem_cat /2/
- |#H >odot_true >sem_pre_true @(eqP_trans … (sem_pre_concat_r …))
- >erase_bull @eqP_trans [|@(eqP_union_l … H)]
- @eqP_trans [|@eqP_union_l[|@union_comm ]]
- @eqP_trans [|@eqP_sym @union_assoc ] /3/
- ]
-qed.
-
-lemma minus_eps_pre_aux: ∀S.∀e:pre S.∀i:pitem S.∀A.
- \sem{e} =1 \sem{i} ∪ A → \sem{\fst e} =1 \sem{i} ∪ (A - {[ ]}).
-#S #e #i #A #seme
-@eqP_trans [|@minus_eps_pre]
-@eqP_trans [||@eqP_union_r [|@eqP_sym @minus_eps_item]]
-@eqP_trans [||@distribute_substract]
-@eqP_substract_r //
-qed.
-
-(* theorem 16: 1 *)
-theorem sem_bull: ∀S:DeqSet. ∀i:pitem S. \sem{•i} =1 \sem{i} ∪ \sem{|i|}.
-#S #e elim e
- [#w normalize % [/2/ | * //]
- |/2/
- |#x normalize #w % [ /2/ | * [@False_ind | //]]
- |#x normalize #w % [ /2/ | * // ]
- |#i1 #i2 #IH1 #IH2 >eclose_dot
- @eqP_trans [|@odot_dot_aux //] >sem_cat
- @eqP_trans
- [|@eqP_union_r
- [|@eqP_trans [|@(cat_ext_l … IH1)] @distr_cat_r]]
- @eqP_trans [|@union_assoc]
- @eqP_trans [||@eqP_sym @union_assoc]
- @eqP_union_l //
- |#i1 #i2 #IH1 #IH2 >eclose_plus
- @eqP_trans [|@sem_oplus] >sem_plus >erase_plus
- @eqP_trans [|@(eqP_union_l … IH2)]
- @eqP_trans [|@eqP_sym @union_assoc]
- @eqP_trans [||@union_assoc] @eqP_union_r
- @eqP_trans [||@eqP_sym @union_assoc]
- @eqP_trans [||@eqP_union_l [|@union_comm]]
- @eqP_trans [||@union_assoc] /2/
- |#i #H >sem_pre_true >sem_star >erase_bull >sem_star
- @eqP_trans [|@eqP_union_r [|@cat_ext_l [|@minus_eps_pre_aux //]]]
- @eqP_trans [|@eqP_union_r [|@distr_cat_r]]
- @eqP_trans [|@union_assoc] @eqP_union_l >erase_star
- @eqP_sym @star_fix_eps
- ]
-qed.
-
-(* blank item *)
-let rec blank (S: DeqSet) (i: re S) on i :pitem S ≝
- match i with
- [ z ⇒ `∅
- | e ⇒ ϵ
- | s y ⇒ `y
- | o e1 e2 ⇒ (blank S e1) + (blank S e2)
- | c e1 e2 ⇒ (blank S e1) · (blank S e2)
- | k e ⇒ (blank S e)^* ].
-
-lemma forget_blank: ∀S.∀e:re S.|blank S e| = e.
-#S #e elim e normalize //
-qed.
-
-lemma sem_blank: ∀S.∀e:re S.\sem{blank S e} =1 ∅.
-#S #e elim e
- [1,2:@eq_to_ex_eq //
- |#s @eq_to_ex_eq //
- |#e1 #e2 #Hind1 #Hind2 >sem_cat
- @eqP_trans [||@(union_empty_r … ∅)]
- @eqP_trans [|@eqP_union_l[|@Hind2]] @eqP_union_r
- @eqP_trans [||@(cat_empty_l … ?)] @cat_ext_l @Hind1
- |#e1 #e2 #Hind1 #Hind2 >sem_plus
- @eqP_trans [||@(union_empty_r … ∅)]
- @eqP_trans [|@eqP_union_l[|@Hind2]] @eqP_union_r @Hind1
- |#e #Hind >sem_star
- @eqP_trans [||@(cat_empty_l … ?)] @cat_ext_l @Hind
- ]
-qed.
-
-theorem re_embedding: ∀S.∀e:re S.
- \sem{•(blank S e)} =1 \sem{e}.
-#S #e @eqP_trans [|@sem_bull] >forget_blank
-@eqP_trans [|@eqP_union_r [|@sem_blank]]
-@eqP_trans [|@union_comm] @union_empty_r.
-qed.
-
-(* lefted operations *)
-definition lifted_cat ≝ λS:DeqSet.λe:pre S.
- lift S (pre_concat_l S eclose e).
-
-notation "e1 ⊙ e2" left associative with precedence 70 for @{'odot $e1 $e2}.
-
-interpretation "lifted cat" 'odot e1 e2 = (lifted_cat ? e1 e2).
-
-lemma odot_true_b : ∀S.∀i1,i2:pitem S.∀b.
- 〈i1,true〉 ⊙ 〈i2,b〉 = 〈i1 · (\fst (•i2)),\snd (•i2) ∨ b〉.
-#S #i1 #i2 #b normalize in ⊢ (??%?); cases (•i2) //
-qed.
-
-lemma odot_false_b : ∀S.∀i1,i2:pitem S.∀b.
- 〈i1,false〉 ⊙ 〈i2,b〉 = 〈i1 · i2 ,b〉.
-//
-qed.
-
-lemma erase_odot:∀S.∀e1,e2:pre S.
- |\fst (e1 ⊙ e2)| = |\fst e1| · (|\fst e2|).
-#S * #i1 * * #i2 #b2 // >odot_true_b >erase_dot //
-qed.
-
-definition lk ≝ λS:DeqSet.λe:pre S.
- match e with
- [ mk_Prod i1 b1 ⇒
- match b1 with
- [true ⇒ 〈(\fst (eclose ? i1))^*, true〉
- |false ⇒ 〈i1^*,false〉
- ]
- ].
-
-(* notation < "a \sup ⊛" non associative with precedence 90 for @{'lk $a}.*)
-interpretation "lk" 'lk a = (lk ? a).
-notation "a^⊛" non associative with precedence 90 for @{'lk $a}.
-
-
-lemma ostar_true: ∀S.∀i:pitem S.
- 〈i,true〉^⊛ = 〈(\fst (•i))^*, true〉.
-// qed.
-
-lemma ostar_false: ∀S.∀i:pitem S.
- 〈i,false〉^⊛ = 〈i^*, false〉.
-// qed.
-
-lemma erase_ostar: ∀S.∀e:pre S.
- |\fst (e^⊛)| = |\fst e|^*.
-#S * #i * // qed.
-
-lemma sem_odot_true: ∀S:DeqSet.∀e1:pre S.∀i.
- \sem{e1 ⊙ 〈i,true〉} =1 \sem{e1 ▹ i} ∪ { [ ] }.
-#S #e1 #i
-cut (e1 ⊙ 〈i,true〉 = 〈\fst (e1 ▹ i), \snd(e1 ▹ i) ∨ true〉) [//]
-#H >H cases (e1 ▹ i) #i1 #b1 cases b1
- [>sem_pre_true @eqP_trans [||@eqP_sym @union_assoc]
- @eqP_union_l /2/
- |/2/
- ]
-qed.
-
-lemma eq_odot_false: ∀S:DeqSet.∀e1:pre S.∀i.
- e1 ⊙ 〈i,false〉 = e1 ▹ i.
-#S #e1 #i
-cut (e1 ⊙ 〈i,false〉 = 〈\fst (e1 ▹ i), \snd(e1 ▹ i) ∨ false〉) [//]
-cases (e1 ▹ i) #i1 #b1 cases b1 #H @H
-qed.
-
-lemma sem_odot:
- ∀S.∀e1,e2: pre S. \sem{e1 ⊙ e2} =1 \sem{e1}· \sem{|\fst e2|} ∪ \sem{e2}.
-#S #e1 * #i2 *
- [>sem_pre_true
- @eqP_trans [|@sem_odot_true]
- @eqP_trans [||@union_assoc] @eqP_union_r @odot_dot_aux //
- |>sem_pre_false >eq_odot_false @odot_dot_aux //
- ]
-qed.
-
-(* theorem 16: 4 *)
-theorem sem_ostar: ∀S.∀e:pre S.
- \sem{e^⊛} =1 \sem{e} · \sem{|\fst e|}^*.
-#S * #i #b cases b
- [>sem_pre_true >sem_pre_true >sem_star >erase_bull
- @eqP_trans [|@eqP_union_r[|@cat_ext_l [|@minus_eps_pre_aux //]]]
- @eqP_trans [|@eqP_union_r [|@distr_cat_r]]
- @eqP_trans [||@eqP_sym @distr_cat_r]
- @eqP_trans [|@union_assoc] @eqP_union_l
- @eqP_trans [||@eqP_sym @epsilon_cat_l] @eqP_sym @star_fix_eps
- |>sem_pre_false >sem_pre_false >sem_star /2/
- ]
-qed.
-