...

[helm.git] / helm / software / matita / contribs / didactic / induction.ma

diff --git a/helm/software/matita/contribs/didactic/induction.ma b/helm/software/matita/contribs/didactic/induction.ma
index bc52a8246f2521c3e1b5483ad2f87ef259e24a51..e2da2243ac90ede12b9d3be50969659b8fd71481 100644 (file)
--- a/helm/software/matita/contribs/didactic/induction.ma
+++ b/helm/software/matita/contribs/didactic/induction.ma
@@ -1,4 +1,16 @@
 (* Esercitazione di logica 22/10/2008. *)
+
+(* Nota per gli studenti
+   =====================
+
+   * La lezione del pomeriggio con il Prof. Sacerdoti si terrà in aula 
+     Pinkerle e non Cremona.
+
+   * Un piccolo manuale sul software Matita è disponibile al seguente URL:
+
+       http://mowgli.cs.unibo.it/~tassi/exercise-induction.ma.html 
+
+*)
    
 (* Esercizio 0 
    ===========
@@ -21,7 +33,10 @@
    
    * salvare il file (menu `File ▹ Save as ...`) nella directory (cartella)
      /public/ con nome linguaggi_Account1.ma, ad esempio Mario Rossi, il cui
-     account è mrossi deve salvare il file in /public/linguaggi_mrossi.ma
+     account è mrossi, deve salvare il file in /public/linguaggi_mrossi.ma
+
+   * mandatevi via email o stampate il file. Per stampare potete usare
+     usare l'editor gedit che offre la funzionalità di stampa
 *)
 
 (*DOCBEGIN
@@ -190,7 +205,7 @@ let rec sem (v: nat → nat) (F: Formula) on F ≝
 *)
 definition if_then_else ≝ λT:Type.λe,t,f.match e return λ_.T with [ true ⇒ t | false ⇒ f].
 notation > "'if' term 19 e 'then' term 19 t 'else' term 90 f" non associative with precedence 90 for @{ 'if_then_else $e $t $f }.
-notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 90 f \nbsp" non associative with precedence 90 for @{ 'if_then_else _ $e $t $f }.
+notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 90 f \nbsp" non associative with precedence 90 for @{ 'if_then_else $e $t $f }.
 interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else _ e t f).
 notation < "[[ \nbsp term 19 a \nbsp ]] \nbsp \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }.
 notation > "[[ term 19 a ]] \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }.
@@ -221,14 +236,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 +268,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 +299,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