X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Ftutorial%2Fchapter9.ma;h=147bad1b9dd656b11c23d0c783dadcca5b89c9e6;hb=01ce59a8a53aad0e7375fcc76125842382480a59;hp=c9a65f57b0935ee4774b84ce39f5f1767690f977;hpb=6248fe356b55750c565ef7f36a40e593338a3c43;p=helm.git

diff --git a/weblib/tutorial/chapter9.ma b/weblib/tutorial/chapter9.ma
index c9a65f57b..147bad1b9 100644
--- a/weblib/tutorial/chapter9.ma
+++ b/weblib/tutorial/chapter9.ma
@@ -121,7 +121,7 @@ lemma moves_cons: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"
 // qed.
 
 lemma moves_left : ∀S,a,w,e. 
-  a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a S (wa title="append" href="cic:/fakeuri.def(1)"@/aa title="cons" href="cic:/fakeuri.def(1)"[/aa]) e a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a S a (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a S w e)). 
+  a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a S (wa title="append" href="cic:/fakeuri.def(1)"@/a(aa title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a])) e a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a S a (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a S w e)). 
 #S #a #w elim w // #x #tl #Hind #e >a href="cic:/matita/tutorial/chapter9/moves_cons.def(8)"moves_cons/a >a href="cic:/matita/tutorial/chapter9/moves_cons.def(8)"moves_cons/a //
 qed.
 
@@ -186,65 +186,65 @@ are final, while 8 and 9 are not).
 h2Move to pit/h2. 
 
 We conclude this chapter with a few properties of the move opertions in relation
-with the pit state. *).
+with the pit state. *)
 
-definition pit_pre ≝ λS.λi.〈blank S (|i|), false〉. 
+definition pit_pre ≝ λS.λi.a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter8/blank.fix(0,1,3)"blank/a S (a title="forget" href="cic:/fakeuri.def(1)"|/ai|), a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a〉. 
 
-(* The following function compute if a symbol in S occurs in a given
-item i *).
+(* The following function compute the list of characters occurring in a given
+item i. *)
 
-let rec occur (S: DeqSet) (i: re S) on i ≝  
+let rec occur (S: a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a) (i: a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"re/a S) on i ≝  
   match i with
-  [ z ⇒ [ ]
-  | e ⇒ [ ]
-  | s y ⇒ [y]
-  | o e1 e2 ⇒ unique_append ? (occur S e1) (occur S e2) 
-  | c e1 e2 ⇒ unique_append ? (occur S e1) (occur S e2) 
+  [ z ⇒ a title="nil" href="cic:/fakeuri.def(1)"[/a ]
+  | e ⇒ a title="nil" href="cic:/fakeuri.def(1)"[/a ]
+  | s y ⇒ ya title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]
+  | o e1 e2 ⇒ a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"unique_append/a ? (occur S e1) (occur S e2) 
+  | c e1 e2 ⇒ a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"unique_append/a ? (occur S e1) (occur S e2) 
   | k e ⇒ occur S e].
 
 (* If a symbol a does not occur in i, then move(i,a) gets to the
-pit state. *).
+pit state. *)
 
-lemma not_occur_to_pit: ∀S,a.∀i:pitem S. memb S a (occur S (|i|)) ≠ true →
-  move S a i  = pit_pre S i.
+lemma not_occur_to_pit: ∀S,a.∀i:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S. a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a (a href="cic:/matita/tutorial/chapter9/occur.fix(0,1,6)"occur/a S (a title="forget" href="cic:/fakeuri.def(1)"|/ai|)) a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a →
+  a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a S a i  a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"pit_pre/a S i.
 #S #a #i elim i //
