Up to index of Isabelle/HOL/HOL-Multivariate_Analysis/Gauss-Jordan
theory Numeral_Type_Addendatheory Numeral_Type_Addenda
imports
"$ISABELLE_HOME/src/HOL/Library/Enum"
"$ISABELLE_HOME/src/HOL/Library/Numeral_Type"
"$ISABELLE_HOME/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space"
begin
(*
Title: Numeral_Type_Addenda.thy
Author: Jose Divasón <jose.divasonm at unirioja.es>
Author: Jesús Aransay <jesus-maria.aransay at unirioja.es>
*)
text{*Code equations for @{typ num1}:*}
lemma [code abstype]: "Abs_num1 (Rep_num1 v) = (v::num1)" by (metis Rep_num1_inverse)
lemma [code abstract]: "Rep_num1 (1) = ()" by simp
text{*Code equations for @{typ "'a::finite bit0"}:*}
lemma [code abstype]: "Abs_bit0 (Rep_bit0 a) = a" using bit0.Rep_inverse .
lemma [code abstract]: "Rep_bit0 0 = 0" unfolding bit0.Rep_0 ..
lemma [code abstract]: "Rep_bit0 1 = 1" unfolding bit0.Rep_1 ..
text{*If the underlying finite type has a computable cardinal, then the representation
of elements can be ``computed'' as follows:*}
lemma [code abstract]:
"Rep_bit0 (Abs_bit0' x :: 'a :: {finite, card_UNIV} bit0) = x mod int (CARD('a bit0))"
apply(simp add: Abs_bit0'_def)
apply(rule Abs_bit0_inverse)
apply simp
by (metis bit0.Rep_Abs_mod bit0.Rep_less_n card_bit0 of_nat_numeral zmult_int)
text{*Code equations for @{typ "'a::finite bit1"}:*}
lemma [code abstype]: "Abs_bit1 (Rep_bit1 a) = a" using bit1.Rep_inverse .
lemma [code abstract]: "Rep_bit1 0 = 0" unfolding bit1.Rep_0 ..
lemma [code abstract]: "Rep_bit1 1 = 1" unfolding bit1.Rep_1 ..
text{*If the underlying finite type has a computable cardinal, then the representation
of elements can be ``computed'' as follows:*}
lemma [code abstract]:
"Rep_bit1 (Abs_bit1' x :: 'a :: {finite, card_UNIV} bit1) = x mod int (CARD('a bit1))"
apply(simp add: Abs_bit1'_def)
apply(rule Abs_bit1_inverse)
apply simp
by (metis of_nat_0_less_iff of_nat_Suc of_nat_mult of_nat_numeral pos_mod_conj zero_less_Suc)
text{*The @{typ num1} is trivially an instance of the equal type class:*}
instantiation num1 :: equal
begin
definition equal_num1 :: "num1 => num1 => bool"
where "equal_num1 x y = True"
instance by (intro_classes, simp add: equal_num1_def num1_eq_iff)
end
text{*The numeral types @{typ "'a bit0"} and @{typ "'a bit1"} are instances
of the type class equal; would it be better to use @{const "Rep_bit0"} in the rhs,
instead of standard equality?:*}
instantiation
bit0 and bit1 :: (finite) equal
begin
definition equal_bit0 :: "'a bit0 => 'a bit0 => bool"
where "equal_bit0 x y = (x = y)"
definition equal_bit1 :: "'a bit1 => 'a bit1 => bool"
where "equal_bit1 x y = (x = y)"
instance
by (intro_classes, unfold equal_bit0_def equal_bit1_def)
(metis bit0.Rep_inverse, metis bit1.Rep_inverse)
end
text{*The previous definitions of @{thm equal_bit0_def} and @{thm equal_bit1_def} would make
the code generator loop; instead, we introduce the following ones:*}
lemma equal_bit0_code [code]:
"equal_class.equal x y = (Rep_bit0 x = Rep_bit0 y)"
by (simp add: equal_eq Rep_bit0_inject)
lemma equal_bit1_code [code]:
"equal_class.equal x y = (Rep_bit1 x = Rep_bit1 y)"
by (simp add: equal_eq Rep_bit1_inject)
lemma card_1 [simp]: "card {1::num1} = 1" by simp
text{*The definitions of @{thm equal_bit0_def} and @{thm equal_bit1_def} preserve
the equality of elements:*}
lemma "equal_class.equal (2::4) (6::4)"
using equal_bit0_def [of "2::4" 6] by auto
lemma "equal_class.equal (2::5) (7::5)"
using equal_bit1_def [of "2::5" 7] by auto
text{*The type @{typ "num0"} is an instance of the
classes @{text finite_UNIV} and @{text card_UNIV}, but with cardinal zero
so it is not finite itself:*}
instantiation num0 :: card_UNIV begin
definition "finite_UNIV = Phantom(num0) False"
definition "card_UNIV = Phantom(num0) 0"
instance apply (intro_classes, unfold finite_UNIV_num0_def card_UNIV_num0_def)
apply (metis (full_types) card_num0 finite_UNIV_card_ge_0 less_nat_zero_code)
by (metis (hide_lams, mono_tags) card_num0)
end
text{*The type @{typ "num1"} with a single element is an instance of the
classes @{text finite_UNIV} and @{text card_UNIV}, with cardinal
equal to one:*}
instantiation num1 :: card_UNIV begin
definition "finite_UNIV = Phantom(num1) True"
definition "card_UNIV = Phantom(num1) 1"
instance apply (intro_classes, unfold finite_UNIV_num1_def card_UNIV_num1_def)
by (metis (full_types) finite_code, metis card_num1)
end
text{*The two following lemmas are required to prove that @{typ "'a bit0"}
and @{typ "'a bit1"} are instances of @{text finite_UNIV}; under the assumption
of the underlying type @{typ "'a::finite"} of being finite, they are easy to prove;
otherwise, I do not know how to prove them; the premise about classes being
instance of finite then follows along the development:*}
lemma finite_bit0_UNIV_iff: "finite (UNIV::'a::finite set) <-> finite (UNIV::'a bit0 set)"
by (metis finite_class.finite_UNIV)
lemma finite_bit1_UNIV_iff: "finite (UNIV::'a::finite set) <-> finite (UNIV::'a bit1 set)"
by (metis finite_class.finite_UNIV)
text{*With the previous results, now we can prove that @{typ "'a::{finite,finite_UNIV} bit0"}
is an instance of the type class @{text "finite_UNIV"} and that @{typ "'a::{finite,card_UNIV} bit0"}
is an instance of the type class @{text "card_UNIV"}:*}
instantiation bit0 :: ("{finite,finite_UNIV}") finite_UNIV begin
definition "finite_UNIV = Phantom('a bit0) (of_phantom (finite_UNIV :: 'a finite_UNIV))"
instance
by (intro_classes, unfold finite_UNIV_bit0_def finite_UNIV_code [symmetric],
rule cong [of "Phantom('a bit0)"], rule refl) (rule finite_bit0_UNIV_iff)
end
instantiation bit0 :: ("{finite,card_UNIV}") card_UNIV begin
definition "card_UNIV = Phantom('a bit0) (2 * of_phantom (card_UNIV :: 'a card_UNIV))"
instance
by (intro_classes, unfold card_UNIV_bit0_def finite_UNIV_bit0_def card_UNIV_code [symmetric])
(rule cong [of "Phantom ('a bit0)"], rule refl, rule card_bit0 [symmetric])
end
text{*With the previous results, now we can prove that @{typ "'a::{finite,finite_UNIV} bit1"}
is an instance of the type class @{text "finite_UNIV"} and that @{typ "'a::{finite,card_UNIV} bit1"}
is an instance of the type class @{text "card_UNIV"}:*}
instantiation bit1 :: ("{finite,finite_UNIV}") finite_UNIV begin
definition "finite_UNIV = Phantom('a bit1) (of_phantom (finite_UNIV :: 'a finite_UNIV))"
instance by (intro_classes, unfold finite_UNIV_bit1_def finite_UNIV_code [symmetric],
rule cong [of "Phantom('a bit1)"], rule refl) (rule finite_bit1_UNIV_iff)
end
instantiation bit1 :: ("{finite,card_UNIV}") card_UNIV begin
definition "card_UNIV = Phantom('a bit1) (Suc (2 * of_phantom (card_UNIV :: 'a card_UNIV)))"
instance
by (intro_classes, unfold card_UNIV_bit1_def finite_UNIV_bit1_def card_UNIV_code [symmetric],
rule cong [of "Phantom ('a bit1)"], rule refl, rule card_bit1 [symmetric])
end
text{*Some other interesting instantiations that are missed in the Library:*}
instantiation bit0 and bit1 :: (finite) linorder begin
definition less_bit0 :: "'a bit0 => 'a bit0 => bool"
where "less_bit0 a b == (Rep_bit0 a) < (Rep_bit0 b)"
definition less_eq_bit0 :: "'a bit0 => 'a bit0 => bool"
where "less_eq_bit0 a b == (Rep_bit0 a) ≤ (Rep_bit0 b)"
definition less_bit1 :: "'a bit1 => 'a bit1 => bool"
where "less_bit1 a b == (Rep_bit1 a) < (Rep_bit1 b)"
definition less_eq_bit1 :: "'a bit1 => 'a bit1 => bool"
where "less_eq_bit1 a b == (Rep_bit1 a) ≤ (Rep_bit1 b)"
instance
by (intro_classes, unfold less_eq_bit0_def less_bit0_def,
unfold less_eq_bit1_def less_bit1_def, auto)
(metis bit0.Rep_inverse, metis bit1.Rep_inverse)
end
instantiation num1 :: enum begin
definition "(enum_class.enum::num1 list) = [1::1]"
definition "enum_class.enum_all (P::num1 => bool) = P 1"
definition "enum_class.enum_ex (P::num1 => bool) = P 1"
instance proof
show "(UNIV::num1 set) = set enum_class.enum"
unfolding enum_num1_def using num1_eq_iff by fastforce
show "distinct (enum_class.enum::num1 list)"
unfolding enum_num1_def using num1_eq_iff by fastforce
fix P::"1 => bool" show "enum_class.enum_all P = Ball UNIV P"
unfolding enum_all_num1_def unfolding enum_num1_def Ball_def
using num1_eq_iff by (auto)
show "enum_class.enum_ex P = Bex UNIV P"
unfolding enum_ex_num1_def enum_num1_def Ball_def
using num1_eq_iff by (auto)
qed
end
text{*We are now to prove that @{typ "'a bit0"} and @{typ "'a bit1"} are instances
of the type class enum; we must provide an enumeration of the universe of that types;
we first provide an explicit expression of such lists, by means of the following mappings:*}
definition create_list_bit0 :: "nat => ('b::{finite} bit0) list"
where "create_list_bit0 n = map ((Abs_bit0'::int => 'b::finite bit0) o int) (upt 0 n)"
definition create_list_bit1 :: "nat => ('b::{finite} bit1) list"
where "create_list_bit1 n = map ((Abs_bit1'::int => 'b::finite bit1) o int) (upt 0 n)"
text{*Some relevant properties of @{thm "create_list_bit0_def"}:*}
lemma create_list_bit0_0: "create_list_bit0 (0::nat) = []"
unfolding create_list_bit0_def by auto
lemma length_create_list_bit0: "length (create_list_bit0 (n)) = n"
unfolding create_list_bit0_def unfolding length_map by auto
text{*We have to prove that the elements inside of the lit are different of each other,
as long as the index @{term "n::nat"} is smaller than the cardinal of the
underlying type*}
lemma distinct_create_list_bit0:
assumes n: "n ≤ 2*CARD('a::finite)"
shows "distinct ((create_list_bit0 n)::'a bit0 list)"
proof (unfold create_list_bit0_def distinct_map inj_on_def, auto)
fix x y::nat assume x: "x < n" and y: "y < n"
and Abs_eq: "(Abs_bit0' (int x)::'a bit0) = Abs_bit0' (int y)"
have "Abs_bit0 (int y) = Abs_bit0 (int (y mod CARD ('a bit0)))" using mod_less y n by auto
also have "... = Abs_bit0 (int y mod int CARD('a bit0))" unfolding transfer_int_nat_functions(2) ..
also have "... = (Abs_bit0' (int y)::'a bit0)" using Abs_bit0'_def[of "int y", where ?'a='a] ..
also have "... = (Abs_bit0' (int x)::'a bit0)" using Abs_eq ..
also have "... = Abs_bit0 (int x mod int CARD('a bit0))"
using Abs_bit0'_def[of "int x", where ?'a='a] .
also have "... = Abs_bit0 (int (x mod CARD ('a bit0)))" unfolding transfer_int_nat_functions(2) ..
also have "... = Abs_bit0 (int (x))" using mod_less x n by auto
finally have Abs_eq': "(Abs_bit0 (int (y::nat))::'a bit0) = Abs_bit0 (int (x::nat))" by auto
have "((Abs_bit0 (int (y::nat))::'a bit0) = Abs_bit0 (int (x::nat))) = (int y = int x)"
proof (rule Abs_bit0_inject)
have "x ∈ {0..<(2 * CARD('a))}" using x n by auto
thus "int x ∈ {0::int..<(2::int) * int CARD('a)}" by auto
have "y ∈ {0..<(2 * CARD('a))}" using y n by auto
thus "int y ∈ {0::int..<(2::int) * int CARD('a)}" by auto
qed
thus "x=y" using Abs_eq' by simp
qed
corollary distinct_create_list_bit0':
assumes n: "n ≤ CARD('a::finite bit0)"
shows "distinct ((create_list_bit0 n)::'a bit0 list)"
by (rule distinct_create_list_bit0) (unfold card_bit0 [symmetric], rule n)
text{*Since all the elements in the list are different,
the set to which the list gives place has equal cardinal:*}
lemma card_create_list_bit0:
assumes n:"n ≤ 2* CARD ('a::finite)"
shows "card (set ((create_list_bit0 (n))::'a bit0 list)) = n"
using distinct_card[OF distinct_create_list_bit0[OF n]] unfolding length_create_list_bit0 .
corollary card_create_list_bit0':
assumes n: "n ≤ CARD ('a::finite bit0)"
shows "card (set ((create_list_bit0 n)::'a bit0 list)) = n"
by (rule card_create_list_bit0) (unfold card_bit0 [symmetric], rule n)
text{*Some relevant properties of @{thm "create_list_bit1_def"}*}
lemma create_list_bit1_0: "create_list_bit1 (0::nat) = []"
unfolding create_list_bit1_def by auto
lemma length_create_list_bit1: "length (create_list_bit1 (n)) = n"
unfolding create_list_bit1_def unfolding length_map by auto
lemma distinct_create_list_bit1:
assumes n: "n ≤ 1 + 2 * CARD('a::finite)"
shows "distinct ((create_list_bit1 (n))::'a bit1 list)"
proof (unfold create_list_bit1_def distinct_map inj_on_def, auto)
fix x y::nat assume x: "x < n" and y: "y < n"
and Abs_eq: "(Abs_bit1' (int x)::'a bit1) = Abs_bit1' (int y)"
have "(Abs_bit1 (int y)::'a bit1) = Abs_bit1 (int (y mod CARD ('a bit1)))"
using mod_less[of y "CARD ('a)"] using y n by auto
also have "... = Abs_bit1 (int y mod int CARD('a bit1))" unfolding transfer_int_nat_functions(2) ..
also have "... = (Abs_bit1' (int y)::'a bit1)" using Abs_bit1'_def[of "int y", where ?'a='a] ..
also have "... = (Abs_bit1' (int x)::'a bit1)" using Abs_eq ..
also have "... = Abs_bit1 (int x mod int CARD('a bit1))"
using Abs_bit1'_def[of "int x", where ?'a='a] .
also have "... = Abs_bit1 (int (x mod CARD ('a bit1)))" unfolding transfer_int_nat_functions(2) ..
also have "... = Abs_bit1 (int (x))" using mod_less x n by auto
finally have Abs_eq': "(Abs_bit1 (int (y::nat))::'a bit1) = Abs_bit1 (int (x::nat))" by auto
have "((Abs_bit1 (int (y::nat))::'a bit1) = Abs_bit1 (int (x::nat))) = (int y = int x)"
proof (rule Abs_bit1_inject)
have "x ∈ {0..< 1 + (2 * CARD('a))}" using x n by auto
thus "int x ∈ {0::int..<1 + (2::int) * int CARD('a)}" by auto
have "y ∈ {0..< 1 +(2 * CARD('a))}" using y n by auto
thus "int y ∈ {0::int..< 1 + (2::int) * int CARD('a)}" by auto
qed
thus "x=y" using Abs_eq' by simp
qed
corollary distinct_create_list_bit1':
assumes n: "n ≤ CARD('a::finite bit1)"
shows "distinct ((create_list_bit1 n)::'a bit1 list)"
by (rule distinct_create_list_bit1)
(unfold Suc_eq_plus1_left [symmetric], unfold card_bit1 [symmetric], rule n)
lemma card_create_list_bit1:
assumes n:"n ≤ 1 + 2 * CARD ('a::finite)"
shows "card (set ((create_list_bit1 (n))::'a bit1 list)) = n"
using distinct_card[OF distinct_create_list_bit1 [OF n]] unfolding length_create_list_bit1 .
corollary card_create_list_bit1':
assumes n: "n ≤ CARD ('a::finite bit1)"
shows "card (set ((create_list_bit1 n)::'a bit1 list)) = n"
by (rule card_create_list_bit1)
(unfold Suc_eq_plus1_left [symmetric], unfold card_bit1 [symmetric], rule n)
text{*The type constructors bit0 and bit1, over finite types,
are instances of type class enum; we make use of the previously defined functions
@{thm create_list_bit0_def} and @{thm create_list_bit1_def}:*}
instantiation bit0 :: (finite) enum
begin
definition "(enum_class.enum::'a bit0 list) = create_list_bit0 (CARD('a bit0))"
definition "enum_class.enum_all (P::'a bit0 => bool) = (filter P enum_class.enum = enum_class.enum)"
definition "enum_class.enum_ex (P::'a bit0 => bool) = (filter P enum_class.enum ≠ [])"
instance proof (default, unfold ball_UNIV bex_UNIV)
show univ_eq:"(UNIV::'a bit0 set) = set enum_class.enum"
proof (rule card_eq_UNIV_imp_eq_UNIV[symmetric])
show "finite (UNIV::'a bit0 set)" by (metis finite_class.finite_UNIV)
show "card (set (enum_class.enum::'a bit0 list)) = CARD('a bit0)"
unfolding enum_bit0_def using card_create_list_bit0 by auto
qed
show "distinct (enum_class.enum::'a bit0 list)"
unfolding enum_bit0_def by (metis distinct_create_list_bit0' order_refl)
fix P :: "'a bit0 => bool"
show "enum_class.enum_all P = All P"
unfolding enum_all_bit0_def
unfolding filter_id_conv unfolding univ_eq[symmetric] by simp
show "enum_class.enum_ex P = Ex P"
unfolding enum_ex_bit0_def
unfolding filter_empty_conv unfolding univ_eq[symmetric] by fast
qed
end
text{*The following restriction in the type class of the type @{typ "'a"} is necessary to
get code generation; not only the underlying type @{typ "'a"} has to be finite,
but also of the type class @{text "card_UNIV"}, which is the only one which knows
how to compute the cardinal of types; more explanations in the mail by Andreas Lochbihler:*}
lemmas enum_bit0_code [code] = enum_bit0_def [where ?'a="'a :: {finite, card_UNIV}"] (*new*)
instantiation bit1 :: (finite) enum begin
definition "(enum_class.enum::'a bit1 list) = create_list_bit1 (CARD('a bit1))"
definition "enum_class.enum_all (P::'a bit1 => bool) = (filter P enum_class.enum = enum_class.enum)"
definition "enum_class.enum_ex (P::'a bit1 => bool) = (filter P enum_class.enum ≠ [])"
instance proof (default, unfold ball_UNIV bex_UNIV)
show univ_eq: "(UNIV::'a bit1 set) = set enum_class.enum"
proof (rule card_eq_UNIV_imp_eq_UNIV[symmetric])
show "finite (UNIV::'a bit1 set)" by (metis finite)
show "card (set (enum_class.enum::'a bit1 list)) = CARD('a bit1)"
unfolding enum_bit1_def using card_create_list_bit1[of "2*CARD('a)+1", where ?'a='a] by simp
qed
show "distinct (enum_class.enum::'a bit1 list)"
unfolding enum_bit1_def by (metis distinct_create_list_bit1' le_refl)
fix P :: "'a bit1 => bool"
show "enum_class.enum_all P = All P"
unfolding enum_all_bit1_def univ_eq[symmetric] filter_id_conv by fast
show "enum_class.enum_ex P = Ex P"
unfolding enum_ex_bit1_def
unfolding filter_empty_conv unfolding univ_eq[symmetric] by simp
qed
end
instantiation vec :: (type, finite) equal
begin
definition equal_vec :: "('a, 'b::finite) vec => ('a, 'b::finite) vec => bool"
where "equal_vec x y = (∀i. x$i = y$i)"
instance
proof (intro_classes)
fix x y::"('a, 'b::finite) vec"
show "equal_class.equal x y = (x = y)" unfolding equal_vec_def using vec_eq_iff by auto
qed
end
text{*@{typ "'a bit0"} and @{typ "'a bit1"} are instances of the type class wellorder:*}
lemma (in preorder) tranclp_less: "op <⇧+⇧+ = op <"
by(auto simp add: fun_eq_iff intro: less_trans elim: tranclp.induct)
instance bit0 and bit1 :: (finite) wellorder
proof -
have "wf {(x :: 'a bit0, y). x < y}"
by(auto simp add: trancl_def tranclp_less intro!: finite_acyclic_wf acyclicI)
thus "OFCLASS('a bit0, wellorder_class)"
by(rule wf_wellorderI) intro_classes
next
have "wf {(x :: 'a bit1, y). x < y}"
by(auto simp add: trancl_def tranclp_less intro!: finite_acyclic_wf acyclicI)
thus "OFCLASS('a bit1, wellorder_class)"
by(rule wf_wellorderI) intro_classes
qed
text{*The following restriction in the type class of the type @{typ "'a"} is necessary to
get code generation; not only the underlying type @{typ "'a"} has to be finite,
but also of the type class @{text "card_UNIV"}, which is the only one which knows
how to compute the cardinal of types; more explanations in the mail by Andreas Lochbihler:*}
lemmas enum_bit1_code [code] = enum_bit1_def[where ?'a="'a :: {finite, card_UNIV}"] (*new*)
end