commit by user andrea

diff --git a/weblib/tutorial/chapter9.ma b/weblib/tutorial/chapter9.ma
index fb11216e53fb538d84099769257b5e77045687f2..c9a65f57b0935ee4774b84ce39f5f1767690f977 100644 (file)
--- a/weblib/tutorial/chapter9.ma
+++ b/weblib/tutorial/chapter9.ma
@@ -107,42 +107,42 @@ qed.
 
 notation > "x ↦* E" non associative with precedence 60 for @{moves ? $x $E}.
 
 
 notation > "x ↦* E" non associative with precedence 60 for @{moves ? $x $E}.
 

-let rec moves (S : DeqSet) w e on w : pre S ≝
+let rec moves (S : \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6) w e on w : \ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S ≝

  match w with
   [ nil ⇒ e
  match w with
   [ nil ⇒ e

-  | cons x w' ⇒ w' ↦* (move S x (\fst e))]. 
+  | cons x w' ⇒ w' ↦* (\ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"\ 6move\ 5/a\ 6 S x (\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e))]. 

 
 

-lemma moves_empty: ∀S:DeqSet.∀e:pre S. 
-  moves ? [ ] e = e.
+lemma moves_empty: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀e:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S. 
+  \ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 ? \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ] e \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 e.

 // qed.
 
 // qed.
 

-lemma moves_cons: ∀S:DeqSet.∀a:S.∀w.∀e:pre S. 
-  moves ? (a::w)  e = moves ? w (move S a (\fst e)).
+lemma moves_cons: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀a:S.∀w.∀e:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S. 
+  \ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 ? (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:w)  e \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 ? w (\ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"\ 6move\ 5/a\ 6 S a (\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e)).

 // qed.
 
 lemma moves_left : ∀S,a,w,e. 
 // qed.
 
 lemma moves_left : ∀S,a,w,e. 

-  moves S (w@[a]) e = move S a (\fst (moves S w e)). 
-#S #a #w elim w // #x #tl #Hind #e >moves_cons >moves_cons //
+  \ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 S (w\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6a]) e \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"\ 6move\ 5/a\ 6 S a (\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 S w e)). 
+#S #a #w elim w // #x #tl #Hind #e >\ 5a href="cic:/matita/tutorial/chapter9/moves_cons.def(8)"\ 6moves_cons\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter9/moves_cons.def(8)"\ 6moves_cons\ 5/a\ 6 //

 qed.
 
 qed.
 

-lemma not_epsilon_sem: ∀S:DeqSet.∀a:S.∀w: word S. ∀e:pre S. 
-  iff ((a::w) ∈ e) ((a::w) ∈ \fst e).
+lemma not_epsilon_sem: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀a:S.∀w: \ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S. ∀e:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S. 
+  \ 5a href="cic:/matita/basics/logic/iff.def(1)"\ 6iff\ 5/a\ 6 ((a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:w) \ 5a title="in_prl mem" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 e) ((a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:w) \ 5a title="in_pl mem" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 \ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e).

 #S #a #w * #i #b cases b normalize 
 #S #a #w * #i #b cases b normalize 

-  [% /2/ * // #H destruct |% normalize /2/]
+  [% /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ * // #H destruct |% normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/]

 qed.
 
 qed.
 

-lemma same_kernel_moves: ∀S:DeqSet.∀w.∀e:pre S.
-  |\fst (moves ? w e)| = |\fst e|.
+lemma same_kernel_moves: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀w.∀e:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.
+  \ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 ? w e)| \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e|.

 #S #w elim w //
 qed.
 
 #S #w elim w //
 qed.
 

-theorem decidable_sem: ∀S:DeqSet.∀w: word S. ∀e:pre S. 
-   (\snd (moves ? w e) = true) ↔ \sem{e} w.
+theorem decidable_sem: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀w: \ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S. ∀e:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S. 
+   (\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 ? w e) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6) \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e} w.

 #S #w elim w 
 #S #w elim w 

