X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdidactic%2Fexercises%2Fsubstitution.ma;h=db83cfef8cd43346cdfc43daf7ebaed3b442be8b;hb=e78cf74f8976cf0ca554f64baa9979d0423ee927;hp=8ac8fbc1e96223fc8904d29462aa6842d80bae38;hpb=c6094ab9349aaa41a8c29c5773a3e756ac819e7f;p=helm.git

diff --git a/helm/software/matita/library/didactic/exercises/substitution.ma b/helm/software/matita/library/didactic/exercises/substitution.ma
index 8ac8fbc1e..db83cfef8 100644
--- a/helm/software/matita/library/didactic/exercises/substitution.ma
+++ b/helm/software/matita/library/didactic/exercises/substitution.ma
@@ -192,10 +192,10 @@ let rec sem (v: nat → nat) (F: Formula) on F ≝
    Un esempio di espressione è `eqb n m`, che confronta i due numeri naturali
    `n` ed `m`. 
    
-   * [[ formula ]]_v
+   * [[ formula ]]v
    
    Questa notazione utilizza la funzione `sem` precedentemente definita, in 
-   particolare `[[ f ]]_v` è una abbreviazione per `sem v f`.
+   particolare `[[ f ]]v` è una abbreviazione per `sem v f`.
 
 
    ATTENZIONE
@@ -206,10 +206,10 @@ 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 }.
-interpretation "Formula if_then_else" 'if_then_else e t f = (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 }.
-notation > "[[ term 19 a ]]_ term 90 v" non associative with precedence 90 for @{ sem $v $a }.
+notation > "[[ term 19 a ]] term 90 v" non associative with precedence 90 for @{ sem $v $a }.
 interpretation "Semantic of Formula" 'semantics v a = (sem v a).
 
 
@@ -229,7 +229,7 @@ interpretation "Semantic of Formula" 'semantics v a = (sem v a).
    
    Tale formula è valida per la funzione di valutazione `v1101`. 
    
-   Il comando `eval normalize [[ esempio1 ]]_v1101` permette di calcolare
+   Il comando `eval normalize [[ esempio1 ]]v1101` permette di calcolare
    la funzione `sem` che avete appena definito. Tale funzione deve 
    computare a 1 (verrà mostrata una finestra col risultato).
    Se così non fosse significa che avete commesso un errore nella 
@@ -248,7 +248,7 @@ definition esempio1 ≝
 
 (* Decommenta ed esegui. *)
 
