From f3e11860b6138abb22a2449eb7eeb3818248c875 Mon Sep 17 00:00:00 2001
From: matitaweb <claudio.sacerdoticoen@unibo.it>
Date: Wed, 9 Nov 2011 08:44:23 +0000
Subject: [PATCH] commit by user andrea

---
 weblib/tutorial/chapter4.ma | 74 ++++++++++++++++++++++++++++++++-----
 1 file changed, 64 insertions(+), 10 deletions(-)

diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma
index 79b6bafff..21a7a6c0e 100644
--- a/weblib/tutorial/chapter4.ma
+++ b/weblib/tutorial/chapter4.ma
@@ -69,19 +69,19 @@ definition cat : ∀S,l1,l2,w.Prop ≝
   λS.λl1,l2.λw:a href="cic:/matita/tutorial/chapter4/word.def(3)"word/a S.a title="exists" href="cic:/fakeuri.def(1)"∃/aw1,w2.w1 a title="append" href="cic:/fakeuri.def(1)"@/a w2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a w a title="logical and" href="cic:/fakeuri.def(1)"∧/a l1 w1 a title="logical and" href="cic:/fakeuri.def(1)"∧/a l2 w2.
 interpretation "cat lang" 'concat a b = (cat ? a b).
 
-definition star ≝ λ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 ? l).
+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
  [ zero ⇒ a title="empty lang" href="cic:/fakeuri.def(1)"∅/a 
  | epsilon ⇒ a title="sing lang" href="cic:/fakeuri.def(1)"{/a: a title="nil" href="cic:/fakeuri.def(1)"[/a] }
- |  char 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] }
- | concat r1 r2 ⇒ ℓ r1 a title="cat lang" href="cic:/fakeuri.def(1)"·/a ℓ r2 
- | or r1 r2 ⇒ ℓ r1 a title="union lang" href="cic:/fakeuri.def(1)"∪/a ℓ r2 
- | star r1 ⇒ (ℓ r1)a title="star lang" href="cic:/fakeuri.def(1)"^/a* 
+ | char 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] }
+ | concat r1 r2 ⇒ in_l ? r1 a title="cat lang" href="cic:/fakeuri.def(1)"·/a in_l ? r2 
+ | or r1 r2 ⇒ in_l ? r1 a title="union lang" href="cic:/fakeuri.def(1)"∪/a in_l ? r2 
+ | 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}.
@@ -131,11 +131,65 @@ let rec forget (S: a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"Alph
   | 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* 
+  | pstar e ⇒ │e│a title="star" href="cic:/fakeuri.def(1)"^/a*
   ].
 
-notation < "|term 19 e|" non associative with precedence 70 for @{'forget $e}.
+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}.
+
+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
+  [ pzero ⇒ a title="empty lang" href="cic:/fakeuri.def(1)"∅/a 
+  | 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 
+  | 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*
+  ].
+
+interpretation "in_pl" 'in_l E = (in_pl ? E).
+interpretation "in_pl mem" 'mem w l = (in_pl ? l w).
+
+definition epsilon ≝ λS,b.if b then { ([ ] : word S) } else {}.
+
+interpretation "epsilon" 'epsilon = (epsilon ?).
+notation < "ϵ b" non associative with precedence 90 for @{'app_epsilon $b}.
+interpretation "epsilon lang" 'app_epsilon b = (epsilon ? b).
+
+ndefinition in_prl ≝ λS : Alpha.λp:pre S.  𝐋\p (\fst p) ∪ ϵ (\snd p).
+  
+interpretation "in_prl mem" 'mem w l = (in_prl ? l w).
+interpretation "in_prl" 'in_pl E = (in_prl ? E).
+
+nlemma append_eq_nil : ∀S.∀w1,w2:word S. w1 @ w2 = [ ] → w1 = [ ].
+#S w1; nelim w1; //. #x tl IH w2; nnormalize; #abs; ndestruct; nqed.
+
+(* lemma 12 *)
+nlemma epsilon_in_true : ∀S.∀e:pre S. [ ] ∈ e ↔ \snd e = true.
+#S r; ncases r; #e b; @; ##[##2: #H; nrewrite > H; @2; /2/; ##] ncases b;//; 
+nnormalize; *; ##[##2:*] nelim e;
+##[ ##1,2: *; ##| #c; *; ##| #c; nnormalize; #; ndestruct; ##| ##7: #p H;
+##| #r1 r2 H G; *; ##[##2: /3/ by or_intror]
+##| #r1 r2 H1 H2; *; /3/ by or_intror, or_introl; ##]
+*; #w1; *; #w2; *; *; #defw1; nrewrite > (append_eq_nil … w1 w2 …); /3/ by {};//;
+nqed.
+
+nlemma not_epsilon_lp : ∀S:Alpha.∀e:pitem S. ¬ ((𝐋\p e) [ ]).
+#S e; nelim e; nnormalize; /2/ by nmk;
+##[ #; @; #; ndestruct;
+##| #r1 r2 n1 n2; @; *; /2/; *; #w1; *; #w2; *; *; #H;
+    nrewrite > (append_eq_nil …H…); /2/;
+##| #r1 r2 n1 n2; @; *; /2/;
+##| #r n; @; *; #w1; *; #w2; *; *; #H;     
+    nrewrite > (append_eq_nil …H…); /2/;##]
+nqed.
+
+ndefinition lo ≝ λS:Alpha.λ
\ No newline at end of file
-- 
2.39.2