--- a/src/HOL/Bali/Decl.thy Wed Mar 28 12:28:24 2012 +0200
+++ b/src/HOL/Bali/Decl.thy Wed Mar 28 13:38:56 2012 +0200
@@ -129,11 +129,12 @@
acc_modi_Package_le acc_modi_le_Package
acc_modi_Protected_le acc_modi_le_Protected
-lemma acc_modi_Package_le_cases
- [consumes 1,case_names Package Protected Public]:
- "Package \<le> m \<Longrightarrow> ( m = Package \<Longrightarrow> P m) \<Longrightarrow> (m=Protected \<Longrightarrow> P m) \<Longrightarrow>
- (m=Public \<Longrightarrow> P m) \<Longrightarrow> P m"
-by (auto dest: acc_modi_Package_le)
+lemma acc_modi_Package_le_cases:
+ assumes "Package \<le> m"
+ obtains (Package) "m = Package"
+ | (Protected) "m = Protected"
+ | (Public) "m = Public"
+using assms by (auto dest: acc_modi_Package_le)
subsubsection {* Static Modifier *}
--- a/src/HOL/Bali/Trans.thy Wed Mar 28 12:28:24 2012 +0200
+++ b/src/HOL/Bali/Trans.thy Wed Mar 28 13:38:56 2012 +0200
@@ -17,23 +17,18 @@
| e1.[e2] \<Rightarrow> \<exists> a i. e1= Lit a \<and> e2 = Lit i
| InsInitV c v \<Rightarrow> False)"
-lemma groundVar_cases [consumes 1, case_names LVar FVar AVar]:
- assumes ground: "groundVar v" and
- LVar: "\<And> ln. \<lbrakk>v=LVar ln\<rbrakk> \<Longrightarrow> P" and
- FVar: "\<And> accC statDeclC stat a fn.
- \<lbrakk>v={accC,statDeclC,stat}(Lit a)..fn\<rbrakk> \<Longrightarrow> P" and
- AVar: "\<And> a i. \<lbrakk>v=(Lit a).[Lit i]\<rbrakk> \<Longrightarrow> P"
- shows "P"
-proof -
- from ground LVar FVar AVar
- show ?thesis
- apply (cases v)
- apply (simp add: groundVar_def)
- apply (simp add: groundVar_def,blast)
- apply (simp add: groundVar_def,blast)
- apply (simp add: groundVar_def)
- done
-qed
+lemma groundVar_cases:
+ assumes ground: "groundVar v"
+ obtains (LVar) ln where "v=LVar ln"
+ | (FVar) accC statDeclC stat a fn where "v={accC,statDeclC,stat}(Lit a)..fn"
+ | (AVar) a i where "v=(Lit a).[Lit i]"
+ using ground LVar FVar AVar
+ apply (cases v)
+ apply (simp add: groundVar_def)
+ apply (simp add: groundVar_def,blast)
+ apply (simp add: groundVar_def,blast)
+ apply (simp add: groundVar_def)
+ done
definition
groundExprs :: "expr list \<Rightarrow> bool"
--- a/src/HOL/Bali/TypeRel.thy Wed Mar 28 12:28:24 2012 +0200
+++ b/src/HOL/Bali/TypeRel.thy Wed Mar 28 13:38:56 2012 +0200
@@ -200,9 +200,10 @@
qed
qed
-lemma subclseq_cases [consumes 1, case_names Eq Subcls]:
- "\<lbrakk>G\<turnstile>C \<preceq>\<^sub>C D; C = D \<Longrightarrow> P; G\<turnstile>C \<prec>\<^sub>C D \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
-by (blast intro: rtrancl_cases)
+lemma subclseq_cases:
+ assumes "G\<turnstile>C \<preceq>\<^sub>C D"
+ obtains (Eq) "C = D" | (Subcls) "G\<turnstile>C \<prec>\<^sub>C D"
+using assms by (blast intro: rtrancl_cases)
lemma subclseq_acyclic:
"\<lbrakk>G\<turnstile>C \<preceq>\<^sub>C D; G\<turnstile>D \<preceq>\<^sub>C C; ws_prog G\<rbrakk> \<Longrightarrow> C=D"
--- a/src/HOL/Bali/WellForm.thy Wed Mar 28 12:28:24 2012 +0200
+++ b/src/HOL/Bali/WellForm.thy Wed Mar 28 13:38:56 2012 +0200
@@ -1052,23 +1052,19 @@
qed
qed
-lemma non_Package_instance_method_inheritance_cases [consumes 6,
- case_names Inheritance Overriding]:
+lemma non_Package_instance_method_inheritance_cases:
assumes old_inheritable: "G\<turnstile>Method old inheritable_in (pid C)" and
accmodi_old: "accmodi old \<noteq> Package" and
instance_method: "\<not> is_static old" and
subcls: "G\<turnstile>C \<prec>\<^sub>C declclass old" and
old_declared: "G\<turnstile>Method old declared_in (declclass old)" and
- wf: "wf_prog G" and
- inheritance: "G\<turnstile>Method old member_of C \<Longrightarrow> P" and
- overriding: "\<And> new.
- \<lbrakk>G\<turnstile> new overrides\<^sub>S old;G\<turnstile>Method new member_of C\<rbrakk>
- \<Longrightarrow> P"
- shows P
+ wf: "wf_prog G"
+ obtains (Inheritance) "G\<turnstile>Method old member_of C"
+ | (Overriding) new where "G\<turnstile> new overrides\<^sub>S old" and "G\<turnstile>Method new member_of C"
proof -
from old_inheritable accmodi_old instance_method subcls old_declared wf
- inheritance overriding
- show ?thesis
+ Inheritance Overriding
+ show thesis
by (auto dest: non_Package_instance_method_inheritance)
qed
@@ -1438,15 +1434,13 @@
qed
qed
-lemma methd_rec_Some_cases [consumes 4, case_names NewMethod InheritedMethod]:
+lemma methd_rec_Some_cases:
assumes methd_C: "methd G C sig = Some m" and
ws: "ws_prog G" and
clsC: "class G C = Some c" and
neq_C_Obj: "C\<noteq>Object"
- shows
-"\<lbrakk>table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig = Some m \<Longrightarrow> P;
- \<lbrakk>G\<turnstile>C inherits (method sig m); methd G (super c) sig = Some m\<rbrakk> \<Longrightarrow> P
- \<rbrakk> \<Longrightarrow> P"
+ obtains (NewMethod) "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig = Some m"
+ | (InheritedMethod) "G\<turnstile>C inherits (method sig m)" and "methd G (super c) sig = Some m"
proof -
let ?inherited = "filter_tab (\<lambda>sig m. G\<turnstile>C inherits method sig m)
(methd G (super c))"
@@ -1454,20 +1448,17 @@
from ws clsC neq_C_Obj methd_C
have methd_unfold: "(?inherited ++ ?new) sig = Some m"
by (simp add: methd_rec)
- assume NewMethod: "?new sig = Some m \<Longrightarrow> P"
- assume InheritedMethod: "\<lbrakk>G\<turnstile>C inherits (method sig m);
- methd G (super c) sig = Some m\<rbrakk> \<Longrightarrow> P"
- show P
+ show thesis
proof (cases "?new sig")
case None
with methd_unfold have "?inherited sig = Some m"
by (auto)
- with InheritedMethod show P by blast
+ with InheritedMethod show ?thesis by blast
next
case Some
with methd_unfold have "?new sig = Some m"
by auto
- with NewMethod show P by blast
+ with NewMethod show ?thesis by blast
qed
qed
@@ -1708,23 +1699,19 @@
qed
qed
-lemma inheritable_instance_methd_cases [consumes 6
- , case_names Inheritance Overriding]:
+lemma inheritable_instance_methd_cases:
assumes subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D" and
is_cls_D: "is_class G D" and
wf: "wf_prog G" and
old: "methd G D sig = Some old" and
accmodi_old: "Protected \<le> accmodi old" and
- not_static_old: "\<not> is_static old" and
- inheritance: "methd G C sig = Some old \<Longrightarrow> P" and
- overriding: "\<And> new. \<lbrakk>methd G C sig = Some new;
- G,sig\<turnstile>new overrides\<^sub>S old\<rbrakk> \<Longrightarrow> P"
-
- shows P
+ not_static_old: "\<not> is_static old"
+ obtains (Inheritance) "methd G C sig = Some old"
+ | (Overriding) new where "methd G C sig = Some new" and "G,sig\<turnstile>new overrides\<^sub>S old"
proof -
-from subclseq_C_D is_cls_D wf old accmodi_old not_static_old
-show ?thesis
- by (auto dest: inheritable_instance_methd intro: inheritance overriding)
+ from subclseq_C_D is_cls_D wf old accmodi_old not_static_old
+ show ?thesis
+ by (auto dest: inheritable_instance_methd intro: Inheritance Overriding)
qed
lemma inheritable_instance_methd_props:
@@ -1941,21 +1928,22 @@
apply (auto dest!: accmethd_SomeD)
done
-lemma mheads_cases [consumes 2, case_names Class_methd
- Iface_methd Iface_Object_methd Array_Object_methd]:
-"\<lbrakk>emh \<in> mheads G S t sig; wf_prog G;
- \<And> C D m. \<lbrakk>t = ClassT C;declrefT emh = ClassT D; accmethd G S C sig = Some m;
- (declclass m = D); mhead (mthd m) = (mhd emh)\<rbrakk> \<Longrightarrow> P emh;
- \<And> I im. \<lbrakk>t = IfaceT I; im \<in> accimethds G (pid S) I sig; mthd im = mhd emh\<rbrakk>
- \<Longrightarrow> P emh;
- \<And> I m. \<lbrakk>t = IfaceT I; G\<turnstile>Iface I accessible_in (pid S);
- accmethd G S Object sig = Some m; accmodi m \<noteq> Private;
- declrefT emh = ClassT Object; mhead (mthd m) = mhd emh\<rbrakk> \<Longrightarrow> P emh;
- \<And> T m. \<lbrakk>t = ArrayT T;G\<turnstile>Array T accessible_in (pid S);
- accmethd G S Object sig = Some m; accmodi m \<noteq> Private;
- declrefT emh = ClassT Object; mhead (mthd m) = mhd emh\<rbrakk> \<Longrightarrow> P emh
-\<rbrakk> \<Longrightarrow> P emh"
-by (blast dest!: mheadsD)
+lemma mheads_cases:
+ assumes "emh \<in> mheads G S t sig" and "wf_prog G"
+ obtains (Class_methd) C D m where
+ "t = ClassT C" "declrefT emh = ClassT D" "accmethd G S C sig = Some m"
+ "declclass m = D" "mhead (mthd m) = mhd emh"
+ | (Iface_methd) I im where "t = IfaceT I"
+ "im \<in> accimethds G (pid S) I sig" "mthd im = mhd emh"
+ | (Iface_Object_methd) I m where
+ "t = IfaceT I" "G\<turnstile>Iface I accessible_in (pid S)"
+ "accmethd G S Object sig = Some m" "accmodi m \<noteq> Private"
+ "declrefT emh = ClassT Object" "mhead (mthd m) = mhd emh"
+ | (Array_Object_methd) T m where
+ "t = ArrayT T" "G\<turnstile>Array T accessible_in (pid S)"
+ "accmethd G S Object sig = Some m" "accmodi m \<noteq> Private"
+ "declrefT emh = ClassT Object" "mhead (mthd m) = mhd emh"
+using assms by (blast dest!: mheadsD)
lemma declclassD[rule_format]:
"\<lbrakk>wf_prog G;class G C = Some c; methd G C sig = Some m;
--- a/src/HOL/Unix/Unix.thy Wed Mar 28 12:28:24 2012 +0200
+++ b/src/HOL/Unix/Unix.thy Wed Mar 28 13:38:56 2012 +0200
@@ -558,7 +558,7 @@
*}
lemma transitions_invariant:
- assumes r: "\<And>r x r'. r \<midarrow>x\<rightarrow> r' \<Longrightarrow> Q r \<Longrightarrow> P x \<Longrightarrow> Q r'"
+ assumes r: "\<And>r x r'. r \<midarrow>x\<rightarrow> r' \<Longrightarrow> Q r \<Longrightarrow> P x \<Longrightarrow> Q r'"
and trans: "root =xs\<Rightarrow> root'"
shows "Q root \<Longrightarrow> \<forall>x \<in> set xs. P x \<Longrightarrow> Q root'"
using trans