X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Ftutorial%2Fchapter4.ma;h=fd0f711443a8554f57061c1d22c4b39463a540e9;hb=7aa41e02e64bd09df253cc4267a44b4f49b16e03;hp=cf7f4aafce387300d1191b7300a5b7bcc4ca5d4c;hpb=b5f54d2815f446a999736abd0ffe80641596a5f6;p=helm.git

diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma
index cf7f4aafc..fd0f71144 100644
--- a/weblib/tutorial/chapter4.ma
+++ b/weblib/tutorial/chapter4.ma
@@ -72,7 +72,7 @@ interpretation "cat lang" 'concat a b = (cat ? a b).
 definition star_lang ≝ λS.λl.λw:a href="cic:/matita/tutorial/chapter4/word.def(3)"word/a S.a title="exists" href="cic:/fakeuri.def(1)"∃/alw. a href="cic:/matita/tutorial/chapter4/flatten.fix(0,1,4)"flatten/a ? lw a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a w a title="logical and" href="cic:/fakeuri.def(1)"∧/a a href="cic:/matita/tutorial/chapter4/conjunct.fix(0,1,4)"conjunct/a ? 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 : a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"Alpha/a) (r : a href="cic:/matita/tutorial/chapter4/re.ind(1,0,1)"re/a S) on r : a href="cic:/matita/tutorial/chapter4/word.def(3)"word/a S → Prop ≝ 
 match r with
@@ -84,8 +84,8 @@ match r with
  | star r1 ⇒ (in_l ? r1)a title="star lang" href="cic:/fakeuri.def(1)"^/a* 
  ].
 
-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}.
@@ -107,6 +107,8 @@ inductive pitem (S: a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"Alp
  
 definition pre ≝ λS.a href="cic:/matita/tutorial/chapter4/pitem.ind(1,0,1)"pitem/a S a title="Product" href="cic:/fakeuri.def(1)"×/a a href="cic:/matita/basics/bool/bool.ind(1,0,0)" title="null"bool/a.
 
+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).
@@ -121,28 +123,21 @@ interpretation "patom" 'pchar a = (pchar ? a).
 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: a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"Alpha/a) (l : a href="cic:/matita/tutorial/chapter4/pitem.ind(1,0,1)"pitem/a S) on l: a href="cic:/matita/tutorial/chapter4/re.ind(1,0,1)"re/a S ≝
  match l with
   [ pzero ⇒ a title="empty" href="cic:/fakeuri.def(1)"∅/a
   | pepsilon ⇒ a title="epsilon" href="cic:/fakeuri.def(1)"ϵ/a
   | pchar x ⇒ a href="cic:/matita/tutorial/chapter4/re.con(0,3,1)"char/a ? x 
-  | ppoint x ⇒ a href="cic:/matita/tutorial/chapter4/re.con(0,3,1)"char/a ? x  
-  | pconcat e1 e2 ⇒ │e1│ a title="cat" href="cic:/fakeuri.def(1)"·/a │e2│
-  | por e1 e2 ⇒ │e1│  a title="or" href="cic:/fakeuri.def(1)"+/a │e2│
-  | pstar e ⇒ │e│a title="star" href="cic:/fakeuri.def(1)"^/a*
+  | ppoint x ⇒ a href="cic:/matita/tutorial/chapter4/re.con(0,3,1)"char/a ? x 
+  | pconcat e1 e2 ⇒ |e1| a title="cat" href="cic:/fakeuri.def(1)"·/a |e2| 
+  | por e1 e2 ⇒ |e1|  a title="or" href="cic:/fakeuri.def(1)"+/a |e2|
+  | pstar e ⇒ |e|a title="star" href="cic:/fakeuri.def(1)"^/a*
   ].
 
-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 : a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"Alpha/a) (r : a href="cic:/matita/tutorial/chapter4/pitem.ind(1,0,1)"pitem/a S) on r : a href="cic:/matita/tutorial/chapter4/word.def(3)"word/a S → Prop ≝ 
 match r with
@@ -150,28 +145,27 @@ match r with
   | pepsilon ⇒ a title="empty lang" href="cic:/fakeuri.def(1)"∅/a
   | pchar _ ⇒ a title="empty lang" href="cic:/fakeuri.def(1)"∅/a
   | ppoint x ⇒ a title="sing lang" href="cic:/fakeuri.def(1)"{/a: xa title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a] } 
-  | pconcat pe1 pe2 ⇒ in_pl ? pe1 a title="cat lang" href="cic:/fakeuri.def(1)"·/a a title="in_l" href="cic:/fakeuri.def(1)"ℓ/a │pe2│  a title="union lang" href="cic:/fakeuri.def(1)"∪/a in_pl ? pe2 
+  | pconcat pe1 pe2 ⇒ in_pl ? pe1 a title="cat lang" href="cic:/fakeuri.def(1)"·/a a title="in_l" href="cic:/fakeuri.def(1)"\sem/a{|pe2|}  a title="union lang" href="cic:/fakeuri.def(1)"∪/a in_pl ? pe2 
   | por pe1 pe2 ⇒ in_pl ? pe1 a title="union lang" href="cic:/fakeuri.def(1)"∪/a in_pl ? pe2
-  | pstar pe ⇒ in_pl ? pe a title="cat lang" href="cic:/fakeuri.def(1)"·/a a title="in_l" href="cic:/fakeuri.def(1)"ℓ/a │pe│a title="star" href="cic:/fakeuri.def(1)"^/a*
+  | pstar pe ⇒ in_pl ? pe a title="cat lang" href="cic:/fakeuri.def(1)"·/a a title="in_l" href="cic:/fakeuri.def(1)"\sem/a{|pe|}a title="star lang" href="cic:/fakeuri.def(1)"^/a*
   ].
 
