Я попытался решить проблему и предложил несколько силовой метод ее решения:
context
fixes c d :: real
assumes "c ≠ 0" "∃b. c = b^2" "∃b'. d = b'^2"
begin
definition t where "t = sqrt(d/c)"
definition e' where "e' x y = x^2 + y^2 - 1 - t^2 * x^2 * y^2"
context
assumes nz_t: "t ≠ 0"
begin
definition ρ :: "real × real ⇒ real × real" where
"ρ z = (-snd z, fst z)"
definition τ :: "real × real ⇒ real × real" where
"τ z = (1/(t*fst z), 1/(t*snd z))"
definition S where
"S ≡
{
id,
(λz. (-snd z, fst z)),
(λz. (-fst z, -snd z)),
(λz. (snd z, -fst z)),
(λz. (1/(t*fst z), 1/(t*snd z))),
(λz. (-1/(t*snd z), 1/(t*fst z))),
(λz. (-1/(t*fst z), -1/(t*snd z))),
(λz. (1/(t*snd z), -1/(t*fst z)))
}"
definition ρS where
"ρS ≡
{id, (λz. (-snd z, fst z)), (λz. (-fst z, -snd z)), (λz. (snd z, -fst z))}"
definition τS where
"τS ≡ {id, (λz. (1/(t*fst z), 1/(t*snd z)))}"
definition BIJ where "BIJ = ⦇carrier = {f. bij f}, mult = comp, one = id⦈"
interpretation bij: group BIJ
unfolding BIJ_def
apply unfold_locales
subgoal by (simp add: bij_comp)
subgoal by (simp add: comp_assoc)
subgoal by simp
subgoal by simp
subgoal by simp
subgoal
unfolding Units_def
by clarsimp
(metis inj_iff bij_betw_def bij_betw_inv_into inv_o_cancel surj_iff)
done
(*the proof may take quite a few seconds*)
lemma comp_S: "x ∈ S ⟹ y ∈ S ⟹ x ∘ y ∈ S"
unfolding comp_apply S_def Set.insert_iff by (elim disjE) fastforce+
lemma comm_S: "x ∈ S ⟹ y ∈ S ⟹ x ∘ y = y ∘ x"
unfolding comp_apply S_def Set.insert_iff by (elim disjE) fastforce+
lemma bij_ρ: "bij ρ"
unfolding bij_def inj_def surj_def ρ_def
by clarsimp (metis add.inverse_inverse)
lemma bij_τ: "bij τ"
unfolding bij_def inj_def surj_def τ_def
proof(simp add: nz_t, intro allI, intro exI)
fix a show "a = 1 / (t * (1/(a*t)))" using nz_t by simp
qed
lemma generate_ρτ: "generate BIJ {ρ, τ} = S"
proof(standard; intro subsetI)
have inv_τ: "inv⇘BIJ⇙ τ = τ"
unfolding m_inv_def
proof(standard)
show "τ ∈ carrier BIJ ∧ τ ⊗⇘BIJ⇙ τ = ?⇘BIJ⇙ ∧ τ ⊗⇘BIJ⇙ τ = ?⇘BIJ⇙"
unfolding BIJ_def apply(intro conjI)
subgoal using bij_τ by simp
subgoal unfolding τ_def using nz_t by auto
subgoal unfolding τ_def using nz_t by auto
done
then show
"y ∈ carrier BIJ ∧ τ ⊗⇘BIJ⇙ y = ?⇘BIJ⇙ ∧ y ⊗⇘BIJ⇙ τ = ?⇘BIJ⇙ ⟹ y = τ"
for y
unfolding BIJ_def by (auto intro: left_right_inverse_eq)
qed
define ρ' :: "real × real ⇒ real × real" where "ρ' = (λz. (snd z, -fst z))"
have bij_ρ': "bij ρ'"
unfolding bij_def inj_def surj_def ρ'_def
by simp (metis add.inverse_inverse)
have inv_ρ: "inv⇘BIJ⇙ ρ = ρ'"
unfolding m_inv_def
proof(standard)
show "ρ' ∈ carrier BIJ ∧ ρ ⊗⇘BIJ⇙ ρ' = ?⇘BIJ⇙ ∧ ρ' ⊗⇘BIJ⇙ ρ = ?⇘BIJ⇙"
unfolding BIJ_def apply(intro conjI)
subgoal using bij_ρ' by auto
subgoal unfolding ρ_def ρ'_def by auto
subgoal unfolding ρ_def ρ'_def by auto
done
then show
"y ∈ carrier BIJ ∧ ρ ⊗⇘BIJ⇙ y = ?⇘BIJ⇙ ∧ y ⊗⇘BIJ⇙ ρ = ?⇘BIJ⇙ ⟹ y = ρ'"
for y
unfolding BIJ_def by (auto intro: left_right_inverse_eq)
qed
have ττ: "τ ⊗⇘BIJ⇙ τ = ?⇘BIJ⇙"
unfolding BIJ_def τ_def comp_def by (auto simp: nz_t)
show "x ∈ generate BIJ {ρ, τ} ⟹ x ∈ S" for x
apply(induction rule: generate.induct)
subgoal unfolding BIJ_def S_def by auto
subgoal unfolding BIJ_def S_def ρ_def τ_def by auto
subgoal
unfolding Set.insert_iff apply(elim disjE)
subgoal using inv_ρ unfolding BIJ_def S_def ρ_def ρ'_def by simp
subgoal using inv_τ unfolding BIJ_def S_def τ_def by simp
subgoal by simp
done
subgoal unfolding BIJ_def by (metis monoid.select_convs(1) comp_S)
done
show "x ∈ S ⟹ x ∈ generate BIJ {ρ, τ}" for x
unfolding S_def Set.insert_iff
proof(elim disjE; clarsimp)
show "id ∈ generate BIJ {ρ, τ}"
unfolding BIJ_def using generate.simps by fastforce
show ρ_gen: "(λz. (- snd z, fst z)) ∈ generate BIJ {ρ, τ}"
by (fold ρ_def, rule generate.simps[THEN iffD2]) simp
show τ_gen: "(λz. (1 / (t * fst z), 1 / (t * snd z))) ∈ generate BIJ {ρ, τ}"
by (fold τ_def) (simp add: generate.incl)
from inv_ρ show inv_ρ_gen: "(λz. (snd z, - fst z)) ∈ generate BIJ {ρ, τ}"
by (fold ρ'_def) (auto simp: generate.inv insertI1)
show ρρ_gen: "(λz. (- fst z, - snd z)) ∈ generate BIJ {ρ, τ}"
proof-
have ρρ: "(λz. (- fst z, - snd z)) = ρ ⊗⇘BIJ⇙ ρ"
unfolding ρ_def BIJ_def by auto
show ?thesis
apply(rule generate.simps[THEN iffD2])
using ρρ ρ_gen[folded ρ_def] by auto
qed
show "(λz. (- (1 / (t * snd z)), 1 / (t * fst z))) ∈ generate BIJ {ρ, τ}"
proof-
have ρτ: "(λz. (- (1 / (t * snd z)), 1 / (t * fst z))) = ρ ⊗⇘BIJ⇙ τ"
unfolding ρ_def τ_def BIJ_def by auto
show ?thesis
apply(rule generate.simps[THEN iffD2])
using ρτ ρ_gen[folded ρ_def] τ_gen[folded τ_def] by auto
qed
show
"(λz. (- (1 / (t * fst z)), - (1 / (t * snd z)))) ∈ generate BIJ {ρ, τ}"
proof-
have ρρτ:
"(λz. (- (1 / (t * fst z)), - (1 / (t * snd z)))) =
(λz. (- fst z, - snd z)) ⊗⇘BIJ⇙ τ"
unfolding τ_def BIJ_def by auto
show ?thesis
apply(rule generate.simps[THEN iffD2])
using ρρτ ρρ_gen τ_gen[folded τ_def] by auto
qed
show "(λz. (1 / (t * snd z), - (1 / (t * fst z)))) ∈ generate BIJ {ρ, τ}"
proof-
have inv_ρ_τ:
"(λz. (1 / (t * snd z), - (1 / (t * fst z)))) =
(λz. (snd z, - fst z)) ⊗⇘BIJ⇙ τ"
unfolding τ_def BIJ_def by auto
show ?thesis
apply(rule generate.simps[THEN iffD2])
using inv_ρ_τ inv_ρ_gen τ_gen[folded τ_def] by auto
qed
qed
qed
lemma "comm_group (BIJ⦇carrier := (generate BIJ {ρ, τ})⦈)"
proof-
have ρτ_ss_BIJ: "{ρ, τ} ⊆ carrier BIJ"
using bij_ρ bij_τ unfolding BIJ_def by simp
interpret ρτ_sg: subgroup "(generate BIJ {ρ, τ})" BIJ
using ρτ_ss_BIJ by (rule bij.generate_is_subgroup)
interpret ρτ_g: group "BIJ⦇carrier := (generate BIJ {ρ, τ})⦈"
by (rule ρτ_sg.subgroup_is_group[OF bij.group_axioms])
have car_S: "carrier (BIJ⦇carrier := S⦈) = S" by simp
have BIJ_comp: "x ⊗⇘BIJ⦇carrier := S⦈⇙ y = x ∘ y" for x y
unfolding BIJ_def by auto
from ρτ_g.group_comm_groupI[
unfolded generate_ρτ car_S BIJ_comp, OF comm_S, simplified
]
show ?thesis unfolding generate_ρτ by assumption
qed
lemma id_pair_def: "(λx. x) = (λz. (fst z, snd z))" by simp
lemma distinct_single: "distinct [x] = True" by simp
lemma ne_ff'_gg'_imp_ne_fgf'g':
assumes "f ≠ f' ∨ g ≠ g'"
shows
"(λz. (f (fst z) (snd z), g (fst z) (snd z))) ≠
(λz. (f' (fst z) (snd z), g' (fst z) (snd z)))"
using assms
proof(rule disjE)
assume "f ≠ f'"
then obtain x y where "f x y ≠ f' x y" by blast
then show ?thesis by (metis (hide_lams) fst_eqD snd_eqD)
next
assume "g ≠ g'"
then obtain x y where "g x y ≠ g' x y" by blast
then show ?thesis by (metis (hide_lams) fst_eqD snd_eqD)
qed
lemma id_ne_hyp: "(λa. a) ≠ (λa. 1/(t*a))"
proof(rule ccontr, simp)
assume id_eq_hyp: "(λa. a) = (λa. 1/(t*a))"
{
fix a :: real assume "a > 0"
define b where "b = sqrt(a)"
from ‹a > 0› have "a = b*b" and "b > 0" unfolding b_def by auto
from id_eq_hyp have "b = 1/(t*b)" by metis
with ‹b > 0› have "b div b =(1/(t*b)) div b" by simp
with ‹b > 0› have "1 = (1/(t*a))" unfolding ‹a = b*b› by simp
with ‹a > 0› nz_t have "t*a = 1" by simp
}
note ta_eq_one = this
define t2 where "t2 = (if t > 0 then 2/t else -2/t)"
with nz_t have "t2 > 0" unfolding t2_def by auto
from nz_t have "t*t2 = 2 ∨ t*t2 = -2" unfolding t2_def by auto
from ta_eq_one ‹t2 > 0› this show False by auto
qed
lemma id_ne_mhyp: "(λa. a) ≠ (λa. -1/(t*a))"
proof(rule ccontr, simp)
assume id_eq_hyp: "(λa. a) = (λa. -(1/(t*a)))"
{
fix a :: real assume "a > 0"
define b where "b = sqrt(a)"
from ‹a > 0› have "a = b*b" and "b > 0" unfolding b_def by auto
from id_eq_hyp have "b = -(1/(t*b))" by metis
with ‹b > 0› have "b div b =-1/(t*b) div b" by simp
with ‹b > 0› have "1 = -1/(t*a)" unfolding ‹a = b*b› by simp
with ‹a > 0› nz_t have "t*a = -1" by (metis divide_eq_1_iff)
}
note ta_eq_one = this
define t2 where "t2 = (if t > 0 then 2/t else -2/t)"
with nz_t have "t2 > 0" unfolding t2_def by auto
from nz_t have "t*t2 = 2 ∨ t*t2 = -2" unfolding t2_def by auto
from ta_eq_one ‹t2 > 0› this show False by auto
qed
lemma mid_ne_hyp: "(λa. -a) ≠ (λa. 1 / (t*a))"
using id_ne_mhyp by (metis minus_divide_left minus_equation_iff)
lemma mid_ne_mhyp: "(λa. -a) ≠ (λa. -1 / (t*a))"
using id_ne_hyp by (metis divide_minus_left minus_equation_iff)
lemma hyp_neq_hyp_1: "(λa. - 1/(t*a)) ≠ (λa. 1/(t*a))"
using nz_t
by (metis divide_cancel_right id_ne_mhyp mult_cancel_right1 mult_left_cancel
one_neq_neg_one)
lemma distinct:
"distinct
[
id,
(λz. (-snd z, fst z)),
(λz. (-fst z, -snd z)),
(λz. (snd z, -fst z)),
(λz. (1/(t*fst z), 1/(t*snd z))),
(λz. (-1/(t*snd z), 1/(t*fst z))),
(λz. (-1/(t*fst z), -1/(t*snd z))),
(λz. (1/(t*snd z), -1/(t*fst z)))
]"
apply(unfold distinct_length_2_or_more)+
unfolding
distinct_length_2_or_more
distinct_single
id_def id_pair_def
HOL.simp_thms(21)
by
(intro conjI)
(
rule ne_ff'_gg'_imp_ne_fgf'g',
metis one_neq_neg_one id_ne_hyp id_ne_mhyp
mid_ne_hyp mid_ne_mhyp hyp_neq_hyp_1
)+
lemma "card S = 8"
using distinct unfolding S_def using card_empty card_insert_disjoint by auto
end
end
Примечания
- Я полагался на
sledgehammer для многих частей доказательств, и есть некоторое ненужное дублирование кода. Поэтому, как и большинство моих ответов по SO, этот ответ далек от совершенства с точки зрения стиля кодирования.
- Мне было бы интересно узнать, существует ли лучший общий подход к решению. Так или иначе, я пришел к выводу, что большинство более вдумчивых подходов (например, использование теорем о циклических группах для определения порядка
ρ и τ и затем использование |HK|=|H||K|/|H∩K| для определения порядка G) потребует доказательства целый ряд дополнительных теорем для HOL-Algebra, но я не проверял AFP, прежде чем сделать это замечание, и я не использую HOL-Algebra на регулярной основе. Поэтому я, возможно, что-то упустил.