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_: "\m. n = cnam_ m" + surj_vnam_: "\m. n = vnam_ m" - surj_cnam_ "\\m. n = cnam_ m" - surj_vnam_ "\\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 \\ Object" - Ext_not_Object "Ext \\ Object" +axioms + + Base_not_Object: "Base \ Object" + Ext_not_Object: "Ext \ 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)\\Bool False) - ((vee, Ext )\\Intg #0))" + "obj1" <= "(Ext, empty((vee, Base)\Bool False) + ((vee, Ext )\Intg #0))" "s0" == " Norm (empty, empty)" - "s1" == " Norm (empty(a\\obj1),empty(e\\Addr a))" - "s2" == " Norm (empty(a\\obj1),empty(x\\Null)(This\\Addr a))" - "s3" == "(Some NP, empty(a\\obj1),empty(e\\Addr a))" + "s1" == " Norm (empty(a\obj1),empty(e\Addr a))" + "s2" == " Norm (empty(a\obj1),empty(x\Null)(This\Addr a))" + "s3" == "(Some NP, empty(a\obj1),empty(e\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\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) \ (subcls1 tprg)^+ ==> R" +apply (auto dest!: tranclD subcls1D) +done + +lemma subcls_ObjectD [dest!]: "tprg\Object\C C ==> C = Object" +apply (erule rtrancl_induct) +apply auto +apply (drule subcls1D) +apply auto +done + +lemma not_Base_subcls_Ext [elim!]: "(Base, Ext) \ (subcls1 tprg)^+ ==> R" +apply (auto dest!: tranclD subcls1D) +done + +lemma class_tprgD: +"class tprg C = Some z ==> C=Object \ C=Base \ 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) \ (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\Ext\C Base" +apply (rule subcls_direct) +apply auto +done + +lemma Ext_widen_Base [simp]: "tprg\Class Ext\ 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\NT\ 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\Class Base))\ + Expr(e::=NewC Ext);; Expr({Base}LAcc e..foo({?pTs'}[Lit Null]))\" +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\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