| star r1 ⇒ (in_l ? r1)\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*
].
-notation "\sem{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}.
| por: pitem S → pitem S → pitem S
| pstar: pitem S → pitem S.
-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 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.
interpretation "pstar" 'kstar a = (pstar ? a).
interpretation "por" 'plus a b = (por ? a b).
notation "| e |" non associative with precedence 65 for @{'fmap $e}.
interpretation "forget" 'fmap a = (forget ? a).
-lemma foo:∀a. 'fst a = 0.
-
-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 "\sem{E}" non associative with precedence 75 for @{in_pl ? $E}. *)
-
-let rec in_pl (S : Alpha) (r : pitem S) on r : word S → Prop ≝
+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
- [ pzero ⇒ ∅
- | pepsilon ⇒ ∅
- | pchar _ ⇒ ∅
- | ppoint x ⇒ {: x::[] }
- | pconcat pe1 pe2 ⇒ in_pl ? pe1 · \sem{|pe2|} ∪ in_pl ? pe2
- | por pe1 pe2 ⇒ in_pl ? pe1 ∪ in_pl ? pe2
- | pstar pe ⇒ in_pl ? pe · \sem{|pe|}^*
+ [ pzero ⇒ \ 5a title="empty lang" href="cic:/fakeuri.def(1)"\ 6∅\ 5/a\ 6
+ | 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\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\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:Alpha.bool → word S → Prop
- ≝ λS,b. if_then_else ? b {: [] } ∅.
+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 : Alpha.λp:pre S. ℓ (\fst p) ∪ ϵ_(\snd 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).
-
-lemma not_epsilon_lp :∀S.∀pi:pitem S. ¬ ((ℓ pi) []).
-#S #pi (elim pi) normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace nmk\ 5/span\ 6\ 5/span\ 6/
- [#pi1 #pi2 #H1 #H2 % * /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace absurd\ 5/span\ 6\ 5/span\ 6/ * #w1 * #w2 * * #appnil
- cases (nil_to_nil … appnil) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace absurd\ 5/span\ 6\ 5/span\ 6/
- |#p11 #p12 #H1 #H2 % * /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace absurd\ 5/span\ 6\ 5/span\ 6/
- |#pi #H % * #w1 * #w2 * * #appnil (cases (nil_to_nil … appnil)) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace absurd\ 5/span\ 6\ 5/span\ 6/
+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\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/
+ |#pi #H % * #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/
]
qed.
-lemma if_true_epsilon: ∀S.∀e:pre S. \snd e = true → ((ℓ e) []).
+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:pre S. [ ] ∈ e → \snd e = true.
-#S * #pi #b * [normalize #abs @False_ind /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〉.
+
+interpretation "item concat" 'concat i e = (item_concat ? i e).
+
+definition lcat: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"\ 6Alpha\ 5/a\ 6.∀bcast:(∀S:\ 5a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"\ 6Alpha\ 5/a\ 6.\ 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).\ 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 → \ 5a href="cic:/matita/tutorial/chapter4/pre.def(1)"\ 6pre\ 5/a\ 6 S
+ ≝ λS,bcast,e1,e2.
+ match e1 with [ pair i1 b1 ⇒ if_then_else b1 (i1 \ 5a title="item concat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 e2) (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).
| #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
| #x; #y; #K; ncases (?:False); /2/
| #x; #y; #z; #w; #a; #b; #c; #d; #K; ncases (?:False); /2/ ]
-##| #r1; #r2; #r1'; #r2'; #H1; #H2; #H3; #H4; #H5; #H6;
\ No newline at end of file
+##| #r1; #r2; #r1'; #r2'; #H1; #H2; #H3; #H4; #H5; #H6;
\ No newline at end of file
projects / helm.git / blobdiff