# HG changeset patch
# User wenzelm
# Date 1332934736 -7200
# Node ID 0e5bd01383a29225cdfff3afef5fb8db35480cfc
# Parent  f760e15343bc70e0e61d0b3ef56898e2b44facd2# Parent  568fdc70e565604210fd56e0b12b16eb091853ef
merged

diff -r f760e15343bc -r 0e5bd01383a2 src/HOL/Bali/Decl.thy
--- 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 *}
diff -r f760e15343bc -r 0e5bd01383a2 src/HOL/Bali/Trans.thy
--- 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"
diff -r f760e15343bc -r 0e5bd01383a2 src/HOL/Bali/TypeRel.thy
--- 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"
diff -r f760e15343bc -r 0e5bd01383a2 src/HOL/Bali/WellForm.thy
--- 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; 
diff -r f760e15343bc -r 0e5bd01383a2 src/HOL/Unix/Unix.thy
--- 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