# HG changeset patch
# User Andreas Lochbihler
# Date 1312546604 -7200
# Node ID 322d1657c40c0083db4d053ff92930b7f74290b4
# Parent  53a081c8873d6936cb6c6ed46301f285ac1b7497
replace old SML code generator by new code generator in MicroJava/JVM and /BV

diff -r 53a081c8873d -r 322d1657c40c src/HOL/MicroJava/BV/BVExample.thy
--- a/src/HOL/MicroJava/BV/BVExample.thy	Fri Aug 05 00:14:08 2011 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Fri Aug 05 14:16:44 2011 +0200
@@ -21,13 +21,6 @@
 *}
 
 section "Setup"
-text {*
-  Since the types @{typ cnam}, @{text vnam}, and @{text mname} are 
-  anonymous, we describe distinctness of names in the example by axioms:
-*}
-axioms 
-  distinct_classes: "list_nam \<noteq> test_nam"
-  distinct_fields:  "val_nam \<noteq> next_nam"
 
 text {* Abbreviations for definitions we will have to use often in the
 proofs below: *}
@@ -415,35 +408,45 @@
     in  kiljvm G mxs (1+size pTs+mxl) rT et instr start)"
 
 lemma [code]:
-  "unstables r step ss = (UN p:{..<size ss}. if \<not>stable r step ss p then {p} else {})"
-  apply (unfold unstables_def)
-  apply (rule equalityI)
-  apply (rule subsetI)
-  apply (erule CollectE)
-  apply (erule conjE)
-  apply (rule UN_I)
-  apply simp
-  apply simp
-  apply (rule subsetI)
-  apply (erule UN_E)
-  apply (case_tac "\<not> stable r step ss p")
-  apply simp+
-  done
+  "unstables r step ss = 
+   foldr (\<lambda>p A. if \<not>stable r step ss p then insert p A else A) [0..<size ss] {}"
+proof -
+  have "unstables r step ss = (UN p:{..<size ss}. if \<not>stable r step ss p then {p} else {})"
+    apply (unfold unstables_def)
+    apply (rule equalityI)
+    apply (rule subsetI)
+    apply (erule CollectE)
+    apply (erule conjE)
+    apply (rule UN_I)
+    apply simp
+    apply simp
+    apply (rule subsetI)
+    apply (erule UN_E)
+    apply (case_tac "\<not> stable r step ss p")
+    apply simp+
+    done
+  also have "\<And>f. (UN p:{..<size ss}. f p) = Union (set (map f [0..<size ss]))" by auto
+  also note Sup_set_foldr also note foldr_map
+  also have "op \<union> \<circ> (\<lambda>p. if \<not> stable r step ss p then {p} else {}) = 
+            (\<lambda>p A. if \<not>stable r step ss p then insert p A else A)"
+    by(auto simp add: fun_eq_iff)
+  finally show ?thesis .
+qed
 
-definition some_elem :: "'a set \<Rightarrow> 'a" where
+definition some_elem :: "'a set \<Rightarrow> 'a" where [code del]:
   "some_elem = (%S. SOME x. x : S)"
-
-consts_code
-  "some_elem" ("(case/ _ of/ {*Set*}/ xs/ =>/ hd/ xs)")
+code_const some_elem
+  (SML "(case/ _ of/ Set/ xs/ =>/ hd/ xs)")
+setup {* Code.add_signature_cmd ("some_elem", "'a set \<Rightarrow> 'a") *}
 
 text {* This code setup is just a demonstration and \emph{not} sound! *}
 
 lemma False
 proof -
   have "some_elem (set [False, True]) = False"
-    by evaluation
+    by eval
   moreover have "some_elem (set [True, False]) = True"
-    by evaluation
+    by eval
   ultimately show False
     by (simp add: some_elem_def)
 qed
@@ -465,15 +468,35 @@
   by simp
 
 lemmas [code] = JType.sup_def [unfolded exec_lub_def] JVM_le_unfold
