1.1 --- a/src/HOL/Library/Numeral_Type.thy Fri Feb 15 10:52:47 2013 +0100
1.2 +++ b/src/HOL/Library/Numeral_Type.thy Fri Feb 15 11:02:34 2013 +0100
1.3 @@ -29,6 +29,10 @@
1.4 unfolding type_definition.card [OF type_definition_num0]
1.5 by simp
1.6
1.7 +lemma infinite_num0: "\<not> finite (UNIV :: num0 set)"
1.8 + using card_num0[unfolded card_eq_0_iff]
1.9 + by simp
1.10 +
1.11 lemma card_num1 [simp]: "CARD(num1) = 1"
1.12 unfolding type_definition.card [OF type_definition_num1]
1.13 by (simp only: card_UNIV_unit)
1.14 @@ -283,6 +287,172 @@
1.15 declare eq_numeral_iff_iszero [where 'a="('a::finite) bit0", standard, simp]
1.16 declare eq_numeral_iff_iszero [where 'a="('a::finite) bit1", standard, simp]
1.17
1.18 +subsection {* Linorder instance *}
1.19 +
1.20 +instantiation bit0 and bit1 :: (finite) linorder begin
1.21 +
1.22 +definition "a < b \<longleftrightarrow> Rep_bit0 a < Rep_bit0 b"
1.23 +definition "a \<le> b \<longleftrightarrow> Rep_bit0 a \<le> Rep_bit0 b"
1.24 +definition "a < b \<longleftrightarrow> Rep_bit1 a < Rep_bit1 b"
1.25 +definition "a \<le> b \<longleftrightarrow> Rep_bit1 a \<le> Rep_bit1 b"
1.26 +
1.27 +instance
1.28 + by(intro_classes)
1.29 + (auto simp add: less_eq_bit0_def less_bit0_def less_eq_bit1_def less_bit1_def Rep_bit0_inject Rep_bit1_inject)
1.30 +
1.31 +end
1.32 +
1.33 +subsection {* Code setup and type classes for code generation *}
1.34 +
1.35 +text {* Code setup for @{typ num0} and @{typ num1} *}
1.36 +
1.37 +definition Num0 :: num0 where "Num0 = Abs_num0 0"
1.38 +code_datatype Num0
1.39 +
1.40 +instantiation num0 :: equal begin
1.41 +definition equal_num0 :: "num0 \<Rightarrow> num0 \<Rightarrow> bool"
1.42 + where "equal_num0 = op ="
1.43 +instance by intro_classes (simp add: equal_num0_def)
1.44 +end
1.45 +
1.46 +lemma equal_num0_code [code]:
1.47 + "equal_class.equal Num0 Num0 = True"
1.48 +by(rule equal_refl)
1.49 +
1.50 +code_datatype "1 :: num1"
1.51 +
1.52 +instantiation num1 :: equal begin
1.53 +definition equal_num1 :: "num1 \<Rightarrow> num1 \<Rightarrow> bool"
1.54 + where "equal_num1 = op ="
1.55 +instance by intro_classes (simp add: equal_num1_def)
1.56 +end
1.57 +
1.58 +lemma equal_num1_code [code]:
1.59 + "equal_class.equal (1 :: num1) 1 = True"
1.60 +by(rule equal_refl)
1.61 +
1.62 +instantiation num1 :: enum begin
1.63 +definition "enum_class.enum = [1 :: num1]"
1.64 +definition "enum_class.enum_all P = P (1 :: num1)"
1.65 +definition "enum_class.enum_ex P = P (1 :: num1)"
1.66 +instance
1.67 + by intro_classes
1.68 + (auto simp add: enum_num1_def enum_all_num1_def enum_ex_num1_def num1_eq_iff Ball_def,
1.69 + (metis (full_types) num1_eq_iff)+)
1.70 +end
1.71 +
1.72 +instantiation num0 and num1 :: card_UNIV begin
1.73 +definition "finite_UNIV = Phantom(num0) False"
1.74 +definition "card_UNIV = Phantom(num0) 0"
1.75 +definition "finite_UNIV = Phantom(num1) True"
1.76 +definition "card_UNIV = Phantom(num1) 1"
1.77 +instance
1.78 + by intro_classes
1.79 + (simp_all add: finite_UNIV_num0_def card_UNIV_num0_def infinite_num0 finite_UNIV_num1_def card_UNIV_num1_def)
1.80 +end
1.81 +
1.82 +
1.83 +text {* Code setup for @{typ "'a bit0"} and @{typ "'a bit1"} *}
1.84 +
1.85 +declare
1.86 + bit0.Rep_inverse[code abstype]
1.87 + bit0.Rep_0[code abstract]
1.88 + bit0.Rep_1[code abstract]
1.89 +
1.90 +lemma Abs_bit0'_code [code abstract]:
1.91 + "Rep_bit0 (Abs_bit0' x :: 'a :: finite bit0) = x mod int (CARD('a bit0))"
1.92 +by(auto simp add: Abs_bit0'_def intro!: Abs_bit0_inverse)
1.93 + (metis bit0.Rep_Abs_mod bit0.Rep_less_n card_bit0 of_nat_numeral zmult_int)
1.94 +
1.95 +lemma inj_on_Abs_bit0:
1.96 + "inj_on (Abs_bit0 :: int \<Rightarrow> 'a bit0) {0..<2 * int CARD('a :: finite)}"
1.97 +by(auto intro: inj_onI simp add: Abs_bit0_inject)
1.98 +
1.99 +declare
1.100 + bit1.Rep_inverse[code abstype]
1.101 + bit1.Rep_0[code abstract]
1.102 + bit1.Rep_1[code abstract]
1.103 +
1.104 +lemma Abs_bit1'_code [code abstract]:
1.105 + "Rep_bit1 (Abs_bit1' x :: 'a :: finite bit1) = x mod int (CARD('a bit1))"
1.106 +by(auto simp add: Abs_bit1'_def intro!: Abs_bit1_inverse)
1.107 + (metis of_nat_0_less_iff of_nat_Suc of_nat_mult of_nat_numeral pos_mod_conj zero_less_Suc)
1.108 +
1.109 +lemma inj_on_Abs_bit1:
1.110 + "inj_on (Abs_bit1 :: int \<Rightarrow> 'a bit1) {0..<1 + 2 * int CARD('a :: finite)}"
1.111 +by(auto intro: inj_onI simp add: Abs_bit1_inject)
1.112 +
1.113 +instantiation bit0 and bit1 :: (finite) equal begin
1.114 +
1.115 +definition "equal_class.equal x y \<longleftrightarrow> Rep_bit0 x = Rep_bit0 y"
1.116 +definition "equal_class.equal x y \<longleftrightarrow> Rep_bit1 x = Rep_bit1 y"
1.117 +
1.118 +instance
1.119 + by intro_classes (simp_all add: equal_bit0_def equal_bit1_def Rep_bit0_inject Rep_bit1_inject)
1.120 +
1.121 +end
1.122 +
1.123 +instantiation bit0 :: (finite) enum begin
1.124 +definition "(enum_class.enum :: 'a bit0 list) = map (Abs_bit0' \<circ> int) (upt 0 (CARD('a bit0)))"
1.125 +definition "enum_class.enum_all P = (\<forall>b :: 'a bit0 \<in> set enum_class.enum. P b)"
1.126 +definition "enum_class.enum_ex P = (\<exists>b :: 'a bit0 \<in> set enum_class.enum. P b)"
1.127 +
1.128 +instance
1.129 +proof(intro_classes)
1.130 + show "distinct (enum_class.enum :: 'a bit0 list)"
1.131 + by(auto intro!: inj_onI simp add: Abs_bit0'_def Abs_bit0_inject zmod_int[symmetric] enum_bit0_def distinct_map)
1.132 +
1.133 + show univ_eq: "(UNIV :: 'a bit0 set) = set enum_class.enum"
1.134 + unfolding enum_bit0_def type_definition.Abs_image[OF type_definition_bit0, symmetric]
1.135 + by(simp add: image_comp inj_on_Abs_bit0 card_image image_int_atLeastLessThan)
1.136 + (auto intro!: image_cong[OF refl] simp add: Abs_bit0'_def mod_pos_pos_trivial)
1.137 +
1.138 + fix P :: "'a bit0 \<Rightarrow> bool"
1.139 + show "enum_class.enum_all P = Ball UNIV P"
1.140 + and "enum_class.enum_ex P = Bex UNIV P"
1.141 + by(simp_all add: enum_all_bit0_def enum_ex_bit0_def univ_eq)
1.142 +qed
1.143 +
1.144 +end
1.145 +
1.146 +instantiation bit1 :: (finite) enum begin
1.147 +definition "(enum_class.enum :: 'a bit1 list) = map (Abs_bit1' \<circ> int) (upt 0 (CARD('a bit1)))"
1.148 +definition "enum_class.enum_all P = (\<forall>b :: 'a bit1 \<in> set enum_class.enum. P b)"
1.149 +definition "enum_class.enum_ex P = (\<exists>b :: 'a bit1 \<in> set enum_class.enum. P b)"
1.150 +
1.151 +instance
1.152 +proof(intro_classes)
1.153 + show "distinct (enum_class.enum :: 'a bit1 list)"
1.154 + by(simp only: Abs_bit1'_def zmod_int[symmetric] enum_bit1_def distinct_map Suc_eq_plus1 card_bit1 o_apply inj_on_def)
1.155 + (clarsimp simp add: Abs_bit1_inject)
1.156 +
1.157 + show univ_eq: "(UNIV :: 'a bit1 set) = set enum_class.enum"
1.158 + unfolding enum_bit1_def type_definition.Abs_image[OF type_definition_bit1, symmetric]
1.159 + by(simp add: image_comp inj_on_Abs_bit1 card_image image_int_atLeastLessThan)
1.160 + (auto intro!: image_cong[OF refl] simp add: Abs_bit1'_def mod_pos_pos_trivial)
1.161 +
1.162 + fix P :: "'a bit1 \<Rightarrow> bool"
1.163 + show "enum_class.enum_all P = Ball UNIV P"
1.164 + and "enum_class.enum_ex P = Bex UNIV P"
1.165 + by(simp_all add: enum_all_bit1_def enum_ex_bit1_def univ_eq)
1.166 +qed
1.167 +
1.168 +end
1.169 +
1.170 +instantiation bit0 and bit1 :: (finite) finite_UNIV begin
1.171 +definition "finite_UNIV = Phantom('a bit0) True"
1.172 +definition "finite_UNIV = Phantom('a bit1) True"
1.173 +instance by intro_classes (simp_all add: finite_UNIV_bit0_def finite_UNIV_bit1_def)
1.174 +end
1.175 +
1.176 +instantiation bit0 and bit1 :: ("{finite,card_UNIV}") card_UNIV begin
1.177 +definition "card_UNIV = Phantom('a bit0) (2 * of_phantom (card_UNIV :: 'a card_UNIV))"
1.178 +definition
1.179 + "card_UNIV = Phantom('a bit1) (let ca = of_phantom (card_UNIV :: 'a card_UNIV)
1.180 + in if ca \<noteq> 0 then 1 + 2 * ca else 2 * ca)"
1.181 +instance by intro_classes (simp_all add: card_UNIV_bit0_def card_UNIV_bit1_def card_UNIV)
1.182 +end
1.183 +
1.184 subsection {* Syntax *}
1.185
1.186 syntax