interpretation "star" 'pk a = (k ? a).
interpretation "or" 'plus a b = (o ? a b).
-notation "a · b" non associative with precedence 60 for @{ 'pc $a $b}.
+notation "a · b" non associative with precedence 65 for @{ 'pc $a $b}.
interpretation "cat" 'pc a b = (c ? a b).
(* to get rid of \middot *)
nqed.
ndefinition lo ≝ λS:Alpha.λa,b:pre S.〈\fst a + \fst b,\snd a || \snd b〉.
-notation "a ⊕ b" left associative with precedence 60 for @{'oplus $a $b}.
+notation "a ⊕ b" left associative with precedence 65 for @{'oplus $a $b}.
interpretation "oplus" 'oplus a b = (lo ? a b).
ndefinition lc ≝ λS:Alpha.λbcast:∀S:Alpha.∀E:pitem S.pre S.λa,b:pre S.
[ false ⇒ 〈e1 · \fst b, \snd b〉
| true ⇒ 〈e1 · \fst (bcast ? (\fst b)),\snd b || \snd (bcast ? (\fst b))〉]].
-notation < "a ⊙ b" left associative with precedence 60 for @{'lc $op $a $b}.
+notation < "a ⊙ b" left associative with precedence 65 for @{'lc $op $a $b}.
interpretation "lc" 'lc op a b = (lc ? op a b).
-notation > "a ⊙ b" left associative with precedence 60 for @{'lc eclose $a $b}.
+notation > "a ⊙ b" left associative with precedence 65 for @{'lc eclose $a $b}.
ndefinition lk ≝ λS:Alpha.λbcast:∀S:Alpha.∀E:pitem S.pre S.λa:pre S.
match a with [ mk_pair e1 b1 ⇒
interpretation "lk" 'lk op a = (lk ? op a).
notation > "a ^ ⊛" non associative with precedence 75 for @{'lk eclose $a}.
-notation > "•" non associative with precedence 60 for @{eclose ?}.
+notation > "•" non associative with precedence 65 for @{eclose ?}.
nlet rec eclose (S: Alpha) (E: pitem S) on E : pre S ≝
match E with
[ pz ⇒ 〈 0, false 〉
| po E1 E2 ⇒ •E1 ⊕ •E2
| pc E1 E2 ⇒ •E1 ⊙ 〈 E2, false 〉
| pk E ⇒ 〈(\fst (•E))^*,true〉].
-notation < "• x" non associative with precedence 60 for @{'eclose $x}.
+notation < "• x" non associative with precedence 65 for @{'eclose $x}.
interpretation "eclose" 'eclose x = (eclose ? x).
-notation > "• x" non associative with precedence 60 for @{'eclose $x}.
+notation > "• x" non associative with precedence 65 for @{'eclose $x}.
ndefinition reclose ≝ λS:Alpha.λp:pre S.let p' ≝ •\fst p in 〈\fst p',\snd p || \snd p'〉.
interpretation "reclose" 'eclose x = (reclose ? x).
@; //;##]
nqed.
-STOP
-
(* theorem 16: 1 *)
alias symbol "pc" (instance 13) = "cat lang".
alias symbol "in_pl" (instance 23) = "in_pl".
alias symbol "in_pl" (instance 5) = "in_pl".
alias symbol "eclose" (instance 21) = "eclose".
-ntheorem bull_cup : ∀S:Alpha. ∀e:pitem S. 𝐋\p (•e) = 𝐋\p e ∪ 𝐋 .|e|.
+ntheorem bull_cup : ∀S:Alpha. ∀e:pitem S. 𝐋\p (•e) = 𝐋\p e ∪ 𝐋 |e|.
#S e; nelim e; //;
- ##[ #a; napply extP; #w; nnormalize; @; *; /3/ by or_introl, or_intror;
- ##| #a; napply extP; #w; nnormalize; @; *; /3/ by or_introl; *;
+ ##[ #a; napply ext_set; #w; @; *; /3/ by or_introl, or_intror;
+ ##| #a; napply ext_set; #w; @; *; /3/ by or_introl; *;
##| #e1 e2 IH1 IH2;
- nchange in ⊢ (??(??(%))?) with (•e1 ⊙ 〈e2,false〉);
- nrewrite > (odot_dot_aux S (•e1) 〈e2,false〉 IH2);
- nrewrite > (IH1 …); nrewrite > (cup_dotD …);
- nrewrite > (cupA …); nrewrite > (cupC ?? (𝐋\p ?) …);
- nchange in match (𝐋\p 〈?,?〉) with (𝐋\p e2 ∪ {}); nrewrite > (cup0 …);
- nrewrite < (erase_dot …); nrewrite < (cupA …); //;
+ nchange in match (•(e1·e2)) with (•e1 ⊙ 〈e2,false〉);
+ napply (.=_1 (odot_dot_aux ?? 〈e2,false〉 IH2));
+ napply (.=_1 (IH1 ╪_1 #) ╪_1 #);
+ napply (.=_1 (cup_dotD …) ╪_1 #);
+ napply (.=_1 (cupA …));
+ napply (.=_1 # ╪_1 ((erase_dot ???)^-1 ╪_1 (cup0 ??)));
+ napply (.=_1 # ╪_1 (cupC…));
+ napply (.=_1 (cupA …)^-1);
+ //;
##| #e1 e2 IH1 IH2;
- nchange in match (•(?+?)) with (•e1 ⊕ •e2); nrewrite > (oplus_cup …);
- nrewrite > (IH1 …); nrewrite > (IH2 …); nrewrite > (cupA …);
- nrewrite > (cupC ? (𝐋\p e2)…);nrewrite < (cupA ??? (𝐋\p e2)…);
- nrewrite > (cupC ?? (𝐋\p e2)…); nrewrite < (cupA …);
- nrewrite < (erase_plus …); //.
+ nchange in match (•(?+?)) with (•e1 ⊕ •e2);
+ napply (.=_1 (oplus_cup …));
+ napply (.=_1 IH1 ╪_1 IH2);
+ napply (.=_1 (cupA …));
+ napply (.=_1 # ╪_1 (# ╪_1 (cupC…)));
+ napply (.=_1 # ╪_1 (cupA ????)^-1);
+ napply (.=_1 # ╪_1 (cupC…));
+ napply (.=_1 (cupA ????)^-1);
+ napply (.=_1 # ╪_1 (erase_plus ???)^-1);
+ //;
##| #e; nletin e' ≝ (\fst (•e)); nletin b' ≝ (\snd (•e)); #IH;
- nchange in match (𝐋\p ?) with (𝐋\p 〈e'^*,true〉);
+ nchange in match (𝐋\p ?) with (𝐋\p 〈e'^*,true〉);
nchange in match (𝐋\p ?) with (𝐋\p (e'^* ) ∪ {[ ]});
- nchange in ⊢ (??(??%?)?) with (𝐋\p e' · 𝐋 .|e'|^* );
+STOP
+ nchange in match (𝐋\p (pk ? e')) with (𝐋\p e' · 𝐋 |e'|^* );
nrewrite > (erase_bull…e);
nrewrite > (erase_star …);
nrewrite > (?: 𝐋\p e' = 𝐋\p e ∪ (𝐋 .|e| - ϵ b')); ##[##2:
nrewrite > (cup_dotD…); nrewrite > (cupA…);
nrewrite > (?: ((?·?)∪{[]} = 𝐋 .|e^*|)); //;
nchange in match (𝐋 .|e^*|) with ((𝐋. |e|)^* ); napply sub_dot_star;##]
- nqed.
+nqed.
(* theorem 16: 3 *)
nlemma odot_dot:
STOP
notation > "\move term 90 x term 90 E"
-non associative with precedence 60 for @{move ? $x $E}.
+non associative with precedence 65 for @{move ? $x $E}.
nlet rec move (S: Alpha) (x:S) (E: pitem S) on E : pre S ≝
match E with
[ pz ⇒ 〈 ∅, false 〉
| po e1 e2 ⇒ \move x e1 ⊕ \move x e2
| pc e1 e2 ⇒ \move x e1 ⊙ \move x e2
| pk e ⇒ (\move x e)^⊛ ].
-notation < "\move\shy x\shy E" non associative with precedence 60 for @{'move $x $E}.
-notation > "\move term 90 x term 90 E" non associative with precedence 60 for @{'move $x $E}.
+notation < "\move\shy x\shy E" non associative with precedence 65 for @{'move $x $E}.
+notation > "\move term 90 x term 90 E" non associative with precedence 65 for @{'move $x $E}.
interpretation "move" 'move x E = (move ? x E).
ndefinition rmove ≝ λS:Alpha.λx:S.λe:pre S. \move x (\fst e).
nqed.
-notation > "x ↦* E" non associative with precedence 60 for @{move_star ? $x $E}.
+notation > "x ↦* E" non associative with precedence 65 for @{move_star ? $x $E}.
nlet rec move_star (S : decidable) w E on w : bool × (pre S) ≝
match w with
[ nil ⇒ E
projects / helm.git / blobdiff