# HG changeset patch
# User paulson
# Date 863086921 -7200
# Node ID 04b0d8941365e460a16940ac5b23d01c4f064b3f
# Parent  d60e49b86c6a2a4e8cf1f9d305971552e91211f1
New proofs about WHILE and VALOF

diff -r d60e49b86c6a -r 04b0d8941365 src/HOL/Induct/Exp.ML
--- a/src/HOL/Induct/Exp.ML	Thu May 08 11:44:59 1997 +0200
+++ b/src/HOL/Induct/Exp.ML	Thu May 08 12:22:01 1997 +0200
@@ -8,6 +8,8 @@
 
 open Exp;
 
+AddIs eval.intrs;
+
 val eval_elim_cases = map (eval.mk_cases exp.simps)
    ["(N(n),sigma) -|-> (n',s')", "(X(x),sigma) -|-> (n,s')",
     "(Op f a1 a2,sigma)  -|-> (n,s')",
@@ -84,3 +86,77 @@
 by (ALLGOALS (full_simp_tac (!simpset addsimps [Unique_def])));
 by (ALLGOALS Blast_tac);
 qed "Function_eval";
+
+
+goal thy "!!x. (e,s) -|-> (v,s') ==> (e = N n) --> (v=n & s'=s)";
+by (etac eval.induct 1);
+by (ALLGOALS Asm_simp_tac);
+val lemma = result();
+bind_thm ("eval_N_E", refl RSN (2, lemma RS mp));
+
+AddSEs [eval_N_E];
+
+
+(*This theorem says that "WHILE TRUE DO c" cannot terminate*)
+goal thy "!!x. (c', s) -[eval]-> t ==> (c' = WHILE (N 0) DO c) --> False";
+by (etac exec.induct 1);
+by (Auto_tac());
+bind_thm ("while_true_E", refl RSN (2, result() RS mp));
+
+
+(** Equivalence of IF e THEN c;;(WHILE e DO c) ELSE SKIP  and  WHILE e DO c **)
+
+goal thy "!!x. (c',s) -[eval]-> t ==> \
+\              (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 Blast_tac); 
+bind_thm ("while_if1", refl RSN (2, result() RS mp));
+
+
+goal thy "!!x. (c',s) -[eval]-> t ==> \
+\              (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 Blast_tac); 
+bind_thm ("while_if2", refl RSN (2, result() RS mp));
+
+
+goal thy "((IF e THEN c;;(WHILE e DO c) ELSE SKIP, s) -[eval]-> t)  =  \
+\         ((WHILE e DO c, s) -[eval]-> t)";
+by (blast_tac (!claset addIs [while_if1, while_if2]) 1);
+qed "while_if";
+
+
+
+(** Equivalence of  VALOF c1 RESULTIS (VALOF c2 RESULTIS e)
+               and  VALOF c1;;c2 RESULTIS e
+ **)
+
+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);
+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);
+bind_thm ("valof_valof2", refl RSN (2, result() RS mp));
+
+
+goal thy "((VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) -|-> (v,s'))  =  \
+\         ((VALOF c1;;c2 RESULTIS e, s) -|-> (v,s'))";
+by (blast_tac (!claset addIs [valof_valof1, valof_valof2]) 1);
+qed "valof_valof";
+