doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
changeset 22473 753123c89d72
parent 22423 c1836b14c63a
child 22479 de15ea8fb348
     1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Mon Mar 19 19:28:27 2007 +0100
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Tue Mar 20 08:27:15 2007 +0100
     1.3 @@ -141,12 +141,10 @@
     1.4    most cases code generation proceeds without further ado:
     1.5  *}
     1.6  
     1.7 -consts
     1.8 -  fac :: "nat \<Rightarrow> nat"
     1.9 -
    1.10 -primrec
    1.11 -  "fac 0 = 1"
    1.12 -  "fac (Suc n) = Suc n * fac n"
    1.13 +fun
    1.14 +  fac :: "nat \<Rightarrow> nat" where
    1.15 +    "fac 0 = 1"
    1.16 +  | "fac (Suc n) = Suc n * fac n"
    1.17  
    1.18  text {*
    1.19    This executable specification is now turned to SML code:
    1.20 @@ -324,7 +322,7 @@
    1.21    assigning to each of its inhabitants a \qt{null} value:
    1.22  *}
    1.23  
    1.24 -class null =
    1.25 +class null = type +
    1.26    fixes null :: 'a
    1.27  
    1.28  consts
    1.29 @@ -551,9 +549,6 @@
    1.30  fun
    1.31    in_interval :: "nat \<times> nat \<Rightarrow> nat \<Rightarrow> bool" where
    1.32    "in_interval (k, l) n \<longleftrightarrow> k \<le> n \<and> n \<le> l"
    1.33 -(*<*)
    1.34 -declare in_interval.simps [code func]
    1.35 -(*>*)
    1.36  
    1.37  (*<*)
    1.38  code_type %tt bool
    1.39 @@ -716,15 +711,12 @@
    1.40  
    1.41  fun
    1.42    collect_duplicates :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    1.43 -  "collect_duplicates xs ys [] = xs"
    1.44 -  "collect_duplicates xs ys (z#zs) = (if z \<in> set xs
    1.45 -    then if z \<in> set ys
    1.46 -      then collect_duplicates xs ys zs
    1.47 -      else collect_duplicates xs (z#ys) zs
    1.48 -    else collect_duplicates (z#xs) (z#ys) zs)"
    1.49 -(*<*)
    1.50 -lemmas [code func] = collect_duplicates.simps
    1.51 -(*>*)
    1.52 +    "collect_duplicates xs ys [] = xs"
    1.53 +  | "collect_duplicates xs ys (z#zs) = (if z \<in> set xs
    1.54 +      then if z \<in> set ys
    1.55 +        then collect_duplicates xs ys zs
    1.56 +        else collect_duplicates xs (z#ys) zs
    1.57 +      else collect_duplicates (z#xs) (z#ys) zs)"
    1.58  
    1.59  text {*
    1.60    The membership test during preprocessing is rewritten,
    1.61 @@ -749,7 +741,7 @@
    1.62  consts "op =" :: "'a"
    1.63  (*>*)
    1.64  
    1.65 -class eq (attach "op =") = notes reflexive
    1.66 +class eq (attach "op =") = type
    1.67  
    1.68  text {*
    1.69    This merely introduces a class @{text eq} with corresponding
    1.70 @@ -782,11 +774,8 @@
    1.71  
    1.72  fun
    1.73    lookup :: "(key \<times> 'a) list \<Rightarrow> key \<Rightarrow> 'a option" where
    1.74 -  "lookup [] l = None"
    1.75 -  "lookup ((k, v) # xs) l = (if k = l then Some v else lookup xs l)"
    1.76 -(*<*)
    1.77 -lemmas [code func] = lookup.simps
    1.78 -(*>*)
    1.79 +    "lookup [] l = None"
    1.80 +  | "lookup ((k, v) # xs) l = (if k = l then Some v else lookup xs l)"
    1.81  
    1.82  code_type %tt key
    1.83    (SML "string")
    1.84 @@ -883,7 +872,7 @@
    1.85  
    1.86  (*<*)
    1.87  setup {* Sign.add_path "bar" *}
    1.88 -class eq = fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    1.89 +class eq = type + fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    1.90  (*>*)
    1.91  
    1.92  code_class %tt eq
    1.93 @@ -1091,11 +1080,8 @@
    1.94  
    1.95  fun
    1.96    dummy_option :: "'a list \<Rightarrow> 'a option" where
    1.97 -  "dummy_option (x#xs) = Some x"
    1.98 -  "dummy_option [] = arbitrary"
    1.99 -(*<*)
   1.100 -declare dummy_option.simps [code func]
   1.101 -(*>*)
   1.102 +    "dummy_option (x#xs) = Some x"
   1.103 +  | "dummy_option [] = arbitrary"
   1.104  
   1.105  code_gen dummy_option (*<*)(SML #)(*>*)(SML "examples/arbitrary.ML")
   1.106