
diff -r a70b796d9af8 -r a50365d21144 src/HOL/MicroJava/J/Example.thy
--- a/src/HOL/MicroJava/J/Example.thy	Thu Feb 01 20:51:48 2001 +0100
+++ b/src/HOL/MicroJava/J/Example.thy	Thu Feb 01 20:53:13 2001 +0100
@@ -28,7 +28,7 @@
 }
 *)
 
-Example = Eval + 
+theory Example = Eval:
 
 datatype cnam_ = Base_ | Ext_
 datatype vnam_ = vee_ | x_ | e_
@@ -38,18 +38,23 @@
   cnam_ :: "cnam_ => cname"
   vnam_ :: "vnam_ => vnam"
 
-rules (* cnam_ and vnam_ are intended to be isomorphic to cnam and vnam *)
+axioms (* cnam_ and vnam_ are intended to be isomorphic to cnam and vnam *)
+
+  inj_cnam_:  "(cnam_ x = cnam_ y) = (x = y)"
+  inj_vnam_:  "(vnam_ x = vnam_ y) = (x = y)"
 
-  inj_cnam_  "(cnam_ x = cnam_ y) = (x = y)"
-  inj_vnam_  "(vnam_ x = vnam_ y) = (x = y)"
+  surj_cnam_: "\<exists>m. n = cnam_ m"
+  surj_vnam_: "\<exists>m. n = vnam_ m"
 
-  surj_cnam_ "\\<exists>m. n = cnam_ m"
-  surj_vnam_ "\\<exists>m. n = vnam_ m"
+declare inj_cnam_ [simp] inj_vnam_ [simp]
 
 syntax
 
-  Base,  Ext	:: cname
-  vee, x, e	:: vname
+  Base :: cname
+  Ext  :: cname
+  vee  :: vname
+  x    :: vname
+  e    :: vname
 
 translations
 
@@ -59,51 +64,323 @@
   "x"	 == "VName (vnam_ x_)"
   "e"	 == "VName (vnam_ e_)"
 
-rules
-  Base_not_Object "Base \\<noteq> Object"
-  Ext_not_Object  "Ext  \\<noteq> Object"
+axioms
+
+  Base_not_Object: "Base \<noteq> Object"
+  Ext_not_Object:  "Ext  \<noteq> Object"
+
+declare Base_not_Object [simp] Ext_not_Object [simp]
+declare Base_not_Object [THEN not_sym, simp] 
+declare Ext_not_Object  [THEN not_sym, simp]
 
 consts
 
-  foo_Base       :: java_mb
-  foo_Ext        :: java_mb
-  BaseC, ExtC    :: java_mb cdecl
-  test		 :: stmt
-  foo	         :: mname
-  a,b		 :: loc
+  foo_Base::  java_mb
+  foo_Ext ::  java_mb
+  BaseC   :: "java_mb cdecl"
+  ExtC    :: "java_mb cdecl"
+  test	  ::  stmt
+  foo	  ::  mname
+  a	  ::  loc
+  b       ::  loc
 
 defs
 
-  foo_Base_def "foo_Base == ([x],[],Skip,LAcc x)"
-  BaseC_def "BaseC == (Base, (Object, 
+  foo_Base_def:"foo_Base == ([x],[],Skip,LAcc x)"
+  BaseC_def:"BaseC == (Base, (Object, 
 			     [(vee, PrimT Boolean)], 
 			     [((foo,[Class Base]),Class Base,foo_Base)]))"
-  foo_Ext_def "foo_Ext == ([x],[],Expr( {Ext}Cast Ext
+  foo_Ext_def:"foo_Ext == ([x],[],Expr( {Ext}Cast Ext
 				       (LAcc x)..vee:=Lit (Intg #1)),
 				   Lit Null)"
-  ExtC_def  "ExtC  == (Ext,  (Base  , 
+  ExtC_def: "ExtC  == (Ext,  (Base  , 
 			     [(vee, PrimT Integer)], 
 			     [((foo,[Class Base]),Class Ext,foo_Ext)]))"
 
