--- 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