+lemmas [code] = lesub_def plussub_def
 
-lemmas [code_ind] = rtranclp.rtrancl_refl converse_rtranclp_into_rtranclp
+setup {*
+  Code.add_signature_cmd ("More_Set.is_empty", "'a set \<Rightarrow> bool")
+  #> Code.add_signature_cmd ("propa", "('s \<Rightarrow> 's \<Rightarrow> 's) \<Rightarrow> (nat \<times> 's) list \<Rightarrow> 's list \<Rightarrow> nat set \<Rightarrow> 's list * nat set") 
+  #> Code.add_signature_cmd 
+     ("iter", "('s \<Rightarrow> 's \<Rightarrow> 's) \<Rightarrow> (nat \<Rightarrow> 's \<Rightarrow> (nat \<times> 's) list) \<Rightarrow> 's list \<Rightarrow> nat set \<Rightarrow> 's list * nat set")
+  #> Code.add_signature_cmd ("unstables", "('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> (nat \<Rightarrow> 's \<Rightarrow> (nat \<times> 's) list) \<Rightarrow> 's list \<Rightarrow> nat set") 
+*}
+
+definition [code del]: "mem2 = op :"
+lemma [code]: "mem2 x A = A x"
+  by(simp add: mem2_def mem_def)
 
-code_module BV
-contains
-  test1 = "test_kil E list_name [Class list_name] (PrimT Void) 3 0
+lemmas [folded mem2_def, code] =
+  JType.sup_def[unfolded exec_lub_def]
+  wf_class_code
+  widen.equation
+  match_exception_entry_def
+
+definition test1 where
+  "test1 = test_kil E list_name [Class list_name] (PrimT Void) 3 0
     [(Suc 0, 2, 8, Xcpt NullPointer)] append_ins"
-  test2 = "test_kil E test_name [] (PrimT Void) 3 2 [] make_list_ins"
-ML BV.test1
-ML BV.test2
+definition test2 where
+  "test2 = test_kil E test_name [] (PrimT Void) 3 2 [] make_list_ins"
+
+ML {* 
+  @{code test1}; 
+  @{code test2};
+*}
 
 end
diff -r 53a081c8873d -r 322d1657c40c src/HOL/MicroJava/J/JBasis.thy
--- a/src/HOL/MicroJava/J/JBasis.thy	Fri Aug 05 00:14:08 2011 +0200
+++ b/src/HOL/MicroJava/J/JBasis.thy	Fri Aug 05 14:16:44 2011 +0200
@@ -7,7 +7,7 @@
   \isaheader{Some Auxiliary Definitions}
 *}
 
-theory JBasis imports Main begin 
+theory JBasis imports Main "~~/src/HOL/Library/Transitive_Closure_Table" begin 
 
 lemmas [simp] = Let_def
 
diff -r 53a081c8873d -r 322d1657c40c src/HOL/MicroJava/J/State.thy
--- a/src/HOL/MicroJava/J/State.thy	Fri Aug 05 00:14:08 2011 +0200
+++ b/src/HOL/MicroJava/J/State.thy	Fri Aug 05 14:16:44 2011 +0200
@@ -52,8 +52,18 @@
 definition raise_if :: "bool \<Rightarrow> xcpt \<Rightarrow> val option \<Rightarrow> val option" where
   "raise_if b x xo \<equiv> if b \<and>  (xo = None) then Some (Addr (XcptRef x)) else xo"
 
