# HG changeset patch
# User kleing
# Date 1011129725 -3600
# Node ID a47f51daa6dc9567626211eade21074f23266b11
# Parent  7b7051ae49a04dd3182e24b63d892f141f8ff873
use exec_lub instead of some_lub

diff -r 7b7051ae49a0 -r a47f51daa6dc src/HOL/MicroJava/BV/JType.thy
--- a/src/HOL/MicroJava/BV/JType.thy	Tue Jan 15 22:21:30 2002 +0100
+++ b/src/HOL/MicroJava/BV/JType.thy	Tue Jan 15 22:22:05 2002 +0100
@@ -9,6 +9,14 @@
 theory JType = WellForm + Err:
 
 constdefs
+  super :: "'a prog \<Rightarrow> cname \<Rightarrow> cname"
+  "super G C == fst (the (class G C))"
+
+lemma superI:
+  "(C,D) \<in> subcls1 G \<Longrightarrow> super G C = D"
+  by (unfold super_def) (auto dest: subcls1D)
+
+constdefs
   is_ref :: "ty => bool"
   "is_ref T == case T of PrimT t => False | RefT r => True"
 
@@ -19,7 +27,7 @@
            | RefT R1 => (case T2 of PrimT P => Err | RefT R2 => 
   (case R1 of NullT => (case R2 of NullT => OK NT | ClassT C => OK (Class C))
             | ClassT C => (case R2 of NullT => OK (Class C) 
-                           | ClassT D => OK (Class (some_lub ((subcls1 G)^* ) C D)))))"
+                           | ClassT D => OK (Class (exec_lub (subcls1 G) (super G) C D)))))"
 
   subtype :: "'c prog => ty => ty => bool"
   "subtype G T1 T2 == G \<turnstile> T1 \<preceq> T2"
@@ -28,6 +36,7 @@
   "is_ty G T == case T of PrimT P => True | RefT R =>
                (case R of NullT => True | ClassT C => (C,Object):(subcls1 G)^*)"
 
+
 translations
   "types G" == "Collect (is_type G)"
 
@@ -156,8 +165,8 @@
   apply (auto split: err.split)
   apply (drule is_tyI, assumption)
   apply (auto simp add: is_ty_def is_type_conv simp del: is_type.simps 
-              split: ty.split ref_ty.split)
-  apply (blast dest!: is_lub_some_lub is_lubD is_ubD intro!: is_ubI)
+              split: ty.split ref_ty.split)  
+  apply (blast dest!: is_lub_exec_lub is_lubD is_ubD intro!: is_ubI superI)
   done
 
 
@@ -181,10 +190,15 @@
     obtain u where
       "is_lub ((subcls1 G)^* ) c1 c2 u"      
       by (blast dest: single_valued_has_lubs)
-    with acyclic
-    have "G \<turnstile> c1 \<preceq>C some_lub ((subcls1 G)^* ) c1 c2 \<and>
-          G \<turnstile> c2 \<preceq>C some_lub ((subcls1 G)^* ) c1 c2"
-      by (simp add: some_lub_conv) (blast dest: is_lubD is_ubD)
+    moreover
+    note acyclic
+    moreover
+    have "\<forall>x y. (x, y) \<in> subcls1 G \<longrightarrow> super G x = y"
+      by (blast intro: superI)
+    ultimately
+    have "G \<turnstile> c1 \<preceq>C exec_lub (subcls1 G) (super G) c1 c2 \<and>
+          G \<turnstile> c2 \<preceq>C exec_lub (subcls1 G) (super G) c1 c2"
+      by (simp add: exec_lub_conv) (blast dest: is_lubD is_ubD)
   } note this [simp]
       
   assume "is_type G t1" "is_type G t2" "sup G t1 t2 = OK s"
@@ -218,14 +232,14 @@
       lub: "is_lub ((subcls1 G)^* ) c1 c2 u"
       by (blast dest: single_valued_has_lubs)   
     with acyclic
-    have "some_lub ((subcls1 G)^* ) c1 c2 = u"
-      by (rule some_lub_conv)
+    have "exec_lub (subcls1 G) (super G) c1 c2 = u"
+      by (blast intro: superI exec_lub_conv)
     moreover
     from lub le
     have "G \<turnstile> u \<preceq>C D" 
       by (simp add: is_lub_def is_ub_def)
     ultimately     
-    have "G \<turnstile> some_lub ((subcls1 G)\<^sup>*) c1 c2 \<preceq>C D"
+    have "G \<turnstile> exec_lub (subcls1 G) (super G) c1 c2 \<preceq>C D"
       by blast
   } note this [intro]
 
diff -r 7b7051ae49a0 -r a47f51daa6dc src/HOL/MicroJava/BV/Semilat.thy
--- a/src/HOL/MicroJava/BV/Semilat.thy	Tue Jan 15 22:21:30 2002 +0100
+++ b/src/HOL/MicroJava/BV/Semilat.thy	Tue Jan 15 22:22:05 2002 +0100
@@ -251,8 +251,9 @@
 done
 
 
-lemma "\<lbrakk> acyclic r; !x y. (x,y) \<in> r \<longrightarrow> f x = y; is_lub (r\<^sup>*) x y u \<rbrakk> \<Longrightarrow>
-       exec_lub r f x y = u";
+lemma exec_lub_conv:
+  "\<lbrakk> acyclic r; !x y. (x,y) \<in> r \<longrightarrow> f x = y; is_lub (r\<^sup>*) x y u \<rbrakk> \<Longrightarrow>
+  exec_lub r f x y = u";
 apply(unfold exec_lub_def)
 apply(rule_tac P = "\<lambda>z. (y,z) \<in> r\<^sup>* \<and> (z,u) \<in> r\<^sup>*" and
                r = "(r \<inter> {(a,b). (y,a) \<in> r\<^sup>* \<and> (b,u) \<in> r\<^sup>*})^-1" in while_rule)
@@ -285,4 +286,9 @@
 apply(blast dest:rtrancl_into_rtrancl)
 done
 
+lemma is_lub_exec_lub:
+  "\<lbrakk> single_valued r; acyclic r; (x,u):r^*; (y,u):r^*; !x y. (x,y) \<in> r \<longrightarrow> f x = y \<rbrakk>
+  \<Longrightarrow> is_lub (r^* ) x y (exec_lub r f x y)"
+  by (fastsimp dest: single_valued_has_lubs simp add: exec_lub_conv)
+
 end
diff -r 7b7051ae49a0 -r a47f51daa6dc src/HOL/MicroJava/ROOT.ML
--- a/src/HOL/MicroJava/ROOT.ML	Tue Jan 15 22:21:30 2002 +0100
+++ b/src/HOL/MicroJava/ROOT.ML	Tue Jan 15 22:22:05 2002 +0100
@@ -4,6 +4,10 @@
 add_path "JVM";
 add_path "BV";
 
+use_thy "JVMType"
+use_thy "JVMExceptions"
+
+(*
 use_thy "JTypeSafe";
 use_thy "Example";
 use_thy "JListExample";
@@ -11,6 +15,7 @@
 use_thy "BVSpecTypeSafe";
 use_thy "JVM";
 use_thy "LBVSpec"; 
+*)
 (* momentarily broken:
 use_thy "LBVCorrect";
 use_thy "LBVComplete";