src/HOL/MicroJava/J/Example.thy

--- a/src/HOL/MicroJava/J/Example.thy	Tue Feb 26 13:47:19 2002 +0100
+++ b/src/HOL/MicroJava/J/Example.thy	Tue Feb 26 15:45:32 2002 +0100
@@ -6,7 +6,7 @@
 
 header {* \isaheader{Example MicroJava Program} *}
 
-theory Example = Eval:
+theory Example = SystemClasses + Eval:
 
 text {* 
 The following example MicroJava program includes:
@@ -72,12 +72,17 @@
 axioms
   Base_not_Object: "Base \<noteq> Object"
   Ext_not_Object:  "Ext  \<noteq> Object"
-  e_not_This:      "e \<noteq> This"
+  Base_not_Xcpt:   "Base \<noteq> Xcpt z"
+  Ext_not_Xcpt:    "Ext  \<noteq> Xcpt z"
+  e_not_This:      "e \<noteq> This"  
 
 declare Base_not_Object [simp] Ext_not_Object [simp]
+declare Base_not_Xcpt [simp] Ext_not_Xcpt [simp]
 declare e_not_This [simp]
-declare Base_not_Object [THEN not_sym, simp]
-declare Ext_not_Object  [THEN not_sym, simp]
+declare Base_not_Object [symmetric, simp]
+declare Ext_not_Object  [symmetric, simp]
+declare Base_not_Xcpt [symmetric, simp]
+declare Ext_not_Xcpt  [symmetric, simp]
 
 consts
   foo_Base::  java_mb
@@ -119,7 +124,7 @@
 
 translations
   "NP"   == "NullPointer"
-  "tprg" == "[ObjectC, BaseC, ExtC]"
+  "tprg" == "[ObjectC, BaseC, ExtC, ClassCastC, NullPointerC, OutOfMemoryC]"
   "obj1"    <= "(Ext, empty((vee, Base)\<mapsto>Bool False)
          ((vee, Ext )\<mapsto>Intg 0))"
   "s0" == " Norm    (empty, empty)"
@@ -142,11 +147,26 @@
 apply (simp (no_asm))
 done
 
+lemma class_tprg_NP [simp]: "class tprg (Xcpt NP) = Some (Object, [], [])"
+apply (unfold ObjectC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def BaseC_def ExtC_def class_def)
+apply (simp (no_asm))
+done
+
+lemma class_tprg_OM [simp]: "class tprg (Xcpt OutOfMemory) = Some (Object, [], [])"
+apply (unfold ObjectC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def BaseC_def ExtC_def class_def)
+apply (simp (no_asm))
+done
+
+lemma class_tprg_CC [simp]: "class tprg (Xcpt ClassCast) = Some (Object, [], [])"
+apply (unfold ObjectC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def BaseC_def ExtC_def class_def)
+apply (simp (no_asm))
+done
+
 lemma class_tprg_Base [simp]: 
 "class tprg Base = Some (Object,  
     [(vee, PrimT Boolean)],  
           [((foo, [Class Base]), Class Base, foo_Base)])"
-apply (unfold ObjectC_def BaseC_def ExtC_def class_def)
+apply (unfold ObjectC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def BaseC_def ExtC_def class_def)
 apply (simp (no_asm))
 done
 
@@ -174,8 +194,8 @@
 done
 
 lemma class_tprgD: 
-"class tprg C = Some z ==> C=Object \<or> C=Base \<or> C=Ext"
-apply (unfold ObjectC_def BaseC_def ExtC_def class_def)
+"class tprg C = Some z ==> C=Object \<or> C=Base \<or> C=Ext \<or> C=Xcpt NP \<or> C=Xcpt ClassCast \<or> C=Xcpt OutOfMemory"
+apply (unfold ObjectC_def ClassCastC_def NullPointerC_def OutOfMemoryC_def BaseC_def ExtC_def class_def)
 apply (auto split add: split_if_asm simp add: map_of_Cons)
 done
 
@@ -188,7 +208,7 @@
 done
 
 lemma unique_classes: "unique tprg"
-apply (simp (no_asm) add: ObjectC_def BaseC_def ExtC_def)
+apply (simp (no_asm) add: ObjectC_def BaseC_def ExtC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def)
 done
 
 lemmas subcls_direct = subcls1I [THEN r_into_rtrancl]
@@ -278,6 +298,30 @@
 apply (simp (no_asm))
 done
 
+lemma wf_NP:
+"wf_cdecl wf_java_mdecl tprg NullPointerC"
+apply (unfold wf_cdecl_def wf_fdecl_def NullPointerC_def)
+apply (simp add: class_def)
+apply (fold NullPointerC_def class_def)
+apply auto
+done
+
+lemma wf_OM:
+"wf_cdecl wf_java_mdecl tprg OutOfMemoryC"
+apply (unfold wf_cdecl_def wf_fdecl_def OutOfMemoryC_def)
+apply (simp add: class_def)
+apply (fold OutOfMemoryC_def class_def)
+apply auto
+done
+
+lemma wf_CC:
+"wf_cdecl wf_java_mdecl tprg ClassCastC"
+apply (unfold wf_cdecl_def wf_fdecl_def ClassCastC_def)
+apply (simp add: class_def)
+apply (fold ClassCastC_def class_def)
+apply auto
+done
+
 lemma wf_BaseC: 
 "wf_cdecl wf_java_mdecl tprg BaseC"
 apply (unfold wf_cdecl_def wf_fdecl_def BaseC_def)
@@ -298,10 +342,14 @@
 apply auto
 done
 
+lemma [simp]: "fst ObjectC = Object" by (simp add: ObjectC_def)
+
 lemma wf_tprg: 
 "wf_prog wf_java_mdecl tprg"
 apply (unfold wf_prog_def Let_def)
-apply(simp add: wf_ObjectC wf_BaseC wf_ExtC unique_classes)
+apply (simp add: wf_ObjectC wf_BaseC wf_ExtC wf_NP wf_OM wf_CC unique_classes)
+apply (rule wf_syscls)
+apply (simp add: SystemClasses_def)
 done
 
 lemma appl_methds_foo_Base: