1.1 --- a/src/HOL/IsaMakefile Wed Aug 27 12:00:28 2008 +0200
1.2 +++ b/src/HOL/IsaMakefile Wed Aug 27 12:01:59 2008 +0200
1.3 @@ -768,7 +768,7 @@
1.4 ex/InductiveInvariant_examples.thy ex/Intuitionistic.thy \
1.5 ex/Lagrange.thy ex/LexOrds.thy ex/Locales.thy ex/LocaleTest2.thy ex/MT.thy \
1.6 ex/MergeSort.thy ex/MonoidGroup.thy ex/Multiquote.thy ex/NatSum.thy \
1.7 - ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy ex/Puzzle.thy \
1.8 + ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy ex/Puzzle.thy \
1.9 ex/Quickcheck_Examples.thy ex/Reflection.thy ex/reflection_data.ML \
1.10 ex/ReflectionEx.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy \
1.11 ex/Reflected_Presburger.thy ex/coopertac.ML \
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/HOL/ex/Numeral.thy Wed Aug 27 12:01:59 2008 +0200
2.3 @@ -0,0 +1,910 @@
2.4 +(* Title: HOL/ex/Numeral.thy
2.5 + ID: $Id$
2.6 + Author: Florian Haftmann
2.7 +
2.8 +An experimental alternative numeral representation.
2.9 +*)
2.10 +
2.11 +theory Numeral
2.12 +imports Int Inductive
2.13 +begin
2.14 +
2.15 +subsection {* The @{text num} type *}
2.16 +
2.17 +text {*
2.18 + We construct @{text num} as a copy of strictly positive
2.19 + natural numbers.
2.20 +*}
2.21 +
2.22 +typedef (open) num = "\<lambda>n\<Colon>nat. n > 0"
2.23 + morphisms nat_of_num num_of_nat_abs
2.24 + by (auto simp add: mem_def)
2.25 +
2.26 +text {*
2.27 + A totalized abstraction function. It is not entirely clear
2.28 + whether this is really useful.
2.29 +*}
2.30 +
2.31 +definition num_of_nat :: "nat \<Rightarrow> num" where
2.32 + "num_of_nat n = (if n = 0 then num_of_nat_abs 1 else num_of_nat_abs n)"
2.33 +
2.34 +lemma num_cases [case_names nat, cases type: num]:
2.35 + assumes "(\<And>n\<Colon>nat. m = num_of_nat n \<Longrightarrow> 0 < n \<Longrightarrow> P)"
2.36 + shows P
2.37 +apply (rule num_of_nat_abs_cases)
2.38 +apply (unfold mem_def)
2.39 +using assms unfolding num_of_nat_def
2.40 +apply auto
2.41 +done
2.42 +
2.43 +lemma num_of_nat_zero: "num_of_nat 0 = num_of_nat 1"
2.44 + by (simp add: num_of_nat_def)
2.45 +
2.46 +lemma num_of_nat_inverse: "nat_of_num (num_of_nat n) = (if n = 0 then 1 else n)"
2.47 + apply (simp add: num_of_nat_def)
2.48 + apply (subst num_of_nat_abs_inverse)
2.49 + apply (auto simp add: mem_def num_of_nat_abs_inverse)
2.50 + done
2.51 +
2.52 +lemma num_of_nat_inject:
2.53 + "num_of_nat m = num_of_nat n \<longleftrightarrow> m = n \<or> (m = 0 \<or> m = 1) \<and> (n = 0 \<or> n = 1)"
2.54 +by (auto simp add: num_of_nat_def num_of_nat_abs_inject [unfolded mem_def])
2.55 +
2.56 +lemma split_num_all:
2.57 + "(\<And>m. PROP P m) \<equiv> (\<And>n. PROP P (num_of_nat n))"
2.58 +proof
2.59 + fix n
2.60 + assume "\<And>m\<Colon>num. PROP P m"
2.61 + then show "PROP P (num_of_nat n)" .
2.62 +next
2.63 + fix m
2.64 + have nat_of_num: "\<And>m. nat_of_num m \<noteq> 0"
2.65 + using nat_of_num by (auto simp add: mem_def)
2.66 + have nat_of_num_inverse: "\<And>m. num_of_nat (nat_of_num m) = m"
2.67 + by (auto simp add: num_of_nat_def nat_of_num_inverse nat_of_num)
2.68 + assume "\<And>n. PROP P (num_of_nat n)"
2.69 + then have "PROP P (num_of_nat (nat_of_num m))" .
2.70 + then show "PROP P m" unfolding nat_of_num_inverse .
2.71 +qed
2.72 +
2.73 +
2.74 +subsection {* Digit representation for @{typ num} *}
2.75 +
2.76 +instantiation num :: "{semiring, monoid_mult}"
2.77 +begin
2.78 +
2.79 +definition one_num :: num where
2.80 + [code func del]: "1 = num_of_nat 1"
2.81 +
2.82 +definition plus_num :: "num \<Rightarrow> num \<Rightarrow> num" where
2.83 + [code func del]: "m + n = num_of_nat (nat_of_num m + nat_of_num n)"
2.84 +
2.85 +definition times_num :: "num \<Rightarrow> num \<Rightarrow> num" where
2.86 + [code func del]: "m * n = num_of_nat (nat_of_num m * nat_of_num n)"
2.87 +
2.88 +definition Dig0 :: "num \<Rightarrow> num" where
2.89 + [code func del]: "Dig0 n = n + n"
2.90 +
2.91 +definition Dig1 :: "num \<Rightarrow> num" where
2.92 + [code func del]: "Dig1 n = n + n + 1"
2.93 +
2.94 +instance proof
2.95 +qed (simp_all add: one_num_def plus_num_def times_num_def
2.96 + split_num_all num_of_nat_inverse num_of_nat_zero add_ac mult_ac nat_distrib)
2.97 +
2.98 +end
2.99 +
2.100 +text {*
2.101 + The following proofs seem horribly complicated.
2.102 + Any room for simplification!?
2.103 +*}
2.104 +
2.105 +lemma nat_dig_cases [case_names 0 1 dig0 dig1]:
2.106 + fixes n :: nat
2.107 + assumes "n = 0 \<Longrightarrow> P"
2.108 + and "n = 1 \<Longrightarrow> P"
2.109 + and "\<And>m. m > 0 \<Longrightarrow> n = m + m \<Longrightarrow> P"
2.110 + and "\<And>m. m > 0 \<Longrightarrow> n = Suc (m + m) \<Longrightarrow> P"
2.111 + shows P
2.112 +using assms proof (induct n)
2.113 + case 0 then show ?case by simp
2.114 +next
2.115 + case (Suc n)
2.116 + show P proof (rule Suc.hyps)
2.117 + assume "n = 0"
2.118 + then have "Suc n = 1" by simp
2.119 + then show P by (rule Suc.prems(2))
2.120 + next
2.121 + assume "n = 1"
2.122 + have "1 > (0\<Colon>nat)" by simp
2.123 + moreover from `n = 1` have "Suc n = 1 + 1" by simp
2.124 + ultimately show P by (rule Suc.prems(3))
2.125 + next
2.126 + fix m
2.127 + assume "0 < m" and "n = m + m"
2.128 + note `0 < m`
2.129 + moreover from `n = m + m` have "Suc n = Suc (m + m)" by simp
2.130 + ultimately show P by (rule Suc.prems(4))
2.131 + next
2.132 + fix m
2.133 + assume "0 < m" and "n = Suc (m + m)"
2.134 + have "0 < Suc m" by simp
2.135 + moreover from `n = Suc (m + m)` have "Suc n = Suc m + Suc m" by simp
2.136 + ultimately show P by (rule Suc.prems(3))
2.137 + qed
2.138 +qed
2.139 +
2.140 +lemma num_induct_raw:
2.141 + fixes n :: nat
2.142 + assumes not0: "n > 0"
2.143 + assumes "P 1"
2.144 + and "\<And>n. n > 0 \<Longrightarrow> P n \<Longrightarrow> P (n + n)"
2.145 + and "\<And>n. n > 0 \<Longrightarrow> P n \<Longrightarrow> P (Suc (n + n))"
2.146 + shows "P n"
2.147 +using not0 proof (induct n rule: less_induct)
2.148 + case (less n)
2.149 + show "P n" proof (cases n rule: nat_dig_cases)
2.150 + case 0 then show ?thesis using less by simp
2.151 + next
2.152 + case 1 then show ?thesis using assms by simp
2.153 + next
2.154 + case (dig0 m)
2.155 + then show ?thesis apply simp
2.156 + apply (rule assms(3)) apply assumption
2.157 + apply (rule less)
2.158 + apply simp_all
2.159 + done
2.160 + next
2.161 + case (dig1 m)
2.162 + then show ?thesis apply simp
2.163 + apply (rule assms(4)) apply assumption
2.164 + apply (rule less)
2.165 + apply simp_all
2.166 + done
2.167 + qed
2.168 +qed
2.169 +
2.170 +lemma num_of_nat_Suc: "num_of_nat (Suc n) = (if n = 0 then 1 else num_of_nat n + 1)"
2.171 + by (cases n) (auto simp add: one_num_def plus_num_def num_of_nat_inverse)
2.172 +
2.173 +lemma num_induct [case_names 1 Suc, induct type: num]:
2.174 + fixes P :: "num \<Rightarrow> bool"
2.175 + assumes 1: "P 1"
2.176 + and Suc: "\<And>n. P n \<Longrightarrow> P (n + 1)"
2.177 + shows "P n"
2.178 +proof (cases n)
2.179 + case (nat m) then show ?thesis by (induct m arbitrary: n)
2.180 + (auto simp: num_of_nat_Suc intro: 1 Suc split: split_if_asm)
2.181 +qed
2.182 +
2.183 +rep_datatype "1::num" Dig0 Dig1 proof -
2.184 + fix P m
2.185 + assume 1: "P 1"
2.186 + and Dig0: "\<And>m. P m \<Longrightarrow> P (Dig0 m)"
2.187 + and Dig1: "\<And>m. P m \<Longrightarrow> P (Dig1 m)"
2.188 + obtain n where "0 < n" and m: "m = num_of_nat n"
2.189 + by (cases m) auto
2.190 + from `0 < n` have "P (num_of_nat n)" proof (induct n rule: num_induct_raw)
2.191 + case 1 from `0 < n` show ?case .
2.192 + next
2.193 + case 2 with 1 show ?case by (simp add: one_num_def)
2.194 + next
2.195 + case (3 n) then have "P (num_of_nat n)" by auto
2.196 + then have "P (Dig0 (num_of_nat n))" by (rule Dig0)
2.197 + with 3 show ?case by (simp add: Dig0_def plus_num_def num_of_nat_inverse)
2.198 + next
2.199 + case (4 n) then have "P (num_of_nat n)" by auto
2.200 + then have "P (Dig1 (num_of_nat n))" by (rule Dig1)
2.201 + with 4 show ?case by (simp add: Dig1_def one_num_def plus_num_def num_of_nat_inverse)
2.202 + qed
2.203 + with m show "P m" by simp
2.204 +next
2.205 + fix m n
2.206 + show "Dig0 m = Dig0 n \<longleftrightarrow> m = n"
2.207 + apply (cases m) apply (cases n)
2.208 + by (auto simp add: Dig0_def plus_num_def num_of_nat_inverse num_of_nat_inject)
2.209 +next
2.210 + fix m n
2.211 + show "Dig1 m = Dig1 n \<longleftrightarrow> m = n"
2.212 + apply (cases m) apply (cases n)
2.213 + by (auto simp add: Dig1_def plus_num_def num_of_nat_inverse num_of_nat_inject)
2.214 +next
2.215 + fix n
2.216 + show "1 \<noteq> Dig0 n"
2.217 + apply (cases n)
2.218 + by (auto simp add: Dig0_def one_num_def plus_num_def num_of_nat_inverse num_of_nat_inject)
2.219 +next
2.220 + fix n
2.221 + show "1 \<noteq> Dig1 n"
2.222 + apply (cases n)
2.223 + by (auto simp add: Dig1_def one_num_def plus_num_def num_of_nat_inverse num_of_nat_inject)
2.224 +next
2.225 + fix m n
2.226 + have "\<And>n m. n + n \<noteq> Suc (m + m)"
2.227 + proof -
2.228 + fix n m
2.229 + show "n + n \<noteq> Suc (m + m)"
2.230 + proof (induct m arbitrary: n)
2.231 + case 0 then show ?case by (cases n) simp_all
2.232 + next
2.233 + case (Suc m) then show ?case by (cases n) simp_all
2.234 + qed
2.235 + qed
2.236 + then show "Dig0 n \<noteq> Dig1 m"
2.237 + apply (cases n) apply (cases m)
2.238 + by (auto simp add: Dig0_def Dig1_def one_num_def plus_num_def num_of_nat_inverse num_of_nat_inject)
2.239 +qed
2.240 +
2.241 +text {*
2.242 + From now on, there are two possible models for @{typ num}:
2.243 + as positive naturals (rules @{text "num_induct"}, @{text "num_cases"})
2.244 + and as digit representation (rules @{text "num.induct"}, @{text "num.cases"}).
2.245 +
2.246 + It is not entirely clear in which context it is better to use
2.247 + the one or the other, or whether the construction should be reversed.
2.248 +*}
2.249 +
2.250 +
2.251 +subsection {* Binary numerals *}
2.252 +
2.253 +text {*
2.254 + We embed binary representations into a generic algebraic
2.255 + structure using @{text of_num}
2.256 +*}
2.257 +
2.258 +ML {*
2.259 +structure DigSimps =
2.260 + NamedThmsFun(val name = "numeral"; val description = "Simplification rules for numerals")
2.261 +*}
2.262 +
2.263 +setup DigSimps.setup
2.264 +
2.265 +class semiring_numeral = semiring + monoid_mult
2.266 +begin
2.267 +
2.268 +primrec of_num :: "num \<Rightarrow> 'a" where
2.269 + of_num_one [numeral]: "of_num 1 = 1"
2.270 + | "of_num (Dig0 n) = of_num n + of_num n"
2.271 + | "of_num (Dig1 n) = of_num n + of_num n + 1"
2.272 +
2.273 +declare of_num.simps [simp del]
2.274 +
2.275 +end
2.276 +
2.277 +text {*
2.278 + ML stuff and syntax.
2.279 +*}
2.280 +
2.281 +ML {*
2.282 +fun mk_num 1 = @{term "1::num"}
2.283 + | mk_num k =
2.284 + let
2.285 + val (l, b) = Integer.div_mod k 2;
2.286 + val bit = (if b = 0 then @{term Dig0} else @{term Dig1});
2.287 + in bit $ (mk_num l) end;
2.288 +
2.289 +fun dest_num @{term "1::num"} = 1
2.290 + | dest_num (@{term Dig0} $ n) = 2 * dest_num n
2.291 + | dest_num (@{term Dig1} $ n) = 2 * dest_num n + 1;
2.292 +
2.293 +(*FIXME these have to gain proper context via morphisms phi*)
2.294 +
2.295 +fun mk_numeral T k = Const (@{const_name of_num}, @{typ num} --> T)
2.296 + $ mk_num k
2.297 +
2.298 +fun dest_numeral (Const (@{const_name of_num}, Type ("fun", [@{typ num}, T])) $ t) =
2.299 + (T, dest_num t)
2.300 +*}
2.301 +
2.302 +syntax
2.303 + "_Numerals" :: "xnum \<Rightarrow> 'a" ("_")
2.304 +
2.305 +parse_translation {*
2.306 +let
2.307 + fun num_of_int n = if n > 0 then case IntInf.quotRem (n, 2)
2.308 + of (0, 1) => Const (@{const_name HOL.one}, dummyT)
2.309 + | (n, 0) => Const (@{const_name Dig0}, dummyT) $ num_of_int n
2.310 + | (n, 1) => Const (@{const_name Dig1}, dummyT) $ num_of_int n
2.311 + else raise Match;
2.312 + fun numeral_tr [Free (num, _)] =
2.313 + let
2.314 + val {leading_zeros, value, ...} = Syntax.read_xnum num;
2.315 + val _ = leading_zeros = 0 andalso value > 0
2.316 + orelse error ("Bad numeral: " ^ num);
2.317 + in Const (@{const_name of_num}, @{typ num} --> dummyT) $ num_of_int value end
2.318 + | numeral_tr ts = raise TERM ("numeral_tr", ts);
2.319 +in [("_Numerals", numeral_tr)] end
2.320 +*}
2.321 +
2.322 +typed_print_translation {*
2.323 +let
2.324 + fun dig b n = b + 2 * n;
2.325 + fun int_of_num' (Const (@{const_syntax Dig0}, _) $ n) =
2.326 + dig 0 (int_of_num' n)
2.327 + | int_of_num' (Const (@{const_syntax Dig1}, _) $ n) =
2.328 + dig 1 (int_of_num' n)
2.329 + | int_of_num' (Const (@{const_syntax HOL.one}, _)) = 1;
2.330 + fun num_tr' show_sorts T [n] =
2.331 + let
2.332 + val k = int_of_num' n;
2.333 + val t' = Syntax.const "_Numerals" $ Syntax.free ("#" ^ string_of_int k);
2.334 + in case T
2.335 + of Type ("fun", [_, T']) =>
2.336 + if not (! show_types) andalso can Term.dest_Type T' then t'
2.337 + else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T'
2.338 + | T' => if T' = dummyT then t' else raise Match
2.339 + end;
2.340 +in [(@{const_syntax of_num}, num_tr')] end
2.341 +*}
2.342 +
2.343 +
2.344 +subsection {* Numeral operations *}
2.345 +
2.346 +text {*
2.347 + First, addition and multiplication on digits.
2.348 +*}
2.349 +
2.350 +lemma Dig_plus [numeral, simp, code]:
2.351 + "1 + 1 = Dig0 1"
2.352 + "1 + Dig0 m = Dig1 m"
2.353 + "1 + Dig1 m = Dig0 (m + 1)"
2.354 + "Dig0 n + 1 = Dig1 n"
2.355 + "Dig0 n + Dig0 m = Dig0 (n + m)"
2.356 + "Dig0 n + Dig1 m = Dig1 (n + m)"
2.357 + "Dig1 n + 1 = Dig0 (n + 1)"
2.358 + "Dig1 n + Dig0 m = Dig1 (n + m)"
2.359 + "Dig1 n + Dig1 m = Dig0 (n + m + 1)"
2.360 + by (simp_all add: add_ac Dig0_def Dig1_def)
2.361 +
2.362 +lemma Dig_times [numeral, simp, code]:
2.363 + "1 * 1 = (1::num)"
2.364 + "1 * Dig0 n = Dig0 n"
2.365 + "1 * Dig1 n = Dig1 n"
2.366 + "Dig0 n * 1 = Dig0 n"
2.367 + "Dig0 n * Dig0 m = Dig0 (n * Dig0 m)"
2.368 + "Dig0 n * Dig1 m = Dig0 (n * Dig1 m)"
2.369 + "Dig1 n * 1 = Dig1 n"
2.370 + "Dig1 n * Dig0 m = Dig0 (n * Dig0 m + m)"
2.371 + "Dig1 n * Dig1 m = Dig1 (n * Dig1 m + m)"
2.372 + by (simp_all add: left_distrib right_distrib add_ac Dig0_def Dig1_def)
2.373 +
2.374 +text {*
2.375 + @{const of_num} is a morphism.
2.376 +*}
2.377 +
2.378 +context semiring_numeral
2.379 +begin
2.380 +
2.381 +abbreviation "Num1 \<equiv> of_num 1"
2.382 +
2.383 +text {*
2.384 + Alas, there is still the duplication of @{term 1},
2.385 + thought the duplicated @{term 0} has disappeared.
2.386 + We could get rid of it by replacing the constructor
2.387 + @{term 1} in @{typ num} by two constructors
2.388 + @{text two} and @{text three}, resulting in a further
2.389 + blow-up. But it could be worth the effort.
2.390 +*}
2.391 +
2.392 +lemma of_num_plus_one [numeral]:
2.393 + "of_num n + 1 = of_num (n + 1)"
2.394 + by (rule sym, induct n) (simp_all add: Dig_plus of_num.simps add_ac)
2.395 +
2.396 +lemma of_num_one_plus [numeral]:
2.397 + "1 + of_num n = of_num (n + 1)"
2.398 + unfolding of_num_plus_one [symmetric] add_commute ..
2.399 +
2.400 +lemma of_num_plus [numeral]:
2.401 + "of_num m + of_num n = of_num (m + n)"
2.402 + by (induct n rule: num_induct)
2.403 + (simp_all add: Dig_plus of_num_one semigroup_add_class.plus.add_assoc [symmetric, of m]
2.404 + add_ac of_num_plus_one [symmetric])
2.405 +
2.406 +lemma of_num_times_one [numeral]:
2.407 + "of_num n * 1 = of_num n"
2.408 + by simp
2.409 +
2.410 +lemma of_num_one_times [numeral]:
2.411 + "1 * of_num n = of_num n"
2.412 + by simp
2.413 +
2.414 +lemma of_num_times [numeral]:
2.415 + "of_num m * of_num n = of_num (m * n)"
2.416 + by (induct n rule: num_induct)
2.417 + (simp_all add: of_num_plus [symmetric]
2.418 + semiring_class.plus_times.right_distrib right_distrib of_num_one)
2.419 +
2.420 +end
2.421 +
2.422 +text {*
2.423 + Structures with a @{term 0}.
2.424 +*}
2.425 +
2.426 +context semiring_1
2.427 +begin
2.428 +
2.429 +subclass semiring_numeral ..
2.430 +
2.431 +lemma of_nat_of_num [numeral]: "of_nat (of_num n) = of_num n"
2.432 + by (induct n)
2.433 + (simp_all add: semiring_numeral_class.of_num.simps of_num.simps add_ac)
2.434 +
2.435 +declare of_nat_1 [numeral]
2.436 +
2.437 +lemma Dig_plus_zero [numeral]:
2.438 + "0 + 1 = 1"
2.439 + "0 + of_num n = of_num n"
2.440 + "1 + 0 = 1"
2.441 + "of_num n + 0 = of_num n"
2.442 + by simp_all
2.443 +
2.444 +lemma Dig_times_zero [numeral]:
2.445 + "0 * 1 = 0"
2.446 + "0 * of_num n = 0"
2.447 + "1 * 0 = 0"
2.448 + "of_num n * 0 = 0"
2.449 + by simp_all
2.450 +
2.451 +end
2.452 +
2.453 +lemma nat_of_num_of_num: "nat_of_num = of_num"
2.454 +proof
2.455 + fix n
2.456 + have "of_num n = nat_of_num n" apply (induct n)
2.457 + apply (simp_all add: of_num.simps)
2.458 + using nat_of_num
2.459 + apply (simp_all add: one_num_def plus_num_def Dig0_def Dig1_def num_of_nat_inverse mem_def)
2.460 + done
2.461 + then show "nat_of_num n = of_num n" by simp
2.462 +qed
2.463 +
2.464 +text {*
2.465 + Equality.
2.466 +*}
2.467 +
2.468 +context semiring_char_0
2.469 +begin
2.470 +
2.471 +lemma of_num_eq_iff [numeral]:
2.472 + "of_num m = of_num n \<longleftrightarrow> m = n"
2.473 + unfolding of_nat_of_num [symmetric] nat_of_num_of_num [symmetric]
2.474 + of_nat_eq_iff nat_of_num_inject ..
2.475 +
2.476 +lemma of_num_eq_one_iff [numeral]:
2.477 + "of_num n = 1 \<longleftrightarrow> n = 1"
2.478 +proof -
2.479 + have "of_num n = of_num 1 \<longleftrightarrow> n = 1" unfolding of_num_eq_iff ..
2.480 + then show ?thesis by (simp add: of_num_one)
2.481 +qed
2.482 +
2.483 +lemma one_eq_of_num_iff [numeral]:
2.484 + "1 = of_num n \<longleftrightarrow> n = 1"
2.485 + unfolding of_num_eq_one_iff [symmetric] by auto
2.486 +
2.487 +end
2.488 +
2.489 +text {*
2.490 + Comparisons. Could be perhaps more general than here.
2.491 +*}
2.492 +
2.493 +lemma (in ordered_semidom) of_num_pos: "0 < of_num n"
2.494 +proof -
2.495 + have "(0::nat) < of_num n"
2.496 + by (induct n) (simp_all add: semiring_numeral_class.of_num.simps)
2.497 + then have "of_nat 0 \<noteq> of_nat (of_num n)"
2.498 + by (cases n) (simp_all only: semiring_numeral_class.of_num.simps of_nat_eq_iff)
2.499 + then have "0 \<noteq> of_num n"
2.500 + by (simp add: of_nat_of_num)
2.501 + moreover have "0 \<le> of_nat (of_num n)" by simp
2.502 + ultimately show ?thesis by (simp add: of_nat_of_num)
2.503 +qed
2.504 +
2.505 +instantiation num :: linorder
2.506 +begin
2.507 +
2.508 +definition less_eq_num :: "num \<Rightarrow> num \<Rightarrow> bool" where
2.509 + [code func del]: "m \<le> n \<longleftrightarrow> nat_of_num m \<le> nat_of_num n"
2.510 +
2.511 +definition less_num :: "num \<Rightarrow> num \<Rightarrow> bool" where
2.512 + [code func del]: "m < n \<longleftrightarrow> nat_of_num m < nat_of_num n"
2.513 +
2.514 +instance proof
2.515 +qed (auto simp add: less_eq_num_def less_num_def
2.516 + split_num_all num_of_nat_inverse num_of_nat_inject split: split_if_asm)
2.517 +
2.518 +end
2.519 +
2.520 +lemma less_eq_num_code [numeral, simp, code]:
2.521 + "(1::num) \<le> n \<longleftrightarrow> True"
2.522 + "Dig0 m \<le> 1 \<longleftrightarrow> False"
2.523 + "Dig1 m \<le> 1 \<longleftrightarrow> False"
2.524 + "Dig0 m \<le> Dig0 n \<longleftrightarrow> m \<le> n"
2.525 + "Dig0 m \<le> Dig1 n \<longleftrightarrow> m \<le> n"
2.526 + "Dig1 m \<le> Dig1 n \<longleftrightarrow> m \<le> n"
2.527 + "Dig1 m \<le> Dig0 n \<longleftrightarrow> m < n"
2.528 + using of_num_pos [of n, where ?'a = nat] of_num_pos [of m, where ?'a = nat]
2.529 + by (auto simp add: less_eq_num_def less_num_def nat_of_num_of_num of_num.simps)
2.530 +
2.531 +lemma less_num_code [numeral, simp, code]:
2.532 + "m < (1::num) \<longleftrightarrow> False"
2.533 + "(1::num) < 1 \<longleftrightarrow> False"
2.534 + "1 < Dig0 n \<longleftrightarrow> True"
2.535 + "1 < Dig1 n \<longleftrightarrow> True"
2.536 + "Dig0 m < Dig0 n \<longleftrightarrow> m < n"
2.537 + "Dig0 m < Dig1 n \<longleftrightarrow> m \<le> n"
2.538 + "Dig1 m < Dig1 n \<longleftrightarrow> m < n"
2.539 + "Dig1 m < Dig0 n \<longleftrightarrow> m < n"
2.540 + using of_num_pos [of n, where ?'a = nat] of_num_pos [of m, where ?'a = nat]
2.541 + by (auto simp add: less_eq_num_def less_num_def nat_of_num_of_num of_num.simps)
2.542 +
2.543 +context ordered_semidom
2.544 +begin
2.545 +
2.546 +lemma of_num_less_eq_iff [numeral]: "of_num m \<le> of_num n \<longleftrightarrow> m \<le> n"
2.547 +proof -
2.548 + have "of_nat (of_num m) \<le> of_nat (of_num n) \<longleftrightarrow> m \<le> n"
2.549 + unfolding less_eq_num_def nat_of_num_of_num of_nat_le_iff ..
2.550 + then show ?thesis by (simp add: of_nat_of_num)
2.551 +qed
2.552 +
2.553 +lemma of_num_less_eq_one_iff [numeral]: "of_num n \<le> 1 \<longleftrightarrow> n = 1"
2.554 +proof -
2.555 + have "of_num n \<le> of_num 1 \<longleftrightarrow> n = 1"
2.556 + by (cases n) (simp_all add: of_num_less_eq_iff)
2.557 + then show ?thesis by (simp add: of_num_one)
2.558 +qed
2.559 +
2.560 +lemma one_less_eq_of_num_iff [numeral]: "1 \<le> of_num n"
2.561 +proof -
2.562 + have "of_num 1 \<le> of_num n"
2.563 + by (cases n) (simp_all add: of_num_less_eq_iff)
2.564 + then show ?thesis by (simp add: of_num_one)
2.565 +qed
2.566 +
2.567 +lemma of_num_less_iff [numeral]: "of_num m < of_num n \<longleftrightarrow> m < n"
2.568 +proof -
2.569 + have "of_nat (of_num m) < of_nat (of_num n) \<longleftrightarrow> m < n"
2.570 + unfolding less_num_def nat_of_num_of_num of_nat_less_iff ..
2.571 + then show ?thesis by (simp add: of_nat_of_num)
2.572 +qed
2.573 +
2.574 +lemma of_num_less_one_iff [numeral]: "\<not> of_num n < 1"
2.575 +proof -
2.576 + have "\<not> of_num n < of_num 1"
2.577 + by (cases n) (simp_all add: of_num_less_iff)
2.578 + then show ?thesis by (simp add: of_num_one)
2.579 +qed
2.580 +
2.581 +lemma one_less_of_num_iff [numeral]: "1 < of_num n \<longleftrightarrow> n \<noteq> 1"
2.582 +proof -
2.583 + have "of_num 1 < of_num n \<longleftrightarrow> n \<noteq> 1"
2.584 + by (cases n) (simp_all add: of_num_less_iff)
2.585 + then show ?thesis by (simp add: of_num_one)
2.586 +qed
2.587 +
2.588 +end
2.589 +
2.590 +text {*
2.591 + Structures with subtraction @{term "op -"}.
2.592 +*}
2.593 +
2.594 +text {* A decrement function *}
2.595 +
2.596 +primrec dec :: "num \<Rightarrow> num" where
2.597 + "dec 1 = 1"
2.598 + | "dec (Dig0 n) = (case n of 1 \<Rightarrow> 1 | _ \<Rightarrow> Dig1 (dec n))"
2.599 + | "dec (Dig1 n) = Dig0 n"
2.600 +
2.601 +declare dec.simps [simp del, code del]
2.602 +
2.603 +lemma Dig_dec [numeral, simp, code]:
2.604 + "dec 1 = 1"
2.605 + "dec (Dig0 1) = 1"
2.606 + "dec (Dig0 (Dig0 n)) = Dig1 (dec (Dig0 n))"
2.607 + "dec (Dig0 (Dig1 n)) = Dig1 (Dig0 n)"
2.608 + "dec (Dig1 n) = Dig0 n"
2.609 + by (simp_all add: dec.simps)
2.610 +
2.611 +lemma Dig_dec_plus_one:
2.612 + "dec n + 1 = (if n = 1 then Dig0 1 else n)"
2.613 + by (induct n)
2.614 + (auto simp add: Dig_plus dec.simps,
2.615 + auto simp add: Dig_plus split: num.splits)
2.616 +
2.617 +lemma Dig_one_plus_dec:
2.618 + "1 + dec n = (if n = 1 then Dig0 1 else n)"
2.619 + unfolding add_commute [of 1] Dig_dec_plus_one ..
2.620 +
2.621 +class semiring_minus = semiring + minus + zero +
2.622 + assumes minus_inverts_plus1: "a + b = c \<Longrightarrow> c - b = a"
2.623 + assumes minus_minus_zero_inverts_plus1: "a + b = c \<Longrightarrow> b - c = 0 - a"
2.624 +begin
2.625 +
2.626 +lemma minus_inverts_plus2: "a + b = c \<Longrightarrow> c - a = b"
2.627 + by (simp add: add_ac minus_inverts_plus1 [of b a])
2.628 +
2.629 +lemma minus_minus_zero_inverts_plus2: "a + b = c \<Longrightarrow> a - c = 0 - b"
2.630 + by (simp add: add_ac minus_minus_zero_inverts_plus1 [of b a])
2.631 +
2.632 +end
2.633 +
2.634 +class semiring_1_minus = semiring_1 + semiring_minus
2.635 +begin
2.636 +
2.637 +lemma Dig_of_num_pos:
2.638 + assumes "k + n = m"
2.639 + shows "of_num m - of_num n = of_num k"
2.640 + using assms by (simp add: of_num_plus minus_inverts_plus1)
2.641 +
2.642 +lemma Dig_of_num_zero:
2.643 + shows "of_num n - of_num n = 0"
2.644 + by (rule minus_inverts_plus1) simp
2.645 +
2.646 +lemma Dig_of_num_neg:
2.647 + assumes "k + m = n"
2.648 + shows "of_num m - of_num n = 0 - of_num k"
2.649 + by (rule minus_minus_zero_inverts_plus1) (simp add: of_num_plus assms)
2.650 +
2.651 +lemmas Dig_plus_eval =
2.652 + of_num_plus of_num_eq_iff Dig_plus refl [of "1::num", THEN eqTrueI] num.inject
2.653 +
2.654 +simproc_setup numeral_minus ("of_num m - of_num n") = {*
2.655 + let
2.656 + (*TODO proper implicit use of morphism via pattern antiquotations*)
2.657 + fun cdest_of_num ct = (snd o split_last o snd o Drule.strip_comb) ct;
2.658 + fun cdest_minus ct = case (rev o snd o Drule.strip_comb) ct of [n, m] => (m, n);
2.659 + fun attach_num ct = (dest_num (Thm.term_of ct), ct);
2.660 + fun cdifference t = (pairself (attach_num o cdest_of_num) o cdest_minus) t;
2.661 + val simplify = MetaSimplifier.rewrite false (map mk_meta_eq @{thms Dig_plus_eval});
2.662 + fun cert ck cl cj = @{thm eqTrueE} OF [@{thm meta_eq_to_obj_eq} OF [simplify (Drule.list_comb (@{cterm "op = :: num \<Rightarrow> _"},
2.663 + [Drule.list_comb (@{cterm "op + :: num \<Rightarrow> _"}, [ck, cl]), cj]))]];
2.664 + in fn phi => fn _ => fn ct => case try cdifference ct
2.665 + of NONE => (NONE)
2.666 + | SOME ((k, ck), (l, cl)) => SOME (let val j = k - l in if j = 0
2.667 + then MetaSimplifier.rewrite false [mk_meta_eq (Morphism.thm phi @{thm Dig_of_num_zero})] ct
2.668 + else mk_meta_eq (let
2.669 + val cj = Thm.cterm_of (Thm.theory_of_cterm ct) (mk_num (abs j));
2.670 + in
2.671 + (if j > 0 then (Morphism.thm phi @{thm Dig_of_num_pos}) OF [cert cj cl ck]
2.672 + else (Morphism.thm phi @{thm Dig_of_num_neg}) OF [cert cj ck cl])
2.673 + end) end)
2.674 + end
2.675 +*}
2.676 +
2.677 +lemma Dig_of_num_minus_zero [numeral]:
2.678 + "of_num n - 0 = of_num n"
2.679 + by (simp add: minus_inverts_plus1)
2.680 +
2.681 +lemma Dig_one_minus_zero [numeral]:
2.682 + "1 - 0 = 1"
2.683 + by (simp add: minus_inverts_plus1)
2.684 +
2.685 +lemma Dig_one_minus_one [numeral]:
2.686 + "1 - 1 = 0"
2.687 + by (simp add: minus_inverts_plus1)
2.688 +
2.689 +lemma Dig_of_num_minus_one [numeral]:
2.690 + "of_num (Dig0 n) - 1 = of_num (dec (Dig0 n))"
2.691 + "of_num (Dig1 n) - 1 = of_num (Dig0 n)"
2.692 + by (auto intro: minus_inverts_plus1 simp add: Dig_dec_plus_one of_num.simps of_num_plus_one)
2.693 +
2.694 +lemma Dig_one_minus_of_num [numeral]:
2.695 + "1 - of_num (Dig0 n) = 0 - of_num (dec (Dig0 n))"
2.696 + "1 - of_num (Dig1 n) = 0 - of_num (Dig0 n)"
2.697 + by (auto intro: minus_minus_zero_inverts_plus1 simp add: Dig_dec_plus_one of_num.simps of_num_plus_one)
2.698 +
2.699 +end
2.700 +
2.701 +context ring_1
2.702 +begin
2.703 +
2.704 +subclass semiring_1_minus
2.705 + by unfold_locales (simp_all add: ring_simps)
2.706 +
2.707 +lemma Dig_zero_minus_of_num [numeral]:
2.708 + "0 - of_num n = - of_num n"
2.709 + by simp
2.710 +
2.711 +lemma Dig_zero_minus_one [numeral]:
2.712 + "0 - 1 = - 1"
2.713 + by simp
2.714 +
2.715 +lemma Dig_uminus_uminus [numeral]:
2.716 + "- (- of_num n) = of_num n"
2.717 + by simp
2.718 +
2.719 +lemma Dig_plus_uminus [numeral]:
2.720 + "of_num m + - of_num n = of_num m - of_num n"
2.721 + "- of_num m + of_num n = of_num n - of_num m"
2.722 + "- of_num m + - of_num n = - (of_num m + of_num n)"
2.723 + "of_num m - - of_num n = of_num m + of_num n"
2.724 + "- of_num m - of_num n = - (of_num m + of_num n)"
2.725 + "- of_num m - - of_num n = of_num n - of_num m"
2.726 + by (simp_all add: diff_minus add_commute)
2.727 +
2.728 +lemma Dig_times_uminus [numeral]:
2.729 + "- of_num n * of_num m = - (of_num n * of_num m)"
2.730 + "of_num n * - of_num m = - (of_num n * of_num m)"
2.731 + "- of_num n * - of_num m = of_num n * of_num m"
2.732 + by (simp_all add: minus_mult_left [symmetric] minus_mult_right [symmetric])
2.733 +
2.734 +lemma of_int_of_num [numeral]: "of_int (of_num n) = of_num n"
2.735 +by (induct n)
2.736 + (simp_all only: of_num.simps semiring_numeral_class.of_num.simps of_int_add, simp_all)
2.737 +
2.738 +declare of_int_1 [numeral]
2.739 +
2.740 +end
2.741 +
2.742 +text {*
2.743 + Greetings to @{typ nat}.
2.744 +*}
2.745 +
2.746 +instance nat :: semiring_1_minus proof qed simp_all
2.747 +
2.748 +lemma Suc_of_num [numeral]: "Suc (of_num n) = of_num (n + 1)"
2.749 + unfolding of_num_plus_one [symmetric] by simp
2.750 +
2.751 +lemma nat_number:
2.752 + "1 = Suc 0"
2.753 + "of_num 1 = Suc 0"
2.754 + "of_num (Dig0 n) = Suc (of_num (dec (Dig0 n)))"
2.755 + "of_num (Dig1 n) = Suc (of_num (Dig0 n))"
2.756 + by (simp_all add: of_num.simps Dig_dec_plus_one Suc_of_num)
2.757 +
2.758 +declare diff_0_eq_0 [numeral]
2.759 +
2.760 +
2.761 +subsection {* Code generator setup for @{typ int} *}
2.762 +
2.763 +definition Pls :: "num \<Rightarrow> int" where
2.764 + [simp, code post]: "Pls n = of_num n"
2.765 +
2.766 +definition Mns :: "num \<Rightarrow> int" where
2.767 + [simp, code post]: "Mns n = - of_num n"
2.768 +
2.769 +code_datatype "0::int" Pls Mns
2.770 +
2.771 +lemmas [code inline] = Pls_def [symmetric] Mns_def [symmetric]
2.772 +
2.773 +definition sub :: "num \<Rightarrow> num \<Rightarrow> int" where
2.774 + [simp, code func del]: "sub m n = (of_num m - of_num n)"
2.775 +
2.776 +definition dup :: "int \<Rightarrow> int" where
2.777 + [code func del]: "dup k = 2 * k"
2.778 +
2.779 +lemma Dig_sub [code]:
2.780 + "sub 1 1 = 0"
2.781 + "sub (Dig0 m) 1 = of_num (dec (Dig0 m))"
2.782 + "sub (Dig1 m) 1 = of_num (Dig0 m)"
2.783 + "sub 1 (Dig0 n) = - of_num (dec (Dig0 n))"
2.784 + "sub 1 (Dig1 n) = - of_num (Dig0 n)"
2.785 + "sub (Dig0 m) (Dig0 n) = dup (sub m n)"
2.786 + "sub (Dig1 m) (Dig1 n) = dup (sub m n)"
2.787 + "sub (Dig1 m) (Dig0 n) = dup (sub m n) + 1"
2.788 + "sub (Dig0 m) (Dig1 n) = dup (sub m n) - 1"
2.789 + apply (simp_all add: dup_def ring_simps)
2.790 + apply (simp_all add: of_num_plus Dig_one_plus_dec)[4]
2.791 + apply (simp_all add: of_num.simps)
2.792 + done
2.793 +
2.794 +lemma dup_code [code]:
2.795 + "dup 0 = 0"
2.796 + "dup (Pls n) = Pls (Dig0 n)"
2.797 + "dup (Mns n) = Mns (Dig0 n)"
2.798 + by (simp_all add: dup_def of_num.simps)
2.799 +
2.800 +lemma [code func, code func del]:
2.801 + "(1 :: int) = 1"
2.802 + "(op + :: int \<Rightarrow> int \<Rightarrow> int) = op +"
2.803 + "(uminus :: int \<Rightarrow> int) = uminus"
2.804 + "(op - :: int \<Rightarrow> int \<Rightarrow> int) = op -"
2.805 + "(op * :: int \<Rightarrow> int \<Rightarrow> int) = op *"
2.806 + "(op = :: int \<Rightarrow> int \<Rightarrow> bool) = op ="
2.807 + "(op \<le> :: int \<Rightarrow> int \<Rightarrow> bool) = op \<le>"
2.808 + "(op < :: int \<Rightarrow> int \<Rightarrow> bool) = op <"
2.809 + by rule+
2.810 +
2.811 +lemma one_int_code [code]:
2.812 + "1 = Pls 1"
2.813 + by (simp add: of_num_one)
2.814 +
2.815 +lemma plus_int_code [code]:
2.816 + "k + 0 = (k::int)"
2.817 + "0 + l = (l::int)"
2.818 + "Pls m + Pls n = Pls (m + n)"
2.819 + "Pls m - Pls n = sub m n"
2.820 + "Mns m + Mns n = Mns (m + n)"
2.821 + "Mns m - Mns n = sub n m"
2.822 + by (simp_all add: of_num_plus [symmetric])
2.823 +
2.824 +lemma uminus_int_code [code]:
2.825 + "uminus 0 = (0::int)"
2.826 + "uminus (Pls m) = Mns m"
2.827 + "uminus (Mns m) = Pls m"
2.828 + by simp_all
2.829 +
2.830 +lemma minus_int_code [code]:
2.831 + "k - 0 = (k::int)"
2.832 + "0 - l = uminus (l::int)"
2.833 + "Pls m - Pls n = sub m n"
2.834 + "Pls m - Mns n = Pls (m + n)"
2.835 + "Mns m - Pls n = Mns (m + n)"
2.836 + "Mns m - Mns n = sub n m"
2.837 + by (simp_all add: of_num_plus [symmetric])
2.838 +
2.839 +lemma times_int_code [code]:
2.840 + "k * 0 = (0::int)"
2.841 + "0 * l = (0::int)"
2.842 + "Pls m * Pls n = Pls (m * n)"
2.843 + "Pls m * Mns n = Mns (m * n)"
2.844 + "Mns m * Pls n = Mns (m * n)"
2.845 + "Mns m * Mns n = Pls (m * n)"
2.846 + by (simp_all add: of_num_times [symmetric])
2.847 +
2.848 +lemma eq_int_code [code]:
2.849 + "0 = (0::int) \<longleftrightarrow> True"
2.850 + "0 = Pls l \<longleftrightarrow> False"
2.851 + "0 = Mns l \<longleftrightarrow> False"
2.852 + "Pls k = 0 \<longleftrightarrow> False"
2.853 + "Pls k = Pls l \<longleftrightarrow> k = l"
2.854 + "Pls k = Mns l \<longleftrightarrow> False"
2.855 + "Mns k = 0 \<longleftrightarrow> False"
2.856 + "Mns k = Pls l \<longleftrightarrow> False"
2.857 + "Mns k = Mns l \<longleftrightarrow> k = l"
2.858 + using of_num_pos [of l, where ?'a = int] of_num_pos [of k, where ?'a = int]
2.859 + by (simp_all add: of_num_eq_iff)
2.860 +
2.861 +lemma less_eq_int_code [code]:
2.862 + "0 \<le> (0::int) \<longleftrightarrow> True"
2.863 + "0 \<le> Pls l \<longleftrightarrow> True"
2.864 + "0 \<le> Mns l \<longleftrightarrow> False"
2.865 + "Pls k \<le> 0 \<longleftrightarrow> False"
2.866 + "Pls k \<le> Pls l \<longleftrightarrow> k \<le> l"
2.867 + "Pls k \<le> Mns l \<longleftrightarrow> False"
2.868 + "Mns k \<le> 0 \<longleftrightarrow> True"
2.869 + "Mns k \<le> Pls l \<longleftrightarrow> True"
2.870 + "Mns k \<le> Mns l \<longleftrightarrow> l \<le> k"
2.871 + using of_num_pos [of l, where ?'a = int] of_num_pos [of k, where ?'a = int]
2.872 + by (simp_all add: of_num_less_eq_iff)
2.873 +
2.874 +lemma less_int_code [code]:
2.875 + "0 < (0::int) \<longleftrightarrow> False"
2.876 + "0 < Pls l \<longleftrightarrow> True"
2.877 + "0 < Mns l \<longleftrightarrow> False"
2.878 + "Pls k < 0 \<longleftrightarrow> False"
2.879 + "Pls k < Pls l \<longleftrightarrow> k < l"
2.880 + "Pls k < Mns l \<longleftrightarrow> False"
2.881 + "Mns k < 0 \<longleftrightarrow> True"
2.882 + "Mns k < Pls l \<longleftrightarrow> True"
2.883 + "Mns k < Mns l \<longleftrightarrow> l < k"
2.884 + using of_num_pos [of l, where ?'a = int] of_num_pos [of k, where ?'a = int]
2.885 + by (simp_all add: of_num_less_iff)
2.886 +
2.887 +lemma [code inline del]: "(0::int) \<equiv> Numeral0" by simp
2.888 +lemma [code inline del]: "(1::int) \<equiv> Numeral1" by simp
2.889 +declare zero_is_num_zero [code inline del]
2.890 +declare one_is_num_one [code inline del]
2.891 +
2.892 +hide (open) const sub dup
2.893 +
2.894 +
2.895 +subsection {* Numeral equations as default simplification rules *}
2.896 +
2.897 +text {* TODO. Be more precise here with respect to subsumed facts. *}
2.898 +declare (in semiring_numeral) numeral [simp]
2.899 +declare (in semiring_1) numeral [simp]
2.900 +declare (in semiring_char_0) numeral [simp]
2.901 +declare (in ring_1) numeral [simp]
2.902 +thm numeral
2.903 +
2.904 +
2.905 +text {* Toy examples *}
2.906 +
2.907 +definition "bar \<longleftrightarrow> #4 * #2 + #7 = (#8 :: nat) \<and> #4 * #2 + #7 \<ge> (#8 :: int) - #3"
2.908 +code_thms bar
2.909 +export_code bar in Haskell file -
2.910 +export_code bar in OCaml module_name Foo file -
2.911 +ML {* @{code bar} *}
2.912 +
2.913 +end
3.1 --- a/src/HOL/ex/ROOT.ML Wed Aug 27 12:00:28 2008 +0200
3.2 +++ b/src/HOL/ex/ROOT.ML Wed Aug 27 12:01:59 2008 +0200
3.3 @@ -20,6 +20,7 @@
3.4 no_document use_thy "Codegenerator_Pretty";
3.5
3.6 use_thys [
3.7 + "Numeral",
3.8 "ImperativeQuicksort",
3.9 "Higher_Order_Logic",
3.10 "Abstract_NAT",