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