28021

1 
(* Title: HOL/ex/Numeral.thy


2 
ID: $Id$


3 
Author: Florian Haftmann


4 


5 
An experimental alternative numeral representation.


6 
*)


7 


8 
theory Numeral


9 
imports Int Inductive


10 
begin


11 


12 
subsection {* The @{text num} type *}


13 


14 
text {*


15 
We construct @{text num} as a copy of strictly positive


16 
natural numbers.


17 
*}


18 


19 
typedef (open) num = "\<lambda>n\<Colon>nat. n > 0"


20 
morphisms nat_of_num num_of_nat_abs


21 
by (auto simp add: mem_def)


22 


23 
text {*


24 
A totalized abstraction function. It is not entirely clear


25 
whether this is really useful.


26 
*}


27 


28 
definition num_of_nat :: "nat \<Rightarrow> num" where


29 
"num_of_nat n = (if n = 0 then num_of_nat_abs 1 else num_of_nat_abs n)"


30 


31 
lemma num_cases [case_names nat, cases type: num]:


32 
assumes "(\<And>n\<Colon>nat. m = num_of_nat n \<Longrightarrow> 0 < n \<Longrightarrow> P)"


33 
shows P


34 
apply (rule num_of_nat_abs_cases)


35 
apply (unfold mem_def)


36 
using assms unfolding num_of_nat_def


37 
apply auto


38 
done


39 


40 
lemma num_of_nat_zero: "num_of_nat 0 = num_of_nat 1"


41 
by (simp add: num_of_nat_def)


42 


43 
lemma num_of_nat_inverse: "nat_of_num (num_of_nat n) = (if n = 0 then 1 else n)"


44 
apply (simp add: num_of_nat_def)


45 
apply (subst num_of_nat_abs_inverse)


46 
apply (auto simp add: mem_def num_of_nat_abs_inverse)


47 
done


48 


49 
lemma num_of_nat_inject:


50 
"num_of_nat m = num_of_nat n \<longleftrightarrow> m = n \<or> (m = 0 \<or> m = 1) \<and> (n = 0 \<or> n = 1)"


51 
by (auto simp add: num_of_nat_def num_of_nat_abs_inject [unfolded mem_def])


52 


53 
lemma split_num_all:


54 
"(\<And>m. PROP P m) \<equiv> (\<And>n. PROP P (num_of_nat n))"


55 
proof


56 
fix n


57 
assume "\<And>m\<Colon>num. PROP P m"


58 
then show "PROP P (num_of_nat n)" .


59 
next


60 
fix m


61 
have nat_of_num: "\<And>m. nat_of_num m \<noteq> 0"


62 
using nat_of_num by (auto simp add: mem_def)


63 
have nat_of_num_inverse: "\<And>m. num_of_nat (nat_of_num m) = m"


64 
by (auto simp add: num_of_nat_def nat_of_num_inverse nat_of_num)


65 
assume "\<And>n. PROP P (num_of_nat n)"


66 
then have "PROP P (num_of_nat (nat_of_num m))" .


67 
then show "PROP P m" unfolding nat_of_num_inverse .


68 
qed


69 


70 


71 
subsection {* Digit representation for @{typ num} *}


72 


73 
instantiation num :: "{semiring, monoid_mult}"


74 
begin


75 


76 
definition one_num :: num where


77 
[code func del]: "1 = num_of_nat 1"


78 


79 
definition plus_num :: "num \<Rightarrow> num \<Rightarrow> num" where


80 
[code func del]: "m + n = num_of_nat (nat_of_num m + nat_of_num n)"


81 


82 
definition times_num :: "num \<Rightarrow> num \<Rightarrow> num" where


83 
[code func del]: "m * n = num_of_nat (nat_of_num m * nat_of_num n)"


84 


85 
definition Dig0 :: "num \<Rightarrow> num" where


86 
[code func del]: "Dig0 n = n + n"


87 


88 
definition Dig1 :: "num \<Rightarrow> num" where


89 
[code func del]: "Dig1 n = n + n + 1"


90 


91 
instance proof


92 
qed (simp_all add: one_num_def plus_num_def times_num_def


93 
split_num_all num_of_nat_inverse num_of_nat_zero add_ac mult_ac nat_distrib)


94 


95 
end


96 


97 
text {*


98 
The following proofs seem horribly complicated.


99 
Any room for simplification!?


100 
*}


101 


102 
lemma nat_dig_cases [case_names 0 1 dig0 dig1]:


103 
fixes n :: nat


104 
assumes "n = 0 \<Longrightarrow> P"


105 
and "n = 1 \<Longrightarrow> P"


106 
and "\<And>m. m > 0 \<Longrightarrow> n = m + m \<Longrightarrow> P"


107 
and "\<And>m. m > 0 \<Longrightarrow> n = Suc (m + m) \<Longrightarrow> P"


108 
shows P


109 
using assms proof (induct n)


110 
case 0 then show ?case by simp


111 
next


112 
case (Suc n)


113 
show P proof (rule Suc.hyps)


114 
assume "n = 0"


115 
then have "Suc n = 1" by simp


116 
then show P by (rule Suc.prems(2))


117 
next


118 
assume "n = 1"


119 
have "1 > (0\<Colon>nat)" by simp


120 
moreover from `n = 1` have "Suc n = 1 + 1" by simp


121 
ultimately show P by (rule Suc.prems(3))


122 
next


123 
fix m


