dropped code generator setup garbage
authorhaftmann
Fri Aug 10 17:10:06 2007 +0200 (2007-08-10)
changeset 24225348e982c694b
parent 24224 a5c95bbeb31d
child 24226 86f228ce1aef
dropped code generator setup garbage
src/HOL/MicroJava/JVM/JVMListExample.thy
     1.1 --- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Fri Aug 10 17:10:05 2007 +0200
     1.2 +++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Fri Aug 10 17:10:06 2007 +0200
     1.3 @@ -112,60 +112,6 @@
     1.4    "val_nam" ("\"val\"")
     1.5    "next_nam" ("\"next\"")
     1.6  
     1.7 -code_type cnam and vnam and mname and loc_
     1.8 -  (SML "string" and "string" and "string" and "IntInf.int")
     1.9 -
    1.10 -instance cnam :: eq
    1.11 -  and cname :: eq
    1.12 -  and vname :: eq
    1.13 -  and mname :: eq
    1.14 -  and ty :: eq
    1.15 -  and val :: eq
    1.16 -  and instr :: eq ..
    1.17 -
    1.18 -definition
    1.19 -  arbitrary_val :: val where
    1.20 -  [symmetric, code inline]: "arbitrary_val = arbitrary"
    1.21 -definition
    1.22 -  arbitrary_cname :: cname where
    1.23 -  [symmetric, code inline]: "arbitrary_cname = arbitrary"
    1.24 -
    1.25 -definition "unit' = Unit"
    1.26 -definition "object' = Object"
    1.27 -
    1.28 -code_axioms
    1.29 -  arbitrary_val \<equiv> unit'
    1.30 -  arbitrary_cname \<equiv> object'
    1.31 -
    1.32 -code_const list_nam and test_nam and append_name and makelist_name and val_nam and next_nam
    1.33 -  (SML "\"list\"" and "\"test\"" and "\"append\""
    1.34 -    and "\"makelist\"" and "\"val\"" and "\"next\"")
    1.35 -
    1.36 -axiomatization
    1.37 -  incr_loc :: "loc_ \<Rightarrow> loc_"
    1.38 -  and zero_loc :: "loc_"
    1.39 -
    1.40 -code_const incr_loc and zero_loc
    1.41 -  (SML "(op +)/ (_, 1)" and "0")
    1.42 -
    1.43 -axiomatization
    1.44 -  test_loc :: "(loc_ \<Rightarrow> bool) \<Rightarrow> (loc_ \<Rightarrow> 'a) \<Rightarrow> loc_ \<Rightarrow> 'a" where
    1.45 -  "test_loc p v l = (if p l then v l else test_loc p v (incr l))"
    1.46 -
    1.47 -definition
    1.48 -  new_addr' :: "(loc \<Rightarrow> (cname \<times> (vname \<times> cname \<Rightarrow> val option)) option) \<Rightarrow> loc \<times> val option" where
    1.49 -  "new_addr' hp =
    1.50 -    test_loc (\<lambda>i. hp (Loc i) = None) (\<lambda>i. (Loc i, None)) zero_loc"
    1.51 -
    1.52 -lemma [code func]:
    1.53 -  "wf_class = wf_class" ..
    1.54 -
    1.55 -code_const
    1.56 -  wf_class (SML "(fn `_ => true)")
    1.57 -
    1.58 -code_axioms
    1.59 -  new_Addr \<equiv> new_addr'
    1.60 -
    1.61  definition
    1.62    "test = exec (E, start_state E test_name makelist_name)"
    1.63  
    1.64 @@ -174,7 +120,8 @@
    1.65  
    1.66  code_module JVM
    1.67  contains
    1.68 -  test = "exec (E, start_state E test_name makelist_name)"
    1.69 +  exec = exec
    1.70 +  test = test
    1.71  
    1.72  ML {*
    1.73  JVM.test;