From 8421cc771e2a316e028b6dab25bdacb8f8cd6c2b Mon Sep 17 00:00:00 2001 From: matitaweb Date: Wed, 9 Nov 2011 09:34:13 +0000 Subject: [PATCH] commit by user andrea --- weblib/tutorial/chapter4.ma | 23 +++++++++++++++-------- 1 file changed, 15 insertions(+), 8 deletions(-) diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma index 21a7a6c0e..77e42066e 100644 --- a/weblib/tutorial/chapter4.ma +++ b/weblib/tutorial/chapter4.ma @@ -158,18 +158,23 @@ match r with 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 {}. +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 + ≝ λ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 = (epsilon ? b). +(* interpretation "epsilon" 'epsilon = (epsilon ?). *) +notation "ϵ _ b" non associative with precedence 90 for @{'app_epsilon $b}. +interpretation "epsilon lang" 'app_epsilon b = (eps ? b). -ndefinition in_prl ≝ λS : Alpha.λp:pre S. 𝐋\p (\fst p) ∪ ϵ (\snd 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)"ℓ/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). interpretation "in_prl mem" 'mem w l = (in_prl ? l w). -interpretation "in_prl" 'in_pl E = (in_prl ? E). +interpretation "in_prl" 'in_l 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 /2/ + [#pi1 #pi2 #H1 #H2 % * /2/ * #w1 * #w2 * * /2/; -nlemma append_eq_nil : ∀S.∀w1,w2:word S. w1 @ w2 = [ ] → w1 = [ ]. +lemma 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 *) @@ -192,4 +197,6 @@ nlemma not_epsilon_lp : ∀S:Alpha.∀e:pitem S. ¬ ((𝐋\p e) [ ]). nrewrite > (append_eq_nil …H…); /2/;##] nqed. -ndefinition lo ≝ λS:Alpha.λ \ No newline at end of file +ndefinition lo ≝ λS:Alpha.λ + + -- 2.39.2