124 
assume "0 < m" and "n = m + m"


125 
note `0 < m`


126 
moreover from `n = m + m` have "Suc n = Suc (m + m)" by simp


127 
ultimately show P by (rule Suc.prems(4))


128 
next


129 
fix m


130 
assume "0 < m" and "n = Suc (m + m)"


131 
have "0 < Suc m" by simp


132 
moreover from `n = Suc (m + m)` have "Suc n = Suc m + Suc m" by simp


133 
ultimately show P by (rule Suc.prems(3))


134 
qed


135 
qed


136 


137 
lemma num_induct_raw:


138 
fixes n :: nat


139 
assumes not0: "n > 0"


140 
assumes "P 1"


141 
and "\<And>n. n > 0 \<Longrightarrow> P n \<Longrightarrow> P (n + n)"


142 
and "\<And>n. n > 0 \<Longrightarrow> P n \<Longrightarrow> P (Suc (n + n))"


143 
shows "P n"


144 
using not0 proof (induct n rule: less_induct)


145 
case (less n)


146 
show "P n" proof (cases n rule: nat_dig_cases)


147 
case 0 then show ?thesis using less by simp


148 
next


149 
case 1 then show ?thesis using assms by simp


150 
next


151 
case (dig0 m)


152 
then show ?thesis apply simp


153 
apply (rule assms(3)) apply assumption


154 
apply (rule less)


155 
apply simp_all


156 
done


157 
next


158 
case (dig1 m)


159 
then show ?thesis apply simp


160 
apply (rule assms(4)) apply assumption


161 
apply (rule less)


162 
apply simp_all


163 
done


164 
qed


165 
qed


166 


167 
lemma num_of_nat_Suc: "num_of_nat (Suc n) = (if n = 0 then 1 else num_of_nat n + 1)"


168 
by (cases n) (auto simp add: one_num_def plus_num_def num_of_nat_inverse)


169 


170 
lemma num_induct [case_names 1 Suc, induct type: num]:


171 
fixes P :: "num \<Rightarrow> bool"


172 
assumes 1: "P 1"


173 
and Suc: "\<And>n. P n \<Longrightarrow> P (n + 1)"


174 
shows "P n"


175 
proof (cases n)


176 
case (nat m) then show ?thesis by (induct m arbitrary: n)


177 
(auto simp: num_of_nat_Suc intro: 1 Suc split: split_if_asm)


178 
qed


179 


180 
rep_datatype "1::num" Dig0 Dig1 proof 


181 
fix P m


182 
assume 1: "P 1"


183 
and Dig0: "\<And>m. P m \<Longrightarrow> P (Dig0 m)"


184 
and Dig1: "\<And>m. P m \<Longrightarrow> P (Dig1 m)"


185 
obtain n where "0 < n" and m: "m = num_of_nat n"


186 
by (cases m) auto


187 
from `0 < n` have "P (num_of_nat n)" proof (induct n rule: num_induct_raw)


188 
case 1 from `0 < n` show ?case .


189 
next


190 
case 2 with 1 show ?case by (simp add: one_num_def)


191 
next


192 
case (3 n) then have "P (num_of_nat n)" by auto


193 
then have "P (Dig0 (num_of_nat n))" by (rule Dig0)


194 
with 3 show ?case by (simp add: Dig0_def plus_num_def num_of_nat_inverse)


195 
next


196 
case (4 n) then have "P (num_of_nat n)" by auto


197 
then have "P (Dig1 (num_of_nat n))" by (rule Dig1)


198 
with 4 show ?case by (simp add: Dig1_def one_num_def plus_num_def num_of_nat_inverse)


199 
qed


200 
with m show "P m" by simp


201 
next


202 
fix m n


203 
show "Dig0 m = Dig0 n \<longleftrightarrow> m = n"


204 
apply (cases m) apply (cases n)


205 
by (auto simp add: Dig0_def plus_num_def num_of_nat_inverse num_of_nat_inject)


206 
next


207 
fix m n


208 
show "Dig1 m = Dig1 n \<longleftrightarrow> m = n"


209 
apply (cases m) apply (cases n)


210 
by (auto simp add: Dig1_def plus_num_def num_of_nat_inverse num_of_nat_inject)


211 
next


212 
fix n


213 
show "1 \<noteq> Dig0 n"


214 
apply (cases n)


215 
by (auto simp add: Dig0_def one_num_def plus_num_def num_of_nat_inverse num_of_nat_inject)


216 
next


217 
fix n


218 
show "1 \<noteq> Dig1 n"


219 
apply (cases n)


220 
by (auto simp add: Dig1_def one_num_def plus_num_def num_of_nat_inverse num_of_nat_inject)


221 
next


222 
fix m n


223 
have "\<And>n m. n + n \<noteq> Suc (m + m)"


224 
proof 


225 
fix n m


226 
show "n + n \<noteq> Suc (m + m)"


227 
proof (induct m arbitrary: n)


228 
case 0 then show ?case by (cases n) simp_all


229 
next


230 
case (Suc m) then show ?case by (cases n) simp_all


231 
qed


232 
qed


233 
then show "Dig0 n \<noteq> Dig1 m"


234 
apply (cases n) apply (cases m)


235 
by (auto simp add: Dig0_def Dig1_def one_num_def plus_num_def num_of_nat_inverse num_of_nat_inject)


236 
qed


237 


