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
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).
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
(* Decommenta ed esegui. *)
-(* eval normalize on [[ esempio1 ]]_v1101. *)
+(* eval normalize on [[ esempio1 ]]v1101. *)
(* Esercizio 3
* 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`.
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).
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*)
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*)
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.
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.
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.