-  [#x normalize cases (a==x) normalize // #H @False_ind /2/
-  |#i1 #i2 #Hind1 #Hind2 #H >move_cat 
-   >Hind1 [2:@(not_to_not … H) #H1 @sublist_unique_append_l1 //]
-   >Hind2 [2:@(not_to_not … H) #H1 @sublist_unique_append_l2 //] //
-  |#i1 #i2 #Hind1 #Hind2 #H >move_plus 
-   >Hind1 [2:@(not_to_not … H) #H1 @sublist_unique_append_l1 //]
-   >Hind2 [2:@(not_to_not … H) #H1 @sublist_unique_append_l2 //] //
-  |#i #Hind #H >move_star >Hind // 
+  [#x normalize cases (aa title="eqb" href="cic:/fakeuri.def(1)"=/a=x) normalize // #H @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/
+  |#i1 #i2 #Hind1 #Hind2 #H >a href="cic:/matita/tutorial/chapter9/move_cat.def(7)"move_cat/a 
+   >Hind1 [2:@(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … H) #H1 @a href="cic:/matita/tutorial/chapter5/sublist_unique_append_l1.def(6)"sublist_unique_append_l1/a //]
+   >Hind2 [2:@(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … H) #H1 @a href="cic:/matita/tutorial/chapter5/sublist_unique_append_l2.def(6)"sublist_unique_append_l2/a //] //
+  |#i1 #i2 #Hind1 #Hind2 #H >a href="cic:/matita/tutorial/chapter9/move_plus.def(7)"move_plus/a 
+   >Hind1 [2:@(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … H) #H1 @a href="cic:/matita/tutorial/chapter5/sublist_unique_append_l1.def(6)"sublist_unique_append_l1/a //]
+   >Hind2 [2:@(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … H) #H1 @a href="cic:/matita/tutorial/chapter5/sublist_unique_append_l2.def(6)"sublist_unique_append_l2/a //] //
+  |#i #Hind #H >a href="cic:/matita/tutorial/chapter9/move_star.def(7)"move_star/a >Hind // 
   ]
 qed.
 
-(* We cannot escape form the pit state. *).
+(* We cannot escape form the pit state. *)
 
-lemma move_pit: ∀S,a,i. move S a (\fst (pit_pre S i)) = pit_pre S i.
+lemma move_pit: ∀S,a,i. a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a S a (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"pit_pre/a S i)) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"pit_pre/a S i.
 #S #a #i elim i //
-  [#i1 #i2 #Hind1 #Hind2 >move_cat >Hind1 >Hind2 // 
-  |#i1 #i2 #Hind1 #Hind2 >move_plus >Hind1 >Hind2 // 
-  |#i #Hind >move_star >Hind //
+  [#i1 #i2 #Hind1 #Hind2 >a href="cic:/matita/tutorial/chapter9/move_cat.def(7)"move_cat/a >Hind1 >Hind2 // 
+  |#i1 #i2 #Hind1 #Hind2 >a href="cic:/matita/tutorial/chapter9/move_plus.def(7)"move_plus/a >Hind1 >Hind2 // 
+  |#i #Hind >a href="cic:/matita/tutorial/chapter9/move_star.def(7)"move_star/a >Hind //
   ]
 qed. 
 
-lemma moves_pit: ∀S,w,i. moves S w (pit_pre S i) = pit_pre S i.
+lemma moves_pit: ∀S,w,i. a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a S w (a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"pit_pre/a S i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"pit_pre/a S i.
 #S #w #i elim w // 
 qed. 
  
 (* If any character in w does not occur in i, then moves(i,w) gets
-to the pit state. *).
+to the pit state. *)
 
-lemma to_pit: ∀S,w,e. ¬ sublist S w (occur S (|\fst e|)) →
- moves S w e = pit_pre S (\fst e).
+lemma to_pit: ∀S,w,e. a title="logical not" href="cic:/fakeuri.def(1)"¬/a a href="cic:/matita/tutorial/chapter5/sublist.def(5)"sublist/a S w (a href="cic:/matita/tutorial/chapter9/occur.fix(0,1,6)"occur/a S (a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e|)) →
+ a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a S w e a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"pit_pre/a S (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e).
 #S #w elim w
-  [#e * #H @False_ind @H normalize #a #abs @False_ind /2/
-  |#a #tl #Hind #e #H cases (true_or_false (memb S a (occur S (|\fst e|))))
-    [#Htrue >moves_cons whd in ⊢ (???%); <(same_kernel … a) 
-     @Hind >same_kernel @(not_to_not … H) #H1 #b #memb cases (orb_true_l … memb)
+  [#e * #H @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a @H normalize #a #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/
+  |#a #tl #Hind #e #H cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a (a href="cic:/matita/tutorial/chapter9/occur.fix(0,1,6)"occur/a S (a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e|))))
+    [#Htrue >a href="cic:/matita/tutorial/chapter9/moves_cons.def(8)"moves_cons/a whd in ⊢ (???%); <(a href="cic:/matita/tutorial/chapter9/same_kernel.def(8)"same_kernel/a … a) 
+     @Hind >a href="cic:/matita/tutorial/chapter9/same_kernel.def(8)"same_kernel/a @(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … H) #H1 #b #memb cases (a href="cic:/matita/basics/bool/orb_true_l.def(2)"orb_true_l/a … memb)
       [#H2 >(\P H2) // |#H2 @H1 //]
-    |#Hfalse >moves_cons >not_occur_to_pit // >Hfalse /2/ 
+    |#Hfalse >a href="cic:/matita/tutorial/chapter9/moves_cons.def(8)"moves_cons/a >a href="cic:/matita/tutorial/chapter9/not_occur_to_pit.def(8)"not_occur_to_pit/a // >Hfalse /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/bool/eqnot_to_noteq.def(4)"eqnot_to_noteq/a/span/span/ 
     ]
   ]
 qed.
\ No newline at end of file