src/HOL/Library/Numeral_Type.thy
 author haftmann Fri Oct 30 14:00:43 2009 +0100 (2009-10-30) changeset 33361 1f18de40b43f parent 33035 15eab423e573 child 35115 446c5063e4fd permissions -rw-r--r--
combined former theories Divides and IntDiv to one theory Divides
```     1 (*  Title:      HOL/Library/Numeral_Type.thy
```
```     2     Author:     Brian Huffman
```
```     3 *)
```
```     4
```
```     5 header {* Numeral Syntax for Types *}
```
```     6
```
```     7 theory Numeral_Type
```
```     8 imports Main
```
```     9 begin
```
```    10
```
```    11 subsection {* Preliminary lemmas *}
```
```    12 (* These should be moved elsewhere *)
```
```    13
```
```    14 lemma (in type_definition) univ:
```
```    15   "UNIV = Abs ` A"
```
```    16 proof
```
```    17   show "Abs ` A \<subseteq> UNIV" by (rule subset_UNIV)
```
```    18   show "UNIV \<subseteq> Abs ` A"
```
```    19   proof
```
```    20     fix x :: 'b
```
```    21     have "x = Abs (Rep x)" by (rule Rep_inverse [symmetric])
```
```    22     moreover have "Rep x \<in> A" by (rule Rep)
```
```    23     ultimately show "x \<in> Abs ` A" by (rule image_eqI)
```
```    24   qed
```
```    25 qed
```
```    26
```
```    27 lemma (in type_definition) card: "card (UNIV :: 'b set) = card A"
```
```    28   by (simp add: univ card_image inj_on_def Abs_inject)
```
```    29
```
```    30
```
```    31 subsection {* Cardinalities of types *}
```
```    32
```
```    33 syntax "_type_card" :: "type => nat" ("(1CARD/(1'(_')))")
```
```    34
```
```    35 translations "CARD(t)" => "CONST card (CONST UNIV \<Colon> t set)"
```
```    36
```
```    37 typed_print_translation {*
```
```    38 let
```
```    39   fun card_univ_tr' show_sorts _ [Const (@{const_syntax UNIV}, Type(_,[T,_]))] =
```
```    40     Syntax.const "_type_card" \$ Syntax.term_of_typ show_sorts T;
```
```    41 in [(@{const_syntax card}, card_univ_tr')]
```
```    42 end
```
```    43 *}
```
```    44
```
```    45 lemma card_unit [simp]: "CARD(unit) = 1"
```
```    46   unfolding UNIV_unit by simp
```
```    47
```
```    48 lemma card_bool [simp]: "CARD(bool) = 2"
```
```    49   unfolding UNIV_bool by simp
```
```    50
```
```    51 lemma card_prod [simp]: "CARD('a \<times> 'b) = CARD('a::finite) * CARD('b::finite)"
```
```    52   unfolding UNIV_Times_UNIV [symmetric] by (simp only: card_cartesian_product)
```
```    53
```
```    54 lemma card_sum [simp]: "CARD('a + 'b) = CARD('a::finite) + CARD('b::finite)"
```
```    55   unfolding UNIV_Plus_UNIV [symmetric] by (simp only: finite card_Plus)
```
```    56
```
```    57 lemma card_option [simp]: "CARD('a option) = Suc CARD('a::finite)"
```
```    58   unfolding UNIV_option_conv
```
```    59   apply (subgoal_tac "(None::'a option) \<notin> range Some")
```
```    60   apply (simp add: card_image)
```
```    61   apply fast
```
```    62   done
```
```    63
```
```    64 lemma card_set [simp]: "CARD('a set) = 2 ^ CARD('a::finite)"
```
```    65   unfolding Pow_UNIV [symmetric]
```
```    66   by (simp only: card_Pow finite numeral_2_eq_2)
```
```    67
```
```    68 lemma card_nat [simp]: "CARD(nat) = 0"
```
```    69   by (simp add: infinite_UNIV_nat card_eq_0_iff)
```
```    70
```
```    71
```
```    72 subsection {* Classes with at least 1 and 2  *}
```
```    73
```
```    74 text {* Class finite already captures "at least 1" *}
```
```    75
```
```    76 lemma zero_less_card_finite [simp]: "0 < CARD('a::finite)"
```
```    77   unfolding neq0_conv [symmetric] by simp
```
```    78
```
```    79 lemma one_le_card_finite [simp]: "Suc 0 \<le> CARD('a::finite)"
```
```    80   by (simp add: less_Suc_eq_le [symmetric])
```
```    81
```
```    82 text {* Class for cardinality "at least 2" *}
```
```    83
```
```    84 class card2 = finite +
```
```    85   assumes two_le_card: "2 \<le> CARD('a)"
```
```    86
```
```    87 lemma one_less_card: "Suc 0 < CARD('a::card2)"
```
```    88   using two_le_card [where 'a='a] by simp
```
```    89
```
```    90 lemma one_less_int_card: "1 < int CARD('a::card2)"
```
```    91   using one_less_card [where 'a='a] by simp
```
```    92
```
```    93
```
```    94 subsection {* Numeral Types *}
```
```    95
```
```    96 typedef (open) num0 = "UNIV :: nat set" ..
```
```    97 typedef (open) num1 = "UNIV :: unit set" ..
```
```    98
```
```    99 typedef (open) 'a bit0 = "{0 ..< 2 * int CARD('a::finite)}"
```
```   100 proof
```
```   101   show "0 \<in> {0 ..< 2 * int CARD('a)}"
```
```   102     by simp
```
```   103 qed
```
```   104
```
```   105 typedef (open) 'a bit1 = "{0 ..< 1 + 2 * int CARD('a::finite)}"
```
```   106 proof
```
```   107   show "0 \<in> {0 ..< 1 + 2 * int CARD('a)}"
```
```   108     by simp
```
```   109 qed
```
```   110
```
```   111 lemma card_num0 [simp]: "CARD (num0) = 0"
```
```   112   unfolding type_definition.card [OF type_definition_num0]
```
```   113   by simp
```
```   114
```
```   115 lemma card_num1 [simp]: "CARD(num1) = 1"
```
```   116   unfolding type_definition.card [OF type_definition_num1]
```
```   117   by (simp only: card_unit)
```
```   118
```
```   119 lemma card_bit0 [simp]: "CARD('a bit0) = 2 * CARD('a::finite)"
```
```   120   unfolding type_definition.card [OF type_definition_bit0]
```
```   121   by simp
```
```   122
```
```   123 lemma card_bit1 [simp]: "CARD('a bit1) = Suc (2 * CARD('a::finite))"
```
```   124   unfolding type_definition.card [OF type_definition_bit1]
```
```   125   by simp
```
```   126
```
```   127 instance num1 :: finite
```
```   128 proof
```
```   129   show "finite (UNIV::num1 set)"
```
```   130     unfolding type_definition.univ [OF type_definition_num1]
```
```   131     using finite by (rule finite_imageI)
```
```   132 qed
```
```   133
```
```   134 instance bit0 :: (finite) card2
```
```   135 proof
```
```   136   show "finite (UNIV::'a bit0 set)"
```
```   137     unfolding type_definition.univ [OF type_definition_bit0]
```
```   138     by simp
```
```   139   show "2 \<le> CARD('a bit0)"
```
```   140     by simp
```
```   141 qed
```
```   142
```
```   143 instance bit1 :: (finite) card2
```
```   144 proof
```
```   145   show "finite (UNIV::'a bit1 set)"
```
```   146     unfolding type_definition.univ [OF type_definition_bit1]
```
```   147     by simp
```
```   148   show "2 \<le> CARD('a bit1)"
```
```   149     by simp
```
```   150 qed
```
```   151
```
```   152
```
```   153 subsection {* Locale for modular arithmetic subtypes *}
```
```   154
```
```   155 locale mod_type =
```
```   156   fixes n :: int
```
```   157   and Rep :: "'a::{zero,one,plus,times,uminus,minus} \<Rightarrow> int"
```
```   158   and Abs :: "int \<Rightarrow> 'a::{zero,one,plus,times,uminus,minus}"
```
```   159   assumes type: "type_definition Rep Abs {0..<n}"
```
```   160   and size1: "1 < n"
```
```   161   and zero_def: "0 = Abs 0"
```
```   162   and one_def:  "1 = Abs 1"
```
```   163   and add_def:  "x + y = Abs ((Rep x + Rep y) mod n)"
```
```   164   and mult_def: "x * y = Abs ((Rep x * Rep y) mod n)"
```
```   165   and diff_def: "x - y = Abs ((Rep x - Rep y) mod n)"
```
```   166   and minus_def: "- x = Abs ((- Rep x) mod n)"
```
```   167 begin
```
```   168
```
```   169 lemma size0: "0 < n"
```
```   170 by (cut_tac size1, simp)
```
```   171
```
```   172 lemmas definitions =
```
```   173   zero_def one_def add_def mult_def minus_def diff_def
```
```   174
```
```   175 lemma Rep_less_n: "Rep x < n"
```
```   176 by (rule type_definition.Rep [OF type, simplified, THEN conjunct2])
```
```   177
```
```   178 lemma Rep_le_n: "Rep x \<le> n"
```
```   179 by (rule Rep_less_n [THEN order_less_imp_le])
```
```   180
```
```   181 lemma Rep_inject_sym: "x = y \<longleftrightarrow> Rep x = Rep y"
```
```   182 by (rule type_definition.Rep_inject [OF type, symmetric])
```
```   183
```
```   184 lemma Rep_inverse: "Abs (Rep x) = x"
```
```   185 by (rule type_definition.Rep_inverse [OF type])
```
```   186
```
```   187 lemma Abs_inverse: "m \<in> {0..<n} \<Longrightarrow> Rep (Abs m) = m"
```
```   188 by (rule type_definition.Abs_inverse [OF type])
```
```   189
```
```   190 lemma Rep_Abs_mod: "Rep (Abs (m mod n)) = m mod n"
```
```   191 by (simp add: Abs_inverse pos_mod_conj [OF size0])
```
```   192
```
```   193 lemma Rep_Abs_0: "Rep (Abs 0) = 0"
```
```   194 by (simp add: Abs_inverse size0)
```
```   195
```
```   196 lemma Rep_0: "Rep 0 = 0"
```
```   197 by (simp add: zero_def Rep_Abs_0)
```
```   198
```
```   199 lemma Rep_Abs_1: "Rep (Abs 1) = 1"
```
```   200 by (simp add: Abs_inverse size1)
```
```   201
```
```   202 lemma Rep_1: "Rep 1 = 1"
```
```   203 by (simp add: one_def Rep_Abs_1)
```
```   204
```
```   205 lemma Rep_mod: "Rep x mod n = Rep x"
```
```   206 apply (rule_tac x=x in type_definition.Abs_cases [OF type])
```
```   207 apply (simp add: type_definition.Abs_inverse [OF type])
```
```   208 apply (simp add: mod_pos_pos_trivial)
```
```   209 done
```
```   210
```
```   211 lemmas Rep_simps =
```
```   212   Rep_inject_sym Rep_inverse Rep_Abs_mod Rep_mod Rep_Abs_0 Rep_Abs_1
```
```   213
```
```   214 lemma comm_ring_1: "OFCLASS('a, comm_ring_1_class)"
```
```   215 apply (intro_classes, unfold definitions)
```
```   216 apply (simp_all add: Rep_simps zmod_simps ring_simps)
```
```   217 done
```
```   218
```
```   219 end
```
```   220
```
```   221 locale mod_ring = mod_type +
```
```   222   constrains n :: int
```
```   223   and Rep :: "'a::{number_ring} \<Rightarrow> int"
```
```   224   and Abs :: "int \<Rightarrow> 'a::{number_ring}"
```
```   225 begin
```
```   226
```
```   227 lemma of_nat_eq: "of_nat k = Abs (int k mod n)"
```
```   228 apply (induct k)
```
```   229 apply (simp add: zero_def)
```
```   230 apply (simp add: Rep_simps add_def one_def zmod_simps add_ac)
```
```   231 done
```
```   232
```
```   233 lemma of_int_eq: "of_int z = Abs (z mod n)"
```
```   234 apply (cases z rule: int_diff_cases)
```
```   235 apply (simp add: Rep_simps of_nat_eq diff_def zmod_simps)
```
```   236 done
```
```   237
```
```   238 lemma Rep_number_of:
```
```   239   "Rep (number_of w) = number_of w mod n"
```
```   240 by (simp add: number_of_eq of_int_eq Rep_Abs_mod)
```
```   241
```
```   242 lemma iszero_number_of:
```
```   243   "iszero (number_of w::'a) \<longleftrightarrow> number_of w mod n = 0"
```
```   244 by (simp add: Rep_simps number_of_eq of_int_eq iszero_def zero_def)
```
```   245
```
```   246 lemma cases:
```
```   247   assumes 1: "\<And>z. \<lbrakk>(x::'a) = of_int z; 0 \<le> z; z < n\<rbrakk> \<Longrightarrow> P"
```
```   248   shows "P"
```
```   249 apply (cases x rule: type_definition.Abs_cases [OF type])
```
```   250 apply (rule_tac z="y" in 1)
```
```   251 apply (simp_all add: of_int_eq mod_pos_pos_trivial)
```
```   252 done
```
```   253
```
```   254 lemma induct:
```
```   255   "(\<And>z. \<lbrakk>0 \<le> z; z < n\<rbrakk> \<Longrightarrow> P (of_int z)) \<Longrightarrow> P (x::'a)"
```
```   256 by (cases x rule: cases) simp
```
```   257
```
```   258 end
```
```   259
```
```   260
```
```   261 subsection {* Number ring instances *}
```
```   262
```
```   263 text {*
```
```   264   Unfortunately a number ring instance is not possible for
```
```   265   @{typ num1}, since 0 and 1 are not distinct.
```
```   266 *}
```
```   267
```
```   268 instantiation num1 :: "{comm_ring,comm_monoid_mult,number}"
```
```   269 begin
```
```   270
```
```   271 lemma num1_eq_iff: "(x::num1) = (y::num1) \<longleftrightarrow> True"
```
```   272   by (induct x, induct y) simp
```
```   273
```
```   274 instance proof
```
```   275 qed (simp_all add: num1_eq_iff)
```
```   276
```
```   277 end
```
```   278
```
```   279 instantiation
```
```   280   bit0 and bit1 :: (finite) "{zero,one,plus,times,uminus,minus}"
```
```   281 begin
```
```   282
```
```   283 definition Abs_bit0' :: "int \<Rightarrow> 'a bit0" where
```
```   284   "Abs_bit0' x = Abs_bit0 (x mod int CARD('a bit0))"
```
```   285
```
```   286 definition Abs_bit1' :: "int \<Rightarrow> 'a bit1" where
```
```   287   "Abs_bit1' x = Abs_bit1 (x mod int CARD('a bit1))"
```
```   288
```
```   289 definition "0 = Abs_bit0 0"
```
```   290 definition "1 = Abs_bit0 1"
```
```   291 definition "x + y = Abs_bit0' (Rep_bit0 x + Rep_bit0 y)"
```
```   292 definition "x * y = Abs_bit0' (Rep_bit0 x * Rep_bit0 y)"
```
```   293 definition "x - y = Abs_bit0' (Rep_bit0 x - Rep_bit0 y)"
```
```   294 definition "- x = Abs_bit0' (- Rep_bit0 x)"
```
```   295
```
```   296 definition "0 = Abs_bit1 0"
```
```   297 definition "1 = Abs_bit1 1"
```
```   298 definition "x + y = Abs_bit1' (Rep_bit1 x + Rep_bit1 y)"
```
```   299 definition "x * y = Abs_bit1' (Rep_bit1 x * Rep_bit1 y)"
```
```   300 definition "x - y = Abs_bit1' (Rep_bit1 x - Rep_bit1 y)"
```
```   301 definition "- x = Abs_bit1' (- Rep_bit1 x)"
```
```   302
```
```   303 instance ..
```
```   304
```
```   305 end
```
```   306
```
```   307 interpretation bit0:
```
```   308   mod_type "int CARD('a::finite bit0)"
```
```   309            "Rep_bit0 :: 'a::finite bit0 \<Rightarrow> int"
```
```   310            "Abs_bit0 :: int \<Rightarrow> 'a::finite bit0"
```
```   311 apply (rule mod_type.intro)
```
```   312 apply (simp add: int_mult type_definition_bit0)
```
```   313 apply (rule one_less_int_card)
```
```   314 apply (rule zero_bit0_def)
```
```   315 apply (rule one_bit0_def)
```
```   316 apply (rule plus_bit0_def [unfolded Abs_bit0'_def])
```
```   317 apply (rule times_bit0_def [unfolded Abs_bit0'_def])
```
```   318 apply (rule minus_bit0_def [unfolded Abs_bit0'_def])
```
```   319 apply (rule uminus_bit0_def [unfolded Abs_bit0'_def])
```
```   320 done
```
```   321
```
```   322 interpretation bit1:
```
```   323   mod_type "int CARD('a::finite bit1)"
```
```   324            "Rep_bit1 :: 'a::finite bit1 \<Rightarrow> int"
```
```   325            "Abs_bit1 :: int \<Rightarrow> 'a::finite bit1"
```
```   326 apply (rule mod_type.intro)
```
```   327 apply (simp add: int_mult type_definition_bit1)
```
```   328 apply (rule one_less_int_card)
```
```   329 apply (rule zero_bit1_def)
```
```   330 apply (rule one_bit1_def)
```
```   331 apply (rule plus_bit1_def [unfolded Abs_bit1'_def])
```
```   332 apply (rule times_bit1_def [unfolded Abs_bit1'_def])
```
```   333 apply (rule minus_bit1_def [unfolded Abs_bit1'_def])
```
```   334 apply (rule uminus_bit1_def [unfolded Abs_bit1'_def])
```
```   335 done
```
```   336
```
```   337 instance bit0 :: (finite) comm_ring_1
```
```   338   by (rule bit0.comm_ring_1)+
```
```   339
```
```   340 instance bit1 :: (finite) comm_ring_1
```
```   341   by (rule bit1.comm_ring_1)+
```
```   342
```
```   343 instantiation bit0 and bit1 :: (finite) number_ring
```
```   344 begin
```
```   345
```
```   346 definition "(number_of w :: _ bit0) = of_int w"
```
```   347
```
```   348 definition "(number_of w :: _ bit1) = of_int w"
```
```   349
```
```   350 instance proof
```
```   351 qed (rule number_of_bit0_def number_of_bit1_def)+
```
```   352
```
```   353 end
```
```   354
```
```   355 interpretation bit0:
```
```   356   mod_ring "int CARD('a::finite bit0)"
```
```   357            "Rep_bit0 :: 'a::finite bit0 \<Rightarrow> int"
```
```   358            "Abs_bit0 :: int \<Rightarrow> 'a::finite bit0"
```
```   359   ..
```
```   360
```
```   361 interpretation bit1:
```
```   362   mod_ring "int CARD('a::finite bit1)"
```
```   363            "Rep_bit1 :: 'a::finite bit1 \<Rightarrow> int"
```
```   364            "Abs_bit1 :: int \<Rightarrow> 'a::finite bit1"
```
```   365   ..
```
```   366
```
```   367 text {* Set up cases, induction, and arithmetic *}
```
```   368
```
```   369 lemmas bit0_cases [case_names of_int, cases type: bit0] = bit0.cases
```
```   370 lemmas bit1_cases [case_names of_int, cases type: bit1] = bit1.cases
```
```   371
```
```   372 lemmas bit0_induct [case_names of_int, induct type: bit0] = bit0.induct
```
```   373 lemmas bit1_induct [case_names of_int, induct type: bit1] = bit1.induct
```
```   374
```
```   375 lemmas bit0_iszero_number_of [simp] = bit0.iszero_number_of
```
```   376 lemmas bit1_iszero_number_of [simp] = bit1.iszero_number_of
```
```   377
```
```   378
```
```   379 subsection {* Syntax *}
```
```   380
```
```   381 syntax
```
```   382   "_NumeralType" :: "num_const => type"  ("_")
```
```   383   "_NumeralType0" :: type ("0")
```
```   384   "_NumeralType1" :: type ("1")
```
```   385
```
```   386 translations
```
```   387   "_NumeralType1" == (type) "num1"
```
```   388   "_NumeralType0" == (type) "num0"
```
```   389
```
```   390 parse_translation {*
```
```   391 let
```
```   392
```
```   393 val num1_const = Syntax.const "Numeral_Type.num1";
```
```   394 val num0_const = Syntax.const "Numeral_Type.num0";
```
```   395 val B0_const = Syntax.const "Numeral_Type.bit0";
```
```   396 val B1_const = Syntax.const "Numeral_Type.bit1";
```
```   397
```
```   398 fun mk_bintype n =
```
```   399   let
```
```   400     fun mk_bit n = if n = 0 then B0_const else B1_const;
```
```   401     fun bin_of n =
```
```   402       if n = 1 then num1_const
```
```   403       else if n = 0 then num0_const
```
```   404       else if n = ~1 then raise TERM ("negative type numeral", [])
```
```   405       else
```
```   406         let val (q, r) = Integer.div_mod n 2;
```
```   407         in mk_bit r \$ bin_of q end;
```
```   408   in bin_of n end;
```
```   409
```
```   410 fun numeral_tr (*"_NumeralType"*) [Const (str, _)] =
```
```   411       mk_bintype (the (Int.fromString str))
```
```   412   | numeral_tr (*"_NumeralType"*) ts = raise TERM ("numeral_tr", ts);
```
```   413
```
```   414 in [("_NumeralType", numeral_tr)] end;
```
```   415 *}
```
```   416
```
```   417 print_translation {*
```
```   418 let
```
```   419 fun int_of [] = 0
```
```   420   | int_of (b :: bs) = b + 2 * int_of bs;
```
```   421
```
```   422 fun bin_of (Const ("num0", _)) = []
```
```   423   | bin_of (Const ("num1", _)) = [1]
```
```   424   | bin_of (Const ("bit0", _) \$ bs) = 0 :: bin_of bs
```
```   425   | bin_of (Const ("bit1", _) \$ bs) = 1 :: bin_of bs
```
```   426   | bin_of t = raise TERM("bin_of", [t]);
```
```   427
```
```   428 fun bit_tr' b [t] =
```
```   429   let
```
```   430     val rev_digs = b :: bin_of t handle TERM _ => raise Match
```
```   431     val i = int_of rev_digs;
```
```   432     val num = string_of_int (abs i);
```
```   433   in
```
```   434     Syntax.const "_NumeralType" \$ Syntax.free num
```
```   435   end
```
```   436   | bit_tr' b _ = raise Match;
```
```   437
```
```   438 in [("bit0", bit_tr' 0), ("bit1", bit_tr' 1)] end;
```
```   439 *}
```
```   440
```
```   441 subsection {* Examples *}
```
```   442
```
```   443 lemma "CARD(0) = 0" by simp
```
```   444 lemma "CARD(17) = 17" by simp
```
```   445 lemma "8 * 11 ^ 3 - 6 = (2::5)" by simp
```
```   446
```
```   447 end
```