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";