1.1 --- a/doc-src/Codegen/Thy/Adaptation.thy Tue May 19 13:57:51 2009 +0200
1.2 +++ b/doc-src/Codegen/Thy/Adaptation.thy Tue May 19 16:54:55 2009 +0200
1.3 @@ -127,8 +127,8 @@
1.4 Useful for code setups which involve e.g. indexing of
1.5 target-language arrays.
1.6 \item[@{theory "String"}] provides an additional datatype
1.7 - @{typ message_string} which is isomorphic to strings;
1.8 - @{typ message_string}s are mapped to target-language strings.
1.9 + @{typ String.literal} which is isomorphic to strings;
1.10 + @{typ String.literal}s are mapped to target-language strings.
1.11 Useful for code setups which involve e.g. printing (error) messages.
1.12
1.13 \end{description}
2.1 --- a/src/HOL/Code_Eval.thy Tue May 19 13:57:51 2009 +0200
2.2 +++ b/src/HOL/Code_Eval.thy Tue May 19 16:54:55 2009 +0200
2.3 @@ -5,7 +5,7 @@
2.4 header {* Term evaluation using the generic code generator *}
2.5
2.6 theory Code_Eval
2.7 -imports Plain Typerep Code_Index
2.8 +imports Plain Typerep Code_Numeral
2.9 begin
2.10
2.11 subsection {* Term representation *}
2.12 @@ -14,7 +14,7 @@
2.13
2.14 datatype "term" = dummy_term
2.15
2.16 -definition Const :: "message_string \<Rightarrow> typerep \<Rightarrow> term" where
2.17 +definition Const :: "String.literal \<Rightarrow> typerep \<Rightarrow> term" where
2.18 "Const _ _ = dummy_term"
2.19
2.20 definition App :: "term \<Rightarrow> term \<Rightarrow> term" where
2.21 @@ -63,10 +63,7 @@
2.22 let
2.23 val need_inst = not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of})
2.24 andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep};
2.25 - in
2.26 - thy
2.27 - |> need_inst ? add_term_of tyco raw_vs
2.28 - end;
2.29 + in if need_inst then add_term_of tyco raw_vs thy else thy end;
2.30 in
2.31 Code.type_interpretation ensure_term_of
2.32 end
2.33 @@ -102,10 +99,7 @@
2.34 fun ensure_term_of_code (tyco, (raw_vs, cs)) thy =
2.35 let
2.36 val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
2.37 - in
2.38 - thy
2.39 - |> has_inst ? add_term_of_code tyco raw_vs cs
2.40 - end;
2.41 + in if has_inst then add_term_of_code tyco raw_vs cs thy else thy end;
2.42 in
2.43 Code.type_interpretation ensure_term_of_code
2.44 end
2.45 @@ -119,7 +113,7 @@
2.46
2.47 lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
2.48 lemma [code, code del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
2.49 -lemma [code, code del]: "(term_of \<Colon> message_string \<Rightarrow> term) = term_of" ..
2.50 +lemma [code, code del]: "(term_of \<Colon> String.literal \<Rightarrow> term) = term_of" ..
2.51 lemma [code, code del]:
2.52 "(Code_Eval.term_of \<Colon> 'a::{type, term_of} Predicate.pred \<Rightarrow> Code_Eval.term) = Code_Eval.term_of" ..
2.53 lemma [code, code del]:
2.54 @@ -137,7 +131,7 @@
2.55 code_const Const and App
2.56 (Eval "Term.Const/ (_, _)" and "Term.$/ (_, _)")
2.57
2.58 -code_const "term_of \<Colon> message_string \<Rightarrow> term"
2.59 +code_const "term_of \<Colon> String.literal \<Rightarrow> term"
2.60 (Eval "HOLogic.mk'_message'_string")
2.61
2.62 code_reserved Eval HOLogic
2.63 @@ -215,8 +209,8 @@
2.64 else termify (uminus :: int \<Rightarrow> int) <\<cdot>> (termify (number_of :: int \<Rightarrow> int) <\<cdot>> term_of_num (2::int) (- k)))"
2.65 by (simp only: term_of_anything)
2.66
2.67 -lemma (in term_syntax) term_of_index_code [code]:
2.68 - "term_of (k::index) = termify (number_of :: int \<Rightarrow> index) <\<cdot>> term_of_num (2::index) k"
2.69 +lemma (in term_syntax) term_of_code_numeral_code [code]:
2.70 + "term_of (k::code_numeral) = termify (number_of :: int \<Rightarrow> code_numeral) <\<cdot>> term_of_num (2::code_numeral) k"
2.71 by (simp only: term_of_anything)
2.72
2.73 subsection {* Obfuscate *}
3.1 --- a/src/HOL/Code_Index.thy Tue May 19 13:57:51 2009 +0200
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,325 +0,0 @@
3.4 -(* Author: Florian Haftmann, TU Muenchen *)
3.5 -
3.6 -header {* Type of indices *}
3.7 -
3.8 -theory Code_Index
3.9 -imports Nat_Numeral
3.10 -begin
3.11 -
3.12 -text {*
3.13 - Indices are isomorphic to HOL @{typ nat} but
3.14 - mapped to target-language builtin integers.
3.15 -*}
3.16 -
3.17 -subsection {* Datatype of indices *}
3.18 -
3.19 -typedef (open) index = "UNIV \<Colon> nat set"
3.20 - morphisms nat_of of_nat by rule
3.21 -
3.22 -lemma of_nat_nat_of [simp]:
3.23 - "of_nat (nat_of k) = k"
3.24 - by (rule nat_of_inverse)
3.25 -
3.26 -lemma nat_of_of_nat [simp]:
3.27 - "nat_of (of_nat n) = n"
3.28 - by (rule of_nat_inverse) (rule UNIV_I)
3.29 -
3.30 -lemma [measure_function]:
3.31 - "is_measure nat_of" by (rule is_measure_trivial)
3.32 -
3.33 -lemma index:
3.34 - "(\<And>n\<Colon>index. PROP P n) \<equiv> (\<And>n\<Colon>nat. PROP P (of_nat n))"
3.35 -proof
3.36 - fix n :: nat
3.37 - assume "\<And>n\<Colon>index. PROP P n"
3.38 - then show "PROP P (of_nat n)" .
3.39 -next
3.40 - fix n :: index
3.41 - assume "\<And>n\<Colon>nat. PROP P (of_nat n)"
3.42 - then have "PROP P (of_nat (nat_of n))" .
3.43 - then show "PROP P n" by simp
3.44 -qed
3.45 -
3.46 -lemma index_case:
3.47 - assumes "\<And>n. k = of_nat n \<Longrightarrow> P"
3.48 - shows P
3.49 - by (rule assms [of "nat_of k"]) simp
3.50 -
3.51 -lemma index_induct_raw:
3.52 - assumes "\<And>n. P (of_nat n)"
3.53 - shows "P k"
3.54 -proof -
3.55 - from assms have "P (of_nat (nat_of k))" .
3.56 - then show ?thesis by simp
3.57 -qed
3.58 -
3.59 -lemma nat_of_inject [simp]:
3.60 - "nat_of k = nat_of l \<longleftrightarrow> k = l"
3.61 - by (rule nat_of_inject)
3.62 -
3.63 -lemma of_nat_inject [simp]:
3.64 - "of_nat n = of_nat m \<longleftrightarrow> n = m"
3.65 - by (rule of_nat_inject) (rule UNIV_I)+
3.66 -
3.67 -instantiation index :: zero
3.68 -begin
3.69 -
3.70 -definition [simp, code del]:
3.71 - "0 = of_nat 0"
3.72 -
3.73 -instance ..
3.74 -
3.75 -end
3.76 -
3.77 -definition [simp]:
3.78 - "Suc_index k = of_nat (Suc (nat_of k))"
3.79 -
3.80 -rep_datatype "0 \<Colon> index" Suc_index
3.81 -proof -
3.82 - fix P :: "index \<Rightarrow> bool"
3.83 - fix k :: index
3.84 - assume "P 0" then have init: "P (of_nat 0)" by simp
3.85 - assume "\<And>k. P k \<Longrightarrow> P (Suc_index k)"
3.86 - then have "\<And>n. P (of_nat n) \<Longrightarrow> P (Suc_index (of_nat n))" .
3.87 - then have step: "\<And>n. P (of_nat n) \<Longrightarrow> P (of_nat (Suc n))" by simp
3.88 - from init step have "P (of_nat (nat_of k))"
3.89 - by (induct "nat_of k") simp_all
3.90 - then show "P k" by simp
3.91 -qed simp_all
3.92 -
3.93 -declare index_case [case_names nat, cases type: index]
3.94 -declare index.induct [case_names nat, induct type: index]
3.95 -
3.96 -lemma index_decr [termination_simp]:
3.97 - "k \<noteq> Code_Index.of_nat 0 \<Longrightarrow> Code_Index.nat_of k - Suc 0 < Code_Index.nat_of k"
3.98 - by (cases k) simp
3.99 -
3.100 -lemma [simp, code]:
3.101 - "index_size = nat_of"
3.102 -proof (rule ext)
3.103 - fix k
3.104 - have "index_size k = nat_size (nat_of k)"
3.105 - by (induct k rule: index.induct) (simp_all del: zero_index_def Suc_index_def, simp_all)
3.106 - also have "nat_size (nat_of k) = nat_of k" by (induct "nat_of k") simp_all
3.107 - finally show "index_size k = nat_of k" .
3.108 -qed
3.109 -
3.110 -lemma [simp, code]:
3.111 - "size = nat_of"
3.112 -proof (rule ext)
3.113 - fix k
3.114 - show "size k = nat_of k"
3.115 - by (induct k) (simp_all del: zero_index_def Suc_index_def, simp_all)
3.116 -qed
3.117 -
3.118 -lemmas [code del] = index.recs index.cases
3.119 -
3.120 -lemma [code]:
3.121 - "eq_class.eq k l \<longleftrightarrow> eq_class.eq (nat_of k) (nat_of l)"
3.122 - by (cases k, cases l) (simp add: eq)
3.123 -
3.124 -lemma [code nbe]:
3.125 - "eq_class.eq (k::index) k \<longleftrightarrow> True"
3.126 - by (rule HOL.eq_refl)
3.127 -
3.128 -
3.129 -subsection {* Indices as datatype of ints *}
3.130 -
3.131 -instantiation index :: number
3.132 -begin
3.133 -
3.134 -definition
3.135 - "number_of = of_nat o nat"
3.136 -
3.137 -instance ..
3.138 -
3.139 -end
3.140 -
3.141 -lemma nat_of_number [simp]:
3.142 - "nat_of (number_of k) = number_of k"
3.143 - by (simp add: number_of_index_def nat_number_of_def number_of_is_id)
3.144 -
3.145 -code_datatype "number_of \<Colon> int \<Rightarrow> index"
3.146 -
3.147 -
3.148 -subsection {* Basic arithmetic *}
3.149 -
3.150 -instantiation index :: "{minus, ordered_semidom, semiring_div, linorder}"
3.151 -begin
3.152 -
3.153 -definition [simp, code del]:
3.154 - "(1\<Colon>index) = of_nat 1"
3.155 -
3.156 -definition [simp, code del]:
3.157 - "n + m = of_nat (nat_of n + nat_of m)"
3.158 -
3.159 -definition [simp, code del]:
3.160 - "n - m = of_nat (nat_of n - nat_of m)"
3.161 -
3.162 -definition [simp, code del]:
3.163 - "n * m = of_nat (nat_of n * nat_of m)"
3.164 -
3.165 -definition [simp, code del]:
3.166 - "n div m = of_nat (nat_of n div nat_of m)"
3.167 -
3.168 -definition [simp, code del]:
3.169 - "n mod m = of_nat (nat_of n mod nat_of m)"
3.170 -
3.171 -definition [simp, code del]:
3.172 - "n \<le> m \<longleftrightarrow> nat_of n \<le> nat_of m"
3.173 -
3.174 -definition [simp, code del]:
3.175 - "n < m \<longleftrightarrow> nat_of n < nat_of m"
3.176 -
3.177 -instance proof
3.178 -qed (auto simp add: index left_distrib div_mult_self1)
3.179 -
3.180 -end
3.181 -
3.182 -lemma zero_index_code [code inline, code]:
3.183 - "(0\<Colon>index) = Numeral0"
3.184 - by (simp add: number_of_index_def Pls_def)
3.185 -lemma [code post]: "Numeral0 = (0\<Colon>index)"
3.186 - using zero_index_code ..
3.187 -
3.188 -lemma one_index_code [code inline, code]:
3.189 - "(1\<Colon>index) = Numeral1"
3.190 - by (simp add: number_of_index_def Pls_def Bit1_def)
3.191 -lemma [code post]: "Numeral1 = (1\<Colon>index)"
3.192 - using one_index_code ..
3.193 -
3.194 -lemma plus_index_code [code nbe]:
3.195 - "of_nat n + of_nat m = of_nat (n + m)"
3.196 - by simp
3.197 -
3.198 -definition subtract_index :: "index \<Rightarrow> index \<Rightarrow> index" where
3.199 - [simp, code del]: "subtract_index = op -"
3.200 -
3.201 -lemma subtract_index_code [code nbe]:
3.202 - "subtract_index (of_nat n) (of_nat m) = of_nat (n - m)"
3.203 - by simp
3.204 -
3.205 -lemma minus_index_code [code]:
3.206 - "n - m = subtract_index n m"
3.207 - by simp
3.208 -
3.209 -lemma times_index_code [code nbe]:
3.210 - "of_nat n * of_nat m = of_nat (n * m)"
3.211 - by simp
3.212 -
3.213 -lemma less_eq_index_code [code nbe]:
3.214 - "of_nat n \<le> of_nat m \<longleftrightarrow> n \<le> m"
3.215 - by simp
3.216 -
3.217 -lemma less_index_code [code nbe]:
3.218 - "of_nat n < of_nat m \<longleftrightarrow> n < m"
3.219 - by simp
3.220 -
3.221 -lemma Suc_index_minus_one: "Suc_index n - 1 = n" by simp
3.222 -
3.223 -lemma of_nat_code [code]:
3.224 - "of_nat = Nat.of_nat"
3.225 -proof
3.226 - fix n :: nat
3.227 - have "Nat.of_nat n = of_nat n"
3.228 - by (induct n) simp_all
3.229 - then show "of_nat n = Nat.of_nat n"
3.230 - by (rule sym)
3.231 -qed
3.232 -
3.233 -lemma index_not_eq_zero: "i \<noteq> of_nat 0 \<longleftrightarrow> i \<ge> 1"
3.234 - by (cases i) auto
3.235 -
3.236 -definition nat_of_aux :: "index \<Rightarrow> nat \<Rightarrow> nat" where
3.237 - "nat_of_aux i n = nat_of i + n"
3.238 -
3.239 -lemma nat_of_aux_code [code]:
3.240 - "nat_of_aux i n = (if i = 0 then n else nat_of_aux (i - 1) (Suc n))"
3.241 - by (auto simp add: nat_of_aux_def index_not_eq_zero)
3.242 -
3.243 -lemma nat_of_code [code]:
3.244 - "nat_of i = nat_of_aux i 0"
3.245 - by (simp add: nat_of_aux_def)
3.246 -
3.247 -definition div_mod_index :: "index \<Rightarrow> index \<Rightarrow> index \<times> index" where
3.248 - [code del]: "div_mod_index n m = (n div m, n mod m)"
3.249 -
3.250 -lemma [code]:
3.251 - "div_mod_index n m = (if m = 0 then (0, n) else (n div m, n mod m))"
3.252 - unfolding div_mod_index_def by auto
3.253 -
3.254 -lemma [code]:
3.255 - "n div m = fst (div_mod_index n m)"
3.256 - unfolding div_mod_index_def by simp
3.257 -
3.258 -lemma [code]:
3.259 - "n mod m = snd (div_mod_index n m)"
3.260 - unfolding div_mod_index_def by simp
3.261 -
3.262 -definition int_of :: "index \<Rightarrow> int" where
3.263 - "int_of = Nat.of_nat o nat_of"
3.264 -
3.265 -lemma int_of_code [code]:
3.266 - "int_of k = (if k = 0 then 0
3.267 - else (if k mod 2 = 0 then 2 * int_of (k div 2) else 2 * int_of (k div 2) + 1))"
3.268 - by (auto simp add: int_of_def mod_div_equality')
3.269 -
3.270 -hide (open) const of_nat nat_of int_of
3.271 -
3.272 -
3.273 -subsection {* Code generator setup *}
3.274 -
3.275 -text {* Implementation of indices by bounded integers *}
3.276 -
3.277 -code_type index
3.278 - (SML "int")
3.279 - (OCaml "int")
3.280 - (Haskell "Int")
3.281 -
3.282 -code_instance index :: eq
3.283 - (Haskell -)
3.284 -
3.285 -setup {*
3.286 - fold (Numeral.add_code @{const_name number_index_inst.number_of_index}
3.287 - false false) ["SML", "OCaml", "Haskell"]
3.288 -*}
3.289 -
3.290 -code_reserved SML Int int
3.291 -code_reserved OCaml Pervasives int
3.292 -
3.293 -code_const "op + \<Colon> index \<Rightarrow> index \<Rightarrow> index"
3.294 - (SML "Int.+/ ((_),/ (_))")
3.295 - (OCaml "Pervasives.( + )")
3.296 - (Haskell infixl 6 "+")
3.297 -
3.298 -code_const "subtract_index \<Colon> index \<Rightarrow> index \<Rightarrow> index"
3.299 - (SML "Int.max/ (_/ -/ _,/ 0 : int)")
3.300 - (OCaml "Pervasives.max/ (_/ -/ _)/ (0 : int) ")
3.301 - (Haskell "max/ (_/ -/ _)/ (0 :: Int)")
3.302 -
3.303 -code_const "op * \<Colon> index \<Rightarrow> index \<Rightarrow> index"
3.304 - (SML "Int.*/ ((_),/ (_))")
3.305 - (OCaml "Pervasives.( * )")
3.306 - (Haskell infixl 7 "*")
3.307 -
3.308 -code_const div_mod_index
3.309 - (SML "(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
3.310 - (OCaml "(fun n -> fun m ->/ if m = 0/ then (0, n) else/ (n '/ m, n mod m))")
3.311 - (Haskell "divMod")
3.312 -
3.313 -code_const "eq_class.eq \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
3.314 - (SML "!((_ : Int.int) = _)")
3.315 - (OCaml "!((_ : int) = _)")
3.316 - (Haskell infixl 4 "==")
3.317 -
3.318 -code_const "op \<le> \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
3.319 - (SML "Int.<=/ ((_),/ (_))")
3.320 - (OCaml "!((_ : int) <= _)")
3.321 - (Haskell infix 4 "<=")
3.322 -
3.323 -code_const "op < \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
3.324 - (SML "Int.</ ((_),/ (_))")
3.325 - (OCaml "!((_ : int) < _)")
3.326 - (Haskell infix 4 "<")
3.327 -
3.328 -end
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/HOL/Code_Numeral.thy Tue May 19 16:54:55 2009 +0200
4.3 @@ -0,0 +1,325 @@
4.4 +(* Author: Florian Haftmann, TU Muenchen *)
4.5 +
4.6 +header {* Type of target language numerals *}
4.7 +
4.8 +theory Code_Numeral
4.9 +imports Nat_Numeral
4.10 +begin
4.11 +
4.12 +text {*
4.13 + Code numerals are isomorphic to HOL @{typ nat} but
4.14 + mapped to target-language builtin numerals.
4.15 +*}
4.16 +
4.17 +subsection {* Datatype of target language numerals *}
4.18 +
4.19 +typedef (open) code_numeral = "UNIV \<Colon> nat set"
4.20 + morphisms nat_of of_nat by rule
4.21 +
4.22 +lemma of_nat_nat_of [simp]:
4.23 + "of_nat (nat_of k) = k"
4.24 + by (rule nat_of_inverse)
4.25 +
4.26 +lemma nat_of_of_nat [simp]:
4.27 + "nat_of (of_nat n) = n"
4.28 + by (rule of_nat_inverse) (rule UNIV_I)
4.29 +
4.30 +lemma [measure_function]:
4.31 + "is_measure nat_of" by (rule is_measure_trivial)
4.32 +
4.33 +lemma code_numeral:
4.34 + "(\<And>n\<Colon>code_numeral. PROP P n) \<equiv> (\<And>n\<Colon>nat. PROP P (of_nat n))"
4.35 +proof
4.36 + fix n :: nat
4.37 + assume "\<And>n\<Colon>code_numeral. PROP P n"
4.38 + then show "PROP P (of_nat n)" .
4.39 +next
4.40 + fix n :: code_numeral
4.41 + assume "\<And>n\<Colon>nat. PROP P (of_nat n)"
4.42 + then have "PROP P (of_nat (nat_of n))" .
4.43 + then show "PROP P n" by simp
4.44 +qed
4.45 +
4.46 +lemma code_numeral_case:
4.47 + assumes "\<And>n. k = of_nat n \<Longrightarrow> P"
4.48 + shows P
4.49 + by (rule assms [of "nat_of k"]) simp
4.50 +
4.51 +lemma code_numeral_induct_raw:
4.52 + assumes "\<And>n. P (of_nat n)"
4.53 + shows "P k"
4.54 +proof -
4.55 + from assms have "P (of_nat (nat_of k))" .
4.56 + then show ?thesis by simp
4.57 +qed
4.58 +
4.59 +lemma nat_of_inject [simp]:
4.60 + "nat_of k = nat_of l \<longleftrightarrow> k = l"
4.61 + by (rule nat_of_inject)
4.62 +
4.63 +lemma of_nat_inject [simp]:
4.64 + "of_nat n = of_nat m \<longleftrightarrow> n = m"
4.65 + by (rule of_nat_inject) (rule UNIV_I)+
4.66 +
4.67 +instantiation code_numeral :: zero
4.68 +begin
4.69 +
4.70 +definition [simp, code del]:
4.71 + "0 = of_nat 0"
4.72 +
4.73 +instance ..
4.74 +
4.75 +end
4.76 +
4.77 +definition [simp]:
4.78 + "Suc_code_numeral k = of_nat (Suc (nat_of k))"
4.79 +
4.80 +rep_datatype "0 \<Colon> code_numeral" Suc_code_numeral
4.81 +proof -
4.82 + fix P :: "code_numeral \<Rightarrow> bool"
4.83 + fix k :: code_numeral
4.84 + assume "P 0" then have init: "P (of_nat 0)" by simp
4.85 + assume "\<And>k. P k \<Longrightarrow> P (Suc_code_numeral k)"
4.86 + then have "\<And>n. P (of_nat n) \<Longrightarrow> P (Suc_code_numeral (of_nat n))" .
4.87 + then have step: "\<And>n. P (of_nat n) \<Longrightarrow> P (of_nat (Suc n))" by simp
4.88 + from init step have "P (of_nat (nat_of k))"
4.89 + by (induct "nat_of k") simp_all
4.90 + then show "P k" by simp
4.91 +qed simp_all
4.92 +
4.93 +declare code_numeral_case [case_names nat, cases type: code_numeral]
4.94 +declare code_numeral.induct [case_names nat, induct type: code_numeral]
4.95 +
4.96 +lemma code_numeral_decr [termination_simp]:
4.97 + "k \<noteq> of_nat 0 \<Longrightarrow> nat_of k - Suc 0 < nat_of k"
4.98 + by (cases k) simp
4.99 +
4.100 +lemma [simp, code]:
4.101 + "code_numeral_size = nat_of"
4.102 +proof (rule ext)
4.103 + fix k
4.104 + have "code_numeral_size k = nat_size (nat_of k)"
4.105 + by (induct k rule: code_numeral.induct) (simp_all del: zero_code_numeral_def Suc_code_numeral_def, simp_all)
4.106 + also have "nat_size (nat_of k) = nat_of k" by (induct "nat_of k") simp_all
4.107 + finally show "code_numeral_size k = nat_of k" .
4.108 +qed
4.109 +
4.110 +lemma [simp, code]:
4.111 + "size = nat_of"
4.112 +proof (rule ext)
4.113 + fix k
4.114 + show "size k = nat_of k"
4.115 + by (induct k) (simp_all del: zero_code_numeral_def Suc_code_numeral_def, simp_all)
4.116 +qed
4.117 +
4.118 +lemmas [code del] = code_numeral.recs code_numeral.cases
4.119 +
4.120 +lemma [code]:
4.121 + "eq_class.eq k l \<longleftrightarrow> eq_class.eq (nat_of k) (nat_of l)"
4.122 + by (cases k, cases l) (simp add: eq)
4.123 +
4.124 +lemma [code nbe]:
4.125 + "eq_class.eq (k::code_numeral) k \<longleftrightarrow> True"
4.126 + by (rule HOL.eq_refl)
4.127 +
4.128 +
4.129 +subsection {* Indices as datatype of ints *}
4.130 +
4.131 +instantiation code_numeral :: number
4.132 +begin
4.133 +
4.134 +definition
4.135 + "number_of = of_nat o nat"
4.136 +
4.137 +instance ..
4.138 +
4.139 +end
4.140 +
4.141 +lemma nat_of_number [simp]:
4.142 + "nat_of (number_of k) = number_of k"
4.143 + by (simp add: number_of_code_numeral_def nat_number_of_def number_of_is_id)
4.144 +
4.145 +code_datatype "number_of \<Colon> int \<Rightarrow> code_numeral"
4.146 +
4.147 +
4.148 +subsection {* Basic arithmetic *}
4.149 +
4.150 +instantiation code_numeral :: "{minus, ordered_semidom, semiring_div, linorder}"
4.151 +begin
4.152 +
4.153 +definition [simp, code del]:
4.154 + "(1\<Colon>code_numeral) = of_nat 1"
4.155 +
4.156 +definition [simp, code del]:
4.157 + "n + m = of_nat (nat_of n + nat_of m)"
4.158 +
4.159 +definition [simp, code del]:
4.160 + "n - m = of_nat (nat_of n - nat_of m)"
4.161 +
4.162 +definition [simp, code del]:
4.163 + "n * m = of_nat (nat_of n * nat_of m)"
4.164 +
4.165 +definition [simp, code del]:
4.166 + "n div m = of_nat (nat_of n div nat_of m)"
4.167 +
4.168 +definition [simp, code del]:
4.169 + "n mod m = of_nat (nat_of n mod nat_of m)"
4.170 +
4.171 +definition [simp, code del]:
4.172 + "n \<le> m \<longleftrightarrow> nat_of n \<le> nat_of m"
4.173 +
4.174 +definition [simp, code del]:
4.175 + "n < m \<longleftrightarrow> nat_of n < nat_of m"
4.176 +
4.177 +instance proof
4.178 +qed (auto simp add: code_numeral left_distrib div_mult_self1)
4.179 +
4.180 +end
4.181 +
4.182 +lemma zero_code_numeral_code [code inline, code]:
4.183 + "(0\<Colon>code_numeral) = Numeral0"
4.184 + by (simp add: number_of_code_numeral_def Pls_def)
4.185 +lemma [code post]: "Numeral0 = (0\<Colon>code_numeral)"
4.186 + using zero_code_numeral_code ..
4.187 +
4.188 +lemma one_code_numeral_code [code inline, code]:
4.189 + "(1\<Colon>code_numeral) = Numeral1"
4.190 + by (simp add: number_of_code_numeral_def Pls_def Bit1_def)
4.191 +lemma [code post]: "Numeral1 = (1\<Colon>code_numeral)"
4.192 + using one_code_numeral_code ..
4.193 +
4.194 +lemma plus_code_numeral_code [code nbe]:
4.195 + "of_nat n + of_nat m = of_nat (n + m)"
4.196 + by simp
4.197 +
4.198 +definition subtract_code_numeral :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
4.199 + [simp, code del]: "subtract_code_numeral = op -"
4.200 +
4.201 +lemma subtract_code_numeral_code [code nbe]:
4.202 + "subtract_code_numeral (of_nat n) (of_nat m) = of_nat (n - m)"
4.203 + by simp
4.204 +
4.205 +lemma minus_code_numeral_code [code]:
4.206 + "n - m = subtract_code_numeral n m"
4.207 + by simp
4.208 +
4.209 +lemma times_code_numeral_code [code nbe]:
4.210 + "of_nat n * of_nat m = of_nat (n * m)"
4.211 + by simp
4.212 +
4.213 +lemma less_eq_code_numeral_code [code nbe]:
4.214 + "of_nat n \<le> of_nat m \<longleftrightarrow> n \<le> m"
4.215 + by simp
4.216 +
4.217 +lemma less_code_numeral_code [code nbe]:
4.218 + "of_nat n < of_nat m \<longleftrightarrow> n < m"
4.219 + by simp
4.220 +
4.221 +lemma Suc_code_numeral_minus_one: "Suc_code_numeral n - 1 = n" by simp
4.222 +
4.223 +lemma of_nat_code [code]:
4.224 + "of_nat = Nat.of_nat"
4.225 +proof
4.226 + fix n :: nat
4.227 + have "Nat.of_nat n = of_nat n"
4.228 + by (induct n) simp_all
4.229 + then show "of_nat n = Nat.of_nat n"
4.230 + by (rule sym)
4.231 +qed
4.232 +
4.233 +lemma code_numeral_not_eq_zero: "i \<noteq> of_nat 0 \<longleftrightarrow> i \<ge> 1"
4.234 + by (cases i) auto
4.235 +
4.236 +definition nat_of_aux :: "code_numeral \<Rightarrow> nat \<Rightarrow> nat" where
4.237 + "nat_of_aux i n = nat_of i + n"
4.238 +
4.239 +lemma nat_of_aux_code [code]:
4.240 + "nat_of_aux i n = (if i = 0 then n else nat_of_aux (i - 1) (Suc n))"
4.241 + by (auto simp add: nat_of_aux_def code_numeral_not_eq_zero)
4.242 +
4.243 +lemma nat_of_code [code]:
4.244 + "nat_of i = nat_of_aux i 0"
4.245 + by (simp add: nat_of_aux_def)
4.246 +
4.247 +definition div_mod_code_numeral :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<times> code_numeral" where
4.248 + [code del]: "div_mod_code_numeral n m = (n div m, n mod m)"
4.249 +
4.250 +lemma [code]:
4.251 + "div_mod_code_numeral n m = (if m = 0 then (0, n) else (n div m, n mod m))"
4.252 + unfolding div_mod_code_numeral_def by auto
4.253 +
4.254 +lemma [code]:
4.255 + "n div m = fst (div_mod_code_numeral n m)"
4.256 + unfolding div_mod_code_numeral_def by simp
4.257 +
4.258 +lemma [code]:
4.259 + "n mod m = snd (div_mod_code_numeral n m)"
4.260 + unfolding div_mod_code_numeral_def by simp
4.261 +
4.262 +definition int_of :: "code_numeral \<Rightarrow> int" where
4.263 + "int_of = Nat.of_nat o nat_of"
4.264 +
4.265 +lemma int_of_code [code]:
4.266 + "int_of k = (if k = 0 then 0
4.267 + else (if k mod 2 = 0 then 2 * int_of (k div 2) else 2 * int_of (k div 2) + 1))"
4.268 + by (auto simp add: int_of_def mod_div_equality')
4.269 +
4.270 +hide (open) const of_nat nat_of int_of
4.271 +
4.272 +
4.273 +subsection {* Code generator setup *}
4.274 +
4.275 +text {* Implementation of indices by bounded integers *}
4.276 +
4.277 +code_type code_numeral
4.278 + (SML "int")
4.279 + (OCaml "int")
4.280 + (Haskell "Int")
4.281 +
4.282 +code_instance code_numeral :: eq
4.283 + (Haskell -)
4.284 +
4.285 +setup {*
4.286 + fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
4.287 + false false) ["SML", "OCaml", "Haskell"]
4.288 +*}
4.289 +
4.290 +code_reserved SML Int int
4.291 +code_reserved OCaml Pervasives int
4.292 +
4.293 +code_const "op + \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
4.294 + (SML "Int.+/ ((_),/ (_))")
4.295 + (OCaml "Pervasives.( + )")
4.296 + (Haskell infixl 6 "+")
4.297 +
4.298 +code_const "subtract_code_numeral \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
4.299 + (SML "Int.max/ (_/ -/ _,/ 0 : int)")
4.300 + (OCaml "Pervasives.max/ (_/ -/ _)/ (0 : int) ")
4.301 + (Haskell "max/ (_/ -/ _)/ (0 :: Int)")
4.302 +
4.303 +code_const "op * \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
4.304 + (SML "Int.*/ ((_),/ (_))")
4.305 + (OCaml "Pervasives.( * )")
4.306 + (Haskell infixl 7 "*")
4.307 +
4.308 +code_const div_mod_code_numeral
4.309 + (SML "(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
4.310 + (OCaml "(fun n -> fun m ->/ if m = 0/ then (0, n) else/ (n '/ m, n mod m))")
4.311 + (Haskell "divMod")
4.312 +
4.313 +code_const "eq_class.eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
4.314 + (SML "!((_ : Int.int) = _)")
4.315 + (OCaml "!((_ : int) = _)")
4.316 + (Haskell infixl 4 "==")
4.317 +
4.318 +code_const "op \<le> \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
4.319 + (SML "Int.<=/ ((_),/ (_))")
4.320 + (OCaml "!((_ : int) <= _)")
4.321 + (Haskell infix 4 "<=")
4.322 +
4.323 +code_const "op < \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
4.324 + (SML "Int.</ ((_),/ (_))")
4.325 + (OCaml "!((_ : int) < _)")
4.326 + (Haskell infix 4 "<")
4.327 +
4.328 +end
5.1 --- a/src/HOL/Imperative_HOL/Array.thy Tue May 19 13:57:51 2009 +0200
5.2 +++ b/src/HOL/Imperative_HOL/Array.thy Tue May 19 16:54:55 2009 +0200
5.3 @@ -115,47 +115,47 @@
5.4 subsubsection {* Logical intermediate layer *}
5.5
5.6 definition new' where
5.7 - [code del]: "new' = Array.new o Code_Index.nat_of"
5.8 + [code del]: "new' = Array.new o Code_Numeral.nat_of"
5.9 hide (open) const new'
5.10 lemma [code]:
5.11 - "Array.new = Array.new' o Code_Index.of_nat"
5.12 + "Array.new = Array.new' o Code_Numeral.of_nat"
5.13 by (simp add: new'_def o_def)
5.14
5.15 definition of_list' where
5.16 - [code del]: "of_list' i xs = Array.of_list (take (Code_Index.nat_of i) xs)"
5.17 + [code del]: "of_list' i xs = Array.of_list (take (Code_Numeral.nat_of i) xs)"
5.18 hide (open) const of_list'
5.19 lemma [code]:
5.20 - "Array.of_list xs = Array.of_list' (Code_Index.of_nat (List.length xs)) xs"
5.21 + "Array.of_list xs = Array.of_list' (Code_Numeral.of_nat (List.length xs)) xs"
5.22 by (simp add: of_list'_def)
5.23
5.24 definition make' where
5.25 - [code del]: "make' i f = Array.make (Code_Index.nat_of i) (f o Code_Index.of_nat)"
5.26 + [code del]: "make' i f = Array.make (Code_Numeral.nat_of i) (f o Code_Numeral.of_nat)"
5.27 hide (open) const make'
5.28 lemma [code]:
5.29 - "Array.make n f = Array.make' (Code_Index.of_nat n) (f o Code_Index.nat_of)"
5.30 + "Array.make n f = Array.make' (Code_Numeral.of_nat n) (f o Code_Numeral.nat_of)"
5.31 by (simp add: make'_def o_def)
5.32
5.33 definition length' where
5.34 - [code del]: "length' = Array.length \<guillemotright>== liftM Code_Index.of_nat"
5.35 + [code del]: "length' = Array.length \<guillemotright>== liftM Code_Numeral.of_nat"
5.36 hide (open) const length'
5.37 lemma [code]:
5.38 - "Array.length = Array.length' \<guillemotright>== liftM Code_Index.nat_of"
5.39 + "Array.length = Array.length' \<guillemotright>== liftM Code_Numeral.nat_of"
5.40 by (simp add: length'_def monad_simp',
5.41 simp add: liftM_def comp_def monad_simp,
5.42 simp add: monad_simp')
5.43
5.44 definition nth' where
5.45 - [code del]: "nth' a = Array.nth a o Code_Index.nat_of"
5.46 + [code del]: "nth' a = Array.nth a o Code_Numeral.nat_of"
5.47 hide (open) const nth'
5.48 lemma [code]:
5.49 - "Array.nth a n = Array.nth' a (Code_Index.of_nat n)"
5.50 + "Array.nth a n = Array.nth' a (Code_Numeral.of_nat n)"
5.51 by (simp add: nth'_def)
5.52
5.53 definition upd' where
5.54 - [code del]: "upd' a i x = Array.upd (Code_Index.nat_of i) x a \<guillemotright> return ()"
5.55 + [code del]: "upd' a i x = Array.upd (Code_Numeral.nat_of i) x a \<guillemotright> return ()"
5.56 hide (open) const upd'
5.57 lemma [code]:
5.58 - "Array.upd i x a = Array.upd' a (Code_Index.of_nat i) x \<guillemotright> return a"
5.59 + "Array.upd i x a = Array.upd' a (Code_Numeral.of_nat i) x \<guillemotright> return a"
5.60 by (simp add: upd'_def monad_simp upd_return)
5.61
5.62
6.1 --- a/src/HOL/Imperative_HOL/Heap.thy Tue May 19 13:57:51 2009 +0200
6.2 +++ b/src/HOL/Imperative_HOL/Heap.thy Tue May 19 16:54:55 2009 +0200
6.3 @@ -28,11 +28,11 @@
6.4
6.5 instance int :: heap ..
6.6
6.7 -instance message_string :: countable
6.8 - by (rule countable_classI [of "message_string_case to_nat"])
6.9 - (auto split: message_string.splits)
6.10 +instance String.literal :: countable
6.11 + by (rule countable_classI [of "String.literal_case to_nat"])
6.12 + (auto split: String.literal.splits)
6.13
6.14 -instance message_string :: heap ..
6.15 +instance String.literal :: heap ..
6.16
6.17 text {* Reflected types themselves are heap-representable *}
6.18
7.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy Tue May 19 13:57:51 2009 +0200
7.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Tue May 19 16:54:55 2009 +0200
7.3 @@ -274,7 +274,7 @@
7.4 subsubsection {* Logical intermediate layer *}
7.5
7.6 definition
7.7 - Fail :: "message_string \<Rightarrow> exception"
7.8 + Fail :: "String.literal \<Rightarrow> exception"
7.9 where
7.10 [code del]: "Fail s = Exn"
7.11
8.1 --- a/src/HOL/IsaMakefile Tue May 19 13:57:51 2009 +0200
8.2 +++ b/src/HOL/IsaMakefile Tue May 19 16:54:55 2009 +0200
8.3 @@ -206,7 +206,7 @@
8.4 MAIN_DEPENDENCIES = $(PLAIN_DEPENDENCIES) \
8.5 ATP_Linkup.thy \
8.6 Code_Eval.thy \
8.7 - Code_Index.thy \
8.8 + Code_Numeral.thy \
8.9 Equiv_Relations.thy \
8.10 Groebner_Basis.thy \
8.11 Hilbert_Choice.thy \
9.1 --- a/src/HOL/Library/Code_Integer.thy Tue May 19 13:57:51 2009 +0200
9.2 +++ b/src/HOL/Library/Code_Integer.thy Tue May 19 16:54:55 2009 +0200
9.3 @@ -91,7 +91,7 @@
9.4 (OCaml "Big'_int.lt'_big'_int")
9.5 (Haskell infix 4 "<")
9.6
9.7 -code_const Code_Index.int_of
9.8 +code_const Code_Numeral.int_of
9.9 (SML "IntInf.fromInt")
9.10 (OCaml "Big'_int.big'_int'_of'_int")
9.11 (Haskell "toEnum")
10.1 --- a/src/HOL/Library/Efficient_Nat.thy Tue May 19 13:57:51 2009 +0200
10.2 +++ b/src/HOL/Library/Efficient_Nat.thy Tue May 19 16:54:55 2009 +0200
10.3 @@ -369,12 +369,12 @@
10.4
10.5 text {* Conversion from and to indices. *}
10.6
10.7 -code_const Code_Index.of_nat
10.8 +code_const Code_Numeral.of_nat
10.9 (SML "IntInf.toInt")
10.10 (OCaml "Big'_int.int'_of'_big'_int")
10.11 (Haskell "fromEnum")
10.12
10.13 -code_const Code_Index.nat_of
10.14 +code_const Code_Numeral.nat_of
10.15 (SML "IntInf.fromInt")
10.16 (OCaml "Big'_int.big'_int'_of'_int")
10.17 (Haskell "toEnum")
11.1 --- a/src/HOL/Quickcheck.thy Tue May 19 13:57:51 2009 +0200
11.2 +++ b/src/HOL/Quickcheck.thy Tue May 19 16:54:55 2009 +0200
11.3 @@ -13,7 +13,7 @@
11.4 subsection {* The @{text random} class *}
11.5
11.6 class random = typerep +
11.7 - fixes random :: "index \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
11.8 + fixes random :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
11.9
11.10
11.11 subsection {* Quickcheck generator *}
11.12 @@ -49,7 +49,7 @@
11.13 (mk_split ty $ Abs ("", ty, Abs ("", @{typ "unit \<Rightarrow> term"}, t')));
11.14 fun mk_bindclause (_, _, i, ty) = mk_scomp_split ty
11.15 (Sign.mk_const thy (@{const_name random}, [ty]) $ Bound i);
11.16 - in Abs ("n", @{typ index}, fold_rev mk_bindclause bounds (return $ check)) end;
11.17 + in Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check)) end;
11.18
11.19 fun compile_generator_expr thy t =
11.20 let
11.21 @@ -84,7 +84,7 @@
11.22 instantiation itself :: (typerep) random
11.23 begin
11.24
11.25 -definition random_itself :: "index \<Rightarrow> Random.seed \<Rightarrow> ('a itself \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
11.26 +definition random_itself :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a itself \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
11.27 "random_itself _ = Pair (Code_Eval.valtermify TYPE('a))"
11.28
11.29 instance ..
11.30 @@ -139,7 +139,7 @@
11.31 instantiation "fun" :: ("{eq, term_of}", "{type, random}") random
11.32 begin
11.33
11.34 -definition random_fun :: "index \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
11.35 +definition random_fun :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
11.36 "random n = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of (random n) Random.split_seed"
11.37
11.38 instance ..
11.39 @@ -154,9 +154,9 @@
11.40 instantiation nat :: random
11.41 begin
11.42
11.43 -definition random_nat :: "index \<Rightarrow> Random.seed \<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Eval.term)) \<times> Random.seed" where
11.44 +definition random_nat :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Eval.term)) \<times> Random.seed" where
11.45 "random_nat i = Random.range (i + 1) o\<rightarrow> (\<lambda>k. Pair (
11.46 - let n = Code_Index.nat_of k
11.47 + let n = Code_Numeral.nat_of k
11.48 in (n, \<lambda>_. Code_Eval.term_of n)))"
11.49
11.50 instance ..
11.51 @@ -168,7 +168,7 @@
11.52
11.53 definition
11.54 "random i = Random.range (2 * i + 1) o\<rightarrow> (\<lambda>k. Pair (
11.55 - let j = (if k \<ge> i then Code_Index.int_of (k - i) else - Code_Index.int_of (i - k))
11.56 + let j = (if k \<ge> i then Code_Numeral.int_of (k - i) else - Code_Numeral.int_of (i - k))
11.57 in (j, \<lambda>_. Code_Eval.term_of j)))"
11.58
11.59 instance ..
12.1 --- a/src/HOL/Random.thy Tue May 19 13:57:51 2009 +0200
12.2 +++ b/src/HOL/Random.thy Tue May 19 16:54:55 2009 +0200
12.3 @@ -3,7 +3,7 @@
12.4 header {* A HOL random engine *}
12.5
12.6 theory Random
12.7 -imports Code_Index List
12.8 +imports Code_Numeral List
12.9 begin
12.10
12.11 notation fcomp (infixl "o>" 60)
12.12 @@ -12,21 +12,21 @@
12.13
12.14 subsection {* Auxiliary functions *}
12.15
12.16 -definition inc_shift :: "index \<Rightarrow> index \<Rightarrow> index" where
12.17 +definition inc_shift :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
12.18 "inc_shift v k = (if v = k then 1 else k + 1)"
12.19
12.20 -definition minus_shift :: "index \<Rightarrow> index \<Rightarrow> index \<Rightarrow> index" where
12.21 +definition minus_shift :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
12.22 "minus_shift r k l = (if k < l then r + k - l else k - l)"
12.23
12.24 -fun log :: "index \<Rightarrow> index \<Rightarrow> index" where
12.25 +fun log :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
12.26 "log b i = (if b \<le> 1 \<or> i < b then 1 else 1 + log b (i div b))"
12.27
12.28
12.29 subsection {* Random seeds *}
12.30
12.31 -types seed = "index \<times> index"
12.32 +types seed = "code_numeral \<times> code_numeral"
12.33
12.34 -primrec "next" :: "seed \<Rightarrow> index \<times> seed" where
12.35 +primrec "next" :: "seed \<Rightarrow> code_numeral \<times> seed" where
12.36 "next (v, w) = (let
12.37 k = v div 53668;
12.38 v' = minus_shift 2147483563 (40014 * (v mod 53668)) (k * 12211);
12.39 @@ -55,10 +55,10 @@
12.40
12.41 subsection {* Base selectors *}
12.42
12.43 -fun iterate :: "index \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
12.44 +fun iterate :: "code_numeral \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
12.45 "iterate k f x = (if k = 0 then Pair x else f x o\<rightarrow> iterate (k - 1) f)"
12.46
12.47 -definition range :: "index \<Rightarrow> seed \<Rightarrow> index \<times> seed" where
12.48 +definition range :: "code_numeral \<Rightarrow> seed \<Rightarrow> code_numeral \<times> seed" where
12.49 "range k = iterate (log 2147483561 k)
12.50 (\<lambda>l. next o\<rightarrow> (\<lambda>v. Pair (v + l * 2147483561))) 1
12.51 o\<rightarrow> (\<lambda>v. Pair (v mod k))"
12.52 @@ -68,23 +68,23 @@
12.53 by (simp add: range_def scomp_apply split_def del: log.simps iterate.simps)
12.54
12.55 definition select :: "'a list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
12.56 - "select xs = range (Code_Index.of_nat (length xs))
12.57 - o\<rightarrow> (\<lambda>k. Pair (nth xs (Code_Index.nat_of k)))"
12.58 + "select xs = range (Code_Numeral.of_nat (length xs))
12.59 + o\<rightarrow> (\<lambda>k. Pair (nth xs (Code_Numeral.nat_of k)))"
12.60
12.61 lemma select:
12.62 assumes "xs \<noteq> []"
12.63 shows "fst (select xs s) \<in> set xs"
12.64 proof -
12.65 - from assms have "Code_Index.of_nat (length xs) > 0" by simp
12.66 + from assms have "Code_Numeral.of_nat (length xs) > 0" by simp
12.67 with range have
12.68 - "fst (range (Code_Index.of_nat (length xs)) s) < Code_Index.of_nat (length xs)" by best
12.69 + "fst (range (Code_Numeral.of_nat (length xs)) s) < Code_Numeral.of_nat (length xs)" by best
12.70 then have
12.71 - "Code_Index.nat_of (fst (range (Code_Index.of_nat (length xs)) s)) < length xs" by simp
12.72 + "Code_Numeral.nat_of (fst (range (Code_Numeral.of_nat (length xs)) s)) < length xs" by simp
12.73 then show ?thesis
12.74 by (simp add: scomp_apply split_beta select_def)
12.75 qed
12.76
12.77 -primrec pick :: "(index \<times> 'a) list \<Rightarrow> index \<Rightarrow> 'a" where
12.78 +primrec pick :: "(code_numeral \<times> 'a) list \<Rightarrow> code_numeral \<Rightarrow> 'a" where
12.79 "pick (x # xs) i = (if i < fst x then snd x else pick xs (i - fst x))"
12.80
12.81 lemma pick_member:
12.82 @@ -96,14 +96,14 @@
12.83 by (induct xs) (auto simp add: expand_fun_eq)
12.84
12.85 lemma pick_same:
12.86 - "l < length xs \<Longrightarrow> Random.pick (map (Pair 1) xs) (Code_Index.of_nat l) = nth xs l"
12.87 + "l < length xs \<Longrightarrow> Random.pick (map (Pair 1) xs) (Code_Numeral.of_nat l) = nth xs l"
12.88 proof (induct xs arbitrary: l)
12.89 case Nil then show ?case by simp
12.90 next
12.91 case (Cons x xs) then show ?case by (cases l) simp_all
12.92 qed
12.93
12.94 -definition select_weight :: "(index \<times> 'a) list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
12.95 +definition select_weight :: "(code_numeral \<times> 'a) list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
12.96 "select_weight xs = range (listsum (map fst xs))
12.97 o\<rightarrow> (\<lambda>k. Pair (pick xs k))"
12.98
12.99 @@ -130,16 +130,16 @@
12.100 assumes "xs \<noteq> []"
12.101 shows "Random.select_weight (map (Pair 1) xs) = Random.select xs"
12.102 proof -
12.103 - have less: "\<And>s. fst (Random.range (Code_Index.of_nat (length xs)) s) < Code_Index.of_nat (length xs)"
12.104 + have less: "\<And>s. fst (Random.range (Code_Numeral.of_nat (length xs)) s) < Code_Numeral.of_nat (length xs)"
12.105 using assms by (intro range) simp
12.106 - moreover have "listsum (map fst (map (Pair 1) xs)) = Code_Index.of_nat (length xs)"
12.107 + moreover have "listsum (map fst (map (Pair 1) xs)) = Code_Numeral.of_nat (length xs)"
12.108 by (induct xs) simp_all
12.109 ultimately show ?thesis
12.110 by (auto simp add: select_weight_def select_def scomp_def split_def
12.111 expand_fun_eq pick_same [symmetric])
12.112 qed
12.113
12.114 -definition select_default :: "index \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
12.115 +definition select_default :: "code_numeral \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
12.116 [code del]: "select_default k x y = range k
12.117 o\<rightarrow> (\<lambda>l. Pair (if l + 1 < k then x else y))"
12.118
12.119 @@ -153,7 +153,7 @@
12.120 else range k o\<rightarrow> (\<lambda>l. Pair (if l + 1 < k then x else y)))"
12.121 proof
12.122 fix s
12.123 - have "snd (range (Code_Index.of_nat 0) s) = snd (range (Code_Index.of_nat 1) s)"
12.124 + have "snd (range (Code_Numeral.of_nat 0) s) = snd (range (Code_Numeral.of_nat 1) s)"
12.125 by (simp add: range_def scomp_Pair scomp_apply split_beta)
12.126 then show "select_default k x y s = (if k = 0
12.127 then range 1 o\<rightarrow> (\<lambda>_. Pair y)
13.1 --- a/src/HOL/Rational.thy Tue May 19 13:57:51 2009 +0200
13.2 +++ b/src/HOL/Rational.thy Tue May 19 16:54:55 2009 +0200
13.3 @@ -1013,7 +1013,7 @@
13.4
13.5 definition
13.6 "random i = random i o\<rightarrow> (\<lambda>num. Random.range i o\<rightarrow> (\<lambda>denom. Pair (
13.7 - let j = Code_Index.int_of (denom + 1)
13.8 + let j = Code_Numeral.int_of (denom + 1)
13.9 in valterm_fract num (j, \<lambda>u. Code_Eval.term_of j))))"
13.10
13.11 instance ..
14.1 --- a/src/HOL/String.thy Tue May 19 13:57:51 2009 +0200
14.2 +++ b/src/HOL/String.thy Tue May 19 16:54:55 2009 +0200
14.3 @@ -85,15 +85,14 @@
14.4
14.5 subsection {* Strings as dedicated datatype *}
14.6
14.7 -datatype message_string = STR string
14.8 +datatype literal = STR string
14.9
14.10 -lemmas [code del] =
14.11 - message_string.recs message_string.cases
14.12 +lemmas [code del] = literal.recs literal.cases
14.13
14.14 -lemma [code]: "size (s\<Colon>message_string) = 0"
14.15 +lemma [code]: "size (s\<Colon>literal) = 0"
14.16 by (cases s) simp_all
14.17
14.18 -lemma [code]: "message_string_size (s\<Colon>message_string) = 0"
14.19 +lemma [code]: "literal_size (s\<Colon>literal) = 0"
14.20 by (cases s) simp_all
14.21
14.22
14.23 @@ -101,19 +100,19 @@
14.24
14.25 use "Tools/string_code.ML"
14.26
14.27 -code_type message_string
14.28 +code_type literal
14.29 (SML "string")
14.30 (OCaml "string")
14.31 (Haskell "String")
14.32
14.33 setup {*
14.34 - fold String_Code.add_literal_message ["SML", "OCaml", "Haskell"]
14.35 + fold String_Code.add_literal_string ["SML", "OCaml", "Haskell"]
14.36 *}
14.37
14.38 -code_instance message_string :: eq
14.39 +code_instance literal :: eq
14.40 (Haskell -)
14.41
14.42 -code_const "eq_class.eq \<Colon> message_string \<Rightarrow> message_string \<Rightarrow> bool"
14.43 +code_const "eq_class.eq \<Colon> literal \<Rightarrow> literal \<Rightarrow> bool"
14.44 (SML "!((_ : string) = _)")
14.45 (OCaml "!((_ : string) = _)")
14.46 (Haskell infixl 4 "==")
14.47 @@ -147,4 +146,6 @@
14.48 in Codegen.add_codegen "char_codegen" char_codegen end
14.49 *}
14.50
14.51 +hide (open) type literal
14.52 +
14.53 end
14.54 \ No newline at end of file
15.1 --- a/src/HOL/Tools/hologic.ML Tue May 19 13:57:51 2009 +0200
15.2 +++ b/src/HOL/Tools/hologic.ML Tue May 19 16:54:55 2009 +0200
15.3 @@ -87,7 +87,7 @@
15.4 val dest_nat: term -> int
15.5 val class_size: string
15.6 val size_const: typ -> term
15.7 - val indexT: typ
15.8 + val code_numeralT: typ
15.9 val intT: typ
15.10 val pls_const: term
15.11 val min_const: term
15.12 @@ -116,9 +116,9 @@
15.13 val stringT: typ
15.14 val mk_string: string -> term
15.15 val dest_string: term -> string
15.16 - val message_stringT: typ
15.17 - val mk_message_string: string -> term
15.18 - val dest_message_string: term -> string
15.19 + val literalT: typ
15.20 + val mk_literal: string -> term
15.21 + val dest_literal: term -> string
15.22 val mk_typerep: typ -> term
15.23 val mk_term_of: typ -> term -> term
15.24 val reflect_term: term -> term
15.25 @@ -461,9 +461,9 @@
15.26 fun size_const T = Const ("Nat.size_class.size", T --> natT);
15.27
15.28
15.29 -(* index *)
15.30 +(* code numeral *)
15.31
15.32 -val indexT = Type ("Code_Index.index", []);
15.33 +val code_numeralT = Type ("Code_Numeral.code_numeral", []);
15.34
15.35
15.36 (* binary numerals and int -- non-unique representation due to leading zeros/ones! *)
15.37 @@ -586,15 +586,15 @@
15.38 val dest_string = implode o map (chr o dest_char) o dest_list;
15.39
15.40
15.41 -(* message_string *)
15.42 +(* literal *)
15.43
15.44 -val message_stringT = Type ("String.message_string", []);
15.45 +val literalT = Type ("String.literal", []);
15.46
15.47 -fun mk_message_string s = Const ("String.message_string.STR", stringT --> message_stringT)
15.48 +fun mk_literal s = Const ("String.literal.STR", stringT --> literalT)
15.49 $ mk_string s;
15.50 -fun dest_message_string (Const ("String.message_string.STR", _) $ t) =
15.51 +fun dest_literal (Const ("String.literal.STR", _) $ t) =
15.52 dest_string t
15.53 - | dest_message_string t = raise TERM ("dest_message_string", [t]);
15.54 + | dest_literal t = raise TERM ("dest_literal", [t]);
15.55
15.56
15.57 (* typerep and term *)
15.58 @@ -609,8 +609,8 @@
15.59 fun mk_term_of T t = Const ("Code_Eval.term_of_class.term_of", T --> termT) $ t;
15.60
15.61 fun reflect_term (Const (c, T)) =
15.62 - Const ("Code_Eval.Const", message_stringT --> typerepT --> termT)
15.63 - $ mk_message_string c $ mk_typerep T
15.64 + Const ("Code_Eval.Const", literalT --> typerepT --> termT)
15.65 + $ mk_literal c $ mk_typerep T
15.66 | reflect_term (t1 $ t2) =
15.67 Const ("Code_Eval.App", termT --> termT --> termT)
15.68 $ reflect_term t1 $ reflect_term t2
16.1 --- a/src/HOL/Tools/string_code.ML Tue May 19 13:57:51 2009 +0200
16.2 +++ b/src/HOL/Tools/string_code.ML Tue May 19 16:54:55 2009 +0200
16.3 @@ -7,7 +7,7 @@
16.4 sig
16.5 val add_literal_list_string: string -> theory -> theory
16.6 val add_literal_char: string -> theory -> theory
16.7 - val add_literal_message: string -> theory -> theory
16.8 + val add_literal_string: string -> theory -> theory
16.9 end;
16.10
16.11 structure String_Code : STRING_CODE =
16.12 @@ -72,7 +72,7 @@
16.13 @{const_name Char} (SOME (2, (cs_nibbles, pretty)))
16.14 end;
16.15
16.16 -fun add_literal_message target =
16.17 +fun add_literal_string target =
16.18 let
16.19 fun pretty literals (nil' :: cons' :: char' :: nibbles') _ thm _ _ [(t, _)] =
16.20 case List_Code.implode_list nil' cons' t
17.1 --- a/src/HOL/Typerep.thy Tue May 19 13:57:51 2009 +0200
17.2 +++ b/src/HOL/Typerep.thy Tue May 19 16:54:55 2009 +0200
17.3 @@ -6,7 +6,7 @@
17.4 imports Plain String
17.5 begin
17.6
17.7 -datatype typerep = Typerep message_string "typerep list"
17.8 +datatype typerep = Typerep String.literal "typerep list"
17.9
17.10 class typerep =
17.11 fixes typerep :: "'a itself \<Rightarrow> typerep"
17.12 @@ -45,7 +45,7 @@
17.13 val ty = Type (tyco, map TFree vs);
17.14 val lhs = Const (@{const_name typerep}, Term.itselfT ty --> @{typ typerep})
17.15 $ Free ("T", Term.itselfT ty);
17.16 - val rhs = @{term Typerep} $ HOLogic.mk_message_string tyco
17.17 + val rhs = @{term Typerep} $ HOLogic.mk_literal tyco
17.18 $ HOLogic.mk_list @{typ typerep} (map (HOLogic.mk_typerep o TFree) vs);
17.19 val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
17.20 in