added example for operational classes and code generator
authorhaftmann
Fri Mar 17 14:20:24 2006 +0100 (2006-03-17)
changeset 19281b411f25fff25
parent 19280 5091dc43817b
child 19282 89949d8652c3
added example for operational classes and code generator
src/HOL/ex/Classpackage.thy
src/HOL/ex/Codegenerator.thy
src/HOL/ex/ROOT.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/ex/Classpackage.thy	Fri Mar 17 14:20:24 2006 +0100
     1.3 @@ -0,0 +1,323 @@
     1.4 +(*  ID:         $Id$
     1.5 +    Author:     Florian Haftmann, TU Muenchen
     1.6 +*)
     1.7 +
     1.8 +header {* Test and Examples for Pure/Tools/class_package.ML *}
     1.9 +
    1.10 +theory Classpackage
    1.11 +imports Main
    1.12 +begin
    1.13 +
    1.14 +class semigroup =
    1.15 +  fixes mult :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>\<otimes>" 70)
    1.16 +  assumes assoc: "x \<^loc>\<otimes> y \<^loc>\<otimes> z = x \<^loc>\<otimes> (y \<^loc>\<otimes> z)"
    1.17 +
    1.18 +instance nat :: semigroup
    1.19 +  "m \<otimes> n == (m::nat) + n"
    1.20 +proof
    1.21 +  fix m n q :: nat 
    1.22 +  from semigroup_nat_def show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)" by simp
    1.23 +qed
    1.24 +
    1.25 +instance int :: semigroup
    1.26 +  "k \<otimes> l == (k::int) + l"
    1.27 +proof
    1.28 +  fix k l j :: int
    1.29 +  from semigroup_int_def show "k \<otimes> l \<otimes> j = k \<otimes> (l \<otimes> j)" by simp
    1.30 +qed
    1.31 +
    1.32 +instance (type) list :: semigroup
    1.33 +  "xs \<otimes> ys == xs @ ys"
    1.34 +proof
    1.35 +  fix xs ys zs :: "'a list"
    1.36 +  show "xs \<otimes> ys \<otimes> zs = xs \<otimes> (ys \<otimes> zs)"
    1.37 +  proof -
    1.38 +    from semigroup_list_def have "\<And>xs ys::'a list. xs \<otimes> ys == xs @ ys".
    1.39 +    thus ?thesis by simp
    1.40 +  qed
    1.41 +qed
    1.42 +
    1.43 +class monoidl = semigroup +
    1.44 +  fixes one :: 'a ("\<^loc>\<one>")
    1.45 +  assumes neutl: "\<^loc>\<one> \<^loc>\<otimes> x = x"
    1.46 +
    1.47 +instance nat :: monoidl
    1.48 +  "\<one> == (0::nat)"
    1.49 +proof
    1.50 +  fix n :: nat
    1.51 +  from semigroup_nat_def monoidl_nat_def show "\<one> \<otimes> n = n" by simp
    1.52 +qed
    1.53 +
    1.54 +instance int :: monoidl
    1.55 +  "\<one> == (0::int)"
    1.56 +proof
    1.57 +  fix k :: int
    1.58 +  from semigroup_int_def monoidl_int_def show "\<one> \<otimes> k = k" by simp
    1.59 +qed
    1.60 +
    1.61 +instance (type) list :: monoidl
    1.62 +  "\<one> == []"
    1.63 +proof
    1.64 +  fix xs :: "'a list"
    1.65 +  show "\<one> \<otimes> xs = xs"
    1.66 +  proof -
    1.67 +    from semigroup_list_def have "\<And>xs ys::'a list. xs \<otimes> ys == xs @ ys".
    1.68 +    moreover from monoidl_list_def have "\<one> == []::'a list".
    1.69 +    ultimately show ?thesis by simp
    1.70 +  qed
    1.71 +qed  
    1.72 +
    1.73 +class monoid = monoidl +
    1.74 +  assumes neutr: "x \<^loc>\<otimes> \<^loc>\<one> = x"
    1.75 +
    1.76 +instance (type) list :: monoid
    1.77 +proof
    1.78 +  fix xs :: "'a list"
    1.79 +  show "xs \<otimes> \<one> = xs"
    1.80 +  proof -
    1.81 +    from semigroup_list_def have "\<And>xs ys::'a list. xs \<otimes> ys == xs @ ys".
    1.82 +    moreover from monoidl_list_def have "\<one> == []::'a list".
    1.83 +    ultimately show ?thesis by simp
    1.84 +  qed
    1.85 +qed  
    1.86 +
    1.87 +class monoid_comm = monoid +
    1.88 +  assumes comm: "x \<^loc>\<otimes> y = y \<^loc>\<otimes> x"
    1.89 +
    1.90 +instance nat :: monoid_comm
    1.91 +proof
    1.92 +  fix n :: nat
    1.93 +  from semigroup_nat_def monoidl_nat_def show "n \<otimes> \<one> = n" by simp
    1.94 +next
    1.95 +  fix n m :: nat
    1.96 +  from semigroup_nat_def monoidl_nat_def show "n \<otimes> m = m \<otimes> n" by simp
    1.97 +qed
    1.98 +
    1.99 +instance int :: monoid_comm
   1.100 +proof
   1.101 +  fix k :: int
   1.102 +  from semigroup_int_def monoidl_int_def show "k \<otimes> \<one> = k" by simp
   1.103 +next
   1.104 +  fix k l :: int
   1.105 +  from semigroup_int_def monoidl_int_def show "k \<otimes> l = l \<otimes> k" by simp
   1.106 +qed
   1.107 +
   1.108 +definition (in monoid)
   1.109 +  units :: "'a set"
   1.110 +  units_def: "units = { y. \<exists>x. x \<^loc>\<otimes> y = \<^loc>\<one> \<and> y \<^loc>\<otimes> x = \<^loc>\<one> }"
   1.111 +
   1.112 +lemma (in monoid) inv_obtain:
   1.113 +  assumes ass: "x \<in> units"
   1.114 +  obtains y where "y \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> y = \<^loc>\<one>"
   1.115 +proof -
   1.116 +  from ass units_def obtain y
   1.117 +    where "y \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> y = \<^loc>\<one>" by auto
   1.118 +  thus ?thesis ..
   1.119 +qed
   1.120 +
   1.121 +lemma (in monoid) inv_unique:
   1.122 +  assumes eq: "y \<^loc>\<otimes> x = \<^loc>\<one>" "x \<^loc>\<otimes> y' = \<^loc>\<one>"
   1.123 +  shows "y = y'"
   1.124 +proof -
   1.125 +  from eq neutr have "y = y \<^loc>\<otimes> (x \<^loc>\<otimes> y')" by simp
   1.126 +  also with assoc have "... = (y \<^loc>\<otimes> x) \<^loc>\<otimes> y'" by simp
   1.127 +  also with eq neutl have "... = y'" by simp
   1.128 +  finally show ?thesis .
   1.129 +qed
   1.130 +
   1.131 +lemma (in monoid) units_inv_comm:
   1.132 +  assumes inv: "x \<^loc>\<otimes> y = \<^loc>\<one>"
   1.133 +    and G: "x \<in> units"
   1.134 +  shows "y \<^loc>\<otimes> x = \<^loc>\<one>"
   1.135 +proof -
   1.136 +  from G inv_obtain obtain z
   1.137 +    where z_choice: "z \<^loc>\<otimes> x = \<^loc>\<one>" by blast
   1.138 +  from inv neutl neutr have "x \<^loc>\<otimes> y \<^loc>\<otimes> x = x \<^loc>\<otimes> \<^loc>\<one>" by simp
   1.139 +  with assoc have "z \<^loc>\<otimes> x \<^loc>\<otimes> y \<^loc>\<otimes> x = z \<^loc>\<otimes> x \<^loc>\<otimes> \<^loc>\<one>" by simp
   1.140 +  with neutl z_choice show ?thesis by simp
   1.141 +qed
   1.142 +
   1.143 +consts
   1.144 +  reduce :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"
   1.145 +
   1.146 +primrec
   1.147 +  "reduce f g 0 x = g"
   1.148 +  "reduce f g (Suc n) x = f x (reduce f g n x)"
   1.149 +
   1.150 +definition (in monoid)
   1.151 +  npow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"
   1.152 +  npow_def_prim: "npow n x = reduce (op \<^loc>\<otimes>) \<^loc>\<one> n x"
   1.153 +
   1.154 +abbreviation (in monoid)
   1.155 +  abbrev_npow :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75)
   1.156 +    "(x \<^loc>\<up> n) = npow n x"
   1.157 +
   1.158 +lemma (in monoid) npow_def:
   1.159 +  "x \<^loc>\<up> 0 = \<^loc>\<one>"
   1.160 +  "x \<^loc>\<up> Suc n = x \<^loc>\<otimes> x \<^loc>\<up> n"
   1.161 +using npow_def_prim by simp_all
   1.162 +
   1.163 +lemma (in monoid) nat_pow_one:
   1.164 +  "\<^loc>\<one> \<^loc>\<up> n = \<^loc>\<one>"
   1.165 +using npow_def neutl by (induct n) simp_all
   1.166 +
   1.167 +lemma (in monoid) nat_pow_mult:
   1.168 +  "npow n x \<^loc>\<otimes> npow m x = npow (n + m) x"
   1.169 +proof (induct n)
   1.170 +  case 0 with neutl npow_def show ?case by simp
   1.171 +next
   1.172 +  case (Suc n) with prems assoc npow_def show ?case by simp
   1.173 +qed
   1.174 +
   1.175 +lemma (in monoid) nat_pow_pow:
   1.176 +  "npow n (npow m x) = npow (n * m) x"
   1.177 +using npow_def nat_pow_mult by (induct n) simp_all
   1.178 +
   1.179 +class group = monoidl +
   1.180 +  fixes inv :: "'a \<Rightarrow> 'a" ("\<^loc>\<div> _" [81] 80)
   1.181 +  assumes invl: "\<^loc>\<div> x \<^loc>\<otimes> x = \<^loc>\<one>"
   1.182 +
   1.183 +class group_comm = group + monoid_comm
   1.184 +
   1.185 +instance int :: group_comm
   1.186 +  "\<div> k == - (k::int)"
   1.187 +proof
   1.188 +  fix k :: int
   1.189 +  from semigroup_int_def monoidl_int_def group_comm_int_def show "\<div> k \<otimes> k = \<one>" by simp
   1.190 +qed
   1.191 +
   1.192 +lemma (in group) cancel:
   1.193 +  "(x \<^loc>\<otimes> y = x \<^loc>\<otimes> z) = (y = z)"
   1.194 +proof
   1.195 +  fix x y z :: 'a
   1.196 +  assume eq: "x \<^loc>\<otimes> y = x \<^loc>\<otimes> z"
   1.197 +  hence "\<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> y) = \<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> z)" by simp
   1.198 +  with assoc have "\<^loc>\<div> x \<^loc>\<otimes> x \<^loc>\<otimes> y = \<^loc>\<div> x \<^loc>\<otimes> x \<^loc>\<otimes> z" by simp
   1.199 +  with neutl invl show "y = z" by simp
   1.200 +next
   1.201 +  fix x y z :: 'a
   1.202 +  assume eq: "y = z"
   1.203 +  thus "x \<^loc>\<otimes> y = x \<^loc>\<otimes> z" by simp
   1.204 +qed
   1.205 +
   1.206 +lemma (in group) neutr:
   1.207 +  "x \<^loc>\<otimes> \<^loc>\<one> = x"
   1.208 +proof -
   1.209 +  from invl have "\<^loc>\<div> x \<^loc>\<otimes> x = \<^loc>\<one>" by simp
   1.210 +  with assoc [symmetric] neutl invl have "\<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<one>) = \<^loc>\<div> x \<^loc>\<otimes> x" by simp
   1.211 +  with cancel show ?thesis by simp
   1.212 +qed
   1.213 +
   1.214 +lemma (in group) invr:
   1.215 +  "x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<one>"
   1.216 +proof -
   1.217 +  from neutl invl have "\<^loc>\<div> x \<^loc>\<otimes> x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<div> x" by simp
   1.218 +  with neutr have "\<^loc>\<div> x \<^loc>\<otimes> x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<div> x \<^loc>\<otimes> \<^loc>\<one> " by simp
   1.219 +  with assoc have "\<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<div> x) = \<^loc>\<div> x \<^loc>\<otimes> \<^loc>\<one> " by simp
   1.220 +  with cancel show ?thesis ..
   1.221 +qed
   1.222 +
   1.223 +interpretation group < monoid
   1.224 +proof
   1.225 +  fix x :: "'a"
   1.226 +  from neutr show "x \<^loc>\<otimes> \<^loc>\<one> = x" .
   1.227 +qed
   1.228 +
   1.229 +instance group < monoid
   1.230 +proof
   1.231 +  fix x :: "'a::group"
   1.232 +  from group.mult_one.neutr [standard] show "x \<otimes> \<one> = x" .
   1.233 +qed
   1.234 +
   1.235 +lemma (in group) all_inv [intro]:
   1.236 +  "(x::'a) \<in> monoid.units (op \<^loc>\<otimes>) \<^loc>\<one>"
   1.237 +  unfolding units_def
   1.238 +proof -
   1.239 +  fix x :: "'a"
   1.240 +  from invl invr have "\<^loc>\<div> x \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<one>" . 
   1.241 +  then obtain y where "y \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> y = \<^loc>\<one>" ..
   1.242 +  hence "\<exists>y\<Colon>'a. y \<^loc>\<otimes> x = \<^loc>\<one> \<and> x \<^loc>\<otimes> y = \<^loc>\<one>" by blast
   1.243 +  thus "x \<in> {y\<Colon>'a. \<exists>x\<Colon>'a. x \<^loc>\<otimes> y = \<^loc>\<one> \<and> y \<^loc>\<otimes> x = \<^loc>\<one>}" by simp
   1.244 +qed
   1.245 +
   1.246 +lemma (in group) cancer:
   1.247 +  "(y \<^loc>\<otimes> x = z \<^loc>\<otimes> x) = (y = z)"
   1.248 +proof
   1.249 +  assume eq: "y \<^loc>\<otimes> x = z \<^loc>\<otimes> x"
   1.250 +  with assoc [symmetric] have "y \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<div> x) = z \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<div> x)" by (simp del: invr)
   1.251 +  with invr neutr show "y = z" by simp
   1.252 +next
   1.253 +  assume eq: "y = z"
   1.254 +  thus "y \<^loc>\<otimes> x = z \<^loc>\<otimes> x" by simp
   1.255 +qed
   1.256 +
   1.257 +lemma (in group) inv_one:
   1.258 +  "\<^loc>\<div> \<^loc>\<one> = \<^loc>\<one>"
   1.259 +proof -
   1.260 +  from neutl have "\<^loc>\<div> \<^loc>\<one> = \<^loc>\<one> \<^loc>\<otimes> (\<^loc>\<div> \<^loc>\<one>)" ..
   1.261 +  moreover from invr have "... = \<^loc>\<one>" by simp
   1.262 +  finally show ?thesis .
   1.263 +qed
   1.264 +
   1.265 +lemma (in group) inv_inv:
   1.266 +  "\<^loc>\<div> (\<^loc>\<div> x) = x"
   1.267 +proof -
   1.268 +  from invl invr neutr
   1.269 +    have "\<^loc>\<div> (\<^loc>\<div> x) \<^loc>\<otimes> \<^loc>\<div> x \<^loc>\<otimes> x = x \<^loc>\<otimes> \<^loc>\<div> x \<^loc>\<otimes> x" by simp
   1.270 +  with assoc [symmetric]
   1.271 +    have "\<^loc>\<div> (\<^loc>\<div> x) \<^loc>\<otimes> (\<^loc>\<div> x \<^loc>\<otimes> x) = x \<^loc>\<otimes> (\<^loc>\<div> x \<^loc>\<otimes> x)" by simp
   1.272 +  with invl neutr show ?thesis by simp
   1.273 +qed
   1.274 +
   1.275 +lemma (in group) inv_mult_group:
   1.276 +  "\<^loc>\<div> (x \<^loc>\<otimes> y) = \<^loc>\<div> y \<^loc>\<otimes> \<^loc>\<div> x"
   1.277 +proof -
   1.278 +  from invl have "\<^loc>\<div> (x \<^loc>\<otimes> y) \<^loc>\<otimes> (x \<^loc>\<otimes> y) = \<^loc>\<one>" by simp
   1.279 +  with assoc have "\<^loc>\<div> (x \<^loc>\<otimes> y) \<^loc>\<otimes> x \<^loc>\<otimes> y = \<^loc>\<one>" by simp
   1.280 +  with neutl have "\<^loc>\<div> (x \<^loc>\<otimes> y) \<^loc>\<otimes> x \<^loc>\<otimes> y \<^loc>\<otimes> \<^loc>\<div> y \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<div> y \<^loc>\<otimes> \<^loc>\<div> x" by simp
   1.281 +  with assoc have "\<^loc>\<div> (x \<^loc>\<otimes> y) \<^loc>\<otimes> (x \<^loc>\<otimes> (y \<^loc>\<otimes> \<^loc>\<div> y) \<^loc>\<otimes> \<^loc>\<div> x) = \<^loc>\<div> y \<^loc>\<otimes> \<^loc>\<div> x" by simp
   1.282 +  with invr neutr show ?thesis by simp
   1.283 +qed
   1.284 +
   1.285 +lemma (in group) inv_comm:
   1.286 +  "x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<div> x \<^loc>\<otimes> x"
   1.287 +using invr invl by simp
   1.288 +
   1.289 +definition (in group)
   1.290 +  pow :: "int \<Rightarrow> 'a \<Rightarrow> 'a"
   1.291 +  pow_def: "pow k x = (if k < 0 then \<^loc>\<div> (monoid.npow (op \<^loc>\<otimes>) \<^loc>\<one> (nat (-k)) x)
   1.292 +    else (monoid.npow (op \<^loc>\<otimes>) \<^loc>\<one> (nat k) x))"
   1.293 +
   1.294 +abbreviation (in group)
   1.295 +  abbrev_pow :: "'a \<Rightarrow> int \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75)
   1.296 +    "(x \<^loc>\<up> k) = pow k x"
   1.297 +
   1.298 +lemma (in group) int_pow_zero:
   1.299 +  "x \<^loc>\<up> (0::int) = \<^loc>\<one>"
   1.300 +using npow_def pow_def by simp
   1.301 +
   1.302 +lemma (in group) int_pow_one:
   1.303 +  "\<^loc>\<one> \<^loc>\<up> (k::int) = \<^loc>\<one>"
   1.304 +using pow_def nat_pow_one inv_one by simp
   1.305 +
   1.306 +instance group_prod_def: (group, group) * :: group
   1.307 +  mult_prod_def: "x \<otimes> y == let (x1, x2) = x in (let (y1, y2) = y in
   1.308 +              (x1 \<otimes> y1, x2 \<otimes> y2))"
   1.309 +  mult_one_def: "\<one> == (\<one>, \<one>)"
   1.310 +  mult_inv_def: "\<div> x == let (x1, x2) = x in (\<div> x1, \<div> x2)"
   1.311 +by default (simp_all add: split_paired_all group_prod_def semigroup.assoc monoidl.neutl group.invl)
   1.312 +
   1.313 +instance group_comm_prod_def: (group_comm, group_comm) * :: group_comm
   1.314 +by default (simp_all add: split_paired_all group_prod_def semigroup.assoc monoidl.neutl group.invl monoid_comm.comm)
   1.315 +
   1.316 +definition
   1.317 +  "x = ((2::nat) \<otimes> \<one> \<otimes> 3, (2::int) \<otimes> \<one> \<otimes> \<div> 3, [1::nat, 2] \<otimes> \<one> \<otimes> [1, 2, 3])"
   1.318 +  "y = (2 :: int, \<div> 2 :: int) \<otimes> \<one> \<otimes> (3, \<div> 3)"
   1.319 +
   1.320 +code_generate "op \<otimes>" "\<one>" "inv"
   1.321 +code_generate x
   1.322 +code_generate y
   1.323 +
   1.324 +code_serialize ml (-)
   1.325 +
   1.326 +end
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/ex/Codegenerator.thy	Fri Mar 17 14:20:24 2006 +0100
     2.3 @@ -0,0 +1,133 @@
     2.4 +(*  ID:         $Id$
     2.5 +    Author:     Florian Haftmann, TU Muenchen
     2.6 +*)
     2.7 +
     2.8 +header {* Test and Examples for Code Generator *}
     2.9 +
    2.10 +theory Codegenerator
    2.11 +imports Main
    2.12 +begin
    2.13 +
    2.14 +subsection {* booleans *}
    2.15 +
    2.16 +definition
    2.17 +  xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
    2.18 +  "xor p q = ((p | q) & \<not> (p & q))"
    2.19 +
    2.20 +code_generate xor
    2.21 +
    2.22 +subsection {* natural numbers *}
    2.23 +
    2.24 +definition
    2.25 +  one :: nat
    2.26 +  "one = 1"
    2.27 +  n :: nat
    2.28 +  "n = 42"
    2.29 +
    2.30 +code_generate
    2.31 +  "0::nat" "one" n
    2.32 +  "op + :: nat \<Rightarrow> nat \<Rightarrow> nat"
    2.33 +  "op - :: nat \<Rightarrow> nat \<Rightarrow> nat"
    2.34 +  "op * :: nat \<Rightarrow> nat \<Rightarrow> nat"
    2.35 +  "op < :: nat \<Rightarrow> nat \<Rightarrow> bool"
    2.36 +  "op <= :: nat \<Rightarrow> nat \<Rightarrow> bool"
    2.37 +
    2.38 +subsection {* pairs *}
    2.39 +
    2.40 +definition
    2.41 +  swap :: "'a * 'b \<Rightarrow> 'b * 'a"
    2.42 +  "swap p = (let (x, y) = p in (y, x))"
    2.43 +  swapp :: "'a * 'b \<Rightarrow> 'c * 'd \<Rightarrow> ('a * 'c) * ('b * 'd)"
    2.44 +  "swapp = (\<lambda>(x, y) (z, w). ((x, z), (y, w)))"
    2.45 +  appl :: "('a \<Rightarrow> 'b) * 'a \<Rightarrow> 'b"
    2.46 +  "appl p = (let (f, x) = p in f x)"
    2.47 +
    2.48 +code_generate Pair fst snd Let split swap swapp appl
    2.49 +
    2.50 +definition
    2.51 +  k :: "int"
    2.52 +  "k = 42"
    2.53 +
    2.54 +consts
    2.55 +  fac :: "int => int"
    2.56 +
    2.57 +recdef fac "measure nat"
    2.58 +  "fac j = (if j <= 0 then 1 else j * (fac (j - 1)))"
    2.59 +
    2.60 +code_generate
    2.61 +  "0::int" "1::int" k
    2.62 +  "op + :: int \<Rightarrow> int \<Rightarrow> int"
    2.63 +  "op - :: int \<Rightarrow> int \<Rightarrow> int"
    2.64 +  "op * :: int \<Rightarrow> int \<Rightarrow> int"
    2.65 +  "op < :: int \<Rightarrow> int \<Rightarrow> bool"
    2.66 +  "op <= :: int \<Rightarrow> int \<Rightarrow> bool"
    2.67 +  fac
    2.68 +
    2.69 +subsection {* sums *}
    2.70 +
    2.71 +code_generate Inl Inr
    2.72 +
    2.73 +subsection {* options *}
    2.74 +
    2.75 +code_generate None Some
    2.76 +
    2.77 +subsection {* lists *}
    2.78 +
    2.79 +definition
    2.80 +  ps :: "nat list"
    2.81 +  "ps = [2, 3, 5, 7, 11]"
    2.82 +  qs :: "nat list"
    2.83 +  "qs == rev ps"
    2.84 +
    2.85 +code_generate hd tl "op @" ps qs
    2.86 +
    2.87 +subsection {* mutual datatypes *}
    2.88 +
    2.89 +datatype mut1 = Tip | Top mut2
    2.90 +  and mut2 = Tip | Top mut1
    2.91 +
    2.92 +consts
    2.93 +  mut1 :: "mut1 \<Rightarrow> mut1"
    2.94 +  mut2 :: "mut2 \<Rightarrow> mut2"
    2.95 +
    2.96 +primrec
    2.97 +  "mut1 mut1.Tip = mut1.Tip"
    2.98 +  "mut1 (mut1.Top x) = mut1.Top (mut2 x)"
    2.99 +  "mut2 mut2.Tip = mut2.Tip"
   2.100 +  "mut2 (mut2.Top x) = mut2.Top (mut1 x)"
   2.101 +
   2.102 +code_generate mut1 mut2
   2.103 +
   2.104 +subsection {* equalities *}
   2.105 +
   2.106 +code_generate
   2.107 +  "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"
   2.108 +  "op = :: nat \<Rightarrow> nat \<Rightarrow> bool"
   2.109 +  "op = :: int \<Rightarrow> int \<Rightarrow> bool"
   2.110 +  "op = :: 'a * 'b \<Rightarrow> 'a * 'b \<Rightarrow> bool"
   2.111 +  "op = :: 'a + 'b \<Rightarrow> 'a + 'b \<Rightarrow> bool"
   2.112 +  "op = :: 'a option \<Rightarrow> 'a option \<Rightarrow> bool"
   2.113 +  "op = :: 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
   2.114 +  "op = :: mut1 \<Rightarrow> mut1 \<Rightarrow> bool"
   2.115 +  "op = :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
   2.116 +
   2.117 +subsection {* heavy use of names *}
   2.118 +
   2.119 +definition
   2.120 +  f :: nat
   2.121 +  "f = 2"
   2.122 +  g :: nat
   2.123 +  "g = f"
   2.124 +  h :: nat
   2.125 +  "h = g"
   2.126 +
   2.127 +code_alias
   2.128 +  "Codegenerator.f" "Mymod.f"
   2.129 +  "Codegenerator.g" "Mymod.A.f"
   2.130 +  "Codegenerator.h" "Mymod.A.B.f"
   2.131 +
   2.132 +code_generate f g h
   2.133 +
   2.134 +code_serialize ml (-)
   2.135 +
   2.136 +end
   2.137 \ No newline at end of file
     3.1 --- a/src/HOL/ex/ROOT.ML	Fri Mar 17 14:19:24 2006 +0100
     3.2 +++ b/src/HOL/ex/ROOT.ML	Fri Mar 17 14:20:24 2006 +0100
     3.3 @@ -57,6 +57,8 @@
     3.4  
     3.5  time_use_thy "Refute_Examples";
     3.6  time_use_thy "Quickcheck_Examples";
     3.7 +no_document time_use_thy "Classpackage";
     3.8 +no_document time_use_thy "Codegenerator";
     3.9  no_document time_use_thy "nbe";
    3.10  
    3.11  no_document use_thy "Word";