kleing@12951: (* Title: HOL/MicroJava/J/JListExample.thy berghofe@12442: Author: Stefan Berghofer berghofe@12442: *) berghofe@12442: kleing@12911: header {* \isaheader{Example for generating executable code from Java semantics} *} berghofe@12442: haftmann@28524: theory JListExample haftmann@32356: imports Eval haftmann@28524: begin berghofe@12442: wenzelm@46512: declare [[syntax_ambiguity_warning = false]] berghofe@12442: berghofe@12442: consts Andreas@44037: list_nam :: cnam berghofe@12442: append_name :: mname Andreas@44037: Andreas@44037: axiomatization val_nam next_nam l_nam l1_nam l2_nam l3_nam l4_nam :: vnam Andreas@44037: where distinct_fields: "val_name \ next_name" Andreas@44037: and distinct_vars: Andreas@44037: "l_nam \ l1_nam" "l_nam \ l2_nam" "l_nam \ l3_nam" "l_nam \ l4_nam" Andreas@44037: "l1_nam \ l2_nam" "l1_nam \ l3_nam" "l1_nam \ l4_nam" Andreas@44037: "l2_nam \ l3_nam" "l2_nam \ l4_nam" Andreas@44037: "l3_nam \ l4_nam" Andreas@44037: Andreas@44037: definition list_name :: cname where Andreas@44037: "list_name = Cname list_nam" berghofe@12442: haftmann@35416: definition val_name :: vname where berghofe@12442: "val_name == VName val_nam" berghofe@12442: haftmann@35416: definition next_name :: vname where berghofe@12442: "next_name == VName next_nam" berghofe@12442: haftmann@35416: definition l_name :: vname where berghofe@12442: "l_name == VName l_nam" berghofe@12442: haftmann@35416: definition l1_name :: vname where berghofe@12442: "l1_name == VName l1_nam" berghofe@12442: haftmann@35416: definition l2_name :: vname where berghofe@12442: "l2_name == VName l2_nam" berghofe@12442: haftmann@35416: definition l3_name :: vname where berghofe@12442: "l3_name == VName l3_nam" berghofe@12442: haftmann@35416: definition l4_name :: vname where berghofe@12442: "l4_name == VName l4_nam" berghofe@12442: haftmann@35416: definition list_class :: "java_mb class" where berghofe@12442: "list_class == berghofe@12442: (Object, berghofe@12442: [(val_name, PrimT Integer), (next_name, RefT (ClassT list_name))], berghofe@12442: [((append_name, [RefT (ClassT list_name)]), PrimT Void, berghofe@12442: ([l_name], [], berghofe@12442: If(BinOp Eq ({list_name}(LAcc This)..next_name) (Lit Null)) berghofe@12442: Expr ({list_name}(LAcc This)..next_name:=LAcc l_name) berghofe@12442: Else berghofe@12442: Expr ({list_name}({list_name}(LAcc This)..next_name).. berghofe@12442: append_name({[RefT (ClassT list_name)]}[LAcc l_name])), berghofe@12442: Lit Unit))])" berghofe@12442: haftmann@35416: definition example_prg :: "java_mb prog" where berghofe@12442: "example_prg == [ObjectC, (list_name, list_class)]" berghofe@12442: Andreas@44037: code_datatype list_nam Andreas@44037: lemma equal_cnam_code [code]: Andreas@44037: "HOL.equal list_nam list_nam \ True" Andreas@44037: by(simp add: equal_cnam_def) Andreas@44037: Andreas@44037: code_datatype append_name Andreas@44037: lemma equal_mname_code [code]: Andreas@44037: "HOL.equal append_name append_name \ True" Andreas@44037: by(simp add: equal_mname_def) berghofe@12442: Andreas@44037: code_datatype val_nam next_nam l_nam l1_nam l2_nam l3_nam l4_nam Andreas@44037: lemma equal_vnam_code [code]: Andreas@44037: "HOL.equal val_nam val_nam \ True" Andreas@44037: "HOL.equal next_nam next_nam \ True" Andreas@44037: "HOL.equal l_nam l_nam \ True" Andreas@44037: "HOL.equal l1_nam l1_nam \ True" Andreas@44037: "HOL.equal l2_nam l2_nam \ True" Andreas@44037: "HOL.equal l3_nam l3_nam \ True" Andreas@44037: "HOL.equal l4_nam l4_nam \ True" Andreas@44037: Andreas@44037: "HOL.equal val_nam next_nam \ False" Andreas@44037: "HOL.equal next_nam val_nam \ False" berghofe@12442: Andreas@44037: "HOL.equal l_nam l1_nam \ False" Andreas@44037: "HOL.equal l_nam l2_nam \ False" Andreas@44037: "HOL.equal l_nam l3_nam \ False" Andreas@44037: "HOL.equal l_nam l4_nam \ False" Andreas@44037: Andreas@44037: "HOL.equal l1_nam l_nam \ False" Andreas@44037: "HOL.equal l1_nam l2_nam \ False" Andreas@44037: "HOL.equal l1_nam l3_nam \ False" Andreas@44037: "HOL.equal l1_nam l4_nam \ False" Andreas@44037: Andreas@44037: "HOL.equal l2_nam l_nam \ False" Andreas@44037: "HOL.equal l2_nam l1_nam \ False" Andreas@44037: "HOL.equal l2_nam l3_nam \ False" Andreas@44037: "HOL.equal l2_nam l4_nam \ False" berghofe@12442: Andreas@44037: "HOL.equal l3_nam l_nam \ False" Andreas@44037: "HOL.equal l3_nam l1_nam \ False" Andreas@44037: "HOL.equal l3_nam l2_nam \ False" Andreas@44037: "HOL.equal l3_nam l4_nam \ False" Andreas@44037: Andreas@44037: "HOL.equal l4_nam l_nam \ False" Andreas@44037: "HOL.equal l4_nam l1_nam \ False" Andreas@44037: "HOL.equal l4_nam l2_nam \ False" Andreas@44037: "HOL.equal l4_nam l3_nam \ False" Andreas@44037: by(simp_all add: distinct_fields distinct_fields[symmetric] distinct_vars distinct_vars[symmetric] equal_vnam_def) Andreas@44037: wenzelm@45827: axiomatization where wenzelm@45827: nat_to_loc'_inject: "nat_to_loc' l = nat_to_loc' l' \ l = l'" wenzelm@45827: Andreas@44037: lemma equal_loc'_code [code]: Andreas@44037: "HOL.equal (nat_to_loc' l) (nat_to_loc' l') \ l = l'" Andreas@44037: by(simp add: equal_loc'_def nat_to_loc'_inject) berghofe@12442: Andreas@44037: definition undefined_cname :: cname Andreas@44037: where [code del]: "undefined_cname = undefined" bulwahn@45231: declare undefined_cname_def[symmetric, code_unfold] Andreas@44037: code_datatype Object Xcpt Cname undefined_cname Andreas@44037: Andreas@44037: definition undefined_val :: val Andreas@44037: where [code del]: "undefined_val = undefined" bulwahn@45231: declare undefined_val_def[symmetric, code_unfold] Andreas@44037: code_datatype Unit Null Bool Intg Addr undefined_val Andreas@44037: Andreas@44037: definition E where Andreas@44037: "E = Expr (l1_name::=NewC list_name);; Andreas@44037: Expr ({list_name}(LAcc l1_name)..val_name:=Lit (Intg 1));; Andreas@44037: Expr (l2_name::=NewC list_name);; Andreas@44037: Expr ({list_name}(LAcc l2_name)..val_name:=Lit (Intg 2));; Andreas@44037: Expr (l3_name::=NewC list_name);; Andreas@44037: Expr ({list_name}(LAcc l3_name)..val_name:=Lit (Intg 3));; Andreas@44037: Expr (l4_name::=NewC list_name);; Andreas@44037: Expr ({list_name}(LAcc l4_name)..val_name:=Lit (Intg 4));; Andreas@44037: Expr ({list_name}(LAcc l1_name).. Andreas@44037: append_name({[RefT (ClassT list_name)]}[LAcc l2_name]));; Andreas@44037: Expr ({list_name}(LAcc l1_name).. Andreas@44037: append_name({[RefT (ClassT list_name)]}[LAcc l3_name]));; Andreas@44037: Expr ({list_name}(LAcc l1_name).. Andreas@44037: append_name({[RefT (ClassT list_name)]}[LAcc l4_name]))" Andreas@44037: Andreas@44037: definition test where Andreas@44037: "test = Predicate.Pred (\s. example_prg\Norm (empty, empty) -E-> s)" berghofe@12442: Andreas@44037: lemma test_code [code]: Andreas@44037: "test = exec_i_i_i_o example_prg (Norm (empty, empty)) E" Andreas@44037: by(auto intro: exec_i_i_i_oI intro!: pred_eqI elim: exec_i_i_i_oE simp add: test_def) berghofe@12442: Andreas@44037: ML {* Andreas@44037: val SOME ((_, (heap, locs)), _) = Predicate.yield @{code test}; Andreas@44037: locs @{code l1_name}; Andreas@44037: locs @{code l2_name}; Andreas@44037: locs @{code l3_name}; Andreas@44037: locs @{code l4_name}; berghofe@12442: Andreas@44037: fun list_fields n = Andreas@44037: @{code snd} (@{code the} (heap (@{code Loc} (@{code "nat_to_loc'"} n)))); Andreas@44037: fun val_field n = Andreas@44037: list_fields n (@{code val_name}, @{code "list_name"}); Andreas@44037: fun next_field n = Andreas@44037: list_fields n (@{code next_name}, @{code "list_name"}); Andreas@44037: val Suc = @{code Suc}; berghofe@12442: Andreas@44037: val_field @{code "0 :: nat"}; Andreas@44037: next_field @{code "0 :: nat"}; Andreas@44037: Andreas@44037: val_field @{code "1 :: nat"}; Andreas@44037: next_field @{code "1 :: nat"}; Andreas@44037: Andreas@44037: val_field (Suc (Suc @{code "0 :: nat"})); Andreas@44037: next_field (Suc (Suc @{code "0 :: nat"})); Andreas@44037: Andreas@44037: val_field (Suc (Suc (Suc @{code "0 :: nat"}))); Andreas@44037: next_field (Suc (Suc (Suc @{code "0 :: nat"}))); berghofe@12442: *} berghofe@12442: berghofe@12442: end