New equivalence proofs

--- a/src/HOL/Induct/Exp.ML	Thu May 08 12:22:01 1997 +0200
+++ b/src/HOL/Induct/Exp.ML	Fri May 09 10:17:41 1997 +0200
@@ -8,7 +8,8 @@
 
 open Exp;
 
-AddIs eval.intrs;
+AddSIs [eval.N, eval.X];
+AddIs  [eval.Op, eval.valOf];
 
 val eval_elim_cases = map (eval.mk_cases exp.simps)
    ["(N(n),sigma) -|-> (n',s')", "(X(x),sigma) -|-> (n,s')",
@@ -19,6 +20,13 @@
 AddSEs eval_elim_cases;
 
 
+goal thy "(X x, s[n/x]) -|-> (n, s[n/x])";
+by (rtac (assign_same RS subst) 1 THEN resolve_tac eval.intrs 1);
+qed "var_assign_eval";
+
+AddSIs [var_assign_eval];
+
+
 (** Make the induction rule look nicer -- though eta_contract makes the new
     version look worse than it is...**)
 
@@ -40,6 +48,7 @@
 \        |] ==> P (Op f e0 e1) s (f n0 n1) s1;                   \
 \     !!c e n s s0 s1.                                           \
 \        [| (c,s) -[eval Int {((e,s),(n,s')). P e s n s'}]-> s0; \
+\           (c,s) -[eval]-> s0;                                  \
 \           (e,s0) -|-> (n,s1); P e s0 n s1 |]                   \
 \        ==> P (VALOF c RESULTIS e) s n s1                       \
 \  |] ==> P e s n s'";
@@ -47,6 +56,7 @@
 by (blast_tac (!claset addIs prems) 1);
 by (blast_tac (!claset addIs prems) 1);
 by (blast_tac (!claset addIs prems) 1);
+by (forward_tac [impOfSubs (Int_lower1 RS exec_mono)] 1);
 by (fast_tac (!claset addIs prems addss (!simpset addsimps [split_lemma])) 1);
 qed "eval_induct";
 
@@ -89,7 +99,7 @@
 
 
 goal thy "!!x. (e,s) -|-> (v,s') ==> (e = N n) --> (v=n & s'=s)";
-by (etac eval.induct 1);
+by (etac eval_induct 1);
 by (ALLGOALS Asm_simp_tac);
 val lemma = result();
 bind_thm ("eval_N_E", refl RSN (2, lemma RS mp));
@@ -110,7 +120,7 @@
 \              (c' = WHILE e DO c) --> \
 \              (IF e THEN c;;c' ELSE SKIP, s) -[eval]-> t";
 by (etac exec.induct 1);
-by (ALLGOALS Asm_full_simp_tac);
+by (ALLGOALS Asm_simp_tac);
 by (ALLGOALS Blast_tac); 
 bind_thm ("while_if1", refl RSN (2, result() RS mp));
 
@@ -119,7 +129,7 @@
 \              (c' = IF e THEN c;;(WHILE e DO c) ELSE SKIP) --> \
 \              (WHILE e DO c, s) -[eval]-> t";
 by (etac exec.induct 1);
-by (ALLGOALS Asm_full_simp_tac);
+by (ALLGOALS Asm_simp_tac);
 by (ALLGOALS Blast_tac); 
 bind_thm ("while_if2", refl RSN (2, result() RS mp));
 
@@ -131,6 +141,34 @@
 
 
 
+(** Equivalence of  (IF e THEN c1 ELSE c2);;c
+               and  IF e THEN (c1;;c) ELSE (c2;;c)   **)
+
+goal thy "!!x. (c',s) -[eval]-> t ==> \
+\              (c' = (IF e THEN c1 ELSE c2);;c) --> \
+\              (IF e THEN (c1;;c) ELSE (c2;;c), s) -[eval]-> t";
+by (etac exec.induct 1);
+by (ALLGOALS Asm_simp_tac);
+by (Blast_tac 1); 
+bind_thm ("if_semi1", refl RSN (2, result() RS mp));
+
+
+goal thy "!!x. (c',s) -[eval]-> t ==> \
+\              (c' = IF e THEN (c1;;c) ELSE (c2;;c)) --> \
+\              ((IF e THEN c1 ELSE c2);;c, s) -[eval]-> t";
+by (etac exec.induct 1);
+by (ALLGOALS Asm_simp_tac);
+by (ALLGOALS Blast_tac); 
+bind_thm ("if_semi2", refl RSN (2, result() RS mp));
+
+
+goal thy "(((IF e THEN c1 ELSE c2);;c, s) -[eval]-> t)  =  \
+\         ((IF e THEN (c1;;c) ELSE (c2;;c), s) -[eval]-> t)";
+by (blast_tac (!claset addIs [if_semi1, if_semi2]) 1);
+qed "if_semi";
+
+
+
 (** Equivalence of  VALOF c1 RESULTIS (VALOF c2 RESULTIS e)
                and  VALOF c1;;c2 RESULTIS e
  **)
@@ -138,20 +176,18 @@
 goal thy "!!x. (e',s) -|-> (v,s') ==> \
 \              (e' = VALOF c1 RESULTIS (VALOF c2 RESULTIS e)) --> \
 \              (VALOF c1;;c2 RESULTIS e, s) -|-> (v,s')";
-by (etac eval.induct 1);
-by (ALLGOALS Asm_full_simp_tac);
-(*The destruction rule below replaces (c,s)-[eval Int ...]->t by 
-   (c,s)-[eval]->t.  The new induction rule might include this assumption*)
-by (blast_tac (!claset addSDs [impOfSubs (Int_lower1 RS exec_mono)]) 1);
+by (etac eval_induct 1);
+by (ALLGOALS Asm_simp_tac);
+by (Blast_tac 1); 
 bind_thm ("valof_valof1", refl RSN (2, result() RS mp));
 
 
 goal thy "!!x. (e',s) -|-> (v,s') ==> \
 \              (e' = VALOF c1;;c2 RESULTIS e) --> \
 \              (VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) -|-> (v,s')";
-by (etac eval.induct 1);
-by (ALLGOALS Asm_full_simp_tac);
-by (blast_tac (!claset addSDs [impOfSubs (Int_lower1 RS exec_mono)]) 1);
+by (etac eval_induct 1);
+by (ALLGOALS Asm_simp_tac);
+by (Blast_tac 1); 
 bind_thm ("valof_valof2", refl RSN (2, result() RS mp));
 
 
@@ -160,3 +196,44 @@
 by (blast_tac (!claset addIs [valof_valof1, valof_valof2]) 1);
 qed "valof_valof";
 
+
+
+(** Equivalence of  VALOF SKIP RESULTIS e  and  e **)
+
+
+goal thy "!!x. (e',s) -|-> (v,s') ==> \
+\              (e' = VALOF SKIP RESULTIS e) --> \
+\              (e, s) -|-> (v,s')";
+by (etac eval_induct 1);
+by (ALLGOALS Asm_simp_tac);
+by (Blast_tac 1); 
+bind_thm ("valof_skip1", refl RSN (2, result() RS mp));
+
+goal thy "!!x. (e,s) -|-> (v,s') ==> (VALOF SKIP RESULTIS e, s) -|-> (v,s')";
+by (Blast_tac 1);
+qed "valof_skip2";
+
+goal thy "((VALOF SKIP RESULTIS e, s) -|-> (v,s'))  =  ((e, s) -|-> (v,s'))";
+by (blast_tac (!claset addIs [valof_skip1, valof_skip2]) 1);
+qed "valof_skip";
+
+
+
+(** Equivalence of  VALOF x:=e RESULTIS x  and  e **)
+
+goal thy "!!x. (e',s) -|-> (v,s'') ==> \
+\              (e' = VALOF x:=e RESULTIS X x) --> \
+\              (EX s'. (e, s) -|-> (v,s') & (s'' = s'[v/x]))";
+by (etac eval_induct 1);
+by (ALLGOALS Asm_simp_tac);
+by (thin_tac "?PP-->?QQ" 1);
+by (Step_tac 1);
+by (Simp_tac 1);
+by (Blast_tac 1); 
+bind_thm ("valof_assign1", refl RSN (2, result() RS mp));
+
+
+goal thy "!!x. (e,s) -|-> (v,s') ==> \
+\              (VALOF x:=e RESULTIS X x, s) -|-> (v,s'[v/x])";
+by (Blast_tac 1);
+qed "valof_assign2";