# HG changeset patch
# User wenzelm
# Date 1182456616 -7200
# Node ID d1b97708d5ebe1d91735c894b88b2f2fb34c73e8
# Parent  886655a150f6a044fc8cb05289344e8bf1e58355
tuned proofs -- avoid implicit prems;

diff -r 886655a150f6 -r d1b97708d5eb src/CCL/Fix.thy
--- a/src/CCL/Fix.thy	Thu Jun 21 20:48:48 2007 +0200
+++ b/src/CCL/Fix.thy	Thu Jun 21 22:10:16 2007 +0200
@@ -181,9 +181,10 @@
   done
 
 lemma term_ind:
-  assumes "P(bot)" "P(true)" "P(false)"
-    "!!x y.[| P(x);  P(y) |] ==> P(<x,y>)"
-    "!!u.(!!x. P(u(x))) ==> P(lam x. u(x))"  "INCL(P)"
+  assumes 1: "P(bot)" and 2: "P(true)" and 3: "P(false)"
+    and 4: "!!x y.[| P(x);  P(y) |] ==> P(<x,y>)"
+    and 5: "!!u.(!!x. P(u(x))) ==> P(lam x. u(x))"
+    and 6: "INCL(P)"
   shows "P(t)"
   apply (rule reachability [THEN id_apply, THEN subst])
   apply (rule_tac x = t in spec)
@@ -191,12 +192,12 @@
     apply (unfold idgen_def)
     apply (rule allI)
     apply (subst applyBbot)
-    apply assumption
+    apply (rule 1)
    apply (rule allI)
    apply (rule applyB [THEN ssubst])
     apply (rule_tac t = "xa" in term_case)
        apply simp_all
-       apply (fast intro: prems INCL_subst all_INCL)+
+       apply (fast intro: assms INCL_subst all_INCL)+
   done
 
 end
diff -r 886655a150f6 -r d1b97708d5eb src/CCL/Wfd.thy
--- a/src/CCL/Wfd.thy	Thu Jun 21 20:48:48 2007 +0200
+++ b/src/CCL/Wfd.thy	Thu Jun 21 22:10:16 2007 +0200
@@ -340,7 +340,11 @@
   apply (rule 3)
     apply (rule 1 [symmetric])
   apply (rule rcall2T)
-      apply assumption+
+      apply (rule 2)
+     apply assumption
+    apply (rule 4)
+   apply (rule 5)
+  apply (rule 6)
   done
 
 lemma hyprcall3T:
@@ -355,7 +359,12 @@
   apply (rule 3)
    apply (rule 1 [symmetric])
   apply (rule rcall3T)
-  apply assumption+
+       apply (rule 2)
+      apply assumption
+     apply (rule 4)
+    apply (rule 5)
+   apply (rule 6)
+  apply (rule 7)
   done
 
 lemmas hyprcallTs = hyprcallT hyprcall2T hyprcall3T
diff -r 886655a150f6 -r d1b97708d5eb src/CTT/CTT.thy
--- a/src/CTT/CTT.thy	Thu Jun 21 20:48:48 2007 +0200
+++ b/src/CTT/CTT.thy	Thu Jun 21 22:10:16 2007 +0200
@@ -397,13 +397,13 @@
 
 (*Simplify the parameter of a unary type operator.*)
 lemma subst_eqtyparg:
-  assumes "a=c : A"
-    and "!!z. z:A ==> B(z) type"
+  assumes 1: "a=c : A"
+    and 2: "!!z. z:A ==> B(z) type"
   shows "B(a)=B(c)"
 apply (rule subst_typeL)
 apply (rule_tac [2] refl_type)
-apply (rule prems)
-apply assumption
+apply (rule 1)
+apply (erule 2)
 done
 
 (*Simplification rules for Constructive Type Theory*)
diff -r 886655a150f6 -r d1b97708d5eb src/HOL/MicroJava/BV/BVNoTypeError.thy
--- a/src/HOL/MicroJava/BV/BVNoTypeError.thy	Thu Jun 21 20:48:48 2007 +0200
+++ b/src/HOL/MicroJava/BV/BVNoTypeError.thy	Thu Jun 21 22:10:16 2007 +0200
@@ -159,8 +159,8 @@
   obtain apTs where
     "ST = (rev apTs) @ ys" and "length apTs = length fpTs"
   proof -
-    have "ST = rev (rev xs) @ ys" by simp
-    with xs show ?thesis by - (rule that, assumption, simp)
+    from xs(1) have "ST = rev (rev xs) @ ys" by simp
+    then show thesis by (rule that) (simp add: xs(2))
   qed
   moreover
   from l xs obtain X ST' where "ys = X#ST'" by (auto simp add: neq_Nil_conv)
@@ -244,7 +244,7 @@
       phi:    "Phi C sig ! pc = Some (ST,LT)" and
       frame:  "correct_frame G hp (ST,LT) maxl ins (stk,loc,C,sig,pc)" and
       frames: "correct_frames G hp Phi rT sig frs'"
-      by (auto simp add: correct_state_def)
+      by (auto simp add: correct_state_def) (rule that)
 
     from frame obtain
       stk: "approx_stk G hp stk ST" and
@@ -427,15 +427,18 @@
 
 corollary no_type_errors_initial:
   fixes G ("\<Gamma>") and Phi ("\<Phi>")
-  assumes "wt_jvm_prog \<Gamma> \<Phi>"  
-  assumes "is_class \<Gamma> C" "method (\<Gamma>,C) (m,[]) = Some (C, b)" "m \<noteq> init"
+  assumes wt: "wt_jvm_prog \<Gamma> \<Phi>"  
+  assumes is_class: "is_class \<Gamma> C"
+    and method: "method (\<Gamma>,C) (m,[]) = Some (C, b)"
+    and m: "m \<noteq> init"
   defines start: "s \<equiv> start_state \<Gamma> C m"
 
-  assumes "\<Gamma> \<turnstile> (Normal s) -jvmd\<rightarrow> t" 
+  assumes s: "\<Gamma> \<turnstile> (Normal s) -jvmd\<rightarrow> t" 
   shows "t \<noteq> TypeError"
 proof -
-  have "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>" by (unfold start, rule BV_correct_initial)
-  thus ?thesis by - (rule no_type_errors)
+  from wt is_class method have "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
+    unfolding start by (rule BV_correct_initial)
+  from wt this s show ?thesis by (rule no_type_errors)
 qed
 
 text {*
@@ -445,20 +448,27 @@
 *} 
 corollary welltyped_commutes:
   fixes G ("\<Gamma>") and Phi ("\<Phi>")
-  assumes "wt_jvm_prog \<Gamma> \<Phi>" and "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>" 
+  assumes wt: "wt_jvm_prog \<Gamma> \<Phi>" and *: "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>" 
   shows "\<Gamma> \<turnstile> (Normal s) -jvmd\<rightarrow> (Normal t) = \<Gamma> \<turnstile> s -jvm\<rightarrow> t"
-  by rule (erule defensive_imp_aggressive,rule welltyped_aggressive_imp_defensive)
-
+  apply rule
+   apply (erule defensive_imp_aggressive, rule welltyped_aggressive_imp_defensive)
+    apply (rule wt)
+   apply (rule *)
+  apply assumption
+  done
 
 corollary welltyped_initial_commutes:
   fixes G ("\<Gamma>") and Phi ("\<Phi>")
-  assumes "wt_jvm_prog \<Gamma> \<Phi>"  
-  assumes "is_class \<Gamma> C" "method (\<Gamma>,C) (m,[]) = Some (C, b)" "m \<noteq> init"
+  assumes wt: "wt_jvm_prog \<Gamma> \<Phi>"  
+  assumes is_class: "is_class \<Gamma> C"
+    and method: "method (\<Gamma>,C) (m,[]) = Some (C, b)"
+    and m: "m \<noteq> init"
   defines start: "s \<equiv> start_state \<Gamma> C m"
   shows "\<Gamma> \<turnstile> (Normal s) -jvmd\<rightarrow> (Normal t) = \<Gamma> \<turnstile> s -jvm\<rightarrow> t"
 proof -
-  have "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>" by (unfold start, rule BV_correct_initial)
-  thus ?thesis by  - (rule welltyped_commutes)
+  from wt is_class method have "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
+    unfolding start by (rule BV_correct_initial)
+  with wt show ?thesis by (rule welltyped_commutes)
 qed
  
 end  
diff -r 886655a150f6 -r d1b97708d5eb src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Thu Jun 21 20:48:48 2007 +0200
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Thu Jun 21 22:10:16 2007 +0200
@@ -572,7 +572,7 @@
       show ?thesis by (rule that)
     qed (insert xp', auto) -- "the other instructions don't generate exceptions"
 
-    from state' meth hp_ok "class" frames phi_pc' frame' 
+    from state' meth hp_ok "class" frames phi_pc' frame' prehp
     have ?thesis by (unfold correct_state_def) simp
   }
   ultimately
@@ -830,7 +830,7 @@
     is_class_C: "is_class G C" and
     frame:   "correct_frame G hp s maxl ins (stk, loc, C, sig, pc)" and
     frames:  "correct_frames G hp phi rT sig frs"
-    by (clarsimp simp add: correct_state_def iff del: not_None_eq)
+    by (auto iff del: not_None_eq simp add: correct_state_def)
 
   from ins wti phi_pc
   obtain apTs X ST LT D' rT body where 
@@ -972,8 +972,15 @@
   qed
 
   from state'_val heap_ok mD'' ins method phi_pc s X' l mX
-       frames s' LT0 c_f is_class_C stk' oX_Addr frame prealloc
-  show ?thesis by (simp add: correct_state_def) (intro exI conjI, blast)
+       frames s' LT0 c_f is_class_C stk' oX_Addr frame prealloc and l
+  show ?thesis
+    apply (simp add: correct_state_def)
+    apply (intro exI conjI)
+       apply blast
+      apply (rule l)
+     apply (rule mX)
+    apply (rule mD)
+    done
 qed
 
 lemmas [simp del] = map_append
diff -r 886655a150f6 -r d1b97708d5eb src/HOL/MicroJava/BV/EffectMono.thy
--- a/src/HOL/MicroJava/BV/EffectMono.thy	Thu Jun 21 20:48:48 2007 +0200
+++ b/src/HOL/MicroJava/BV/EffectMono.thy	Thu Jun 21 22:10:16 2007 +0200
@@ -291,7 +291,7 @@
   
   note [simp] = eff_def
 
-  hence "G \<turnstile> (Some s1) <=' (Some s2)" by simp
+  with G have "G \<turnstile> (Some s1) <=' (Some s2)" by simp
   from this app2
   have app1: "app i G m rT pc et (Some s1)" by (rule app_mono)
 
@@ -439,4 +439,3 @@
 lemmas [iff del] = not_Err_eq
 
 end
-
diff -r 886655a150f6 -r d1b97708d5eb src/HOL/MicroJava/BV/Kildall.thy
--- a/src/HOL/MicroJava/BV/Kildall.thy	Thu Jun 21 20:48:48 2007 +0200
+++ b/src/HOL/MicroJava/BV/Kildall.thy	Thu Jun 21 22:10:16 2007 +0200
@@ -58,15 +58,15 @@
   assume l:  "p < length ss"
   assume "?steptype (p'#ps')"
   then obtain a b where