238 
text {*


239 
From now on, there are two possible models for @{typ num}:


240 
as positive naturals (rules @{text "num_induct"}, @{text "num_cases"})


241 
and as digit representation (rules @{text "num.induct"}, @{text "num.cases"}).


242 


243 
It is not entirely clear in which context it is better to use


244 
the one or the other, or whether the construction should be reversed.


245 
*}


246 


247 


248 
subsection {* Binary numerals *}


249 


250 
text {*


251 
We embed binary representations into a generic algebraic


252 
structure using @{text of_num}


253 
*}


254 


255 
ML {*


256 
structure DigSimps =


257 
NamedThmsFun(val name = "numeral"; val description = "Simplification rules for numerals")


258 
*}


259 


260 
setup DigSimps.setup


261 


262 
class semiring_numeral = semiring + monoid_mult


263 
begin


264 


265 
primrec of_num :: "num \<Rightarrow> 'a" where


266 
of_num_one [numeral]: "of_num 1 = 1"


267 
 "of_num (Dig0 n) = of_num n + of_num n"


268 
 "of_num (Dig1 n) = of_num n + of_num n + 1"


269 


270 
declare of_num.simps [simp del]


271 


272 
end


273 


274 
text {*


275 
ML stuff and syntax.


276 
*}


277 


278 
ML {*


279 
fun mk_num 1 = @{term "1::num"}


280 
 mk_num k =


281 
let


282 
val (l, b) = Integer.div_mod k 2;


283 
val bit = (if b = 0 then @{term Dig0} else @{term Dig1});


284 
in bit $ (mk_num l) end;


285 


286 
fun dest_num @{term "1::num"} = 1


287 
 dest_num (@{term Dig0} $ n) = 2 * dest_num n


288 
 dest_num (@{term Dig1} $ n) = 2 * dest_num n + 1;


289 


290 
(*FIXME these have to gain proper context via morphisms phi*)


291 


292 
fun mk_numeral T k = Const (@{const_name of_num}, @{typ num} > T)


293 
$ mk_num k


294 


295 
fun dest_numeral (Const (@{const_name of_num}, Type ("fun", [@{typ num}, T])) $ t) =


296 
(T, dest_num t)


297 
*}


298 


299 
syntax


300 
"_Numerals" :: "xnum \<Rightarrow> 'a" ("_")


301 


302 
parse_translation {*


303 
let


304 
fun num_of_int n = if n > 0 then case IntInf.quotRem (n, 2)


305 
of (0, 1) => Const (@{const_name HOL.one}, dummyT)


306 
 (n, 0) => Const (@{const_name Dig0}, dummyT) $ num_of_int n


307 
 (n, 1) => Const (@{const_name Dig1}, dummyT) $ num_of_int n


308 
else raise Match;


309 
fun numeral_tr [Free (num, _)] =


310 
let


311 
val {leading_zeros, value, ...} = Syntax.read_xnum num;


312 
val _ = leading_zeros = 0 andalso value > 0


313 
orelse error ("Bad numeral: " ^ num);


314 
in Const (@{const_name of_num}, @{typ num} > dummyT) $ num_of_int value end


315 
 numeral_tr ts = raise TERM ("numeral_tr", ts);


316 
in [("_Numerals", numeral_tr)] end


317 
*}


318 


