src/HOL/ex/Numeral.thy
author nipkow
Fri Mar 06 17:38:47 2009 +0100 (2009-03-06)
changeset 30313 b2441b0c8d38
parent 29991 c60ace776315
child 30792 809c38c1a26c
permissions -rw-r--r--
added lemmas
     1 (*  Title:      HOL/ex/Numeral.thy
     2     Author:     Florian Haftmann
     3 *)
     4 
     5 header {* An experimental alternative numeral representation. *}
     6 
     7 theory Numeral
     8 imports Int Inductive
     9 begin
    10 
    11 subsection {* The @{text num} type *}
    12 
    13 datatype num = One | Dig0 num | Dig1 num
    14 
    15 text {* Increment function for type @{typ num} *}
    16 
    17 primrec
    18   inc :: "num \<Rightarrow> num"
    19 where
    20   "inc One = Dig0 One"
    21 | "inc (Dig0 x) = Dig1 x"
    22 | "inc (Dig1 x) = Dig0 (inc x)"
    23 
    24 text {* Converting between type @{typ num} and type @{typ nat} *}
    25 
    26 primrec
    27   nat_of_num :: "num \<Rightarrow> nat"
    28 where
    29   "nat_of_num One = Suc 0"
    30 | "nat_of_num (Dig0 x) = nat_of_num x + nat_of_num x"
    31 | "nat_of_num (Dig1 x) = Suc (nat_of_num x + nat_of_num x)"
    32 
    33 primrec
    34   num_of_nat :: "nat \<Rightarrow> num"
    35 where
    36   "num_of_nat 0 = One"
    37 | "num_of_nat (Suc n) = (if 0 < n then inc (num_of_nat n) else One)"
    38 
    39 lemma nat_of_num_pos: "0 < nat_of_num x"
    40   by (induct x) simp_all
    41 
    42 lemma nat_of_num_neq_0: " nat_of_num x \<noteq> 0"
    43   by (induct x) simp_all
    44 
    45 lemma nat_of_num_inc: "nat_of_num (inc x) = Suc (nat_of_num x)"
    46   by (induct x) simp_all
    47 
    48 lemma num_of_nat_double:
    49   "0 < n \<Longrightarrow> num_of_nat (n + n) = Dig0 (num_of_nat n)"
    50   by (induct n) simp_all
    51 
    52 text {*
    53   Type @{typ num} is isomorphic to the strictly positive
    54   natural numbers.
    55 *}
    56 
    57 lemma nat_of_num_inverse: "num_of_nat (nat_of_num x) = x"
    58   by (induct x) (simp_all add: num_of_nat_double nat_of_num_pos)
    59 
    60 lemma num_of_nat_inverse: "0 < n \<Longrightarrow> nat_of_num (num_of_nat n) = n"
    61   by (induct n) (simp_all add: nat_of_num_inc)
    62 
    63 lemma num_eq_iff: "x = y \<longleftrightarrow> nat_of_num x = nat_of_num y"
    64   apply safe
    65   apply (drule arg_cong [where f=num_of_nat])
    66   apply (simp add: nat_of_num_inverse)
    67   done
    68 
    69 lemma num_induct [case_names One inc]:
    70   fixes P :: "num \<Rightarrow> bool"
    71   assumes One: "P One"
    72     and inc: "\<And>x. P x \<Longrightarrow> P (inc x)"
    73   shows "P x"
    74 proof -
    75   obtain n where n: "Suc n = nat_of_num x"
    76     by (cases "nat_of_num x", simp_all add: nat_of_num_neq_0)
    77   have "P (num_of_nat (Suc n))"
    78   proof (induct n)
    79     case 0 show ?case using One by simp
    80   next
    81     case (Suc n)
    82     then have "P (inc (num_of_nat (Suc n)))" by (rule inc)
    83     then show "P (num_of_nat (Suc (Suc n)))" by simp
    84   qed
    85   with n show "P x"
    86     by (simp add: nat_of_num_inverse)
    87 qed
    88 
    89 text {*
    90   From now on, there are two possible models for @{typ num}:
    91   as positive naturals (rule @{text "num_induct"})
    92   and as digit representation (rules @{text "num.induct"}, @{text "num.cases"}).
    93 
    94   It is not entirely clear in which context it is better to use
    95   the one or the other, or whether the construction should be reversed.
    96 *}
    97 
    98 
    99 subsection {* Numeral operations *}
   100 
   101 ML {*
   102 structure DigSimps =
   103   NamedThmsFun(val name = "numeral"; val description = "Simplification rules for numerals")
   104 *}
   105 
   106 setup DigSimps.setup
   107 
   108 instantiation num :: "{plus,times,ord}"
   109 begin
   110 
   111 definition plus_num :: "num \<Rightarrow> num \<Rightarrow> num" where
   112   [code del]: "m + n = num_of_nat (nat_of_num m + nat_of_num n)"
   113 
   114 definition times_num :: "num \<Rightarrow> num \<Rightarrow> num" where
   115   [code del]: "m * n = num_of_nat (nat_of_num m * nat_of_num n)"
   116 
   117 definition less_eq_num :: "num \<Rightarrow> num \<Rightarrow> bool" where
   118   [code del]: "m \<le> n \<longleftrightarrow> nat_of_num m \<le> nat_of_num n"
   119 
   120 definition less_num :: "num \<Rightarrow> num \<Rightarrow> bool" where
   121   [code del]: "m < n \<longleftrightarrow> nat_of_num m < nat_of_num n"
   122 
   123 instance ..
   124 
   125 end
   126 
   127 lemma nat_of_num_add: "nat_of_num (x + y) = nat_of_num x + nat_of_num y"
   128   unfolding plus_num_def
   129   by (intro num_of_nat_inverse add_pos_pos nat_of_num_pos)
   130 
   131 lemma nat_of_num_mult: "nat_of_num (x * y) = nat_of_num x * nat_of_num y"
   132   unfolding times_num_def
   133   by (intro num_of_nat_inverse mult_pos_pos nat_of_num_pos)
   134 
   135 lemma Dig_plus [numeral, simp, code]:
   136   "One + One = Dig0 One"
   137   "One + Dig0 m = Dig1 m"
   138   "One + Dig1 m = Dig0 (m + One)"
   139   "Dig0 n + One = Dig1 n"
   140   "Dig0 n + Dig0 m = Dig0 (n + m)"
   141   "Dig0 n + Dig1 m = Dig1 (n + m)"
   142   "Dig1 n + One = Dig0 (n + One)"
   143   "Dig1 n + Dig0 m = Dig1 (n + m)"
   144   "Dig1 n + Dig1 m = Dig0 (n + m + One)"
   145   by (simp_all add: num_eq_iff nat_of_num_add)
   146 
   147 lemma Dig_times [numeral, simp, code]:
   148   "One * One = One"
   149   "One * Dig0 n = Dig0 n"
   150   "One * Dig1 n = Dig1 n"
   151   "Dig0 n * One = Dig0 n"
   152   "Dig0 n * Dig0 m = Dig0 (n * Dig0 m)"
   153   "Dig0 n * Dig1 m = Dig0 (n * Dig1 m)"
   154   "Dig1 n * One = Dig1 n"
   155   "Dig1 n * Dig0 m = Dig0 (n * Dig0 m + m)"
   156   "Dig1 n * Dig1 m = Dig1 (n * Dig1 m + m)"
   157   by (simp_all add: num_eq_iff nat_of_num_add nat_of_num_mult
   158                     left_distrib right_distrib)
   159 
   160 lemma Dig_eq:
   161   "One = One \<longleftrightarrow> True"
   162   "One = Dig0 n \<longleftrightarrow> False"
   163   "One = Dig1 n \<longleftrightarrow> False"
   164   "Dig0 m = One \<longleftrightarrow> False"
   165   "Dig1 m = One \<longleftrightarrow> False"
   166   "Dig0 m = Dig0 n \<longleftrightarrow> m = n"
   167   "Dig0 m = Dig1 n \<longleftrightarrow> False"
   168   "Dig1 m = Dig0 n \<longleftrightarrow> False"
   169   "Dig1 m = Dig1 n \<longleftrightarrow> m = n"
   170   by simp_all
   171 
   172 lemma less_eq_num_code [numeral, simp, code]:
   173   "One \<le> n \<longleftrightarrow> True"
   174   "Dig0 m \<le> One \<longleftrightarrow> False"
   175   "Dig1 m \<le> One \<longleftrightarrow> False"
   176   "Dig0 m \<le> Dig0 n \<longleftrightarrow> m \<le> n"
   177   "Dig0 m \<le> Dig1 n \<longleftrightarrow> m \<le> n"
   178   "Dig1 m \<le> Dig1 n \<longleftrightarrow> m \<le> n"
   179   "Dig1 m \<le> Dig0 n \<longleftrightarrow> m < n"
   180   using nat_of_num_pos [of n] nat_of_num_pos [of m]
   181   by (auto simp add: less_eq_num_def less_num_def)
   182 
   183 lemma less_num_code [numeral, simp, code]:
   184   "m < One \<longleftrightarrow> False"
   185   "One < One \<longleftrightarrow> False"
   186   "One < Dig0 n \<longleftrightarrow> True"
   187   "One < Dig1 n \<longleftrightarrow> True"
   188   "Dig0 m < Dig0 n \<longleftrightarrow> m < n"
   189   "Dig0 m < Dig1 n \<longleftrightarrow> m \<le> n"
   190   "Dig1 m < Dig1 n \<longleftrightarrow> m < n"
   191   "Dig1 m < Dig0 n \<longleftrightarrow> m < n"
   192   using nat_of_num_pos [of n] nat_of_num_pos [of m]
   193   by (auto simp add: less_eq_num_def less_num_def)
   194 
   195 text {* Rules using @{text One} and @{text inc} as constructors *}
   196 
   197 lemma add_One: "x + One = inc x"
   198   by (simp add: num_eq_iff nat_of_num_add nat_of_num_inc)
   199 
   200 lemma add_inc: "x + inc y = inc (x + y)"
   201   by (simp add: num_eq_iff nat_of_num_add nat_of_num_inc)
   202 
   203 lemma mult_One: "x * One = x"
   204   by (simp add: num_eq_iff nat_of_num_mult)
   205 
   206 lemma mult_inc: "x * inc y = x * y + x"
   207   by (simp add: num_eq_iff nat_of_num_mult nat_of_num_add nat_of_num_inc)
   208 
   209 text {* A double-and-decrement function *}
   210 
   211 primrec DigM :: "num \<Rightarrow> num" where
   212   "DigM One = One"
   213   | "DigM (Dig0 n) = Dig1 (DigM n)"
   214   | "DigM (Dig1 n) = Dig1 (Dig0 n)"
   215 
   216 lemma DigM_plus_one: "DigM n + One = Dig0 n"
   217   by (induct n) simp_all
   218 
   219 lemma add_One_commute: "One + n = n + One"
   220   by (induct n) simp_all
   221 
   222 lemma one_plus_DigM: "One + DigM n = Dig0 n"
   223   unfolding add_One_commute DigM_plus_one ..
   224 
   225 text {* Squaring and exponentiation *}
   226 
   227 primrec square :: "num \<Rightarrow> num" where
   228   "square One = One"
   229 | "square (Dig0 n) = Dig0 (Dig0 (square n))"
   230 | "square (Dig1 n) = Dig1 (Dig0 (square n + n))"
   231 
   232 primrec pow :: "num \<Rightarrow> num \<Rightarrow> num"
   233 where
   234   "pow x One = x"
   235 | "pow x (Dig0 y) = square (pow x y)"
   236 | "pow x (Dig1 y) = x * square (pow x y)"
   237 
   238 
   239 subsection {* Binary numerals *}
   240 
   241 text {*
   242   We embed binary representations into a generic algebraic
   243   structure using @{text of_num}.
   244 *}
   245 
   246 class semiring_numeral = semiring + monoid_mult
   247 begin
   248 
   249 primrec of_num :: "num \<Rightarrow> 'a" where
   250   of_num_one [numeral]: "of_num One = 1"
   251   | "of_num (Dig0 n) = of_num n + of_num n"
   252   | "of_num (Dig1 n) = of_num n + of_num n + 1"
   253 
   254 lemma of_num_inc: "of_num (inc x) = of_num x + 1"
   255   by (induct x) (simp_all add: add_ac)
   256 
   257 declare of_num.simps [simp del]
   258 
   259 end
   260 
   261 text {*
   262   ML stuff and syntax.
   263 *}
   264 
   265 ML {*
   266 fun mk_num 1 = @{term One}
   267   | mk_num k =
   268       let
   269         val (l, b) = Integer.div_mod k 2;
   270         val bit = (if b = 0 then @{term Dig0} else @{term Dig1});
   271       in bit $ (mk_num l) end;
   272 
   273 fun dest_num @{term One} = 1
   274   | dest_num (@{term Dig0} $ n) = 2 * dest_num n
   275   | dest_num (@{term Dig1} $ n) = 2 * dest_num n + 1;
   276 
   277 (*FIXME these have to gain proper context via morphisms phi*)
   278 
   279 fun mk_numeral T k = Const (@{const_name of_num}, @{typ num} --> T)
   280   $ mk_num k
   281 
   282 fun dest_numeral (Const (@{const_name of_num}, Type ("fun", [@{typ num}, T])) $ t) =
   283   (T, dest_num t)
   284 *}
   285 
   286 syntax
   287   "_Numerals" :: "xnum \<Rightarrow> 'a"    ("_")
   288 
   289 parse_translation {*
   290 let
   291   fun num_of_int n = if n > 0 then case IntInf.quotRem (n, 2)
   292      of (0, 1) => Const (@{const_name One}, dummyT)
   293       | (n, 0) => Const (@{const_name Dig0}, dummyT) $ num_of_int n
   294       | (n, 1) => Const (@{const_name Dig1}, dummyT) $ num_of_int n
   295     else raise Match;
   296   fun numeral_tr [Free (num, _)] =
   297         let
   298           val {leading_zeros, value, ...} = Syntax.read_xnum num;
   299           val _ = leading_zeros = 0 andalso value > 0
   300             orelse error ("Bad numeral: " ^ num);
   301         in Const (@{const_name of_num}, @{typ num} --> dummyT) $ num_of_int value end
   302     | numeral_tr ts = raise TERM ("numeral_tr", ts);
   303 in [("_Numerals", numeral_tr)] end
   304 *}
   305 
   306 typed_print_translation {*
   307 let
   308   fun dig b n = b + 2 * n; 
   309   fun int_of_num' (Const (@{const_syntax Dig0}, _) $ n) =
   310         dig 0 (int_of_num' n)
   311     | int_of_num' (Const (@{const_syntax Dig1}, _) $ n) =
   312         dig 1 (int_of_num' n)
   313     | int_of_num' (Const (@{const_syntax One}, _)) = 1;
   314   fun num_tr' show_sorts T [n] =
   315     let
   316       val k = int_of_num' n;
   317       val t' = Syntax.const "_Numerals" $ Syntax.free ("#" ^ string_of_int k);
   318     in case T
   319      of Type ("fun", [_, T']) =>
   320          if not (! show_types) andalso can Term.dest_Type T' then t'
   321          else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T'
   322       | T' => if T' = dummyT then t' else raise Match
   323     end;
   324 in [(@{const_syntax of_num}, num_tr')] end
   325 *}
   326 
   327 subsection {* Class-specific numeral rules *}
   328 
   329 text {*
   330   @{const of_num} is a morphism.
   331 *}
   332 
   333 subsubsection {* Class @{text semiring_numeral} *}
   334 
   335 context semiring_numeral
   336 begin
   337 
   338 abbreviation "Num1 \<equiv> of_num One"
   339 
   340 text {*
   341   Alas, there is still the duplication of @{term 1},
   342   thought the duplicated @{term 0} has disappeared.
   343   We could get rid of it by replacing the constructor
   344   @{term 1} in @{typ num} by two constructors
   345   @{text two} and @{text three}, resulting in a further
   346   blow-up.  But it could be worth the effort.
   347 *}
   348 
   349 lemma of_num_plus_one [numeral]:
   350   "of_num n + 1 = of_num (n + One)"
   351   by (rule sym, induct n) (simp_all add: of_num.simps add_ac)
   352 
   353 lemma of_num_one_plus [numeral]:
   354   "1 + of_num n = of_num (n + One)"
   355   unfolding of_num_plus_one [symmetric] add_commute ..
   356 
   357 lemma of_num_plus [numeral]:
   358   "of_num m + of_num n = of_num (m + n)"
   359   by (induct n rule: num_induct)
   360      (simp_all add: add_One add_inc of_num_one of_num_inc add_ac)
   361 
   362 lemma of_num_times_one [numeral]:
   363   "of_num n * 1 = of_num n"
   364   by simp
   365 
   366 lemma of_num_one_times [numeral]:
   367   "1 * of_num n = of_num n"
   368   by simp
   369 
   370 lemma of_num_times [numeral]:
   371   "of_num m * of_num n = of_num (m * n)"
   372   by (induct n rule: num_induct)
   373     (simp_all add: of_num_plus [symmetric] mult_One mult_inc
   374     semiring_class.right_distrib right_distrib of_num_one of_num_inc)
   375 
   376 end
   377 
   378 subsubsection {*
   379   Structures with a zero: class @{text semiring_1}
   380 *}
   381 
   382 context semiring_1
   383 begin
   384 
   385 subclass semiring_numeral ..
   386 
   387 lemma of_nat_of_num [numeral]: "of_nat (of_num n) = of_num n"
   388   by (induct n)
   389     (simp_all add: semiring_numeral_class.of_num.simps of_num.simps add_ac)
   390 
   391 declare of_nat_1 [numeral]
   392 
   393 lemma Dig_plus_zero [numeral]:
   394   "0 + 1 = 1"
   395   "0 + of_num n = of_num n"
   396   "1 + 0 = 1"
   397   "of_num n + 0 = of_num n"
   398   by simp_all
   399 
   400 lemma Dig_times_zero [numeral]:
   401   "0 * 1 = 0"
   402   "0 * of_num n = 0"
   403   "1 * 0 = 0"
   404   "of_num n * 0 = 0"
   405   by simp_all
   406 
   407 end
   408 
   409 lemma nat_of_num_of_num: "nat_of_num = of_num"
   410 proof
   411   fix n
   412   have "of_num n = nat_of_num n"
   413     by (induct n) (simp_all add: of_num.simps)
   414   then show "nat_of_num n = of_num n" by simp
   415 qed
   416 
   417 subsubsection {*
   418   Equality: class @{text semiring_char_0}
   419 *}
   420 
   421 context semiring_char_0
   422 begin
   423 
   424 lemma of_num_eq_iff [numeral]:
   425   "of_num m = of_num n \<longleftrightarrow> m = n"
   426   unfolding of_nat_of_num [symmetric] nat_of_num_of_num [symmetric]
   427     of_nat_eq_iff num_eq_iff ..
   428 
   429 lemma of_num_eq_one_iff [numeral]:
   430   "of_num n = 1 \<longleftrightarrow> n = One"
   431 proof -
   432   have "of_num n = of_num One \<longleftrightarrow> n = One" unfolding of_num_eq_iff ..
   433   then show ?thesis by (simp add: of_num_one)
   434 qed
   435 
   436 lemma one_eq_of_num_iff [numeral]:
   437   "1 = of_num n \<longleftrightarrow> n = One"
   438   unfolding of_num_eq_one_iff [symmetric] by auto
   439 
   440 end
   441 
   442 subsubsection {*
   443   Comparisons: class @{text ordered_semidom}
   444 *}
   445 
   446 text {*  Could be perhaps more general than here. *}
   447 
   448 context ordered_semidom
   449 begin
   450 
   451 lemma of_num_pos [numeral]: "0 < of_num n"
   452   by (induct n) (simp_all add: of_num.simps add_pos_pos)
   453 
   454 lemma of_num_less_eq_iff [numeral]: "of_num m \<le> of_num n \<longleftrightarrow> m \<le> n"
   455 proof -
   456   have "of_nat (of_num m) \<le> of_nat (of_num n) \<longleftrightarrow> m \<le> n"
   457     unfolding less_eq_num_def nat_of_num_of_num of_nat_le_iff ..
   458   then show ?thesis by (simp add: of_nat_of_num)
   459 qed
   460 
   461 lemma of_num_less_eq_one_iff [numeral]: "of_num n \<le> 1 \<longleftrightarrow> n = One"
   462 proof -
   463   have "of_num n \<le> of_num One \<longleftrightarrow> n = One"
   464     by (cases n) (simp_all add: of_num_less_eq_iff)
   465   then show ?thesis by (simp add: of_num_one)
   466 qed
   467 
   468 lemma one_less_eq_of_num_iff [numeral]: "1 \<le> of_num n"
   469 proof -
   470   have "of_num One \<le> of_num n"
   471     by (cases n) (simp_all add: of_num_less_eq_iff)
   472   then show ?thesis by (simp add: of_num_one)
   473 qed
   474 
   475 lemma of_num_less_iff [numeral]: "of_num m < of_num n \<longleftrightarrow> m < n"
   476 proof -
   477   have "of_nat (of_num m) < of_nat (of_num n) \<longleftrightarrow> m < n"
   478     unfolding less_num_def nat_of_num_of_num of_nat_less_iff ..
   479   then show ?thesis by (simp add: of_nat_of_num)
   480 qed
   481 
   482 lemma of_num_less_one_iff [numeral]: "\<not> of_num n < 1"
   483 proof -
   484   have "\<not> of_num n < of_num One"
   485     by (cases n) (simp_all add: of_num_less_iff)
   486   then show ?thesis by (simp add: of_num_one)
   487 qed
   488 
   489 lemma one_less_of_num_iff [numeral]: "1 < of_num n \<longleftrightarrow> n \<noteq> One"
   490 proof -
   491   have "of_num One < of_num n \<longleftrightarrow> n \<noteq> One"
   492     by (cases n) (simp_all add: of_num_less_iff)
   493   then show ?thesis by (simp add: of_num_one)
   494 qed
   495 
   496 lemma of_num_nonneg [numeral]: "0 \<le> of_num n"
   497   by (induct n) (simp_all add: of_num.simps add_nonneg_nonneg)
   498 
   499 lemma of_num_less_zero_iff [numeral]: "\<not> of_num n < 0"
   500   by (simp add: not_less of_num_nonneg)
   501 
   502 lemma of_num_le_zero_iff [numeral]: "\<not> of_num n \<le> 0"
   503   by (simp add: not_le of_num_pos)
   504 
   505 end
   506 
   507 context ordered_idom
   508 begin
   509 
   510 lemma minus_of_num_less_of_num_iff [numeral]: "- of_num m < of_num n"
   511 proof -
   512   have "- of_num m < 0" by (simp add: of_num_pos)
   513   also have "0 < of_num n" by (simp add: of_num_pos)
   514   finally show ?thesis .
   515 qed
   516 
   517 lemma minus_of_num_less_one_iff [numeral]: "- of_num n < 1"
   518 proof -
   519   have "- of_num n < 0" by (simp add: of_num_pos)
   520   also have "0 < 1" by simp
   521   finally show ?thesis .
   522 qed
   523 
   524 lemma minus_one_less_of_num_iff [numeral]: "- 1 < of_num n"
   525 proof -
   526   have "- 1 < 0" by simp
   527   also have "0 < of_num n" by (simp add: of_num_pos)
   528   finally show ?thesis .
   529 qed
   530 
   531 lemma minus_of_num_le_of_num_iff [numeral]: "- of_num m \<le> of_num n"
   532   by (simp add: less_imp_le minus_of_num_less_of_num_iff)
   533 
   534 lemma minus_of_num_le_one_iff [numeral]: "- of_num n \<le> 1"
   535   by (simp add: less_imp_le minus_of_num_less_one_iff)
   536 
   537 lemma minus_one_le_of_num_iff [numeral]: "- 1 \<le> of_num n"
   538   by (simp add: less_imp_le minus_one_less_of_num_iff)
   539 
   540 lemma of_num_le_minus_of_num_iff [numeral]: "\<not> of_num m \<le> - of_num n"
   541   by (simp add: not_le minus_of_num_less_of_num_iff)
   542 
   543 lemma one_le_minus_of_num_iff [numeral]: "\<not> 1 \<le> - of_num n"
   544   by (simp add: not_le minus_of_num_less_one_iff)
   545 
   546 lemma of_num_le_minus_one_iff [numeral]: "\<not> of_num n \<le> - 1"
   547   by (simp add: not_le minus_one_less_of_num_iff)
   548 
   549 lemma of_num_less_minus_of_num_iff [numeral]: "\<not> of_num m < - of_num n"
   550   by (simp add: not_less minus_of_num_le_of_num_iff)
   551 
   552 lemma one_less_minus_of_num_iff [numeral]: "\<not> 1 < - of_num n"
   553   by (simp add: not_less minus_of_num_le_one_iff)
   554 
   555 lemma of_num_less_minus_one_iff [numeral]: "\<not> of_num n < - 1"
   556   by (simp add: not_less minus_one_le_of_num_iff)
   557 
   558 end
   559 
   560 subsubsection {*
   561   Structures with subtraction: class @{text semiring_1_minus}
   562 *}
   563 
   564 class semiring_minus = semiring + minus + zero +
   565   assumes minus_inverts_plus1: "a + b = c \<Longrightarrow> c - b = a"
   566   assumes minus_minus_zero_inverts_plus1: "a + b = c \<Longrightarrow> b - c = 0 - a"
   567 begin
   568 
   569 lemma minus_inverts_plus2: "a + b = c \<Longrightarrow> c - a = b"
   570   by (simp add: add_ac minus_inverts_plus1 [of b a])
   571 
   572 lemma minus_minus_zero_inverts_plus2: "a + b = c \<Longrightarrow> a - c = 0 - b"
   573   by (simp add: add_ac minus_minus_zero_inverts_plus1 [of b a])
   574 
   575 end
   576 
   577 class semiring_1_minus = semiring_1 + semiring_minus
   578 begin
   579 
   580 lemma Dig_of_num_pos:
   581   assumes "k + n = m"
   582   shows "of_num m - of_num n = of_num k"
   583   using assms by (simp add: of_num_plus minus_inverts_plus1)
   584 
   585 lemma Dig_of_num_zero:
   586   shows "of_num n - of_num n = 0"
   587   by (rule minus_inverts_plus1) simp
   588 
   589 lemma Dig_of_num_neg:
   590   assumes "k + m = n"
   591   shows "of_num m - of_num n = 0 - of_num k"
   592   by (rule minus_minus_zero_inverts_plus1) (simp add: of_num_plus assms)
   593 
   594 lemmas Dig_plus_eval =
   595   of_num_plus of_num_eq_iff Dig_plus refl [of One, THEN eqTrueI] num.inject
   596 
   597 simproc_setup numeral_minus ("of_num m - of_num n") = {*
   598   let
   599     (*TODO proper implicit use of morphism via pattern antiquotations*)
   600     fun cdest_of_num ct = (snd o split_last o snd o Drule.strip_comb) ct;
   601     fun cdest_minus ct = case (rev o snd o Drule.strip_comb) ct of [n, m] => (m, n);
   602     fun attach_num ct = (dest_num (Thm.term_of ct), ct);
   603     fun cdifference t = (pairself (attach_num o cdest_of_num) o cdest_minus) t;
   604     val simplify = MetaSimplifier.rewrite false (map mk_meta_eq @{thms Dig_plus_eval});
   605     fun cert ck cl cj = @{thm eqTrueE} OF [@{thm meta_eq_to_obj_eq} OF [simplify (Drule.list_comb (@{cterm "op = :: num \<Rightarrow> _"},
   606       [Drule.list_comb (@{cterm "op + :: num \<Rightarrow> _"}, [ck, cl]), cj]))]];
   607   in fn phi => fn _ => fn ct => case try cdifference ct
   608    of NONE => (NONE)
   609     | SOME ((k, ck), (l, cl)) => SOME (let val j = k - l in if j = 0
   610         then MetaSimplifier.rewrite false [mk_meta_eq (Morphism.thm phi @{thm Dig_of_num_zero})] ct
   611         else mk_meta_eq (let
   612           val cj = Thm.cterm_of (Thm.theory_of_cterm ct) (mk_num (abs j));
   613         in
   614           (if j > 0 then (Morphism.thm phi @{thm Dig_of_num_pos}) OF [cert cj cl ck]
   615           else (Morphism.thm phi @{thm Dig_of_num_neg}) OF [cert cj ck cl])
   616         end) end)
   617   end
   618 *}
   619 
   620 lemma Dig_of_num_minus_zero [numeral]:
   621   "of_num n - 0 = of_num n"
   622   by (simp add: minus_inverts_plus1)
   623 
   624 lemma Dig_one_minus_zero [numeral]:
   625   "1 - 0 = 1"
   626   by (simp add: minus_inverts_plus1)
   627 
   628 lemma Dig_one_minus_one [numeral]:
   629   "1 - 1 = 0"
   630   by (simp add: minus_inverts_plus1)
   631 
   632 lemma Dig_of_num_minus_one [numeral]:
   633   "of_num (Dig0 n) - 1 = of_num (DigM n)"
   634   "of_num (Dig1 n) - 1 = of_num (Dig0 n)"
   635   by (auto intro: minus_inverts_plus1 simp add: DigM_plus_one of_num.simps of_num_plus_one)
   636 
   637 lemma Dig_one_minus_of_num [numeral]:
   638   "1 - of_num (Dig0 n) = 0 - of_num (DigM n)"
   639   "1 - of_num (Dig1 n) = 0 - of_num (Dig0 n)"
   640   by (auto intro: minus_minus_zero_inverts_plus1 simp add: DigM_plus_one of_num.simps of_num_plus_one)
   641 
   642 end
   643 
   644 subsubsection {*
   645   Structures with negation: class @{text ring_1}
   646 *}
   647 
   648 context ring_1
   649 begin
   650 
   651 subclass semiring_1_minus
   652   proof qed (simp_all add: algebra_simps)
   653 
   654 lemma Dig_zero_minus_of_num [numeral]:
   655   "0 - of_num n = - of_num n"
   656   by simp
   657 
   658 lemma Dig_zero_minus_one [numeral]:
   659   "0 - 1 = - 1"
   660   by simp
   661 
   662 lemma Dig_uminus_uminus [numeral]:
   663   "- (- of_num n) = of_num n"
   664   by simp
   665 
   666 lemma Dig_plus_uminus [numeral]:
   667   "of_num m + - of_num n = of_num m - of_num n"
   668   "- of_num m + of_num n = of_num n - of_num m"
   669   "- of_num m + - of_num n = - (of_num m + of_num n)"
   670   "of_num m - - of_num n = of_num m + of_num n"
   671   "- of_num m - of_num n = - (of_num m + of_num n)"
   672   "- of_num m - - of_num n = of_num n - of_num m"
   673   by (simp_all add: diff_minus add_commute)
   674 
   675 lemma Dig_times_uminus [numeral]:
   676   "- of_num n * of_num m = - (of_num n * of_num m)"
   677   "of_num n * - of_num m = - (of_num n * of_num m)"
   678   "- of_num n * - of_num m = of_num n * of_num m"
   679   by (simp_all add: minus_mult_left [symmetric] minus_mult_right [symmetric])
   680 
   681 lemma of_int_of_num [numeral]: "of_int (of_num n) = of_num n"
   682 by (induct n)
   683   (simp_all only: of_num.simps semiring_numeral_class.of_num.simps of_int_add, simp_all)
   684 
   685 declare of_int_1 [numeral]
   686 
   687 end
   688 
   689 subsubsection {*
   690   Structures with exponentiation
   691 *}
   692 
   693 lemma of_num_square: "of_num (square x) = of_num x * of_num x"
   694 by (induct x)
   695    (simp_all add: of_num.simps of_num_plus [symmetric] algebra_simps)
   696 
   697 lemma of_num_pow:
   698   "(of_num (pow x y)::'a::{semiring_numeral,recpower}) = of_num x ^ of_num y"
   699 by (induct y)
   700    (simp_all add: of_num.simps of_num_square of_num_times [symmetric]
   701                   power_Suc power_add)
   702 
   703 lemma power_of_num [numeral]:
   704   "of_num x ^ of_num y = (of_num (pow x y)::'a::{semiring_numeral,recpower})"
   705   by (rule of_num_pow [symmetric])
   706 
   707 lemma power_zero_of_num [numeral]:
   708   "0 ^ of_num n = (0::'a::{semiring_0,recpower})"
   709   using of_num_pos [where n=n and ?'a=nat]
   710   by (simp add: power_0_left)
   711 
   712 lemma power_minus_one_double:
   713   "(- 1) ^ (n + n) = (1::'a::{ring_1,recpower})"
   714   by (induct n) (simp_all add: power_Suc)
   715 
   716 lemma power_minus_Dig0 [numeral]:
   717   fixes x :: "'a::{ring_1,recpower}"
   718   shows "(- x) ^ of_num (Dig0 n) = x ^ of_num (Dig0 n)"
   719   by (subst power_minus)
   720      (simp add: of_num.simps power_minus_one_double)
   721 
   722 lemma power_minus_Dig1 [numeral]:
   723   fixes x :: "'a::{ring_1,recpower}"
   724   shows "(- x) ^ of_num (Dig1 n) = - (x ^ of_num (Dig1 n))"
   725   by (subst power_minus)
   726      (simp add: of_num.simps power_Suc power_minus_one_double)
   727 
   728 declare power_one [numeral]
   729 
   730 
   731 subsubsection {*
   732   Greetings to @{typ nat}.
   733 *}
   734 
   735 instance nat :: semiring_1_minus proof qed simp_all
   736 
   737 lemma Suc_of_num [numeral]: "Suc (of_num n) = of_num (n + One)"
   738   unfolding of_num_plus_one [symmetric] by simp
   739 
   740 lemma nat_number:
   741   "1 = Suc 0"
   742   "of_num One = Suc 0"
   743   "of_num (Dig0 n) = Suc (of_num (DigM n))"
   744   "of_num (Dig1 n) = Suc (of_num (Dig0 n))"
   745   by (simp_all add: of_num.simps DigM_plus_one Suc_of_num)
   746 
   747 declare diff_0_eq_0 [numeral]
   748 
   749 
   750 subsection {* Code generator setup for @{typ int} *}
   751 
   752 definition Pls :: "num \<Rightarrow> int" where
   753   [simp, code post]: "Pls n = of_num n"
   754 
   755 definition Mns :: "num \<Rightarrow> int" where
   756   [simp, code post]: "Mns n = - of_num n"
   757 
   758 code_datatype "0::int" Pls Mns
   759 
   760 lemmas [code inline] = Pls_def [symmetric] Mns_def [symmetric]
   761 
   762 definition sub :: "num \<Rightarrow> num \<Rightarrow> int" where
   763   [simp, code del]: "sub m n = (of_num m - of_num n)"
   764 
   765 definition dup :: "int \<Rightarrow> int" where
   766   [code del]: "dup k = 2 * k"
   767 
   768 lemma Dig_sub [code]:
   769   "sub One One = 0"
   770   "sub (Dig0 m) One = of_num (DigM m)"
   771   "sub (Dig1 m) One = of_num (Dig0 m)"
   772   "sub One (Dig0 n) = - of_num (DigM n)"
   773   "sub One (Dig1 n) = - of_num (Dig0 n)"
   774   "sub (Dig0 m) (Dig0 n) = dup (sub m n)"
   775   "sub (Dig1 m) (Dig1 n) = dup (sub m n)"
   776   "sub (Dig1 m) (Dig0 n) = dup (sub m n) + 1"
   777   "sub (Dig0 m) (Dig1 n) = dup (sub m n) - 1"
   778   apply (simp_all add: dup_def algebra_simps)
   779   apply (simp_all add: of_num_plus one_plus_DigM)[4]
   780   apply (simp_all add: of_num.simps)
   781   done
   782 
   783 lemma dup_code [code]:
   784   "dup 0 = 0"
   785   "dup (Pls n) = Pls (Dig0 n)"
   786   "dup (Mns n) = Mns (Dig0 n)"
   787   by (simp_all add: dup_def of_num.simps)
   788   
   789 lemma [code, code del]:
   790   "(1 :: int) = 1"
   791   "(op + :: int \<Rightarrow> int \<Rightarrow> int) = op +"
   792   "(uminus :: int \<Rightarrow> int) = uminus"
   793   "(op - :: int \<Rightarrow> int \<Rightarrow> int) = op -"
   794   "(op * :: int \<Rightarrow> int \<Rightarrow> int) = op *"
   795   "(eq_class.eq :: int \<Rightarrow> int \<Rightarrow> bool) = eq_class.eq"
   796   "(op \<le> :: int \<Rightarrow> int \<Rightarrow> bool) = op \<le>"
   797   "(op < :: int \<Rightarrow> int \<Rightarrow> bool) = op <"
   798   by rule+
   799 
   800 lemma one_int_code [code]:
   801   "1 = Pls One"
   802   by (simp add: of_num_one)
   803 
   804 lemma plus_int_code [code]:
   805   "k + 0 = (k::int)"
   806   "0 + l = (l::int)"
   807   "Pls m + Pls n = Pls (m + n)"
   808   "Pls m - Pls n = sub m n"
   809   "Mns m + Mns n = Mns (m + n)"
   810   "Mns m - Mns n = sub n m"
   811   by (simp_all add: of_num_plus [symmetric])
   812 
   813 lemma uminus_int_code [code]:
   814   "uminus 0 = (0::int)"
   815   "uminus (Pls m) = Mns m"
   816   "uminus (Mns m) = Pls m"
   817   by simp_all
   818 
   819 lemma minus_int_code [code]:
   820   "k - 0 = (k::int)"
   821   "0 - l = uminus (l::int)"
   822   "Pls m - Pls n = sub m n"
   823   "Pls m - Mns n = Pls (m + n)"
   824   "Mns m - Pls n = Mns (m + n)"
   825   "Mns m - Mns n = sub n m"
   826   by (simp_all add: of_num_plus [symmetric])
   827 
   828 lemma times_int_code [code]:
   829   "k * 0 = (0::int)"
   830   "0 * l = (0::int)"
   831   "Pls m * Pls n = Pls (m * n)"
   832   "Pls m * Mns n = Mns (m * n)"
   833   "Mns m * Pls n = Mns (m * n)"
   834   "Mns m * Mns n = Pls (m * n)"
   835   by (simp_all add: of_num_times [symmetric])
   836 
   837 lemma eq_int_code [code]:
   838   "eq_class.eq 0 (0::int) \<longleftrightarrow> True"
   839   "eq_class.eq 0 (Pls l) \<longleftrightarrow> False"
   840   "eq_class.eq 0 (Mns l) \<longleftrightarrow> False"
   841   "eq_class.eq (Pls k) 0 \<longleftrightarrow> False"
   842   "eq_class.eq (Pls k) (Pls l) \<longleftrightarrow> eq_class.eq k l"
   843   "eq_class.eq (Pls k) (Mns l) \<longleftrightarrow> False"
   844   "eq_class.eq (Mns k) 0 \<longleftrightarrow> False"
   845   "eq_class.eq (Mns k) (Pls l) \<longleftrightarrow> False"
   846   "eq_class.eq (Mns k) (Mns l) \<longleftrightarrow> eq_class.eq k l"
   847   using of_num_pos [of l, where ?'a = int] of_num_pos [of k, where ?'a = int]
   848   by (simp_all add: of_num_eq_iff eq)
   849 
   850 lemma less_eq_int_code [code]:
   851   "0 \<le> (0::int) \<longleftrightarrow> True"
   852   "0 \<le> Pls l \<longleftrightarrow> True"
   853   "0 \<le> Mns l \<longleftrightarrow> False"
   854   "Pls k \<le> 0 \<longleftrightarrow> False"
   855   "Pls k \<le> Pls l \<longleftrightarrow> k \<le> l"
   856   "Pls k \<le> Mns l \<longleftrightarrow> False"
   857   "Mns k \<le> 0 \<longleftrightarrow> True"
   858   "Mns k \<le> Pls l \<longleftrightarrow> True"
   859   "Mns k \<le> Mns l \<longleftrightarrow> l \<le> k"
   860   using of_num_pos [of l, where ?'a = int] of_num_pos [of k, where ?'a = int]
   861   by (simp_all add: of_num_less_eq_iff)
   862 
   863 lemma less_int_code [code]:
   864   "0 < (0::int) \<longleftrightarrow> False"
   865   "0 < Pls l \<longleftrightarrow> True"
   866   "0 < Mns l \<longleftrightarrow> False"
   867   "Pls k < 0 \<longleftrightarrow> False"
   868   "Pls k < Pls l \<longleftrightarrow> k < l"
   869   "Pls k < Mns l \<longleftrightarrow> False"
   870   "Mns k < 0 \<longleftrightarrow> True"
   871   "Mns k < Pls l \<longleftrightarrow> True"
   872   "Mns k < Mns l \<longleftrightarrow> l < k"
   873   using of_num_pos [of l, where ?'a = int] of_num_pos [of k, where ?'a = int]
   874   by (simp_all add: of_num_less_iff)
   875 
   876 lemma [code inline del]: "(0::int) \<equiv> Numeral0" by simp
   877 lemma [code inline del]: "(1::int) \<equiv> Numeral1" by simp
   878 declare zero_is_num_zero [code inline del]
   879 declare one_is_num_one [code inline del]
   880 
   881 hide (open) const sub dup
   882 
   883 
   884 subsection {* Numeral equations as default simplification rules *}
   885 
   886 text {* TODO.  Be more precise here with respect to subsumed facts.  Or use named theorems anyway. *}
   887 declare (in semiring_numeral) numeral [simp]
   888 declare (in semiring_1) numeral [simp]
   889 declare (in semiring_char_0) numeral [simp]
   890 declare (in ring_1) numeral [simp]
   891 thm numeral
   892 
   893 
   894 text {* Toy examples *}
   895 
   896 definition "bar \<longleftrightarrow> #4 * #2 + #7 = (#8 :: nat) \<and> #4 * #2 + #7 \<ge> (#8 :: int) - #3"
   897 code_thms bar
   898 export_code bar in Haskell file -
   899 export_code bar in OCaml module_name Foo file -
   900 ML {* @{code bar} *}
   901 
   902 end