-(* eval normalize on [[ esempio1 ]]_v1101. *)
+(* eval normalize on [[ esempio1 ]]v1101. *)
 
 
 (* Esercizio 3
@@ -283,7 +283,7 @@ let rec subst (x:nat) (G: Formula) (F: Formula) on F ≝
   
   * F ≡ G
   
-  Questa notazione è una abbreviazione per `∀v.[[ f ]]_v = [[ g ]]_v`. 
+  Questa notazione è una abbreviazione per `∀v.[[ f ]]v = [[ g ]]v`. 
   Asserisce che for ogni funzione di valutazione `v`, la semantica di `f`
   in `v` è uguale alla semantica di `g` in `v`.
 
@@ -296,7 +296,7 @@ let rec subst (x:nat) (G: Formula) (F: Formula) on F ≝
 notation < "t [ \nbsp term 19 a / term 19 b \nbsp ]" non associative with precedence 90 for @{ 'substitution $b $a $t }.
 notation > "t [ term 90 a / term 90 b]" non associative with precedence 90 for @{ 'substitution $b $a $t }.
 interpretation "Substitution for Formula" 'substitution b a t = (subst b a t).
-definition equiv ≝ λF1,F2. ∀v.[[ F1 ]]_v = [[ F2 ]]_v.
+definition equiv ≝ λF1,F2. ∀v.[[ F1 ]]v = [[ F2 ]]v.
 notation "hvbox(a \nbsp break mstyle color #0000ff (≡) \nbsp b)"  non associative with precedence 45 for @{ 'equivF $a $b }.
 notation > "a ≡ b" non associative with precedence 50 for @{ equiv $a $b }.
 interpretation "equivalence for Formulas" 'equivF a b = (equiv a b).
@@ -417,16 +417,16 @@ case FBot.
   the thesis becomes (FBot[ G1/x ] ≡ FBot[ G2/x ]).
   the thesis becomes (FBot ≡ FBot[ G2/x ]).
   the thesis becomes (FBot ≡ FBot).
-  the thesis becomes (∀v.[[FBot]]_v = [[FBot]]_v).
+  the thesis becomes (∀v.[[FBot]]v = [[FBot]]v).
   assume v : (ℕ → ℕ).
-  the thesis becomes (0 = [[FBot]]_v).
+  the thesis becomes (0 = [[FBot]]v).
   the thesis becomes (0 = 0).
   done.  
 case FTop.
   (*BEGIN*)
   the thesis becomes (FTop[ G1/x ] ≡ FTop[ G2/x ]).
   the thesis becomes (FTop ≡ FTop).
-  the thesis becomes (∀v. [[FTop]]_v = [[FTop]]_v).
+  the thesis becomes (∀v. [[FTop]]v = [[FTop]]v).
   assume v : (ℕ → ℕ).
   the thesis becomes (1 = 1).
   (*END*)
@@ -448,7 +448,7 @@ case FAtom.
   case false.
     (*BEGIN*)
     the thesis becomes (FAtom n ≡ FAtom n).
-    the thesis becomes (∀v. [[FAtom n]]_v = [[FAtom n]]_v).
+    the thesis becomes (∀v. [[FAtom n]]v = [[FAtom n]]v).
     assume v : (ℕ → ℕ).
     the thesis becomes (v n = v n).
     (*END*)
@@ -459,19 +459,19 @@ case FAnd.
   assume F2 : Formula.
   by induction hypothesis we know (F2[ G1/x ] ≡ F2[ G2/x ]) (IH2).    
   the thesis becomes 
-    (∀v.[[ (FAnd F1 F2)[ G1/x ] ]]_v = [[ (FAnd F1 F2)[ G2/x ] ]]_v).
+    (∀v.[[ (FAnd F1 F2)[ G1/x ] ]]v = [[ (FAnd F1 F2)[ G2/x ] ]]v).
   assume v : (ℕ → ℕ). 
   the thesis becomes 
-    (min ([[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v) = 
-     min ([[ F1[ G2/x ] ]]_v) ([[ F2[ G2/x ] ]]_v)).
-  by IH1 we proved (∀v1.[[ F1[ G1/x ] ]]_v1 = [[ F1[ G2/x ] ]]_v1) (IH11).
-  by (*BEGIN*)IH2(*END*) we proved (∀v2.[[ F2[ G1/x ] ]]_v2 = [[ F2[ G2/x ] ]]_v2) (IH22).
-  by IH11 we proved ([[ F1[ G1/x ] ]]_v = [[ F1[ G2/x ] ]]_v) (IH111).
-  by (*BEGIN*)IH22(*END*) we proved ([[ F2[ G1/x ] ]]_v = [[ F2[ G2/x ] ]]_v) (IH222).
+    (min ([[ F1[ G1/x ] ]]v) ([[ F2[ G1/x ] ]]v) = 
+     min ([[ F1[ G2/x ] ]]v) ([[ F2[ G2/x ] ]]v)).
+  by IH1 we proved (∀v1.[[ F1[ G1/x ] ]]v1 = [[ F1[ G2/x ] ]]v1) (IH11).
+  by (*BEGIN*)IH2(*END*) we proved (∀v2.[[ F2[ G1/x ] ]]v2 = [[ F2[ G2/x ] ]]v2) (IH22).
+  by IH11 we proved ([[ F1[ G1/x ] ]]v = [[ F1[ G2/x ] ]]v) (IH111).
+  by (*BEGIN*)IH22(*END*) we proved ([[ F2[ G1/x ] ]]v = [[ F2[ G2/x ] ]]v) (IH222).
   conclude 
-      (min ([[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) 
-    = (min ([[ F1[ G2/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) by IH111.
-    = (min ([[(F1[ G2/x ])]]_v) ([[(F2[ G2/x ])]]_v)) by (*BEGIN*)IH222(*END*).
+      (min ([[ F1[ G1/x ] ]]v) ([[ F2[ G1/x ] ]]v)) 
+    = (min ([[ F1[ G2/x ] ]]v) ([[ F2[ G1/x ] ]]v)) by IH111.
+    = (min ([[(F1[ G2/x ])]]v) ([[(F2[ G2/x ])]]v)) by (*BEGIN*)IH222(*END*).
   (*END*)
   done.
 case FOr.
@@ -481,19 +481,19 @@ case FOr.
   assume F2 : Formula.
   by induction hypothesis we know (F2[ G1/x ] ≡ F2[ G2/x ]) (IH2).    
   the thesis becomes 
-    (∀v.[[ (FOr F1 F2)[ G1/x ] ]]_v = [[ (FOr F1 F2)[ G2/x ] ]]_v).
+    (∀v.[[ (FOr F1 F2)[ G1/x ] ]]v = [[ (FOr F1 F2)[ G2/x ] ]]v).
   assume v : (ℕ → ℕ). 
   the thesis becomes 
-    (max ([[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v) = 
-     max ([[ F1[ G2/x ] ]]_v) ([[ F2[ G2/x ] ]]_v)).
-  by IH1 we proved (∀v1.[[ F1[ G1/x ] ]]_v1 = [[ F1[ G2/x ] ]]_v1) (IH11).
-  by IH2 we proved (∀v2.[[ F2[ G1/x ] ]]_v2 = [[ F2[ G2/x ] ]]_v2) (IH22).
-  by IH11 we proved ([[ F1[ G1/x ] ]]_v = [[ F1[ G2/x ] ]]_v) (IH111).
-  by IH22 we proved ([[ F2[ G1/x ] ]]_v = [[ F2[ G2/x ] ]]_v) (IH222).
+    (max ([[ F1[ G1/x ] ]]v) ([[ F2[ G1/x ] ]]v) = 
+     max ([[ F1[ G2/x ] ]]v) ([[ F2[ G2/x ] ]]v)).
+  by IH1 we proved (∀v1.[[ F1[ G1/x ] ]]v1 = [[ F1[ G2/x ] ]]v1) (IH11).
+  by IH2 we proved (∀v2.[[ F2[ G1/x ] ]]v2 = [[ F2[ G2/x ] ]]v2) (IH22).
+  by IH11 we proved ([[ F1[ G1/x ] ]]v = [[ F1[ G2/x ] ]]v) (IH111).
+  by IH22 we proved ([[ F2[ G1/x ] ]]v = [[ F2[ G2/x ] ]]v) (IH222).
   conclude 
-      (max ([[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) 
-    = (max ([[ F1[ G2/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) by IH111.
-    = (max ([[(F1[ G2/x ])]]_v) ([[(F2[ G2/x ])]]_v)) by IH222.
+      (max ([[ F1[ G1/x ] ]]v) ([[ F2[ G1/x ] ]]v)) 
+    = (max ([[ F1[ G2/x ] ]]v) ([[ F2[ G1/x ] ]]v)) by IH111.
+    = (max ([[(F1[ G2/x ])]]v) ([[(F2[ G2/x ])]]v)) by IH222.
   (*END*)
   done.
 case FImpl.
@@ -503,30 +503,30 @@ case FImpl.
   assume F2 : Formula.
   by induction hypothesis we know (F2[ G1/x ] ≡ F2[ G2/x ]) (IH2).
   the thesis becomes 
-    (∀v.max (1 - [[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v) =
-        max (1 - [[ F1[ G2/x ] ]]_v) ([[ F2[ G2/x ] ]]_v)).
+    (∀v.max (1 - [[ F1[ G1/x ] ]]v) ([[ F2[ G1/x ] ]]v) =
+        max (1 - [[ F1[ G2/x ] ]]v) ([[ F2[ G2/x ] ]]v)).
   assume v : (ℕ → ℕ).       
-  by IH1 we proved ([[ F1[ G1/x ] ]]_v = [[ F1[ G2/x ] ]]_v) (IH11).
-  by IH2 we proved ([[ F2[ G1/x ] ]]_v = [[ F2[ G2/x ] ]]_v) (IH22).
+  by IH1 we proved ([[ F1[ G1/x ] ]]v = [[ F1[ G2/x ] ]]v) (IH11).
+  by IH2 we proved ([[ F2[ G1/x ] ]]v = [[ F2[ G2/x ] ]]v) (IH22).
   conclude 
-      (max (1-[[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v))
-    = (max (1-[[ F1[ G2/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) by IH11.  
-    = (max (1-[[ F1[ G2/x ] ]]_v) ([[ F2[ G2/x ] ]]_v)) by IH22.
+      (max (1-[[ F1[ G1/x ] ]]v) ([[ F2[ G1/x ] ]]v))
+    = (max (1-[[ F1[ G2/x ] ]]v) ([[ F2[ G1/x ] ]]v)) by IH11.  
+    = (max (1-[[ F1[ G2/x ] ]]v) ([[ F2[ G2/x ] ]]v)) by IH22.
   done. 
 case FNot.
   (*BEGIN*)
   assume F1 : Formula.
   by induction hypothesis we know (F1[ G1/x ] ≡ F1[ G2/x ]) (IH).   
   the thesis becomes (FNot (F1[ G1/x ]) ≡ FNot (F1[ G2/x ])).
-  the thesis becomes (∀v.[[FNot (F1[ G1/x ])]]_v = [[FNot (F1[ G2/x ])]]_v).
+  the thesis becomes (∀v.[[FNot (F1[ G1/x ])]]v = [[FNot (F1[ G2/x ])]]v).
   assume v : (ℕ → ℕ).
-  the thesis becomes (1 - [[F1[ G1/x ]]]_v = [[FNot (F1[ G2/x ])]]_v).
-  the thesis becomes (1 - [[ F1[ G1/x ] ]]_v = 1 - [[ F1[ G2/x ] ]]_v).
-  by IH we proved (∀v1.[[ F1[	 G1/x ] ]]_v1 = [[ F1[ G2/x ] ]]_v1) (IH1).
-  by IH1 we proved ([[ F1[ G1/x ] ]]_v = [[ F1[ G2/x ] ]]_v) (IH2).
+  the thesis becomes (1 - [[F1[ G1/x ]]]v = [[FNot (F1[ G2/x ])]]v).
+  the thesis becomes (1 - [[ F1[ G1/x ] ]]v = 1 - [[ F1[ G2/x ] ]]v).
+  by IH we proved (∀v1.[[ F1[	 G1/x ] ]]v1 = [[ F1[ G2/x ] ]]v1) (IH1).
+  by IH1 we proved ([[ F1[ G1/x ] ]]v = [[ F1[ G2/x ] ]]v) (IH2).
   conclude 
-      (1-[[ F1[ G1/x ] ]]_v) 
-    = (1-[[ F1[ G2/x ] ]]_v) by IH2.
+      (1-[[ F1[ G1/x ] ]]v) 
+    = (1-[[ F1[ G2/x ] ]]v) by IH2.
   (*END*)
   done.
 qed.