definition star_lang ≝ λS.λl.λw:\ 5a href="cic:/matita/tutorial/chapter4/word.def(3)"\ 6word\ 5/a\ 6 S.\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6lw. \ 5a href="cic:/matita/tutorial/chapter4/flatten.fix(0,1,4)"\ 6flatten\ 5/a\ 6 ? lw \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 w \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter4/conjunct.fix(0,1,4)"\ 6conjunct\ 5/a\ 6 ? lw l.
interpretation "star lang" 'kstar l = (star_lang ? l).
-(* notation "ℓ term 70 E" non associative with precedence 75 for @{in_l ? $E}. *)
+(* notation "| term 70 E| " non associative with precedence 75 for @{in_l ? $E}. *)
let rec in_l (S : \ 5a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"\ 6Alpha\ 5/a\ 6) (r : \ 5a href="cic:/matita/tutorial/chapter4/re.ind(1,0,1)"\ 6re\ 5/a\ 6 S) on r : \ 5a href="cic:/matita/tutorial/chapter4/word.def(3)"\ 6word\ 5/a\ 6 S → Prop ≝
match r with
| star r1 ⇒ (in_l ? r1)\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*
].
-notation "ℓ term 70 E" non associative with precedence 75 for @{'in_l $E}.
-interpretation "in_l" 'in_l E = (in_l ? E).
+notation "\sem{E}" non associative with precedence 75 for @{'sem $E}.
+interpretation "in_l" 'sem E = (in_l ? E).
interpretation "in_l mem" 'mem w l = (in_l ? l w).
notation "a ∨ b" left associative with precedence 30 for @{'orb $a $b}.
definition pre ≝ λS.\ 5a href="cic:/matita/tutorial/chapter4/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S \ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)" title="null"\ 6bool\ 5/a\ 6.
+definition test ≝ λS:Alpha.λe: pre S. match e with [mk_pair i b ⇒ e].
+
interpretation "pstar" 'kstar a = (pstar ? a).
interpretation "por" 'plus a b = (por ? a b).
interpretation "pcat" 'concat a b = (pconcat ? a b).
interpretation "pepsilon" 'epsilon = (pepsilon ?).
interpretation "pempty" 'empty = (pzero ?).
-notation "\boxv term 19 e \boxv" (* slash boxv *) non associative with precedence 70 for @{forget ? $e}.
+notation "| e |" non associative with precedence 65 for @{forget ? $e}.
let rec forget (S: \ 5a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"\ 6Alpha\ 5/a\ 6) (l : \ 5a href="cic:/matita/tutorial/chapter4/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S) on l: \ 5a href="cic:/matita/tutorial/chapter4/re.ind(1,0,1)"\ 6re\ 5/a\ 6 S ≝
match l with
[ pzero ⇒ \ 5a title="empty" href="cic:/fakeuri.def(1)"\ 6∅\ 5/a\ 6
| pepsilon ⇒ \ 5a title="epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6
| pchar x ⇒ \ 5a href="cic:/matita/tutorial/chapter4/re.con(0,3,1)"\ 6char\ 5/a\ 6 ? x
- | ppoint x ⇒ \ 5a href="cic:/matita/tutorial/chapter4/re.con(0,3,1)"\ 6char\ 5/a\ 6 ? x
- | pconcat e1 e2 ⇒ │e1│ \ 5a title="cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 │e2│
- | por e1 e2 ⇒ │e1│ \ 5a title="or" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 │e2│
- | pstar e ⇒ │e│\ 5a title="star" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*
+ | ppoint x ⇒ \ 5a href="cic:/matita/tutorial/chapter4/re.con(0,3,1)"\ 6char\ 5/a\ 6 ? x
+ | pconcat e1 e2 ⇒ |e1| \ 5a title="cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 |e2|
+ | por e1 e2 ⇒ |e1| \ 5a title="or" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 |e2|
+ | pstar e ⇒ |e|\ 5a title="star" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*
].
-notation "│ term 19 e │" non associative with precedence 70 for @{'forget $e}.
-interpretation "forget" 'forget a = (forget ? a).
-
-notation "\fst term 90 x" non associative with precedence 90 for @{'fst $x}.
-interpretation "fst" 'fst x = (fst ? ? x).
-notation "\snd term 90 x" non associative with precedence 90 for @{'snd $x}.
-interpretation "snd" 'snd x = (snd ? ? x).
-
-notation "ℓ term 70 E" non associative with precedence 75 for @{in_pl ? $E}.
+notation "| e |" non associative with precedence 65 for @{'fmap $e}.
+interpretation "forget" 'fmap a = (forget ? a).
let rec in_pl (S : \ 5a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"\ 6Alpha\ 5/a\ 6) (r : \ 5a href="cic:/matita/tutorial/chapter4/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S) on r : \ 5a href="cic:/matita/tutorial/chapter4/word.def(3)"\ 6word\ 5/a\ 6 S → Prop ≝
match r with
| pepsilon ⇒ \ 5a title="empty lang" href="cic:/fakeuri.def(1)"\ 6∅\ 5/a\ 6
| pchar _ ⇒ \ 5a title="empty lang" href="cic:/fakeuri.def(1)"\ 6∅\ 5/a\ 6
| ppoint x ⇒ \ 5a title="sing lang" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6: x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] }
- | pconcat pe1 pe2 ⇒ in_pl ? pe1 \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 \ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6ℓ\ 5/a\ 6 │pe2│ \ 5a title="union lang" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 in_pl ? pe2
+ | pconcat pe1 pe2 ⇒ in_pl ? pe1 \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 \ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{|pe2|} \ 5a title="union lang" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 in_pl ? pe2
| por pe1 pe2 ⇒ in_pl ? pe1 \ 5a title="union lang" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 in_pl ? pe2
- | pstar pe ⇒ in_pl ? pe \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 \ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6ℓ\ 5/a\ 6 │pe│\ 5a title="star" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*
+ | pstar pe ⇒ in_pl ? pe \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 \ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{|pe|}\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*
].
-interpretation "in_pl" 'in_l E = (in_pl ? E).
+interpretation "in_pl" 'sem E = (in_pl ? E).
interpretation "in_pl mem" 'mem w l = (in_pl ? l w).
-definition eps: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"\ 6Alpha\ 5/a\ 6.\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)" title="null"\ 6bool\ 5/a\ 6 → \ 5a href="cic:/matita/tutorial/chapter4/word.def(3)"\ 6word\ 5/a\ 6 S → Prop
+definition eps: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"\ 6Alpha\ 5/a\ 6.\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 → \ 5a href="cic:/matita/tutorial/chapter4/word.def(3)"\ 6word\ 5/a\ 6 S → Prop
≝ λS,b. \ 5a href="cic:/matita/basics/bool/if_then_else.def(1)"\ 6if_then_else\ 5/a\ 6 ? b \ 5a title="sing lang" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6: \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] } \ 5a title="empty lang" href="cic:/fakeuri.def(1)"\ 6∅\ 5/a\ 6.
-(* interpretation "epsilon" 'epsilon = (epsilon ?). *)
notation "ϵ _ b" non associative with precedence 90 for @{'app_epsilon $b}.
interpretation "epsilon lang" 'app_epsilon b = (eps ? b).
-definition in_prl ≝ λS : \ 5a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"\ 6Alpha\ 5/a\ 6.λp:\ 5a href="cic:/matita/tutorial/chapter4/pre.def(1)"\ 6pre\ 5/a\ 6 S. \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6ℓ\ 5/a\ 6 (\ 5a title="fst" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 p) \ 5a title="union lang" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 \ 5a title="epsilon lang" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6_(\ 5a title="snd" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 p).
+definition in_prl ≝ λS : \ 5a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"\ 6Alpha\ 5/a\ 6.λp:\ 5a href="cic:/matita/tutorial/chapter4/pre.def(1)"\ 6pre\ 5/a\ 6 S. \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 p} \ 5a title="union lang" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 \ 5a title="epsilon lang" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6_(\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 p).
interpretation "in_prl mem" 'mem w l = (in_prl ? l w).
-interpretation "in_prl" 'in_l E = (in_prl ? E).
+interpretation "in_prl" 'sem E = (in_prl ? E).
-lemma not_epsilon_lp :∀S.∀pi:\ 5a href="cic:/matita/tutorial/chapter4/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S. \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 ((\ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6ℓ\ 5/a\ 6 pi) \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6]).
-#S #pi (elim pi) normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Not.con(0,1,1)"\ 6nmk\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+lemma not_epsilon_lp :∀S.∀pi:\ 5a href="cic:/matita/tutorial/chapter4/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.\ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6\neg\ 5/a\ 6(\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] \ 5a title="in_pl mem" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 pi).
+#S #pi (elim pi) normalize / \ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Not.con(0,1,1)"\ 6nmk\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
[#pi1 #pi2 #H1 #H2 % * /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ * #w1 * #w2 * * #appnil
cases (\ 5a href="cic:/matita/tutorial/chapter3/nil_to_nil.def(5)"\ 6nil_to_nil\ 5/a\ 6 … appnil) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
|#p11 #p12 #H1 #H2 % * /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
]
qed.
-lemma if_true_epsilon: ∀S.∀e:\ 5a href="cic:/matita/tutorial/chapter4/pre.def(1)"\ 6pre\ 5/a\ 6 S. \ 5a title="snd" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 e \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → ((\ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6ℓ\ 5/a\ 6 e) \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6]).
+lemma if_true_epsilon: ∀S.∀e:\ 5a href="cic:/matita/tutorial/chapter4/pre.def(1)"\ 6pre\ 5/a\ 6 S. \ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 e \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → (\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] \ 5a title="in_prl mem" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 e).
#S #e #H %2 >H // qed.
-lemma if_epsilon_true : ∀S.∀e:\ 5a href="cic:/matita/tutorial/chapter4/pre.def(1)"\ 6pre\ 5/a\ 6 S. \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ] \ 5a title="in_prl mem" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 e → \ 5a title="snd" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 e \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
-#S * #pi #b * [normalize #abs @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /2/] cases b normalize // @False_ind
+lemma if_epsilon_true : ∀S.∀e:\ 5a href="cic:/matita/tutorial/chapter4/pre.def(1)"\ 6pre\ 5/a\ 6 S. \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ] \ 5a title="in_prl mem" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 e → \ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 e \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
+#S * #pi #b * [normalize #abs @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/] cases b normalize // @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6
qed.
-definition lor ≝ λS:Alpha.λa,b:pre S.〈\fst a + \fst b,\snd a ∨ \snd b〉.
+definition lor ≝ λS:\ 5a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"\ 6Alpha\ 5/a\ 6.λa,b:\ 5a href="cic:/matita/tutorial/chapter4/pre.def(1)"\ 6pre\ 5/a\ 6 S.\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 a \ 5a title="por" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 \ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 b,\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 a \ 5a title="boolean or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 \ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 b〉.
notation "a ⊕ b" left associative with precedence 60 for @{'oplus $a $b}.
-interpretation "oplus" 'oplus a b = (lo ? a b).
+interpretation "oplus" 'oplus a b = (lor ? a b).
-ndefinition lc ≝ λS:Alpha.λbcast:∀S:Alpha.∀E:pitem S.pre S.λa,b:pre S.
- match a with [ mk_pair e1 b1 ⇒
- match b1 with
- [ false ⇒ 〈e1 · \fst b, \snd b〉
- | true ⇒ 〈e1 · \fst (bcast ? (\fst b)),\snd b || \snd (bcast ? (\fst b))〉]].
+definition item_concat: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"\ 6Alpha\ 5/a\ 6.\ 5a href="cic:/matita/tutorial/chapter4/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S → \ 5a href="cic:/matita/tutorial/chapter4/pre.def(1)"\ 6pre\ 5/a\ 6 S → \ 5a href="cic:/matita/tutorial/chapter4/pre.def(1)"\ 6pre\ 5/a\ 6 S ≝
+ λS,i,e.\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i \ 5a title="pcat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 \ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e, \ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 e〉.
+
+definition lcat: ∀S:Alpha.∀bcast:(∀S:Alpha.pre S →pre S).pre S → pre S → pre S
+ ≝ λS:Alpha.λbcast:∀S:Alpha.pre S → pre S.λe1,e2:pre S.
+ match e1 with [ mk_pair i1 b1 ⇒ e2].
+
+ match e1 with [ _ => e1].
+
+ match b1 with
+ [ false ⇒ e2 | _ => e1 ]].
+
+ | true ⇒ item_concat S i1 (bcast S e2)
+ ]
+].
notation < "a ⊙ b" left associative with precedence 60 for @{'lc $op $a $b}.
interpretation "lc" 'lc op a b = (lc ? op a b).
projects / helm.git / blobdiff