src/HOL/MicroJava/BV/BVExample.thy
changeset 13092 eae72c47d07f
parent 13052 3bf41c474a88
child 13101 90b31354fe15
     1.1 --- a/src/HOL/MicroJava/BV/BVExample.thy	Fri Apr 19 14:44:50 2002 +0200
     1.2 +++ b/src/HOL/MicroJava/BV/BVExample.thy	Fri Apr 19 14:47:10 2002 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  
     1.5  header {* \isaheader{Example Welltypings}\label{sec:BVExample} *}
     1.6  
     1.7 -theory BVExample = JVMListExample + BVSpecTypeSafe:
     1.8 +theory BVExample = JVMListExample + BVSpecTypeSafe + JVM:
     1.9  
    1.10  text {*
    1.11    This theory shows type correctness of the example program in section 
    1.12 @@ -372,4 +372,83 @@
    1.13    apply simp
    1.14    done
    1.15  
    1.16 +
    1.17 +section "Example for code generation: inferring method types"
    1.18 +
    1.19 +constdefs
    1.20 +  test_kil :: "jvm_prog \<Rightarrow> cname \<Rightarrow> ty List.list \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 
    1.21 +             exception_table \<Rightarrow> instr List.list \<Rightarrow> JVMType.state List.list"
    1.22 +  "test_kil G C pTs rT mxs mxl et instr ==
    1.23 +   (let first  = Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err));
    1.24 +        start  = OK first#(replicate (size instr - 1) (OK None))
    1.25 +    in  kiljvm G mxs (1+size pTs+mxl) rT et instr start)"
    1.26 +
    1.27 +lemma [code]:
    1.28 +  "unstables r step ss = (UN p:{..size ss(}. if \<not>stable r step ss p then {p} else {})"
    1.29 +  apply (unfold unstables_def)
    1.30 +  apply (rule equalityI)
    1.31 +  apply (rule subsetI)
    1.32 +  apply (erule CollectE)
    1.33 +  apply (erule conjE)
    1.34 +  apply (rule UN_I)
    1.35 +  apply simp
    1.36 +  apply simp
    1.37 +  apply (rule subsetI)
    1.38 +  apply (erule UN_E)
    1.39 +  apply (case_tac "\<not> stable r step ss p")
    1.40 +  apply simp+
    1.41 +  done
    1.42 +
    1.43 +lemmas [code] = lessThan_0 lessThan_Suc
    1.44 +
    1.45 +constdefs
    1.46 +  some_elem :: "'a set \<Rightarrow> 'a"
    1.47 +  "some_elem == (%S. SOME x. x : S)"
    1.48 +
    1.49 +lemma [code]:
    1.50 +"iter f step ss w =
    1.51 + while (%(ss,w). w \<noteq> {})
    1.52 +       (%(ss,w). let p = some_elem w
    1.53 +                 in propa f (step p (ss!p)) ss (w-{p}))
    1.54 +       (ss,w)"
    1.55 +  by (unfold iter_def some_elem_def, rule refl)
    1.56 +
    1.57 +types_code
    1.58 +  set ("_ list")
    1.59 +
    1.60 +consts_code
    1.61 +  "{}"     ("[]")
    1.62 +  "insert" ("(_ ins _)")
    1.63 +  "op :"   ("(_ mem _)")
    1.64 +  "op Un"  ("(_ union _)")
    1.65 +  "image"  ("map")
    1.66 +  "UNION"  ("(fn A => fn f => flat (map f A))")
    1.67 +  "Bex"    ("(fn A => fn f => exists f A)")
    1.68 +  "Ball"   ("(fn A => fn f => forall f A)")
    1.69 +  "some_elem" ("hd")
    1.70 +  "op -" :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"  ("(_ \\ _)")
    1.71 +
    1.72 +lemma JVM_sup_unfold [code]:
    1.73 + "JVMType.sup S m n = lift2 (Opt.sup
    1.74 +       (Product.sup (Listn.sup (JType.sup S))
    1.75 +         (\<lambda>x y. OK (map2 (lift2 (JType.sup S)) x y))))" 
    1.76 +  apply (unfold JVMType.sup_def JVMType.sl_def Opt.esl_def Err.sl_def
    1.77 +         stk_esl_def reg_sl_def Product.esl_def  
    1.78 +         Listn.sl_def upto_esl_def JType.esl_def Err.esl_def) 
    1.79 +  by simp
    1.80 +
    1.81 +lemmas [code] =
    1.82 +  meta_eq_to_obj_eq [OF JType.sup_def [unfolded exec_lub_def]]
    1.83 +  meta_eq_to_obj_eq [OF JVM_le_unfold]
    1.84 +
    1.85 +lemmas [code ind] = rtrancl_refl converse_rtrancl_into_rtrancl
    1.86 +
    1.87 +generate_code
    1.88 +  test1 = "test_kil E list_name [Class list_name] (PrimT Void) 3 0
    1.89 +    [(Suc 0, 2, 8, Xcpt NullPointer)] append_ins"
    1.90 +  test2 = "test_kil E test_name [] (PrimT Void) 3 2 [] make_list_ins"
    1.91 +
    1.92 +ML test1
    1.93 +ML test2
    1.94 +
    1.95  end