-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:a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"Alpha/a.a href="cic:/matita/basics/bool/bool.ind(1,0,0)" title="null"bool/a → a href="cic:/matita/tutorial/chapter4/word.def(3)"word/a S → Prop 
+definition eps: ∀S:a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"Alpha/a.a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a → a href="cic:/matita/tutorial/chapter4/word.def(3)"word/a S → Prop 
   ≝ λS,b. a href="cic:/matita/basics/bool/if_then_else.def(1)"if_then_else/a ? b a title="sing lang" href="cic:/fakeuri.def(1)"{/a: a title="nil" href="cic:/fakeuri.def(1)"[/a] } a title="empty lang" href="cic:/fakeuri.def(1)"∅/a.
 
-(* 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 : a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"Alpha/a.λp:a href="cic:/matita/tutorial/chapter4/pre.def(1)"pre/a S.  a title="in_pl" href="cic:/fakeuri.def(1)"ℓ/a (a title="fst" href="cic:/fakeuri.def(1)"\fst/a p) a title="union lang" href="cic:/fakeuri.def(1)"∪/a a title="epsilon lang" href="cic:/fakeuri.def(1)"ϵ/a_(a title="snd" href="cic:/fakeuri.def(1)"\snd/a p).
+definition in_prl ≝ λS : a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"Alpha/a.λp:a href="cic:/matita/tutorial/chapter4/pre.def(1)"pre/a S.  a title="in_pl" href="cic:/fakeuri.def(1)"\sem/a{a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a p} a title="union lang" href="cic:/fakeuri.def(1)"∪/a a title="epsilon lang" href="cic:/fakeuri.def(1)"ϵ/a_(a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a 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:a href="cic:/matita/tutorial/chapter4/pitem.ind(1,0,1)"pitem/a S. a title="logical not" href="cic:/fakeuri.def(1)"¬/a ((a title="in_pl" href="cic:/fakeuri.def(1)"ℓ/a pi) a title="nil" href="cic:/fakeuri.def(1)"[/a]).
-#S #pi (elim pi) normalize /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/Not.con(0,1,1)"nmk/a/span/span/
+lemma not_epsilon_lp :∀S.∀pi:a href="cic:/matita/tutorial/chapter4/pitem.ind(1,0,1)"pitem/a S.a title="logical not" href="cic:/fakeuri.def(1)"\neg/a(a title="nil" href="cic:/fakeuri.def(1)"[/a] a title="in_pl mem" href="cic:/fakeuri.def(1)"∈/a pi).
+#S #pi (elim pi) normalize /  span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/Not.con(0,1,1)"nmk/a/span/span/
   [#pi1 #pi2 #H1 #H2 % * /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/ * #w1 * #w2 * * #appnil 
    cases (a href="cic:/matita/tutorial/chapter3/nil_to_nil.def(5)"nil_to_nil/a … appnil) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/
   |#p11 #p12 #H1 #H2 % * /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/
@@ -179,23 +173,33 @@ lemma not_epsilon_lp :∀S.∀pi:a href="cic:/matita/tutorial/chapter4/pitem.in
   ]
 qed.
 
-lemma if_true_epsilon: ∀S.∀e:a href="cic:/matita/tutorial/chapter4/pre.def(1)"pre/a S. a title="snd" href="cic:/fakeuri.def(1)"\snd/a e a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → ((a title="in_prl" href="cic:/fakeuri.def(1)"ℓ/a e) a title="nil" href="cic:/fakeuri.def(1)"[/a]).
+lemma if_true_epsilon: ∀S.∀e:a href="cic:/matita/tutorial/chapter4/pre.def(1)"pre/a S. a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a e a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → (a title="nil" href="cic:/fakeuri.def(1)"[/a] a title="in_prl mem" href="cic:/fakeuri.def(1)"∈/a e).
 #S #e #H %2 >H // qed.
 
-lemma if_epsilon_true : ∀S.∀e:a href="cic:/matita/tutorial/chapter4/pre.def(1)"pre/a S. a title="nil" href="cic:/fakeuri.def(1)"[/a ] a title="in_prl mem" href="cic:/fakeuri.def(1)"∈/a e → a title="snd" href="cic:/fakeuri.def(1)"\snd/a e a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a.
-#S * #pi #b * [normalize #abs @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /2/] cases b normalize // @False_ind
+lemma if_epsilon_true : ∀S.∀e:a href="cic:/matita/tutorial/chapter4/pre.def(1)"pre/a S. a title="nil" href="cic:/fakeuri.def(1)"[/a ] a title="in_prl mem" href="cic:/fakeuri.def(1)"∈/a e → a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a e a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a.
+#S * #pi #b * [normalize #abs @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/] cases b normalize // @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a
 qed.
 
-definition lor ≝ λS:Alpha.λa,b:pre S.〈\fst a + \fst b,\snd a ∨ \snd b〉.
+definition lor ≝ λS:a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"Alpha/a.λa,b:a href="cic:/matita/tutorial/chapter4/pre.def(1)"pre/a S.a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a a a title="por" href="cic:/fakeuri.def(1)"+/a a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a b,a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a a a title="boolean or" href="cic:/fakeuri.def(1)"∨/a a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a 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:a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"Alpha/a.a href="cic:/matita/tutorial/chapter4/pitem.ind(1,0,1)"pitem/a S → a href="cic:/matita/tutorial/chapter4/pre.def(1)"pre/a S → a href="cic:/matita/tutorial/chapter4/pre.def(1)"pre/a S ≝
+ λS,i,e.a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai a title="pcat" href="cic:/fakeuri.def(1)"·/a a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e, a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a 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).