Changeset 3553

Timestamp:

Apr 10, 2015, 3:08:55 PM (5 years ago)

Author:

pellitta

Message:

inizio prima compilazione

File:

• LTS/imp.ma (modified) (5 diffs)

LTS/imp.ma

@@ -54 +54 @@
 
 (* is ex_falso in the standard libary? *)
-lemma ex_falso_quodlibet:∀P:Prop.False→ P.
-#P #F cases F qed.
+(*lemma ex_falso_quodlibet:∀P:Prop.False→ P.
+#P #F cases F qed.*)
+lemma ex_falso_quodlibet:False→ ∀P:Prop.P.
+#F cases F qed.
 
 (* what about this? *)
@@ -62 +64 @@
 
 lemma contradiction:∀P.P→¬P→ (∀A:Prop.A).
-#P #H #Hn #A @(ex_falso_quodlibet A (absurd P H Hn)) qed.
+#P #H #Hn #A @(ex_falso_quodlibet (absurd P H Hn)) qed.
 
 (*
@@ -75 +77 @@
 @(contradiction (?=?) (refl …) H) qed.
 
+lemma neq_bool:∀b1,b2.b1=(notb b2)→(b1≠b2).* * normalize #H /2 by sym_not_eq/ qed.
+
 lemma eqb_refl:∀T:DeqSet.∀t:T.(t==t)=true.
 #T #t @(\b ?) % qed. (* inversion(t==t) #H try(%) lapply(\Pf H) #ABS @(contradiction …) [@(t=t)|@refl|@ABS] qed.*)
@@ -80 +84 @@
 lemma eqb_sym:∀T:DeqSet.∀t1,t2:T.(t1==t2)=(t2==t1).
 #T #t1 #t2 inversion(t1==t2) #INV [lapply(\P INV)|lapply(\Pf INV)] #H [>H >eqb_refl %
-|elim H #H' inversion(t2==t1) #INV2 [lapply(\P INV2) #ABS destruct @(contradiction ((t1==t1)=true) INV2 ?)
+|inversion(t2==t1) #INV2 [lapply(\P INV2) #ABS destruct @(contradiction ((t1==t1)=true) INV2 ?)
 /2 by /|%] qed.
+
+lemma neq_refl_false:∀T.∀t:T.(t≠t)→ ∀P:Prop.P.
+#T #t #H @(contradiction (t=t) (refl …) H) qed.
+
+lemma neqb_refl_false:∀T:DeqSet.∀t:T.(t==t)=false→ ∀P:Prop.P.
+#T #t #ABS @(contradiction ((t==t)=true) (eqb_refl …) ?) @neq_bool whd in match(¬true);
+assumption qed.
 
 (* Syntax *)
@@ -559 +570 @@
 definition Lt:expr → expr → condition≝λe1,e2.Not (Geq e2 e1).
 
+(* Abitare tipo Program *)
+
+  (* Abitare tipo Instructions *)
+  
+definition imp_Instructions≝Instructions imp_state_params.
+
+definition imp_signature≝signature imp_state_params imp_state_params.
+
+check CallCostLabel
+
+definition imp_envitem:(env_item imp_env_params imp_instr_params)≝
 
 (* | mIfThenElse1: