--- 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
--- 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
--- 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*)
--- 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
--- 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
--- 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
-
--- 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
--- 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
--- 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
--- 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]"
--- 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