# HG changeset patch
# User wenzelm
# Date 1154552989 -7200
# Node ID 0f904a66eb75cca671888a667c10b09c67d0d763
# Parent  267917c7cec3c0e75babcd72a8d7d0587200c275
tuned proofs;

diff -r 267917c7cec3 -r 0f904a66eb75 src/HOL/Bali/DefiniteAssignmentCorrect.thy
--- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Wed Aug 02 22:27:08 2006 +0200
+++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Wed Aug 02 23:09:49 2006 +0200
@@ -4459,40 +4459,38 @@
   qed
 qed
 
-lemma da_good_approxE [consumes 4]:
-  "\<lbrakk>prg Env\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v, s1); Env\<turnstile>t\<Colon>T; Env\<turnstile> dom (locals (store s0)) \<guillemotright>t\<guillemotright> A;
-   wf_prog (prg Env);
-   \<lbrakk>normal s1 \<Longrightarrow> nrm A \<subseteq> dom (locals (store s1));
-     \<And> l. \<lbrakk>abrupt s1 = Some (Jump (Break l)); normal s0\<rbrakk>
-           \<Longrightarrow> brk A l \<subseteq> dom (locals (store s1));
-     \<lbrakk>abrupt s1 = Some (Jump Ret);normal s0\<rbrakk>\<Longrightarrow>Result \<in> dom (locals (store s1))
-   \<rbrakk> \<Longrightarrow> P
-  \<rbrakk> \<Longrightarrow> P"
-by (drule (3) da_good_approx) simp
+lemma da_good_approxE:
+  assumes
+    "prg Env\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v, s1)" and "Env\<turnstile>t\<Colon>T" and
+    "Env\<turnstile> dom (locals (store s0)) \<guillemotright>t\<guillemotright> A" and "wf_prog (prg Env)"
+  obtains
+    "normal s1 \<Longrightarrow> nrm A \<subseteq> dom (locals (store s1))" and
+    "\<And> l. \<lbrakk>abrupt s1 = Some (Jump (Break l)); normal s0\<rbrakk>
+           \<Longrightarrow> brk A l \<subseteq> dom (locals (store s1))" and
+    "\<lbrakk>abrupt s1 = Some (Jump Ret);normal s0\<rbrakk>\<Longrightarrow>Result \<in> dom (locals (store s1))"
+  using prems by - (drule (3) da_good_approx, simp)
 
 
 (* Same as above but with explicit environment; 
    It would be nicer to find a "normalized" way to right down those things
    in Bali.
 *)
-lemma da_good_approxE' [consumes 4]:
+lemma da_good_approxE':
   assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v, s1)"
      and    wt: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T"
      and    da: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile> dom (locals (store s0)) \<guillemotright>t\<guillemotright> A"
      and    wf: "wf_prog G"
-     and  elim: "\<lbrakk>normal s1 \<Longrightarrow> nrm A \<subseteq> dom (locals (store s1));
-                 \<And> l. \<lbrakk>abrupt s1 = Some (Jump (Break l)); normal s0\<rbrakk>
-                       \<Longrightarrow> brk A l \<subseteq> dom (locals (store s1));
-                  \<lbrakk>abrupt s1 = Some (Jump Ret);normal s0\<rbrakk>
-                  \<Longrightarrow>Result \<in> dom (locals (store s1))
-                 \<rbrakk> \<Longrightarrow> P"
-  shows "P"
+  obtains "normal s1 \<Longrightarrow> nrm A \<subseteq> dom (locals (store s1))" and
+    "\<And> l. \<lbrakk>abrupt s1 = Some (Jump (Break l)); normal s0\<rbrakk>
+                       \<Longrightarrow> brk A l \<subseteq> dom (locals (store s1))" and
+    "\<lbrakk>abrupt s1 = Some (Jump Ret);normal s0\<rbrakk>
+        \<Longrightarrow> Result \<in> dom (locals (store s1))"
 proof -
   from eval have "prg \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v, s1)" by simp
   moreover note wt da
   moreover from wf have "wf_prog (prg \<lparr>prg=G,cls=C,lcl=L\<rparr>)" by simp
-  ultimately show ?thesis
-    using elim by (rule da_good_approxE) iprover+
+  ultimately show thesis
+    using that by (rule da_good_approxE) iprover+
 qed
 
 ML {*