- [* #i #b >moves_empty cases b % /2/
- |#a #w1 #Hind #e >moves_cons
-  @iff_trans [||@iff_sym @not_epsilon_sem]
-  @iff_trans [||@move_ok] @Hind
+ [* #i #b >\ 5a href="cic:/matita/tutorial/chapter9/moves_empty.def(8)"\ 6moves_empty\ 5/a\ 6 cases b % /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/tutorial/chapter7/true_to_epsilon.def(9)"\ 6true_to_epsilon\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/\ 5span class="error" title="error location"\ 6\ 5/span\ 6 #H @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+ |#a #w1 #Hind #e >\ 5a href="cic:/matita/tutorial/chapter9/moves_cons.def(8)"\ 6moves_cons\ 5/a\ 6
+  @\ 5a href="cic:/matita/basics/logic/iff_trans.def(2)"\ 6iff_trans\ 5/a\ 6 [||@\ 5a href="cic:/matita/basics/logic/iff_sym.def(2)"\ 6iff_sym\ 5/a\ 6 @\ 5a href="cic:/matita/tutorial/chapter9/not_epsilon_sem.def(9)"\ 6not_epsilon_sem\ 5/a\ 6]
+  @\ 5a href="cic:/matita/basics/logic/iff_trans.def(2)"\ 6iff_trans\ 5/a\ 6 [||@\ 5a href="cic:/matita/tutorial/chapter9/move_ok.def(14)"\ 6move_ok\ 5/a\ 6] @Hind

  ]
 qed.
 
  ]
 qed.
 


@@ -158,7 +158,7 @@ Let us discuss a couple of examples.
 \ 5b\ 6Example\ 5/b\ 6. 
 Below is the DFA associated with the regular expression (ac+bc)*.
 
 \ 5b\ 6Example\ 5/b\ 6. 
 Below is the DFA associated with the regular expression (ac+bc)*.
 

-\ 5img src="http://www.cs.unibo.it/~asperti/FIGURES/acUbc.gif" alt="DFA for (ac+bc)"/\ 6  
+\ 5img src="http://www.cs.unibo.it/~asperti/FIGURES/acUbc.gif" alt="DFA for (ac+bc)"\ 6  

 
 The graphical description of the automaton is the traditional one, with nodes for 
 states and labelled arcs for transitions. Unreachable states are not shown.
 
 The graphical description of the automaton is the traditional one, with nodes for 
 states and labelled arcs for transitions. Unreachable states are not shown.


@@ -176,14 +176,13 @@ Let us consider a more complex case.
 \ 5b\ 6Example\ 5/b\ 6. 
 Starting form the regular expression (a+ϵ)(b*a + b)b, we obtain the following automaton.
 
 \ 5b\ 6Example\ 5/b\ 6. 
 Starting form the regular expression (a+ϵ)(b*a + b)b, we obtain the following automaton.
 

-\ 5img src="http://www.cs.unibo.it/~asperti/FIGURES/automaton.gif" alt="DFA for (a+ϵ)(b*a + b)b"/\ 6 
+\ 5img src="http://www.cs.unibo.it/~asperti/FIGURES/automaton.gif" alt="DFA for (a+ϵ)(b*a + b)b"\ 6 

 
 Remarkably, this DFA is minimal, testifying the small number of states produced by our 
 
 Remarkably, this DFA is minimal, testifying the small number of states produced by our 

-technique (the pair ofstates 6-8 and 7-9 differ for the fact that 6 and 7 
+technique (the pair of states 6-8 and 7-9 differ for the fact that 6 and 7 

 are final, while 8 and 9 are not). 
 are final, while 8 and 9 are not). 

-*) 

 
 

-(*
+

 \ 5h2\ 6Move to pit\ 5/h2\ 6. 
 
 We conclude this chapter with a few properties of the move opertions in relation
 \ 5h2\ 6Move to pit\ 5/h2\ 6. 
 
 We conclude this chapter with a few properties of the move opertions in relation