--- 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";