X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdidactic%2Finduction.ma;h=aa7b7aff6d7a742d4ac5359bb34434c890b0ba64;hb=f0643b9fd4160f49c0d368855d0e3e638f2d58ca;hp=99a0e8a5a07b55768b5266f4a799f3de965e4419;hpb=a4e18d465037106982d84a85194c4593dad530b8;p=helm.git

diff --git a/helm/software/matita/contribs/didactic/induction.ma b/helm/software/matita/contribs/didactic/induction.ma
index 99a0e8a5a..aa7b7aff6 100644
--- a/helm/software/matita/contribs/didactic/induction.ma
+++ b/helm/software/matita/contribs/didactic/induction.ma
@@ -30,7 +30,7 @@ Come scrivere i simboli
 =======================
 
 Per inserire i simboli matematici è necessario digitare il loro nome
-e poi premere CTRL-L. In generale i nomi dei simboli sono della forma
+e poi premere ALT-L. In generale i nomi dei simboli sono della forma
 `\nome`, ad esempio `\equiv`. Alcuni simboli molto frequenti hanno
 dei sinonimi più comodi da digitare, per esemio `⇒` ha sia il nome
 `\Rightarrow` sia `=>`.
@@ -46,7 +46,7 @@ l'intera lista dal menù a tendina `View ▹ TeX/UTF8 table`.
 * `≡` : `\equiv`
 * `∀` : `\forall`
 
-La sintassi `∀v.P` significa "per tutti i `v` vale `P`".
+La sintassi `∀x.P` significa "per tutti gli `x` vale `P`".
 
 La sintassi `F → G` dove `F` e `G` sono proposizioni nel metalinguaggio
 significa "`F` implica `G`". Attenzione, il simbolo `⇒` (usato a lezione)
@@ -221,14 +221,15 @@ interpretation "Semantic of Formula" 'semantics v a = (sem v a).
    definizione di `sem` e prima di continuare è necessario che la sistemiate.   
 *)
 definition v1101 ≝ λx.
-      if eqb x 0 then 1  (* Atom 0 ↦ 1 *)
- else if eqb x 1 then 1  (* Atom 1 ↦ 1 *)
- else if eqb x 2 then 0  (* Atom 2 ↦ 0 *)
- else if eqb x 3 then 1  (* Atom 3 ↦ 1 *)
- else                 0. (* Atom _ ↦ 0 *) 
+      if eqb x 0 then 1  (* FAtom 0 ↦ 1 *)
+ else if eqb x 1 then 1  (* FAtom 1 ↦ 1 *)
+ else if eqb x 2 then 0  (* FAtom 2 ↦ 0 *)
+ else if eqb x 3 then 1  (* FAtom 3 ↦ 1 *)
+ else                 0. (* FAtom _ ↦ 0 *) 
 
 
-definition esempio1 ≝ (FImpl (FAtom 3) (FOr (FAtom 2) (FAnd (FAtom 1) (FAtom 0)))).
+definition esempio1 ≝ 
+  (FImpl (FNot (FAtom 3)) (FOr (FAtom 2) (FAnd (FAtom 1) (FAtom 0)))).
 
 eval normalize on [[ esempio1 ]]_v1101.
 
@@ -252,8 +253,6 @@ let rec subst (x:nat) (G: Formula) (F: Formula) on F ≝
   | FNot F ⇒ FNot (subst x G F)
   ].
 
-(* AGGIUNGERE ALCUNI TEST *)
-
 
 (* NOTA
    ====
@@ -285,6 +284,25 @@ notation "hvbox(a \nbsp break mstyle color #0000ff (≡) \nbsp b)"  non associat
 notation > "a ≡ b" non associative with precedence 50 for @{ equiv $a $b }.
 interpretation "equivalence for Formulas" 'equivF a b = (equiv a b).
 
+(* Test 2
+   ======
+   
+   Viene fornita una formula di esempio `esempio2`,
+   e una formula `esempio3` che rimpiazzerà gli atomi
+   `FAtom 2` di `esempio2`.
+   
+   Il risultato atteso è la formula:
+   
+        FAnd (FImpl (FOr (FAtom O) (FAtom 1)) (FAtom 1)) 
+             (FOr (FAtom O) (FAtom 1))
+   
+*)
+
+definition esempio2 ≝ (FAnd (FImpl (FAtom 2) (FAtom 1)) (FAtom 2)). 
+   
+definition esempio3 ≝ (FOr (FAtom 0) (FAtom 1)).
+
+eval normalize on (esempio2 [ esempio3 / 2]).
 
 (*DOCBEGIN
    
@@ -346,8 +364,9 @@ Tale linguaggio è composto dai seguenti comandi:
 
   Quando la tesi è della forma `P = Q`, si possono utilizzare delle ipotesi
   della forma `A = B` riscrivendo `A` in `B` (o viceversa) in `P`. Per esempio
-  se la tesi fosse `sin π + 3 = 3` e si avesse una ipotesi `sin π = 0` dal
-  nome `H`, si potrebbe usare il comando `conclude (0 + 3) = 3 by H`.
+  se la tesi fosse `sin π + 3 = 7 - 4` e si avesse una ipotesi `sin π = 0` dal
+  nome `H`, si potrebbe usare il comando `conclude (sin π + 3) = (0 + 3) by H`
+  per cambiare la conclusione in `0 + 3 = 7 - 4`.
 
 * `= (P) by name`