
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 \<noteq> next_name"
Andreas@44037:   and distinct_vars:
Andreas@44037:   "l_nam \<noteq> l1_nam" "l_nam \<noteq> l2_nam" "l_nam \<noteq> l3_nam" "l_nam \<noteq> l4_nam"
Andreas@44037:   "l1_nam \<noteq> l2_nam" "l1_nam \<noteq> l3_nam" "l1_nam \<noteq> l4_nam"
Andreas@44037:   "l2_nam \<noteq> l3_nam" "l2_nam \<noteq> l4_nam"
Andreas@44037:   "l3_nam \<noteq> 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 \<longleftrightarrow> 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 \<longleftrightarrow> 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 \<longleftrightarrow> True"
Andreas@44037:   "HOL.equal next_nam next_nam \<longleftrightarrow> True"
Andreas@44037:   "HOL.equal l_nam l_nam \<longleftrightarrow> True"
Andreas@44037:   "HOL.equal l1_nam l1_nam \<longleftrightarrow> True"
Andreas@44037:   "HOL.equal l2_nam l2_nam \<longleftrightarrow> True"
Andreas@44037:   "HOL.equal l3_nam l3_nam \<longleftrightarrow> True"
Andreas@44037:   "HOL.equal l4_nam l4_nam \<longleftrightarrow> True"
Andreas@44037: 
Andreas@44037:   "HOL.equal val_nam next_nam \<longleftrightarrow> False"
Andreas@44037:   "HOL.equal next_nam val_nam \<longleftrightarrow> False"
berghofe@12442: 
Andreas@44037:   "HOL.equal l_nam l1_nam \<longleftrightarrow> False"
Andreas@44037:   "HOL.equal l_nam l2_nam \<longleftrightarrow> False"
Andreas@44037:   "HOL.equal l_nam l3_nam \<longleftrightarrow> False"
Andreas@44037:   "HOL.equal l_nam l4_nam \<longleftrightarrow> False"
Andreas@44037: 
Andreas@44037:   "HOL.equal l1_nam l_nam \<longleftrightarrow> False"
Andreas@44037:   "HOL.equal l1_nam l2_nam \<longleftrightarrow> False"
Andreas@44037:   "HOL.equal l1_nam l3_nam \<longleftrightarrow> False"
Andreas@44037:   "HOL.equal l1_nam l4_nam \<longleftrightarrow> False"
Andreas@44037: 
Andreas@44037:   "HOL.equal l2_nam l_nam \<longleftrightarrow> False"
Andreas@44037:   "HOL.equal l2_nam l1_nam \<longleftrightarrow> False"
Andreas@44037:   "HOL.equal l2_nam l3_nam \<longleftrightarrow> False"
Andreas@44037:   "HOL.equal l2_nam l4_nam \<longleftrightarrow> False"
berghofe@12442: 
Andreas@44037:   "HOL.equal l3_nam l_nam \<longleftrightarrow> False"
Andreas@44037:   "HOL.equal l3_nam l1_nam \<longleftrightarrow> False"
Andreas@44037:   "HOL.equal l3_nam l2_nam \<longleftrightarrow> False"
Andreas@44037:   "HOL.equal l3_nam l4_nam \<longleftrightarrow> False"
Andreas@44037: 
Andreas@44037:   "HOL.equal l4_nam l_nam \<longleftrightarrow> False"
Andreas@44037:   "HOL.equal l4_nam l1_nam \<longleftrightarrow> False"
Andreas@44037:   "HOL.equal l4_nam l2_nam \<longleftrightarrow> False"
Andreas@44037:   "HOL.equal l4_nam l3_nam \<longleftrightarrow> 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' \<longleftrightarrow> l = l'"
wenzelm@45827: 
Andreas@44037: lemma equal_loc'_code [code]:
Andreas@44037:   "HOL.equal (nat_to_loc' l) (nat_to_loc' l') \<longleftrightarrow> 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 (\<lambda>s. example_prg\<turnstile>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




