replace old SML code generator by new code generator in MicroJava/JVM and /BV
authorAndreas Lochbihler
Fri Aug 05 14:16:44 2011 +0200 (2011-08-05)
changeset 44035322d1657c40c
parent 44034 53a081c8873d
child 44036 d03f9f28d01d
child 44037 25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/JVM and /BV
src/HOL/MicroJava/BV/BVExample.thy
src/HOL/MicroJava/J/JBasis.thy
src/HOL/MicroJava/J/State.thy
src/HOL/MicroJava/J/SystemClasses.thy
src/HOL/MicroJava/J/Type.thy
src/HOL/MicroJava/J/TypeRel.thy
src/HOL/MicroJava/JVM/JVMListExample.thy
     1.1 --- a/src/HOL/MicroJava/BV/BVExample.thy	Fri Aug 05 00:14:08 2011 +0200
     1.2 +++ b/src/HOL/MicroJava/BV/BVExample.thy	Fri Aug 05 14:16:44 2011 +0200
     1.3 @@ -21,13 +21,6 @@
     1.4  *}
     1.5  
     1.6  section "Setup"
     1.7 -text {*
     1.8 -  Since the types @{typ cnam}, @{text vnam}, and @{text mname} are 
     1.9 -  anonymous, we describe distinctness of names in the example by axioms:
    1.10 -*}
    1.11 -axioms 
    1.12 -  distinct_classes: "list_nam \<noteq> test_nam"
    1.13 -  distinct_fields:  "val_nam \<noteq> next_nam"
    1.14  
    1.15  text {* Abbreviations for definitions we will have to use often in the
    1.16  proofs below: *}
    1.17 @@ -415,35 +408,45 @@
    1.18      in  kiljvm G mxs (1+size pTs+mxl) rT et instr start)"
    1.19  
    1.20  lemma [code]:
    1.21 -  "unstables r step ss = (UN p:{..<size ss}. if \<not>stable r step ss p then {p} else {})"
    1.22 -  apply (unfold unstables_def)
    1.23 -  apply (rule equalityI)
    1.24 -  apply (rule subsetI)
    1.25 -  apply (erule CollectE)
    1.26 -  apply (erule conjE)
    1.27 -  apply (rule UN_I)
    1.28 -  apply simp
    1.29 -  apply simp
    1.30 -  apply (rule subsetI)
    1.31 -  apply (erule UN_E)
    1.32 -  apply (case_tac "\<not> stable r step ss p")
    1.33 -  apply simp+
    1.34 -  done
    1.35 +  "unstables r step ss = 
    1.36 +   foldr (\<lambda>p A. if \<not>stable r step ss p then insert p A else A) [0..<size ss] {}"
    1.37 +proof -
    1.38 +  have "unstables r step ss = (UN p:{..<size ss}. if \<not>stable r step ss p then {p} else {})"
    1.39 +    apply (unfold unstables_def)
    1.40 +    apply (rule equalityI)
    1.41 +    apply (rule subsetI)
    1.42 +    apply (erule CollectE)
    1.43 +    apply (erule conjE)
    1.44 +    apply (rule UN_I)
    1.45 +    apply simp
    1.46 +    apply simp
    1.47 +    apply (rule subsetI)
    1.48 +    apply (erule UN_E)
    1.49 +    apply (case_tac "\<not> stable r step ss p")
    1.50 +    apply simp+
    1.51 +    done
    1.52 +  also have "\<And>f. (UN p:{..<size ss}. f p) = Union (set (map f [0..<size ss]))" by auto
    1.53 +  also note Sup_set_foldr also note foldr_map
    1.54 +  also have "op \<union> \<circ> (\<lambda>p. if \<not> stable r step ss p then {p} else {}) = 
    1.55 +            (\<lambda>p A. if \<not>stable r step ss p then insert p A else A)"
    1.56 +    by(auto simp add: fun_eq_iff)
    1.57 +  finally show ?thesis .
    1.58 +qed
    1.59  
    1.60 -definition some_elem :: "'a set \<Rightarrow> 'a" where
    1.61 +definition some_elem :: "'a set \<Rightarrow> 'a" where [code del]:
    1.62    "some_elem = (%S. SOME x. x : S)"
    1.63 -
    1.64 -consts_code
    1.65 -  "some_elem" ("(case/ _ of/ {*Set*}/ xs/ =>/ hd/ xs)")
    1.66 +code_const some_elem
    1.67 +  (SML "(case/ _ of/ Set/ xs/ =>/ hd/ xs)")
    1.68 +setup {* Code.add_signature_cmd ("some_elem", "'a set \<Rightarrow> 'a") *}
    1.69  
    1.70  text {* This code setup is just a demonstration and \emph{not} sound! *}
    1.71  
    1.72  lemma False
    1.73  proof -
    1.74    have "some_elem (set [False, True]) = False"
    1.75 -    by evaluation
    1.76 +    by eval
    1.77    moreover have "some_elem (set [True, False]) = True"
    1.78 -    by evaluation
    1.79 +    by eval
    1.80    ultimately show False
    1.81      by (simp add: some_elem_def)
    1.82  qed
    1.83 @@ -465,15 +468,35 @@
    1.84    by simp
    1.85  
    1.86  lemmas [code] = JType.sup_def [unfolded exec_lub_def] JVM_le_unfold
    1.87 +lemmas [code] = lesub_def plussub_def
    1.88  
    1.89 -lemmas [code_ind] = rtranclp.rtrancl_refl converse_rtranclp_into_rtranclp
    1.90 +setup {*
    1.91 +  Code.add_signature_cmd ("More_Set.is_empty", "'a set \<Rightarrow> bool")
    1.92 +  #> 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") 
    1.93 +  #> Code.add_signature_cmd 
    1.94 +     ("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")
    1.95 +  #> 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") 
    1.96 +*}
    1.97 +
    1.98 +definition [code del]: "mem2 = op :"
    1.99 +lemma [code]: "mem2 x A = A x"
   1.100 +  by(simp add: mem2_def mem_def)
   1.101  
   1.102 -code_module BV
   1.103 -contains
   1.104 -  test1 = "test_kil E list_name [Class list_name] (PrimT Void) 3 0
   1.105 +lemmas [folded mem2_def, code] =
   1.106 +  JType.sup_def[unfolded exec_lub_def]
   1.107 +  wf_class_code
   1.108 +  widen.equation
   1.109 +  match_exception_entry_def
   1.110 +
   1.111 +definition test1 where
   1.112 +  "test1 = test_kil E list_name [Class list_name] (PrimT Void) 3 0
   1.113      [(Suc 0, 2, 8, Xcpt NullPointer)] append_ins"
   1.114 -  test2 = "test_kil E test_name [] (PrimT Void) 3 2 [] make_list_ins"
   1.115 -ML BV.test1
   1.116 -ML BV.test2
   1.117 +definition test2 where
   1.118 +  "test2 = test_kil E test_name [] (PrimT Void) 3 2 [] make_list_ins"
   1.119 +
   1.120 +ML {* 
   1.121 +  @{code test1}; 
   1.122 +  @{code test2};
   1.123 +*}
   1.124  
   1.125  end
     2.1 --- a/src/HOL/MicroJava/J/JBasis.thy	Fri Aug 05 00:14:08 2011 +0200
     2.2 +++ b/src/HOL/MicroJava/J/JBasis.thy	Fri Aug 05 14:16:44 2011 +0200
     2.3 @@ -7,7 +7,7 @@
     2.4    \isaheader{Some Auxiliary Definitions}
     2.5  *}
     2.6  
     2.7 -theory JBasis imports Main begin 
     2.8 +theory JBasis imports Main "~~/src/HOL/Library/Transitive_Closure_Table" begin 
     2.9  
    2.10  lemmas [simp] = Let_def
    2.11  
     3.1 --- a/src/HOL/MicroJava/J/State.thy	Fri Aug 05 00:14:08 2011 +0200
     3.2 +++ b/src/HOL/MicroJava/J/State.thy	Fri Aug 05 14:16:44 2011 +0200
     3.3 @@ -52,8 +52,18 @@
     3.4  definition raise_if :: "bool \<Rightarrow> xcpt \<Rightarrow> val option \<Rightarrow> val option" where
     3.5    "raise_if b x xo \<equiv> if b \<and>  (xo = None) then Some (Addr (XcptRef x)) else xo"
     3.6  
     3.7 +text {* Make new_Addr completely specified (at least for the code generator) *}
     3.8 +(*
     3.9  definition new_Addr  :: "aheap => loc \<times> val option" where
    3.10    "new_Addr h \<equiv> SOME (a,x). (h a = None \<and>  x = None) |  x = Some (Addr (XcptRef OutOfMemory))"
    3.11 +*)
    3.12 +consts nat_to_loc' :: "nat => loc'"
    3.13 +code_datatype nat_to_loc'
    3.14 +definition new_Addr  :: "aheap => loc \<times> val option" where
    3.15 +  "new_Addr h \<equiv> 
    3.16 +   if \<exists>n. h (Loc (nat_to_loc' n)) = None 
    3.17 +   then (Loc (nat_to_loc' (LEAST n. h (Loc (nat_to_loc' n)) = None)), None)
    3.18 +   else (Loc (nat_to_loc' 0), Some (Addr (XcptRef OutOfMemory)))"
    3.19  
    3.20  definition np    :: "val => val option => val option" where
    3.21   "np v == raise_if (v = Null) NullPointer"
    3.22 @@ -74,11 +84,8 @@
    3.23    hp ref = None \<and> xcp = None \<or> xcp = Some (Addr (XcptRef OutOfMemory))"
    3.24  apply (drule sym)
    3.25  apply (unfold new_Addr_def)
    3.26 -apply(simp add: Pair_fst_snd_eq Eps_split)
    3.27 -apply(rule someI)
    3.28 -apply(rule disjI2)
    3.29 -apply(rule_tac r = "snd (?a,Some (Addr (XcptRef OutOfMemory)))" in trans)
    3.30 -apply auto
    3.31 +apply (simp split: split_if_asm)
    3.32 +apply (erule LeastI)
    3.33  done
    3.34  
    3.35  lemma raise_if_True [simp]: "raise_if True x y \<noteq> None"
    3.36 @@ -150,4 +157,42 @@
    3.37  lemma c_hupd_fst [simp]: "fst (c_hupd h (x, s)) = x"
    3.38  by (simp add: c_hupd_def split_beta)
    3.39  
    3.40 +text {* Naive implementation for @{term "new_Addr"} by exhaustive search *}
    3.41 +
    3.42 +definition gen_new_Addr :: "aheap => nat \<Rightarrow> loc \<times> val option" where
    3.43 +  "gen_new_Addr h n \<equiv> 
    3.44 +   if \<exists>a. a \<ge> n \<and> h (Loc (nat_to_loc' a)) = None 
    3.45 +   then (Loc (nat_to_loc' (LEAST a. a \<ge> n \<and> h (Loc (nat_to_loc' a)) = None)), None)
    3.46 +   else (Loc (nat_to_loc' 0), Some (Addr (XcptRef OutOfMemory)))"
    3.47 +
    3.48 +lemma new_Addr_code_code [code]:
    3.49 +  "new_Addr h = gen_new_Addr h 0"
    3.50 +by(simp only: new_Addr_def gen_new_Addr_def split: split_if) simp
    3.51 +
    3.52 +lemma gen_new_Addr_code [code]:
    3.53 +  "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))"
    3.54 +apply(simp add: gen_new_Addr_def)
    3.55 +apply(rule impI)
    3.56 +apply(rule conjI)
    3.57 + apply safe[1]
    3.58 +  apply(auto intro: arg_cong[where f=nat_to_loc'] Least_equality)[1]
    3.59 + apply(rule arg_cong[where f=nat_to_loc'])
    3.60 + apply(rule arg_cong[where f=Least])
    3.61 + apply(rule ext)
    3.62 + apply(safe, simp_all)[1]
    3.63 + apply(rename_tac "n'")
    3.64 + apply(case_tac "n = n'", simp_all)[1]
    3.65 +apply clarify
    3.66 +apply(subgoal_tac "a = n")
    3.67 + apply(auto intro: Least_equality arg_cong[where f=nat_to_loc'])[1]
    3.68 +apply(rule ccontr)
    3.69 +apply(erule_tac x="a" in allE)
    3.70 +apply simp
    3.71 +done
    3.72 +
    3.73 +instantiation loc' :: equal begin
    3.74 +definition "HOL.equal (l :: loc') l' \<longleftrightarrow> l = l'"
    3.75 +instance proof qed(simp add: equal_loc'_def)
    3.76  end
    3.77 +
    3.78 +end
     4.1 --- a/src/HOL/MicroJava/J/SystemClasses.thy	Fri Aug 05 00:14:08 2011 +0200
     4.2 +++ b/src/HOL/MicroJava/J/SystemClasses.thy	Fri Aug 05 14:16:44 2011 +0200
     4.3 @@ -13,18 +13,18 @@
     4.4  *}
     4.5  
     4.6  definition ObjectC :: "'c cdecl" where
     4.7 -  "ObjectC \<equiv> (Object, (undefined,[],[]))"
     4.8 +  [code_inline]: "ObjectC \<equiv> (Object, (undefined,[],[]))"
     4.9  
    4.10  definition NullPointerC :: "'c cdecl" where
    4.11 -  "NullPointerC \<equiv> (Xcpt NullPointer, (Object,[],[]))"
    4.12 +  [code_inline]: "NullPointerC \<equiv> (Xcpt NullPointer, (Object,[],[]))"
    4.13  
    4.14  definition ClassCastC :: "'c cdecl" where
    4.15 -  "ClassCastC \<equiv> (Xcpt ClassCast, (Object,[],[]))"
    4.16 +  [code_inline]: "ClassCastC \<equiv> (Xcpt ClassCast, (Object,[],[]))"
    4.17  
    4.18  definition OutOfMemoryC :: "'c cdecl" where
    4.19 -  "OutOfMemoryC \<equiv> (Xcpt OutOfMemory, (Object,[],[]))"
    4.20 +  [code_inline]: "OutOfMemoryC \<equiv> (Xcpt OutOfMemory, (Object,[],[]))"
    4.21  
    4.22  definition SystemClasses :: "'c cdecl list" where
    4.23 -  "SystemClasses \<equiv> [ObjectC, NullPointerC, ClassCastC, OutOfMemoryC]"
    4.24 +  [code_inline]: "SystemClasses \<equiv> [ObjectC, NullPointerC, ClassCastC, OutOfMemoryC]"
    4.25  
    4.26  end
     5.1 --- a/src/HOL/MicroJava/J/Type.thy	Fri Aug 05 00:14:08 2011 +0200
     5.2 +++ b/src/HOL/MicroJava/J/Type.thy	Fri Aug 05 14:16:44 2011 +0200
     5.3 @@ -8,6 +8,10 @@
     5.4  theory Type imports JBasis begin
     5.5  
     5.6  typedecl cnam 
     5.7 +instantiation cnam :: equal begin
     5.8 +definition "HOL.equal (cn :: cnam) cn' \<longleftrightarrow> cn = cn'"
     5.9 +instance proof qed(simp add: equal_cnam_def)
    5.10 +end
    5.11  
    5.12   -- "exceptions"
    5.13  datatype 
    5.14 @@ -23,7 +27,16 @@
    5.15    | Cname cnam 
    5.16  
    5.17  typedecl vnam   -- "variable or field name"
    5.18 +instantiation vnam :: equal begin
    5.19 +definition "HOL.equal (vn :: vnam) vn' \<longleftrightarrow> vn = vn'"
    5.20 +instance proof qed(simp add: equal_vnam_def)
    5.21 +end
    5.22 +
    5.23  typedecl mname  -- "method name"
    5.24 +instantiation mname :: equal begin
    5.25 +definition "HOL.equal (M :: mname) M' \<longleftrightarrow> M = M'"
    5.26 +instance proof qed(simp add: equal_mname_def)
    5.27 +end
    5.28  
    5.29  -- "names for @{text This} pointer and local/field variables"
    5.30  datatype vname 
     6.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Fri Aug 05 00:14:08 2011 +0200
     6.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Fri Aug 05 14:16:44 2011 +0200
     6.3 @@ -77,22 +77,112 @@
     6.4    "wf_class G = wf ((subcls1 G)^-1)"
     6.5  
     6.6  
     6.7 -text {* Code generator setup (FIXME!) *}
     6.8 +
     6.9 +text {* Code generator setup *}
    6.10 +
    6.11 +code_pred 
    6.12 +  (modes: i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool, i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool)
    6.13 +  subcls1p 
    6.14 +  .
    6.15 +declare subcls1_def[unfolded Collect_def, code_pred_def]
    6.16 +code_pred 
    6.17 +  (modes: i \<Rightarrow> i \<times> o \<Rightarrow> bool, i \<Rightarrow> i \<times> i \<Rightarrow> bool)
    6.18 +  [inductify]
    6.19 +  subcls1 
    6.20 +  .
    6.21 +
    6.22 +definition subcls' where "subcls' G = (subcls1p G)^**"
    6.23 +code_pred
    6.24 +  (modes: i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool, i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool)
    6.25 +  [inductify]
    6.26 +  subcls'
    6.27 +.
    6.28 +lemma subcls_conv_subcls' [code_inline]:
    6.29 +  "(subcls1 G)^* = (\<lambda>(C, D). subcls' G C D)"
    6.30 +by(simp add: subcls'_def subcls1_def rtrancl_def)(simp add: Collect_def)
    6.31 +
    6.32 +lemma class_rec_code [code]:
    6.33 +  "class_rec G C t f = 
    6.34 +  (if wf_class G then 
    6.35 +    (case class G C of
    6.36 +       None \<Rightarrow> class_rec G C t f
    6.37 +     | Some (D, fs, ms) \<Rightarrow> 
    6.38 +       if C = Object then f Object fs ms t else f C fs ms (class_rec G D t f))
    6.39 +   else class_rec G C t f)"
    6.40 +apply(cases "wf_class G")
    6.41 + apply(unfold class_rec_def wf_class_def)
    6.42 + apply(subst wfrec, assumption)
    6.43 + apply(cases "class G C")
    6.44 +  apply(simp add: wfrec)
    6.45 + apply clarsimp
    6.46 + apply(rename_tac D fs ms)
    6.47 + apply(rule_tac f="f C fs ms" in arg_cong)
    6.48 + apply(clarsimp simp add: cut_def)
    6.49 + apply(blast intro: subcls1I)
    6.50 +apply simp
    6.51 +done
    6.52  
    6.53 -consts_code
    6.54 -  "wfrec"   ("\<module>wfrec?")
    6.55 -attach {*
    6.56 -fun wfrec f x = f (wfrec f) x;
    6.57 -*}
    6.58 +lemma wf_class_code [code]:
    6.59 +  "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)"
    6.60 +proof
    6.61 +  assume "wf_class G"
    6.62 +  hence wf: "wf (((subcls1 G)^+)^-1)" unfolding wf_class_def by(rule wf_converse_trancl)
    6.63 +  hence acyc: "acyclic ((subcls1 G)^+)" by(auto dest: wf_acyclic)
    6.64 +  show "\<forall>(C, rest) \<in> set G. C \<noteq> Object \<longrightarrow> \<not> G \<turnstile> fst (the (class G C)) \<preceq>C C"
    6.65 +  proof(safe)
    6.66 +    fix C D fs ms
    6.67 +    assume "(C, D, fs, ms) \<in> set G"
    6.68 +      and "C \<noteq> Object"
    6.69 +      and subcls: "G \<turnstile> fst (the (class G C)) \<preceq>C C"
    6.70 +    from `(C, D, fs, ms) \<in> set G` obtain D' fs' ms'
    6.71 +      where "class": "class G C = Some (D', fs', ms')"
    6.72 +      unfolding class_def by(auto dest!: weak_map_of_SomeI)
    6.73 +    hence "G \<turnstile> C \<prec>C1 D'" using `C \<noteq> Object` ..
    6.74 +    hence "(C, D') \<in> (subcls1 G)^+" ..
    6.75 +    also with acyc have "C \<noteq> D'" by(auto simp add: acyclic_def)
    6.76 +    with subcls "class" have "(D', C) \<in> (subcls1 G)^+" by(auto dest: rtranclD)
    6.77 +    finally show False using acyc by(auto simp add: acyclic_def)
    6.78 +  qed
    6.79 +next
    6.80 +  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"
    6.81 +  have "acyclic (subcls1 G)"
    6.82 +  proof(intro acyclicI strip notI)
    6.83 +    fix C
    6.84 +    assume "(C, C) \<in> (subcls1 G)\<^sup>+"
    6.85 +    thus False
    6.86 +    proof(cases)
    6.87 +      case base
    6.88 +      then obtain rest where "class G C = Some (C, rest)"
    6.89 +        and "C \<noteq> Object" by cases
    6.90 +      from `class G C = Some (C, rest)` have "(C, C, rest) \<in> set G"
    6.91 +        unfolding class_def by(rule map_of_SomeD)
    6.92 +      with `C \<noteq> Object` `class G C = Some (C, rest)`
    6.93 +      have "\<not> G \<turnstile> C \<preceq>C C" by(auto dest: rhs)
    6.94 +      thus False by simp
    6.95 +    next
    6.96 +      case (step D)
    6.97 +      from `G \<turnstile> D \<prec>C1 C` obtain rest where "class G D = Some (C, rest)"
    6.98 +        and "D \<noteq> Object" by cases
    6.99 +      from `class G D = Some (C, rest)` have "(D, C, rest) \<in> set G"
   6.100 +        unfolding class_def by(rule map_of_SomeD)
   6.101 +      with `D \<noteq> Object` `class G D = Some (C, rest)`
   6.102 +      have "\<not> G \<turnstile> C \<preceq>C D" by(auto dest: rhs)
   6.103 +      moreover from `(C, D) \<in> (subcls1 G)\<^sup>+`
   6.104 +      have "G \<turnstile> C \<preceq>C D" by(rule trancl_into_rtrancl)
   6.105 +      ultimately show False by contradiction
   6.106 +    qed
   6.107 +  qed
   6.108 +  thus "wf_class G" unfolding wf_class_def
   6.109 +    by(rule finite_acyclic_wf_converse[OF finite_subcls1])
   6.110 +qed
   6.111  
   6.112  consts
   6.113 -
   6.114    method :: "'c prog \<times> cname => ( sig   \<rightharpoonup> cname \<times> ty \<times> 'c)" (* ###curry *)
   6.115    field  :: "'c prog \<times> cname => ( vname \<rightharpoonup> cname \<times> ty     )" (* ###curry *)
   6.116    fields :: "'c prog \<times> cname => ((vname \<times> cname) \<times> ty) list" (* ###curry *)
   6.117  
   6.118  -- "methods of a class, with inheritance, overriding and hiding, cf. 8.4.6"
   6.119 -defs method_def: "method \<equiv> \<lambda>(G,C). class_rec G C empty (\<lambda>C fs ms ts.
   6.120 +defs method_def [code]: "method \<equiv> \<lambda>(G,C). class_rec G C empty (\<lambda>C fs ms ts.
   6.121                             ts ++ map_of (map (\<lambda>(s,m). (s,(C,m))) ms))"
   6.122  
   6.123  lemma method_rec_lemma: "[|class G C = Some (D,fs,ms); wf ((subcls1 G)^-1)|] ==>
   6.124 @@ -106,7 +196,7 @@
   6.125  
   6.126  
   6.127  -- "list of fields of a class, including inherited and hidden ones"
   6.128 -defs fields_def: "fields \<equiv> \<lambda>(G,C). class_rec G C []    (\<lambda>C fs ms ts.
   6.129 +defs fields_def [code]: "fields \<equiv> \<lambda>(G,C). class_rec G C []    (\<lambda>C fs ms ts.
   6.130                             map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ ts)"
   6.131  
   6.132  lemma fields_rec_lemma: "[|class G C = Some (D,fs,ms); wf ((subcls1 G)^-1)|] ==>
   6.133 @@ -119,7 +209,7 @@
   6.134  done
   6.135  
   6.136  
   6.137 -defs field_def: "field == map_of o (map (\<lambda>((fn,fd),ft). (fn,(fd,ft)))) o fields"
   6.138 +defs field_def [code]: "field == map_of o (map (\<lambda>((fn,fd),ft). (fn,(fd,ft)))) o fields"
   6.139  
   6.140  lemma field_fields: 
   6.141  "field (G,C) fn = Some (fd, fT) \<Longrightarrow> map_of (fields (G,C)) (fn, fd) = Some fT"
   6.142 @@ -138,6 +228,8 @@
   6.143  | subcls         : "G\<turnstile>C\<preceq>C D ==> G\<turnstile>Class C \<preceq> Class D"
   6.144  | null   [intro!]:             "G\<turnstile>     NT \<preceq> RefT R"
   6.145  
   6.146 +code_pred widen .
   6.147 +
   6.148  lemmas refl = HOL.refl
   6.149  
   6.150  -- "casting conversion, cf. 5.5 / 5.1.5"
     7.1 --- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Fri Aug 05 00:14:08 2011 +0200
     7.2 +++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Fri Aug 05 14:16:44 2011 +0200
     7.3 @@ -8,13 +8,20 @@
     7.4  imports "../J/SystemClasses" JVMExec
     7.5  begin
     7.6  
     7.7 -consts
     7.8 -  list_nam :: cnam
     7.9 -  test_nam :: cnam
    7.10 -  append_name :: mname
    7.11 -  makelist_name :: mname
    7.12 -  val_nam :: vnam
    7.13 -  next_nam :: vnam
    7.14 +text {*
    7.15 +  Since the types @{typ cnam}, @{text vnam}, and @{text mname} are 
    7.16 +  anonymous, we describe distinctness of names in the example by axioms:
    7.17 +*}
    7.18 +axiomatization list_nam test_nam :: cnam
    7.19 +where distinct_classes: "list_nam \<noteq> test_nam"
    7.20 +
    7.21 +axiomatization append_name makelist_name :: mname
    7.22 +where distinct_methods: "append_name \<noteq> makelist_name"
    7.23 +
    7.24 +axiomatization val_nam next_nam :: vnam
    7.25 +where distinct_fields: "val_nam \<noteq> next_nam"
    7.26 +
    7.27 +axioms nat_to_loc'_inject: "nat_to_loc' l = nat_to_loc' l' \<longleftrightarrow> l = l'"
    7.28  
    7.29  definition list_name :: cname where
    7.30    "list_name == Cname list_nam"
    7.31 @@ -86,96 +93,103 @@
    7.32  definition E :: jvm_prog where
    7.33    "E == SystemClasses @ [(list_name, list_class), (test_name, test_class)]"
    7.34  
    7.35 +code_datatype list_nam test_nam
    7.36 +lemma equal_cnam_code [code]:
    7.37 +  "HOL.equal list_nam list_nam \<longleftrightarrow> True"
    7.38 +  "HOL.equal test_nam test_nam \<longleftrightarrow> True"
    7.39 +  "HOL.equal list_nam test_nam \<longleftrightarrow> False"
    7.40 +  "HOL.equal test_nam list_nam \<longleftrightarrow> False"
    7.41 +  by(simp_all add: distinct_classes distinct_classes[symmetric] equal_cnam_def)
    7.42  
    7.43 -types_code
    7.44 -  cnam ("string")
    7.45 -  vnam ("string")
    7.46 -  mname ("string")
    7.47 -  loc' ("int")
    7.48 +code_datatype append_name makelist_name
    7.49 +lemma equal_mname_code [code]: 
    7.50 +  "HOL.equal append_name append_name \<longleftrightarrow> True"
    7.51 +  "HOL.equal makelist_name makelist_name \<longleftrightarrow> True"
    7.52 +  "HOL.equal append_name makelist_name \<longleftrightarrow> False"
    7.53 +  "HOL.equal makelist_name append_name \<longleftrightarrow> False"
    7.54 +  by(simp_all add: distinct_methods distinct_methods[symmetric] equal_mname_def)
    7.55  
    7.56 -consts_code
    7.57 -  "new_Addr" ("\<module>new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *}/ {* Loc *}")
    7.58 -attach {*
    7.59 -fun new_addr p none loc hp =
    7.60 -  let fun nr i = if p (hp (loc i)) then (loc i, none) else nr (i+1);
    7.61 -  in nr 0 end;
    7.62 -*}
    7.63 +code_datatype val_nam next_nam
    7.64 +lemma equal_vnam_code [code]: 
    7.65 +  "HOL.equal val_nam val_nam \<longleftrightarrow> True"
    7.66 +  "HOL.equal next_nam next_nam \<longleftrightarrow> True"
    7.67 +  "HOL.equal val_nam next_nam \<longleftrightarrow> False"
    7.68 +  "HOL.equal next_nam val_nam \<longleftrightarrow> False"
    7.69 +  by(simp_all add: distinct_fields distinct_fields[symmetric] equal_vnam_def)
    7.70 +
    7.71  
    7.72 -  "undefined" ("(raise Match)")
    7.73 -  "undefined :: val" ("{* Unit *}")
    7.74 -  "undefined :: cname" ("{* Object *}")
    7.75 +lemma equal_loc'_code [code]:
    7.76 +  "HOL.equal (nat_to_loc' l) (nat_to_loc' l') \<longleftrightarrow> l = l'"
    7.77 +  by(simp add: equal_loc'_def nat_to_loc'_inject)
    7.78  
    7.79 -  "list_nam" ("\"list\"")
    7.80 -  "test_nam" ("\"test\"")
    7.81 -  "append_name" ("\"append\"")
    7.82 -  "makelist_name" ("\"makelist\"")
    7.83 -  "val_nam" ("\"val\"")
    7.84 -  "next_nam" ("\"next\"")
    7.85 +definition undefined_cname :: cname 
    7.86 +  where [code del]: "undefined_cname = undefined"
    7.87 +code_datatype Object Xcpt Cname undefined_cname
    7.88 +declare undefined_cname_def[symmetric, code_inline]
    7.89 +
    7.90 +definition undefined_val :: val
    7.91 +  where [code del]: "undefined_val = undefined"
    7.92 +declare undefined_val_def[symmetric, code_inline]
    7.93 +code_datatype Unit Null Bool Intg Addr undefined_val
    7.94  
    7.95  definition
    7.96    "test = exec (E, start_state E test_name makelist_name)"
    7.97  
    7.98 -
    7.99 -subsection {* Single step execution *}
   7.100 -
   7.101 -code_module JVM
   7.102 -contains
   7.103 -  exec = exec
   7.104 -  test = test
   7.105 -
   7.106 -ML {* JVM.test *}
   7.107 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.108 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.109 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.110 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.111 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.112 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.113 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.114 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.115 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.116 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.117 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.118 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.119 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.120 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.121 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.122 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.123 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.124 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.125 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.126 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.127 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.128 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.129 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.130 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.131 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.132 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.133 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.134 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.135 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.136 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.137 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.138 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.139 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.140 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.141 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.142 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.143 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.144 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.145 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.146 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.147 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.148 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.149 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.150 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.151 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.152 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.153 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.154 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.155 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.156 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.157 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.158 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.159 -ML {* JVM.exec (JVM.E, JVM.the it) *}
   7.160 +ML {*
   7.161 +  @{code test}; 
   7.162 +  @{code exec} (@{code E}, @{code the} it);
   7.163 +  @{code exec} (@{code E}, @{code the} it);
   7.164 +  @{code exec} (@{code E}, @{code the} it);
   7.165 +  @{code exec} (@{code E}, @{code the} it);
   7.166 +  @{code exec} (@{code E}, @{code the} it);
   7.167 +  @{code exec} (@{code E}, @{code the} it);
   7.168 +  @{code exec} (@{code E}, @{code the} it);
   7.169 +  @{code exec} (@{code E}, @{code the} it);
   7.170 +  @{code exec} (@{code E}, @{code the} it);
   7.171 +  @{code exec} (@{code E}, @{code the} it);
   7.172 +  @{code exec} (@{code E}, @{code the} it);
   7.173 +  @{code exec} (@{code E}, @{code the} it);
   7.174 +  @{code exec} (@{code E}, @{code the} it);
   7.175 +  @{code exec} (@{code E}, @{code the} it);
   7.176 +  @{code exec} (@{code E}, @{code the} it);
   7.177 +  @{code exec} (@{code E}, @{code the} it);
   7.178 +  @{code exec} (@{code E}, @{code the} it);
   7.179 +  @{code exec} (@{code E}, @{code the} it);
   7.180 +  @{code exec} (@{code E}, @{code the} it);
   7.181 +  @{code exec} (@{code E}, @{code the} it);
   7.182 +  @{code exec} (@{code E}, @{code the} it);
   7.183 +  @{code exec} (@{code E}, @{code the} it);
   7.184 +  @{code exec} (@{code E}, @{code the} it);
   7.185 +  @{code exec} (@{code E}, @{code the} it);
   7.186 +  @{code exec} (@{code E}, @{code the} it);
   7.187 +  @{code exec} (@{code E}, @{code the} it);
   7.188 +  @{code exec} (@{code E}, @{code the} it);
   7.189 +  @{code exec} (@{code E}, @{code the} it);
   7.190 +  @{code exec} (@{code E}, @{code the} it);
   7.191 +  @{code exec} (@{code E}, @{code the} it);
   7.192 +  @{code exec} (@{code E}, @{code the} it);
   7.193 +  @{code exec} (@{code E}, @{code the} it);
   7.194 +  @{code exec} (@{code E}, @{code the} it);
   7.195 +  @{code exec} (@{code E}, @{code the} it);
   7.196 +  @{code exec} (@{code E}, @{code the} it);
   7.197 +  @{code exec} (@{code E}, @{code the} it);
   7.198 +  @{code exec} (@{code E}, @{code the} it);
   7.199 +  @{code exec} (@{code E}, @{code the} it);
   7.200 +  @{code exec} (@{code E}, @{code the} it);
   7.201 +  @{code exec} (@{code E}, @{code the} it);
   7.202 +  @{code exec} (@{code E}, @{code the} it);
   7.203 +  @{code exec} (@{code E}, @{code the} it);
   7.204 +  @{code exec} (@{code E}, @{code the} it);
   7.205 +  @{code exec} (@{code E}, @{code the} it);
   7.206 +  @{code exec} (@{code E}, @{code the} it);
   7.207 +  @{code exec} (@{code E}, @{code the} it);
   7.208 +  @{code exec} (@{code E}, @{code the} it);
   7.209 +  @{code exec} (@{code E}, @{code the} it);
   7.210 +  @{code exec} (@{code E}, @{code the} it);
   7.211 +  @{code exec} (@{code E}, @{code the} it);
   7.212 +  @{code exec} (@{code E}, @{code the} it);
   7.213 +  @{code exec} (@{code E}, @{code the} it);
   7.214 +  @{code exec} (@{code E}, @{code the} it);
   7.215 +*}
   7.216  
   7.217  end