Theory Algebra_Towers_Examples
theory Algebra_Towers_Examples
imports
Algebra_Norm
"HOL-Computational_Algebra.Primes"
begin
section ‹Examples›
subsection ‹Finite-field towers›
datatype gf4 = GF4 bool bool
instantiation gf4 :: field
begin
definition zero_gf4 :: gf4
where "zero_gf4 = GF4 False False"
definition one_gf4 :: gf4
where "one_gf4 = GF4 True False"
fun plus_gf4 :: "gf4 ⇒ gf4 ⇒ gf4"
where "plus_gf4 (GF4 a b) (GF4 c d) =
GF4 (a ≠ c) (b ≠ d)"
fun uminus_gf4 :: "gf4 ⇒ gf4"
where "uminus_gf4 (GF4 a b) = GF4 a b"
definition minus_gf4 :: "gf4 ⇒ gf4 ⇒ gf4"
where "minus_gf4 x y = x + y"
fun times_gf4 :: "gf4 ⇒ gf4 ⇒ gf4"
where "times_gf4 (GF4 a b) (GF4 c d) =
GF4 ((a ∧ c) ≠ (b ∧ d))
(((a ∧ d) ≠ (b ∧ c)) ≠ (b ∧ d))"
fun inverse_gf4 :: "gf4 ⇒ gf4"
where
"inverse_gf4 (GF4 False False) = GF4 False False"
| "inverse_gf4 (GF4 True False) = GF4 True False"
| "inverse_gf4 (GF4 False True) = GF4 True True"
| "inverse_gf4 (GF4 True True) = GF4 False True"
definition divide_gf4 :: "gf4 ⇒ gf4 ⇒ gf4"
where "divide_gf4 x y = x * inverse y"
lemma inverse_times_gf4:
assumes "x ≠ (0 :: gf4)"
shows "inverse x * x = 1"
proof (cases x)
case (GF4 a b)
then show ?thesis
using assms
by (cases a; cases b;
simp add: zero_gf4_def one_gf4_def)
qed
instance
apply standard
subgoal for a b c
by (cases a; cases b; cases c; auto)
subgoal for a b
by (cases a; cases b; auto)
subgoal for a
by (cases a; auto simp: one_gf4_def)
subgoal for a b c
by (cases a; cases b; cases c; auto)
subgoal for a b
by (cases a; cases b; auto)
subgoal for a
by (cases a; auto simp: zero_gf4_def)
subgoal for a
by (cases a; auto simp: zero_gf4_def)
subgoal for a b
by (cases a; cases b; auto simp: minus_gf4_def)
subgoal for a b c
by (cases a; cases b; cases c; auto)
apply (simp_all add: inverse_times_gf4 divide_gf4_def
zero_gf4_def one_gf4_def)
done
end
instance gf4 :: finite_field
proof
show "finite (UNIV :: gf4 set)"
proof (rule finite_subset)
show "finite
{GF4 False False, GF4 True False, GF4 False True, GF4 True True}"
by simp
show "UNIV ⊆
{GF4 False False, GF4 True False, GF4 False True, GF4 True True}"
proof
fix x :: gf4
assume "x ∈ UNIV"
obtain a b where "x = GF4 a b"
by (cases x) simp
show "x ∈
{GF4 False False, GF4 True False, GF4 False True, GF4 True True}"
using ‹x = GF4 a b›
by (cases a; cases b; simp)
qed
qed
qed
locale finite_field_tower_example =
indexed_field_algebra_tower rS sA rA lower_basis upper_basis
for rS :: "'r::finite_field ⇒ 's::finite_field ⇒ 's"
and sA :: "'s ⇒ 'a::finite_field ⇒ 'a"
and rA :: "'r ⇒ 'a ⇒ 'a"
and lower_basis :: "'i::finite ⇒ 's"
and upper_basis :: "'j::finite ⇒ 'a"
begin
sublocale dimensions: indexed_field_tower
rS sA rA lower_basis upper_basis
by unfold_locales
theorem finite_field_tower_dimension:
"dimensions.direct_space.dim UNIV =
dimensions.lower_space.dim UNIV *
dimensions.upper_space.dim UNIV"
by (rule dimensions.finrank_tower)
theorem finite_field_tower_trace:
"tower_algebra.algebra_trace a =
lower_algebra.algebra_trace (upper_algebra.algebra_trace a)"
by (rule algebra_trace_trans)
theorem finite_field_tower_norm:
"tower_algebra.algebra_norm a =
lower_algebra.algebra_norm (upper_algebra.algebra_norm a)"
by (rule algebra_norm_trans)
end
text ‹
The preceding locale covers arbitrary nested finite fields without imposing a
separability assumption. The next example supplies a concrete nontrivial
extension: the four-element field is represented as
\<^term>‹GF4 a b›, corresponding to \(a+b\alpha\) over
\(\mathbb F_2\), with \(\alpha^2=\alpha+1\).
›
subsection ‹The four-element field over \(\mathbb F_2\)›
lemma gf2_cases [case_names zero one]:
fixes r :: gf2
obtains "r = 0" | "r = 1"
by transfer auto
lemma gf2_one_add_one [simp]:
"(1 :: gf2) + 1 = 0"
by transfer simp
lemma gf2_two [simp]:
"(2 :: gf2) = 0"
using gf2_one_add_one
by (simp only: one_add_one)
definition gf2_gf4_embed :: "gf2 ⇒ gf4"
where "gf2_gf4_embed r = (if r = 0 then 0 else 1)"
definition gf2_gf4_scale :: "gf2 ⇒ gf4 ⇒ gf4"
where "gf2_gf4_scale r x = gf2_gf4_embed r * x"
definition gf4_self_scale :: "gf4 ⇒ gf4 ⇒ gf4"
where "gf4_self_scale r x = r * x"
lemma gf2_gf4_embed_zero [simp]:
"gf2_gf4_embed 0 = 0"
by (simp add: gf2_gf4_embed_def)
lemma gf2_gf4_embed_one [simp]:
"gf2_gf4_embed 1 = 1"
by (simp add: gf2_gf4_embed_def)
lemma gf2_gf4_embed_add [simp]:
"gf2_gf4_embed (r + s) =
gf2_gf4_embed r + gf2_gf4_embed s"
by (cases r rule: gf2_cases; cases s rule: gf2_cases;
simp add: gf2_gf4_embed_def zero_gf4_def one_gf4_def)
lemma gf2_gf4_embed_mult [simp]:
"gf2_gf4_embed (r * s) =
gf2_gf4_embed r * gf2_gf4_embed s"
by (cases r rule: gf2_cases; cases s rule: gf2_cases;
simp add: gf2_gf4_embed_def)