--- a/src/HOL/Algebra/AbelCoset.thy Wed Jun 13 00:01:38 2007 +0200
+++ b/src/HOL/Algebra/AbelCoset.thy Wed Jun 13 00:01:41 2007 +0200
@@ -185,13 +185,13 @@
lemma (in additive_subgroup) is_additive_subgroup:
shows "additive_subgroup H G"
-by -
+by fact
lemma additive_subgroupI:
includes struct G
assumes a_subgroup: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
shows "additive_subgroup H G"
-by (rule additive_subgroup.intro)
+by (rule additive_subgroup.intro) (rule a_subgroup)
lemma (in additive_subgroup) a_subset:
"H \<subseteq> carrier G"
@@ -225,7 +225,7 @@
lemma (in abelian_subgroup) is_abelian_subgroup:
shows "abelian_subgroup H G"
-by -
+by fact
lemma abelian_subgroupI:
assumes a_normal: "normal H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
@@ -328,14 +328,22 @@
lemma (in abelian_group) a_l_repr_imp_subset:
assumes y: "y \<in> x <+ H" and x: "x \<in> carrier G" and sb: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
shows "y <+ H \<subseteq> x <+ H"
-by (rule group.l_repr_imp_subset [OF a_group,
+apply (rule group.l_repr_imp_subset [OF a_group,
folded a_l_coset_def, simplified monoid_record_simps])
+apply (rule y)
+apply (rule x)
+apply (rule sb)
+done
lemma (in abelian_group) a_l_repr_independence:
assumes y: "y \<in> x <+ H" and x: "x \<in> carrier G" and sb: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
shows "x <+ H = y <+ H"
-by (rule group.l_repr_independence [OF a_group,
+apply (rule group.l_repr_independence [OF a_group,
folded a_l_coset_def, simplified monoid_record_simps])
+apply (rule y)
+apply (rule x)
+apply (rule sb)
+done
lemma (in abelian_group) setadd_subset_G:
"\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G\<rbrakk> \<Longrightarrow> H <+> K \<subseteq> carrier G"
@@ -350,7 +358,7 @@
assumes x: "x \<in> carrier G"
shows "a_set_inv (H +> x) = H +> (\<ominus> x)"
by (rule normal.rcos_inv [OF a_normal,
- folded a_r_coset_def a_inv_def A_SET_INV_def, simplified monoid_record_simps])
+ folded a_r_coset_def a_inv_def A_SET_INV_def, simplified monoid_record_simps]) (rule x)
lemma (in abelian_group) a_setmult_rcos_assoc:
"\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk>
@@ -388,7 +396,7 @@
assumes a: "a \<in> carrier G"
shows "a <+ H = racong H `` {a}"
by (rule subgroup.l_coset_eq_rcong [OF a_subgroup a_group,
- folded a_r_congruent_def a_l_coset_def, simplified monoid_record_simps])
+ folded a_r_congruent_def a_l_coset_def, simplified monoid_record_simps]) (rule a)
lemma (in abelian_subgroup) a_rcos_equation:
shows
@@ -531,7 +539,11 @@
assumes a_group_hom: "group_hom (| carrier = carrier G, mult = add G, one = zero G |)
(| carrier = carrier H, mult = add H, one = zero H |) h"
shows "abelian_group_hom G H h"
-by (intro abelian_group_hom.intro abelian_group_hom_axioms.intro)
+apply (intro abelian_group_hom.intro abelian_group_hom_axioms.intro)
+ apply (rule G.abelian_group_axioms)
+ apply (rule H.abelian_group_axioms)
+apply (rule a_group_hom)
+done
lemma (in abelian_group_hom) is_abelian_group_hom:
"abelian_group_hom G H h"
@@ -588,13 +600,13 @@
assumes X: "X \<in> carrier (G A_Mod a_kernel G H h)"
shows "X \<noteq> {}"
by (rule group_hom.FactGroup_nonempty[OF a_group_hom,
- folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
+ folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) (rule X)
lemma (in abelian_group_hom) FactGroup_contents_mem:
assumes X: "X \<in> carrier (G A_Mod (a_kernel G H h))"
shows "contents (h`X) \<in> carrier H"
by (rule group_hom.FactGroup_contents_mem[OF a_group_hom,
- folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
+ folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) (rule X)
lemma (in abelian_group_hom) A_FactGroup_hom:
"(\<lambda>X. contents (h`X)) \<in> hom (G A_Mod (a_kernel G H h))
@@ -613,7 +625,7 @@
assumes h: "h ` carrier G = carrier H"
shows "(\<lambda>X. contents (h ` X)) ` carrier (G A_Mod a_kernel G H h) = carrier H"
by (rule group_hom.FactGroup_onto[OF a_group_hom,
- folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
+ folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) (rule h)
text{*If @{term h} is a homomorphism from @{term G} onto @{term H}, then the
quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.*}
@@ -634,7 +646,7 @@
assumes hH: "h \<in> H"
shows "h \<in> carrier G"
by (rule subgroup.mem_carrier [OF a_subgroup,
- simplified monoid_record_simps])
+ simplified monoid_record_simps]) (rule hH)
subsection {* Lemmas for Right Cosets *}
@@ -644,31 +656,33 @@
and a': "a' \<in> H +> a"
shows "a' \<in> carrier G"
by (rule subgroup.elemrcos_carrier [OF a_subgroup a_group,
- folded a_r_coset_def, simplified monoid_record_simps])
+ folded a_r_coset_def, simplified monoid_record_simps]) (rule acarr, rule a')
lemma (in abelian_subgroup) a_rcos_const:
assumes hH: "h \<in> H"
shows "H +> h = H"
by (rule subgroup.rcos_const [OF a_subgroup a_group,
- folded a_r_coset_def, simplified monoid_record_simps])
+ folded a_r_coset_def, simplified monoid_record_simps]) (rule hH)
lemma (in abelian_subgroup) a_rcos_module_imp:
assumes xcarr: "x \<in> carrier G"
and x'cos: "x' \<in> H +> x"
shows "(x' \<oplus> \<ominus>x) \<in> H"
by (rule subgroup.rcos_module_imp [OF a_subgroup a_group,
- folded a_r_coset_def a_inv_def, simplified monoid_record_simps])
+ folded a_r_coset_def a_inv_def, simplified monoid_record_simps]) (rule xcarr, rule x'cos)
lemma (in abelian_subgroup) a_rcos_module_rev:
- assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
- and xixH: "(x' \<oplus> \<ominus>x) \<in> H"
+ assumes "x \<in> carrier G" "x' \<in> carrier G"
+ and "(x' \<oplus> \<ominus>x) \<in> H"
shows "x' \<in> H +> x"
+using assms
by (rule subgroup.rcos_module_rev [OF a_subgroup a_group,
folded a_r_coset_def a_inv_def, simplified monoid_record_simps])
lemma (in abelian_subgroup) a_rcos_module:
- assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
+ assumes "x \<in> carrier G" "x' \<in> carrier G"
shows "(x' \<in> H +> x) = (x' \<oplus> \<ominus>x \<in> H)"
+using assms
by (rule subgroup.rcos_module [OF a_subgroup a_group,
folded a_r_coset_def a_inv_def, simplified monoid_record_simps])
@@ -679,10 +693,10 @@
shows "(x' \<in> H +> x) = (x' \<ominus> x \<in> H)"
proof -
from carr
- have "(x' \<in> H +> x) = (x' \<oplus> \<ominus>x \<in> H)" by (rule a_rcos_module)
- from this and carr
- show "(x' \<in> H +> x) = (x' \<ominus> x \<in> H)"
- by (simp add: minus_eq)
+ have "(x' \<in> H +> x) = (x' \<oplus> \<ominus>x \<in> H)" by (rule a_rcos_module)
+ with carr
+ show "(x' \<in> H +> x) = (x' \<ominus> x \<in> H)"
+ by (simp add: minus_eq)
qed
lemma (in abelian_subgroup) a_repr_independence':
--- a/src/HOL/Algebra/Coset.thy Wed Jun 13 00:01:38 2007 +0200
+++ b/src/HOL/Algebra/Coset.thy Wed Jun 13 00:01:41 2007 +0200
@@ -107,13 +107,17 @@
subgroup.one_closed)
done
-text {* Opposite of @{thm [locale=group,source] "repr_independence"} *}
+text (in group) {* Opposite of @{thm [source] "repr_independence"} *}
lemma (in group) repr_independenceD:
includes subgroup H G
assumes ycarr: "y \<in> carrier G"
and repr: "H #> x = H #> y"
shows "y \<in> H #> x"
- by (subst repr, intro rcos_self)
+ apply (subst repr)
+ apply (intro rcos_self)
+ apply (rule ycarr)
+ apply (rule is_subgroup)
+ done
text {* Elements of a right coset are in the carrier *}
lemma (in subgroup) elemrcos_carrier:
@@ -819,8 +823,8 @@
includes group G
shows "H \<in> rcosets H"
proof -
- have "H #> \<one> = H"
- by (rule coset_join2, auto)
+ from _ `subgroup H G` have "H #> \<one> = H"
+ by (rule coset_join2) auto
then show ?thesis
by (auto simp add: RCOSETS_def)
qed
--- a/src/HOL/Algebra/FiniteProduct.thy Wed Jun 13 00:01:38 2007 +0200
+++ b/src/HOL/Algebra/FiniteProduct.thy Wed Jun 13 00:01:41 2007 +0200
@@ -263,9 +263,9 @@
lemma (in ACeD) left_ident [simp]: "x \<in> D ==> e \<cdot> x = x"
proof -
- assume D: "x \<in> D"
- have "x \<cdot> e = x" by (rule ident)
- with D show ?thesis by (simp add: commute)
+ assume "x \<in> D"
+ then have "x \<cdot> e = x" by (rule ident)
+ with `x \<in> D` show ?thesis by (simp add: commute)
qed
lemma (in ACeD) foldD_Un_Int:
@@ -424,9 +424,9 @@
then have "finprod G f A = finprod G f (insert x B)" by simp
also from insert have "... = f x \<otimes> finprod G f B"
proof (intro finprod_insert)
- show "finite B" .
+ show "finite B" by fact
next
- show "x ~: B" .
+ show "x ~: B" by fact
next
assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
"g \<in> insert x B \<rightarrow> carrier G"
--- a/src/HOL/Algebra/Group.thy Wed Jun 13 00:01:38 2007 +0200
+++ b/src/HOL/Algebra/Group.thy Wed Jun 13 00:01:41 2007 +0200
@@ -195,7 +195,7 @@
assumes Units: "carrier G <= Units G"
-lemma (in group) is_group: "group G" .
+lemma (in group) is_group: "group G" by fact
theorem groupI:
fixes G (structure)
@@ -383,7 +383,7 @@
and m_inv_closed [intro,simp]: "x \<in> H \<Longrightarrow> inv x \<in> H"
lemma (in subgroup) is_subgroup:
- "subgroup H G" .
+ "subgroup H G" by fact
declare (in subgroup) group.intro [intro]
@@ -694,7 +694,7 @@
lemma (in group) subgroup_imp_group:
"subgroup H G ==> group (G(| carrier := H |))"
- by (rule subgroup.subgroup_is_group)
+ by (erule subgroup.subgroup_is_group) (rule `group G`)
lemma (in group) is_monoid [intro, simp]:
"monoid G"
--- a/src/HOL/Algebra/Ideal.thy Wed Jun 13 00:01:38 2007 +0200
+++ b/src/HOL/Algebra/Ideal.thy Wed Jun 13 00:01:41 2007 +0200
@@ -25,7 +25,7 @@
lemma (in ideal) is_ideal:
"ideal I R"
-by -
+by fact
lemma idealI:
includes ring
@@ -50,7 +50,7 @@
lemma (in principalideal) is_principalideal:
shows "principalideal I R"
-by -
+by fact
lemma principalidealI:
includes ideal
@@ -85,7 +85,7 @@
lemma (in primeideal) is_primeideal:
shows "primeideal I R"
-by -
+by fact
lemma primeidealI:
includes ideal
@@ -166,7 +166,7 @@
lemma (in ideal) Icarr:
assumes iI: "i \<in> I"
shows "i \<in> carrier R"
-by (rule a_Hcarr)
+using iI by (rule a_Hcarr)
subsection {* Intersection of Ideals *}
@@ -361,7 +361,7 @@
shows "(Idl H \<subseteq> I) = (H \<subseteq> I)"
proof
assume a: "Idl H \<subseteq> I"
- have "H \<subseteq> Idl H" by (rule genideal_self)
+ from Hcarr have "H \<subseteq> Idl H" by (rule genideal_self)
from this and a
show "H \<subseteq> I" by simp
next
@@ -504,8 +504,11 @@
assumes aJ: "a \<in> J"
shows "PIdl a \<subseteq> J"
unfolding cgenideal_def
-by (rule, clarify, rule I_l_closed)
-
+apply rule
+apply clarify
+using aJ
+apply (erule I_l_closed)
+done
lemma (in cring) cgenideal_eq_genideal:
assumes icarr: "i \<in> carrier R"
--- a/src/HOL/Algebra/Lattice.thy Wed Jun 13 00:01:38 2007 +0200
+++ b/src/HOL/Algebra/Lattice.thy Wed Jun 13 00:01:41 2007 +0200
@@ -265,7 +265,7 @@
assume "z \<in> {x}" (* FIXME "z = x"; declare specific elim rule for "insert x {}" (!?) *)
with y L show ?thesis by blast
qed
- qed (rule Upper_closed [THEN subsetD])
+ qed (rule Upper_closed [THEN subsetD, OF y])
next
from L show "insert x A \<subseteq> carrier L" by simp
from least_s show "s \<in> carrier L" by simp
@@ -307,13 +307,13 @@
assume "z \<in> {x}"
with y L show ?thesis by blast
qed
- qed (rule Upper_closed [THEN subsetD])
+ qed (rule Upper_closed [THEN subsetD, OF y])
next
from L show "insert x A \<subseteq> carrier L" by simp
from least_s show "s \<in> carrier L" by simp
qed
- qed
- qed
+ qed (rule least_l)
+ qed (rule P)
qed
lemma (in lattice) finite_sup_least:
@@ -375,12 +375,12 @@
lemma (in lattice) join_le:
assumes sub: "x \<sqsubseteq> z" "y \<sqsubseteq> z"
- and L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L"
+ and x: "x \<in> carrier L" and y: "y \<in> carrier L" and z: "z \<in> carrier L"
shows "x \<squnion> y \<sqsubseteq> z"
-proof (rule joinI)
+proof (rule joinI [OF _ x y])
fix s
assume "least L s (Upper L {x, y})"
- with sub L show "s \<sqsubseteq> z" by (fast elim: least_le intro: Upper_memI)
+ with sub z show "s \<sqsubseteq> z" by (fast elim: least_le intro: Upper_memI)
qed
lemma (in lattice) join_assoc_lemma:
@@ -491,7 +491,7 @@
assume "z \<in> {x}"
with y L show ?thesis by blast
qed
- qed (rule Lower_closed [THEN subsetD])
+ qed (rule Lower_closed [THEN subsetD, OF y])
next
from L show "insert x A \<subseteq> carrier L" by simp
from greatest_i show "i \<in> carrier L" by simp
@@ -533,13 +533,13 @@
assume "z \<in> {x}"
with y L show ?thesis by blast
qed
- qed (rule Lower_closed [THEN subsetD])
+ qed (rule Lower_closed [THEN subsetD, OF y])
next
from L show "insert x A \<subseteq> carrier L" by simp
from greatest_i show "i \<in> carrier L" by simp
qed
- qed
- qed
+ qed (rule greatest_g)
+ qed (rule P)
qed
lemma (in lattice) finite_inf_greatest:
@@ -603,12 +603,12 @@
lemma (in lattice) meet_le:
assumes sub: "z \<sqsubseteq> x" "z \<sqsubseteq> y"
- and L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L"
+ and x: "x \<in> carrier L" and y: "y \<in> carrier L" and z: "z \<in> carrier L"
shows "z \<sqsubseteq> x \<sqinter> y"
-proof (rule meetI)
+proof (rule meetI [OF _ x y])
fix i
assume "greatest L i (Lower L {x, y})"
- with sub L show "z \<sqsubseteq> i" by (fast elim: greatest_le intro: Lower_memI)
+ with sub z show "z \<sqsubseteq> i" by (fast elim: greatest_le intro: Lower_memI)
qed
lemma (in lattice) meet_assoc_lemma:
--- a/src/HOL/Algebra/QuotRing.thy Wed Jun 13 00:01:38 2007 +0200
+++ b/src/HOL/Algebra/QuotRing.thy Wed Jun 13 00:01:41 2007 +0200
@@ -247,23 +247,23 @@
assume "\<zero>\<^bsub>R Quot I\<^esub> = \<one>\<^bsub>R Quot I\<^esub>"
hence II1: "I = I +> \<one>" by (simp add: FactRing_def)
from a_rcos_self[OF one_closed]
- have "\<one> \<in> I" by (simp add: II1[symmetric])
+ have "\<one> \<in> I" by (simp add: II1[symmetric])
hence "I = carrier R" by (rule one_imp_carrier)
from this and I_notcarr
- show "False" by simp
+ show "False" by simp
next
--{* Existence of Inverse *}
fix a
assume IanI: "I +> a \<noteq> I"
- and acarr: "a \<in> carrier R"
+ and acarr: "a \<in> carrier R"
--{* Helper ideal @{text "J"} *}
def J \<equiv> "(carrier R #> a) <+> I :: 'a set"
have idealJ: "ideal J R"
- apply (unfold J_def, rule add_ideals)
- apply (simp only: cgenideal_eq_rcos[symmetric], rule cgenideal_ideal, rule acarr)
- apply (rule is_ideal)
- done
+ apply (unfold J_def, rule add_ideals)
+ apply (simp only: cgenideal_eq_rcos[symmetric], rule cgenideal_ideal, rule acarr)
+ apply (rule is_ideal)
+ done
--{* Showing @{term "J"} not smaller than @{term "I"} *}
have IinJ: "I \<subseteq> J"
@@ -275,7 +275,7 @@
have "x = \<zero> \<otimes> a \<oplus> x" by algebra
from Zcarr and xI and this
- show "\<exists>xa\<in>carrier R. \<exists>k\<in>I. x = xa \<otimes> a \<oplus> k" by fast
+ show "\<exists>xa\<in>carrier R. \<exists>k\<in>I. x = xa \<otimes> a \<oplus> k" by fast
qed
--{* Showing @{term "J \<noteq> I"} *}
@@ -284,57 +284,58 @@
assume "a \<in> I"
hence "I +> a = I" by (rule a_rcos_const)
from this and IanI
- show "False" by simp
+ show "False" by simp
qed
have aJ: "a \<in> J"
proof (simp add: J_def r_coset_def set_add_defs)
from acarr
- have "a = \<one> \<otimes> a \<oplus> \<zero>" by algebra
+ have "a = \<one> \<otimes> a \<oplus> \<zero>" by algebra
from one_closed and additive_subgroup.zero_closed[OF is_additive_subgroup] and this
- show "\<exists>x\<in>carrier R. \<exists>k\<in>I. a = x \<otimes> a \<oplus> k" by fast
+ show "\<exists>x\<in>carrier R. \<exists>k\<in>I. a = x \<otimes> a \<oplus> k" by fast
qed
from aJ and anI
- have JnI: "J \<noteq> I" by fast
+ have JnI: "J \<noteq> I" by fast
--{* Deducing @{term "J = carrier R"} because @{term "I"} is maximal *}
from idealJ and IinJ
- have "J = I \<or> J = carrier R"
+ have "J = I \<or> J = carrier R"
proof (rule I_maximal, unfold J_def)
have "carrier R #> a \<subseteq> carrier R"
- by (rule r_coset_subset_G) fast
+ using subset_refl acarr
+ by (rule r_coset_subset_G)
from this and a_subset
- show "carrier R #> a <+> I \<subseteq> carrier R" by (rule set_add_closed)
+ show "carrier R #> a <+> I \<subseteq> carrier R" by (rule set_add_closed)
qed
from this and JnI
- have Jcarr: "J = carrier R" by simp
+ have Jcarr: "J = carrier R" by simp
--{* Calculating an inverse for @{term "a"} *}
from one_closed[folded Jcarr]
- have "\<exists>r\<in>carrier R. \<exists>i\<in>I. \<one> = r \<otimes> a \<oplus> i"
- by (simp add: J_def r_coset_def set_add_defs)
+ have "\<exists>r\<in>carrier R. \<exists>i\<in>I. \<one> = r \<otimes> a \<oplus> i"
+ by (simp add: J_def r_coset_def set_add_defs)
from this
- obtain r i
- where rcarr: "r \<in> carrier R"
- and iI: "i \<in> I"
- and one: "\<one> = r \<otimes> a \<oplus> i"
- by fast
+ obtain r i
+ where rcarr: "r \<in> carrier R"
+ and iI: "i \<in> I"
+ and one: "\<one> = r \<otimes> a \<oplus> i"
+ by fast
from one and rcarr and acarr and iI[THEN a_Hcarr]
- have rai1: "a \<otimes> r = \<ominus>i \<oplus> \<one>" by algebra
+ have rai1: "a \<otimes> r = \<ominus>i \<oplus> \<one>" by algebra
--{* Lifting to cosets *}
from iI
- have "\<ominus>i \<oplus> \<one> \<in> I +> \<one>"
- by (intro a_rcosI, simp, intro a_subset, simp)
+ have "\<ominus>i \<oplus> \<one> \<in> I +> \<one>"
+ by (intro a_rcosI, simp, intro a_subset, simp)
from this and rai1
- have "a \<otimes> r \<in> I +> \<one>" by simp
+ have "a \<otimes> r \<in> I +> \<one>" by simp
from this have "I +> \<one> = I +> a \<otimes> r"
- by (rule a_repr_independence, simp) (rule a_subgroup)
+ by (rule a_repr_independence, simp) (rule a_subgroup)
from rcarr and this[symmetric]
- show "\<exists>r\<in>carrier R. I +> a \<otimes> r = I +> \<one>" by fast
+ show "\<exists>r\<in>carrier R. I +> a \<otimes> r = I +> \<one>" by fast
qed
end
--- a/src/HOL/Algebra/Ring.thy Wed Jun 13 00:01:38 2007 +0200
+++ b/src/HOL/Algebra/Ring.thy Wed Jun 13 00:01:41 2007 +0200
@@ -249,8 +249,11 @@
fixes A
assumes fin: "finite A" and f: "f \<in> A -> carrier G"
shows "finsum G f A \<in> carrier G"
- by (rule comm_monoid.finprod_closed [OF a_comm_monoid,
+ apply (rule comm_monoid.finprod_closed [OF a_comm_monoid,
folded finsum_def, simplified monoid_record_simps])
+ apply (rule fin)
+ apply (rule f)
+ done
lemma (in abelian_monoid) finsum_Un_Int:
"[| finite A; finite B; g \<in> A -> carrier G; g \<in> B -> carrier G |] ==>
@@ -359,7 +362,7 @@
lemma (in ring) is_ring:
"ring R"
- .
+ by fact
lemmas ring_record_simps = monoid_record_simps ring.simps
@@ -370,34 +373,34 @@
and l_distr: "!!x y z. [| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
==> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
shows "cring R"
- proof (intro cring.intro ring.intro)
- show "ring_axioms R"
+proof (intro cring.intro ring.intro)
+ show "ring_axioms R"
-- {* Right-distributivity follows from left-distributivity and
commutativity. *}
- proof (rule ring_axioms.intro)
- fix x y z
- assume R: "x \<in> carrier R" "y \<in> carrier R" "z \<in> carrier R"
- note [simp]= comm_monoid.axioms [OF comm_monoid]
- abelian_group.axioms [OF abelian_group]
- abelian_monoid.a_closed
+ proof (rule ring_axioms.intro)
+ fix x y z
+ assume R: "x \<in> carrier R" "y \<in> carrier R" "z \<in> carrier R"
+ note [simp] = comm_monoid.axioms [OF comm_monoid]
+ abelian_group.axioms [OF abelian_group]
+ abelian_monoid.a_closed
- from R have "z \<otimes> (x \<oplus> y) = (x \<oplus> y) \<otimes> z"
- by (simp add: comm_monoid.m_comm [OF comm_monoid.intro])
- also from R have "... = x \<otimes> z \<oplus> y \<otimes> z" by (simp add: l_distr)
- also from R have "... = z \<otimes> x \<oplus> z \<otimes> y"
- by (simp add: comm_monoid.m_comm [OF comm_monoid.intro])
- finally show "z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y" .
- qed
- qed (auto intro: cring.intro
- abelian_group.axioms comm_monoid.axioms ring_axioms.intro prems)
+ from R have "z \<otimes> (x \<oplus> y) = (x \<oplus> y) \<otimes> z"
+ by (simp add: comm_monoid.m_comm [OF comm_monoid.intro])
+ also from R have "... = x \<otimes> z \<oplus> y \<otimes> z" by (simp add: l_distr)
+ also from R have "... = z \<otimes> x \<oplus> z \<otimes> y"
+ by (simp add: comm_monoid.m_comm [OF comm_monoid.intro])
+ finally show "z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y" .
+ qed (rule l_distr)
+qed (auto intro: cring.intro
+ abelian_group.axioms comm_monoid.axioms ring_axioms.intro prems)
lemma (in cring) is_comm_monoid:
"comm_monoid R"
by (auto intro!: comm_monoidI m_assoc m_comm)
lemma (in cring) is_cring:
- "cring R"
- .
+ "cring R" by fact
+
subsubsection {* Normaliser for Rings *}
@@ -647,7 +650,7 @@
have "b = \<zero>" .
thus "a = \<zero> \<or> b = \<zero>" by simp
qed
-qed
+qed (rule field_Units)
text {* Another variant to show that something is a field *}
lemma (in cring) cring_fieldI2:
--- a/src/HOL/Algebra/RingHom.thy Wed Jun 13 00:01:38 2007 +0200
+++ b/src/HOL/Algebra/RingHom.thy Wed Jun 13 00:01:41 2007 +0200
@@ -34,7 +34,7 @@
lemma (in ring_hom_ring) is_ring_hom_ring:
includes struct R + struct S
shows "ring_hom_ring R S h"
-by -
+by fact
lemma ring_hom_ringI:
includes ring R + ring S
@@ -51,9 +51,13 @@
lemma ring_hom_ringI2:
includes ring R + ring S
- assumes "h \<in> ring_hom R S"
+ assumes h: "h \<in> ring_hom R S"
shows "ring_hom_ring R S h"
-by (intro ring_hom_ring.intro ring_hom_ring_axioms.intro)
+apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro)
+apply (rule R.is_ring)
+apply (rule S.is_ring)
+apply (rule h)
+done
lemma ring_hom_ringI3:
includes abelian_group_hom R S + ring R + ring S
--- a/src/HOL/Algebra/UnivPoly.thy Wed Jun 13 00:01:38 2007 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy Wed Jun 13 00:01:41 2007 +0200
@@ -306,7 +306,7 @@
next
case (Suc k)
then have "k <= n" by arith
- then have "?eq k" by (rule Suc)
+ from this R have "?eq k" by (rule Suc)
with R show ?case
by (simp cong: finsum_cong
add: Suc_diff_le Pi_def l_distr r_distr m_assoc)
@@ -633,14 +633,14 @@
*)
lemma (in UP_cring) deg_aboveD:
- "[| deg R p < m; p \<in> carrier P |] ==> coeff P p m = \<zero>"
+ assumes "deg R p < m" and "p \<in> carrier P"
+ shows "coeff P p m = \<zero>"
proof -
- assume R: "p \<in> carrier P" and "deg R p < m"
- from R obtain n where "bound \<zero> n (coeff P p)"
+ from `p \<in> carrier P` obtain n where "bound \<zero> n (coeff P p)"
by (auto simp add: UP_def P_def)
then have "bound \<zero> (deg R p) (coeff P p)"
by (auto simp: deg_def P_def dest: LeastI)
- then show ?thesis ..
+ from this and `deg R p < m` show ?thesis ..
qed
lemma (in UP_cring) deg_belowI:
@@ -672,7 +672,7 @@
then have "EX m. deg R p - 1 < m & coeff P p m ~= \<zero>"
by (unfold bound_def) fast
then have "EX m. deg R p <= m & coeff P p m ~= \<zero>" by (simp add: deg minus)
- then show ?thesis by auto
+ then show ?thesis by (auto intro: that)
qed
with deg_belowI R have "deg R p = m" by fastsimp
with m_coeff show ?thesis by simp
@@ -689,7 +689,7 @@
with nonzero show ?thesis by contradiction
qed
then obtain m where coeff: "coeff P p m ~= \<zero>" ..
- then have "m <= deg R p" by (rule deg_belowI)
+ from this and R have "m <= deg R p" by (rule deg_belowI)
then have "m = 0" by (simp add: deg)
with coeff show ?thesis by simp
qed
@@ -773,7 +773,7 @@
shows "deg R (a \<odot>\<^bsub>P\<^esub> p) = (if a = \<zero> then 0 else deg R p)"
proof (rule le_anti_sym)
show "deg R (a \<odot>\<^bsub>P\<^esub> p) <= (if a = \<zero> then 0 else deg R p)"
- by (rule deg_smult_ring)
+ using R by (rule deg_smult_ring)
next
show "(if a = \<zero> then 0 else deg R p) <= deg R (a \<odot>\<^bsub>P\<^esub> p)"
proof (cases "a = \<zero>")
@@ -805,7 +805,7 @@
deg R (p \<otimes>\<^bsub>P\<^esub> q) = deg R p + deg R q"
proof (rule le_anti_sym)
assume "p \<in> carrier P" " q \<in> carrier P"
- show "deg R (p \<otimes>\<^bsub>P\<^esub> q) <= deg R p + deg R q" by (rule deg_mult_cring)
+ then show "deg R (p \<otimes>\<^bsub>P\<^esub> q) <= deg R p + deg R q" by (rule deg_mult_cring)
next
let ?s = "(%i. coeff P p i \<otimes> coeff P q (deg R p + deg R q - i))"
assume R: "p \<in> carrier P" "q \<in> carrier P" and nz: "p ~= \<zero>\<^bsub>P\<^esub>" "q ~= \<zero>\<^bsub>P\<^esub>"
@@ -884,7 +884,7 @@
also have "... = finsum P ?s {..deg R p}"
by (simp cong: P.finsum_cong add: P.finsum_Un_disjoint ivl_disj_int_one
deg_aboveD R Pi_def)
- also have "... = p" by (rule up_repr)
+ also have "... = p" using R by (rule up_repr)
finally show ?thesis .
qed
@@ -1301,6 +1301,7 @@
and "cring S"
and "h \<in> ring_hom R S"
shows "UP_pre_univ_prop R S h"
+ using assms
by (auto intro!: UP_pre_univ_prop.intro ring_hom_cring.intro
ring_hom_cring_axioms.intro UP_cring.intro)
--- a/src/HOL/Algebra/poly/UnivPoly2.thy Wed Jun 13 00:01:38 2007 +0200
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy Wed Jun 13 00:01:41 2007 +0200
@@ -439,11 +439,11 @@
by (unfold deg_def) (fast intro: Least_le)
lemma deg_aboveD:
- assumes prem: "deg p < m" shows "coeff p m = 0"
+ assumes "deg p < m" shows "coeff p m = 0"
proof -
obtain n where "bound n (coeff p)" by (rule bound_coeff_obtain)
then have "bound (deg p) (coeff p)" by (unfold deg_def, rule LeastI)
- then show "coeff p m = 0" by (rule boundD)
+ then show "coeff p m = 0" using `deg p < m` by (rule boundD)
qed
lemma deg_belowI:
@@ -470,7 +470,7 @@
then have "EX m. deg p - 1 < m & coeff p m ~= 0"
by (unfold bound_def) fast
then have "EX m. deg p <= m & coeff p m ~= 0" by (simp add: deg minus)
- then show ?thesis by auto
+ then show ?thesis by (auto intro: that)
qed
with deg_belowI have "deg p = m" by fastsimp
with m_coeff show ?thesis by simp
--- a/src/HOL/Bali/AxSound.thy Wed Jun 13 00:01:38 2007 +0200
+++ b/src/HOL/Bali/AxSound.thy Wed Jun 13 00:01:41 2007 +0200
@@ -6,8 +6,6 @@
statements
*}
-
-
theory AxSound imports AxSem begin
section "validity"
@@ -101,7 +99,7 @@
apply (fast intro: triple_valid2_Suc)
done
-lemma "G|\<Turnstile>n:insert t A = (G\<Turnstile>n:t \<and> G|\<Turnstile>n:A)";
+lemma "G|\<Turnstile>n:insert t A = (G\<Turnstile>n:t \<and> G|\<Turnstile>n:A)"
oops
@@ -131,8 +129,8 @@
qed
next
case (Suc m)
- have hyp: "\<forall>t\<in>A. G\<Turnstile>m\<Colon>t \<Longrightarrow> \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>m\<Colon>t".
- have prem: "\<forall>t\<in>A. G\<Turnstile>Suc m\<Colon>t" .
+ note hyp = `\<forall>t\<in>A. G\<Turnstile>m\<Colon>t \<Longrightarrow> \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>m\<Colon>t`
+ note prem = `\<forall>t\<in>A. G\<Turnstile>Suc m\<Colon>t`
show "\<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>Suc m\<Colon>t"
proof -
{
@@ -357,8 +355,9 @@
by (simp add: ax_valids2_def triple_valid2_def2)
next
case (insert A t ts)
- have valid_t: "G,A|\<Turnstile>\<Colon>{t}" .
- moreover have valid_ts: "G,A|\<Turnstile>\<Colon>ts" .
+ note valid_t = `G,A|\<Turnstile>\<Colon>{t}`
+ moreover
+ note valid_ts = `G,A|\<Turnstile>\<Colon>ts`
{
fix n assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
have "G\<Turnstile>n\<Colon>t" and "\<forall>t\<in>ts. G\<Turnstile>n\<Colon>t"
@@ -376,21 +375,21 @@
by (unfold ax_valids2_def) blast
next
case (asm ts A)
- have "ts \<subseteq> A" .
- then show "G,A|\<Turnstile>\<Colon>ts"
+ from `ts \<subseteq> A`
+ show "G,A|\<Turnstile>\<Colon>ts"
by (auto simp add: ax_valids2_def triple_valid2_def)
next
case (weaken A ts' ts)
- have "G,A|\<Turnstile>\<Colon>ts'" .
- moreover have "ts \<subseteq> ts'" .
+ note `G,A|\<Turnstile>\<Colon>ts'`
+ moreover note `ts \<subseteq> ts'`
ultimately show "G,A|\<Turnstile>\<Colon>ts"
by (unfold ax_valids2_def triple_valid2_def) blast
next
case (conseq P A t Q)
- have con: "\<forall>Y s Z. P Y s Z \<longrightarrow>
+ note con = `\<forall>Y s Z. P Y s Z \<longrightarrow>
(\<exists>P' Q'.
(G,A\<turnstile>{P'} t\<succ> {Q'} \<and> G,A|\<Turnstile>\<Colon>{ {P'} t\<succ> {Q'} }) \<and>
- (\<forall>Y' s'. (\<forall>Y Z'. P' Y s Z' \<longrightarrow> Q' Y' s' Z') \<longrightarrow> Q Y' s' Z))".
+ (\<forall>Y' s'. (\<forall>Y Z'. P' Y s Z' \<longrightarrow> Q' Y' s' Z') \<longrightarrow> Q Y' s' Z))`
show "G,A|\<Turnstile>\<Colon>{ {P} t\<succ> {Q} }"
proof (rule validI)
fix n s0 L accC T C v s1 Y Z
@@ -475,8 +474,8 @@
qed
next
case (FVar A P statDeclC Q e stat fn R accC)
- have valid_init: "G,A|\<Turnstile>\<Colon>{ {Normal P} .Init statDeclC. {Q} }" .
- have valid_e: "G,A|\<Turnstile>\<Colon>{ {Q} e-\<succ> {\<lambda>Val:a:. fvar statDeclC stat fn a ..; R} }" .
+ note valid_init = `G,A|\<Turnstile>\<Colon>{ {Normal P} .Init statDeclC. {Q} }`
+ note valid_e = `G,A|\<Turnstile>\<Colon>{ {Q} e-\<succ> {\<lambda>Val:a:. fvar statDeclC stat fn a ..; R} }`
show "G,A|\<Turnstile>\<Colon>{ {Normal P} {accC,statDeclC,stat}e..fn=\<succ> {R} }"
proof (rule valid_var_NormalI)
fix n s0 L accC' T V vf s3 Y Z
@@ -536,8 +535,8 @@
from eval_init
have "(dom (locals (store s0))) \<subseteq> (dom (locals (store s1)))"
by (rule dom_locals_evaln_mono_elim)
- with da_e show ?thesis
- by (rule da_weakenE)
+ with da_e show thesis
+ by (rule da_weakenE) (rule that)
qed
with valid_e Q valid_A conf_s1 eval_e wt_e
obtain "R \<lfloor>vf\<rfloor>\<^sub>v s2' Z" and "s2\<Colon>\<preceq>(G, L)"
@@ -570,7 +569,7 @@
qed
next
case (AVar A P e1 Q e2 R)
- have valid_e1: "G,A|\<Turnstile>\<Colon>{ {Normal P} e1-\<succ> {Q} }" .
+ note valid_e1 = `G,A|\<Turnstile>\<Colon>{ {Normal P} e1-\<succ> {Q} }`
have valid_e2: "\<And> a. G,A|\<Turnstile>\<Colon>{ {Q\<leftarrow>In1 a} e2-\<succ> {\<lambda>Val:i:. avar G i a ..; R} }"
using AVar.hyps by simp
show "G,A|\<Turnstile>\<Colon>{ {Normal P} e1.[e2]=\<succ> {R} }"
@@ -674,9 +673,9 @@
qed
next
case (NewA A P T Q e R)
- have valid_init: "G,A|\<Turnstile>\<Colon>{ {Normal P} .init_comp_ty T. {Q} }" .
- have valid_e: "G,A|\<Turnstile>\<Colon>{ {Q} e-\<succ> {\<lambda>Val:i:. abupd (check_neg i) .;
- Alloc G (Arr T (the_Intg i)) R}}" .
+ note valid_init = `G,A|\<Turnstile>\<Colon>{ {Normal P} .init_comp_ty T. {Q} }`
+ note valid_e = `G,A|\<Turnstile>\<Colon>{ {Q} e-\<succ> {\<lambda>Val:i:. abupd (check_neg i) .;
+ Alloc G (Arr T (the_Intg i)) R}}`
show "G,A|\<Turnstile>\<Colon>{ {Normal P} New T[e]-\<succ> {R} }"
proof (rule valid_expr_NormalI)
fix n s0 L accC arrT E v s3 Y Z
@@ -978,7 +977,7 @@
qed
next
case (Acc A P var Q)
- have valid_var: "G,A|\<Turnstile>\<Colon>{ {Normal P} var=\<succ> {\<lambda>Var:(v, f):. Q\<leftarrow>In1 v} }" .
+ note valid_var = `G,A|\<Turnstile>\<Colon>{ {Normal P} var=\<succ> {\<lambda>Var:(v, f):. Q\<leftarrow>In1 v} }`
show "G,A|\<Turnstile>\<Colon>{ {Normal P} Acc var-\<succ> {Q} }"
proof (rule valid_expr_NormalI)
fix n s0 L accC T E v s1 Y Z
@@ -1014,7 +1013,7 @@
qed
next
case (Ass A P var Q e R)
- have valid_var: "G,A|\<Turnstile>\<Colon>{ {Normal P} var=\<succ> {Q} }" .
+ note valid_var = `G,A|\<Turnstile>\<Colon>{ {Normal P} var=\<succ> {Q} }`
have valid_e: "\<And> vf.
G,A|\<Turnstile>\<Colon>{ {Q\<leftarrow>In2 vf} e-\<succ> {\<lambda>Val:v:. assign (snd vf) v .; R} }"
using Ass.hyps by simp
@@ -1126,7 +1125,7 @@
qed
next
case (Cond A P e0 P' e1 e2 Q)
- have valid_e0: "G,A|\<Turnstile>\<Colon>{ {Normal P} e0-\<succ> {P'} }" .
+ note valid_e0 = `G,A|\<Turnstile>\<Colon>{ {Normal P} e0-\<succ> {P'} }`
have valid_then_else:"\<And> b. G,A|\<Turnstile>\<Colon>{ {P'\<leftarrow>=b} (if b then e1 else e2)-\<succ> {Q} }"
using Cond.hyps by simp
show "G,A|\<Turnstile>\<Colon>{ {Normal P} e0 ? e1 : e2-\<succ> {Q} }"
@@ -1216,7 +1215,7 @@
qed
next
case (Call A P e Q args R mode statT mn pTs' S accC')
- have valid_e: "G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> {Q} }" .
+ note valid_e = `G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> {Q} }`
have valid_args: "\<And> a. G,A|\<Turnstile>\<Colon>{ {Q\<leftarrow>In1 a} args\<doteq>\<succ> {R a} }"
using Call.hyps by simp
have valid_methd: "\<And> a vs invC declC l.
@@ -1605,9 +1604,9 @@
by (rule Methd_sound)
next
case (Body A P D Q c R)
- have valid_init: "G,A|\<Turnstile>\<Colon>{ {Normal P} .Init D. {Q} }".
- have valid_c: "G,A|\<Turnstile>\<Colon>{ {Q} .c.
- {\<lambda>s.. abupd (absorb Ret) .; R\<leftarrow>In1 (the (locals s Result))} }".
+ note valid_init = `G,A|\<Turnstile>\<Colon>{ {Normal P} .Init D. {Q} }`
+ note valid_c = `G,A|\<Turnstile>\<Colon>{ {Q} .c.
+ {\<lambda>s.. abupd (absorb Ret) .; R\<leftarrow>In1 (the (locals s Result))} }`
show "G,A|\<Turnstile>\<Colon>{ {Normal P} Body D c-\<succ> {R} }"
proof (rule valid_expr_NormalI)
fix n s0 L accC T E v s4 Y Z
@@ -1780,7 +1779,7 @@
qed
next
case (Expr A P e Q)
- have valid_e: "G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> {Q\<leftarrow>\<diamondsuit>} }".
+ note valid_e = `G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> {Q\<leftarrow>\<diamondsuit>} }`
show "G,A|\<Turnstile>\<Colon>{ {Normal P} .Expr e. {Q} }"
proof (rule valid_stmt_NormalI)
fix n s0 L accC C s1 Y Z
@@ -1810,7 +1809,7 @@
qed
next
case (Lab A P c l Q)
- have valid_c: "G,A|\<Turnstile>\<Colon>{ {Normal P} .c. {abupd (absorb l) .; Q} }".
+ note valid_c = `G,A|\<Turnstile>\<Colon>{ {Normal P} .c. {abupd (absorb l) .; Q} }`
show "G,A|\<Turnstile>\<Colon>{ {Normal P} .l\<bullet> c. {Q} }"
proof (rule valid_stmt_NormalI)
fix n s0 L accC C s2 Y Z
@@ -1847,8 +1846,8 @@
qed
next
case (Comp A P c1 Q c2 R)
- have valid_c1: "G,A|\<Turnstile>\<Colon>{ {Normal P} .c1. {Q} }" .
- have valid_c2: "G,A|\<Turnstile>\<Colon>{ {Q} .c2. {R} }" .
+ note valid_c1 = `G,A|\<Turnstile>\<Colon>{ {Normal P} .c1. {Q} }`
+ note valid_c2 = `G,A|\<Turnstile>\<Colon>{ {Q} .c2. {R} }`
show "G,A|\<Turnstile>\<Colon>{ {Normal P} .c1;; c2. {R} }"
proof (rule valid_stmt_NormalI)
fix n s0 L accC C s2 Y Z
@@ -1906,8 +1905,8 @@
qed
next
case (If A P e P' c1 c2 Q)
- have valid_e: "G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> {P'} }" .
- have valid_then_else: "\<And> b. G,A|\<Turnstile>\<Colon>{ {P'\<leftarrow>=b} .(if b then c1 else c2). {Q} }"
+ note valid_e = `G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> {P'} }`
+ have valid_then_else: "\<And> b. G,A|\<Turnstile>\<Colon>{ {P'\<leftarrow>=b} .(if b then c1 else c2). {Q} }"
using If.hyps by simp
show "G,A|\<Turnstile>\<Colon>{ {Normal P} .If(e) c1 Else c2. {Q} }"
proof (rule valid_stmt_NormalI)
@@ -1983,10 +1982,10 @@
qed
next
case (Loop A P e P' c l)
- have valid_e: "G,A|\<Turnstile>\<Colon>{ {P} e-\<succ> {P'} }".
- have valid_c: "G,A|\<Turnstile>\<Colon>{ {Normal (P'\<leftarrow>=True)}
+ note valid_e = `G,A|\<Turnstile>\<Colon>{ {P} e-\<succ> {P'} }`
+ note valid_c = `G,A|\<Turnstile>\<Colon>{ {Normal (P'\<leftarrow>=True)}
.c.
- {abupd (absorb (Cont l)) .; P} }" .
+ {abupd (absorb (Cont l)) .; P} }`
show "G,A|\<Turnstile>\<Colon>{ {P} .l\<bullet> While(e) c. {P'\<leftarrow>=False\<down>=\<diamondsuit>} }"
proof (rule valid_stmtI)
fix n s0 L accC C s3 Y Z
@@ -2021,11 +2020,11 @@
(is "PROP ?Hyp n t s v s'")
proof (induct)
case (Loop s0' e' n' b s1' c' s2' l' s3' Y' T E)
- have while: "(\<langle>l'\<bullet> While(e') c'\<rangle>\<^sub>s::term) = \<langle>l\<bullet> While(e) c\<rangle>\<^sub>s" .
+ note while = `(\<langle>l'\<bullet> While(e') c'\<rangle>\<^sub>s::term) = \<langle>l\<bullet> While(e) c\<rangle>\<^sub>s`
hence eqs: "l'=l" "e'=e" "c'=c" by simp_all
- have valid_A: "\<forall>t\<in>A. G\<Turnstile>n'\<Colon>t".
- have P: "P Y' (Norm s0') Z".
- have conf_s0': "Norm s0'\<Colon>\<preceq>(G, L)" .
+ note valid_A = `\<forall>t\<in>A. G\<Turnstile>n'\<Colon>t`
+ note P = `P Y' (Norm s0') Z`
+ note conf_s0' = `Norm s0'\<Colon>\<preceq>(G, L)`
have wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>\<langle>l\<bullet> While(e) c\<rangle>\<^sub>s\<Colon>T"
using Loop.prems eqs by simp
have da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>
@@ -2123,8 +2122,8 @@
by simp
finally
have "dom (locals (store ((Norm s0')::state))) \<subseteq> \<dots>" .
- with da show ?thesis
- by (rule da_weakenE)
+ with da show thesis
+ by (rule da_weakenE) (rule that)
qed
from valid_A P_s2' conf_absorb wt da_while'
show "(P'\<leftarrow>=False\<down>=\<diamondsuit>) \<diamondsuit> s3' Z"
@@ -2240,7 +2239,7 @@
qed
next
case (Throw A P e Q)
- have valid_e: "G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> {\<lambda>Val:a:. abupd (throw a) .; Q\<leftarrow>\<diamondsuit>} }".
+ note valid_e = `G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> {\<lambda>Val:a:. abupd (throw a) .; Q\<leftarrow>\<diamondsuit>} }`
show "G,A|\<Turnstile>\<Colon>{ {Normal P} .Throw e. {Q} }"
proof (rule valid_stmt_NormalI)
fix n s0 L accC C s2 Y Z
@@ -2278,11 +2277,11 @@
qed
next
case (Try A P c1 Q C vn c2 R)
- have valid_c1: "G,A|\<Turnstile>\<Colon>{ {Normal P} .c1. {SXAlloc G Q} }".
- have valid_c2: "G,A|\<Turnstile>\<Colon>{ {Q \<and>. (\<lambda>s. G,s\<turnstile>catch C) ;. new_xcpt_var vn}
+ note valid_c1 = `G,A|\<Turnstile>\<Colon>{ {Normal P} .c1. {SXAlloc G Q} }`
+ note valid_c2 = `G,A|\<Turnstile>\<Colon>{ {Q \<and>. (\<lambda>s. G,s\<turnstile>catch C) ;. new_xcpt_var vn}
.c2.
- {R} }".
- have Q_R: "(Q \<and>. (\<lambda>s. \<not> G,s\<turnstile>catch C)) \<Rightarrow> R" .
+ {R} }`
+ note Q_R = `(Q \<and>. (\<lambda>s. \<not> G,s\<turnstile>catch C)) \<Rightarrow> R`
show "G,A|\<Turnstile>\<Colon>{ {Normal P} .Try c1 Catch(C vn) c2. {R} }"
proof (rule valid_stmt_NormalI)
fix n s0 L accC E s3 Y Z
@@ -2409,8 +2408,8 @@
qed
qed
next
- case (Fin A P c1 Q c2 R)
- have valid_c1: "G,A|\<Turnstile>\<Colon>{ {Normal P} .c1. {Q} }".
+ case (Fin A P c1 Q c2 R)
+ note valid_c1 = `G,A|\<Turnstile>\<Colon>{ {Normal P} .c1. {Q} }`
have valid_c2: "\<And> abr. G,A|\<Turnstile>\<Colon>{ {Q \<and>. (\<lambda>s. abr = fst s) ;. abupd (\<lambda>x. None)}
.c2.
{abupd (abrupt_if (abr \<noteq> None) abr) .; R} }"
@@ -2507,11 +2506,11 @@
qed
next
case (Init C c A P Q R)
- have c: "the (class G C) = c".
- have valid_super:
- "G,A|\<Turnstile>\<Colon>{ {Normal (P \<and>. Not \<circ> initd C ;. supd (init_class_obj G C))}
+ note c = `the (class G C) = c`
+ note valid_super =
+ `G,A|\<Turnstile>\<Colon>{ {Normal (P \<and>. Not \<circ> initd C ;. supd (init_class_obj G C))}
.(if C = Object then Skip else Init (super c)).
- {Q} }".
+ {Q} }`
have valid_init:
"\<And> l. G,A|\<Turnstile>\<Colon>{ {Q \<and>. (\<lambda>s. l = locals (snd s)) ;. set_lvars empty}
.init c.
--- a/src/HOL/Bali/DefiniteAssignment.thy Wed Jun 13 00:01:38 2007 +0200
+++ b/src/HOL/Bali/DefiniteAssignment.thy Wed Jun 13 00:01:41 2007 +0200
@@ -349,10 +349,10 @@
by (cases binop) (simp_all)
next
case (Cond c e1 e2 b)
- have hyp_c: "\<And> b. ?Const b c \<Longrightarrow> ?Ass b c" .
- have hyp_e1: "\<And> b. ?Const b e1 \<Longrightarrow> ?Ass b e1" .
- have hyp_e2: "\<And> b. ?Const b e2 \<Longrightarrow> ?Ass b e2" .
- have const: "constVal (c ? e1 : e2) = Some (Bool b)" .
+ note hyp_c = `\<And> b. ?Const b c \<Longrightarrow> ?Ass b c`
+ note hyp_e1 = `\<And> b. ?Const b e1 \<Longrightarrow> ?Ass b e1`
+ note hyp_e2 = `\<And> b. ?Const b e2 \<Longrightarrow> ?Ass b e2`
+ note const = `constVal (c ? e1 : e2) = Some (Bool b)`
then obtain bv where bv: "constVal c = Some bv"
by simp
hence emptyC: "assignsE c = {}" by (rule assignsE_const_simp)
@@ -397,10 +397,10 @@
by (cases binop) (simp_all)
next
case (Cond c e1 e2 b)
- have hyp_c: "\<And> b. ?Const b c \<Longrightarrow> ?Ass b c" .
- have hyp_e1: "\<And> b. ?Const b e1 \<Longrightarrow> ?Ass b e1" .
- have hyp_e2: "\<And> b. ?Const b e2 \<Longrightarrow> ?Ass b e2" .
- have const: "constVal (c ? e1 : e2) = Some (Bool b)" .
+ note hyp_c = `\<And> b. ?Const b c \<Longrightarrow> ?Ass b c`
+ note hyp_e1 = `\<And> b. ?Const b e1 \<Longrightarrow> ?Ass b e1`
+ note hyp_e2 = `\<And> b. ?Const b e2 \<Longrightarrow> ?Ass b e2`
+ note const = `constVal (c ? e1 : e2) = Some (Bool b)`
then obtain bv where bv: "constVal c = Some bv"
by simp
show ?case
@@ -958,8 +958,8 @@
case (Cast T e)
have "E\<turnstile>e\<Colon>- (PrimT Boolean)"
proof -
- have "E\<turnstile>(Cast T e)\<Colon>- (PrimT Boolean)" .
- then obtain Te where "E\<turnstile>e\<Colon>-Te"
+ from `E\<turnstile>(Cast T e)\<Colon>- (PrimT Boolean)`
+ obtain Te where "E\<turnstile>e\<Colon>-Te"
"prg E\<turnstile>Te\<preceq>? PrimT Boolean"
by cases simp
thus ?thesis
@@ -988,10 +988,10 @@
by - (cases binop, auto simp add: assignsE_const_simp)
next
case (Cond c e1 e2)
- have hyp_c: "?Boolean c \<Longrightarrow> ?Incl c" .
- have hyp_e1: "?Boolean e1 \<Longrightarrow> ?Incl e1" .
- have hyp_e2: "?Boolean e2 \<Longrightarrow> ?Incl e2" .
- have wt: "E\<turnstile>(c ? e1 : e2)\<Colon>-PrimT Boolean" .
+ note hyp_c = `?Boolean c \<Longrightarrow> ?Incl c`
+ note hyp_e1 = `?Boolean e1 \<Longrightarrow> ?Incl e1`
+ note hyp_e2 = `?Boolean e2 \<Longrightarrow> ?Incl e2`
+ note wt = `E\<turnstile>(c ? e1 : e2)\<Colon>-PrimT Boolean`
then obtain
boolean_c: "E\<turnstile>c\<Colon>-PrimT Boolean" and
boolean_e1: "E\<turnstile>e1\<Colon>-PrimT Boolean" and
@@ -1049,9 +1049,9 @@
by (auto simp add: range_inter_ts_def)
lemma da_monotone:
- assumes da: "Env\<turnstile> B \<guillemotright>t\<guillemotright> A" and
- subseteq_B_B': "B \<subseteq> B'" and
- da': "Env\<turnstile> B' \<guillemotright>t\<guillemotright> A'"
+ assumes da: "Env\<turnstile> B \<guillemotright>t\<guillemotright> A" and
+ "B \<subseteq> B'" and
+ da': "Env\<turnstile> B' \<guillemotright>t\<guillemotright> A'"
shows "(nrm A \<subseteq> nrm A') \<and> (\<forall> l. (brk A l \<subseteq> brk A' l))"
proof -
from da
@@ -1068,10 +1068,10 @@
show ?case by cases simp
next
case (Lab Env B c C A l B' A')
- have A: "nrm A = nrm C \<inter> brk C l" "brk A = rmlab l (brk C)" .
- have "PROP ?Hyp Env B \<langle>c\<rangle> C" .
+ note A = `nrm A = nrm C \<inter> brk C l` `brk A = rmlab l (brk C)`
+ note `PROP ?Hyp Env B \<langle>c\<rangle> C`
moreover
- have "B \<subseteq> B'" .
+ note `B \<subseteq> B'`
moreover
obtain C'
where "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'"
@@ -1094,40 +1094,40 @@
by simp
next
case (Comp Env B c1 C1 c2 C2 A B' A')
- have A: "nrm A = nrm C2" "brk A = brk C1 \<Rightarrow>\<inter> brk C2" .
- have "Env\<turnstile> B' \<guillemotright>\<langle>c1;; c2\<rangle>\<guillemotright> A'" .
- then obtain C1' C2'
+ note A = `nrm A = nrm C2` `brk A = brk C1 \<Rightarrow>\<inter> brk C2`
+ from `Env\<turnstile> B' \<guillemotright>\<langle>c1;; c2\<rangle>\<guillemotright> A'`
+ obtain C1' C2'
where da_c1: "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and
da_c2: "Env\<turnstile> nrm C1' \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and
A': "nrm A' = nrm C2'" "brk A' = brk C1' \<Rightarrow>\<inter> brk C2'"
by (rule da_elim_cases) auto
- have "PROP ?Hyp Env B \<langle>c1\<rangle> C1" .
- moreover have "B \<subseteq> B'" .
+ note `PROP ?Hyp Env B \<langle>c1\<rangle> C1`
+ moreover note `B \<subseteq> B'`
moreover note da_c1
ultimately have C1': "nrm C1 \<subseteq> nrm C1'" "(\<forall>l. brk C1 l \<subseteq> brk C1' l)"
- by (auto)
- have "PROP ?Hyp Env (nrm C1) \<langle>c2\<rangle> C2" .
+ by auto
+ note `PROP ?Hyp Env (nrm C1) \<langle>c2\<rangle> C2`
with da_c2 C1'
have C2': "nrm C2 \<subseteq> nrm C2'" "(\<forall>l. brk C2 l \<subseteq> brk C2' l)"
- by (auto)
+ by auto
with A A' C1'
show ?case
by auto
next
case (If Env B e E c1 C1 c2 C2 A B' A')
- have A: "nrm A = nrm C1 \<inter> nrm C2" "brk A = brk C1 \<Rightarrow>\<inter> brk C2" .
- have "Env\<turnstile> B' \<guillemotright>\<langle>If(e) c1 Else c2\<rangle>\<guillemotright> A'" .
- then obtain C1' C2'
+ note A = `nrm A = nrm C1 \<inter> nrm C2` `brk A = brk C1 \<Rightarrow>\<inter> brk C2`
+ from `Env\<turnstile> B' \<guillemotright>\<langle>If(e) c1 Else c2\<rangle>\<guillemotright> A'`
+ obtain C1' C2'
where da_c1: "Env\<turnstile> B' \<union> assigns_if True e \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and
da_c2: "Env\<turnstile> B' \<union> assigns_if False e \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and
A': "nrm A' = nrm C1' \<inter> nrm C2'" "brk A' = brk C1' \<Rightarrow>\<inter> brk C2'"
by (rule da_elim_cases) auto
- have "PROP ?Hyp Env (B \<union> assigns_if True e) \<langle>c1\<rangle> C1" .
- moreover have B': "B \<subseteq> B'" .
+ note `PROP ?Hyp Env (B \<union> assigns_if True e) \<langle>c1\<rangle> C1`
+ moreover note B' = `B \<subseteq> B'`
moreover note da_c1
ultimately obtain C1': "nrm C1 \<subseteq> nrm C1'" "(\<forall>l. brk C1 l \<subseteq> brk C1' l)"
by blast
- have "PROP ?Hyp Env (B \<union> assigns_if False e) \<langle>c2\<rangle> C2" .
+ note `PROP ?Hyp Env (B \<union> assigns_if False e) \<langle>c2\<rangle> C2`
with da_c2 B'
obtain C2': "nrm C2 \<subseteq> nrm C2'" "(\<forall>l. brk C2 l \<subseteq> brk C2' l)"
by blast
@@ -1136,17 +1136,16 @@
by auto
next
case (Loop Env B e E c C A l B' A')
- have A: "nrm A = nrm C \<inter> (B \<union> assigns_if False e)"
- "brk A = brk C" .
- have "Env\<turnstile> B' \<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<guillemotright> A'" .
- then obtain C'
+ note A = `nrm A = nrm C \<inter> (B \<union> assigns_if False e)` `brk A = brk C`
+ from `Env\<turnstile> B' \<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<guillemotright> A'`
+ obtain C'
where
da_c': "Env\<turnstile> B' \<union> assigns_if True e \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'" and
A': "nrm A' = nrm C' \<inter> (B' \<union> assigns_if False e)"
"brk A' = brk C'"
by (rule da_elim_cases) auto
- have "PROP ?Hyp Env (B \<union> assigns_if True e) \<langle>c\<rangle> C" .
- moreover have B': "B \<subseteq> B'" .
+ note `PROP ?Hyp Env (B \<union> assigns_if True e) \<langle>c\<rangle> C`
+ moreover note B' = `B \<subseteq> B'`
moreover note da_c'
ultimately obtain C': "nrm C \<subseteq> nrm C'" "(\<forall>l. brk C l \<subseteq> brk C' l)"
by blast
@@ -1177,23 +1176,22 @@
case Throw thus ?case by - (erule da_elim_cases, auto)
next
case (Try Env B c1 C1 vn C c2 C2 A B' A')
- have A: "nrm A = nrm C1 \<inter> nrm C2"
- "brk A = brk C1 \<Rightarrow>\<inter> brk C2" .
- have "Env\<turnstile> B' \<guillemotright>\<langle>Try c1 Catch(C vn) c2\<rangle>\<guillemotright> A'" .
- then obtain C1' C2'
+ note A = `nrm A = nrm C1 \<inter> nrm C2` `brk A = brk C1 \<Rightarrow>\<inter> brk C2`
+ from `Env\<turnstile> B' \<guillemotright>\<langle>Try c1 Catch(C vn) c2\<rangle>\<guillemotright> A'`
+ obtain C1' C2'
where da_c1': "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and
da_c2': "Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>\<turnstile> B' \<union> {VName vn}
\<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and
A': "nrm A' = nrm C1' \<inter> nrm C2'"
"brk A' = brk C1' \<Rightarrow>\<inter> brk C2'"
by (rule da_elim_cases) auto
- have "PROP ?Hyp Env B \<langle>c1\<rangle> C1" .
- moreover have B': "B \<subseteq> B'" .
+ note `PROP ?Hyp Env B \<langle>c1\<rangle> C1`
+ moreover note B' = `B \<subseteq> B'`
moreover note da_c1'
ultimately obtain C1': "nrm C1 \<subseteq> nrm C1'" "(\<forall>l. brk C1 l \<subseteq> brk C1' l)"
by blast
- have "PROP ?Hyp (Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>)
- (B \<union> {VName vn}) \<langle>c2\<rangle> C2" .
+ note `PROP ?Hyp (Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>)
+ (B \<union> {VName vn}) \<langle>c2\<rangle> C2`
with B' da_c2'
obtain "nrm C2 \<subseteq> nrm C2'" "(\<forall>l. brk C2 l \<subseteq> brk C2' l)"
by blast
@@ -1202,21 +1200,21 @@
by auto
next
case (Fin Env B c1 C1 c2 C2 A B' A')
- have A: "nrm A = nrm C1 \<union> nrm C2"
- "brk A = (brk C1 \<Rightarrow>\<union>\<^sub>\<forall> nrm C2) \<Rightarrow>\<inter> (brk C2)" .
- have "Env\<turnstile> B' \<guillemotright>\<langle>c1 Finally c2\<rangle>\<guillemotright> A'" .
- then obtain C1' C2'
+ note A = `nrm A = nrm C1 \<union> nrm C2`
+ `brk A = (brk C1 \<Rightarrow>\<union>\<^sub>\<forall> nrm C2) \<Rightarrow>\<inter> (brk C2)`
+ from `Env\<turnstile> B' \<guillemotright>\<langle>c1 Finally c2\<rangle>\<guillemotright> A'`
+ obtain C1' C2'
where da_c1': "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and
da_c2': "Env\<turnstile> B' \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and
A': "nrm A' = nrm C1' \<union> nrm C2'"
"brk A' = (brk C1' \<Rightarrow>\<union>\<^sub>\<forall> nrm C2') \<Rightarrow>\<inter> (brk C2')"
by (rule da_elim_cases) auto
- have "PROP ?Hyp Env B \<langle>c1\<rangle> C1" .
- moreover have B': "B \<subseteq> B'" .
+ note `PROP ?Hyp Env B \<langle>c1\<rangle> C1`
+ moreover note B' = `B \<subseteq> B'`
moreover note da_c1'
ultimately obtain C1': "nrm C1 \<subseteq> nrm C1'" "(\<forall>l. brk C1 l \<subseteq> brk C1' l)"
by blast
- have hyp_c2: "PROP ?Hyp Env B \<langle>c2\<rangle> C2" .
+ note hyp_c2 = `PROP ?Hyp Env B \<langle>c2\<rangle> C2`
from da_c2' B'
obtain "nrm C2 \<subseteq> nrm C2'" "(\<forall>l. brk C2 l \<subseteq> brk C2' l)"
by - (drule hyp_c2,auto)
@@ -1239,17 +1237,17 @@
case UnOp thus ?case by - (erule da_elim_cases, auto)
next
case (CondAnd Env B e1 E1 e2 E2 A B' A')
- have A: "nrm A = B \<union>
+ note A = `nrm A = B \<union>
assigns_if True (BinOp CondAnd e1 e2) \<inter>
- assigns_if False (BinOp CondAnd e1 e2)"
- "brk A = (\<lambda>l. UNIV)" .
- have "Env\<turnstile> B' \<guillemotright>\<langle>BinOp CondAnd e1 e2\<rangle>\<guillemotright> A'" .
- then obtain A': "nrm A' = B' \<union>
+ assigns_if False (BinOp CondAnd e1 e2)`
+ `brk A = (\<lambda>l. UNIV)`
+ from `Env\<turnstile> B' \<guillemotright>\<langle>BinOp CondAnd e1 e2\<rangle>\<guillemotright> A'`
+ obtain A': "nrm A' = B' \<union>
assigns_if True (BinOp CondAnd e1 e2) \<inter>
assigns_if False (BinOp CondAnd e1 e2)"
"brk A' = (\<lambda>l. UNIV)"
by (rule da_elim_cases) auto
- have B': "B \<subseteq> B'" .
+ note B' = `B \<subseteq> B'`
with A A' show ?case
by auto
next
@@ -1268,13 +1266,13 @@
case Ass thus ?case by - (erule da_elim_cases, auto)
next
case (CondBool Env c e1 e2 B C E1 E2 A B' A')
- have A: "nrm A = B \<union>
+ note A = `nrm A = B \<union>
assigns_if True (c ? e1 : e2) \<inter>
- assigns_if False (c ? e1 : e2)"
- "brk A = (\<lambda>l. UNIV)" .
- have "Env\<turnstile> (c ? e1 : e2)\<Colon>- (PrimT Boolean)" .
+ assigns_if False (c ? e1 : e2)`
+ `brk A = (\<lambda>l. UNIV)`
+ note `Env\<turnstile> (c ? e1 : e2)\<Colon>- (PrimT Boolean)`
moreover
- have "Env\<turnstile> B' \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A'" .
+ note `Env\<turnstile> B' \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A'`
ultimately
obtain A': "nrm A' = B' \<union>
assigns_if True (c ? e1 : e2) \<inter>
@@ -1282,16 +1280,15 @@
"brk A' = (\<lambda>l. UNIV)"
by - (erule da_elim_cases,auto simp add: inj_term_simps)
(* inj_term_simps needed to handle wt (defined without \<langle>\<rangle>) *)
- have B': "B \<subseteq> B'" .
+ note B' = `B \<subseteq> B'`
with A A' show ?case
by auto
next
case (Cond Env c e1 e2 B C E1 E2 A B' A')
- have A: "nrm A = nrm E1 \<inter> nrm E2"
- "brk A = (\<lambda>l. UNIV)" .
- have not_bool: "\<not> Env\<turnstile> (c ? e1 : e2)\<Colon>- (PrimT Boolean)" .
- have "Env\<turnstile> B' \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A'" .
- then obtain E1' E2'
+ note A = `nrm A = nrm E1 \<inter> nrm E2` `brk A = (\<lambda>l. UNIV)`
+ note not_bool = `\<not> Env\<turnstile> (c ? e1 : e2)\<Colon>- (PrimT Boolean)`
+ from `Env\<turnstile> B' \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A'`
+ obtain E1' E2'
where da_e1': "Env\<turnstile> B' \<union> assigns_if True c \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'" and
da_e2': "Env\<turnstile> B' \<union> assigns_if False c \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2'" and
A': "nrm A' = nrm E1' \<inter> nrm E2'"
@@ -1299,12 +1296,12 @@
using not_bool
by - (erule da_elim_cases, auto simp add: inj_term_simps)
(* inj_term_simps needed to handle wt (defined without \<langle>\<rangle>) *)
- have "PROP ?Hyp Env (B \<union> assigns_if True c) \<langle>e1\<rangle> E1" .
- moreover have B': "B \<subseteq> B'" .
+ note `PROP ?Hyp Env (B \<union> assigns_if True c) \<langle>e1\<rangle> E1`
+ moreover note B' = `B \<subseteq> B'`
moreover note da_e1'
ultimately obtain E1': "nrm E1 \<subseteq> nrm E1'" "(\<forall>l. brk E1 l \<subseteq> brk E1' l)"
- by blast
- have "PROP ?Hyp Env (B \<union> assigns_if False c) \<langle>e2\<rangle> E2" .
+ by blast
+ note `PROP ?Hyp Env (B \<union> assigns_if False c) \<langle>e2\<rangle> E2`
with B' da_e2'
obtain "nrm E2 \<subseteq> nrm E2'" "(\<forall>l. brk E2 l \<subseteq> brk E2' l)"
by blast
@@ -1330,12 +1327,11 @@
next
case Cons thus ?case by - (erule da_elim_cases, auto)
qed
-qed
+qed (rule da', rule `B \<subseteq> B'`)
lemma da_weaken:
- assumes da: "Env\<turnstile> B \<guillemotright>t\<guillemotright> A" and
- subseteq_B_B': "B \<subseteq> B'"
- shows "\<exists> A'. Env \<turnstile> B' \<guillemotright>t\<guillemotright> A'"
+ assumes da: "Env\<turnstile> B \<guillemotright>t\<guillemotright> A" and "B \<subseteq> B'"
+ shows "\<exists> A'. Env \<turnstile> B' \<guillemotright>t\<guillemotright> A'"
proof -
note assigned.select_convs [Pure.intro]
from da
@@ -1346,9 +1342,9 @@
case Expr thus ?case by (iprover intro: da.Expr)
next
case (Lab Env B c C A l B')
- have "PROP ?Hyp Env B \<langle>c\<rangle>" .
+ note `PROP ?Hyp Env B \<langle>c\<rangle>`
moreover
- have B': "B \<subseteq> B'" .
+ note B' = `B \<subseteq> B'`
ultimately obtain C' where "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'"
by iprover
then obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>Break l\<bullet> c\<rangle>\<guillemotright> A'"
@@ -1356,10 +1352,10 @@
thus ?case ..
next
case (Comp Env B c1 C1 c2 C2 A B')
- have da_c1: "Env\<turnstile> B \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1" .
- have "PROP ?Hyp Env B \<langle>c1\<rangle>" .
+ note da_c1 = `Env\<turnstile> B \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1`
+ note `PROP ?Hyp Env B \<langle>c1\<rangle>`
moreover
- have B': "B \<subseteq> B'" .
+ note B' = `B \<subseteq> B'`
ultimately obtain C1' where da_c1': "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'"
by iprover
with da_c1 B'
@@ -1367,7 +1363,7 @@
"nrm C1 \<subseteq> nrm C1'"
by (rule da_monotone [elim_format]) simp
moreover
- have "PROP ?Hyp Env (nrm C1) \<langle>c2\<rangle>" .
+ note `PROP ?Hyp Env (nrm C1) \<langle>c2\<rangle>`
ultimately obtain C2' where "Env\<turnstile> nrm C1' \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'"
by iprover
with da_c1' obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>c1;; c2\<rangle>\<guillemotright> A'"
@@ -1375,7 +1371,7 @@
thus ?case ..
next
case (If Env B e E c1 C1 c2 C2 A B')
- have B': "B \<subseteq> B'" .
+ note B' = `B \<subseteq> B'`
obtain E' where "Env\<turnstile> B' \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'"
proof -
have "PROP ?Hyp Env B \<langle>e\<rangle>" by (rule If.hyps)
@@ -1409,8 +1405,8 @@
thus ?case ..
next
case (Loop Env B e E c C A l B')
- have B': "B \<subseteq> B'" .
- obtain E' where "Env\<turnstile> B' \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'"
+ note B' = `B \<subseteq> B'`
+ obtain E' where "Env\<turnstile> B' \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'"
proof -
have "PROP ?Hyp Env B \<langle>e\<rangle>" by (rule Loop.hyps)
with B'
@@ -1433,7 +1429,7 @@
thus ?case ..
next
case (Jmp jump B A Env B')
- have B': "B \<subseteq> B'" .
+ note B' = `B \<subseteq> B'`
with Jmp.hyps have "jump = Ret \<longrightarrow> Result \<in> B' "
by auto
moreover
@@ -1452,7 +1448,7 @@
case Throw thus ?case by (iprover intro: da.Throw )
next
case (Try Env B c1 C1 vn C c2 C2 A B')
- have B': "B \<subseteq> B'" .
+ note B' = `B \<subseteq> B'`
obtain C1' where "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'"
proof -
have "PROP ?Hyp Env B \<langle>c1\<rangle>" by (rule Try.hyps)
@@ -1477,7 +1473,7 @@
thus ?case ..
next
case (Fin Env B c1 C1 c2 C2 A B')
- have B': "B \<subseteq> B'" .
+ note B' = `B \<subseteq> B'`
obtain C1' where C1': "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'"
proof -
have "PROP ?Hyp Env B \<langle>c1\<rangle>" by (rule Fin.hyps)
@@ -1511,11 +1507,11 @@
case UnOp thus ?case by (iprover intro: da.UnOp)
next
case (CondAnd Env B e1 E1 e2 E2 A B')
- have B': "B \<subseteq> B'" .
+ note B' = `B \<subseteq> B'`
obtain E1' where "Env\<turnstile> B' \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'"
proof -
have "PROP ?Hyp Env B \<langle>e1\<rangle>" by (rule CondAnd.hyps)
- with B'
+ with B'
show ?thesis using that by iprover
qed
moreover
@@ -1533,7 +1529,7 @@
thus ?case ..
next
case (CondOr Env B e1 E1 e2 E2 A B')
- have B': "B \<subseteq> B'" .
+ note B' = `B \<subseteq> B'`
obtain E1' where "Env\<turnstile> B' \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'"
proof -
have "PROP ?Hyp Env B \<langle>e1\<rangle>" by (rule CondOr.hyps)
@@ -1555,11 +1551,11 @@
thus ?case ..
next
case (BinOp Env B e1 E1 e2 A binop B')
- have B': "B \<subseteq> B'" .
+ note B' = `B \<subseteq> B'`
obtain E1' where E1': "Env\<turnstile> B' \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'"
proof -
have "PROP ?Hyp Env B \<langle>e1\<rangle>" by (rule BinOp.hyps)
- with B'
+ with B'
show ?thesis using that by iprover
qed
moreover
@@ -1579,22 +1575,22 @@
thus ?case ..
next
case (Super B Env B')
- have B': "B \<subseteq> B'" .
- with Super.hyps have "This \<in> B' "
+ note B' = `B \<subseteq> B'`
+ with Super.hyps have "This \<in> B'"
by auto
thus ?case by (iprover intro: da.Super)
next
case (AccLVar vn B A Env B')
- have "vn \<in> B" .
+ note `vn \<in> B`
moreover
- have "B \<subseteq> B'" .
+ note `B \<subseteq> B'`
ultimately have "vn \<in> B'" by auto
thus ?case by (iprover intro: da.AccLVar)
next
case Acc thus ?case by (iprover intro: da.Acc)
next
case (AssLVar Env B e E A vn B')
- have B': "B \<subseteq> B'" .
+ note B' = `B \<subseteq> B'`
then obtain E' where "Env\<turnstile> B' \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'"
by (rule AssLVar.hyps [elim_format]) iprover
then obtain A' where
@@ -1603,8 +1599,8 @@
thus ?case ..
next
case (Ass v Env B V e A B')
- have B': "B \<subseteq> B'" .
- have "\<forall>vn. v \<noteq> LVar vn".
+ note B' = `B \<subseteq> B'`
+ note `\<forall>vn. v \<noteq> LVar vn`
moreover
obtain V' where V': "Env\<turnstile> B' \<guillemotright>\<langle>v\<rangle>\<guillemotright> V'"
proof -
@@ -1629,8 +1625,8 @@
thus ?case ..
next
case (CondBool Env c e1 e2 B C E1 E2 A B')
- have B': "B \<subseteq> B'" .
- have "Env\<turnstile>(c ? e1 : e2)\<Colon>-(PrimT Boolean)" .
+ note B' = `B \<subseteq> B'`
+ note `Env\<turnstile>(c ? e1 : e2)\<Colon>-(PrimT Boolean)`
moreover obtain C' where C': "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'"
proof -
have "PROP ?Hyp Env B \<langle>c\<rangle>" by (rule CondBool.hyps)
@@ -1665,8 +1661,8 @@
thus ?case ..
next
case (Cond Env c e1 e2 B C E1 E2 A B')
- have B': "B \<subseteq> B'" .
- have "\<not> Env\<turnstile>(c ? e1 : e2)\<Colon>-(PrimT Boolean)" .
+ note B' = `B \<subseteq> B'`
+ note `\<not> Env\<turnstile>(c ? e1 : e2)\<Colon>-(PrimT Boolean)`
moreover obtain C' where C': "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'"
proof -
have "PROP ?Hyp Env B \<langle>c\<rangle>" by (rule Cond.hyps)
@@ -1701,7 +1697,7 @@
thus ?case ..
next
case (Call Env B e E args A accC statT mode mn pTs B')
- have B': "B \<subseteq> B'" .
+ note B' = `B \<subseteq> B'`
obtain E' where E': "Env\<turnstile> B' \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'"
proof -
have "PROP ?Hyp Env B \<langle>e\<rangle>" by (rule Call.hyps)
@@ -1727,7 +1723,7 @@
case Methd thus ?case by (iprover intro: da.Methd)
next
case (Body Env B c C A D B')
- have B': "B \<subseteq> B'" .
+ note B' = `B \<subseteq> B'`
obtain C' where C': "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'" and nrm_C': "nrm C \<subseteq> nrm C'"
proof -
have "Env\<turnstile> B \<guillemotright>\<langle>c\<rangle>\<guillemotright> C" by (rule Body.hyps)
@@ -1741,10 +1737,10 @@
with da_c that show ?thesis by iprover
qed
moreover
- have "Result \<in> nrm C" .
+ note `Result \<in> nrm C`
with nrm_C' have "Result \<in> nrm C'"
by blast
- moreover have "jumpNestingOkS {Ret} c" .
+ moreover note `jumpNestingOkS {Ret} c`
ultimately obtain A' where
"Env\<turnstile> B' \<guillemotright>\<langle>Body D c\<rangle>\<guillemotright> A'"
by (iprover intro: da.Body)
@@ -1755,11 +1751,11 @@
case FVar thus ?case by (iprover intro: da.FVar)
next
case (AVar Env B e1 E1 e2 A B')
- have B': "B \<subseteq> B'" .
+ note B' = `B \<subseteq> B'`
obtain E1' where E1': "Env\<turnstile> B' \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'"
proof -
have "PROP ?Hyp Env B \<langle>e1\<rangle>" by (rule AVar.hyps)
- with B'
+ with B'
show ?thesis using that by iprover
qed
moreover
@@ -1781,7 +1777,7 @@
case Nil thus ?case by (iprover intro: da.Nil)
next
case (Cons Env B e E es A B')
- have B': "B \<subseteq> B'" .
+ note B' = `B \<subseteq> B'`
obtain E' where E': "Env\<turnstile> B' \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'"
proof -
have "PROP ?Hyp Env B \<langle>e\<rangle>" by (rule Cons.hyps)
@@ -1804,7 +1800,7 @@
by (iprover intro: da.Cons)
thus ?case ..
qed
-qed
+qed (rule `B \<subseteq> B'`)
(* Remarks about the proof style:
--- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy Wed Jun 13 00:01:38 2007 +0200
+++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy Wed Jun 13 00:01:41 2007 +0200
@@ -1,3 +1,5 @@
+(* $Id$ *)
+
header {* Correctness of Definite Assignment *}
theory DefiniteAssignmentCorrect imports WellForm Eval begin
@@ -107,8 +109,8 @@
and True
proof (induct rule: var_expr_stmt.inducts)
case (Lab j c jmps' jmps)
- have jmpOk: "jumpNestingOkS jmps' (j\<bullet> c)" .
- have jmps: "jmps' \<subseteq> jmps" .
+ note jmpOk = `jumpNestingOkS jmps' (j\<bullet> c)`
+ note jmps = `jmps' \<subseteq> jmps`
with jmpOk have "jumpNestingOkS ({j} \<union> jmps') c" by simp
moreover from jmps have "({j} \<union> jmps') \<subseteq> ({j} \<union> jmps)" by auto
ultimately
@@ -138,10 +140,11 @@
by simp
next
case (Loop l e c jmps' jmps)
- have "jumpNestingOkS jmps' (l\<bullet> While(e) c)" .
- hence "jumpNestingOkS ({Cont l} \<union> jmps') c" by simp
- moreover have "jmps' \<subseteq> jmps" .
- hence "{Cont l} \<union> jmps' \<subseteq> {Cont l} \<union> jmps" by auto
+ from `jumpNestingOkS jmps' (l\<bullet> While(e) c)`
+ have "jumpNestingOkS ({Cont l} \<union> jmps') c" by simp
+ moreover
+ from `jmps' \<subseteq> jmps`
+ have "{Cont l} \<union> jmps' \<subseteq> {Cont l} \<union> jmps" by auto
ultimately
have "jumpNestingOkS ({Cont l} \<union> jmps) c"
by (rule Loop.hyps)
@@ -310,8 +313,8 @@
case Expr thus ?case by (elim wt_elim_cases) simp
next
case (Lab s0 c s1 jmp jmps T Env)
- have jmpOK: "jumpNestingOk jmps (In1r (jmp\<bullet> c))" .
- have G: "prg Env = G" .
+ note jmpOK = `jumpNestingOk jmps (In1r (jmp\<bullet> c))`
+ note G = `prg Env = G`
have wt_c: "Env\<turnstile>c\<Colon>\<surd>"
using Lab.prems by (elim wt_elim_cases)
{
@@ -321,7 +324,7 @@
proof -
from ab_s1 have jmp_s1: "abrupt s1 = Some (Jump j)"
by (cases s1) (simp add: absorb_def)
- have hyp_c: "PROP ?Hyp (In1r c) (Norm s0) s1 \<diamondsuit>" .
+ note hyp_c = `PROP ?Hyp (In1r c) (Norm s0) s1 \<diamondsuit>`
from ab_s1 have "j \<noteq> jmp"
by (cases s1) (simp add: absorb_def)
moreover have "j \<in> {jmp} \<union> jmps"
@@ -339,9 +342,9 @@
thus ?case by simp
next
case (Comp s0 c1 s1 c2 s2 jmps T Env)
- have jmpOk: "jumpNestingOk jmps (In1r (c1;; c2))" .
- have G: "prg Env = G" .
- from Comp.prems obtain
+ note jmpOk = `jumpNestingOk jmps (In1r (c1;; c2))`
+ note G = `prg Env = G`
+ from Comp.prems obtain
wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and wt_c2: "Env\<turnstile>c2\<Colon>\<surd>"
by (elim wt_elim_cases)
{
@@ -351,11 +354,11 @@
proof -
have jmp: "?Jmp jmps s1"
proof -
- have hyp_c1: "PROP ?Hyp (In1r c1) (Norm s0) s1 \<diamondsuit>" .
+ note hyp_c1 = `PROP ?Hyp (In1r c1) (Norm s0) s1 \<diamondsuit>`
with wt_c1 jmpOk G
show ?thesis by simp
qed
- moreover have hyp_c2: "PROP ?Hyp (In1r c2) s1 s2 (\<diamondsuit>::vals)" .
+ moreover note hyp_c2 = `PROP ?Hyp (In1r c2) s1 s2 (\<diamondsuit>::vals)`
have jmpOk': "jumpNestingOk jmps (In1r c2)" using jmpOk by simp
moreover note wt_c2 G abr_s2
ultimately show "j \<in> jmps"
@@ -364,8 +367,8 @@
} thus ?case by simp
next
case (If s0 e b s1 c1 c2 s2 jmps T Env)
- have jmpOk: "jumpNestingOk jmps (In1r (If(e) c1 Else c2))" .
- have G: "prg Env = G" .
+ note jmpOk = `jumpNestingOk jmps (In1r (If(e) c1 Else c2))`
+ note G = `prg Env = G`
from If.prems obtain
wt_e: "Env\<turnstile>e\<Colon>-PrimT Boolean" and
wt_then_else: "Env\<turnstile>(if the_Bool b then c1 else c2)\<Colon>\<surd>"
@@ -375,11 +378,11 @@
assume jmp: "abrupt s2 = Some (Jump j)"
have "j\<in>jmps"
proof -
- have "PROP ?Hyp (In1l e) (Norm s0) s1 (In1 b)" .
+ note `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 b)`
with wt_e G have "?Jmp jmps s1"
by simp
- moreover have hyp_then_else:
- "PROP ?Hyp (In1r (if the_Bool b then c1 else c2)) s1 s2 \<diamondsuit>" .
+ moreover note hyp_then_else =
+ `PROP ?Hyp (In1r (if the_Bool b then c1 else c2)) s1 s2 \<diamondsuit>`
have "jumpNestingOk jmps (In1r (if the_Bool b then c1 else c2))"
using jmpOk by (cases "the_Bool b") simp_all
moreover note wt_then_else G jmp
@@ -390,9 +393,9 @@
thus ?case by simp
next
case (Loop s0 e b s1 c s2 l s3 jmps T Env)
- have jmpOk: "jumpNestingOk jmps (In1r (l\<bullet> While(e) c))" .
- have G: "prg Env = G" .
- have wt: "Env\<turnstile>In1r (l\<bullet> While(e) c)\<Colon>T" .
+ note jmpOk = `jumpNestingOk jmps (In1r (l\<bullet> While(e) c))`
+ note G = `prg Env = G`
+ note wt = `Env\<turnstile>In1r (l\<bullet> While(e) c)\<Colon>T`
then obtain
wt_e: "Env\<turnstile>e\<Colon>-PrimT Boolean" and
wt_c: "Env\<turnstile>c\<Colon>\<surd>"
@@ -402,7 +405,7 @@
assume jmp: "abrupt s3 = Some (Jump j)"
have "j\<in>jmps"
proof -
- have "PROP ?Hyp (In1l e) (Norm s0) s1 (In1 b)" .
+ note `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 b)`
with wt_e G have jmp_s1: "?Jmp jmps s1"
by simp
show ?thesis
@@ -470,8 +473,8 @@
case (Jmp s j jmps T Env) thus ?case by simp
next
case (Throw s0 e a s1 jmps T Env)
- have jmpOk: "jumpNestingOk jmps (In1r (Throw e))" .
- have G: "prg Env = G" .
+ note jmpOk = `jumpNestingOk jmps (In1r (Throw e))`
+ note G = `prg Env = G`
from Throw.prems obtain Te where
wt_e: "Env\<turnstile>e\<Colon>-Te"
by (elim wt_elim_cases)
@@ -480,8 +483,8 @@
assume jmp: "abrupt (abupd (throw a) s1) = Some (Jump j)"
have "j\<in>jmps"
proof -
- have "PROP ?Hyp (In1l e) (Norm s0) s1 (In1 a)" .
- hence "?Jmp jmps s1" using wt_e G by simp
+ from `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 a)`
+ have "?Jmp jmps s1" using wt_e G by simp
moreover
from jmp
have "abrupt s1 = Some (Jump j)"
@@ -492,8 +495,8 @@
thus ?case by simp
next
case (Try s0 c1 s1 s2 C vn c2 s3 jmps T Env)
- have jmpOk: "jumpNestingOk jmps (In1r (Try c1 Catch(C vn) c2))" .
- have G: "prg Env = G" .
+ note jmpOk = `jumpNestingOk jmps (In1r (Try c1 Catch(C vn) c2))`
+ note G = `prg Env = G`
from Try.prems obtain
wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and
wt_c2: "Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>\<turnstile>c2\<Colon>\<surd>"
@@ -503,10 +506,10 @@
assume jmp: "abrupt s3 = Some (Jump j)"
have "j\<in>jmps"
proof -
- have "PROP ?Hyp (In1r c1) (Norm s0) s1 (\<diamondsuit>::vals)" .
+ note `PROP ?Hyp (In1r c1) (Norm s0) s1 (\<diamondsuit>::vals)`
with jmpOk wt_c1 G
have jmp_s1: "?Jmp jmps s1" by simp
- have s2: "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" .
+ note s2 = `G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2`
show "j \<in> jmps"
proof (cases "G,s2\<turnstile>catch C")
case False
@@ -544,8 +547,8 @@
thus ?case by simp
next
case (Fin s0 c1 x1 s1 c2 s2 s3 jmps T Env)
- have jmpOk: " jumpNestingOk jmps (In1r (c1 Finally c2))" .
- have G: "prg Env = G" .
+ note jmpOk = `jumpNestingOk jmps (In1r (c1 Finally c2))`
+ note G = `prg Env = G`
from Fin.prems obtain
wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and wt_c2: "Env\<turnstile>c2\<Colon>\<surd>"
by (elim wt_elim_cases)
@@ -555,16 +558,16 @@
have "j \<in> jmps"
proof (cases "x1=Some (Jump j)")
case True
- have hyp_c1: "PROP ?Hyp (In1r c1) (Norm s0) (x1,s1) \<diamondsuit>" .
+ note hyp_c1 = `PROP ?Hyp (In1r c1) (Norm s0) (x1,s1) \<diamondsuit>`
with True jmpOk wt_c1 G show ?thesis
by - (rule hyp_c1 [THEN conjunct1,rule_format (no_asm)],simp_all)
next
case False
- have hyp_c2: "PROP ?Hyp (In1r c2) (Norm s1) s2 \<diamondsuit>" .
- have "s3 = (if \<exists>err. x1 = Some (Error err) then (x1, s1)
- else abupd (abrupt_if (x1 \<noteq> None) x1) s2)" .
+ note hyp_c2 = `PROP ?Hyp (In1r c2) (Norm s1) s2 \<diamondsuit>`
+ note `s3 = (if \<exists>err. x1 = Some (Error err) then (x1, s1)
+ else abupd (abrupt_if (x1 \<noteq> None) x1) s2)`
with False jmp have "abrupt s2 = Some (Jump j)"
- by (cases s2, simp add: abrupt_if_def)
+ by (cases s2) (simp add: abrupt_if_def)
with jmpOk wt_c2 G show ?thesis
by - (rule hyp_c2 [THEN conjunct1,rule_format (no_asm)],simp_all)
qed
@@ -572,9 +575,9 @@
thus ?case by simp
next
case (Init C c s0 s3 s1 s2 jmps T Env)
- have "jumpNestingOk jmps (In1r (Init C))".
- have G: "prg Env = G" .
- have "the (class G C) = c" .
+ note `jumpNestingOk jmps (In1r (Init C))`
+ note G = `prg Env = G`
+ note `the (class G C) = c`
with Init.prems have c: "class G C = Some c"
by (elim wt_elim_cases) auto
{
@@ -642,16 +645,15 @@
assume jmp: "abrupt s2 = Some (Jump j)"
have "j\<in>jmps"
proof -
- have "prg Env = G" .
- moreover have hyp_init: "PROP ?Hyp (In1r (Init C)) (Norm s0) s1 \<diamondsuit>" .
+ note `prg Env = G`
+ moreover note hyp_init = `PROP ?Hyp (In1r (Init C)) (Norm s0) s1 \<diamondsuit>`
moreover from wf NewC.prems
have "Env\<turnstile>(Init C)\<Colon>\<surd>"
by (elim wt_elim_cases) (drule is_acc_classD,simp)
moreover
have "abrupt s1 = Some (Jump j)"
proof -
- have "G\<turnstile>s1 \<midarrow>halloc CInst C\<succ>a\<rightarrow> s2" .
- from this jmp show ?thesis
+ from `G\<turnstile>s1 \<midarrow>halloc CInst C\<succ>a\<rightarrow> s2` and jmp show ?thesis
by (rule halloc_no_jump')
qed
ultimately show "j \<in> jmps"
@@ -666,20 +668,20 @@
assume jmp: "abrupt s3 = Some (Jump j)"
have "j\<in>jmps"
proof -
- have G: "prg Env = G" .
+ note G = `prg Env = G`
from NewA.prems
obtain wt_init: "Env\<turnstile>init_comp_ty elT\<Colon>\<surd>" and
wt_size: "Env\<turnstile>e\<Colon>-PrimT Integer"
by (elim wt_elim_cases) (auto dest: wt_init_comp_ty')
- have "PROP ?Hyp (In1r (init_comp_ty elT)) (Norm s0) s1 \<diamondsuit>" .
+ note `PROP ?Hyp (In1r (init_comp_ty elT)) (Norm s0) s1 \<diamondsuit>`
with wt_init G
have "?Jmp jmps s1"
by (simp add: init_comp_ty_def)
moreover
- have hyp_e: "PROP ?Hyp (In1l e) s1 s2 (In1 i)" .
+ note hyp_e = `PROP ?Hyp (In1l e) s1 s2 (In1 i)`
have "abrupt s2 = Some (Jump j)"
proof -
- have "G\<turnstile>abupd (check_neg i) s2\<midarrow>halloc Arr elT (the_Intg i)\<succ>a\<rightarrow> s3".
+ note `G\<turnstile>abupd (check_neg i) s2\<midarrow>halloc Arr elT (the_Intg i)\<succ>a\<rightarrow> s3`
moreover note jmp
ultimately
have "abrupt (abupd (check_neg i) s2) = Some (Jump j)"
@@ -698,14 +700,14 @@
assume jmp: "abrupt s2 = Some (Jump j)"
have "j\<in>jmps"
proof -
- have hyp_e: "PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)" .
- have "prg Env = G" .
+ note hyp_e = `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)`
+ note `prg Env = G`
moreover from Cast.prems
obtain eT where "Env\<turnstile>e\<Colon>-eT" by (elim wt_elim_cases)
moreover
have "abrupt s1 = Some (Jump j)"
proof -
- have "s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits cT) ClassCast) s1" .
+ note `s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits cT) ClassCast) s1`
moreover note jmp
ultimately show ?thesis by (cases s1) (simp add: abrupt_if_def)
qed
@@ -721,8 +723,8 @@
assume jmp: "abrupt s1 = Some (Jump j)"
have "j\<in>jmps"
proof -
- have hyp_e: "PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)" .
- have "prg Env = G" .
+ note hyp_e = `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)`
+ note `prg Env = G`
moreover from Inst.prems
obtain eT where "Env\<turnstile>e\<Colon>-eT" by (elim wt_elim_cases)
moreover note jmp
@@ -740,8 +742,8 @@
assume jmp: "abrupt s1 = Some (Jump j)"
have "j\<in>jmps"
proof -
- have hyp_e: "PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)" .
- have "prg Env = G" .
+ note hyp_e = `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)`
+ note `prg Env = G`
moreover from UnOp.prems
obtain eT where "Env\<turnstile>e\<Colon>-eT" by (elim wt_elim_cases)
moreover note jmp
@@ -757,17 +759,17 @@
assume jmp: "abrupt s2 = Some (Jump j)"
have "j\<in>jmps"
proof -
- have G: "prg Env = G" .
+ note G = `prg Env = G`
from BinOp.prems
obtain e1T e2T where
wt_e1: "Env\<turnstile>e1\<Colon>-e1T" and
wt_e2: "Env\<turnstile>e2\<Colon>-e2T"
by (elim wt_elim_cases)
- have "PROP ?Hyp (In1l e1) (Norm s0) s1 (In1 v1)" .
+ note `PROP ?Hyp (In1l e1) (Norm s0) s1 (In1 v1)`
with G wt_e1 have jmp_s1: "?Jmp jmps s1" by simp
- have hyp_e2:
- "PROP ?Hyp (if need_second_arg binop v1 then In1l e2 else In1r Skip)
- s1 s2 (In1 v2)" .
+ note hyp_e2 =
+ `PROP ?Hyp (if need_second_arg binop v1 then In1l e2 else In1r Skip)
+ s1 s2 (In1 v2)`
show "j\<in>jmps"
proof (cases "need_second_arg binop v1")
case True with jmp_s1 wt_e2 jmp G
@@ -790,8 +792,8 @@
assume jmp: "abrupt s1 = Some (Jump j)"
have "j\<in>jmps"
proof -
- have hyp_va: "PROP ?Hyp (In2 va) (Norm s0) s1 (In2 (v,f))" .
- have "prg Env = G" .
+ note hyp_va = `PROP ?Hyp (In2 va) (Norm s0) s1 (In2 (v,f))`
+ note `prg Env = G`
moreover from Acc.prems
obtain vT where "Env\<turnstile>va\<Colon>=vT" by (elim wt_elim_cases)
moreover note jmp
@@ -802,14 +804,14 @@
thus ?case by simp
next
case (Ass s0 va w f s1 e v s2 jmps T Env)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
from Ass.prems
obtain vT eT where
wt_va: "Env\<turnstile>va\<Colon>=vT" and
wt_e: "Env\<turnstile>e\<Colon>-eT"
by (elim wt_elim_cases)
- have hyp_v: "PROP ?Hyp (In2 va) (Norm s0) s1 (In2 (w,f))" .
- have hyp_e: "PROP ?Hyp (In1l e) s1 s2 (In1 v)" .
+ note hyp_v = `PROP ?Hyp (In2 va) (Norm s0) s1 (In2 (w,f))`
+ note hyp_e = `PROP ?Hyp (In1l e) s1 s2 (In1 v)`
{
fix j
assume jmp: "abrupt (assign f v s2) = Some (Jump j)"
@@ -818,8 +820,7 @@
have "abrupt s2 = Some (Jump j)"
proof (cases "normal s2")
case True
- have "G\<turnstile>s1 \<midarrow>e-\<succ>v\<rightarrow> s2" .
- from this True have nrm_s1: "normal s1"
+ from `G\<turnstile>s1 \<midarrow>e-\<succ>v\<rightarrow> s2` and True have nrm_s1: "normal s1"
by (rule eval_no_abrupt_lemma [rule_format])
with nrm_s1 wt_va G True
have "abrupt (f v s2) \<noteq> Some (Jump j)"
@@ -836,16 +837,15 @@
have "?Jmp jmps s1"
by - (rule hyp_v [THEN conjunct1],simp_all)
ultimately show ?thesis using G
- by - (rule hyp_e [THEN conjunct1,rule_format (no_asm)],simp_all)
+ by - (rule hyp_e [THEN conjunct1,rule_format (no_asm)], simp_all, rule wt_e)
qed
}
thus ?case by simp
next
case (Cond s0 e0 b s1 e1 e2 v s2 jmps T Env)
- have G: "prg Env = G" .
- have hyp_e0: "PROP ?Hyp (In1l e0) (Norm s0) s1 (In1 b)" .
- have hyp_e1_e2: "PROP ?Hyp (In1l (if the_Bool b then e1 else e2))
- s1 s2 (In1 v)" .
+ note G = `prg Env = G`
+ note hyp_e0 = `PROP ?Hyp (In1l e0) (Norm s0) s1 (In1 b)`
+ note hyp_e1_e2 = `PROP ?Hyp (In1l (if the_Bool b then e1 else e2)) s1 s2 (In1 v)`
from Cond.prems
obtain e1T e2T
where wt_e0: "Env\<turnstile>e0\<Colon>-PrimT Boolean"
@@ -878,7 +878,7 @@
next
case (Call s0 e a s1 args vs s2 D mode statT mn pTs s3 s3' accC v s4
jmps T Env)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
from Call.prems
obtain eT argsT
where wt_e: "Env\<turnstile>e\<Colon>-eT" and wt_args: "Env\<turnstile>args\<Colon>\<doteq>argsT"
@@ -889,26 +889,26 @@
= Some (Jump j)"
have "j\<in>jmps"
proof -
- have hyp_e: "PROP ?Hyp (In1l e) (Norm s0) s1 (In1 a)" .
+ note hyp_e = `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 a)`
from wt_e G
have jmp_s1: "?Jmp jmps s1"
by - (rule hyp_e [THEN conjunct1],simp_all)
- have hyp_args: "PROP ?Hyp (In3 args) s1 s2 (In3 vs)" .
+ note hyp_args = `PROP ?Hyp (In3 args) s1 s2 (In3 vs)`
have "abrupt s2 = Some (Jump j)"
proof -
- have "G\<turnstile>s3' \<midarrow>Methd D \<lparr>name = mn, parTs = pTs\<rparr>-\<succ>v\<rightarrow> s4" .
+ note `G\<turnstile>s3' \<midarrow>Methd D \<lparr>name = mn, parTs = pTs\<rparr>-\<succ>v\<rightarrow> s4`
moreover
from jmp have "abrupt s4 = Some (Jump j)"
by (cases s4) simp
ultimately have "abrupt s3' = Some (Jump j)"
by - (rule ccontr,drule (1) Methd_no_jump,simp)
- moreover have "s3' = check_method_access G accC statT mode
- \<lparr>name = mn, parTs = pTs\<rparr> a s3" .
+ moreover note `s3' = check_method_access G accC statT mode
+ \<lparr>name = mn, parTs = pTs\<rparr> a s3`
ultimately have "abrupt s3 = Some (Jump j)"
by (cases s3)
(simp add: check_method_access_def abrupt_if_def Let_def)
moreover
- have "s3 = init_lvars G D \<lparr>name=mn, parTs=pTs\<rparr> mode a vs s2" .
+ note `s3 = init_lvars G D \<lparr>name=mn, parTs=pTs\<rparr> mode a vs s2`
ultimately show ?thesis
by (cases s2) (auto simp add: init_lvars_def2)
qed
@@ -920,6 +920,7 @@
thus ?case by simp
next
case (Methd s0 D sig v s1 jmps T Env)
+ from `G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1`
have "G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<rightarrow> s1"
by (rule eval.Methd)
hence "\<And> j. abrupt s1 \<noteq> Some (Jump j)"
@@ -929,7 +930,7 @@
case (Body s0 D s1 c s2 s3 jmps T Env)
have "G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)
\<rightarrow> abupd (absorb Ret) s3"
- by (rule eval.Body)
+ by (rule eval.Body) (rule Body)+
hence "\<And> j. abrupt (abupd (absorb Ret) s3) \<noteq> Some (Jump j)"
by (rule Body_no_jump) simp
thus ?case by simp
@@ -938,7 +939,7 @@
thus ?case by (simp add: lvar_def Let_def)
next
case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC jmps T Env)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
from wf FVar.prems
obtain statC f where
wt_e: "Env\<turnstile>e\<Colon>-Class statC" and
@@ -955,21 +956,21 @@
thus ?thesis
by simp
qed
- have fvar: "(v, s2') = fvar statDeclC stat fn a s2" .
+ note fvar = `(v, s2') = fvar statDeclC stat fn a s2`
{
fix j
assume jmp: "abrupt s3 = Some (Jump j)"
have "j\<in>jmps"
proof -
- have hyp_init: "PROP ?Hyp (In1r (Init statDeclC)) (Norm s0) s1 \<diamondsuit>" .
+ note hyp_init = `PROP ?Hyp (In1r (Init statDeclC)) (Norm s0) s1 \<diamondsuit>`
from G wt_init
have "?Jmp jmps s1"
by - (rule hyp_init [THEN conjunct1],auto)
moreover
- have hyp_e: "PROP ?Hyp (In1l e) s1 s2 (In1 a)" .
+ note hyp_e = `PROP ?Hyp (In1l e) s1 s2 (In1 a)`
have "abrupt s2 = Some (Jump j)"
proof -
- have "s3 = check_field_access G accC statDeclC fn stat a s2'" .
+ note `s3 = check_field_access G accC statDeclC fn stat a s2'`
with jmp have "abrupt s2' = Some (Jump j)"
by (cases s2')
(simp add: check_field_access_def abrupt_if_def Let_def)
@@ -997,23 +998,23 @@
ultimately show ?case using v by simp
next
case (AVar s0 e1 a s1 e2 i s2 v s2' jmps T Env)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
from AVar.prems
obtain e1T e2T where
wt_e1: "Env\<turnstile>e1\<Colon>-e1T" and wt_e2: "Env\<turnstile>e2\<Colon>-e2T"
by (elim wt_elim_cases) simp
- have avar: "(v, s2') = avar G i a s2" .
+ note avar = `(v, s2') = avar G i a s2`
{
fix j
assume jmp: "abrupt s2' = Some (Jump j)"
have "j\<in>jmps"
proof -
- have hyp_e1: "PROP ?Hyp (In1l e1) (Norm s0) s1 (In1 a)" .
+ note hyp_e1 = `PROP ?Hyp (In1l e1) (Norm s0) s1 (In1 a)`
from G wt_e1
have "?Jmp jmps s1"
- by - (rule hyp_e1 [THEN conjunct1],auto)
+ by - (rule hyp_e1 [THEN conjunct1], auto)
moreover
- have hyp_e2: "PROP ?Hyp (In1l e2) s1 s2 (In1 i)" .
+ note hyp_e2 = `PROP ?Hyp (In1l e2) s1 s2 (In1 i)`
have "abrupt s2 = Some (Jump j)"
proof -
from avar have "s2' = snd (avar G i a s2)"
@@ -1043,7 +1044,7 @@
case Nil thus ?case by simp
next
case (Cons s0 e v s1 es vs s2 jmps T Env)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
from Cons.prems obtain eT esT
where wt_e: "Env\<turnstile>e\<Colon>-eT" and wt_e2: "Env\<turnstile>es\<Colon>\<doteq>esT"
by (elim wt_elim_cases) simp
@@ -1052,12 +1053,12 @@
assume jmp: "abrupt s2 = Some (Jump j)"
have "j\<in>jmps"
proof -
- have hyp_e: "PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)" .
+ note hyp_e = `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)`
from G wt_e
have "?Jmp jmps s1"
by - (rule hyp_e [THEN conjunct1],simp_all)
moreover
- have hyp_es: "PROP ?Hyp (In3 es) s1 s2 (In3 vs)" .
+ note hyp_es = `PROP ?Hyp (In3 es) s1 s2 (In3 vs)`
ultimately show ?thesis
using wt_e2 G jmp
by - (rule hyp_es [THEN conjunct1, rule_format (no_asm)],
@@ -1199,7 +1200,7 @@
by auto
moreover
obtain x1 s1 where "f n s = (x1,s1)"
- by (cases "f n s", simp)
+ by (cases "f n s")
ultimately
show ?thesis
using f_ok
@@ -1338,8 +1339,8 @@
then
have s0_s1: "dom (locals (store ((Norm s0)::state)))
\<subseteq> dom (locals (store s1))" by simp
- have "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" .
- hence s1_s2: "dom (locals (store s1)) \<subseteq> dom (locals (store s2))"
+ from `G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2`
+ have s1_s2: "dom (locals (store s1)) \<subseteq> dom (locals (store s2))"
by (rule dom_locals_sxalloc_mono)
thus ?case
proof (cases "G,s2\<turnstile>catch C")
@@ -1406,7 +1407,7 @@
qed
next
case (NewC s0 C s1 a s2)
- have halloc: "G\<turnstile>s1 \<midarrow>halloc CInst C\<succ>a\<rightarrow> s2" .
+ note halloc = `G\<turnstile>s1 \<midarrow>halloc CInst C\<succ>a\<rightarrow> s2`
from NewC.hyps
have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
by simp
@@ -1416,7 +1417,7 @@
finally show ?case by simp
next
case (NewA s0 T s1 e i s2 a s3)
- have halloc: "G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3" .
+ note halloc = `G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3`
from NewA.hyps
have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
by simp
@@ -1474,8 +1475,7 @@
finally show ?thesis by simp
next
case False
- have "G\<turnstile>s1 \<midarrow>e-\<succ>v\<rightarrow> s2" .
- with False
+ with `G\<turnstile>s1 \<midarrow>e-\<succ>v\<rightarrow> s2`
have "s2=s1"
by auto
with s0_s1 False
@@ -1497,7 +1497,7 @@
finally show ?case by simp
next
case (Call s0 e a' s1 args vs s2 D mode statT mn pTs s3 s3' accC v s4)
- have s3: "s3 = init_lvars G D \<lparr>name = mn, parTs = pTs\<rparr> mode a' vs s2" .
+ note s3 = `s3 = init_lvars G D \<lparr>name = mn, parTs = pTs\<rparr> mode a' vs s2`
from Call.hyps
have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
by simp
@@ -1526,11 +1526,11 @@
also
have "\<dots> \<subseteq> dom (locals (store (abupd (absorb Ret) s3)))"
proof -
- have "s3 =
+ from `s3 =
(if \<exists>l. abrupt s2 = Some (Jump (Break l)) \<or>
abrupt s2 = Some (Jump (Cont l))
- then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 else s2)".
- thus ?thesis
+ then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 else s2)`
+ show ?thesis
by simp
qed
finally show ?case by simp
@@ -1551,7 +1551,7 @@
by (simp add: dom_locals_fvar_vvar_mono)
hence v_ok: "(\<forall>vv. In2 v = In2 vv \<and> normal s3 \<longrightarrow> ?V_ok)"
by - (intro strip, simp)
- have s3: "s3 = check_field_access G accC statDeclC fn stat a s2'" .
+ note s3 = `s3 = check_field_access G accC statDeclC fn stat a s2'`
from FVar.hyps
have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
by simp
@@ -1690,7 +1690,7 @@
case NewC show ?case by simp
next
case (NewA s0 T s1 e i s2 a s3)
- have halloc: "G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3" .
+ note halloc = `G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3`
have "assigns (In1l e) \<subseteq> dom (locals (store s2))"
proof -
from NewA
@@ -1733,8 +1733,8 @@
also
have "\<dots> \<subseteq> dom (locals (store s2))"
proof -
- have "G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2
- else In1r Skip)\<succ>\<rightarrow> (In1 v2, s2)" .
+ note `G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2
+ else In1r Skip)\<succ>\<rightarrow> (In1 v2, s2)`
thus ?thesis
by (rule dom_locals_eval_mono_elim)
qed
@@ -1757,7 +1757,7 @@
case Acc thus ?case by simp
next
case (Ass s0 va w f s1 e v s2)
- have nrm_ass_s2: "normal (assign f v s2)" .
+ note nrm_ass_s2 = `normal (assign f v s2)`
hence nrm_s2: "normal s2"
by (cases s2, simp add: assign_def Let_def)
with Ass.hyps
@@ -1848,16 +1848,16 @@
case (Call s0 e a' s1 args vs s2 D mode statT mn pTs s3 s3' accC v s4)
have nrm_s2: "normal s2"
proof -
- have "normal ((set_lvars (locals (snd s2))) s4)" .
- hence normal_s4: "normal s4" by simp
+ from `normal ((set_lvars (locals (snd s2))) s4)`
+ have normal_s4: "normal s4" by simp
hence "normal s3'" using Call.hyps
by - (erule eval_no_abrupt_lemma [rule_format])
- moreover have
- "s3' = check_method_access G accC statT mode \<lparr>name=mn, parTs=pTs\<rparr> a' s3".
+ moreover note
+ `s3' = check_method_access G accC statT mode \<lparr>name=mn, parTs=pTs\<rparr> a' s3`
ultimately have "normal s3"
by (cases s3) (simp add: check_method_access_def Let_def)
moreover
- have s3: "s3 = init_lvars G D \<lparr>name = mn, parTs = pTs\<rparr> mode a' vs s2" .
+ note s3 = `s3 = init_lvars G D \<lparr>name = mn, parTs = pTs\<rparr> mode a' vs s2`
ultimately show "normal s2"
by (cases s2) (simp add: init_lvars_def2)
qed
@@ -1888,11 +1888,11 @@
case LVar thus ?case by simp
next
case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC)
- have s3: "s3 = check_field_access G accC statDeclC fn stat a s2'" .
- have avar: "(v, s2') = fvar statDeclC stat fn a s2" .
+ note s3 = `s3 = check_field_access G accC statDeclC fn stat a s2'`
+ note avar = `(v, s2') = fvar statDeclC stat fn a s2`
have nrm_s2: "normal s2"
proof -
- have "normal s3" .
+ note `normal s3`
with s3 have "normal s2'"
by (cases s2') (simp add: check_field_access_def Let_def)
with avar show "normal s2"
@@ -1917,11 +1917,10 @@
by simp
next
case (AVar s0 e1 a s1 e2 i s2 v s2')
- have avar: "(v, s2') = avar G i a s2" .
+ note avar = `(v, s2') = avar G i a s2`
have nrm_s2: "normal s2"
proof -
- have "normal s2'" .
- with avar
+ from avar and `normal s2'`
show ?thesis by (cases s2) (simp add: avar_def2)
qed
with AVar.hyps
@@ -2024,19 +2023,19 @@
case Inst hence False by simp thus ?case ..
next
case (Lit val c v s0 s)
- have "constVal (Lit val) = Some c" .
+ note `constVal (Lit val) = Some c`
moreover
- have "G\<turnstile>Norm s0 \<midarrow>Lit val-\<succ>v\<rightarrow> s" .
- then obtain "v=val" and "normal s"
+ from `G\<turnstile>Norm s0 \<midarrow>Lit val-\<succ>v\<rightarrow> s`
+ obtain "v=val" and "normal s"
by cases simp
ultimately show "v=c \<and> normal s" by simp
next
case (UnOp unop e c v s0 s)
- have const: "constVal (UnOp unop e) = Some c" .
+ note const = `constVal (UnOp unop e) = Some c`
then obtain ce where ce: "constVal e = Some ce" by simp
- have "G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>v\<rightarrow> s" .
- then obtain ve where ve: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>ve\<rightarrow> s" and
- v: "v = eval_unop unop ve"
+ from `G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>v\<rightarrow> s`
+ obtain ve where ve: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>ve\<rightarrow> s" and
+ v: "v = eval_unop unop ve"
by cases simp
from ce ve
obtain eq_ve_ce: "ve=ce" and nrm_s: "normal s"
@@ -2048,13 +2047,13 @@
show ?case ..
next
case (BinOp binop e1 e2 c v s0 s)
- have const: "constVal (BinOp binop e1 e2) = Some c" .
+ note const = `constVal (BinOp binop e1 e2) = Some c`
then obtain c1 c2 where c1: "constVal e1 = Some c1" and
c2: "constVal e2 = Some c2" and
c: "c = eval_binop binop c1 c2"
by simp
- have "G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>v\<rightarrow> s" .
- then obtain v1 s1 v2
+ from `G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>v\<rightarrow> s`
+ obtain v1 s1 v2
where v1: "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1" and
v2: "G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2
else In1r Skip)\<succ>\<rightarrow> (In1 v2, s)" and
@@ -2095,14 +2094,14 @@
case Ass hence False by simp thus ?case ..
next
case (Cond b e1 e2 c v s0 s)
- have c: "constVal (b ? e1 : e2) = Some c" .
+ note c = `constVal (b ? e1 : e2) = Some c`
then obtain cb c1 c2 where
cb: "constVal b = Some cb" and
c1: "constVal e1 = Some c1" and
c2: "constVal e2 = Some c2"
by (auto split: bool.splits)
- have "G\<turnstile>Norm s0 \<midarrow>b ? e1 : e2-\<succ>v\<rightarrow> s" .
- then obtain vb s1
+ from `G\<turnstile>Norm s0 \<midarrow>b ? e1 : e2-\<succ>v\<rightarrow> s`
+ obtain vb s1
where vb: "G\<turnstile>Norm s0 \<midarrow>b-\<succ>vb\<rightarrow> s1" and
eval_v: "G\<turnstile>s1 \<midarrow>(if the_Bool vb then e1 else e2)-\<succ>v\<rightarrow> s"
by cases simp
@@ -2172,25 +2171,28 @@
case Inst hence False by simp thus ?case ..
next
case (Lit v c)
- have "constVal (Lit v) = Some c" .
- hence "c=v" by simp
- moreover have "Env\<turnstile>Lit v\<Colon>-PrimT Boolean" .
- hence "typeof empty_dt v = Some (PrimT Boolean)"
+ from `constVal (Lit v) = Some c`
+ have "c=v" by simp
+ moreover
+ from `Env\<turnstile>Lit v\<Colon>-PrimT Boolean`
+ have "typeof empty_dt v = Some (PrimT Boolean)"
by cases simp
ultimately show ?case by simp
next
case (UnOp unop e c)
- have "Env\<turnstile>UnOp unop e\<Colon>-PrimT Boolean" .
- hence "Boolean = unop_type unop" by cases simp
- moreover have "constVal (UnOp unop e) = Some c" .
- then obtain ce where "c = eval_unop unop ce" by auto
+ from `Env\<turnstile>UnOp unop e\<Colon>-PrimT Boolean`
+ have "Boolean = unop_type unop" by cases simp
+ moreover
+ from `constVal (UnOp unop e) = Some c`
+ obtain ce where "c = eval_unop unop ce" by auto
ultimately show ?case by (simp add: eval_unop_type)
next
case (BinOp binop e1 e2 c)
- have "Env\<turnstile>BinOp binop e1 e2\<Colon>-PrimT Boolean" .
- hence "Boolean = binop_type binop" by cases simp
- moreover have "constVal (BinOp binop e1 e2) = Some c" .
- then obtain c1 c2 where "c = eval_binop binop c1 c2" by auto
+ from `Env\<turnstile>BinOp binop e1 e2\<Colon>-PrimT Boolean`
+ have "Boolean = binop_type binop" by cases simp
+ moreover
+ from `constVal (BinOp binop e1 e2) = Some c`
+ obtain c1 c2 where "c = eval_binop binop c1 c2" by auto
ultimately show ?case by (simp add: eval_binop_type)
next
case Super hence False by simp thus ?case ..
@@ -2200,13 +2202,13 @@
case Ass hence False by simp thus ?case ..
next
case (Cond b e1 e2 c)
- have c: "constVal (b ? e1 : e2) = Some c" .
+ note c = `constVal (b ? e1 : e2) = Some c`
then obtain cb c1 c2 where
cb: "constVal b = Some cb" and
c1: "constVal e1 = Some c1" and
c2: "constVal e2 = Some c2"
by (auto split: bool.splits)
- have wt: "Env\<turnstile>b ? e1 : e2\<Colon>-PrimT Boolean" .
+ note wt = `Env\<turnstile>b ? e1 : e2\<Colon>-PrimT Boolean`
then
obtain T1 T2
where "Env\<turnstile>b\<Colon>-PrimT Boolean" and
@@ -2255,28 +2257,28 @@
case Abrupt thus ?case by simp
next
case (NewC s0 C s1 a s2)
- have "Env\<turnstile>NewC C\<Colon>-PrimT Boolean" .
- hence False
+ from `Env\<turnstile>NewC C\<Colon>-PrimT Boolean`
+ have False
by cases simp
thus ?case ..
next
case (NewA s0 T s1 e i s2 a s3)
- have "Env\<turnstile>New T[e]\<Colon>-PrimT Boolean" .
- hence False
+ from `Env\<turnstile>New T[e]\<Colon>-PrimT Boolean`
+ have False
by cases simp
thus ?case ..
next
case (Cast s0 e b s1 s2 T)
- have s2: "s2 = abupd (raise_if (\<not> prg Env,snd s1\<turnstile>b fits T) ClassCast) s1".
+ note s2 = `s2 = abupd (raise_if (\<not> prg Env,snd s1\<turnstile>b fits T) ClassCast) s1`
have "assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))"
proof -
- have "normal s2" .
- with s2 have "normal s1"
+ from s2 and `normal s2`
+ have "normal s1"
by (cases s1) simp
moreover
- have "Env\<turnstile>Cast T e\<Colon>-PrimT Boolean" .
- hence "Env\<turnstile>e\<Colon>- PrimT Boolean"
- by (cases) (auto dest: cast_Boolean2)
+ from `Env\<turnstile>Cast T e\<Colon>-PrimT Boolean`
+ have "Env\<turnstile>e\<Colon>- PrimT Boolean"
+ by cases (auto dest: cast_Boolean2)
ultimately show ?thesis
by (rule Cast.hyps [elim_format]) auto
qed
@@ -2286,15 +2288,15 @@
finally show ?case by simp
next
case (Inst s0 e v s1 b T)
- have "prg Env\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1" and "normal s1" .
- hence "assignsE e \<subseteq> dom (locals (store s1))"
+ from `prg Env\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1` and `normal s1`
+ have "assignsE e \<subseteq> dom (locals (store s1))"
by (rule assignsE_good_approx)
thus ?case
by simp
next
case (Lit s v)
- have "Env\<turnstile>Lit v\<Colon>-PrimT Boolean" .
- hence "typeof empty_dt v = Some (PrimT Boolean)"
+ from `Env\<turnstile>Lit v\<Colon>-PrimT Boolean`
+ have "typeof empty_dt v = Some (PrimT Boolean)"
by cases simp
then obtain b where "v=Bool b"
by (cases v) (simp_all add: empty_dt_def)
@@ -2302,13 +2304,13 @@
by simp
next
case (UnOp s0 e v s1 unop)
- have bool: "Env\<turnstile>UnOp unop e\<Colon>-PrimT Boolean" .
+ note bool = `Env\<turnstile>UnOp unop e\<Colon>-PrimT Boolean`
hence bool_e: "Env\<turnstile>e\<Colon>-PrimT Boolean"
by cases (cases unop,simp_all)
show ?case
proof (cases "constVal (UnOp unop e)")
case None
- have "normal s1" .
+ note `normal s1`
moreover note bool_e
ultimately have "assigns_if (the_Bool v) e \<subseteq> dom (locals (store s1))"
by (rule UnOp.hyps [elim_format]) auto
@@ -2324,8 +2326,8 @@
next
case (Some c)
moreover
- have "prg Env\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1" .
- hence "prg Env\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>eval_unop unop v\<rightarrow> s1"
+ from `prg Env\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1`
+ have "prg Env\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>eval_unop unop v\<rightarrow> s1"
by (rule eval.UnOp)
with Some
have "eval_unop unop v=c"
@@ -2342,7 +2344,7 @@
qed
next
case (BinOp s0 e1 v1 s1 binop e2 v2 s2)
- have bool: "Env\<turnstile>BinOp binop e1 e2\<Colon>-PrimT Boolean" .
+ note bool = `Env\<turnstile>BinOp binop e1 e2\<Colon>-PrimT Boolean`
show ?case
proof (cases "constVal (BinOp binop e1 e2)")
case (Some c)
@@ -2395,8 +2397,8 @@
with condAnd
have need_second: "need_second_arg binop v1"
by (simp add: need_second_arg_def)
- have "normal s2" .
- hence "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"
+ from `normal s2`
+ have "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"
by (rule BinOp.hyps [elim_format])
(simp add: need_second bool_e2)+
with e1_s2
@@ -2415,8 +2417,8 @@
obtain "the_Bool v1=True" and "the_Bool v2 = False"
by (simp add: need_second_arg_def)
moreover
- have "normal s2" .
- hence "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"
+ from `normal s2`
+ have "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"
by (rule BinOp.hyps [elim_format]) (simp add: True bool_e2)+
with e1_s2
have "assigns_if (the_Bool v1) e1 \<union> assigns_if (the_Bool v2) e2
@@ -2443,8 +2445,8 @@
with condOr
have need_second: "need_second_arg binop v1"
by (simp add: need_second_arg_def)
- have "normal s2" .
- hence "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"
+ from `normal s2`
+ have "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"
by (rule BinOp.hyps [elim_format])
(simp add: need_second bool_e2)+
with e1_s2
@@ -2463,8 +2465,8 @@
obtain "the_Bool v1=False" and "the_Bool v2 = True"
by (simp add: need_second_arg_def)
moreover
- have "normal s2" .
- hence "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"
+ from `normal s2`
+ have "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"
by (rule BinOp.hyps [elim_format]) (simp add: True bool_e2)+
with e1_s2
have "assigns_if (the_Bool v1) e1 \<union> assigns_if (the_Bool v2) e2
@@ -2486,12 +2488,12 @@
qed
next
case False
- have "\<not> (binop = CondAnd \<or> binop = CondOr)" .
+ note `\<not> (binop = CondAnd \<or> binop = CondOr)`
from BinOp.hyps
have
- "prg Env\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>eval_binop binop v1 v2\<rightarrow> s2"
+ "prg Env\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>eval_binop binop v1 v2\<rightarrow> s2"
by - (rule eval.BinOp)
- moreover have "normal s2" .
+ moreover note `normal s2`
ultimately
have "assignsE (BinOp binop e1 e2) \<subseteq> dom (locals (store s2))"
by (rule assignsE_good_approx)
@@ -2502,38 +2504,37 @@
qed
next
case Super
- have "Env\<turnstile>Super\<Colon>-PrimT Boolean" .
+ note `Env\<turnstile>Super\<Colon>-PrimT Boolean`
hence False
by cases simp
thus ?case ..
next
case (Acc s0 va v f s1)
- have "prg Env\<turnstile>Norm s0 \<midarrow>va=\<succ>(v, f)\<rightarrow> s1" and "normal s1".
- hence "assignsV va \<subseteq> dom (locals (store s1))"
+ from `prg Env\<turnstile>Norm s0 \<midarrow>va=\<succ>(v, f)\<rightarrow> s1` and `normal s1`
+ have "assignsV va \<subseteq> dom (locals (store s1))"
by (rule assignsV_good_approx)
thus ?case by simp
next
case (Ass s0 va w f s1 e v s2)
hence "prg Env\<turnstile>Norm s0 \<midarrow>va := e-\<succ>v\<rightarrow> assign f v s2"
by - (rule eval.Ass)
- moreover have "normal (assign f v s2)" .
+ moreover note `normal (assign f v s2)`
ultimately
have "assignsE (va := e) \<subseteq> dom (locals (store (assign f v s2)))"
by (rule assignsE_good_approx)
thus ?case by simp
next
case (Cond s0 e0 b s1 e1 e2 v s2)
- have "Env\<turnstile>e0 ? e1 : e2\<Colon>-PrimT Boolean" .
- then obtain wt_e1: "Env\<turnstile>e1\<Colon>-PrimT Boolean" and
- wt_e2: "Env\<turnstile>e2\<Colon>-PrimT Boolean"
+ from `Env\<turnstile>e0 ? e1 : e2\<Colon>-PrimT Boolean`
+ obtain wt_e1: "Env\<turnstile>e1\<Colon>-PrimT Boolean" and
+ wt_e2: "Env\<turnstile>e2\<Colon>-PrimT Boolean"
by cases (auto dest: widen_Boolean2)
- have eval_e0: "prg Env\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1" .
+ note eval_e0 = `prg Env\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1`
have e0_s2: "assignsE e0 \<subseteq> dom (locals (store s2))"
proof -
note eval_e0
moreover
- have "normal s2" .
- with Cond.hyps have "normal s1"
+ from Cond.hyps and `normal s2` have "normal s1"
by - (erule eval_no_abrupt_lemma [rule_format],simp)
ultimately
have "assignsE e0 \<subseteq> dom (locals (store s1))"
@@ -2551,15 +2552,15 @@
\<subseteq> dom (locals (store s2))"
proof (cases "the_Bool b")
case True
- have "normal s2" .
- hence "assigns_if (the_Bool v) e1 \<subseteq> dom (locals (store s2))"
+ from `normal s2`
+ have "assigns_if (the_Bool v) e1 \<subseteq> dom (locals (store s2))"
by (rule Cond.hyps [elim_format]) (simp_all add: wt_e1 True)
thus ?thesis
by blast
next
case False
- have "normal s2" .
- hence "assigns_if (the_Bool v) e2 \<subseteq> dom (locals (store s2))"
+ from `normal s2`
+ have "assigns_if (the_Bool v) e2 \<subseteq> dom (locals (store s2))"
by (rule Cond.hyps [elim_format]) (simp_all add: wt_e2 False)
thus ?thesis
by blast
@@ -2578,9 +2579,9 @@
show ?thesis
proof (cases "the_Bool c")
case True
- have "normal s2" .
- hence "assigns_if (the_Bool v) e1 \<subseteq> dom (locals (store s2))"
- by (rule Cond.hyps [elim_format]) (simp_all add: eq_b_c True)
+ from `normal s2`
+ have "assigns_if (the_Bool v) e1 \<subseteq> dom (locals (store s2))"
+ by (rule Cond.hyps [elim_format]) (simp_all add: eq_b_c True wt_e1)
with e0_s2
have "assignsE e0 \<union> assigns_if (the_Bool v) e1 \<subseteq> \<dots>"
by (rule Un_least)
@@ -2588,9 +2589,9 @@
by simp
next
case False
- have "normal s2" .
- hence "assigns_if (the_Bool v) e2 \<subseteq> dom (locals (store s2))"
- by (rule Cond.hyps [elim_format]) (simp_all add: eq_b_c False)
+ from `normal s2`
+ have "assigns_if (the_Bool v) e2 \<subseteq> dom (locals (store s2))"
+ by (rule Cond.hyps [elim_format]) (simp_all add: eq_b_c False wt_e2)
with e0_s2
have "assignsE e0 \<union> assigns_if (the_Bool v) e2 \<subseteq> \<dots>"
by (rule Un_least)
@@ -2606,6 +2607,7 @@
by - (rule eval.Call)
hence "assignsE ({accC,statT,mode}e\<cdot>mn( {pTs}args))
\<subseteq> dom (locals (store ((set_lvars (locals (store s2))) s4)))"
+ using `normal ((set_lvars (locals (snd s2))) s4)`
by (rule assignsE_good_approx)
thus ?case by simp
next
@@ -2695,7 +2697,7 @@
(rule Expr.hyps, auto)
next
case (Lab s0 c s1 j Env T A)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
from Lab.prems
obtain C l where
da_c: "Env\<turnstile> dom (locals (snd (Norm s0))) \<guillemotright>\<langle>c\<rangle>\<guillemotright> C" and
@@ -2754,7 +2756,7 @@
ultimately show ?case by (intro conjI)
next
case (Comp s0 c1 s1 c2 s2 Env T A)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
from Comp.prems
obtain C1 C2
where da_c1: "Env\<turnstile> dom (locals (snd (Norm s0))) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1" and
@@ -2765,7 +2767,7 @@
obtain wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and
wt_c2: "Env\<turnstile>c2\<Colon>\<surd>"
by (elim wt_elim_cases) simp
- have "PROP ?Hyp (In1r c1) (Norm s0) s1" .
+ note `PROP ?Hyp (In1r c1) (Norm s0) s1`
with wt_c1 da_c1 G
obtain nrm_c1: "?NormalAssigned s1 C1" and
brk_c1: "?BreakAssigned (Norm s0) s1 C1" and
@@ -2780,7 +2782,7 @@
nrm_c2: "nrm C2 \<subseteq> nrm C2'" and
brk_c2: "\<forall> l. brk C2 l \<subseteq> brk C2' l"
by (rule da_weakenE) iprover
- have "PROP ?Hyp (In1r c2) s1 s2" .
+ note `PROP ?Hyp (In1r c2) s1 s2`
with wt_c2 da_c2' G
obtain nrm_c2': "?NormalAssigned s2 C2'" and
brk_c2': "?BreakAssigned s1 s2 C2'" and
@@ -2800,8 +2802,8 @@
ultimately show ?thesis by (intro conjI)
next
case False
- have "G\<turnstile>s1 \<midarrow>c2\<rightarrow> s2" .
- with False have eq_s1_s2: "s2=s1" by auto
+ with `G\<turnstile>s1 \<midarrow>c2\<rightarrow> s2`
+ have eq_s1_s2: "s2=s1" by auto
with False have "?NormalAssigned s2 A" by blast
moreover
have "?BreakAssigned (Norm s0) s2 A"
@@ -2827,16 +2829,16 @@
qed
next
case (If s0 e b s1 c1 c2 s2 Env T A)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
with If.hyps have eval_e: "prg Env \<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" by simp
from If.prems
obtain E C1 C2 where
da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> E" and
- da_c1: "Env\<turnstile> (dom (locals (store ((Norm s0)::state)))
+ da_c1: "Env\<turnstile> (dom (locals (store ((Norm s0)::state)))
\<union> assigns_if True e) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1" and
- da_c2: "Env\<turnstile> (dom (locals (store ((Norm s0)::state)))
+ da_c2: "Env\<turnstile> (dom (locals (store ((Norm s0)::state)))
\<union> assigns_if False e) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2" and
- A: "nrm A = nrm C1 \<inter> nrm C2" "brk A = brk C1 \<Rightarrow>\<inter> brk C2"
+ A: "nrm A = nrm C1 \<inter> nrm C2" "brk A = brk C1 \<Rightarrow>\<inter> brk C2"
by (elim da_elim_cases)
from If.prems
obtain
@@ -2923,15 +2925,15 @@
moreover
have "s2 = s1"
proof -
- have "G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2" .
- with abr show ?thesis
+ from abr and `G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2`
+ show ?thesis
by (cases s1) simp
qed
ultimately show ?thesis by simp
qed
next
case (Loop s0 e b s1 c s2 l s3 Env T A)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
with Loop.hyps have eval_e: "prg Env\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1"
by (simp (no_asm_simp))
from Loop.prems
@@ -3137,7 +3139,7 @@
ultimately show ?case by (intro conjI)
next
case (Throw s0 e a s1 Env T A)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
from Throw.prems obtain E where
da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> E"
by (elim da_elim_cases)
@@ -3167,7 +3169,7 @@
ultimately show ?case by (intro conjI)
next
case (Try s0 c1 s1 s2 C vn c2 s3 Env T A)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
from Try.prems obtain C1 C2 where
da_c1: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1" and
da_c2:
@@ -3181,7 +3183,7 @@
by (elim wt_elim_cases)
have sxalloc: "prg Env\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" using Try.hyps G
by (simp (no_asm_simp))
- have "PROP ?Hyp (In1r c1) (Norm s0) s1" .
+ note `PROP ?Hyp (In1r c1) (Norm s0) s1`
with wt_c1 da_c1 G
obtain nrm_C1: "?NormalAssigned s1 C1" and
brk_C1: "?BreakAssigned (Norm s0) s1 C1" and
@@ -3239,8 +3241,8 @@
have "(dom (locals (store ((Norm s0)::state))) \<union> {VName vn})
\<subseteq> dom (locals (store (new_xcpt_var vn s2)))"
proof -
- have "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1" .
- hence "dom (locals (store ((Norm s0)::state)))
+ from `G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1`
+ have "dom (locals (store ((Norm s0)::state)))
\<subseteq> dom (locals (store s1))"
by (rule dom_locals_eval_mono_elim)
also
@@ -3314,7 +3316,7 @@
qed
next
case (Fin s0 c1 x1 s1 c2 s2 s3 Env T A)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
from Fin.prems obtain C1 C2 where
da_C1: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1" and
da_C2: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2" and
@@ -3325,7 +3327,7 @@
wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and
wt_c2: "Env\<turnstile>c2\<Colon>\<surd>"
by (elim wt_elim_cases)
- have "PROP ?Hyp (In1r c1) (Norm s0) (x1,s1)" .
+ note `PROP ?Hyp (In1r c1) (Norm s0) (x1,s1)`
with wt_c1 da_C1 G
obtain nrmAss_C1: "?NormalAssigned (x1,s1) C1" and
brkAss_C1: "?BreakAssigned (Norm s0) (x1,s1) C1" and
@@ -3345,7 +3347,7 @@
nrm_C2': "nrm C2 \<subseteq> nrm C2'" and
brk_C2': "\<forall> l. brk C2 l \<subseteq> brk C2' l"
by (rule da_weakenE) simp
- have "PROP ?Hyp (In1r c2) (Norm s1) s2" .
+ note `PROP ?Hyp (In1r c2) (Norm s1) s2`
with wt_c2 da_C2' G
obtain nrmAss_C2': "?NormalAssigned s2 C2'" and
brkAss_C2': "?BreakAssigned (Norm s1) s2 C2'" and
@@ -3360,12 +3362,12 @@
show ?thesis
using that resAss_s2' by simp
qed
- have s3: "s3 = (if \<exists>err. x1 = Some (Error err) then (x1, s1)
- else abupd (abrupt_if (x1 \<noteq> None) x1) s2)" .
+ note s3 = `s3 = (if \<exists>err. x1 = Some (Error err) then (x1, s1)
+ else abupd (abrupt_if (x1 \<noteq> None) x1) s2)`
have s1_s2: "dom (locals s1) \<subseteq> dom (locals (store s2))"
proof -
- have "G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2" .
- thus ?thesis
+ from `G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2`
+ show ?thesis
by (rule dom_locals_eval_mono_elim) simp
qed
@@ -3455,7 +3457,7 @@
by simp
moreover have "dom (locals (store ((Norm s1)::state)))
\<subseteq> dom (locals (store s2))"
- by (rule dom_locals_eval_mono_elim)
+ by (rule dom_locals_eval_mono_elim) (rule Fin.hyps)
ultimately have "Result \<in> dom (locals (store s2))"
by - (rule subsetD,auto)
with res_s1 s3 show ?thesis
@@ -3473,7 +3475,7 @@
ultimately show ?case by (intro conjI)
next
case (Init C c s0 s3 s1 s2 Env T A)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
from Init.hyps
have eval: "prg Env\<turnstile> Norm s0 \<midarrow>Init C\<rightarrow> s3"
apply (simp only: G)
@@ -3483,8 +3485,7 @@
apply (simp only: if_False )
apply (elim conjE,intro conjI,assumption+,simp)
done (* auto or simp alone always do too much *)
- have "the (class G C) = c" .
- with Init.prems
+ from Init.prems and `the (class G C) = c`
have c: "class G C = Some c"
by (elim wt_elim_cases) auto
from Init.prems obtain
@@ -3529,7 +3530,7 @@
qed
next
case (NewC s0 C s1 a s2 Env T A)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
from NewC.prems
obtain A: "nrm A = dom (locals (store ((Norm s0)::state)))"
"brk A = (\<lambda> l. UNIV)"
@@ -3540,10 +3541,10 @@
have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s2))"
proof -
have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
- by (rule dom_locals_eval_mono_elim)
+ by (rule dom_locals_eval_mono_elim) (rule NewC.hyps)
also
have "\<dots> \<subseteq> dom (locals (store s2))"
- by (rule dom_locals_halloc_mono)
+ by (rule dom_locals_halloc_mono) (rule NewC.hyps)
finally show ?thesis .
qed
with A have "?NormalAssigned s2 A"
@@ -3553,7 +3554,7 @@
fix j have "abrupt s2 \<noteq> Some (Jump j)"
proof -
have eval: "prg Env\<turnstile> Norm s0 \<midarrow>NewC C-\<succ>Addr a\<rightarrow> s2"
- by (simp only: G) (rule eval.NewC)
+ unfolding G by (rule eval.NewC NewC.hyps)+
from NewC.prems
obtain T' where "T=Inl T'"
by (elim wt_elim_cases) simp
@@ -3569,7 +3570,7 @@
ultimately show ?case by (intro conjI)
next
case (NewA s0 elT s1 e i s2 a s3 Env T A)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
from NewA.prems obtain
da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A"
by (elim da_elim_cases)
@@ -3577,15 +3578,15 @@
wt_init: "Env\<turnstile>init_comp_ty elT\<Colon>\<surd>" and
wt_size: "Env\<turnstile>e\<Colon>-PrimT Integer"
by (elim wt_elim_cases) (auto dest: wt_init_comp_ty')
- have halloc:"G\<turnstile>abupd (check_neg i) s2\<midarrow>halloc Arr elT (the_Intg i)\<succ>a\<rightarrow>s3".
+ note halloc = `G\<turnstile>abupd (check_neg i) s2\<midarrow>halloc Arr elT (the_Intg i)\<succ>a\<rightarrow>s3`
have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
- by (rule dom_locals_eval_mono_elim)
+ by (rule dom_locals_eval_mono_elim) (rule NewA.hyps)
with da_e obtain A' where
da_e': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A'"
and nrm_A_A': "nrm A \<subseteq> nrm A'"
and brk_A_A': "\<forall> l. brk A l \<subseteq> brk A' l"
by (rule da_weakenE) simp
- have "PROP ?Hyp (In1l e) s1 s2" .
+ note `PROP ?Hyp (In1l e) s1 s2`
with wt_size da_e' G obtain
nrmAss_A': "?NormalAssigned s2 A'" and
brkAss_A': "?BreakAssigned s1 s2 A'"
@@ -3596,7 +3597,7 @@
\<subseteq> dom (locals (store (abupd (check_neg i) s2)))"
by (simp)
also have "\<dots> \<subseteq> dom (locals (store s3))"
- by (rule dom_locals_halloc_mono)
+ by (rule dom_locals_halloc_mono) (rule NewA.hyps)
finally show ?thesis .
qed
have "?NormalAssigned s3 A"
@@ -3618,7 +3619,7 @@
fix j have "abrupt s3 \<noteq> Some (Jump j)"
proof -
have eval: "prg Env\<turnstile> Norm s0 \<midarrow>New elT[e]-\<succ>Addr a\<rightarrow> s3"
- by (simp only: G) (rule eval.NewA)
+ unfolding G by (rule eval.NewA NewA.hyps)+
from NewA.prems
obtain T' where "T=Inl T'"
by (elim wt_elim_cases) simp
@@ -3634,19 +3635,19 @@
ultimately show ?case by (intro conjI)
next
case (Cast s0 e v s1 s2 cT Env T A)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
from Cast.prems obtain
da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A"
by (elim da_elim_cases)
from Cast.prems obtain eT where
wt_e: "Env\<turnstile>e\<Colon>-eT"
by (elim wt_elim_cases)
- have "PROP ?Hyp (In1l e) (Norm s0) s1" .
+ note `PROP ?Hyp (In1l e) (Norm s0) s1`
with wt_e da_e G obtain
nrmAss_A: "?NormalAssigned s1 A" and
brkAss_A: "?BreakAssigned (Norm s0) s1 A"
by simp
- have s2: "s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits cT) ClassCast) s1" .
+ note s2 = `s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits cT) ClassCast) s1`
hence s1_s2: "dom (locals (store s1)) \<subseteq> dom (locals (store s2))"
by simp
have "?NormalAssigned s2 A"
@@ -3663,7 +3664,7 @@
fix j have "abrupt s2 \<noteq> Some (Jump j)"
proof -
have eval: "prg Env\<turnstile> Norm s0 \<midarrow>Cast cT e-\<succ>v\<rightarrow> s2"
- by (simp only: G) (rule eval.Cast)
+ unfolding G by (rule eval.Cast Cast.hyps)+
from Cast.prems
obtain T' where "T=Inl T'"
by (elim wt_elim_cases) simp
@@ -3679,14 +3680,14 @@
ultimately show ?case by (intro conjI)
next
case (Inst s0 e v s1 b iT Env T A)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
from Inst.prems obtain
da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A"
by (elim da_elim_cases)
from Inst.prems obtain eT where
wt_e: "Env\<turnstile>e\<Colon>-eT"
by (elim wt_elim_cases)
- have "PROP ?Hyp (In1l e) (Norm s0) s1" .
+ note `PROP ?Hyp (In1l e) (Norm s0) s1`
with wt_e da_e G obtain
"?NormalAssigned s1 A" and
"?BreakAssigned (Norm s0) s1 A" and
@@ -3701,14 +3702,14 @@
thus ?case by simp
next
case (UnOp s0 e v s1 unop Env T A)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
from UnOp.prems obtain
da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A"
by (elim da_elim_cases)
from UnOp.prems obtain eT where
wt_e: "Env\<turnstile>e\<Colon>-eT"
by (elim wt_elim_cases)
- have "PROP ?Hyp (In1l e) (Norm s0) s1" .
+ note `PROP ?Hyp (In1l e) (Norm s0) s1`
with wt_e da_e G obtain
"?NormalAssigned s1 A" and
"?BreakAssigned (Norm s0) s1 A" and
@@ -3717,19 +3718,19 @@
thus ?case by (intro conjI)
next
case (BinOp s0 e1 v1 s1 binop e2 v2 s2 Env T A)
- have G: "prg Env = G".
+ note G = `prg Env = G`
from BinOp.hyps
have
- eval: "prg Env\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<rightarrow> s2"
+ eval: "prg Env\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<rightarrow> s2"
by (simp only: G) (rule eval.BinOp)
have s0_s1: "dom (locals (store ((Norm s0)::state)))
\<subseteq> dom (locals (store s1))"
- by (rule dom_locals_eval_mono_elim)
+ by (rule dom_locals_eval_mono_elim) (rule BinOp)
also have s1_s2: "dom (locals (store s1)) \<subseteq> dom (locals (store s2))"
- by (rule dom_locals_eval_mono_elim)
+ by (rule dom_locals_eval_mono_elim) (rule BinOp)
finally
have s0_s2: "dom (locals (store ((Norm s0)::state)))
- \<subseteq> dom (locals (store s2))" .
+ \<subseteq> dom (locals (store s2))" .
from BinOp.prems obtain e1T e2T
where wt_e1: "Env\<turnstile>e1\<Colon>-e1T"
and wt_e2: "Env\<turnstile>e2\<Colon>-e2T"
@@ -3740,7 +3741,7 @@
proof
assume normal_s2: "normal s2"
have normal_s1: "normal s1"
- by (rule eval_no_abrupt_lemma [rule_format])
+ by (rule eval_no_abrupt_lemma [rule_format]) (rule BinOp.hyps, rule normal_s2)
show "nrm A \<subseteq> dom (locals (store s2))"
proof (cases "binop=CondAnd")
case True
@@ -3832,7 +3833,7 @@
where da_e1: "Env\<turnstile> dom (locals (snd (Norm s0))) \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1"
and da_e2: "Env\<turnstile> nrm E1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A"
by (elim da_elim_cases) (simp_all add: notAndOr)
- have "PROP ?Hyp (In1l e1) (Norm s0) s1" .
+ note `PROP ?Hyp (In1l e1) (Norm s0) s1`
with wt_e1 da_e1 G normal_s1
obtain "?NormalAssigned s1 E1"
by simp
@@ -3883,20 +3884,21 @@
from Acc.prems
have "nrm A = dom (locals (store ((Norm s0)::state)))"
by (simp only: vn) (elim da_elim_cases,simp_all)
- moreover have "G\<turnstile>Norm s0 \<midarrow>v=\<succ>(w, upd)\<rightarrow> s1" .
- hence "s1=Norm s0"
+ moreover
+ from `G\<turnstile>Norm s0 \<midarrow>v=\<succ>(w, upd)\<rightarrow> s1`
+ have "s1=Norm s0"
by (simp only: vn) (elim eval_elim_cases,simp)
ultimately show ?thesis by simp
next
case False
- have G: "prg Env = G" .
+ note G = `prg Env = G`
from False Acc.prems
have da_v: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>v\<rangle>\<guillemotright> A"
by (elim da_elim_cases) simp_all
from Acc.prems obtain vT where
wt_v: "Env\<turnstile>v\<Colon>=vT"
by (elim wt_elim_cases)
- have "PROP ?Hyp (In2 v) (Norm s0) s1" .
+ note `PROP ?Hyp (In2 v) (Norm s0) s1`
with wt_v da_v G obtain
"?NormalAssigned s1 A" and
"?BreakAssigned (Norm s0) s1 A" and
@@ -3906,7 +3908,7 @@
qed
next
case (Ass s0 var w upd s1 e v s2 Env T A)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
from Ass.prems obtain varT eT where
wt_var: "Env\<turnstile>var\<Colon>=varT" and
wt_e: "Env\<turnstile>e\<Colon>-eT"
@@ -3920,9 +3922,9 @@
have normal_s2: "normal s2"
by (cases s2) (simp add: assign_def Let_def)
hence normal_s1: "normal s1"
- by - (rule eval_no_abrupt_lemma [rule_format])
- have hyp_var: "PROP ?Hyp (In2 var) (Norm s0) s1" .
- have hyp_e: "PROP ?Hyp (In1l e) s1 s2" .
+ by - (rule eval_no_abrupt_lemma [rule_format], rule Ass.hyps)
+ note hyp_var = `PROP ?Hyp (In2 var) (Norm s0) s1`
+ note hyp_e = `PROP ?Hyp (In1l e) s1 s2`
show "nrm A \<subseteq> dom (locals (store (assign upd v s2)))"
proof (cases "\<exists> vn. var = LVar vn")
case True
@@ -3937,9 +3939,9 @@
proof -
have "dom (locals (store ((Norm s0)::state)))
\<subseteq> dom (locals (store s1))"
- by (rule dom_locals_eval_mono_elim)
- with da_e show ?thesis
- by (rule da_weakenE)
+ by (rule dom_locals_eval_mono_elim) (rule Ass.hyps)
+ with da_e show thesis
+ by (rule da_weakenE) (rule that)
qed
from G eval_var vn
have eval_lvar: "G\<turnstile>Norm s0 \<midarrow>LVar vn=\<succ>(w, upd)\<rightarrow> s1"
@@ -4004,7 +4006,7 @@
fix j have "abrupt (assign upd v s2) \<noteq> Some (Jump j)"
proof -
have eval: "prg Env\<turnstile>Norm s0 \<midarrow>var:=e-\<succ>v\<rightarrow> (assign upd v s2)"
- by (simp only: G) (rule eval.Ass)
+ by (simp only: G) (rule eval.Ass Ass.hyps)+
from Ass.prems
obtain T' where "T=Inl T'"
by (elim wt_elim_cases) simp
@@ -4020,7 +4022,7 @@
ultimately show ?case by (intro conjI)
next
case (Cond s0 e0 b s1 e1 e2 v s2 Env T A)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
have "?NormalAssigned s2 A"
proof
assume normal_s2: "normal s2"
@@ -4033,7 +4035,7 @@
assigns_if False (e0 ? e1 : e2))"
by (elim da_elim_cases) simp_all
have eval: "prg Env\<turnstile>Norm s0 \<midarrow>(e0 ? e1 : e2)-\<succ>v\<rightarrow> s2"
- by (simp only: G) (rule eval.Cond)
+ unfolding G by (rule eval.Cond Cond.hyps)+
from eval
have "dom (locals (store ((Norm s0)::state)))\<subseteq>dom (locals (store s2))"
by (rule dom_locals_eval_mono_elim)
@@ -4075,10 +4077,11 @@
by (elim wt_elim_cases)
have s0_s1: "dom (locals (store ((Norm s0)::state)))
\<subseteq> dom (locals (store s1))"
- by (rule dom_locals_eval_mono_elim)
- have eval_e0: "prg Env\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1" by (simp only: G)
+ by (rule dom_locals_eval_mono_elim) (rule Cond.hyps)
+ have eval_e0: "prg Env\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1"
+ unfolding G by (rule Cond.hyps)
have normal_s1: "normal s1"
- by (rule eval_no_abrupt_lemma [rule_format])
+ by (rule eval_no_abrupt_lemma [rule_format]) (rule Cond.hyps, rule normal_s2)
show ?thesis
proof (cases "the_Bool b")
case True
@@ -4126,7 +4129,7 @@
fix j have "abrupt s2 \<noteq> Some (Jump j)"
proof -
have eval: "prg Env\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<rightarrow> s2"
- by (simp only: G) (rule eval.Cond)
+ unfolding G by (rule eval.Cond Cond.hyps)+
from Cond.prems
obtain T' where "T=Inl T'"
by (elim wt_elim_cases) simp
@@ -4142,7 +4145,7 @@
next
case (Call s0 e a s1 args vs s2 D mode statT mn pTs s3 s3' accC v s4
Env T A)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
have "?NormalAssigned (restore_lvars s2 s4) A"
proof
assume normal_restore_lvars: "normal (restore_lvars s2 s4)"
@@ -4156,23 +4159,23 @@
wt_e: "Env\<turnstile>e\<Colon>-eT" and
wt_args: "Env\<turnstile>args\<Colon>\<doteq>argsT"
by (elim wt_elim_cases)
- have s3: "s3 = init_lvars G D \<lparr>name = mn, parTs = pTs\<rparr> mode a vs s2" .
- have s3': "s3' = check_method_access G accC statT mode
- \<lparr>name=mn,parTs=pTs\<rparr> a s3" .
+ note s3 = `s3 = init_lvars G D \<lparr>name = mn, parTs = pTs\<rparr> mode a vs s2`
+ note s3' = `s3' = check_method_access G accC statT mode
+ \<lparr>name=mn,parTs=pTs\<rparr> a s3`
have normal_s2: "normal s2"
proof -
from normal_restore_lvars have "normal s4"
by simp
then have "normal s3'"
- by - (rule eval_no_abrupt_lemma [rule_format])
+ by - (rule eval_no_abrupt_lemma [rule_format], rule Call.hyps)
with s3' have "normal s3"
by (cases s3) (simp add: check_method_access_def Let_def)
with s3 show "normal s2"
by (cases s2) (simp add: init_lvars_def Let_def)
qed
then have normal_s1: "normal s1"
- by - (rule eval_no_abrupt_lemma [rule_format])
- have "PROP ?Hyp (In1l e) (Norm s0) s1" .
+ by - (rule eval_no_abrupt_lemma [rule_format], rule Call.hyps)
+ note `PROP ?Hyp (In1l e) (Norm s0) s1`
with da_e wt_e G normal_s1
have "nrm E \<subseteq> dom (locals (store s1))"
by simp
@@ -4180,7 +4183,7 @@
da_args': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>args\<rangle>\<guillemotright> A'" and
nrm_A_A': "nrm A \<subseteq> nrm A'"
by (rule da_weakenE) iprover
- have "PROP ?Hyp (In3 args) s1 s2" .
+ note `PROP ?Hyp (In3 args) s1 s2`
with da_args' wt_args G normal_s2
have "nrm A' \<subseteq> dom (locals (store s2))"
by simp
@@ -4197,7 +4200,7 @@
proof -
have eval: "prg Env\<turnstile>Norm s0 \<midarrow>({accC,statT,mode}e\<cdot>mn( {pTs}args))-\<succ>v
\<rightarrow> (restore_lvars s2 s4)"
- by (simp only: G) (rule eval.Call)
+ unfolding G by (rule eval.Call Call)+
from Call.prems
obtain T' where "T=Inl T'"
by (elim wt_elim_cases) simp
@@ -4214,7 +4217,7 @@
ultimately show ?case by (intro conjI)
next
case (Methd s0 D sig v s1 Env T A)
- have G: "prg Env = G".
+ note G = `prg Env = G`
from Methd.prems obtain m where
m: "methd (prg Env) D sig = Some m" and
da_body: "Env\<turnstile>(dom (locals (store ((Norm s0)::state))))
@@ -4224,7 +4227,7 @@
isCls: "is_class (prg Env) D" and
wt_body: "Env \<turnstile>In1l (Body (declclass m) (stmt (mbody (mthd m))))\<Colon>T"
by - (erule wt_elim_cases,simp)
- have "PROP ?Hyp (In1l (body G D sig)) (Norm s0) s1" .
+ note `PROP ?Hyp (In1l (body G D sig)) (Norm s0) s1`
moreover
from wt_body have "Env\<turnstile>In1l (body G D sig)\<Colon>T"
using isCls m G by (simp add: body_def2)
@@ -4236,13 +4239,13 @@
using G by simp
next
case (Body s0 D s1 c s2 s3 Env T A)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
from Body.prems
have nrm_A: "nrm A = dom (locals (store ((Norm s0)::state)))"
by (elim da_elim_cases) simp
have eval: "prg Env\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)
\<rightarrow>abupd (absorb Ret) s3"
- by (simp only: G) (rule eval.Body)
+ unfolding G by (rule eval.Body Body.hyps)+
hence "nrm A \<subseteq> dom (locals (store (abupd (absorb Ret) s3)))"
by (simp only: nrm_A) (rule dom_locals_eval_mono_elim)
hence "?NormalAssigned (abupd (absorb Ret) s3) A"
@@ -4262,14 +4265,14 @@
thus ?case by simp
next
case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC Env T A)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
have "?NormalAssigned s3 A"
proof
assume normal_s3: "normal s3"
show "nrm A \<subseteq> dom (locals (store s3))"
proof -
- have fvar: "(v, s2') = fvar statDeclC stat fn a s2" and
- s3: "s3 = check_field_access G accC statDeclC fn stat a s2'" .
+ note fvar = `(v, s2') = fvar statDeclC stat fn a s2` and
+ s3 = `s3 = check_field_access G accC statDeclC fn stat a s2'`
from FVar.prems
have da_e: "Env\<turnstile> (dom (locals (store ((Norm s0)::state))))\<guillemotright>\<langle>e\<rangle>\<guillemotright> A"
by (elim da_elim_cases)
@@ -4278,7 +4281,7 @@
by (elim wt_elim_cases)
have "(dom (locals (store ((Norm s0)::state))))
\<subseteq> dom (locals (store s1))"
- by (rule dom_locals_eval_mono_elim)
+ by (rule dom_locals_eval_mono_elim) (rule FVar.hyps)
with da_e obtain A' where
da_e': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A'" and
nrm_A_A': "nrm A \<subseteq> nrm A'"
@@ -4292,7 +4295,7 @@
show "normal s2"
by (cases s2) (simp add: fvar_def2)
qed
- have "PROP ?Hyp (In1l e) s1 s2" .
+ note `PROP ?Hyp (In1l e) s1 s2`
with da_e' wt_e G normal_s2
have "nrm A' \<subseteq> dom (locals (store s2))"
by simp
@@ -4318,7 +4321,7 @@
obtain w upd where v: "(w,upd)=v"
by (cases v) auto
have eval: "prg Env\<turnstile>Norm s0\<midarrow>({accC,statDeclC,stat}e..fn)=\<succ>(w,upd)\<rightarrow>s3"
- by (simp only: G v) (rule eval.FVar)
+ by (simp only: G v) (rule eval.FVar FVar.hyps)+
from FVar.prems
obtain T' where "T=Inl T'"
by (elim wt_elim_cases) simp
@@ -4334,13 +4337,13 @@
ultimately show ?case by (intro conjI)
next
case (AVar s0 e1 a s1 e2 i s2 v s2' Env T A)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
have "?NormalAssigned s2' A"
proof
assume normal_s2': "normal s2'"
show "nrm A \<subseteq> dom (locals (store s2'))"
proof -
- have avar: "(v, s2') = avar G i a s2" .
+ note avar = `(v, s2') = avar G i a s2`
from AVar.prems obtain E1 where
da_e1: "Env\<turnstile> (dom (locals (store ((Norm s0)::state))))\<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1" and
da_e2: "Env\<turnstile> nrm E1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A"
@@ -4353,15 +4356,15 @@
have normal_s2: "normal s2"
by (cases s2) (simp add: avar_def2)
hence "normal s1"
- by - (rule eval_no_abrupt_lemma [rule_format])
- moreover have "PROP ?Hyp (In1l e1) (Norm s0) s1" .
+ by - (rule eval_no_abrupt_lemma [rule_format], rule AVar, rule normal_s2)
+ moreover note `PROP ?Hyp (In1l e1) (Norm s0) s1`
ultimately have "nrm E1 \<subseteq> dom (locals (store s1))"
using da_e1 wt_e1 G by simp
with da_e2 obtain A' where
da_e2': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A'" and
nrm_A_A': "nrm A \<subseteq> nrm A'"
by (rule da_weakenE) iprover
- have "PROP ?Hyp (In1l e2) s1 s2" .
+ note `PROP ?Hyp (In1l e2) s1 s2`
with da_e2' wt_e2 G normal_s2
have "nrm A' \<subseteq> dom (locals (store s2))"
by simp
@@ -4384,7 +4387,7 @@
obtain w upd where v: "(w,upd)=v"
by (cases v) auto
have eval: "prg Env\<turnstile>Norm s0\<midarrow>(e1.[e2])=\<succ>(w,upd)\<rightarrow>s2'"
- by (simp only: G v) (rule eval.AVar)
+ unfolding G v by (rule eval.AVar AVar.hyps)+
from AVar.prems
obtain T' where "T=Inl T'"
by (elim wt_elim_cases) simp
@@ -4406,7 +4409,7 @@
thus ?case by simp
next
case (Cons s0 e v s1 es vs s2 Env T A)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
have "?NormalAssigned s2 A"
proof
assume normal_s2: "normal s2"
@@ -4421,15 +4424,15 @@
wt_es: "Env\<turnstile>es\<Colon>\<doteq>esT"
by (elim wt_elim_cases)
have "normal s1"
- by - (rule eval_no_abrupt_lemma [rule_format])
- moreover have "PROP ?Hyp (In1l e) (Norm s0) s1" .
+ by - (rule eval_no_abrupt_lemma [rule_format], rule Cons.hyps, rule normal_s2)
+ moreover note `PROP ?Hyp (In1l e) (Norm s0) s1`
ultimately have "nrm E \<subseteq> dom (locals (store s1))"
using da_e wt_e G by simp
with da_es obtain A' where
da_es': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>es\<rangle>\<guillemotright> A'" and
nrm_A_A': "nrm A \<subseteq> nrm A'"
by (rule da_weakenE) iprover
- have "PROP ?Hyp (In3 es) s1 s2" .
+ note `PROP ?Hyp (In3 es) s1 s2`
with da_es' wt_es G normal_s2
have "nrm A' \<subseteq> dom (locals (store s2))"
by simp
@@ -4442,7 +4445,7 @@
fix j have "abrupt s2 \<noteq> Some (Jump j)"
proof -
have eval: "prg Env\<turnstile>Norm s0\<midarrow>(e # es)\<doteq>\<succ>v#vs\<rightarrow>s2"
- by (simp only: G) (rule eval.Cons)
+ unfolding G by (rule eval.Cons Cons.hyps)+
from Cons.prems
obtain T' where "T=Inr T'"
by (elim wt_elim_cases) simp
--- a/src/HOL/Bali/Evaln.thy Wed Jun 13 00:01:38 2007 +0200
+++ b/src/HOL/Bali/Evaln.thy Wed Jun 13 00:01:41 2007 +0200
@@ -410,7 +410,7 @@
using evaln
proof (induct)
case (Loop s0 e n b s1 c s2 l s3)
- have "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1".
+ note `G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1`
moreover
have "if the_Bool b
then (G\<turnstile>s1 \<midarrow>c\<rightarrow> s2) \<and>
@@ -420,16 +420,16 @@
ultimately show ?case by (rule eval.Loop)
next
case (Try s0 c1 n s1 s2 C vn c2 s3)
- have "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1".
+ note `G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1`
moreover
- have "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2".
+ note `G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2`
moreover
have "if G,s2\<turnstile>catch C then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<rightarrow> s3 else s3 = s2"
using Try.hyps by simp
ultimately show ?case by (rule eval.Try)
next
case (Init C c s0 s3 n s1 s2)
- have "the (class G C) = c".
+ note `the (class G C) = c`
moreover
have "if inited C (globs s0)
then s3 = Norm s0
@@ -600,7 +600,7 @@
"G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> s1"
by (iprover)
moreover
- have sxalloc: "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" .
+ note sxalloc = `G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2`
moreover
from Try.hyps obtain n2 where
"if G,s2\<turnstile>catch catchC then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<midarrow>n2\<rightarrow> s3 else s3 = s2"
@@ -616,9 +616,9 @@
"G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2"
by iprover
moreover
- have s3: "s3 = (if \<exists>err. x1 = Some (Error err)
- then (x1, s1)
- else abupd (abrupt_if (x1 \<noteq> None) x1) s2)" .
+ note s3 = `s3 = (if \<exists>err. x1 = Some (Error err)
+ then (x1, s1)
+ else abupd (abrupt_if (x1 \<noteq> None) x1) s2)`
ultimately
have
"G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<midarrow>max n1 n2\<rightarrow> s3"
@@ -626,7 +626,7 @@
then show ?case ..
next
case (Init C c s0 s3 s1 s2)
- have cls: "the (class G C) = c" .
+ note cls = `the (class G C) = c`
moreover from Init.hyps obtain n where
"if inited C (globs s0) then s3 = Norm s0
else (G\<turnstile>Norm (init_class_obj G C s0)
@@ -653,7 +653,7 @@
"G\<turnstile>s1 \<midarrow>e-\<succ>i\<midarrow>n2\<rightarrow> s2"
by (iprover)
moreover
- have "G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3" .
+ note `G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3`
ultimately
have "G\<turnstile>Norm s0 \<midarrow>New T[e]-\<succ>Addr a\<midarrow>max n1 n2\<rightarrow> s3"
by (blast intro: evaln.NewA dest: evaln_max2)
@@ -664,7 +664,7 @@
"G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
by (iprover)
moreover
- have "s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits castT) ClassCast) s1" .
+ note `s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits castT) ClassCast) s1`
ultimately
have "G\<turnstile>Norm s0 \<midarrow>Cast castT e-\<succ>v\<midarrow>n\<rightarrow> s2"
by (rule evaln.Cast)
@@ -675,7 +675,7 @@
"G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
by (iprover)
moreover
- have "b = (v \<noteq> Null \<and> G,snd s1\<turnstile>v fits RefT T)" .
+ note `b = (v \<noteq> Null \<and> G,snd s1\<turnstile>v fits RefT T)`
ultimately
have "G\<turnstile>Norm s0 \<midarrow>e InstOf T-\<succ>Bool b\<midarrow>n\<rightarrow> s1"
by (rule evaln.Inst)
@@ -745,12 +745,12 @@
"G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<midarrow>n2\<rightarrow> s2"
by iprover
moreover
- have "invDeclC = invocation_declclass G mode (store s2) a' statT
- \<lparr>name=mn,parTs=pTs'\<rparr>" .
+ note `invDeclC = invocation_declclass G mode (store s2) a' statT
+ \<lparr>name=mn,parTs=pTs'\<rparr>`
moreover
- have "s3 = init_lvars G invDeclC \<lparr>name=mn,parTs=pTs'\<rparr> mode a' vs s2" .
+ note `s3 = init_lvars G invDeclC \<lparr>name=mn,parTs=pTs'\<rparr> mode a' vs s2`
moreover
- have "s3'=check_method_access G accC' statT mode \<lparr>name=mn,parTs=pTs'\<rparr> a' s3".
+ note `s3'=check_method_access G accC' statT mode \<lparr>name=mn,parTs=pTs'\<rparr> a' s3`
moreover
from Call.hyps
obtain m where
@@ -776,10 +776,10 @@
evaln_c: "G\<turnstile>s1 \<midarrow>c\<midarrow>n2\<rightarrow> s2"
by (iprover)
moreover
- have "s3 = (if \<exists>l. fst s2 = Some (Jump (Break l)) \<or>
+ note `s3 = (if \<exists>l. fst s2 = Some (Jump (Break l)) \<or>
fst s2 = Some (Jump (Cont l))
- then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2
- else s2)".
+ then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2
+ else s2)`
ultimately
have
"G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)\<midarrow>max n1 n2
@@ -799,8 +799,8 @@
"G\<turnstile>s1 \<midarrow>e-\<succ>a\<midarrow>n2\<rightarrow> s2"
by iprover
moreover
- have "s3 = check_field_access G accC statDeclC fn stat a s2'"
- "(v, s2') = fvar statDeclC stat fn a s2" .
+ note `s3 = check_field_access G accC statDeclC fn stat a s2'`
+ and `(v, s2') = fvar statDeclC stat fn a s2`
ultimately
have "G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<midarrow>max n1 n2\<rightarrow> s3"
by (iprover intro: evaln.FVar dest: evaln_max2)
@@ -812,7 +812,7 @@
"G\<turnstile>s1 \<midarrow>e2-\<succ>i\<midarrow>n2\<rightarrow> s2"
by iprover
moreover
- have "(v, s2') = avar G i a s2" .
+ note `(v, s2') = avar G i a s2`
ultimately
have "G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<midarrow>max n1 n2\<rightarrow> s2'"
by (blast intro!: evaln.AVar dest: evaln_max2)
--- a/src/HOL/Bali/TypeSafe.thy Wed Jun 13 00:01:38 2007 +0200
+++ b/src/HOL/Bali/TypeSafe.thy Wed Jun 13 00:01:41 2007 +0200
@@ -724,7 +724,7 @@
proof -
assume error_free: "error_free state"
obtain a s where "state=(a,s)"
- by (cases state) simp
+ by (cases state)
with error_free
show ?thesis
by (cases a) auto
@@ -792,7 +792,7 @@
proof -
assume error_free: "error_free state"
obtain a s where "state=(a,s)"
- by (cases state) simp
+ by (cases state)
with error_free
show ?thesis
by (cases a) auto
@@ -991,7 +991,7 @@
moreover
from f subclseq
have "G\<turnstile>Field fn f in dynC dyn_accessible_from accC"
- by (auto intro!: static_to_dynamic_accessible_from
+ by (auto intro!: static_to_dynamic_accessible_from wf
dest: accfield_accessibleD)
ultimately show ?thesis
by blast
@@ -1182,8 +1182,8 @@
case Nil thus ?case by simp
next
case (Cons p ps tab qs)
- have "length (p#ps) = length qs" .
- then obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
+ from `length (p#ps) = length qs`
+ obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
by (cases qs) auto
from eq_length have "(tab(p\<mapsto>q))(ps[\<mapsto>]qs'@zs)=(tab(p\<mapsto>q))(ps[\<mapsto>]qs')"
by (rule Cons.hyps)
@@ -1198,8 +1198,8 @@
case Nil thus ?case by simp
next
case (Cons p ps tab qs x y)
- have "length (p#ps) = length qs" .
- then obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
+ from `length (p#ps) = length qs`
+ obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
by (cases qs) auto
from eq_length
have "(tab(p\<mapsto>q))(ps[\<mapsto>]qs')(x\<mapsto>y) = (tab(p\<mapsto>q))(ps@[x][\<mapsto>]qs'@[y])"
@@ -1228,7 +1228,8 @@
show ?case
proof (cases ys)
case Nil
- thus ?thesis by simp
+ with Hyps
+ show ?thesis by simp
next
case (Cons y ys')
have "(tab(x\<mapsto>y)(xs[\<mapsto>]ys')) z = (tab'(x\<mapsto>y)(xs[\<mapsto>]ys')) z"
@@ -1290,14 +1291,14 @@
case Nil thus ?case by simp
next
case (Cons x xs tab ys z)
- have z: "tab vn = Some z" .
+ note z = `tab vn = Some z`
show ?case
proof (cases ys)
case Nil
with z show ?thesis by simp
next
case (Cons y ys')
- have ys: "ys = y#ys'".
+ note ys = `ys = y#ys'`
from z obtain z' where "(tab(x\<mapsto>y)) vn = Some z'"
by (rule map_upd_Some_expand [of tab,elim_format]) blast
hence "\<exists>z. ((tab(x\<mapsto>y))(xs[\<mapsto>]ys')) vn = Some z"
@@ -1332,14 +1333,14 @@
case Nil thus ?case by simp
next
case (Cons x xs tab tab' ys z)
- have some: "(tab(x # xs[\<mapsto>]ys)) vn = Some z" .
- have tab_not_z: "tab vn \<noteq> Some z".
+ note some = `(tab(x # xs[\<mapsto>]ys)) vn = Some z`
+ note tab_not_z = `tab vn \<noteq> Some z`
show ?case
- proof (cases "ys")
+ proof (cases ys)
case Nil with some tab_not_z show ?thesis by simp
next
case (Cons y tl)
- have ys: "ys = y#tl".
+ note ys = `ys = y#tl`
show ?thesis
proof (cases "(tab(x\<mapsto>y)) vn \<noteq> Some z")
case True
@@ -1424,15 +1425,15 @@
case Nil thus ?case by simp
next
case (Cons x xs tab tab' ys)
- have tab_vn: "(tab(x # xs[\<mapsto>]ys)) vn = Some el".
- have tab'_vn: "(tab'(x # xs[\<mapsto>]ys)) vn = None".
+ note tab_vn = `(tab(x # xs[\<mapsto>]ys)) vn = Some el`
+ note tab'_vn = `(tab'(x # xs[\<mapsto>]ys)) vn = None`
show ?case
proof (cases ys)
case Nil
with tab_vn show ?thesis by simp
next
case (Cons y tl)
- have ys: "ys=y#tl".
+ note ys = `ys=y#tl`
with tab_vn tab'_vn
have "(tab(x\<mapsto>y)) vn = Some el"
by - (rule Cons.hyps,auto)
@@ -1509,7 +1510,7 @@
next
case (Cons x xs tab ys)
note Hyp = Cons.hyps
- have len: "length (x#xs)=length ys".
+ note len = `length (x#xs)=length ys`
show ?case
proof (cases ys)
case Nil with len show ?thesis by simp
@@ -1740,30 +1741,30 @@
?ErrorFree s0 s1")
proof (induct)
case (Abrupt xc s t L accC T A)
- have "(Some xc, s)\<Colon>\<preceq>(G,L)" .
- then show "(Some xc, s)\<Colon>\<preceq>(G,L) \<and>
+ from `(Some xc, s)\<Colon>\<preceq>(G,L)`
+ show "(Some xc, s)\<Colon>\<preceq>(G,L) \<and>
(normal (Some xc, s)
\<longrightarrow> G,L,store (Some xc,s)\<turnstile>t\<succ>arbitrary3 t\<Colon>\<preceq>T) \<and>
(error_free (Some xc, s) = error_free (Some xc, s))"
- by (simp)
+ by simp
next
case (Skip s L accC T A)
- have "Norm s\<Colon>\<preceq>(G, L)" and
- "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r Skip\<Colon>T" .
- then show "Norm s\<Colon>\<preceq>(G, L) \<and>
+ from `Norm s\<Colon>\<preceq>(G, L)` and
+ `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r Skip\<Colon>T`
+ show "Norm s\<Colon>\<preceq>(G, L) \<and>
(normal (Norm s) \<longrightarrow> G,L,store (Norm s)\<turnstile>In1r Skip\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
(error_free (Norm s) = error_free (Norm s))"
- by (simp)
+ by simp
next
case (Expr s0 e v s1 L accC T A)
- have "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1" .
- have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)" .
- have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
+ note `G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1`
+ note hyp = `PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)`
+ note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
moreover
- have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (Expr e)\<Colon>T" .
+ note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (Expr e)\<Colon>T`
then obtain eT
where "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l e\<Colon>eT"
- by (rule wt_elim_cases) (blast)
+ by (rule wt_elim_cases) blast
moreover
from Expr.prems obtain E where
"\<lparr>prg=G,cls=accC, lcl=L\<rparr>\<turnstile>dom (locals (store ((Norm s0)::state)))\<guillemotright>In1l e\<guillemotright>E"
@@ -1778,12 +1779,12 @@
by (simp)
next
case (Lab s0 c s1 l L accC T A)
- have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1r c) \<diamondsuit>" .
- have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
+ note hyp = `PROP ?TypeSafe (Norm s0) s1 (In1r c) \<diamondsuit>`
+ note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
moreover
- have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (l\<bullet> c)\<Colon>T" .
+ note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (l\<bullet> c)\<Colon>T`
then have "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c\<Colon>\<surd>"
- by (rule wt_elim_cases) (blast)
+ by (rule wt_elim_cases) blast
moreover from Lab.prems obtain C where
"\<lparr>prg=G,cls=accC, lcl=L\<rparr>\<turnstile>dom (locals (store ((Norm s0)::state)))\<guillemotright>In1r c\<guillemotright>C"
by (elim da_elim_cases) simp
@@ -1801,15 +1802,15 @@
by (simp)
next
case (Comp s0 c1 s1 c2 s2 L accC T A)
- have eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1" .
- have eval_c2: "G\<turnstile>s1 \<midarrow>c2\<rightarrow> s2" .
- have hyp_c1: "PROP ?TypeSafe (Norm s0) s1 (In1r c1) \<diamondsuit>" .
- have hyp_c2: "PROP ?TypeSafe s1 s2 (In1r c2) \<diamondsuit>" .
- have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
- have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (c1;; c2)\<Colon>T" .
+ note eval_c1 = `G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1`
+ note eval_c2 = `G\<turnstile>s1 \<midarrow>c2\<rightarrow> s2`
+ note hyp_c1 = `PROP ?TypeSafe (Norm s0) s1 (In1r c1) \<diamondsuit>`
+ note hyp_c2 = `PROP ?TypeSafe s1 s2 (In1r c2) \<diamondsuit>`
+ note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
+ note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (c1;; c2)\<Colon>T`
then obtain wt_c1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
wt_c2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c2\<Colon>\<surd>"
- by (rule wt_elim_cases) (blast)
+ by (rule wt_elim_cases) blast
from Comp.prems
obtain C1 C2
where da_c1: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>
@@ -1836,8 +1837,8 @@
from eval_c1 wt_c1 da_c1 wf True
have "nrm C1 \<subseteq> dom (locals (store s1))"
by (cases rule: da_good_approxE') iprover
- with da_c2 show ?thesis
- by (rule da_weakenE)
+ with da_c2 show thesis
+ by (rule da_weakenE) (rule that)
qed
with conf_s1 wt_c2
obtain "s2\<Colon>\<preceq>(G, L)" and "error_free s2"
@@ -1847,13 +1848,13 @@
qed
next
case (If s0 e b s1 c1 c2 s2 L accC T A)
- have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" .
- have eval_then_else: "G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2" .
- have hyp_e: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 b)" .
- have hyp_then_else:
- "PROP ?TypeSafe s1 s2 (In1r (if the_Bool b then c1 else c2)) \<diamondsuit>" .
- have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
- have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (If(e) c1 Else c2)\<Colon>T" .
+ note eval_e = `G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1`
+ note eval_then_else = `G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2`
+ note hyp_e = `PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 b)`
+ note hyp_then_else =
+ `PROP ?TypeSafe s1 s2 (In1r (if the_Bool b then c1 else c2)) \<diamondsuit>`
+ note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
+ note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (If(e) c1 Else c2)\<Colon>T`
then obtain
wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean" and
wt_then_else: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(if the_Bool b then c1 else c2)\<Colon>\<surd>"
@@ -1902,8 +1903,8 @@
have "dom (locals (store ((Norm s0)::state)))
\<union> assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))"
by (rule Un_least)
- with da_then_else show ?thesis
- by (rule da_weakenE)
+ with da_then_else show thesis
+ by (rule da_weakenE) (rule that)
qed
with conf_s1 wt_then_else
obtain "s2\<Colon>\<preceq>(G, L)" and "error_free s2"
@@ -1922,15 +1923,15 @@
*}
next
case (Loop s0 e b s1 c s2 l s3 L accC T A)
- have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" .
- have hyp_e: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 b)" .
- have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
- have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (l\<bullet> While(e) c)\<Colon>T" .
+ note eval_e = `G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1`
+ note hyp_e = `PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 b)`
+ note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
+ note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (l\<bullet> While(e) c)\<Colon>T`
then obtain wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean" and
wt_c: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c\<Colon>\<surd>"
- by (rule wt_elim_cases) (blast)
- have da:"\<lparr>prg=G, cls=accC, lcl=L\<rparr>
- \<turnstile> dom (locals(store ((Norm s0)::state))) \<guillemotright>In1r (l\<bullet> While(e) c)\<guillemotright> A".
+ by (rule wt_elim_cases) blast
+ note da = `\<lparr>prg=G, cls=accC, lcl=L\<rparr>
+ \<turnstile> dom (locals(store ((Norm s0)::state))) \<guillemotright>In1r (l\<bullet> While(e) c)\<guillemotright> A`
then
obtain E C where
da_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>
@@ -1939,7 +1940,7 @@
\<turnstile> (dom (locals (store ((Norm s0)::state)))
\<union> assigns_if True e) \<guillemotright>In1r c\<guillemotright> C"
by (rule da_elim_cases) simp
- from conf_s0 wt_e da_e
+ from conf_s0 wt_e da_e
obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
by (rule hyp_e [elim_format]) simp
show "s3\<Colon>\<preceq>(G, L) \<and>
@@ -1978,8 +1979,8 @@
have "dom (locals (store ((Norm s0)::state)))
\<union> assigns_if True e \<subseteq> dom (locals (store s1))"
by (rule Un_least)
- with da_c show ?thesis
- by (rule da_weakenE)
+ with da_c show thesis
+ by (rule da_weakenE) (rule that)
qed
with conf_s1 wt_c
obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
@@ -2004,8 +2005,8 @@
by simp
finally
have "dom (locals (store ((Norm s0)::state))) \<subseteq> \<dots>" .
- with da show ?thesis
- by (rule da_weakenE)
+ with da show thesis
+ by (rule da_weakenE) (rule that)
qed
ultimately obtain "s3\<Colon>\<preceq>(G, L)" and "error_free s3"
by (rule hyp_w [elim_format]) (simp add: error_free_ab_s2)
@@ -2053,7 +2054,7 @@
qed
next
case (Jmp s j L accC T A)
- have "Norm s\<Colon>\<preceq>(G, L)" .
+ note `Norm s\<Colon>\<preceq>(G, L)`
moreover
from Jmp.prems
have "j=Ret \<longrightarrow> Result \<in> dom (locals (store ((Norm s)::state)))"
@@ -2067,10 +2068,10 @@
by simp
next
case (Throw s0 e a s1 L accC T A)
- have "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<rightarrow> s1" .
- have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 a)" .
- have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
- have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (Throw e)\<Colon>T" .
+ note `G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<rightarrow> s1`
+ note hyp = `PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 a)`
+ note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
+ note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (Throw e)\<Colon>T`
then obtain tn
where wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-Class tn" and
throwable: "G\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable"
@@ -2095,11 +2096,11 @@
by simp
next
case (Try s0 c1 s1 s2 catchC vn c2 s3 L accC T A)
- have eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1" .
- have sx_alloc: "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" .
- have hyp_c1: "PROP ?TypeSafe (Norm s0) s1 (In1r c1) \<diamondsuit>" .
- have conf_s0:"Norm s0\<Colon>\<preceq>(G, L)" .
- have wt:"\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>In1r (Try c1 Catch(catchC vn) c2)\<Colon>T" .
+ note eval_c1 = `G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1`
+ note sx_alloc = `G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2`
+ note hyp_c1 = `PROP ?TypeSafe (Norm s0) s1 (In1r c1) \<diamondsuit>`
+ note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
+ note wt = `\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>In1r (Try c1 Catch(catchC vn) c2)\<Colon>T`
then obtain
wt_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
wt_c2: "\<lparr>prg=G,cls=accC,lcl=L(VName vn\<mapsto>Class catchC)\<rparr>\<turnstile>c2\<Colon>\<surd>" and
@@ -2177,8 +2178,8 @@
have "(dom (locals (store ((Norm s0)::state))) \<union> {VName vn})
\<subseteq> dom (locals (store (new_xcpt_var vn s2)))"
proof -
- have "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1" .
- hence "dom (locals (store ((Norm s0)::state)))
+ from `G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1`
+ have "dom (locals (store ((Norm s0)::state)))
\<subseteq> dom (locals (store s1))"
by (rule dom_locals_eval_mono_elim)
also
@@ -2194,8 +2195,8 @@
ultimately show ?thesis
by (rule Un_least)
qed
- with da_c2 show ?thesis
- by (rule da_weakenE)
+ with da_c2 show thesis
+ by (rule da_weakenE) (rule that)
qed
ultimately
obtain conf_s3: "s3\<Colon>\<preceq>(G, L(VName vn\<mapsto>Class catchC))" and
@@ -2212,20 +2213,20 @@
qed
next
case (Fin s0 c1 x1 s1 c2 s2 s3 L accC T A)
- have eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1, s1)" .
- have eval_c2: "G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2" .
- have s3: "s3= (if \<exists>err. x1 = Some (Error err)
+ note eval_c1 = `G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1, s1)`
+ note eval_c2 = `G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2`
+ note s3 = `s3 = (if \<exists>err. x1 = Some (Error err)
then (x1, s1)
- else abupd (abrupt_if (x1 \<noteq> None) x1) s2)" .
- have hyp_c1: "PROP ?TypeSafe (Norm s0) (x1,s1) (In1r c1) \<diamondsuit>" .
- have hyp_c2: "PROP ?TypeSafe (Norm s1) s2 (In1r c2) \<diamondsuit>" .
- have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
- have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (c1 Finally c2)\<Colon>T" .
+ else abupd (abrupt_if (x1 \<noteq> None) x1) s2)`
+ note hyp_c1 = `PROP ?TypeSafe (Norm s0) (x1,s1) (In1r c1) \<diamondsuit>`
+ note hyp_c2 = `PROP ?TypeSafe (Norm s1) s2 (In1r c2) \<diamondsuit>`
+ note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
+ note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (c1 Finally c2)\<Colon>T`
then obtain
wt_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
wt_c2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c2\<Colon>\<surd>"
by (rule wt_elim_cases) blast
- from Fin.prems obtain C1 C2 where
+ from Fin.prems obtain C1 C2 where
da_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1r c1\<guillemotright> C1" and
da_c2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
@@ -2248,8 +2249,8 @@
hence "dom (locals (store ((Norm s0)::state)))
\<subseteq> dom (locals (store ((Norm s1)::state)))"
by simp
- with da_c2 show ?thesis
- by (rule da_weakenE)
+ with da_c2 show thesis
+ by (rule da_weakenE) (rule that)
qed
ultimately
obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
@@ -2261,7 +2262,8 @@
(normal s3 \<longrightarrow> G,L,store s3 \<turnstile>In1r (c1 Finally c2)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
(error_free (Norm s0) = error_free s3)"
proof (cases x1)
- case None with conf_s2 s3' wt show ?thesis by auto
+ case None with conf_s2 s3' wt error_free_s2
+ show ?thesis by auto
next
case (Some x)
from eval_c2 have
@@ -2281,12 +2283,12 @@
qed
next
case (Init C c s0 s3 s1 s2 L accC T A)
- have cls: "the (class G C) = c" .
- have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
- have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (Init C)\<Colon>T" .
+ note cls = `the (class G C) = c`
+ note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
+ note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (Init C)\<Colon>T`
with cls
have cls_C: "class G C = Some c"
- by - (erule wt_elim_cases,auto)
+ by - (erule wt_elim_cases, auto)
show "s3\<Colon>\<preceq>(G, L) \<and> (normal s3 \<longrightarrow> G,L,store s3\<turnstile>In1r (Init C)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
(error_free (Norm s0) = error_free s3)"
proof (cases "inited C (globs s0)")
@@ -2387,12 +2389,12 @@
qed
next
case (NewC s0 C s1 a s2 L accC T A)
- have "G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s1" .
- have halloc: "G\<turnstile>s1 \<midarrow>halloc CInst C\<succ>a\<rightarrow> s2" .
- have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1r (Init C)) \<diamondsuit>" .
- have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
+ note `G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s1`
+ note halloc = `G\<turnstile>s1 \<midarrow>halloc CInst C\<succ>a\<rightarrow> s2`
+ note hyp = `PROP ?TypeSafe (Norm s0) s1 (In1r (Init C)) \<diamondsuit>`
+ note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
moreover
- have wt: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>In1l (NewC C)\<Colon>T" .
+ note wt = `\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>In1l (NewC C)\<Colon>T`
then obtain is_cls_C: "is_class G C" and
T: "T=Inl (Class C)"
by (rule wt_elim_cases) (auto dest: is_acc_classD)
@@ -2419,13 +2421,13 @@
by auto
next
case (NewA s0 elT s1 e i s2 a s3 L accC T A)
- have eval_init: "G\<turnstile>Norm s0 \<midarrow>init_comp_ty elT\<rightarrow> s1" .
- have eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>i\<rightarrow> s2" .
- have halloc: "G\<turnstile>abupd (check_neg i) s2\<midarrow>halloc Arr elT (the_Intg i)\<succ>a\<rightarrow> s3".
- have hyp_init: "PROP ?TypeSafe (Norm s0) s1 (In1r (init_comp_ty elT)) \<diamondsuit>" .
- have hyp_size: "PROP ?TypeSafe s1 s2 (In1l e) (In1 i)" .
- have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
- have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (New elT[e])\<Colon>T" .
+ note eval_init = `G\<turnstile>Norm s0 \<midarrow>init_comp_ty elT\<rightarrow> s1`
+ note eval_e = `G\<turnstile>s1 \<midarrow>e-\<succ>i\<rightarrow> s2`
+ note halloc = `G\<turnstile>abupd (check_neg i) s2\<midarrow>halloc Arr elT (the_Intg i)\<succ>a\<rightarrow> s3`
+ note hyp_init = `PROP ?TypeSafe (Norm s0) s1 (In1r (init_comp_ty elT)) \<diamondsuit>`
+ note hyp_size = `PROP ?TypeSafe s1 s2 (In1l e) (In1 i)`
+ note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
+ note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (New elT[e])\<Colon>T`
then obtain
wt_init: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>init_comp_ty elT\<Colon>\<surd>" and
wt_size: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-PrimT Integer" and
@@ -2457,8 +2459,8 @@
simp add: init_comp_ty_def))
(* simplified: to rewrite \<langle>Skip\<rangle> to In1r (Skip) *)
qed
- ultimately show ?thesis
- by (rule hyp_init [elim_format]) auto
+ ultimately show thesis
+ by (rule hyp_init [elim_format]) (auto intro: that)
qed
obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
proof -
@@ -2490,11 +2492,11 @@
by simp
next
case (Cast s0 e v s1 s2 castT L accC T A)
- have "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1" .
- have s2:"s2 = abupd (raise_if (\<not> G,store s1\<turnstile>v fits castT) ClassCast) s1" .
- have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)" .
- have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
- have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (Cast castT e)\<Colon>T" .
+ note `G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1`
+ note s2 = `s2 = abupd (raise_if (\<not> G,store s1\<turnstile>v fits castT) ClassCast) s1`
+ note hyp = `PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)`
+ note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
+ note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (Cast castT e)\<Colon>T`
then obtain eT
where wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-eT" and
eT: "G\<turnstile>eT\<preceq>? castT" and
@@ -2536,8 +2538,8 @@
by blast
next
case (Inst s0 e v s1 b instT L accC T A)
- have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)" .
- have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
+ note hyp = `PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)`
+ note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
from Inst.prems obtain eT
where wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-RefT eT" and
T: "T=Inl (PrimT Boolean)"
@@ -2560,9 +2562,9 @@
intro: conf_litval simp add: empty_dt_def)
next
case (UnOp s0 e v s1 unop L accC T A)
- have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)" .
- have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
- have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (UnOp unop e)\<Colon>T" .
+ note hyp = `PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)`
+ note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
+ note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (UnOp unop e)\<Colon>T`
then obtain eT
where wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-eT" and
wt_unop: "wt_unop unop eT" and
@@ -2587,15 +2589,15 @@
by simp
next
case (BinOp s0 e1 v1 s1 binop e2 v2 s2 L accC T A)
- have eval_e1: "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1" .
- have eval_e2: "G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2
- else In1r Skip)\<succ>\<rightarrow> (In1 v2, s2)" .
- have hyp_e1: "PROP ?TypeSafe (Norm s0) s1 (In1l e1) (In1 v1)" .
- have hyp_e2: "PROP ?TypeSafe s1 s2
+ note eval_e1 = `G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1`
+ note eval_e2 = `G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2
+ else In1r Skip)\<succ>\<rightarrow> (In1 v2, s2)`
+ note hyp_e1 = `PROP ?TypeSafe (Norm s0) s1 (In1l e1) (In1 v1)`
+ note hyp_e2 = `PROP ?TypeSafe s1 s2
(if need_second_arg binop v1 then In1l e2 else In1r Skip)
- (In1 v2)" .
- have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
- have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (BinOp binop e1 e2)\<Colon>T" .
+ (In1 v2)`
+ note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
+ note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (BinOp binop e1 e2)\<Colon>T`
then obtain e1T e2T where
wt_e1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e1\<Colon>-e1T" and
wt_e2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e2\<Colon>-e2T" and
@@ -2608,8 +2610,8 @@
daSkip: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
\<turnstile> dom (locals (store s1)) \<guillemotright>In1r Skip\<guillemotright> S"
by (auto intro: da_Skip [simplified] assigned.select_convs)
- have da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store ((Norm s0::state))))
- \<guillemotright>\<langle>BinOp binop e1 e2\<rangle>\<^sub>e\<guillemotright> A".
+ note da = `\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store ((Norm s0::state))))
+ \<guillemotright>\<langle>BinOp binop e1 e2\<rangle>\<^sub>e\<guillemotright> A`
then obtain E1 where
da_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1l e1\<guillemotright> E1"
@@ -2703,8 +2705,8 @@
by simp
next
case (Acc s0 v w upd s1 L accC T A)
- have hyp: "PROP ?TypeSafe (Norm s0) s1 (In2 v) (In2 (w,upd))" .
- have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
+ note hyp = `PROP ?TypeSafe (Norm s0) s1 (In2 v) (In2 (w,upd))`
+ note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
from Acc.prems obtain vT where
wt_v: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>v\<Colon>=vT" and
T: "T=Inl vT"
@@ -2712,7 +2714,7 @@
from Acc.prems obtain V where
da_v: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In2 v\<guillemotright> V"
- by (cases "\<exists> n. v=LVar n") (insert da.LVar,auto elim!: da_elim_cases)
+ by (cases "\<exists> n. v=LVar n") (insert da.LVar, auto elim!: da_elim_cases)
{
fix n assume lvar: "v=LVar n"
have "locals (store s1) n \<noteq> None"
@@ -2723,8 +2725,8 @@
also
have "dom (locals s0) \<subseteq> dom (locals (store s1))"
proof -
- have "G\<turnstile>Norm s0 \<midarrow>v=\<succ>(w, upd)\<rightarrow> s1" .
- thus ?thesis
+ from `G\<turnstile>Norm s0 \<midarrow>v=\<succ>(w, upd)\<rightarrow> s1`
+ show ?thesis
by (rule dom_locals_eval_mono_elim) simp
qed
finally show ?thesis
@@ -2743,12 +2745,12 @@
by simp
next
case (Ass s0 var w upd s1 e v s2 L accC T A)
- have eval_var: "G\<turnstile>Norm s0 \<midarrow>var=\<succ>(w, upd)\<rightarrow> s1" .
- have eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>v\<rightarrow> s2" .
- have hyp_var: "PROP ?TypeSafe (Norm s0) s1 (In2 var) (In2 (w,upd))" .
- have hyp_e: "PROP ?TypeSafe s1 s2 (In1l e) (In1 v)" .
- have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
- have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (var:=e)\<Colon>T" .
+ note eval_var = `G\<turnstile>Norm s0 \<midarrow>var=\<succ>(w, upd)\<rightarrow> s1`
+ note eval_e = `G\<turnstile>s1 \<midarrow>e-\<succ>v\<rightarrow> s2`
+ note hyp_var = `PROP ?TypeSafe (Norm s0) s1 (In2 var) (In2 (w,upd))`
+ note hyp_e = `PROP ?TypeSafe s1 s2 (In1l e) (In1 v)`
+ note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
+ note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (var:=e)\<Colon>T`
then obtain varT eT where
wt_var: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>var\<Colon>=varT" and
wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-eT" and
@@ -2790,8 +2792,8 @@
from eval_var wt_var da_var wf normal_s1
have "nrm V \<subseteq> dom (locals (store s1))"
by (cases rule: da_good_approxE') iprover
- with da_e show ?thesis
- by (rule da_weakenE)
+ with da_e show thesis
+ by (rule da_weakenE) (rule that)
qed
with conf_s1 wt_e
obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and
@@ -2844,9 +2846,9 @@
proof -
have "dom (locals (store ((Norm s0)::state)))
\<subseteq> dom (locals (store (s1)))"
- by (rule dom_locals_eval_mono_elim)
- with da_e show ?thesis
- by (rule da_weakenE)
+ by (rule dom_locals_eval_mono_elim) (rule Ass.hyps)
+ with da_e show thesis
+ by (rule da_weakenE) (rule that)
qed
from conf_s0 wt_var da_var
obtain conf_s1: "s1\<Colon>\<preceq>(G, L)"
@@ -2900,13 +2902,13 @@
qed
next
case (Cond s0 e0 b s1 e1 e2 v s2 L accC T A)
- have eval_e0: "G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1" .
- have eval_e1_e2: "G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<rightarrow> s2" .
- have hyp_e0: "PROP ?TypeSafe (Norm s0) s1 (In1l e0) (In1 b)" .
- have hyp_if: "PROP ?TypeSafe s1 s2
- (In1l (if the_Bool b then e1 else e2)) (In1 v)" .
- have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
- have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (e0 ? e1 : e2)\<Colon>T" .
+ note eval_e0 = `G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1`
+ note eval_e1_e2 = `G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<rightarrow> s2`
+ note hyp_e0 = `PROP ?TypeSafe (Norm s0) s1 (In1l e0) (In1 b)`
+ note hyp_if = `PROP ?TypeSafe s1 s2
+ (In1l (if the_Bool b then e1 else e2)) (In1 v)`
+ note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
+ note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (e0 ? e1 : e2)\<Colon>T`
then obtain T1 T2 statT where
wt_e0: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e0\<Colon>-PrimT Boolean" and
wt_e1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e1\<Colon>-T1" and
@@ -2994,24 +2996,24 @@
next
case (Call s0 e a s1 args vs s2 invDeclC mode statT mn pTs' s3 s3' accC'
v s4 L accC T A)
- have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<rightarrow> s1" .
- have eval_args: "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2" .
- have invDeclC: "invDeclC
+ note eval_e = `G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<rightarrow> s1`
+ note eval_args = `G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2`
+ note invDeclC = `invDeclC
= invocation_declclass G mode (store s2) a statT
- \<lparr>name = mn, parTs = pTs'\<rparr>" .
- have init_lvars:
- "s3 = init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> mode a vs s2".
- have check: "s3' =
- check_method_access G accC' statT mode \<lparr>name = mn, parTs = pTs'\<rparr> a s3" .
- have eval_methd:
- "G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<rightarrow> s4" .
- have hyp_e: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 a)" .
- have hyp_args: "PROP ?TypeSafe s1 s2 (In3 args) (In3 vs)" .
- have hyp_methd: "PROP ?TypeSafe s3' s4
- (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)) (In1 v)".
- have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
- have wt: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>
- \<turnstile>In1l ({accC',statT,mode}e\<cdot>mn( {pTs'}args))\<Colon>T" .
+ \<lparr>name = mn, parTs = pTs'\<rparr>`
+ note init_lvars =
+ `s3 = init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> mode a vs s2`
+ note check = `s3' =
+ check_method_access G accC' statT mode \<lparr>name = mn, parTs = pTs'\<rparr> a s3`
+ note eval_methd =
+ `G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<rightarrow> s4`
+ note hyp_e = `PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 a)`
+ note hyp_args = `PROP ?TypeSafe s1 s2 (In3 args) (In3 vs)`
+ note hyp_methd = `PROP ?TypeSafe s3' s4
+ (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)) (In1 v)`
+ note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
+ note wt = `\<lparr>prg=G, cls=accC, lcl=L\<rparr>
+ \<turnstile>In1l ({accC',statT,mode}e\<cdot>mn( {pTs'}args))\<Colon>T`
from wt obtain pTs statDeclT statM where
wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT" and
wt_args: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>args\<Colon>\<doteq>pTs" and
@@ -3074,8 +3076,8 @@
from eval_e wt_e da_e wf normal_s1
have "nrm E \<subseteq> dom (locals (store s1))"
by (cases rule: da_good_approxE') iprover
- with da_args show ?thesis
- by (rule da_weakenE)
+ with da_args show thesis
+ by (rule da_weakenE) (rule that)
qed
with conf_s1 wt_args
obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and
@@ -3290,8 +3292,7 @@
by (iprover intro: da.Body assigned.select_convs)
from _ this [simplified]
show ?thesis
- by (rule da.Methd [simplified,elim_format])
- (auto intro: dynM')
+ by (rule da.Methd [simplified,elim_format]) (auto intro: dynM' that)
qed
ultimately obtain
conf_s4: "s4\<Colon>\<preceq>(G, L')" and
@@ -3337,10 +3338,10 @@
qed
next
case (Methd s0 D sig v s1 L accC T A)
- have "G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1" .
- have hyp:"PROP ?TypeSafe (Norm s0) s1 (In1l (body G D sig)) (In1 v)" .
- have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
- have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (Methd D sig)\<Colon>T" .
+ note `G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1`
+ note hyp = `PROP ?TypeSafe (Norm s0) s1 (In1l (body G D sig)) (In1 v)`
+ note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
+ note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (Methd D sig)\<Colon>T`
then obtain m bodyT where
D: "is_class G D" and
m: "methd G D sig = Some m" and
@@ -3362,12 +3363,12 @@
by (auto simp add: Let_def body_def)
next
case (Body s0 D s1 c s2 s3 L accC T A)
- have eval_init: "G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1" .
- have eval_c: "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2" .
- have hyp_init: "PROP ?TypeSafe (Norm s0) s1 (In1r (Init D)) \<diamondsuit>" .
- have hyp_c: "PROP ?TypeSafe s1 s2 (In1r c) \<diamondsuit>" .
- have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
- have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (Body D c)\<Colon>T" .
+ note eval_init = `G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1`
+ note eval_c = `G\<turnstile>s1 \<midarrow>c\<rightarrow> s2`
+ note hyp_init = `PROP ?TypeSafe (Norm s0) s1 (In1r (Init D)) \<diamondsuit>`
+ note hyp_c = `PROP ?TypeSafe s1 s2 (In1r c) \<diamondsuit>`
+ note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
+ note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (Body D c)\<Colon>T`
then obtain bodyT where
iscls_D: "is_class G D" and
wt_c: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c\<Colon>\<surd>" and
@@ -3399,7 +3400,7 @@
have "(dom (locals (store ((Norm s0)::state))))
\<subseteq> (dom (locals (store s1)))"
by (rule dom_locals_eval_mono_elim)
- with da_c show ?thesis by (rule da_weakenE)
+ with da_c show thesis by (rule da_weakenE) (rule that)
qed
from conf_s1 wt_c da_C'
obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
@@ -3429,7 +3430,7 @@
(if \<exists>l. abrupt s2 = Some (Jump (Break l)) \<or>
abrupt s2 = Some (Jump (Cont l))
then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 else s2)" .
- ultimately show ?thesis
+ ultimately show ?thesis
by force
qed
moreover
@@ -3463,8 +3464,8 @@
by (cases s2) (auto intro: conforms_locals)
next
case (LVar s vn L accC T)
- have conf_s: "Norm s\<Colon>\<preceq>(G, L)" and
- wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In2 (LVar vn)\<Colon>T" .
+ note conf_s = `Norm s\<Colon>\<preceq>(G, L)` and
+ wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In2 (LVar vn)\<Colon>T`
then obtain vnT where
vnT: "L vn = Some vnT" and
T: "T=Inl vnT"
@@ -3486,14 +3487,14 @@
by (simp add: lvar_def)
next
case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC L accC' T A)
- have eval_init: "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<rightarrow> s1" .
- have eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2" .
- have fvar: "(v, s2') = fvar statDeclC stat fn a s2" .
- have check: "s3 = check_field_access G accC statDeclC fn stat a s2'" .
- have hyp_init: "PROP ?TypeSafe (Norm s0) s1 (In1r (Init statDeclC)) \<diamondsuit>" .
- have hyp_e: "PROP ?TypeSafe s1 s2 (In1l e) (In1 a)" .
- have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
- have wt: "\<lparr>prg=G, cls=accC', lcl=L\<rparr>\<turnstile>In2 ({accC,statDeclC,stat}e..fn)\<Colon>T" .
+ note eval_init = `G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<rightarrow> s1`
+ note eval_e = `G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2`
+ note fvar = `(v, s2') = fvar statDeclC stat fn a s2`
+ note check = `s3 = check_field_access G accC statDeclC fn stat a s2'`
+ note hyp_init = `PROP ?TypeSafe (Norm s0) s1 (In1r (Init statDeclC)) \<diamondsuit>`
+ note hyp_e = `PROP ?TypeSafe s1 s2 (In1l e) (In1 a)`
+ note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
+ note wt = `\<lparr>prg=G, cls=accC', lcl=L\<rparr>\<turnstile>In2 ({accC,statDeclC,stat}e..fn)\<Colon>T`
then obtain statC f where
wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-Class statC" and
accfield: "accfield G accC statC fn = Some (statDeclC,f)" and
@@ -3529,8 +3530,8 @@
have "(dom (locals (store ((Norm s0)::state))))
\<subseteq> (dom (locals (store s1)))"
by (rule dom_locals_eval_mono_elim)
- with da_e show ?thesis
- by (rule da_weakenE)
+ with da_e show thesis
+ by (rule da_weakenE) (rule that)
qed
with conf_s1 wt_e
obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and
@@ -3602,13 +3603,13 @@
by auto
next
case (AVar s0 e1 a s1 e2 i s2 v s2' L accC T A)
- have eval_e1: "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>a\<rightarrow> s1" .
- have eval_e2: "G\<turnstile>s1 \<midarrow>e2-\<succ>i\<rightarrow> s2" .
- have hyp_e1: "PROP ?TypeSafe (Norm s0) s1 (In1l e1) (In1 a)" .
- have hyp_e2: "PROP ?TypeSafe s1 s2 (In1l e2) (In1 i)" .
- have avar: "(v, s2') = avar G i a s2" .
- have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
- have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In2 (e1.[e2])\<Colon>T" .
+ note eval_e1 = `G\<turnstile>Norm s0 \<midarrow>e1-\<succ>a\<rightarrow> s1`
+ note eval_e2 = `G\<turnstile>s1 \<midarrow>e2-\<succ>i\<rightarrow> s2`
+ note hyp_e1 = `PROP ?TypeSafe (Norm s0) s1 (In1l e1) (In1 a)`
+ note hyp_e2 = `PROP ?TypeSafe s1 s2 (In1l e2) (In1 i)`
+ note avar = `(v, s2') = avar G i a s2`
+ note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
+ note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In2 (e1.[e2])\<Colon>T`
then obtain elemT
where wt_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e1\<Colon>-elemT.[]" and
wt_e2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e2\<Colon>-PrimT Integer" and
@@ -3702,12 +3703,12 @@
by (auto elim!: wt_elim_cases)
next
case (Cons s0 e v s1 es vs s2 L accC T A)
- have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1" .
- have eval_es: "G\<turnstile>s1 \<midarrow>es\<doteq>\<succ>vs\<rightarrow> s2" .
- have hyp_e: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)" .
- have hyp_es: "PROP ?TypeSafe s1 s2 (In3 es) (In3 vs)" .
- have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
- have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In3 (e # es)\<Colon>T" .
+ note eval_e = `G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1`
+ note eval_es = `G\<turnstile>s1 \<midarrow>es\<doteq>\<succ>vs\<rightarrow> s2`
+ note hyp_e = `PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)`
+ note hyp_es = `PROP ?TypeSafe s1 s2 (In3 es) (In3 vs)`
+ note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
+ note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In3 (e # es)\<Colon>T`
then obtain eT esT where
wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-eT" and
wt_es: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>es\<Colon>\<doteq>esT" and
@@ -3740,8 +3741,8 @@
from eval_e wt_e da_e wf True
have "nrm E \<subseteq> dom (locals (store s1))"
by (cases rule: da_good_approxE') iprover
- with da_es show ?thesis
- by (rule da_weakenE)
+ with da_es show thesis
+ by (rule da_weakenE) (rule that)
qed
with conf_s1 wt_es
obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and
@@ -3758,7 +3759,7 @@
ultimately show ?thesis using T by simp
qed
qed
- then show ?thesis .
+ from this and conf_s0 wt da show ?thesis .
qed
text {*
@@ -3938,8 +3939,8 @@
by (rule lab)
next
case (Comp s0 c1 s1 c2 s2 L accC T A)
- have eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1" .
- have eval_c2: "G\<turnstile>s1 \<midarrow>c2\<rightarrow> s2" .
+ note eval_c1 = `G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1`
+ note eval_c2 = `G\<turnstile>s1 \<midarrow>c2\<rightarrow> s2`
from Comp.prems obtain
wt_c1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
wt_c2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c2\<Colon>\<surd>"
@@ -3967,8 +3968,8 @@
from eval_c1 wt_c1 da_c1 wf normal_s1
have "nrm C1 \<subseteq> dom (locals (store s1))"
by (cases rule: da_good_approxE') iprover
- with da_c2 show ?thesis
- by (rule da_weakenE)
+ with da_c2 show thesis
+ by (rule da_weakenE) (rule that)
qed
with wt_c2 have "P L accC s1 \<langle>c2\<rangle>\<^sub>s \<diamondsuit> s2"
by (rule Comp.hyps)
@@ -3981,8 +3982,8 @@
by (rule comp) iprover+
next
case (If s0 e b s1 c1 c2 s2 L accC T A)
- have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" .
- have eval_then_else: "G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2" .
+ note eval_e = `G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1`
+ note eval_then_else = `G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2`
from If.prems
obtain
wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean" and
@@ -4023,8 +4024,8 @@
have "dom (locals (store ((Norm s0)::state)))
\<union> assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))"
by (rule Un_least)
- with da_then_else show ?thesis
- by (rule da_weakenE)
+ with da_then_else show thesis
+ by (rule da_weakenE) (rule that)
qed
with wt_then_else
have "P L accC s1 \<langle>if the_Bool b then c1 else c2\<rangle>\<^sub>s \<diamondsuit> s2"
--- a/src/HOL/Bali/WellForm.thy Wed Jun 13 00:01:38 2007 +0200
+++ b/src/HOL/Bali/WellForm.thy Wed Jun 13 00:01:41 2007 +0200
@@ -1992,11 +1992,11 @@
show "?thesis m d"
proof (cases "?newMethods")
case None
- from None clsC nObj ws m declC hyp
- show "?thesis" by (auto simp add: methd_rec)
+ from None clsC nObj ws m declC
+ show "?thesis" by (auto simp add: methd_rec) (rule hyp)
next
case Some
- from Some clsC nObj ws m declC hyp
+ from Some clsC nObj ws m declC
show "?thesis"
by (auto simp add: methd_rec
dest: wf_prog_cdecl wf_cdecl_supD is_acc_class_is_class)
@@ -2665,7 +2665,7 @@
with neq show ?thesis
by (contradiction)
next
- case Subcls show ?thesis .
+ case Subcls then show ?thesis .
qed
moreover
from stat_acc wf
@@ -2920,8 +2920,8 @@
show ?thesis
proof (induct)
case (Immediate m C)
- have "G \<turnstile> m in C permits_acc_from accC" and "accmodi m = Private" .
- then show ?case
+ from `G \<turnstile> m in C permits_acc_from accC` and `accmodi m = Private`
+ show ?case
by (simp add: permits_acc_def)
next
case Overriding
@@ -2985,8 +2985,8 @@
show ?thesis
proof (induct)
case (Immediate f C)
- have "G \<turnstile> f in C permits_acc_from accC" and "accmodi f = Package" .
- then show ?case
+ from `G \<turnstile> f in C permits_acc_from accC` and `accmodi f = Package`
+ show ?case
by (simp add: permits_acc_def)
next
case Overriding
@@ -3009,7 +3009,7 @@
show ?thesis
proof (induct)
case (Immediate f C)
- have "G \<turnstile> f in C permits_acc_from accC" .
+ note `G \<turnstile> f in C permits_acc_from accC`
moreover
assume "accmodi f = Protected" and "is_field f" and "\<not> is_static f" and
"pid (declclass f) \<noteq> pid accC"
@@ -3036,14 +3036,14 @@
case (Immediate f C)
assume "accmodi f = Protected" and "is_field f" and "is_static f" and
"pid (declclass f) \<noteq> pid accC"
- moreover
- have "G \<turnstile> f in C permits_acc_from accC" .
+ moreover
+ note `G \<turnstile> f in C permits_acc_from accC`
ultimately
have "G\<turnstile> accC \<preceq>\<^sub>C declclass f"
by (auto simp add: permits_acc_def)
moreover
- have "G \<turnstile> f member_in C" .
- then have "G\<turnstile>C \<preceq>\<^sub>C declclass f"
+ from `G \<turnstile> f member_in C`
+ have "G\<turnstile>C \<preceq>\<^sub>C declclass f"
by (rule member_in_class_relation)
ultimately show ?case
by blast
@@ -3053,4 +3053,4 @@
qed
qed
-end
\ No newline at end of file
+end