319 
typed_print_translation {*


320 
let


321 
fun dig b n = b + 2 * n;


322 
fun int_of_num' (Const (@{const_syntax Dig0}, _) $ n) =


323 
dig 0 (int_of_num' n)


324 
 int_of_num' (Const (@{const_syntax Dig1}, _) $ n) =


325 
dig 1 (int_of_num' n)


326 
 int_of_num' (Const (@{const_syntax HOL.one}, _)) = 1;


327 
fun num_tr' show_sorts T [n] =


328 
let


329 
val k = int_of_num' n;


330 
val t' = Syntax.const "_Numerals" $ Syntax.free ("#" ^ string_of_int k);


331 
in case T


332 
of Type ("fun", [_, T']) =>


333 
if not (! show_types) andalso can Term.dest_Type T' then t'


334 
else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T'


335 
 T' => if T' = dummyT then t' else raise Match


336 
end;


337 
in [(@{const_syntax of_num}, num_tr')] end


338 
*}


339 


340 


341 
subsection {* Numeral operations *}


342 


343 
text {*


344 
First, addition and multiplication on digits.


345 
*}


346 


347 
lemma Dig_plus [numeral, simp, code]:


348 
"1 + 1 = Dig0 1"


349 
"1 + Dig0 m = Dig1 m"


350 
"1 + Dig1 m = Dig0 (m + 1)"


351 
"Dig0 n + 1 = Dig1 n"


352 
"Dig0 n + Dig0 m = Dig0 (n + m)"


353 
"Dig0 n + Dig1 m = Dig1 (n + m)"


354 
"Dig1 n + 1 = Dig0 (n + 1)"


355 
"Dig1 n + Dig0 m = Dig1 (n + m)"


356 
"Dig1 n + Dig1 m = Dig0 (n + m + 1)"


357 
by (simp_all add: add_ac Dig0_def Dig1_def)


358 


359 
lemma Dig_times [numeral, simp, code]:


360 
"1 * 1 = (1::num)"


361 
"1 * Dig0 n = Dig0 n"


362 
"1 * Dig1 n = Dig1 n"


363 
"Dig0 n * 1 = Dig0 n"


364 
"Dig0 n * Dig0 m = Dig0 (n * Dig0 m)"


365 
"Dig0 n * Dig1 m = Dig0 (n * Dig1 m)"


366 
"Dig1 n * 1 = Dig1 n"


367 
"Dig1 n * Dig0 m = Dig0 (n * Dig0 m + m)"


368 
"Dig1 n * Dig1 m = Dig1 (n * Dig1 m + m)"


369 
by (simp_all add: left_distrib right_distrib add_ac Dig0_def Dig1_def)


370 


371 
text {*


372 
@{const of_num} is a morphism.


373 
*}


374 


375 
context semiring_numeral


376 
begin


377 


378 
abbreviation "Num1 \<equiv> of_num 1"


379 


380 
text {*


381 
Alas, there is still the duplication of @{term 1},


382 
thought the duplicated @{term 0} has disappeared.


383 
We could get rid of it by replacing the constructor


384 
@{term 1} in @{typ num} by two constructors


385 
@{text two} and @{text three}, resulting in a further


386 
blowup. But it could be worth the effort.


387 
*}


388 


389 
lemma of_num_plus_one [numeral]:


390 
"of_num n + 1 = of_num (n + 1)"


391 
by (rule sym, induct n) (simp_all add: Dig_plus of_num.simps add_ac)


392 


393 
lemma of_num_one_plus [numeral]:


394 
"1 + of_num n = of_num (n + 1)"


395 
unfolding of_num_plus_one [symmetric] add_commute ..


396 


397 
lemma of_num_plus [numeral]:


398 
"of_num m + of_num n = of_num (m + n)"


399 
by (induct n rule: num_induct)


400 
(simp_all add: Dig_plus of_num_one semigroup_add_class.plus.add_assoc [symmetric, of m]


401 
add_ac of_num_plus_one [symmetric])


402 


403 
lemma of_num_times_one [numeral]:


404 
"of_num n * 1 = of_num n"


405 
by simp


406 


407 
lemma of_num_one_times [numeral]:


408 
"1 * of_num n = of_num n"


409 
by simp


410 


411 
lemma of_num_times [numeral]:


412 
"of_num m * of_num n = of_num (m * n)"


413 
by (induct n rule: num_induct)


414 
(simp_all add: of_num_plus [symmetric]


415 
semiring_class.plus_times.right_distrib right_distrib of_num_one)


416 


417 
end


418 


419 
text {*


420 
Structures with a @{term 0}.


421 
*}


422 


423 
context semiring_1


424 
begin


425 


426 
subclass semiring_numeral ..


427 


428 
lemma of_nat_of_num [numeral]: "of_nat (of_num n) = of_num n"


429 
by (induct n)


430 
(simp_all add: semiring_numeral_class.of_num.simps of_num.simps add_ac)


431 


432 
declare of_nat_1 [numeral]


433 


434 
lemma Dig_plus_zero [numeral]:


435 
"0 + 1 = 1"


436 
"0 + of_num n = of_num n"


437 
"1 + 0 = 1"


438 
"of_num n + 0 = of_num n"


439 
by simp_all


440 


441 
lemma Dig_times_zero [numeral]:


442 
"0 * 1 = 0"


443 
"0 * of_num n = 0"


444 
"1 * 0 = 0"


445 
"of_num n * 0 = 0"


446 
by simp_all


447 


448 
end


449 


450 
lemma nat_of_num_of_num: "nat_of_num = of_num"


451 
proof


452 
fix n


453 
have "of_num n = nat_of_num n" apply (induct n)


454 
apply (simp_all add: of_num.simps)


455 
using nat_of_num


456 
apply (simp_all add: one_num_def plus_num_def Dig0_def Dig1_def num_of_nat_inverse mem_def)


457 
done


458 
then show "nat_of_num n = of_num n" by simp


459 
qed


460 


461 
text {*


462 
Equality.


463 
*}


464 


465 
context semiring_char_0


466 
begin


467 


468 
lemma of_num_eq_iff [numeral]:


469 
"of_num m = of_num n \<longleftrightarrow> m = n"


470 
unfolding of_nat_of_num [symmetric] nat_of_num_of_num [symmetric]


471 
of_nat_eq_iff nat_of_num_inject ..


472 


473 
lemma of_num_eq_one_iff [numeral]:


474 
"of_num n = 1 \<longleftrightarrow> n = 1"


475 
proof 


476 
have "of_num n = of_num 1 \<longleftrightarrow> n = 1" unfolding of_num_eq_iff ..


477 
then show ?thesis by (simp add: of_num_one)


478 
qed


479 


480 
lemma one_eq_of_num_iff [numeral]:


481 
"1 = of_num n \<longleftrightarrow> n = 1"


482 
unfolding of_num_eq_one_iff [symmetric] by auto


483 


484 
end


485 


486 
text {*


487 
Comparisons. Could be perhaps more general than here.


488 
*}


489 


490 
lemma (in ordered_semidom) of_num_pos: "0 < of_num n"


491 
proof 


492 
have "(0::nat) < of_num n"


493 
by (induct n) (simp_all add: semiring_numeral_class.of_num.simps)


494 
then have "of_nat 0 \<noteq> of_nat (of_num n)"


495 
by (cases n) (simp_all only: semiring_numeral_class.of_num.simps of_nat_eq_iff)


496 
then have "0 \<noteq> of_num n"


497 
by (simp add: of_nat_of_num)


498 
moreover have "0 \<le> of_nat (of_num n)" by simp


499 
ultimately show ?thesis by (simp add: of_nat_of_num)


500 
qed


501 


502 
instantiation num :: linorder


503 
begin


504 


505 
definition less_eq_num :: "num \<Rightarrow> num \<Rightarrow> bool" where


506 
[code func del]: "m \<le> n \<longleftrightarrow> nat_of_num m \<le> nat_of_num n"


507 


508 
definition less_num :: "num \<Rightarrow> num \<Rightarrow> bool" where


509 
[code func del]: "m < n \<longleftrightarrow> nat_of_num m < nat_of_num n"


510 


511 
instance proof


512 
qed (auto simp add: less_eq_num_def less_num_def


513 
split_num_all num_of_nat_inverse num_of_nat_inject split: split_if_asm)


514 


515 
end


516 


517 
lemma less_eq_num_code [numeral, simp, code]:


518 
"(1::num) \<le> n \<longleftrightarrow> True"


519 
"Dig0 m \<le> 1 \<longleftrightarrow> False"


520 
"Dig1 m \<le> 1 \<longleftrightarrow> False"


521 
"Dig0 m \<le> Dig0 n \<longleftrightarrow> m \<le> n"


522 
"Dig0 m \<le> Dig1 n \<longleftrightarrow> m \<le> n"


523 
"Dig1 m \<le> Dig1 n \<longleftrightarrow> m \<le> n"


524 
"Dig1 m \<le> Dig0 n \<longleftrightarrow> m < n"


525 
using of_num_pos [of n, where ?'a = nat] of_num_pos [of m, where ?'a = nat]


526 
by (auto simp add: less_eq_num_def less_num_def nat_of_num_of_num of_num.simps)


527 


528 
lemma less_num_code [numeral, simp, code]:


529 
"m < (1::num) \<longleftrightarrow> False"


530 
"(1::num) < 1 \<longleftrightarrow> False"


531 
"1 < Dig0 n \<longleftrightarrow> True"


532 
"1 < Dig1 n \<longleftrightarrow> True"


533 
"Dig0 m < Dig0 n \<longleftrightarrow> m < n"


534 
"Dig0 m < Dig1 n \<longleftrightarrow> m \<le> n"


535 
"Dig1 m < Dig1 n \<longleftrightarrow> m < n"


536 
"Dig1 m < Dig0 n \<longleftrightarrow> m < n"


537 
using of_num_pos [of n, where ?'a = nat] of_num_pos [of m, where ?'a = nat]


538 
by (auto simp add: less_eq_num_def less_num_def nat_of_num_of_num of_num.simps)


539 


540 
context ordered_semidom


541 
begin


542 


543 
lemma of_num_less_eq_iff [numeral]: "of_num m \<le> of_num n \<longleftrightarrow> m \<le> n"


544 
proof 


545 
have "of_nat (of_num m) \<le> of_nat (of_num n) \<longleftrightarrow> m \<le> n"


546 
unfolding less_eq_num_def nat_of_num_of_num of_nat_le_iff ..


547 
then show ?thesis by (simp add: of_nat_of_num)


548 
qed


549 


550 
lemma of_num_less_eq_one_iff [numeral]: "of_num n \<le> 1 \<longleftrightarrow> n = 1"


551 
proof 


552 
have "of_num n \<le> of_num 1 \<longleftrightarrow> n = 1"


553 
by (cases n) (simp_all add: of_num_less_eq_iff)


554 
then show ?thesis by (simp add: of_num_one)


555 
qed


556 


557 
lemma one_less_eq_of_num_iff [numeral]: "1 \<le> of_num n"


558 
proof 


559 
have "of_num 1 \<le> of_num n"


560 
by (cases n) (simp_all add: of_num_less_eq_iff)


561 
then show ?thesis by (simp add: of_num_one)


562 
qed


563 


564 
lemma of_num_less_iff [numeral]: "of_num m < of_num n \<longleftrightarrow> m < n"


565 
proof 


566 
have "of_nat (of_num m) < of_nat (of_num n) \<longleftrightarrow> m < n"


567 
unfolding less_num_def nat_of_num_of_num of_nat_less_iff ..


568 
then show ?thesis by (simp add: of_nat_of_num)


569 
qed


570 


571 
lemma of_num_less_one_iff [numeral]: "\<not> of_num n < 1"


572 
proof 


573 
have "\<not> of_num n < of_num 1"


574 
by (cases n) (simp_all add: of_num_less_iff)


575 
then show ?thesis by (simp add: of_num_one)


576 
qed


577 


578 
lemma one_less_of_num_iff [numeral]: "1 < of_num n \<longleftrightarrow> n \<noteq> 1"


579 
proof 


580 
have "of_num 1 < of_num n \<longleftrightarrow> n \<noteq> 1"


581 
by (cases n) (simp_all add: of_num_less_iff)


582 
then show ?thesis by (simp add: of_num_one)


583 
qed


584 


585 
end


586 


587 
text {*


588 
Structures with subtraction @{term "op "}.


589 
*}


590 


591 
text {* A decrement function *}


592 


593 
primrec dec :: "num \<Rightarrow> num" where


594 
"dec 1 = 1"


595 
 "dec (Dig0 n) = (case n of 1 \<Rightarrow> 1  _ \<Rightarrow> Dig1 (dec n))"


596 
 "dec (Dig1 n) = Dig0 n"


597 


598 
declare dec.simps [simp del, code del]


599 


600 
lemma Dig_dec [numeral, simp, code]:


601 
"dec 1 = 1"


602 
"dec (Dig0 1) = 1"


603 
"dec (Dig0 (Dig0 n)) = Dig1 (dec (Dig0 n))"


604 
"dec (Dig0 (Dig1 n)) = Dig1 (Dig0 n)"


605 
"dec (Dig1 n) = Dig0 n"


606 
by (simp_all add: dec.simps)


607 


608 
lemma Dig_dec_plus_one:


609 
"dec n + 1 = (if n = 1 then Dig0 1 else n)"


610 
by (induct n)


611 
(auto simp add: Dig_plus dec.simps,


612 
auto simp add: Dig_plus split: num.splits)


613 


614 
lemma Dig_one_plus_dec:


615 
"1 + dec n = (if n = 1 then Dig0 1 else n)"


616 
unfolding add_commute [of 1] Dig_dec_plus_one ..


617 


618 
class semiring_minus = semiring + minus + zero +


619 
assumes minus_inverts_plus1: "a + b = c \<Longrightarrow> c  b = a"


620 
assumes minus_minus_zero_inverts_plus1: "a + b = c \<Longrightarrow> b  c = 0  a"


621 
begin


622 


623 
lemma minus_inverts_plus2: "a + b = c \<Longrightarrow> c  a = b"


624 
by (simp add: add_ac minus_inverts_plus1 [of b a])


625 


626 
lemma minus_minus_zero_inverts_plus2: "a + b = c \<Longrightarrow> a  c = 0  b"


627 
by (simp add: add_ac minus_minus_zero_inverts_plus1 [of b a])


628 


629 
end


630 


631 
class semiring_1_minus = semiring_1 + semiring_minus


632 
begin


633 


634 
lemma Dig_of_num_pos:


635 
assumes "k + n = m"


636 
shows "of_num m  of_num n = of_num k"


637 
using assms by (simp add: of_num_plus minus_inverts_plus1)


638 


639 
lemma Dig_of_num_zero:


640 
shows "of_num n  of_num n = 0"


641 
by (rule minus_inverts_plus1) simp


642 


643 
lemma Dig_of_num_neg:


644 
assumes "k + m = n"


645 
shows "of_num m  of_num n = 0  of_num k"


646 
by (rule minus_minus_zero_inverts_plus1) (simp add: of_num_plus assms)


647 


648 
lemmas Dig_plus_eval =


649 
of_num_plus of_num_eq_iff Dig_plus refl [of "1::num", THEN eqTrueI] num.inject


650 


651 
simproc_setup numeral_minus ("of_num m  of_num n") = {*


652 
let


653 
(*TODO proper implicit use of morphism via pattern antiquotations*)


654 
fun cdest_of_num ct = (snd o split_last o snd o Drule.strip_comb) ct;


655 
fun cdest_minus ct = case (rev o snd o Drule.strip_comb) ct of [n, m] => (m, n);


656 
fun attach_num ct = (dest_num (Thm.term_of ct), ct);


657 
fun cdifference t = (pairself (attach_num o cdest_of_num) o cdest_minus) t;


658 
val simplify = MetaSimplifier.rewrite false (map mk_meta_eq @{thms Dig_plus_eval});


659 
fun cert ck cl cj = @{thm eqTrueE} OF [@{thm meta_eq_to_obj_eq} OF [simplify (Drule.list_comb (@{cterm "op = :: num \<Rightarrow> _"},


660 
[Drule.list_comb (@{cterm "op + :: num \<Rightarrow> _"}, [ck, cl]), cj]))]];


661 
in fn phi => fn _ => fn ct => case try cdifference ct


662 
of NONE => (NONE)


663 
 SOME ((k, ck), (l, cl)) => SOME (let val j = k  l in if j = 0


664 
then MetaSimplifier.rewrite false [mk_meta_eq (Morphism.thm phi @{thm Dig_of_num_zero})] ct


665 
else mk_meta_eq (let


666 
val cj = Thm.cterm_of (Thm.theory_of_cterm ct) (mk_num (abs j));


667 
in


668 
(if j > 0 then (Morphism.thm phi @{thm Dig_of_num_pos}) OF [cert cj cl ck]


669 
else (Morphism.thm phi @{thm Dig_of_num_neg}) OF [cert cj ck cl])


670 
end) end)


671 
end


672 
*}


673 


674 
lemma Dig_of_num_minus_zero [numeral]:


675 
"of_num n  0 = of_num n"


676 
by (simp add: minus_inverts_plus1)


677 


678 
lemma Dig_one_minus_zero [numeral]:


679 
"1  0 = 1"


680 
by (simp add: minus_inverts_plus1)


681 


682 
lemma Dig_one_minus_one [numeral]:


683 
"1  1 = 0"


684 
by (simp add: minus_inverts_plus1)


685 


686 
lemma Dig_of_num_minus_one [numeral]:


687 
"of_num (Dig0 n)  1 = of_num (dec (Dig0 n))"


688 
"of_num (Dig1 n)  1 = of_num (Dig0 n)"


689 
by (auto intro: minus_inverts_plus1 simp add: Dig_dec_plus_one of_num.simps of_num_plus_one)


690 


691 
lemma Dig_one_minus_of_num [numeral]:


692 
"1  of_num (Dig0 n) = 0  of_num (dec (Dig0 n))"


693 
"1  of_num (Dig1 n) = 0  of_num (Dig0 n)"


694 
by (auto intro: minus_minus_zero_inverts_plus1 simp add: Dig_dec_plus_one of_num.simps of_num_plus_one)


695 


696 
end


697 


698 
context ring_1


699 
begin


700 


701 
subclass semiring_1_minus


702 
by unfold_locales (simp_all add: ring_simps)


703 


704 
lemma Dig_zero_minus_of_num [numeral]:


705 
"0  of_num n =  of_num n"


706 
by simp


707 


708 
lemma Dig_zero_minus_one [numeral]:


709 
"0  1 =  1"


710 
by simp


711 


712 
lemma Dig_uminus_uminus [numeral]:


713 
" ( of_num n) = of_num n"


714 
by simp


715 


716 
lemma Dig_plus_uminus [numeral]:


717 
"of_num m +  of_num n = of_num m  of_num n"


718 
" of_num m + of_num n = of_num n  of_num m"


719 
" of_num m +  of_num n =  (of_num m + of_num n)"


720 
"of_num m   of_num n = of_num m + of_num n"


721 
" of_num m  of_num n =  (of_num m + of_num n)"


722 
" of_num m   of_num n = of_num n  of_num m"


723 
by (simp_all add: diff_minus add_commute)


724 


725 
lemma Dig_times_uminus [numeral]:


726 
" of_num n * of_num m =  (of_num n * of_num m)"


727 
"of_num n *  of_num m =  (of_num n * of_num m)"


728 
" of_num n *  of_num m = of_num n * of_num m"


729 
by (simp_all add: minus_mult_left [symmetric] minus_mult_right [symmetric])


730 


731 
lemma of_int_of_num [numeral]: "of_int (of_num n) = of_num n"


732 
by (induct n)


733 
(simp_all only: of_num.simps semiring_numeral_class.of_num.simps of_int_add, simp_all)


734 


735 
declare of_int_1 [numeral]


736 


737 
end


738 


739 
text {*


740 
Greetings to @{typ nat}.


741 
*}


742 


743 
instance nat :: semiring_1_minus proof qed simp_all


744 


745 
lemma Suc_of_num [numeral]: "Suc (of_num n) = of_num (n + 1)"


746 
unfolding of_num_plus_one [symmetric] by simp


747 


748 
lemma nat_number:


749 
"1 = Suc 0"


750 
"of_num 1 = Suc 0"


751 
"of_num (Dig0 n) = Suc (of_num (dec (Dig0 n)))"


752 
"of_num (Dig1 n) = Suc (of_num (Dig0 n))"


753 
by (simp_all add: of_num.simps Dig_dec_plus_one Suc_of_num)


754 


755 
declare diff_0_eq_0 [numeral]


756 


757 


758 
subsection {* Code generator setup for @{typ int} *}


759 


760 
definition Pls :: "num \<Rightarrow> int" where


761 
[simp, code post]: "Pls n = of_num n"


762 


763 
definition Mns :: "num \<Rightarrow> int" where


764 
[simp, code post]: "Mns n =  of_num n"


765 


766 
code_datatype "0::int" Pls Mns


767 


768 
lemmas [code inline] = Pls_def [symmetric] Mns_def [symmetric]


769 


770 
definition sub :: "num \<Rightarrow> num \<Rightarrow> int" where


771 
[simp, code func del]: "sub m n = (of_num m  of_num n)"


772 


773 
definition dup :: "int \<Rightarrow> int" where


774 
[code func del]: "dup k = 2 * k"


775 


776 
lemma Dig_sub [code]:


777 
"sub 1 1 = 0"


778 
"sub (Dig0 m) 1 = of_num (dec (Dig0 m))"


779 
"sub (Dig1 m) 1 = of_num (Dig0 m)"


780 
"sub 1 (Dig0 n) =  of_num (dec (Dig0 n))"


781 
"sub 1 (Dig1 n) =  of_num (Dig0 n)"


782 
"sub (Dig0 m) (Dig0 n) = dup (sub m n)"


783 
"sub (Dig1 m) (Dig1 n) = dup (sub m n)"


784 
"sub (Dig1 m) (Dig0 n) = dup (sub m n) + 1"


785 
"sub (Dig0 m) (Dig1 n) = dup (sub m n)  1"


786 
apply (simp_all add: dup_def ring_simps)


787 
apply (simp_all add: of_num_plus Dig_one_plus_dec)[4]


788 
apply (simp_all add: of_num.simps)


789 
done


790 


791 
lemma dup_code [code]:


792 
"dup 0 = 0"


793 
"dup (Pls n) = Pls (Dig0 n)"


794 
"dup (Mns n) = Mns (Dig0 n)"


795 
by (simp_all add: dup_def of_num.simps)


796 


797 
lemma [code func, code func del]:


798 
"(1 :: int) = 1"


799 
"(op + :: int \<Rightarrow> int \<Rightarrow> int) = op +"


800 
"(uminus :: int \<Rightarrow> int) = uminus"


801 
"(op  :: int \<Rightarrow> int \<Rightarrow> int) = op "


802 
"(op * :: int \<Rightarrow> int \<Rightarrow> int) = op *"


803 
"(op = :: int \<Rightarrow> int \<Rightarrow> bool) = op ="


804 
"(op \<le> :: int \<Rightarrow> int \<Rightarrow> bool) = op \<le>"


805 
"(op < :: int \<Rightarrow> int \<Rightarrow> bool) = op <"


806 
by rule+


807 


808 
lemma one_int_code [code]:


809 
"1 = Pls 1"


810 
by (simp add: of_num_one)


811 


812 
lemma plus_int_code [code]:


813 
"k + 0 = (k::int)"


814 
"0 + l = (l::int)"


815 
"Pls m + Pls n = Pls (m + n)"


816 
"Pls m  Pls n = sub m n"


817 
"Mns m + Mns n = Mns (m + n)"


818 
"Mns m  Mns n = sub n m"


819 
by (simp_all add: of_num_plus [symmetric])


820 


821 
lemma uminus_int_code [code]:


822 
"uminus 0 = (0::int)"


823 
"uminus (Pls m) = Mns m"


824 
"uminus (Mns m) = Pls m"


825 
by simp_all


826 


827 
lemma minus_int_code [code]:


828 
"k  0 = (k::int)"


829 
"0  l = uminus (l::int)"


830 
"Pls m  Pls n = sub m n"


831 
"Pls m  Mns n = Pls (m + n)"


832 
"Mns m  Pls n = Mns (m + n)"


833 
"Mns m  Mns n = sub n m"


834 
by (simp_all add: of_num_plus [symmetric])


835 


836 
lemma times_int_code [code]:


837 
"k * 0 = (0::int)"


838 
"0 * l = (0::int)"


839 
"Pls m * Pls n = Pls (m * n)"


840 
"Pls m * Mns n = Mns (m * n)"


841 
"Mns m * Pls n = Mns (m * n)"


842 
"Mns m * Mns n = Pls (m * n)"


843 
by (simp_all add: of_num_times [symmetric])


844 


845 
lemma eq_int_code [code]:


846 
"0 = (0::int) \<longleftrightarrow> True"


847 
"0 = Pls l \<longleftrightarrow> False"


848 
"0 = Mns l \<longleftrightarrow> False"


849 
"Pls k = 0 \<longleftrightarrow> False"


850 
"Pls k = Pls l \<longleftrightarrow> k = l"


851 
"Pls k = Mns l \<longleftrightarrow> False"


852 
"Mns k = 0 \<longleftrightarrow> False"


853 
"Mns k = Pls l \<longleftrightarrow> False"


854 
"Mns k = Mns l \<longleftrightarrow> k = l"


855 
using of_num_pos [of l, where ?'a = int] of_num_pos [of k, where ?'a = int]


856 
by (simp_all add: of_num_eq_iff)


857 


858 
lemma less_eq_int_code [code]:


859 
"0 \<le> (0::int) \<longleftrightarrow> True"


860 
"0 \<le> Pls l \<longleftrightarrow> True"


861 
"0 \<le> Mns l \<longleftrightarrow> False"


862 
"Pls k \<le> 0 \<longleftrightarrow> False"


863 
"Pls k \<le> Pls l \<longleftrightarrow> k \<le> l"


864 
"Pls k \<le> Mns l \<longleftrightarrow> False"


865 
"Mns k \<le> 0 \<longleftrightarrow> True"


866 
"Mns k \<le> Pls l \<longleftrightarrow> True"


867 
"Mns k \<le> Mns l \<longleftrightarrow> l \<le> k"


868 
using of_num_pos [of l, where ?'a = int] of_num_pos [of k, where ?'a = int]


869 
by (simp_all add: of_num_less_eq_iff)


870 


871 
lemma less_int_code [code]:


872 
"0 < (0::int) \<longleftrightarrow> False"


873 
"0 < Pls l \<longleftrightarrow> True"


874 
"0 < Mns l \<longleftrightarrow> False"


875 
"Pls k < 0 \<longleftrightarrow> False"


876 
"Pls k < Pls l \<longleftrightarrow> k < l"


877 
"Pls k < Mns l \<longleftrightarrow> False"


878 
"Mns k < 0 \<longleftrightarrow> True"


879 
"Mns k < Pls l \<longleftrightarrow> True"


880 
"Mns k < Mns l \<longleftrightarrow> l < k"


881 
using of_num_pos [of l, where ?'a = int] of_num_pos [of k, where ?'a = int]


882 
by (simp_all add: of_num_less_iff)


883 


884 
lemma [code inline del]: "(0::int) \<equiv> Numeral0" by simp


885 
lemma [code inline del]: "(1::int) \<equiv> Numeral1" by simp


886 
declare zero_is_num_zero [code inline del]


887 
declare one_is_num_one [code inline del]


888 


889 
hide (open) const sub dup


890 


891 


892 
subsection {* Numeral equations as default simplification rules *}


893 


894 
text {* TODO. Be more precise here with respect to subsumed facts. *}


895 
declare (in semiring_numeral) numeral [simp]


896 
declare (in semiring_1) numeral [simp]


897 
declare (in semiring_char_0) numeral [simp]


898 
declare (in ring_1) numeral [simp]


899 
thm numeral


900 


901 


902 
text {* Toy examples *}


903 


904 
definition "bar \<longleftrightarrow> #4 * #2 + #7 = (#8 :: nat) \<and> #4 * #2 + #7 \<ge> (#8 :: int)  #3"


905 
code_thms bar


906 
export_code bar in Haskell file 


907 
export_code bar in OCaml module_name Foo file 


908 
ML {* @{code bar} *}


909 


910 
end