-    p': "p'=(a,b)" and ab: "a<n" "b\<in>A" and "?steptype ps'"
-    by (cases p', auto)
+    p': "p'=(a,b)" and ab: "a<n" "b\<in>A" and ps': "?steptype ps'"
+    by (cases p') auto
   assume "\<And>ss. p< length ss \<Longrightarrow> ss \<in> list n A \<Longrightarrow> ?steptype ps' \<Longrightarrow> ?P ss ps'"
-  hence IH: "\<And>ss. ss \<in> list n A \<Longrightarrow> p < length ss \<Longrightarrow> ?P ss ps'" .
+  from this [OF _ _ ps'] have IH: "\<And>ss. ss \<in> list n A \<Longrightarrow> p < length ss \<Longrightarrow> ?P ss ps'" .
 
   from ss ab
   have "ss[a := b +_f ss!a] \<in> list n A" by (simp add: closedD)
   moreover
-  from calculation
+  from calculation l
   have "p < length (ss[a := b +_f ss!a])" by simp
   ultimately
   have "?P (ss[a := b +_f ss!a]) ps'" by (rule IH)
@@ -254,7 +254,7 @@
  apply (cases "q \<in> w")
   apply simp
   apply (rule ub1')
-     apply assumption
+     apply (rule semilat)
     apply clarify
     apply (rule pres_typeD)
        apply assumption
@@ -447,7 +447,9 @@
 apply(case_tac "iter f step ss0 (unstables r step ss0)")
 apply(simp)
 apply (rule iter_properties)
-by (simp_all add: unstables_def stable_def)
+apply (simp_all add: unstables_def stable_def)
+apply (rule semilat)
+done
 
 
 lemma is_bcv_kildall: includes semilat
diff -r 886655a150f6 -r d1b97708d5eb src/HOL/MicroJava/BV/LBVComplete.thy
--- a/src/HOL/MicroJava/BV/LBVComplete.thy	Thu Jun 21 20:48:48 2007 +0200
+++ b/src/HOL/MicroJava/BV/LBVComplete.thy	Thu Jun 21 22:10:16 2007 +0200
@@ -346,7 +346,7 @@
   with s_phi pc phi_pc have wt_s_phi: "wtc c pc s <=_r wtc c pc (\<phi>!pc)" by (rule wtc_mono)
   with wt_phi have wt_s: "wtc c pc s \<noteq> \<top>" by simp
   moreover
-  assume s: "s \<noteq> \<top>" 
+  assume s': "s \<noteq> \<top>" 
   ultimately
   have "ls = [] \<Longrightarrow> ?wtl (i#ls) pc s \<noteq> \<top>" by simp
   moreover {
@@ -357,23 +357,23 @@
     moreover
     from cert suc_pc have "c!pc \<in> A" "c!(pc+1) \<in> A" 
       by (auto simp add: cert_ok_def)
-    with pres have "wtc c pc s \<in> A" by (rule wtc_pres)
+    from pres this s pc have "wtc c pc s \<in> A" by (rule wtc_pres)
     ultimately
     have "?wtl ls (Suc pc) (wtc c pc s) \<noteq> \<top>" using IH wt_s by blast
-    with s wt_s have "?wtl (i#ls) pc s \<noteq> \<top>" by simp 
+    with s' wt_s have "?wtl (i#ls) pc s \<noteq> \<top>" by simp
   }
   ultimately show "?wtl (i#ls) pc s \<noteq> \<top>" by (cases ls) blast+
 qed
 
   
 theorem (in lbvc) wtl_complete:
-  assumes "wt_step r \<top> step \<phi>"
-  assumes "s <=_r \<phi>!0" and "s \<in> A" and "s \<noteq> \<top>" and "length ins = length phi"
+  assumes wt: "wt_step r \<top> step \<phi>"
+    and s: "s <=_r \<phi>!0" "s \<in> A" "s \<noteq> \<top>"
+    and len: "length ins = length phi"
   shows "wtl ins c 0 s \<noteq> \<top>"
-proof -  
-  have "0+length ins = length phi" by simp
-  thus ?thesis by - (rule wt_step_wtl_lemma)
+proof -
+  from len have "0+length ins = length phi" by simp
+  from wt this s show ?thesis by (rule wt_step_wtl_lemma)
 qed
 
-
 end
diff -r 886655a150f6 -r d1b97708d5eb src/HOL/MicroJava/BV/LBVJVM.thy
--- a/src/HOL/MicroJava/BV/LBVJVM.thy	Thu Jun 21 20:48:48 2007 +0200
+++ b/src/HOL/MicroJava/BV/LBVJVM.thy	Thu Jun 21 22:10:16 2007 +0200
@@ -89,7 +89,7 @@
   let ?A    = "states G mxs mxr"
 
   have "semilat (JVMType.sl G mxs mxr)" 
-    by (rule semilat_JVM_slI, rule wf_prog_ws_prog)
+    by (rule semilat_JVM_slI, rule wf_prog_ws_prog, rule wf)
   hence "semilat (?A, ?r, ?f)" by (unfold sl_triple_conv)
   moreover
   have "top ?r Err"  by (simp add: JVM_le_unfold)
@@ -110,7 +110,7 @@
   have "cert_ok cert (length ins) Err (OK None) ?A" 
     by (unfold wt_lbv_def) (auto dest: check_certD)
   moreover
-  have "pres_type ?step (length ins) ?A" by (rule exec_pres_type)
+  from wf have "pres_type ?step (length ins) ?A" by (rule exec_pres_type)
   moreover
   let ?start = "OK (Some ([],(OK (Class C))#(map OK pTs)@(replicate mxl Err)))"
   from lbv
@@ -221,7 +221,7 @@
     by (simp (asm_lr) add: wt_method_def2)
   
   have "semilat (JVMType.sl G mxs ?mxr)" 
-    by (rule semilat_JVM_slI, rule wf_prog_ws_prog)
+    by (rule semilat_JVM_slI) (rule wf_prog_ws_prog [OF wf])
   hence "semilat (?A, ?r, ?f)" by (unfold sl_triple_conv)
   moreover
   have "top ?r Err"  by (simp add: JVM_le_unfold)
@@ -242,7 +242,7 @@
     by (rule wf_prog_ws_prog [THEN exec_mono])
   hence "mono ?r ?step (length ?phi) ?A" by (simp add: length)
   moreover
-  have "pres_type ?step (length ins) ?A" by (rule exec_pres_type)
+  from wf have "pres_type ?step (length ins) ?A" by (rule exec_pres_type)
   hence "pres_type ?step (length ?phi) ?A" by (simp add: length)
   moreover
   from ck_types
diff -r 886655a150f6 -r d1b97708d5eb src/HOL/Nominal/Examples/Class.thy
--- a/src/HOL/Nominal/Examples/Class.thy	Thu Jun 21 20:48:48 2007 +0200
+++ b/src/HOL/Nominal/Examples/Class.thy	Thu Jun 21 22:10:16 2007 +0200
@@ -6077,7 +6077,7 @@
   finally show "(ImpR (z).<c>.M d){x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* (ImpR (z).<c>.M d)[x\<turnstile>n>y]" using fs by simp
 next
   case (ImpL c M u N v x a y)
-  have fs: "c\<sharp>x" "c\<sharp>a" "c\<sharp>y" "u\<sharp>x" "u\<sharp>a" "u\<sharp>y" "c\<sharp>N" "c\<sharp>v" "u\<sharp>M" "u\<sharp>v" by fact
+  have fs: "c\<sharp>x" "c\<sharp>a" "c\<sharp>y" "u\<sharp>x" "u\<sharp>a" "u\<sharp>y" "c\<sharp>N" "c\<sharp>v" "u\<sharp>M" "u\<sharp>v" by fact+
   have ih1: "M{x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* M[x\<turnstile>n>y]" by fact
   have ih2: "N{x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* N[x\<turnstile>n>y]" by fact
   show "(ImpL <c>.M (u).N v){x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* (ImpL <c>.M (u).N v)[x\<turnstile>n>y]"
diff -r 886655a150f6 -r d1b97708d5eb src/HOL/Nominal/Examples/LocalWeakening.thy
--- a/src/HOL/Nominal/Examples/LocalWeakening.thy	Thu Jun 21 20:48:48 2007 +0200
+++ b/src/HOL/Nominal/Examples/LocalWeakening.thy	Thu Jun 21 22:10:16 2007 +0200
@@ -170,7 +170,7 @@
   ultimately show "\<Gamma>2 \<turnstile> lPar x : T" by auto
 next
   case (t_lLam x t T1 \<Gamma>1 T2 \<Gamma>2) (* lambda case *)
-  have vc: "x\<sharp>\<Gamma>2" "x\<sharp>t" by fact  (* variable convention *)
+  have vc: "x\<sharp>\<Gamma>2" "x\<sharp>t" by fact+  (* variable convention *)
   have ih: "\<lbrakk>(x,T1)#\<Gamma>1 \<subseteq> (x,T1)#\<Gamma>2; valid ((x,T1)#\<Gamma>2)\<rbrakk> \<Longrightarrow> (x,T1)#\<Gamma>2 \<turnstile> freshen t x : T2" by fact
   have "\<Gamma>1 \<subseteq> \<Gamma>2" by fact
   then have "(x,T1)#\<Gamma>1 \<subseteq> (x,T1)#\<Gamma>2" by simp