haftmann@29629: (* Title: HOL/Library/Numeral_Type.thy haftmann@29629: Author: Brian Huffman kleing@24332: *) kleing@24332: haftmann@29629: header {* Numeral Syntax for Types *} kleing@24332: kleing@24332: theory Numeral_Type haftmann@37653: imports Cardinality kleing@24332: begin kleing@24332: kleing@24332: subsection {* Numeral Types *} kleing@24332: huffman@24406: typedef (open) num0 = "UNIV :: nat set" .. kleing@24332: typedef (open) num1 = "UNIV :: unit set" .. huffman@29997: huffman@29997: typedef (open) 'a bit0 = "{0 ..< 2 * int CARD('a::finite)}" huffman@29997: proof huffman@29997: show "0 \ {0 ..< 2 * int CARD('a)}" huffman@29997: by simp huffman@29997: qed huffman@29997: huffman@29997: typedef (open) 'a bit1 = "{0 ..< 1 + 2 * int CARD('a::finite)}" huffman@29997: proof huffman@29997: show "0 \ {0 ..< 1 + 2 * int CARD('a)}" huffman@29997: by simp huffman@29997: qed kleing@24332: huffman@30001: lemma card_num0 [simp]: "CARD (num0) = 0" huffman@30001: unfolding type_definition.card [OF type_definition_num0] huffman@30001: by simp huffman@30001: huffman@30001: lemma card_num1 [simp]: "CARD(num1) = 1" huffman@30001: unfolding type_definition.card [OF type_definition_num1] huffman@30001: by (simp only: card_unit) huffman@30001: huffman@30001: lemma card_bit0 [simp]: "CARD('a bit0) = 2 * CARD('a::finite)" huffman@30001: unfolding type_definition.card [OF type_definition_bit0] huffman@30001: by simp huffman@30001: huffman@30001: lemma card_bit1 [simp]: "CARD('a bit1) = Suc (2 * CARD('a::finite))" huffman@30001: unfolding type_definition.card [OF type_definition_bit1] huffman@30001: by simp huffman@30001: kleing@24332: instance num1 :: finite kleing@24332: proof kleing@24332: show "finite (UNIV::num1 set)" kleing@24332: unfolding type_definition.univ [OF type_definition_num1] kleing@24332: using finite by (rule finite_imageI) kleing@24332: qed kleing@24332: huffman@30001: instance bit0 :: (finite) card2 kleing@24332: proof kleing@24332: show "finite (UNIV::'a bit0 set)" kleing@24332: unfolding type_definition.univ [OF type_definition_bit0] huffman@29997: by simp huffman@30001: show "2 \ CARD('a bit0)" huffman@30001: by simp kleing@24332: qed kleing@24332: huffman@30001: instance bit1 :: (finite) card2 kleing@24332: proof kleing@24332: show "finite (UNIV::'a bit1 set)" kleing@24332: unfolding type_definition.univ [OF type_definition_bit1] huffman@29997: by simp huffman@30001: show "2 \ CARD('a bit1)" huffman@30001: by simp kleing@24332: qed kleing@24332: wenzelm@25378: haftmann@37653: subsection {* Locales for for modular arithmetic subtypes *} huffman@29997: huffman@29997: locale mod_type = huffman@29997: fixes n :: int haftmann@30960: and Rep :: "'a::{zero,one,plus,times,uminus,minus} \ int" haftmann@30960: and Abs :: "int \ 'a::{zero,one,plus,times,uminus,minus}" huffman@29997: assumes type: "type_definition Rep Abs {0.. n" huffman@29997: by (rule Rep_less_n [THEN order_less_imp_le]) huffman@29997: huffman@29997: lemma Rep_inject_sym: "x = y \ Rep x = Rep y" huffman@29997: by (rule type_definition.Rep_inject [OF type, symmetric]) huffman@29997: huffman@29997: lemma Rep_inverse: "Abs (Rep x) = x" huffman@29997: by (rule type_definition.Rep_inverse [OF type]) huffman@29997: huffman@29997: lemma Abs_inverse: "m \ {0.. Rep (Abs m) = m" huffman@29997: by (rule type_definition.Abs_inverse [OF type]) huffman@29997: huffman@29997: lemma Rep_Abs_mod: "Rep (Abs (m mod n)) = m mod n" haftmann@33361: by (simp add: Abs_inverse pos_mod_conj [OF size0]) huffman@29997: huffman@29997: lemma Rep_Abs_0: "Rep (Abs 0) = 0" huffman@29997: by (simp add: Abs_inverse size0) huffman@29997: huffman@29997: lemma Rep_0: "Rep 0 = 0" huffman@29997: by (simp add: zero_def Rep_Abs_0) huffman@29997: huffman@29997: lemma Rep_Abs_1: "Rep (Abs 1) = 1" huffman@29997: by (simp add: Abs_inverse size1) huffman@29997: huffman@29997: lemma Rep_1: "Rep 1 = 1" huffman@29997: by (simp add: one_def Rep_Abs_1) huffman@29997: huffman@29997: lemma Rep_mod: "Rep x mod n = Rep x" huffman@29997: apply (rule_tac x=x in type_definition.Abs_cases [OF type]) huffman@29997: apply (simp add: type_definition.Abs_inverse [OF type]) huffman@29997: apply (simp add: mod_pos_pos_trivial) huffman@29997: done huffman@29997: huffman@29997: lemmas Rep_simps = huffman@29997: Rep_inject_sym Rep_inverse Rep_Abs_mod Rep_mod Rep_Abs_0 Rep_Abs_1 huffman@29997: huffman@29997: lemma comm_ring_1: "OFCLASS('a, comm_ring_1_class)" huffman@29997: apply (intro_classes, unfold definitions) haftmann@36350: apply (simp_all add: Rep_simps zmod_simps field_simps) huffman@29997: done huffman@29997: huffman@29997: end huffman@29997: huffman@29997: locale mod_ring = mod_type + huffman@29997: constrains n :: int haftmann@30960: and Rep :: "'a::{number_ring} \ int" haftmann@30960: and Abs :: "int \ 'a::{number_ring}" huffman@29997: begin huffman@29997: huffman@29997: lemma of_nat_eq: "of_nat k = Abs (int k mod n)" huffman@29997: apply (induct k) huffman@29997: apply (simp add: zero_def) huffman@29997: apply (simp add: Rep_simps add_def one_def zmod_simps add_ac) huffman@29997: done huffman@29997: huffman@29997: lemma of_int_eq: "of_int z = Abs (z mod n)" huffman@29997: apply (cases z rule: int_diff_cases) huffman@29997: apply (simp add: Rep_simps of_nat_eq diff_def zmod_simps) huffman@29997: done huffman@29997: huffman@29997: lemma Rep_number_of: huffman@29997: "Rep (number_of w) = number_of w mod n" huffman@29997: by (simp add: number_of_eq of_int_eq Rep_Abs_mod) huffman@29997: huffman@29997: lemma iszero_number_of: huffman@29997: "iszero (number_of w::'a) \ number_of w mod n = 0" huffman@29997: by (simp add: Rep_simps number_of_eq of_int_eq iszero_def zero_def) huffman@29997: huffman@29997: lemma cases: huffman@29997: assumes 1: "\z. \(x::'a) = of_int z; 0 \ z; z < n\ \ P" huffman@29997: shows "P" huffman@29997: apply (cases x rule: type_definition.Abs_cases [OF type]) huffman@29997: apply (rule_tac z="y" in 1) huffman@29997: apply (simp_all add: of_int_eq mod_pos_pos_trivial) huffman@29997: done huffman@29997: huffman@29997: lemma induct: huffman@29997: "(\z. \0 \ z; z < n\ \ P (of_int z)) \ P (x::'a)" huffman@29997: by (cases x rule: cases) simp huffman@29997: huffman@29997: end huffman@29997: huffman@29997: huffman@29997: subsection {* Number ring instances *} huffman@29997: huffman@30032: text {* huffman@30032: Unfortunately a number ring instance is not possible for huffman@30032: @{typ num1}, since 0 and 1 are not distinct. huffman@30032: *} huffman@30032: haftmann@30960: instantiation num1 :: "{comm_ring,comm_monoid_mult,number}" huffman@30032: begin huffman@30032: huffman@30032: lemma num1_eq_iff: "(x::num1) = (y::num1) \ True" huffman@30032: by (induct x, induct y) simp huffman@30032: huffman@30032: instance proof huffman@30032: qed (simp_all add: num1_eq_iff) huffman@30032: huffman@30032: end huffman@30032: huffman@29997: instantiation haftmann@30960: bit0 and bit1 :: (finite) "{zero,one,plus,times,uminus,minus}" huffman@29997: begin huffman@29997: huffman@29997: definition Abs_bit0' :: "int \ 'a bit0" where huffman@29998: "Abs_bit0' x = Abs_bit0 (x mod int CARD('a bit0))" huffman@29997: huffman@29997: definition Abs_bit1' :: "int \ 'a bit1" where huffman@29998: "Abs_bit1' x = Abs_bit1 (x mod int CARD('a bit1))" huffman@29997: huffman@29997: definition "0 = Abs_bit0 0" huffman@29997: definition "1 = Abs_bit0 1" huffman@29997: definition "x + y = Abs_bit0' (Rep_bit0 x + Rep_bit0 y)" huffman@29997: definition "x * y = Abs_bit0' (Rep_bit0 x * Rep_bit0 y)" huffman@29997: definition "x - y = Abs_bit0' (Rep_bit0 x - Rep_bit0 y)" huffman@29997: definition "- x = Abs_bit0' (- Rep_bit0 x)" huffman@29997: huffman@29997: definition "0 = Abs_bit1 0" huffman@29997: definition "1 = Abs_bit1 1" huffman@29997: definition "x + y = Abs_bit1' (Rep_bit1 x + Rep_bit1 y)" huffman@29997: definition "x * y = Abs_bit1' (Rep_bit1 x * Rep_bit1 y)" huffman@29997: definition "x - y = Abs_bit1' (Rep_bit1 x - Rep_bit1 y)" huffman@29997: definition "- x = Abs_bit1' (- Rep_bit1 x)" huffman@29997: huffman@29997: instance .. huffman@29997: huffman@29997: end huffman@29997: wenzelm@30729: interpretation bit0: huffman@29998: mod_type "int CARD('a::finite bit0)" huffman@29997: "Rep_bit0 :: 'a::finite bit0 \ int" huffman@29997: "Abs_bit0 :: int \ 'a::finite bit0" huffman@29997: apply (rule mod_type.intro) huffman@29998: apply (simp add: int_mult type_definition_bit0) huffman@30001: apply (rule one_less_int_card) huffman@29997: apply (rule zero_bit0_def) huffman@29997: apply (rule one_bit0_def) huffman@29997: apply (rule plus_bit0_def [unfolded Abs_bit0'_def]) huffman@29997: apply (rule times_bit0_def [unfolded Abs_bit0'_def]) huffman@29997: apply (rule minus_bit0_def [unfolded Abs_bit0'_def]) huffman@29997: apply (rule uminus_bit0_def [unfolded Abs_bit0'_def]) huffman@29997: done huffman@29997: wenzelm@30729: interpretation bit1: huffman@29998: mod_type "int CARD('a::finite bit1)" huffman@29997: "Rep_bit1 :: 'a::finite bit1 \ int" huffman@29997: "Abs_bit1 :: int \ 'a::finite bit1" huffman@29997: apply (rule mod_type.intro) huffman@29998: apply (simp add: int_mult type_definition_bit1) huffman@30001: apply (rule one_less_int_card) huffman@29997: apply (rule zero_bit1_def) huffman@29997: apply (rule one_bit1_def) huffman@29997: apply (rule plus_bit1_def [unfolded Abs_bit1'_def]) huffman@29997: apply (rule times_bit1_def [unfolded Abs_bit1'_def]) huffman@29997: apply (rule minus_bit1_def [unfolded Abs_bit1'_def]) huffman@29997: apply (rule uminus_bit1_def [unfolded Abs_bit1'_def]) huffman@29997: done huffman@29997: haftmann@31021: instance bit0 :: (finite) comm_ring_1 haftmann@31021: by (rule bit0.comm_ring_1)+ huffman@29997: haftmann@31021: instance bit1 :: (finite) comm_ring_1 haftmann@31021: by (rule bit1.comm_ring_1)+ huffman@29997: huffman@29997: instantiation bit0 and bit1 :: (finite) number_ring huffman@29997: begin huffman@29997: huffman@29997: definition "(number_of w :: _ bit0) = of_int w" huffman@29997: huffman@29997: definition "(number_of w :: _ bit1) = of_int w" huffman@29997: huffman@29997: instance proof huffman@29997: qed (rule number_of_bit0_def number_of_bit1_def)+ huffman@29997: huffman@29997: end huffman@29997: wenzelm@30729: interpretation bit0: huffman@29998: mod_ring "int CARD('a::finite bit0)" huffman@29997: "Rep_bit0 :: 'a::finite bit0 \ int" huffman@29997: "Abs_bit0 :: int \ 'a::finite bit0" huffman@29997: .. huffman@29997: wenzelm@30729: interpretation bit1: huffman@29998: mod_ring "int CARD('a::finite bit1)" huffman@29997: "Rep_bit1 :: 'a::finite bit1 \ int" huffman@29997: "Abs_bit1 :: int \ 'a::finite bit1" huffman@29997: .. huffman@29997: huffman@29997: text {* Set up cases, induction, and arithmetic *} huffman@29997: huffman@29999: lemmas bit0_cases [case_names of_int, cases type: bit0] = bit0.cases huffman@29999: lemmas bit1_cases [case_names of_int, cases type: bit1] = bit1.cases huffman@29997: huffman@29999: lemmas bit0_induct [case_names of_int, induct type: bit0] = bit0.induct huffman@29999: lemmas bit1_induct [case_names of_int, induct type: bit1] = bit1.induct huffman@29997: huffman@29997: lemmas bit0_iszero_number_of [simp] = bit0.iszero_number_of huffman@29997: lemmas bit1_iszero_number_of [simp] = bit1.iszero_number_of huffman@29997: huffman@29997: kleing@24332: subsection {* Syntax *} kleing@24332: kleing@24332: syntax wenzelm@46236: "_NumeralType" :: "num_token => type" ("_") kleing@24332: "_NumeralType0" :: type ("0") kleing@24332: "_NumeralType1" :: type ("1") kleing@24332: kleing@24332: translations wenzelm@35362: (type) "1" == (type) "num1" wenzelm@35362: (type) "0" == (type) "num0" kleing@24332: kleing@24332: parse_translation {* kleing@24332: let wenzelm@46236: fun mk_bintype n = wenzelm@46236: let wenzelm@46236: fun mk_bit 0 = Syntax.const @{type_syntax bit0} wenzelm@46236: | mk_bit 1 = Syntax.const @{type_syntax bit1}; wenzelm@46236: fun bin_of n = wenzelm@46236: if n = 1 then Syntax.const @{type_syntax num1} wenzelm@46236: else if n = 0 then Syntax.const @{type_syntax num0} wenzelm@46236: else if n = ~1 then raise TERM ("negative type numeral", []) wenzelm@46236: else wenzelm@46236: let val (q, r) = Integer.div_mod n 2; wenzelm@46236: in mk_bit r $ bin_of q end; wenzelm@46236: in bin_of n end; kleing@24332: wenzelm@46236: fun numeral_tr [Free (str, _)] = mk_bintype (the (Int.fromString str)) wenzelm@46236: | numeral_tr ts = raise TERM ("numeral_tr", ts); kleing@24332: wenzelm@35115: in [(@{syntax_const "_NumeralType"}, numeral_tr)] end; kleing@24332: *} kleing@24332: kleing@24332: print_translation {* kleing@24332: let wenzelm@46236: fun int_of [] = 0 wenzelm@46236: | int_of (b :: bs) = b + 2 * int_of bs; kleing@24332: wenzelm@46236: fun bin_of (Const (@{type_syntax num0}, _)) = [] wenzelm@46236: | bin_of (Const (@{type_syntax num1}, _)) = [1] wenzelm@46236: | bin_of (Const (@{type_syntax bit0}, _) $ bs) = 0 :: bin_of bs wenzelm@46236: | bin_of (Const (@{type_syntax bit1}, _) $ bs) = 1 :: bin_of bs wenzelm@46236: | bin_of t = raise TERM ("bin_of", [t]); kleing@24332: wenzelm@46236: fun bit_tr' b [t] = wenzelm@46236: let wenzelm@46236: val rev_digs = b :: bin_of t handle TERM _ => raise Match wenzelm@46236: val i = int_of rev_digs; wenzelm@46236: val num = string_of_int (abs i); wenzelm@46236: in wenzelm@46236: Syntax.const @{syntax_const "_NumeralType"} $ Syntax.free num wenzelm@46236: end wenzelm@46236: | bit_tr' b _ = raise Match; wenzelm@35362: in [(@{type_syntax bit0}, bit_tr' 0), (@{type_syntax bit1}, bit_tr' 1)] end; kleing@24332: *} kleing@24332: kleing@24332: subsection {* Examples *} kleing@24332: kleing@24332: lemma "CARD(0) = 0" by simp kleing@24332: lemma "CARD(17) = 17" by simp huffman@29997: lemma "8 * 11 ^ 3 - 6 = (2::5)" by simp huffman@28920: kleing@24332: end