-  test_def "test == Expr(e::=NewC Ext);; 
+  test_def:"test == Expr(e::=NewC Ext);; 
                     Expr({Base}LAcc e..foo({[Class Base]}[Lit Null]))"
 
 
 syntax
 
-  NP		:: xcpt
-  tprg 	 	:: java_mb prog
-  obj1, obj2	:: obj
-  s0,s1,s2,s3,s4:: state
+  NP	:: xcpt
+  tprg 	::"java_mb prog"
+  obj1	:: obj
+  obj2	:: obj
+  s0 	:: state
+  s1 	:: state
+  s2 	:: state
+  s3 	:: state
+  s4 	:: state
 
 translations
 
   "NP"   == "NullPointer"
   "tprg" == "[ObjectC, BaseC, ExtC]"
-  "obj1"    <= "(Ext, empty((vee, Base)\\<mapsto>Bool False)
-			   ((vee, Ext )\\<mapsto>Intg #0))"
+  "obj1"    <= "(Ext, empty((vee, Base)\<mapsto>Bool False)
+			   ((vee, Ext )\<mapsto>Intg #0))"
   "s0" == " Norm    (empty, empty)"
-  "s1" == " Norm    (empty(a\\<mapsto>obj1),empty(e\\<mapsto>Addr a))"
-  "s2" == " Norm    (empty(a\\<mapsto>obj1),empty(x\\<mapsto>Null)(This\\<mapsto>Addr a))"
-  "s3" == "(Some NP, empty(a\\<mapsto>obj1),empty(e\\<mapsto>Addr a))"
+  "s1" == " Norm    (empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))"
+  "s2" == " Norm    (empty(a\<mapsto>obj1),empty(x\<mapsto>Null)(This\<mapsto>Addr a))"
+  "s3" == "(Some NP, empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))"
+
+
+ML {* bind_thm ("map_of_Cons", hd (tl (thms "map_of.simps"))) *}
+lemma map_of_Cons1 [simp]: "map_of ((aa,bb)#ps) aa = Some bb"
+apply (simp (no_asm))
+done
+lemma map_of_Cons2 [simp]: "aa\<noteq>k ==> map_of ((k,bb)#ps) aa = map_of ps aa"
+apply (simp (no_asm_simp))
+done
+declare map_of_Cons [simp del]; (* sic! *)
+
+lemma class_tprg_Object [simp]: "class tprg Object = Some (arbitrary, [], [])"
+apply (unfold ObjectC_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 (simp (no_asm))
+done
+
+lemma class_tprg_Ext [simp]: 
+"class tprg Ext = Some (Base,  
+	  [(vee, PrimT Integer)],  
+          [((foo, [Class Base]), Class Ext, foo_Ext)])"
+apply (unfold ObjectC_def BaseC_def ExtC_def class_def)
+apply (simp (no_asm))
+done
+
+lemma not_Object_subcls [elim!]: "(Object,C) \<in> (subcls1 tprg)^+ ==> R"
+apply (auto dest!: tranclD subcls1D)
+done
+
+lemma subcls_ObjectD [dest!]: "tprg\<turnstile>Object\<preceq>C C ==> C = Object"
+apply (erule rtrancl_induct)
+apply  auto
+apply (drule subcls1D)
+apply auto
+done
+
+lemma not_Base_subcls_Ext [elim!]: "(Base, Ext) \<in> (subcls1 tprg)^+ ==> R"
+apply (auto dest!: tranclD subcls1D)
+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)
+apply (auto split add: split_if_asm simp add: map_of_Cons)
+done
+
+lemma not_class_subcls_class [elim!]: "(C,C) \<in> (subcls1 tprg)^+ ==> R"
+apply (auto dest!: tranclD subcls1D)
+apply (frule class_tprgD)
+apply (auto dest!:)
+apply (drule rtranclD)
+apply auto
+done
+
+lemma unique_classes: "unique tprg"
+apply (simp (no_asm) add: ObjectC_def BaseC_def ExtC_def)
+done
+
+lemmas subcls_direct = subcls1I [THEN r_into_rtrancl]
+
+lemma Ext_subcls_Base [simp]: "tprg\<turnstile>Ext\<preceq>C Base"
+apply (rule subcls_direct)
+apply auto
+done
+
+lemma Ext_widen_Base [simp]: "tprg\<turnstile>Class Ext\<preceq> Class Base"
+apply (rule widen.subcls)
+apply (simp (no_asm))
+done
+
+declare ty_expr_ty_exprs_wt_stmt.intros [intro!]
+
+lemma acyclic_subcls1_: "acyclic (subcls1 tprg)"
+apply (rule acyclicI)
+apply safe
+done
+
+lemmas wf_subcls1_ = acyclic_subcls1_ [THEN finite_subcls1 [THEN finite_acyclic_wf_converse]]
+
+lemmas fields_rec_ = wf_subcls1_ [THEN [2] fields_rec_lemma]
+
+lemma fields_Object [simp]: "fields (tprg, Object) = []"
+apply (subst fields_rec_)
+apply   auto
+done
+
+declare is_class_def [simp]
+
+lemma fields_Base [simp]: "fields (tprg,Base) = [((vee, Base), PrimT Boolean)]"
+apply (subst fields_rec_)
+apply   auto
+done
+
+lemma fields_Ext [simp]: 
+  "fields (tprg, Ext)  = [((vee, Ext ), PrimT Integer)] @ fields (tprg, Base)"
+apply (rule trans)
+apply  (rule fields_rec_)
+apply   auto
+done
+
+lemmas method_rec_ = wf_subcls1_ [THEN [2] method_rec_lemma]
+
+lemma method_Object [simp]: "method (tprg,Object) = map_of []"
+apply (subst method_rec_)
+apply  auto
+done
+
+lemma method_Base [simp]: "method (tprg, Base) = map_of  
+  [((foo, [Class Base]), Base, (Class Base, foo_Base))]"
+apply (rule trans)
+apply  (rule method_rec_)
+apply  auto
+done
+
+lemma method_Ext [simp]: "method (tprg, Ext) = (method (tprg, Base) ++ map_of  
+  [((foo, [Class Base]), Ext , (Class Ext, foo_Ext))])"
+apply (rule trans)
+apply  (rule method_rec_)
+apply  auto
+done
+
+lemma wf_foo_Base: 
+"wf_mdecl wf_java_mdecl tprg Base ((foo, [Class Base]), (Class Base, foo_Base))"
+apply (unfold wf_mdecl_def wf_mhead_def wf_java_mdecl_def foo_Base_def)
+apply auto
+done
+
+lemma wf_foo_Ext: 
+"wf_mdecl wf_java_mdecl tprg Ext ((foo, [Class Base]), (Class Ext, foo_Ext))"
+apply (unfold wf_mdecl_def wf_mhead_def wf_java_mdecl_def foo_Ext_def)
+apply auto
+apply  (rule ty_expr_ty_exprs_wt_stmt.Cast)
+prefer 2
+apply   (simp)
+apply   (rule_tac [2] cast.subcls)
+apply   (unfold field_def)
+apply   auto
+done
+
+lemma wf_ObjectC: 
+"wf_cdecl wf_java_mdecl tprg ObjectC"
+apply (unfold wf_cdecl_def wf_fdecl_def ObjectC_def)
+apply (simp (no_asm))
+done
+
+lemma wf_BaseC: 
+"wf_cdecl wf_java_mdecl tprg BaseC"
+apply (unfold wf_cdecl_def wf_fdecl_def BaseC_def)
+apply (simp (no_asm))
+apply (fold BaseC_def)
+apply (rule wf_foo_Base [THEN conjI])
+apply auto
+done
+
+lemma wf_ExtC: 
+"wf_cdecl wf_java_mdecl tprg ExtC"
+apply (unfold wf_cdecl_def wf_fdecl_def ExtC_def)
+apply (simp (no_asm))
+apply (fold ExtC_def)
+apply (rule wf_foo_Ext [THEN conjI])
+apply auto
+apply (drule rtranclD)
+apply auto
+done
+
+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)
+done
+
+lemma appl_methds_foo_Base: 
+"appl_methds tprg Base (foo, [NT]) =  
+  {((Class Base, Class Base), [Class Base])}"
+apply (unfold appl_methds_def)
+apply (simp (no_asm))
+apply (subgoal_tac "tprg\<turnstile>NT\<preceq> Class Base")
+apply  (auto simp add: map_of_Cons foo_Base_def)
+done
+
+lemma max_spec_foo_Base: "max_spec tprg Base (foo, [NT]) =  
+  {((Class Base, Class Base), [Class Base])}"
+apply (unfold max_spec_def)
+apply (auto simp add: appl_methds_foo_Base)
+done
+
+ML {* fun t thm = resolve_tac (thms "ty_expr_ty_exprs_wt_stmt.intros") 1 thm *}
+lemma wt_test: "(tprg, empty(e\<mapsto>Class Base))\<turnstile>  
+  Expr(e::=NewC Ext);; Expr({Base}LAcc e..foo({?pTs'}[Lit Null]))\<surd>"
+apply (tactic t) (* ;; *)
+apply  (tactic t) (* Expr *)
+apply  (tactic t) (* LAss *)
+apply    (tactic t) (* LAcc *)
+apply     (simp (no_asm))
+apply    (simp (no_asm))
+apply   (tactic t) (* NewC *)
+apply   (simp (no_asm))
+apply  (simp (no_asm))
+apply (tactic t) (* Expr *)
+apply (tactic t) (* Call *)
+apply   (tactic t) (* LAcc *)
+apply    (simp (no_asm))
+apply   (simp (no_asm))
+apply  (tactic t) (* Cons *)
+apply   (tactic t) (* Lit *)
+apply   (simp (no_asm))
+apply  (tactic t) (* Nil *)
+apply (simp (no_asm))
+apply (rule max_spec_foo_Base)
+done
+
+ML {* fun e t = resolve_tac (thm "NewCI"::thms "eval_evals_exec.intros") 1 t *}
+
+declare split_if [split del]
+declare init_vars_def [simp] c_hupd_def [simp] cast_ok_def [simp]
+lemma exec_test: 
+" [|new_Addr (heap (snd s0)) = (a, None)|] ==>  
+  tprg\<turnstile>s0 -test-> ?s"
+apply (unfold test_def)
+(* ?s = s3 *)
+apply (tactic e) (* ;; *)
+apply  (tactic e) (* Expr *)
+apply  (tactic e) (* LAss *)
+apply   (tactic e) (* NewC *)
+apply    force
+apply   force
+apply  (simp (no_asm))
+apply (erule thin_rl)
+apply (tactic e) (* Expr *)
+apply (tactic e) (* Call *)
+apply       (tactic e) (* LAcc *)
+apply      force
+apply     (tactic e) (* Cons *)
+apply      (tactic e) (* Lit *)
+apply     (tactic e) (* Nil *)
+apply    (simp (no_asm))
+apply   (force simp add: foo_Ext_def)
+apply  (simp (no_asm))
+apply  (tactic e) (* Expr *)
+apply  (tactic e) (* FAss *)
+apply       (tactic e) (* Cast *)
+apply        (tactic e) (* LAcc *)
+apply       (simp (no_asm))
+apply      (simp (no_asm))
+apply     (simp (no_asm))
+apply     (tactic e) (* XcptE *)
+apply    (simp (no_asm))
+apply   (rule surjective_pairing [THEN sym, THEN[2]trans], subst Pair_eq, force)
+apply  (simp (no_asm))
+apply (simp (no_asm))
+apply (tactic e) (* XcptE *)
+done
+
 end




