commit by user andrea

[helm.git] / weblib / tutorial / chapter4.ma

diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma
index fd0f711443a8554f57061c1d22c4b39463a540e9..8649c4469a7f60cd6190d6b40442c2dc24c25c10 100644 (file)
--- a/weblib/tutorial/chapter4.ma
+++ b/weblib/tutorial/chapter4.ma
@@ -105,9 +105,7 @@ inductive pitem (S: \ 5a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"\ 6Alp
  | 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 test ≝ λS:Alpha.λe: pre S. match e with [mk_pair i b ⇒ e]. 
+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).
@@ -188,17 +186,11 @@ interpretation "oplus" 'oplus a b = (lor ? a 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 ]].
+interpretation "item concat" 'concat i e = (item_concat ? i e).
 
- | true ⇒ item_concat S i1 (bcast S e2)
-   ]
+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}.
@@ -753,4 +745,4 @@ ntheorem der1: ∀S,a,e,e',w. der S a e e' → in_l S w e' → in_l S (a::w) e.
      | #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