# Theory Mod_Type

```(*
Title:      Mod_Type.thy
Author:     Jose Divasón <jose.divasonm at unirioja.es>
Author:     Jesús Aransay <jesus-maria.aransay at unirioja.es>
*)

section‹Class for modular arithmetic›

theory Mod_Type
imports
"HOL-Library.Numeral_Type"
"HOL-Analysis.Cartesian_Euclidean_Space"
Dual_Order
begin

subsection‹Definition and properties›

text‹Class for modular arithmetic. It is inspired by the locale mod\_type.›

class mod_type = times + wellorder + neg_numeral +
fixes Rep :: "'a => int"
and Abs :: "int => 'a"
assumes type: "type_definition Rep Abs {0..<int CARD ('a)}"
and size1: "1 < int CARD ('a)"
and zero_def: "0 = Abs 0"
and one_def:  "1 = Abs 1"
and add_def:  "x + y = Abs ((Rep x + Rep y) mod (int CARD ('a)))"
and mult_def: "x * y = Abs ((Rep x * Rep y) mod (int CARD ('a)))"
and diff_def: "x - y = Abs ((Rep x - Rep y) mod (int CARD ('a)))"
and minus_def: "- x = Abs ((- Rep x) mod (int CARD ('a)))"
and strict_mono_Rep: "strict_mono Rep"
begin

lemma size0: "0 < int CARD ('a)"
using size1 by simp

lemmas definitions =
zero_def one_def add_def mult_def minus_def diff_def

lemma Rep_less_n: "Rep x < int CARD ('a)"
by (rule type_definition.Rep [OF type, simplified, THEN conjunct2])

lemma Rep_le_n: "Rep x ≤ int CARD ('a)"
by (rule Rep_less_n [THEN order_less_imp_le])

lemma Rep_inject_sym: "x = y ⟷ Rep x = Rep y"
by (rule type_definition.Rep_inject [OF type, symmetric])

lemma Rep_inverse: "Abs (Rep x) = x"
by (rule type_definition.Rep_inverse [OF type])

lemma Abs_inverse: "m ∈ {0..<int CARD ('a)} ⟹ Rep (Abs m) = m"
by (rule type_definition.Abs_inverse [OF type])

lemma Rep_Abs_mod: "Rep (Abs (m mod int CARD ('a))) = m mod int CARD ('a)"
using size0 by (auto simp add: Abs_inverse)

lemma Rep_Abs_0: "Rep (Abs 0) = 0"
apply (rule Abs_inverse [of 0])
using size0 by simp

lemma Rep_0: "Rep 0 = 0"

lemma Rep_Abs_1: "Rep (Abs 1) = 1"

lemma Rep_1: "Rep 1 = 1"

lemma Rep_mod: "Rep x mod int CARD ('a) = Rep x"
apply (rule_tac x=x in type_definition.Abs_cases [OF type])
apply (simp add: type_definition.Abs_inverse [OF type])
done

lemmas Rep_simps =
Rep_inject_sym Rep_inverse Rep_Abs_mod Rep_mod Rep_Abs_0 Rep_Abs_1

subsection‹Conversion between a modular class and the subset of natural numbers associated.›
text‹Definitions to make transformations among elements of a modular class and naturals›
definition to_nat :: "'a => nat"
where "to_nat = nat ∘ Rep"

definition Abs' :: "int => 'a"
where "Abs' x = Abs(x mod int CARD ('a))"

definition from_nat :: "nat ⇒ 'a"
where "from_nat = (Abs' ∘ int)"

lemma bij_Rep: "bij_betw (Rep) (UNIV::'a set) {0..<int CARD('a)}"
proof (unfold bij_betw_def, rule conjI)
show "inj Rep" by (metis strict_mono_imp_inj_on strict_mono_Rep)
show "range Rep = {0..<int CARD('a)}" using Typedef.type_definition.Rep_range[OF type] .
qed

lemma mono_Rep: "mono Rep" by (metis strict_mono_Rep strict_mono_mono)

lemma Rep_ge_0: "0 ≤ Rep x" using bij_Rep unfolding bij_betw_def by auto

lemma bij_Abs: "bij_betw (Abs) {0..<int CARD('a)} (UNIV::'a set)"
proof (unfold bij_betw_def, rule conjI)
show "inj_on Abs {0..<int CARD('a)}" by (metis inj_on_inverseI type type_definition.Abs_inverse)
show "Abs ` {0..<int CARD('a)} = (UNIV::'a set)" by (metis type type_definition.univ)
qed

corollary bij_Abs': "bij_betw (Abs') {0..<int CARD('a)} (UNIV::'a set)"
proof (unfold bij_betw_def, rule conjI)
show "inj_on Abs' {0..<int CARD('a)}"
unfolding inj_on_def Abs'_def
by (auto, metis Rep_Abs_mod mod_pos_pos_trivial)
show "Abs' ` {0..<int CARD('a)} = (UNIV::'a set)"
proof (unfold image_def Abs'_def, auto)
fix x show "∃xa∈{0..<int CARD('a)}. x = Abs xa"
by (rule bexI[of _ "Rep x"], auto simp add: Rep_less_n[of x] Rep_ge_0[of x], metis Rep_inverse)
qed
qed

lemma bij_from_nat: "bij_betw (from_nat) {0..<CARD('a)} (UNIV::'a set)"
proof (unfold bij_betw_def, rule conjI)
have set_eq: "{0::int..<int CARD('a)} = int` {0..<CARD('a)}" apply (auto)
proof -
fix x::int  assume x1: "(0::int) ≤ x" and x2: "x < int CARD('a)" show "x ∈ int ` {0::nat..<CARD('a)}"
proof (unfold image_def, auto, rule bexI[of _ "nat x"])
show " x = int (nat x)" using x1 by auto
show "nat x ∈ {0::nat..<CARD('a)}" using x1 x2 by auto
qed
qed
show "inj_on (from_nat::nat⇒'a) {0::nat..<CARD('a)}"
proof (unfold from_nat_def , rule comp_inj_on)
show "inj_on int {0::nat..<CARD('a)}" by (metis inj_of_nat subset_inj_on top_greatest)
show "inj_on (Abs'::int=>'a) (int ` {0::nat..<CARD('a)})"
using bij_Abs unfolding bij_betw_def set_eq
by (metis (opaque_lifting, no_types) Abs'_def Abs_inverse Rep_inverse Rep_mod inj_on_def set_eq)
qed
show "(from_nat::nat=>'a)` {0::nat..<CARD('a)} = UNIV"
unfolding from_nat_def using bij_Abs'
unfolding bij_betw_def set_eq o_def by blast
qed

lemma to_nat_is_inv: "the_inv_into {0..<CARD('a)} (from_nat::nat=>'a) = (to_nat::'a=>nat)"
proof (unfold the_inv_into_def fun_eq_iff from_nat_def to_nat_def o_def, clarify)
fix x::"'a" show "(THE y::nat. y ∈ {0::nat..<CARD('a)} ∧ Abs' (int y) = x) = nat (Rep x)"
proof (rule the_equality, auto)
show " Abs' (Rep x) = x" by (metis Abs'_def Rep_inverse Rep_mod)
show "nat (Rep x) < CARD('a)" by (metis (full_types) Rep_less_n nat_int size0 zless_nat_conj)
assume x:  "¬ (0::int) ≤ Rep x" show "(0::nat) < CARD('a)" and "Abs' (0::int) = x"
using Rep_ge_0 x by auto
next
fix y::nat assume y: "y < CARD('a)"
have "(Rep(Abs'(int y)::'a)) = (Rep((Abs(int y mod int CARD('a)))::'a))" unfolding Abs'_def ..
also have "... =  (Rep (Abs (int y)::'a))" using zmod_int[of y "CARD('a)"]
using y mod_less by auto
also have "... =  (int y)" proof (rule Abs_inverse) show "int y ∈ {0::int..<int CARD('a)}"
using y by auto qed
finally show "y = nat (Rep (Abs' (int y)::'a))" by (metis nat_int)
qed
qed

lemma bij_to_nat: "bij_betw (to_nat) (UNIV::'a set) {0..<CARD('a)}"
using bij_betw_the_inv_into[OF bij_from_nat] unfolding to_nat_is_inv .

lemma finite_mod_type: "finite (UNIV::'a set)"
using finite_imageD[of "to_nat" "UNIV::'a set"] using bij_to_nat unfolding bij_betw_def by auto

subclass (in mod_type) finite by (intro_classes, rule finite_mod_type)

lemma least_0: "(LEAST n. n ∈ (UNIV::'a set)) = 0"
proof (rule Least_equality, auto)
fix y::"'a"
have "(0::'a) ≤ Abs (Rep y mod int CARD('a))" using strict_mono_Rep unfolding strict_mono_def
by (metis (opaque_lifting, mono_tags) Rep_0 Rep_ge_0 strict_mono_Rep strict_mono_less_eq)
also have "... = y" by (metis Rep_inverse Rep_mod)
finally show "(0::'a) ≤ y" .
qed

lemma add_to_nat_def: "x + y = from_nat (to_nat x + to_nat y)"
unfolding from_nat_def to_nat_def o_def using Rep_ge_0[of x] using Rep_ge_0[of y]
using Rep_less_n[of x] Rep_less_n[of y]
unfolding Abs'_def unfolding add_def[of x y] by auto

lemma to_nat_1: "to_nat 1 = 1"

shows "x + y = Abs' (Rep x + Rep y)" unfolding Abs'_def using add_def by simp

lemma Abs'_0:
shows "Abs' (CARD('a))=(0::'a)" by (metis (opaque_lifting, mono_tags) Abs'_def mod_self zero_def)

lemma Rep_plus_one_le_card:
assumes a: "a + 1 ≠ 0"
shows "(Rep a) + 1 < CARD ('a)"
proof (rule ccontr)
assume "¬ Rep a + 1 < CARD('a)" hence to_nat_eq_card: "Rep a + 1 = CARD('a)"
using Rep_less_n
have "a+1 = Abs' (Rep a + Rep (1::'a))" using add_def' by auto
also have "... = Abs' ((Rep a) + 1)" using Rep_1 by simp
also have "... = Abs' (CARD('a))" unfolding to_nat_eq_card ..
also have "... = 0" using Abs'_0 by auto
finally show False using a by contradiction
qed

lemma to_nat_plus_one_less_card: "∀a. a+1 ≠ 0 --> to_nat a + 1 < CARD('a)"
proof (clarify)
fix a
assume a: "a + 1 ≠ 0"
have "Rep a + 1 < int CARD('a)" using Rep_plus_one_le_card[OF a] by auto
hence "nat (Rep a + 1) < nat (int CARD('a))" unfolding zless_nat_conj using size0 by fast
thus "to_nat a + 1 < CARD('a)" unfolding to_nat_def o_def using nat_add_distrib[OF Rep_ge_0] by simp
qed

corollary to_nat_plus_one_less_card':
assumes "a+1 ≠ 0"
shows "to_nat a + 1 < CARD('a)" using to_nat_plus_one_less_card assms by simp

lemma strict_mono_to_nat: "strict_mono to_nat"
using strict_mono_Rep
unfolding strict_mono_def to_nat_def using Rep_ge_0 by (metis comp_apply nat_less_eq_zless)

lemma to_nat_eq [simp]: "to_nat x = to_nat y ⟷ x = y"
using injD [OF bij_betw_imp_inj_on[OF bij_to_nat]] by blast

lemma mod_type_forall_eq [simp]: "(∀j::'a. (to_nat j)<CARD('a) ⟶ P j) = (∀a. P a)"
proof (auto)
fix a assume a: "∀j. (to_nat::'a=>nat) j < CARD('a) ⟶ P j"
have "(to_nat::'a=>nat) a < CARD('a)" using bij_to_nat unfolding bij_betw_def by auto
thus "P a" using a by auto
qed

lemma to_nat_from_nat:
assumes t:"to_nat j = k"
shows "from_nat k = j"
proof -
have "from_nat k = from_nat (to_nat j)"  unfolding t ..
also have "... = from_nat (the_inv_into {0..<CARD('a)} (from_nat) j)" unfolding to_nat_is_inv ..
also have "... = j"
proof (rule f_the_inv_into_f)
show "inj_on from_nat {0..<CARD('a)}" by (metis bij_betw_imp_inj_on bij_from_nat)
show "j ∈ from_nat ` {0..<CARD('a)}" by (metis UNIV_I bij_betw_def bij_from_nat)
qed
finally show "from_nat k = j" .
qed

lemma to_nat_mono:
assumes ab: "a < b"
shows "to_nat a < to_nat b"
using strict_mono_to_nat unfolding strict_mono_def using assms by fast

lemma to_nat_mono':
assumes ab: "a ≤ b"
shows "to_nat a ≤ to_nat b"
proof (cases "a=b")
case True thus ?thesis by auto
next
case False
hence "a<b" using ab by simp
thus ?thesis using to_nat_mono by fastforce
qed

lemma least_mod_type:
shows "0 ≤ (n::'a)"
using least_0 by (metis (full_types) Least_le UNIV_I)

lemma to_nat_from_nat_id:
assumes x: "x<CARD('a)"
shows "to_nat ((from_nat x)::'a) = x"
unfolding to_nat_is_inv[symmetric] proof (rule the_inv_into_f_f)
show "inj_on (from_nat::nat=>'a) {0..<CARD('a)}" using bij_from_nat unfolding bij_betw_def by auto
show "x ∈ {0..<CARD('a)}" using x by simp
qed

lemma from_nat_to_nat_id[simp]:
shows "from_nat (to_nat x) = x" by (metis to_nat_from_nat)

lemma from_nat_to_nat:
assumes t:"from_nat j = k" and j: "j<CARD('a)"
shows "to_nat k = j" by (metis j t to_nat_from_nat_id)

lemma from_nat_mono:
assumes i_le_j: "i<j" and j: "j<CARD('a)"
shows "(from_nat i::'a) < from_nat j"
proof -
have i: "i<CARD('a)" using i_le_j j by simp
obtain a where a: "i=to_nat a"
using bij_to_nat unfolding bij_betw_def using i to_nat_from_nat_id by metis
obtain b where b: "j=to_nat b"
using bij_to_nat unfolding bij_betw_def using j to_nat_from_nat_id by metis
show ?thesis by (metis a b from_nat_to_nat_id i_le_j strict_mono_less strict_mono_to_nat)
qed

lemma from_nat_mono':
assumes i_le_j: "i ≤ j" and "j<CARD ('a)"
shows "(from_nat i::'a) ≤ from_nat j"
proof (cases "i=j")
case True
have "(from_nat i::'a) = from_nat j" using True by simp
thus ?thesis by simp
next
case False
hence "i<j" using i_le_j by simp
thus ?thesis by (metis assms(2) from_nat_mono less_imp_le)
qed

lemma to_nat_suc:
assumes "to_nat (x)+1 < CARD ('a)"
shows "to_nat (x + 1::'a) = (to_nat x) + 1"
proof -
have "(x::'a) + 1 = from_nat (to_nat x + to_nat (1::'a))" unfolding add_to_nat_def ..
hence "to_nat ((x::'a) + 1) = to_nat (from_nat (to_nat x + to_nat (1::'a))::'a)" by presburger
also have "... = to_nat (from_nat (to_nat x + 1)::'a)" unfolding to_nat_1 ..
also have "... = (to_nat x + 1)" by (metis assms to_nat_from_nat_id)
finally show ?thesis .
qed

lemma to_nat_le:
assumes "y < from_nat k"
shows  "to_nat y < k"
proof (cases "k<CARD('a)")
case True show ?thesis by (metis (full_types) True assms to_nat_from_nat_id to_nat_mono)
next
case False have "to_nat y < CARD ('a)" using bij_to_nat unfolding bij_betw_def by auto
thus ?thesis using False by auto
qed

lemma le_Suc:
assumes ab: "a < (b::'a)"
shows "a + 1 ≤ b"
proof -
have "a + 1 = (from_nat (to_nat (a + 1))::'a)" using from_nat_to_nat_id [of "a+1",symmetric] .
also have "... ≤ (from_nat (to_nat (b::'a))::'a)"
proof (rule from_nat_mono')
have "to_nat a < to_nat b" using ab by (metis to_nat_mono)
hence "to_nat a + 1 ≤ to_nat b" by simp
thus "to_nat b < CARD ('a)" using bij_to_nat unfolding  bij_betw_def by auto
hence "to_nat a + 1 < CARD ('a)" by (metis ‹to_nat a + 1 ≤ to_nat b› preorder_class.le_less_trans)
thus "to_nat (a + 1) ≤ to_nat b" by (metis ‹to_nat a + 1 ≤ to_nat b› to_nat_suc)
qed
also have "... = b" by (metis from_nat_to_nat_id)
finally show "a + (1::'a) ≤ b" .
qed

lemma le_Suc':
assumes ab: "a + 1 ≤ b"
and less_card: "(to_nat a) + 1 < CARD ('a)"
shows "a < b"
proof -
have "a = (from_nat (to_nat a)::'a)" using from_nat_to_nat_id [of "a",symmetric] .
also have "... < (from_nat (to_nat b)::'a)"
proof (rule from_nat_mono)
show "to_nat b < CARD('a)" using bij_to_nat unfolding  bij_betw_def by auto
have "to_nat (a + 1) ≤  to_nat b" using ab by (metis to_nat_mono')
hence "to_nat (a) + 1 ≤  to_nat b"  using to_nat_suc[OF less_card] by auto
thus "to_nat a < to_nat b" by simp
qed
finally show "a < b" by (metis to_nat_from_nat)
qed

lemma Suc_le:
assumes less_card: "(to_nat a) + 1 < CARD ('a)"
shows "a < a + 1"
proof -
have "(to_nat a) < (to_nat a) + 1" by simp
hence "(to_nat a) < to_nat (a + 1)" by (metis less_card to_nat_suc)
hence "(from_nat (to_nat a)::'a) < from_nat (to_nat (a + 1))"
by (rule from_nat_mono, metis less_card to_nat_suc)
thus "a < a + 1" by (metis to_nat_from_nat)
qed

lemma Suc_le':
fixes a::'a
assumes "a + 1 ≠ 0"
shows "a < a + 1" using Suc_le to_nat_plus_one_less_card assms by blast

lemma from_nat_not_eq:
assumes a_eq_to_nat: "a ≠ to_nat b"
and a_less_card: "a<CARD('a)"
shows "from_nat a ≠ b"
proof (rule ccontr)
assume "¬ from_nat a ≠ b" hence "from_nat a = b" by simp
hence "to_nat ((from_nat a)::'a) = to_nat b" by auto
thus False by (metis a_eq_to_nat a_less_card to_nat_from_nat_id)
qed

lemma Suc_less:
fixes i::'a
assumes "i<j"
and "i+1 ≠ j"
shows "i+1<j" by (metis assms le_Suc le_neq_trans)

lemma Greatest_is_minus_1: "∀a::'a. a ≤ -1"
proof (clarify)
fix a::'a
have zero_ge_card_1: "0 ≤ int CARD('a) - 1" using size1 by auto
have card_less: "int CARD('a) - 1 < int CARD('a)" by auto
have not_zero: "1 mod int CARD('a) ≠ 0"
by (metis (opaque_lifting, mono_tags) Rep_Abs_1 Rep_mod zero_neq_one)
have int_card: "int (CARD('a) - 1) = int CARD('a) - 1" using of_nat_diff[of 1 "CARD ('a)"]
using size1 by simp
have "a = Abs' (Rep a)" by (metis (opaque_lifting, mono_tags) Rep_0 add_0_right add_def'
also have "... = Abs' (int (nat (Rep a)))" by (metis Rep_ge_0 int_nat_eq)
also have "...  ≤ Abs' (int (CARD('a) - 1))"
proof (rule from_nat_mono'[unfolded from_nat_def o_def, of "nat (Rep a)" "CARD('a) - 1"])
show "nat (Rep a) ≤ CARD('a) - 1" using Rep_less_n
using int_card nat_le_iff by auto
show "CARD('a) - 1 < CARD('a)" using finite_UNIV_card_ge_0 finite_mod_type by fastforce
qed
also have "... = - 1"
unfolding Abs'_def unfolding minus_def zmod_zminus1_eq_if unfolding Rep_1
apply (rule cong [of Abs], rule refl)
unfolding if_not_P [OF not_zero]
unfolding int_card
unfolding mod_pos_pos_trivial[OF zero_ge_card_1 card_less]
using mod_pos_pos_trivial[OF _ size1] by presburger
finally show "a ≤ -1" by fastforce
qed

lemma a_eq_minus_1: "∀a::'a. a+1 = 0 ⟶ a = -1"

lemma forall_from_nat_rw:
shows "(∀x∈{0..<CARD('a)}. P (from_nat x::'a)) = (∀x. P (from_nat x))"
proof (auto)
fix y assume *: "∀x∈{0..<CARD('a)}. P (from_nat x)"
have "from_nat y ∈ (UNIV::'a set)" by auto
from this obtain x where x1: "from_nat y = (from_nat x::'a)" and x2: "x∈{0..<CARD('a)}"
using bij_from_nat unfolding bij_betw_def
by (metis from_nat_to_nat_id rangeI the_inv_into_onto to_nat_is_inv)
show "P (from_nat y::'a)" unfolding x1 using * x2 by simp
qed

lemma from_nat_eq_imp_eq:
assumes f_eq: "from_nat x = (from_nat xa::'a)"
and x: "x<CARD('a)" and xa: "xa<CARD('a)"
shows "x=xa" using assms from_nat_not_eq by metis

lemma to_nat_less_card:
fixes j::"'a"
shows "to_nat j < CARD ('a)"
using bij_to_nat unfolding bij_betw_def by auto

lemma from_nat_0: "from_nat 0 = 0"
unfolding from_nat_def o_def of_nat_0 Abs'_def mod_0 zero_def ..
lemma to_nat_0: "to_nat 0 = 0" unfolding to_nat_def o_def Rep_0 nat_0 ..
lemma to_nat_eq_0: "(to_nat x = 0) = (x = 0)"
by (auto simp add: to_nat_0 from_nat_0 dest: to_nat_from_nat)

lemma suc_not_zero:
assumes "to_nat a + 1 ≠ CARD('a)"
shows "a+1 ≠ 0"
proof (rule ccontr, simp)
assume a_plus_one_zero: "a + 1 = 0"
hence rep_eq_card: "Rep a + 1 = CARD('a)"
using assms to_nat_0 Suc_eq_plus1 Suc_lessI Zero_not_Suc to_nat_less_card to_nat_suc
by (metis (opaque_lifting, mono_tags))
moreover have "Rep a + 1 < CARD('a)"
using Abs'_0 Rep_1 Suc_eq_plus1 Suc_lessI Suc_neq_Zero add_def' assms
rep_eq_card to_nat_0 to_nat_less_card to_nat_suc by (metis (opaque_lifting, mono_tags))
ultimately show False by fastforce
qed

lemma from_nat_suc:
shows "from_nat (j + 1) = from_nat j + 1"
unfolding from_nat_def o_def Abs'_def add_def' Rep_1 Rep_Abs_mod

lemma to_nat_plus_1_set:
shows "to_nat a + 1 ∈ {1..<CARD('a)+1}"
using to_nat_less_card by simp

end

lemma from_nat_CARD:
shows "from_nat (CARD('a)) = (0::'a::{mod_type})"
unfolding from_nat_def o_def Abs'_def by (simp add: zero_def)

subsection‹Instantiations›

instantiation bit0 and bit1:: (finite) mod_type
begin

definition "(Rep::'a bit0 => int)  x = Rep_bit0 x"
definition "(Abs::int => 'a bit0) x = Abs_bit0' x"

definition "(Rep::'a bit1 => int)  x = Rep_bit1 x"
definition "(Abs::int => 'a bit1) x = Abs_bit1' x"

instance
proof
show "(0::'a bit0) = Abs (0::int)" unfolding Abs_bit0_def Abs_bit0'_def zero_bit0_def by auto
show "(1::int) < int CARD('a bit0)" by (metis bit0.size1)
show "type_definition (Rep::'a bit0 => int) (Abs:: int => 'a bit0) {0::int..<int CARD('a bit0)}"
proof (unfold type_definition_def Rep_bit0_def [abs_def]
Abs_bit0_def [abs_def] Abs_bit0'_def, intro conjI)
show "∀x::'a bit0. Rep_bit0 x ∈ {0::int..<int CARD('a bit0)}"
unfolding card_bit0 unfolding of_nat_mult
using Rep_bit0 [where ?'a = "'a"] by simp
show "∀x::'a bit0. Abs_bit0 (Rep_bit0 x mod int CARD('a bit0)) = x"
by (metis Rep_bit0_inverse bit0.Rep_mod)
show "∀y::int. y ∈ {0::int..<int CARD('a bit0)}
⟶ Rep_bit0 ((Abs_bit0::int => 'a bit0) (y mod int CARD('a bit0))) = y"
by (metis bit0.Abs_inverse bit0.Rep_mod)
qed
show "(1::'a bit0) = Abs (1::int)" unfolding Abs_bit0_def Abs_bit0'_def one_bit0_def
by (metis bit0.of_nat_eq of_nat_1 one_bit0_def)
fix x y :: "'a bit0"
show "x + y = Abs ((Rep x + Rep y) mod int CARD('a bit0))"
unfolding Abs_bit0_def Rep_bit0_def plus_bit0_def Abs_bit0'_def by fastforce
show "x * y = Abs (Rep x * Rep y mod int CARD('a bit0))"
unfolding Abs_bit0_def Rep_bit0_def times_bit0_def Abs_bit0'_def by fastforce
show "x - y = Abs ((Rep x - Rep y) mod int CARD('a bit0))"
unfolding Abs_bit0_def Rep_bit0_def minus_bit0_def Abs_bit0'_def by fastforce
show "- x = Abs (- Rep x mod int CARD('a bit0))"
unfolding Abs_bit0_def Rep_bit0_def uminus_bit0_def Abs_bit0'_def by fastforce
show "(0::'a bit1) = Abs (0::int)" unfolding Abs_bit1_def Abs_bit1'_def zero_bit1_def by auto
show "(1::int) < int CARD('a bit1)" by (metis bit1.size1)
show "(1::'a bit1) = Abs (1::int)" unfolding Abs_bit1_def Abs_bit1'_def one_bit1_def
by (metis bit1.of_nat_eq of_nat_1 one_bit1_def)
fix x y :: "'a bit1"
show "x + y = Abs ((Rep x + Rep y) mod int CARD('a bit1))"
unfolding Abs_bit1_def Abs_bit1'_def Rep_bit1_def plus_bit1_def by fastforce
show "x * y = Abs (Rep x * Rep y mod int CARD('a bit1))"
unfolding Abs_bit1_def Rep_bit1_def times_bit1_def Abs_bit1'_def by fastforce
show "x - y = Abs ((Rep x - Rep y) mod int CARD('a bit1))"
unfolding Abs_bit1_def Rep_bit1_def minus_bit1_def Abs_bit1'_def by fastforce
show "- x = Abs (- Rep x mod int CARD('a bit1))"
unfolding Abs_bit1_def Rep_bit1_def uminus_bit1_def Abs_bit1'_def by fastforce
show "type_definition (Rep::'a bit1 => int) (Abs:: int => 'a bit1) {0::int..<int CARD('a bit1)}"
proof (unfold type_definition_def Rep_bit1_def [abs_def]
Abs_bit1_def [abs_def] Abs_bit1'_def, intro conjI)
have int_2: "int 2 = 2" by auto
show "∀x::'a bit1. Rep_bit1 x ∈ {0::int..<int CARD('a bit1)}"
unfolding card_bit1
unfolding of_nat_Suc of_nat_mult
using Rep_bit1 [where ?'a = "'a"]
unfolding int_2 ..
show "∀x::'a bit1. Abs_bit1 (Rep_bit1 x mod int CARD('a bit1)) = x"
by (metis Rep_bit1_inverse bit1.Rep_mod)
show "∀y::int. y ∈ {0::int..<int CARD('a bit1)}
⟶ Rep_bit1 ((Abs_bit1::int => 'a bit1) (y mod int CARD('a bit1))) = y"
by (metis bit1.Abs_inverse bit1.Rep_mod)
qed
show "strict_mono (Rep::'a bit0 => int)" unfolding strict_mono_def
by (metis Rep_bit0_def less_bit0_def)
show "strict_mono (Rep::'a bit1 => int)" unfolding strict_mono_def
by (metis Rep_bit1_def less_bit1_def)
qed
end

end
```