+text {* Make new_Addr completely specified (at least for the code generator) *}
+(*
 definition new_Addr  :: "aheap => loc \<times> val option" where
   "new_Addr h \<equiv> SOME (a,x). (h a = None \<and>  x = None) |  x = Some (Addr (XcptRef OutOfMemory))"
+*)
+consts nat_to_loc' :: "nat => loc'"
+code_datatype nat_to_loc'
+definition new_Addr  :: "aheap => loc \<times> val option" where
+  "new_Addr h \<equiv> 
+   if \<exists>n. h (Loc (nat_to_loc' n)) = None 
+   then (Loc (nat_to_loc' (LEAST n. h (Loc (nat_to_loc' n)) = None)), None)
+   else (Loc (nat_to_loc' 0), Some (Addr (XcptRef OutOfMemory)))"
 
 definition np    :: "val => val option => val option" where
  "np v == raise_if (v = Null) NullPointer"
@@ -74,11 +84,8 @@
   hp ref = None \<and> xcp = None \<or> xcp = Some (Addr (XcptRef OutOfMemory))"
 apply (drule sym)
 apply (unfold new_Addr_def)
-apply(simp add: Pair_fst_snd_eq Eps_split)
-apply(rule someI)
-apply(rule disjI2)
-apply(rule_tac r = "snd (?a,Some (Addr (XcptRef OutOfMemory)))" in trans)
-apply auto
+apply (simp split: split_if_asm)
+apply (erule LeastI)
 done
 
 lemma raise_if_True [simp]: "raise_if True x y \<noteq> None"
@@ -150,4 +157,42 @@
 lemma c_hupd_fst [simp]: "fst (c_hupd h (x, s)) = x"
 by (simp add: c_hupd_def split_beta)
 
+text {* Naive implementation for @{term "new_Addr"} by exhaustive search *}
+
+definition gen_new_Addr :: "aheap => nat \<Rightarrow> loc \<times> val option" where
+  "gen_new_Addr h n \<equiv> 
+   if \<exists>a. a \<ge> n \<and> h (Loc (nat_to_loc' a)) = None 
+   then (Loc (nat_to_loc' (LEAST a. a \<ge> n \<and> h (Loc (nat_to_loc' a)) = None)), None)
+   else (Loc (nat_to_loc' 0), Some (Addr (XcptRef OutOfMemory)))"
+
+lemma new_Addr_code_code [code]:
+  "new_Addr h = gen_new_Addr h 0"
+by(simp only: new_Addr_def gen_new_Addr_def split: split_if) simp
+
+lemma gen_new_Addr_code [code]:
+  "gen_new_Addr h n = (if h (Loc (nat_to_loc' n)) = None then (Loc (nat_to_loc' n), None) else gen_new_Addr h (Suc n))"
+apply(simp add: gen_new_Addr_def)
+apply(rule impI)
+apply(rule conjI)
+ apply safe[1]
+  apply(auto intro: arg_cong[where f=nat_to_loc'] Least_equality)[1]
+ apply(rule arg_cong[where f=nat_to_loc'])
+ apply(rule arg_cong[where f=Least])
+ apply(rule ext)
+ apply(safe, simp_all)[1]
+ apply(rename_tac "n'")
+ apply(case_tac "n = n'", simp_all)[1]
+apply clarify
+apply(subgoal_tac "a = n")
+ apply(auto intro: Least_equality arg_cong[where f=nat_to_loc'])[1]
+apply(rule ccontr)
+apply(erule_tac x="a" in allE)
+apply simp
+done
+
+instantiation loc' :: equal begin
+definition "HOL.equal (l :: loc') l' \<longleftrightarrow> l = l'"
+instance proof qed(simp add: equal_loc'_def)
 end
+
+end
diff -r 53a081c8873d -r 322d1657c40c src/HOL/MicroJava/J/SystemClasses.thy
--- a/src/HOL/MicroJava/J/SystemClasses.thy	Fri Aug 05 00:14:08 2011 +0200
+++ b/src/HOL/MicroJava/J/SystemClasses.thy	Fri Aug 05 14:16:44 2011 +0200
@@ -13,18 +13,18 @@
 *}
 
 definition ObjectC :: "'c cdecl" where
-  "ObjectC \<equiv> (Object, (undefined,[],[]))"
+  [code_inline]: "ObjectC \<equiv> (Object, (undefined,[],[]))"
 
 definition NullPointerC :: "'c cdecl" where
-  "NullPointerC \<equiv> (Xcpt NullPointer, (Object,[],[]))"
+  [code_inline]: "NullPointerC \<equiv> (Xcpt NullPointer, (Object,[],[]))"
 
 definition ClassCastC :: "'c cdecl" where
-  "ClassCastC \<equiv> (Xcpt ClassCast, (Object,[],[]))"
+  [code_inline]: "ClassCastC \<equiv> (Xcpt ClassCast, (Object,[],[]))"
 
 definition OutOfMemoryC :: "'c cdecl" where
-  "OutOfMemoryC \<equiv> (Xcpt OutOfMemory, (Object,[],[]))"
+  [code_inline]: "OutOfMemoryC \<equiv> (Xcpt OutOfMemory, (Object,[],[]))"
 
 definition SystemClasses :: "'c cdecl list" where
-  "SystemClasses \<equiv> [ObjectC, NullPointerC, ClassCastC, OutOfMemoryC]"
+  [code_inline]: "SystemClasses \<equiv> [ObjectC, NullPointerC, ClassCastC, OutOfMemoryC]"
 
 end
diff -r 53a081c8873d -r 322d1657c40c src/HOL/MicroJava/J/Type.thy
--- a/src/HOL/MicroJava/J/Type.thy	Fri Aug 05 00:14:08 2011 +0200
+++ b/src/HOL/MicroJava/J/Type.thy	Fri Aug 05 14:16:44 2011 +0200
@@ -8,6 +8,10 @@
 theory Type imports JBasis begin
 
 typedecl cnam 
+instantiation cnam :: equal begin
+definition "HOL.equal (cn :: cnam) cn' \<longleftrightarrow> cn = cn'"
+instance proof qed(simp add: equal_cnam_def)
+end
 
  -- "exceptions"
 datatype 
@@ -23,7 +27,16 @@
   | Cname cnam 
 
 typedecl vnam   -- "variable or field name"
+instantiation vnam :: equal begin
+definition "HOL.equal (vn :: vnam) vn' \<longleftrightarrow> vn = vn'"
+instance proof qed(simp add: equal_vnam_def)
+end
+
 typedecl mname  -- "method name"
+instantiation mname :: equal begin
+definition "HOL.equal (M :: mname) M' \<longleftrightarrow> M = M'"
+instance proof qed(simp add: equal_mname_def)
+end
 
 -- "names for @{text This} pointer and local/field variables"
 datatype vname 
diff -r 53a081c8873d -r 322d1657c40c src/HOL/MicroJava/J/TypeRel.thy
--- a/src/HOL/MicroJava/J/TypeRel.thy	Fri Aug 05 00:14:08 2011 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.thy	Fri Aug 05 14:16:44 2011 +0200
@@ -77,22 +77,112 @@
   "wf_class G = wf ((subcls1 G)^-1)"
 
 
-text {* Code generator setup (FIXME!) *}
+
+text {* Code generator setup *}
+
+code_pred 
+  (modes: i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool, i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool)
+  subcls1p 
+  .
+declare subcls1_def[unfolded Collect_def, code_pred_def]
+code_pred 
+  (modes: i \<Rightarrow> i \<times> o \<Rightarrow> bool, i \<Rightarrow> i \<times> i \<Rightarrow> bool)
+  [inductify]
+  subcls1 
+  .
+
+definition subcls' where "subcls' G = (subcls1p G)^**"
+code_pred
+  (modes: i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool, i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool)
+  [inductify]
+  subcls'
+.
+lemma subcls_conv_subcls' [code_inline]:
+  "(subcls1 G)^* = (\<lambda>(C, D). subcls' G C D)"
+by(simp add: subcls'_def subcls1_def rtrancl_def)(simp add: Collect_def)
+
+lemma class_rec_code [code]:
+  "class_rec G C t f = 
+  (if wf_class G then 
+    (case class G C of
+       None \<Rightarrow> class_rec G C t f
+     | Some (D, fs, ms) \<Rightarrow> 
+       if C = Object then f Object fs ms t else f C fs ms (class_rec G D t f))
+   else class_rec G C t f)"
+apply(cases "wf_class G")
+ apply(unfold class_rec_def wf_class_def)
+ apply(subst wfrec, assumption)
+ apply(cases "class G C")
+  apply(simp add: wfrec)
+ apply clarsimp
+ apply(rename_tac D fs ms)
+ apply(rule_tac f="f C fs ms" in arg_cong)
+ apply(clarsimp simp add: cut_def)
+ apply(blast intro: subcls1I)
+apply simp
+done
 
-consts_code
-  "wfrec"   ("\<module>wfrec?")
-attach {*
-fun wfrec f x = f (wfrec f) x;
-*}
+lemma wf_class_code [code]:
+  "wf_class G \<longleftrightarrow> (\<forall>(C, rest) \<in> set G. C \<noteq> Object \<longrightarrow> \<not> G \<turnstile> fst (the (class G C)) \<preceq>C C)"
+proof
+  assume "wf_class G"
+  hence wf: "wf (((subcls1 G)^+)^-1)" unfolding wf_class_def by(rule wf_converse_trancl)
+  hence acyc: "acyclic ((subcls1 G)^+)" by(auto dest: wf_acyclic)
+  show "\<forall>(C, rest) \<in> set G. C \<noteq> Object \<longrightarrow> \<not> G \<turnstile> fst (the (class G C)) \<preceq>C C"
+  proof(safe)
+    fix C D fs ms
+    assume "(C, D, fs, ms) \<in> set G"
+      and "C \<noteq> Object"
+      and subcls: "G \<turnstile> fst (the (class G C)) \<preceq>C C"
+    from `(C, D, fs, ms) \<in> set G` obtain D' fs' ms'
+      where "class": "class G C = Some (D', fs', ms')"
+      unfolding class_def by(auto dest!: weak_map_of_SomeI)
+    hence "G \<turnstile> C \<prec>C1 D'" using `C \<noteq> Object` ..
+    hence "(C, D') \<in> (subcls1 G)^+" ..
+    also with acyc have "C \<noteq> D'" by(auto simp add: acyclic_def)
+    with subcls "class" have "(D', C) \<in> (subcls1 G)^+" by(auto dest: rtranclD)
+    finally show False using acyc by(auto simp add: acyclic_def)
+  qed
+next
+  assume rhs[rule_format]: "\<forall>(C, rest) \<in> set G. C \<noteq> Object \<longrightarrow> \<not> G \<turnstile> fst (the (class G C)) \<preceq>C C"
+  have "acyclic (subcls1 G)"
+  proof(intro acyclicI strip notI)
+    fix C
+    assume "(C, C) \<in> (subcls1 G)\<^sup>+"
+    thus False
+    proof(cases)
+      case base
+      then obtain rest where "class G C = Some (C, rest)"
+        and "C \<noteq> Object" by cases
+      from `class G C = Some (C, rest)` have "(C, C, rest) \<in> set G"
+        unfolding class_def by(rule map_of_SomeD)
+      with `C \<noteq> Object` `class G C = Some (C, rest)`
+      have "\<not> G \<turnstile> C \<preceq>C C" by(auto dest: rhs)
+      thus False by simp
+    next
+      case (step D)
+      from `G \<turnstile> D \<prec>C1 C` obtain rest where "class G D = Some (C, rest)"
+        and "D \<noteq> Object" by cases
+      from `class G D = Some (C, rest)` have "(D, C, rest) \<in> set G"
+        unfolding class_def by(rule map_of_SomeD)
+      with `D \<noteq> Object` `class G D = Some (C, rest)`
+      have "\<not> G \<turnstile> C \<preceq>C D" by(auto dest: rhs)
+      moreover from `(C, D) \<in> (subcls1 G)\<^sup>+`
+      have "G \<turnstile> C \<preceq>C D" by(rule trancl_into_rtrancl)
+      ultimately show False by contradiction
+    qed
+  qed
+  thus "wf_class G" unfolding wf_class_def
+    by(rule finite_acyclic_wf_converse[OF finite_subcls1])
+qed
 
 consts
-
   method :: "'c prog \<times> cname => ( sig   \<rightharpoonup> cname \<times> ty \<times> 'c)" (* ###curry *)
   field  :: "'c prog \<times> cname => ( vname \<rightharpoonup> cname \<times> ty     )" (* ###curry *)
   fields :: "'c prog \<times> cname => ((vname \<times> cname) \<times> ty) list" (* ###curry *)
 
 -- "methods of a class, with inheritance, overriding and hiding, cf. 8.4.6"
-defs method_def: "method \<equiv> \<lambda>(G,C). class_rec G C empty (\<lambda>C fs ms ts.
+defs method_def [code]: "method \<equiv> \<lambda>(G,C). class_rec G C empty (\<lambda>C fs ms ts.
                            ts ++ map_of (map (\<lambda>(s,m). (s,(C,m))) ms))"
 
 lemma method_rec_lemma: "[|class G C = Some (D,fs,ms); wf ((subcls1 G)^-1)|] ==>
@@ -106,7 +196,7 @@
 
 
 -- "list of fields of a class, including inherited and hidden ones"
-defs fields_def: "fields \<equiv> \<lambda>(G,C). class_rec G C []    (\<lambda>C fs ms ts.
+defs fields_def [code]: "fields \<equiv> \<lambda>(G,C). class_rec G C []    (\<lambda>C fs ms ts.
                            map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ ts)"
 
 lemma fields_rec_lemma: "[|class G C = Some (D,fs,ms); wf ((subcls1 G)^-1)|] ==>
@@ -119,7 +209,7 @@
 done
 
 
-defs field_def: "field == map_of o (map (\<lambda>((fn,fd),ft). (fn,(fd,ft)))) o fields"
+defs field_def [code]: "field == map_of o (map (\<lambda>((fn,fd),ft). (fn,(fd,ft)))) o fields"
 
 lemma field_fields: 
 "field (G,C) fn = Some (fd, fT) \<Longrightarrow> map_of (fields (G,C)) (fn, fd) = Some fT"
@@ -138,6 +228,8 @@
 | subcls         : "G\<turnstile>C\<preceq>C D ==> G\<turnstile>Class C \<preceq> Class D"
 | null   [intro!]:             "G\<turnstile>     NT \<preceq> RefT R"
 
+code_pred widen .
+
 lemmas refl = HOL.refl
 
 -- "casting conversion, cf. 5.5 / 5.1.5"
diff -r 53a081c8873d -r 322d1657c40c src/HOL/MicroJava/JVM/JVMListExample.thy
--- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Fri Aug 05 00:14:08 2011 +0200
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Fri Aug 05 14:16:44 2011 +0200
@@ -8,13 +8,20 @@
 imports "../J/SystemClasses" JVMExec
 begin
 
-consts
-  list_nam :: cnam
-  test_nam :: cnam
-  append_name :: mname
-  makelist_name :: mname
-  val_nam :: vnam
-  next_nam :: vnam
+text {*
+  Since the types @{typ cnam}, @{text vnam}, and @{text mname} are 
+  anonymous, we describe distinctness of names in the example by axioms:
+*}
+axiomatization list_nam test_nam :: cnam
+where distinct_classes: "list_nam \<noteq> test_nam"
+
+axiomatization append_name makelist_name :: mname
+where distinct_methods: "append_name \<noteq> makelist_name"
+
+axiomatization val_nam next_nam :: vnam
+where distinct_fields: "val_nam \<noteq> next_nam"
+
+axioms nat_to_loc'_inject: "nat_to_loc' l = nat_to_loc' l' \<longleftrightarrow> l = l'"
 
 definition list_name :: cname where
   "list_name == Cname list_nam"
@@ -86,96 +93,103 @@
 definition E :: jvm_prog where
   "E == SystemClasses @ [(list_name, list_class), (test_name, test_class)]"
 
+code_datatype list_nam test_nam
+lemma equal_cnam_code [code]:
+  "HOL.equal list_nam list_nam \<longleftrightarrow> True"
+  "HOL.equal test_nam test_nam \<longleftrightarrow> True"
+  "HOL.equal list_nam test_nam \<longleftrightarrow> False"
+  "HOL.equal test_nam list_nam \<longleftrightarrow> False"
+  by(simp_all add: distinct_classes distinct_classes[symmetric] equal_cnam_def)
 
-types_code
-  cnam ("string")
-  vnam ("string")
-  mname ("string")
-  loc' ("int")
+code_datatype append_name makelist_name
+lemma equal_mname_code [code]: 
+  "HOL.equal append_name append_name \<longleftrightarrow> True"
+  "HOL.equal makelist_name makelist_name \<longleftrightarrow> True"
+  "HOL.equal append_name makelist_name \<longleftrightarrow> False"
+  "HOL.equal makelist_name append_name \<longleftrightarrow> False"
+  by(simp_all add: distinct_methods distinct_methods[symmetric] equal_mname_def)
 
-consts_code
-  "new_Addr" ("\<module>new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *}/ {* Loc *}")
-attach {*
-fun new_addr p none loc hp =
-  let fun nr i = if p (hp (loc i)) then (loc i, none) else nr (i+1);
-  in nr 0 end;
-*}
+code_datatype val_nam next_nam
+lemma equal_vnam_code [code]: 
+  "HOL.equal val_nam val_nam \<longleftrightarrow> True"
+  "HOL.equal next_nam next_nam \<longleftrightarrow> True"
+  "HOL.equal val_nam next_nam \<longleftrightarrow> False"
+  "HOL.equal next_nam val_nam \<longleftrightarrow> False"
+  by(simp_all add: distinct_fields distinct_fields[symmetric] equal_vnam_def)
+
 
-  "undefined" ("(raise Match)")
-  "undefined :: val" ("{* Unit *}")
-  "undefined :: cname" ("{* Object *}")
+lemma equal_loc'_code [code]:
+  "HOL.equal (nat_to_loc' l) (nat_to_loc' l') \<longleftrightarrow> l = l'"
+  by(simp add: equal_loc'_def nat_to_loc'_inject)
 
-  "list_nam" ("\"list\"")
-  "test_nam" ("\"test\"")
-  "append_name" ("\"append\"")
-  "makelist_name" ("\"makelist\"")
-  "val_nam" ("\"val\"")
-  "next_nam" ("\"next\"")
+definition undefined_cname :: cname 
+  where [code del]: "undefined_cname = undefined"
+code_datatype Object Xcpt Cname undefined_cname
+declare undefined_cname_def[symmetric, code_inline]
+
+definition undefined_val :: val
+  where [code del]: "undefined_val = undefined"
+declare undefined_val_def[symmetric, code_inline]
+code_datatype Unit Null Bool Intg Addr undefined_val
 
 definition
   "test = exec (E, start_state E test_name makelist_name)"
 
-
-subsection {* Single step execution *}
-
-code_module JVM
-contains
-  exec = exec
-  test = test
-
-ML {* JVM.test *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
-ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {*
+  @{code test}; 
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+  @{code exec} (@{code E}, @{code the} it);
+*}
 
 end