(* Title: HOL/Cardinals/Ordinal_Arithmetic.thy
Author: Dmitriy Traytel, TU Muenchen
Copyright 2014
Ordinal arithmetic.
*)
header {* Ordinal Arithmetic *}
theory Ordinal_Arithmetic
imports Constructions_on_Wellorders
begin
definition osum :: "'a rel \<Rightarrow> 'b rel \<Rightarrow> ('a + 'b) rel" (infixr "+o" 70)
where
"r +o r' = map_pair Inl Inl ` r \<union> map_pair Inr Inr ` r' \<union>
{(Inl a, Inr a') | a a' . a \<in> Field r \<and> a' \<in> Field r'}"
lemma Field_osum: "Field(r +o r') = Inl ` Field r \<union> Inr ` Field r'"
unfolding osum_def Field_def by auto
lemma osum_Refl:"\<lbrakk>Refl r; Refl r'\<rbrakk> \<Longrightarrow> Refl (r +o r')"
(*Need first unfold Field_osum, only then osum_def*)
unfolding refl_on_def Field_osum unfolding osum_def by blast
lemma osum_trans:
assumes TRANS: "trans r" and TRANS': "trans r'"
shows "trans (r +o r')"
proof(unfold trans_def, safe)
fix x y z assume *: "(x, y) \<in> r +o r'" "(y, z) \<in> r +o r'"
thus "(x, z) \<in> r +o r'"
proof (cases x y z rule: sum.exhaust[case_product sum.exhaust sum.exhaust])
case (Inl_Inl_Inl a b c)
with * have "(a,b) \<in> r" "(b,c) \<in> r" unfolding osum_def by auto
with TRANS have "(a,c) \<in> r" unfolding trans_def by blast
with Inl_Inl_Inl show ?thesis unfolding osum_def by auto
next
case (Inl_Inl_Inr a b c)
with * have "a \<in> Field r" "c \<in> Field r'" unfolding osum_def Field_def by auto
with Inl_Inl_Inr show ?thesis unfolding osum_def by auto
next
case (Inl_Inr_Inr a b c)
with * have "a \<in> Field r" "c \<in> Field r'" unfolding osum_def Field_def by auto
with Inl_Inr_Inr show ?thesis unfolding osum_def by auto
next
case (Inr_Inr_Inr a b c)
with * have "(a,b) \<in> r'" "(b,c) \<in> r'" unfolding osum_def by auto
with TRANS' have "(a,c) \<in> r'" unfolding trans_def by blast
with Inr_Inr_Inr show ?thesis unfolding osum_def by auto
qed (auto simp: osum_def)
qed
lemma osum_Preorder: "\<lbrakk>Preorder r; Preorder r'\<rbrakk> \<Longrightarrow> Preorder (r +o r')"
unfolding preorder_on_def using osum_Refl osum_trans by blast
lemma osum_antisym: "\<lbrakk>antisym r; antisym r'\<rbrakk> \<Longrightarrow> antisym (r +o r')"
unfolding antisym_def osum_def by auto
lemma osum_Partial_order: "\<lbrakk>Partial_order r; Partial_order r'\<rbrakk> \<Longrightarrow> Partial_order (r +o r')"
unfolding partial_order_on_def using osum_Preorder osum_antisym by blast
lemma osum_Total: "\<lbrakk>Total r; Total r'\<rbrakk> \<Longrightarrow> Total (r +o r')"
unfolding total_on_def Field_osum unfolding osum_def by blast
lemma osum_Linear_order: "\<lbrakk>Linear_order r; Linear_order r'\<rbrakk> \<Longrightarrow> Linear_order (r +o r')"
unfolding linear_order_on_def using osum_Partial_order osum_Total by blast
lemma osum_wf:
assumes WF: "wf r" and WF': "wf r'"
shows "wf (r +o r')"
unfolding wf_eq_minimal2 unfolding Field_osum
proof(intro allI impI, elim conjE)
fix A assume *: "A \<subseteq> Inl ` Field r \<union> Inr ` Field r'" and **: "A \<noteq> {}"
obtain B where B_def: "B = A Int Inl ` Field r" by blast
show "\<exists>a\<in>A. \<forall>a'\<in>A. (a', a) \<notin> r +o r'"
proof(cases "B = {}")
case False
hence "B \<noteq> {}" "B \<le> Inl ` Field r" using B_def by auto
hence "Inl -` B \<noteq> {}" "Inl -` B \<le> Field r" unfolding vimage_def by auto
then obtain a where 1: "a \<in> Inl -` B" and "\<forall>a1 \<in> Inl -` B. (a1, a) \<notin> r"
using WF unfolding wf_eq_minimal2 by metis
hence "\<forall>a1 \<in> A. (a1, Inl a) \<notin> r +o r'"
unfolding osum_def using B_def ** by (auto simp: vimage_def Field_def)
thus ?thesis using 1 unfolding B_def by auto
next
case True
hence 1: "A \<le> Inr ` Field r'" using * B_def by auto
with ** have "Inr -`A \<noteq> {}" "Inr -` A \<le> Field r'" unfolding vimage_def by auto
with ** obtain a' where 2: "a' \<in> Inr -` A" and "\<forall>a1' \<in> Inr -` A. (a1',a') \<notin> r'"
using WF' unfolding wf_eq_minimal2 by metis
hence "\<forall>a1' \<in> A. (a1', Inr a') \<notin> r +o r'"
unfolding osum_def using ** 1 by (auto simp: vimage_def Field_def)
thus ?thesis using 2 by blast
qed
qed
lemma osum_minus_Id:
assumes r: "Total r" "\<not> (r \<le> Id)" and r': "Total r'" "\<not> (r' \<le> Id)"
shows "(r +o r') - Id \<le> (r - Id) +o (r' - Id)"
unfolding osum_def Total_Id_Field[OF r] Total_Id_Field[OF r'] by auto
lemma osum_minus_Id1:
"r \<le> Id \<Longrightarrow> (r +o r') - Id \<le> (Inl ` Field r \<times> Inr ` Field r') \<union> (map_pair Inr Inr ` (r' - Id))"
unfolding osum_def by auto
lemma osum_minus_Id2:
"r' \<le> Id \<Longrightarrow> (r +o r') - Id \<le> (map_pair Inl Inl ` (r - Id)) \<union> (Inl ` Field r \<times> Inr ` Field r')"
unfolding osum_def by auto
lemma osum_wf_Id:
assumes TOT: "Total r" and TOT': "Total r'" and WF: "wf(r - Id)" and WF': "wf(r' - Id)"
shows "wf ((r +o r') - Id)"
proof(cases "r \<le> Id \<or> r' \<le> Id")
case False
thus ?thesis
using osum_minus_Id[of r r'] assms osum_wf[of "r - Id" "r' - Id"]
wf_subset[of "(r - Id) +o (r' - Id)" "(r +o r') - Id"] by auto
next
have 1: "wf (Inl ` Field r \<times> Inr ` Field r')" by (rule wf_Int_Times) auto
case True
thus ?thesis
proof (elim disjE)
assume "r \<subseteq> Id"
thus "wf ((r +o r') - Id)"
by (rule wf_subset[rotated, OF osum_minus_Id1 wf_Un[OF 1 wf_map_pair_image[OF WF']]]) auto
next
assume "r' \<subseteq> Id"
thus "wf ((r +o r') - Id)"
by (rule wf_subset[rotated, OF osum_minus_Id2 wf_Un[OF wf_map_pair_image[OF WF] 1]]) auto
qed
qed
lemma osum_Well_order:
assumes WELL: "Well_order r" and WELL': "Well_order r'"
shows "Well_order (r +o r')"
proof-
have "Total r \<and> Total r'" using WELL WELL' by (auto simp add: order_on_defs)
thus ?thesis using assms unfolding well_order_on_def
using osum_Linear_order osum_wf_Id by blast
qed
lemma osum_embedL:
assumes WELL: "Well_order r" and WELL': "Well_order r'"
shows "embed r (r +o r') Inl"
proof -
have 1: "Well_order (r +o r')" using assms by (auto simp add: osum_Well_order)
moreover
have "compat r (r +o r') Inl" unfolding compat_def osum_def by auto
moreover
have "ofilter (r +o r') (Inl ` Field r)"
unfolding wo_rel.ofilter_def[unfolded wo_rel_def, OF 1] Field_osum rel.under_def
unfolding osum_def Field_def by auto
ultimately show ?thesis using assms by (auto simp add: embed_iff_compat_inj_on_ofilter)
qed
corollary osum_ordLeqL:
assumes WELL: "Well_order r" and WELL': "Well_order r'"
shows "r \<le>o r +o r'"
using assms osum_embedL osum_Well_order unfolding ordLeq_def by blast
lemma dir_image_alt: "dir_image r f = map_pair f f ` r"
unfolding dir_image_def map_pair_def by auto
lemma map_pair_ordIso: "\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> map_pair f f ` r =o r"
unfolding dir_image_alt[symmetric] by (rule ordIso_symmetric[OF dir_image_ordIso])
definition oprod :: "'a rel \<Rightarrow> 'b rel \<Rightarrow> ('a \<times> 'b) rel" (infixr "*o" 80)
where "r *o r' = {((x1, y1), (x2, y2)).
(((y1, y2) \<in> r' - Id \<and> x1 \<in> Field r \<and> x2 \<in> Field r) \<or>
((y1, y2) \<in> Restr Id (Field r') \<and> (x1, x2) \<in> r))}"
lemma Field_oprod: "Field (r *o r') = Field r \<times> Field r'"
unfolding oprod_def Field_def by auto blast+
lemma oprod_Refl:"\<lbrakk>Refl r; Refl r'\<rbrakk> \<Longrightarrow> Refl (r *o r')"
unfolding refl_on_def Field_oprod unfolding oprod_def by auto
lemma oprod_trans:
assumes "trans r" "trans r'" "antisym r" "antisym r'"
shows "trans (r *o r')"
proof(unfold trans_def, safe)
fix x y z assume *: "(x, y) \<in> r *o r'" "(y, z) \<in> r *o r'"
thus "(x, z) \<in> r *o r'"
unfolding oprod_def
apply safe
apply (metis assms(2) transE)
apply (metis assms(2) transE)
apply (metis assms(2) transE)
apply (metis assms(4) antisymD)
apply (metis assms(4) antisymD)
apply (metis assms(2) transE)
apply (metis assms(4) antisymD)
apply (metis Field_def Range_iff Un_iff)
apply (metis Field_def Range_iff Un_iff)
apply (metis Field_def Range_iff Un_iff)
apply (metis Field_def Domain_iff Un_iff)
apply (metis Field_def Domain_iff Un_iff)
apply (metis Field_def Domain_iff Un_iff)
apply (metis assms(1) transE)
apply (metis assms(1) transE)
apply (metis assms(1) transE)
apply (metis assms(1) transE)
done
qed
lemma oprod_Preorder: "\<lbrakk>Preorder r; Preorder r'; antisym r; antisym r'\<rbrakk> \<Longrightarrow> Preorder (r *o r')"
unfolding preorder_on_def using oprod_Refl oprod_trans by blast
lemma oprod_antisym: "\<lbrakk>antisym r; antisym r'\<rbrakk> \<Longrightarrow> antisym (r *o r')"
unfolding antisym_def oprod_def by auto
lemma oprod_Partial_order: "\<lbrakk>Partial_order r; Partial_order r'\<rbrakk> \<Longrightarrow> Partial_order (r *o r')"
unfolding partial_order_on_def using oprod_Preorder oprod_antisym by blast
lemma oprod_Total: "\<lbrakk>Total r; Total r'\<rbrakk> \<Longrightarrow> Total (r *o r')"
unfolding total_on_def Field_oprod unfolding oprod_def by auto
lemma oprod_Linear_order: "\<lbrakk>Linear_order r; Linear_order r'\<rbrakk> \<Longrightarrow> Linear_order (r *o r')"
unfolding linear_order_on_def using oprod_Partial_order oprod_Total by blast
lemma oprod_wf:
assumes WF: "wf r" and WF': "wf r'"
shows "wf (r *o r')"
unfolding wf_eq_minimal2 unfolding Field_oprod
proof(intro allI impI, elim conjE)
fix A assume *: "A \<subseteq> Field r \<times> Field r'" and **: "A \<noteq> {}"
then obtain y where y: "y \<in> snd ` A" "\<forall>y'\<in>snd ` A. (y', y) \<notin> r'"
using spec[OF WF'[unfolded wf_eq_minimal2], of "snd ` A"] by auto
let ?A = "fst ` A \<inter> {x. (x, y) \<in> A}"
from * y have "?A \<noteq> {}" "?A \<subseteq> Field r" by auto
then obtain x where x: "x \<in> ?A" and "\<forall>x'\<in> ?A. (x', x) \<notin> r"
using spec[OF WF[unfolded wf_eq_minimal2], of "?A"] by auto
with y have "\<forall>a'\<in>A. (a', (x, y)) \<notin> r *o r'"
unfolding oprod_def mem_Collect_eq split_beta fst_conv snd_conv Id_def by auto
moreover from x have "(x, y) \<in> A" by auto
ultimately show "\<exists>a\<in>A. \<forall>a'\<in>A. (a', a) \<notin> r *o r'" by blast
qed
lemma oprod_minus_Id:
assumes r: "Total r" "\<not> (r \<le> Id)" and r': "Total r'" "\<not> (r' \<le> Id)"
shows "(r *o r') - Id \<le> (r - Id) *o (r' - Id)"
unfolding oprod_def Total_Id_Field[OF r] Total_Id_Field[OF r'] by auto
lemma oprod_minus_Id1:
"r \<le> Id \<Longrightarrow> r *o r' - Id \<le> {((x,y1), (x,y2)). x \<in> Field r \<and> (y1, y2) \<in> (r' - Id)}"
unfolding oprod_def by auto
lemma wf_extend_oprod1:
assumes "wf r"
shows "wf {((x,y1), (x,y2)) . x \<in> A \<and> (y1, y2) \<in> r}"
proof (unfold wf_eq_minimal2, intro allI impI, elim conjE)
fix B
assume *: "B \<subseteq> Field {((x,y1), (x,y2)) . x \<in> A \<and> (y1, y2) \<in> r}" and "B \<noteq> {}"
from image_mono[OF *, of snd] have "snd ` B \<subseteq> Field r" unfolding Field_def by force
with `B \<noteq> {}` obtain x where x: "x \<in> snd ` B" "\<forall>x'\<in>snd ` B. (x', x) \<notin> r"
using spec[OF assms[unfolded wf_eq_minimal2], of "snd ` B"] by auto
then obtain a where "(a, x) \<in> B" by auto
moreover
from * x have "\<forall>a'\<in>B. (a', (a, x)) \<notin> {((x,y1), (x,y2)) . x \<in> A \<and> (y1, y2) \<in> r}" by auto
ultimately show "\<exists>ax\<in>B. \<forall>a'\<in>B. (a', ax) \<notin> {((x,y1), (x,y2)) . x \<in> A \<and> (y1, y2) \<in> r}" by blast
qed
lemma oprod_minus_Id2:
"r' \<le> Id \<Longrightarrow> r *o r' - Id \<le> {((x1,y), (x2,y)). (x1, x2) \<in> (r - Id) \<and> y \<in> Field r'}"
unfolding oprod_def by auto
lemma wf_extend_oprod2:
assumes "wf r"
shows "wf {((x1,y), (x2,y)) . (x1, x2) \<in> r \<and> y \<in> A}"
proof (unfold wf_eq_minimal2, intro allI impI, elim conjE)
fix B
assume *: "B \<subseteq> Field {((x1, y), (x2, y)). (x1, x2) \<in> r \<and> y \<in> A}" and "B \<noteq> {}"
from image_mono[OF *, of fst] have "fst ` B \<subseteq> Field r" unfolding Field_def by force
with `B \<noteq> {}` obtain x where x: "x \<in> fst ` B" "\<forall>x'\<in>fst ` B. (x', x) \<notin> r"
using spec[OF assms[unfolded wf_eq_minimal2], of "fst ` B"] by auto
then obtain a where "(x, a) \<in> B" by auto
moreover
from * x have "\<forall>a'\<in>B. (a', (x, a)) \<notin> {((x1, y), x2, y). (x1, x2) \<in> r \<and> y \<in> A}" by auto
ultimately show "\<exists>xa\<in>B. \<forall>a'\<in>B. (a', xa) \<notin> {((x1, y), x2, y). (x1, x2) \<in> r \<and> y \<in> A}" by blast
qed
lemma oprod_wf_Id:
assumes TOT: "Total r" and TOT': "Total r'" and WF: "wf(r - Id)" and WF': "wf(r' - Id)"
shows "wf ((r *o r') - Id)"
proof(cases "r \<le> Id \<or> r' \<le> Id")
case False
thus ?thesis
using oprod_minus_Id[of r r'] assms oprod_wf[of "r - Id" "r' - Id"]
wf_subset[of "(r - Id) *o (r' - Id)" "(r *o r') - Id"] by auto
next
case True
thus ?thesis using wf_subset[OF wf_extend_oprod1[OF WF'] oprod_minus_Id1]
wf_subset[OF wf_extend_oprod2[OF WF] oprod_minus_Id2] by auto
qed
lemma oprod_Well_order:
assumes WELL: "Well_order r" and WELL': "Well_order r'"
shows "Well_order (r *o r')"
proof-
have "Total r \<and> Total r'" using WELL WELL' by (auto simp add: order_on_defs)
thus ?thesis using assms unfolding well_order_on_def
using oprod_Linear_order oprod_wf_Id by blast
qed
lemma oprod_embed:
assumes WELL: "Well_order r" and WELL': "Well_order r'" and "r' \<noteq> {}"
shows "embed r (r *o r') (\<lambda>x. (x, minim r' (Field r')))" (is "embed _ _ ?f")
proof -
from assms(3) have r': "Field r' \<noteq> {}" unfolding Field_def by auto
have minim[simp]: "minim r' (Field r') \<in> Field r'"
using wo_rel.minim_inField[unfolded wo_rel_def, OF WELL' _ r'] by auto
{ fix b
assume "(b, minim r' (Field r')) \<in> r'"
moreover hence "b \<in> Field r'" unfolding Field_def by auto
hence "(minim r' (Field r'), b) \<in> r'"
using wo_rel.minim_least[unfolded wo_rel_def, OF WELL' subset_refl] r' by auto
ultimately have "b = minim r' (Field r')"
by (metis WELL' antisym_def linear_order_on_def partial_order_on_def well_order_on_def)
} note * = this
have 1: "Well_order (r *o r')" using assms by (auto simp add: oprod_Well_order)
moreover
from r' have "compat r (r *o r') ?f" unfolding compat_def oprod_def by auto
moreover
from * have "ofilter (r *o r') (?f ` Field r)"
unfolding wo_rel.ofilter_def[unfolded wo_rel_def, OF 1] Field_oprod rel.under_def
unfolding oprod_def by auto (auto simp: image_iff Field_def)
moreover have "inj_on ?f (Field r)" unfolding inj_on_def by auto
ultimately show ?thesis using assms by (auto simp add: embed_iff_compat_inj_on_ofilter)
qed
corollary oprod_ordLeq: "\<lbrakk>Well_order r; Well_order r'; r' \<noteq> {}\<rbrakk> \<Longrightarrow> r \<le>o r *o r'"
using oprod_embed oprod_Well_order unfolding ordLeq_def by blast
definition "support z A f = {x \<in> A. f x \<noteq> z}"
lemma support_Un[simp]: "support z (A \<union> B) f = support z A f \<union> support z B f"
unfolding support_def by auto
lemma support_upd[simp]: "support z A (f(x := z)) = support z A f - {x}"
unfolding support_def by auto
lemma support_upd_subset[simp]: "support z A (f(x := y)) \<subseteq> support z A f \<union> {x}"
unfolding support_def by auto
lemma fun_unequal_in_support:
assumes "f \<noteq> g" "f \<in> Func A B" "g \<in> Func A C"
shows "(support z A f \<union> support z A g) \<inter> {a. f a \<noteq> g a} \<noteq> {}" (is "?L \<inter> ?R \<noteq> {}")
proof -
from assms(1) obtain x where x: "f x \<noteq> g x" by blast
hence "x \<in> ?R" by simp
moreover from assms(2-3) x have "x \<in> A" unfolding Func_def by fastforce
with x have "x \<in> ?L" unfolding support_def by auto
ultimately show ?thesis by auto
qed
definition fin_support where
"fin_support z A = {f. finite (support z A f)}"
lemma finite_support: "f \<in> fin_support z A \<Longrightarrow> finite (support z A f)"
unfolding support_def fin_support_def by auto
lemma fin_support_Field_osum:
"f \<in> fin_support z (Inl ` A \<union> Inr ` B) \<longleftrightarrow>
(f o Inl) \<in> fin_support z A \<and> (f o Inr) \<in> fin_support z B" (is "?L \<longleftrightarrow> ?R1 \<and> ?R2")
proof safe
assume ?L
from `?L` show ?R1 unfolding fin_support_def support_def
by (fastforce simp: image_iff elim: finite_surj[of _ _ "sum_case id undefined"])
from `?L` show ?R2 unfolding fin_support_def support_def
by (fastforce simp: image_iff elim: finite_surj[of _ _ "sum_case undefined id"])
next
assume ?R1 ?R2
thus ?L unfolding fin_support_def support_Un
by (auto simp: support_def elim: finite_surj[of _ _ Inl] finite_surj[of _ _ Inr])
qed
lemma Func_upd: "\<lbrakk>f \<in> Func A B; x \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> f(x := y) \<in> Func A B"
unfolding Func_def by auto
context wo_rel
begin
definition isMaxim :: "'a set \<Rightarrow> 'a \<Rightarrow> bool"
where "isMaxim A b \<equiv> b \<in> A \<and> (\<forall>a \<in> A. (a,b) \<in> r)"
definition maxim :: "'a set \<Rightarrow> 'a"
where "maxim A \<equiv> THE b. isMaxim A b"
lemma isMaxim_unique[intro]: "\<lbrakk>isMaxim A x; isMaxim A y\<rbrakk> \<Longrightarrow> x = y"
unfolding isMaxim_def using antisymD[OF ANTISYM, of x y] by auto
lemma maxim_isMaxim: "\<lbrakk>finite A; A \<noteq> {}; A \<subseteq> Field r\<rbrakk> \<Longrightarrow> isMaxim A (maxim A)"
unfolding maxim_def
proof (rule theI', rule ex_ex1I[OF _ isMaxim_unique, rotated], assumption+,
induct A rule: finite_induct)
case (insert x A)
thus ?case
proof (cases "A = {}")
case True
moreover have "isMaxim {x} x" unfolding isMaxim_def using refl_onD[OF REFL] insert(5) by auto
ultimately show ?thesis by blast
next
case False
with insert(3,5) obtain y where "isMaxim A y" by blast
with insert(2,5) have "if (y, x) \<in> r then isMaxim (insert x A) x else isMaxim (insert x A) y"
unfolding isMaxim_def subset_eq by (metis insert_iff max2_def max2_equals1 max2_iff)
thus ?thesis by metis
qed
qed simp
lemma maxim_in: "\<lbrakk>finite A; A \<noteq> {}; A \<subseteq> Field r\<rbrakk> \<Longrightarrow> maxim A \<in> A"
using maxim_isMaxim unfolding isMaxim_def by auto
lemma maxim_greatest: "\<lbrakk>finite A; x \<in> A; A \<subseteq> Field r\<rbrakk> \<Longrightarrow> (x, maxim A) \<in> r"
using maxim_isMaxim unfolding isMaxim_def by auto
lemma isMaxim_zero: "isMaxim A zero \<Longrightarrow> A = {zero}"
unfolding isMaxim_def by auto
lemma maxim_insert:
assumes "finite A" "A \<noteq> {}" "A \<subseteq> Field r" "x \<in> Field r"
shows "maxim (insert x A) = max2 x (maxim A)"
proof -
from assms have *: "isMaxim (insert x A) (maxim (insert x A))" "isMaxim A (maxim A)"
using maxim_isMaxim by auto
show ?thesis
proof (cases "(x, maxim A) \<in> r")
case True
with *(2) have "isMaxim (insert x A) (maxim A)" unfolding isMaxim_def
using transD[OF TRANS, of _ x "maxim A"] by blast
with *(1) True show ?thesis unfolding max2_def by (metis isMaxim_unique)
next
case False
hence "(maxim A, x) \<in> r" by (metis *(2) assms(3,4) in_mono in_notinI isMaxim_def)
with *(2) assms(4) have "isMaxim (insert x A) x" unfolding isMaxim_def
using transD[OF TRANS, of _ "maxim A" x] refl_onD[OF REFL, of x] by blast
with *(1) False show ?thesis unfolding max2_def by (metis isMaxim_unique)
qed
qed
lemma maxim_Un:
assumes "finite A" "A \<noteq> {}" "A \<subseteq> Field r" "finite B" "B \<noteq> {}" "B \<subseteq> Field r"
shows "maxim (A \<union> B) = max2 (maxim A) (maxim B)"
proof -
from assms have *: "isMaxim (A \<union> B) (maxim (A \<union> B))" "isMaxim A (maxim A)" "isMaxim B (maxim B)"
using maxim_isMaxim by auto
show ?thesis
proof (cases "(maxim A, maxim B) \<in> r")
case True
with *(2,3) have "isMaxim (A \<union> B) (maxim B)" unfolding isMaxim_def
using transD[OF TRANS, of _ "maxim A" "maxim B"] by blast
with *(1) True show ?thesis unfolding max2_def by (metis isMaxim_unique)
next
case False
hence "(maxim B, maxim A) \<in> r" by (metis *(2,3) assms(3,6) in_mono in_notinI isMaxim_def)
with *(2,3) have "isMaxim (A \<union> B) (maxim A)" unfolding isMaxim_def
using transD[OF TRANS, of _ "maxim B" "maxim A"] by blast
with *(1) False show ?thesis unfolding max2_def by (metis isMaxim_unique)
qed
qed
lemma maxim_insert_zero:
assumes "finite A" "A \<noteq> {}" "A \<subseteq> Field r"
shows "maxim (insert zero A) = maxim A"
using assms zero_in_Field maxim_in[OF assms] by (subst maxim_insert[unfolded max2_def]) auto
lemma maxim_equality: "isMaxim A x \<Longrightarrow> maxim A = x"
unfolding maxim_def by (rule the_equality) auto
lemma maxim_singleton:
"x \<in> Field r \<Longrightarrow> maxim {x} = x"
using refl_onD[OF REFL] by (intro maxim_equality) (simp add: isMaxim_def)
lemma maxim_Int: "\<lbrakk>finite A; A \<noteq> {}; A \<subseteq> Field r; maxim A \<in> B\<rbrakk> \<Longrightarrow> maxim (A \<inter> B) = maxim A"
by (rule maxim_equality) (auto simp: isMaxim_def intro: maxim_in maxim_greatest)
lemma maxim_mono: "\<lbrakk>X \<subseteq> Y; finite Y; X \<noteq> {}; Y \<subseteq> Field r\<rbrakk> \<Longrightarrow> (maxim X, maxim Y) \<in> r"
using maxim_in[OF finite_subset, of X Y] by (auto intro: maxim_greatest)
definition "max_fun_diff f g \<equiv> maxim ({a \<in> Field r. f a \<noteq> g a})"
lemma max_fun_diff_commute: "max_fun_diff f g = max_fun_diff g f"
unfolding max_fun_diff_def by metis
lemma zero_under: "x \<in> Field r \<Longrightarrow> zero \<in> under x"
unfolding under_def by (auto intro: zero_smallest)
end
definition "FinFunc r s = Func (Field s) (Field r) \<inter> fin_support (zero r) (Field s)"
lemma FinFuncD: "\<lbrakk>f \<in> FinFunc r s; x \<in> Field s\<rbrakk> \<Longrightarrow> f x \<in> Field r"
unfolding FinFunc_def Func_def by (fastforce split: option.splits)
locale wo_rel2 =
fixes r s
assumes rWELL: "Well_order r"
and sWELL: "Well_order s"
begin
interpretation r!: wo_rel r by unfold_locales (rule rWELL)
interpretation s!: wo_rel s by unfold_locales (rule sWELL)
abbreviation "SUPP \<equiv> support r.zero (Field s)"
abbreviation "FINFUNC \<equiv> FinFunc r s"
lemmas FINFUNCD = FinFuncD[of _ r s]
lemma fun_diff_alt: "{a \<in> Field s. f a \<noteq> g a} = (SUPP f \<union> SUPP g) \<inter> {a. f a \<noteq> g a}"
by (auto simp: support_def)
lemma max_fun_diff_alt:
"s.max_fun_diff f g = s.maxim ((SUPP f \<union> SUPP g) \<inter> {a. f a \<noteq> g a})"
unfolding s.max_fun_diff_def fun_diff_alt ..
lemma isMaxim_max_fun_diff: "\<lbrakk>f \<noteq> g; f \<in> FINFUNC; g \<in> FINFUNC\<rbrakk> \<Longrightarrow>
s.isMaxim {a \<in> Field s. f a \<noteq> g a} (s.max_fun_diff f g)"
using fun_unequal_in_support[of f g] unfolding max_fun_diff_alt fun_diff_alt fun_eq_iff
by (intro s.maxim_isMaxim) (auto simp: FinFunc_def fin_support_def support_def)
lemma max_fun_diff_in: "\<lbrakk>f \<noteq> g; f \<in> FINFUNC; g \<in> FINFUNC\<rbrakk> \<Longrightarrow>
s.max_fun_diff f g \<in> {a \<in> Field s. f a \<noteq> g a}"
using isMaxim_max_fun_diff unfolding s.isMaxim_def by blast
lemma max_fun_diff_max: "\<lbrakk>f \<noteq> g; f \<in> FINFUNC; g \<in> FINFUNC; x \<in> {a \<in> Field s. f a \<noteq> g a}\<rbrakk> \<Longrightarrow>
(x, s.max_fun_diff f g) \<in> s"
using isMaxim_max_fun_diff unfolding s.isMaxim_def by blast
lemma max_fun_diff:
"\<lbrakk>f \<noteq> g; f \<in> FINFUNC; g \<in> FINFUNC\<rbrakk> \<Longrightarrow>
(\<exists>a b. a \<noteq> b \<and> a \<in> Field r \<and> b \<in> Field r \<and>
f (s.max_fun_diff f g) = a \<and> g (s.max_fun_diff f g) = b)"
using isMaxim_max_fun_diff[of f g] unfolding s.isMaxim_def FinFunc_def Func_def by auto
lemma max_fun_diff_le_eq:
"\<lbrakk>(s.max_fun_diff f g, x) \<in> s; f \<noteq> g; f \<in> FINFUNC; g \<in> FINFUNC; x \<noteq> s.max_fun_diff f g\<rbrakk> \<Longrightarrow>
f x = g x"
using max_fun_diff_max[of f g x] antisymD[OF s.ANTISYM, of "s.max_fun_diff f g" x]
by (auto simp: Field_def)
lemma max_fun_diff_max2:
assumes ineq: "s.max_fun_diff f g = s.max_fun_diff g h \<longrightarrow>
f (s.max_fun_diff f g) \<noteq> h (s.max_fun_diff g h)" and
fg: "f \<noteq> g" and gh: "g \<noteq> h" and fh: "f \<noteq> h" and
f: "f \<in> FINFUNC" and g: "g \<in> FINFUNC" and h: "h \<in> FINFUNC"
shows "s.max_fun_diff f h = s.max2 (s.max_fun_diff f g) (s.max_fun_diff g h)"
(is "?fh = s.max2 ?fg ?gh")
proof (cases "?fg = ?gh")
case True
with ineq have "f ?fg \<noteq> h ?fg" by simp
moreover
{ fix x assume x: "x \<in> {a \<in> Field s. f a \<noteq> h a}"
hence "(x, ?fg) \<in> s"
proof (cases "x = ?fg")
case False show ?thesis
proof (rule ccontr)
assume "(x, ?fg) \<notin> s"
with max_fun_diff_in[OF fg f g] x False have *: "(?fg, x) \<in> s" by (blast intro: s.in_notinI)
hence "f x = g x" by (rule max_fun_diff_le_eq[OF _ fg f g False])
moreover have "g x = h x" using max_fun_diff_le_eq[OF _ gh g h] False True * by simp
ultimately show False using x by simp
qed
qed (simp add: refl_onD[OF s.REFL])
}
ultimately have "s.isMaxim {a \<in> Field s. f a \<noteq> h a} ?fg"
unfolding s.isMaxim_def using max_fun_diff_in[OF fg f g] by simp
hence "?fh = ?fg" using isMaxim_max_fun_diff[OF fh f h] by blast
thus ?thesis unfolding True s.max2_def by simp
next
case False note * = this
show ?thesis
proof (cases "(?fg, ?gh) \<in> s")
case True
hence *: "f ?gh = g ?gh" by (rule max_fun_diff_le_eq[OF _ fg f g *[symmetric]])
hence "s.isMaxim {a \<in> Field s. f a \<noteq> h a} ?gh" using isMaxim_max_fun_diff[OF gh g h]
isMaxim_max_fun_diff[OF fg f g] transD[OF s.TRANS _ True]
unfolding s.isMaxim_def by auto
hence "?fh = ?gh" using isMaxim_max_fun_diff[OF fh f h] by blast
thus ?thesis using True unfolding s.max2_def by simp
next
case False
with max_fun_diff_in[OF fg f g] max_fun_diff_in[OF gh g h] have True: "(?gh, ?fg) \<in> s"
by (blast intro: s.in_notinI)
hence *: "g ?fg = h ?fg" by (rule max_fun_diff_le_eq[OF _ gh g h *])
hence "s.isMaxim {a \<in> Field s. f a \<noteq> h a} ?fg" using isMaxim_max_fun_diff[OF gh g h]
isMaxim_max_fun_diff[OF fg f g] True transD[OF s.TRANS, of _ _ ?fg]
unfolding s.isMaxim_def by auto
hence "?fh = ?fg" using isMaxim_max_fun_diff[OF fh f h] by blast
thus ?thesis using False unfolding s.max2_def by simp
qed
qed
definition oexp where
"oexp = {(f, g) . f \<in> FINFUNC \<and> g \<in> FINFUNC \<and>
((let m = s.max_fun_diff f g in (f m, g m) \<in> r) \<or> f = g)}"
lemma Field_oexp: "Field oexp = FINFUNC"
unfolding oexp_def FinFunc_def by (auto simp: Let_def Field_def)
lemma oexp_Refl: "Refl oexp"
unfolding refl_on_def Field_oexp unfolding oexp_def by (auto simp: Let_def)
lemma oexp_trans: "trans oexp"
proof (unfold trans_def, safe)
fix f g h :: "'b \<Rightarrow> 'a"
let ?fg = "s.max_fun_diff f g"
and ?gh = "s.max_fun_diff g h"
and ?fh = "s.max_fun_diff f h"
assume oexp: "(f, g) \<in> oexp" "(g, h) \<in> oexp"
thus "(f, h) \<in> oexp"
proof (cases "f = g \<or> g = h")
case False
with oexp have "f \<in> FINFUNC" "g \<in> FINFUNC" "h \<in> FINFUNC"
"(f ?fg, g ?fg) \<in> r" "(g ?gh, h ?gh) \<in> r" unfolding oexp_def Let_def by auto
note * = this False
show ?thesis
proof (cases "f \<noteq> h")
case True
show ?thesis
proof (cases "?fg = ?gh \<longrightarrow> f ?fg \<noteq> h ?gh")
case True
show ?thesis using max_fun_diff_max2[of f g h, OF True] * `f \<noteq> h` max_fun_diff_in
r.max2_iff[OF FINFUNCD FINFUNCD] r.max2_equals1[OF FINFUNCD FINFUNCD] max_fun_diff_le_eq
s.in_notinI[OF disjI1] unfolding oexp_def Let_def s.max2_def mem_Collect_eq by safe metis
next
case False with * show ?thesis unfolding oexp_def Let_def
using antisymD[OF r.ANTISYM, of "g ?gh" "h ?gh"] max_fun_diff_in[of g h] by auto
qed
qed (auto simp: oexp_def *(3))
qed auto
qed
lemma oexp_Preorder: "Preorder oexp"
unfolding preorder_on_def using oexp_Refl oexp_trans by blast
lemma oexp_antisym: "antisym oexp"
proof (unfold antisym_def, safe, rule ccontr)
fix f g assume "(f, g) \<in> oexp" "(g, f) \<in> oexp" "g \<noteq> f"
thus False using refl_onD[OF r.REFL FINFUNCD] max_fun_diff_in unfolding oexp_def Let_def
by (auto dest!: antisymD[OF r.ANTISYM] simp: s.max_fun_diff_commute)
qed
lemma oexp_Partial_order: "Partial_order oexp"
unfolding partial_order_on_def using oexp_Preorder oexp_antisym by blast
lemma oexp_Total: "Total oexp"
unfolding total_on_def Field_oexp unfolding oexp_def using FINFUNCD max_fun_diff_in
by (auto simp: Let_def s.max_fun_diff_commute intro!: r.in_notinI)
lemma oexp_Linear_order: "Linear_order oexp"
unfolding linear_order_on_def using oexp_Partial_order oexp_Total by blast
definition "const = (\<lambda>x. if x \<in> Field s then r.zero else undefined)"
lemma const_in[simp]: "x \<in> Field s \<Longrightarrow> const x = r.zero"
unfolding const_def by auto
lemma const_notin[simp]: "x \<notin> Field s \<Longrightarrow> const x = undefined"
unfolding const_def by auto
lemma const_Int_Field[simp]: "Field s \<inter> - {x. const x = r.zero} = {}"
by auto
lemma const_FINFUNC[simp]: "Field r \<noteq> {} \<Longrightarrow> const \<in> FINFUNC"
unfolding FinFunc_def Func_def fin_support_def support_def const_def Int_iff mem_Collect_eq
using r.zero_in_Field by (metis (lifting) Collect_empty_eq finite.emptyI)
lemma const_least:
assumes "Field r \<noteq> {}" "f \<in> FINFUNC"
shows "(const, f) \<in> oexp"
proof (cases "f = const")
case True thus ?thesis using refl_onD[OF oexp_Refl] assms(2) unfolding Field_oexp by auto
next
case False
with assms show ?thesis using max_fun_diff_in[of f const]
unfolding oexp_def Let_def by (auto intro: r.zero_smallest FinFuncD simp: s.max_fun_diff_commute)
qed
lemma support_not_const:
assumes "F \<subseteq> FINFUNC" and "const \<notin> F"
shows "\<forall>f \<in> F. finite (SUPP f) \<and> SUPP f \<noteq> {} \<and> SUPP f \<subseteq> Field s"
proof (intro ballI conjI)
fix f assume "f \<in> F"
thus "finite (SUPP f)" "SUPP f \<subseteq> Field s"
using assms(1) unfolding FinFunc_def fin_support_def support_def by auto
show "SUPP f \<noteq> {}"
proof (rule ccontr, unfold not_not)
assume "SUPP f = {}"
moreover from `f \<in> F` assms(1) have "f \<in> FINFUNC" by blast
ultimately have "f = const"
by (auto simp: fun_eq_iff support_def FinFunc_def Func_def const_def)
with assms(2) `f \<in> F` show False by blast
qed
qed
lemma maxim_isMaxim_support:
assumes f: "F \<subseteq> FINFUNC" and "const \<notin> F"
shows "\<forall>f \<in> F. s.isMaxim (SUPP f) (s.maxim (SUPP f))"
using support_not_const[OF assms] by (auto intro!: s.maxim_isMaxim)
lemma oexp_empty2: "Field s = {} \<Longrightarrow> oexp = {(\<lambda>x. undefined, \<lambda>x. undefined)}"
unfolding oexp_def FinFunc_def fin_support_def support_def by auto
lemma oexp_empty: "\<lbrakk>Field r = {}; Field s \<noteq> {}\<rbrakk> \<Longrightarrow> oexp = {}"
unfolding oexp_def FinFunc_def Let_def by auto
lemma fun_upd_FINFUNC: "\<lbrakk>f \<in> FINFUNC; x \<in> Field s; y \<in> Field r\<rbrakk> \<Longrightarrow> f(x := y) \<in> FINFUNC"
unfolding FinFunc_def Func_def fin_support_def
by (auto intro: finite_subset[OF support_upd_subset])
lemma fun_upd_same_oexp:
assumes "(f, g) \<in> oexp" "f x = g x" "x \<in> Field s" "y \<in> Field r"
shows "(f(x := y), g(x := y)) \<in> oexp"
proof -
from assms(1) fun_upd_FINFUNC[OF _ assms(3,4)] have fg: "f(x := y) \<in> FINFUNC" "g(x := y) \<in> FINFUNC"
unfolding oexp_def by auto
moreover from assms(2) have "s.max_fun_diff (f(x := y)) (g(x := y)) = s.max_fun_diff f g"
unfolding s.max_fun_diff_def by auto metis
ultimately show ?thesis using assms refl_onD[OF r.REFL] unfolding oexp_def Let_def by auto
qed
lemma fun_upd_smaller_oexp:
assumes "f \<in> FINFUNC" "x \<in> Field s" "y \<in> Field r" "(y, f x) \<in> r"
shows "(f(x := y), f) \<in> oexp"
using assms fun_upd_FINFUNC[OF assms(1-3)] s.maxim_singleton[of "x"]
unfolding oexp_def FinFunc_def Let_def fin_support_def s.max_fun_diff_def by (auto simp: fun_eq_iff)
lemma oexp_wf_Id: "wf (oexp - Id)"
proof (cases "Field r = {} \<or> Field s = {}")
case True thus ?thesis using oexp_empty oexp_empty2 by fastforce
next
case False
hence Fields: "Field s \<noteq> {}" "Field r \<noteq> {}" by simp_all
hence [simp]: "r.zero \<in> Field r" by (intro r.zero_in_Field)
have const[simp]: "\<And>F. \<lbrakk>const \<in> F; F \<subseteq> FINFUNC\<rbrakk> \<Longrightarrow> \<exists>f0\<in>F. \<forall>f\<in>F. (f0, f) \<in> oexp"
using const_least[OF Fields(2)] by auto
show ?thesis
unfolding Linear_order_wf_diff_Id[OF oexp_Linear_order] Field_oexp
proof (intro allI impI)
fix A assume A: "A \<subseteq> FINFUNC" "A \<noteq> {}"
{ fix y F
have "F \<subseteq> FINFUNC \<and> (\<exists>f \<in> F. y = s.maxim (SUPP f)) \<longrightarrow>
(\<exists>f0 \<in> F. \<forall>f \<in> F. (f0, f) \<in> oexp)" (is "?P F y")
proof (induct y arbitrary: F rule: s.well_order_induct)
case (1 y)
show ?case
proof (intro impI, elim conjE bexE)
fix f assume F: "F \<subseteq> FINFUNC" "f \<in> F" "y = s.maxim (SUPP f)"
thus "\<exists>f0\<in>F. \<forall>f\<in>F. (f0, f) \<in> oexp"
proof (cases "const \<in> F")
case False
with F have maxF: "\<forall>f \<in> F. s.isMaxim (SUPP f) (s.maxim (SUPP f))"
and SUPPF: "\<forall>f \<in> F. finite (SUPP f) \<and> SUPP f \<noteq> {} \<and> SUPP f \<subseteq> Field s"
using maxim_isMaxim_support support_not_const by auto
def z \<equiv> "s.minim {s.maxim (SUPP f) | f. f \<in> F}"
from F SUPPF maxF have zmin: "s.isMinim {s.maxim (SUPP f) | f. f \<in> F} z"
unfolding z_def by (intro s.minim_isMinim) (auto simp: s.isMaxim_def)
with F have zy: "(z, y) \<in> s" unfolding s.isMinim_def by auto
hence zField: "z \<in> Field s" unfolding Field_def by auto
def x0 \<equiv> "r.minim {f z | f. f \<in> F \<and> z = s.maxim (SUPP f)}"
from F(1,2) maxF(1) SUPPF zmin
have x0min: "r.isMinim {f z | f. f \<in> F \<and> z = s.maxim (SUPP f)} x0"
unfolding x0_def s.isMaxim_def s.isMinim_def
by (blast intro!: r.minim_isMinim FinFuncD[of _ r s])
with maxF(1) SUPPF F(1) have x0Field: "x0 \<in> Field r"
unfolding r.isMinim_def s.isMaxim_def by (auto intro!: FINFUNCD)
from x0min maxF(1) SUPPF F(1) have x0notzero: "x0 \<noteq> r.zero"
unfolding r.isMinim_def s.isMaxim_def FinFunc_def Func_def support_def
by fastforce
def G \<equiv> "{f(z := r.zero) | f. f \<in> F \<and> z = s.maxim (SUPP f) \<and> f z = x0}"
from zmin x0min have "G \<noteq> {}" unfolding G_def z_def s.isMinim_def r.isMinim_def by blast
have GF: "G \<subseteq> (\<lambda>f. f(z := r.zero)) ` F" unfolding G_def by auto
have "G \<subseteq> fin_support r.zero (Field s)"
unfolding FinFunc_def fin_support_def proof safe
fix g assume "g \<in> G"
with GF obtain f where "f \<in> F" "g = f(z := r.zero)" by auto
moreover with SUPPF have "finite (SUPP f)" by blast
ultimately show "finite (SUPP g)"
by (elim finite_subset[rotated]) (auto simp: support_def)
qed
moreover from F GF zField have "G \<subseteq> Func (Field s) (Field r)"
using Func_upd[of _ "Field s" "Field r" z r.zero] unfolding FinFunc_def by auto
ultimately have G: "G \<subseteq> FINFUNC" unfolding FinFunc_def by blast
hence "\<exists>g0\<in>G. \<forall>g\<in>G. (g0, g) \<in> oexp"
proof (cases "const \<in> G")
case False
with G have maxG: "\<forall>g \<in> G. s.isMaxim (SUPP g) (s.maxim (SUPP g))"
and SUPPG: "\<forall>g \<in> G. finite (SUPP g) \<and> SUPP g \<noteq> {} \<and> SUPP g \<subseteq> Field s"
using maxim_isMaxim_support support_not_const by auto
def y' \<equiv> "s.minim {s.maxim (SUPP f) | f. f \<in> G}"
from G SUPPG maxG `G \<noteq> {}` have y'min: "s.isMinim {s.maxim (SUPP f) | f. f \<in> G} y'"
unfolding y'_def by (intro s.minim_isMinim) (auto simp: s.isMaxim_def)
moreover
have "\<forall>g \<in> G. z \<notin> SUPP g" unfolding support_def G_def by auto
moreover
{ fix g assume g: "g \<in> G"
then obtain f where "f \<in> F" "g = f(z := r.zero)" and z: "z = s.maxim (SUPP f)"
unfolding G_def by auto
with SUPPF bspec[OF SUPPG g] have "(s.maxim (SUPP g), z) \<in> s"
unfolding z by (intro s.maxim_mono) auto
}
moreover from y'min have "\<And>g. g \<in> G \<Longrightarrow> (y', s.maxim (SUPP g)) \<in> s"
unfolding s.isMinim_def by auto
ultimately have "y' \<noteq> z" "(y', z) \<in> s" using maxG
unfolding s.isMinim_def s.isMaxim_def by auto
with zy have "y' \<noteq> y" "(y', y) \<in> s" using antisymD[OF s.ANTISYM] transD[OF s.TRANS]
by blast+
moreover from `G \<noteq> {}` have "\<exists>g \<in> G. y' = wo_rel.maxim s (SUPP g)" using y'min
by (auto simp: G_def s.isMinim_def)
ultimately show ?thesis using mp[OF spec[OF mp[OF spec[OF 1]]], of y' G] G by auto
qed simp
then obtain g0 where g0: "g0 \<in> G" "\<forall>g \<in> G. (g0, g) \<in> oexp" by blast
hence g0z: "g0 z = r.zero" unfolding G_def by auto
def f0 \<equiv> "g0(z := x0)"
with x0notzero zField have SUPP: "SUPP f0 = SUPP g0 \<union> {z}" unfolding support_def by auto
from g0z have f0z: "f0(z := r.zero) = g0" unfolding f0_def fun_upd_upd by auto
have f0: "f0 \<in> F" using x0min g0(1)
Func_elim[OF set_mp[OF subset_trans[OF F(1)[unfolded FinFunc_def] Int_lower1]] zField]
unfolding f0_def r.isMinim_def G_def by (force simp: fun_upd_idem)
from g0(1) maxF(1) have maxf0: "s.maxim (SUPP f0) = z" unfolding SUPP G_def
by (intro s.maxim_equality) (auto simp: s.isMaxim_def)
show ?thesis
proof (intro bexI[OF _ f0] ballI)
fix f assume f: "f \<in> F"
show "(f0, f) \<in> oexp"
proof (cases "f0 = f")
case True thus ?thesis by (metis F(1) Field_oexp f0 in_mono oexp_Refl refl_onD)
next
case False
thus ?thesis
proof (cases "s.maxim (SUPP f) = z \<and> f z = x0")
case True
with f have "f(z := r.zero) \<in> G" unfolding G_def by blast
with g0(2) f0z have "(f0(z := r.zero), f(z := r.zero)) \<in> oexp" by auto
hence "(f0(z := r.zero, z := x0), f(z := r.zero, z := x0)) \<in> oexp"
by (elim fun_upd_same_oexp[OF _ _ zField x0Field]) simp
moreover
with f F(1) x0min True
have "(f(z := x0), f) \<in> oexp" unfolding G_def r.isMinim_def
by (intro fun_upd_smaller_oexp[OF _ zField x0Field]) auto
ultimately show ?thesis using transD[OF oexp_trans, of f0 "f(z := x0)" f]
unfolding f0_def by auto
next
case False note notG = this
thus ?thesis
proof (cases "s.maxim (SUPP f) = z")
case True
with notG have "f0 z \<noteq> f z" unfolding f0_def by auto
hence "f0 z \<noteq> f z" by metis
with True maxf0 f0 f SUPPF have "s.max_fun_diff f0 f = z"
using s.maxim_Un[of "SUPP f0" "SUPP f", unfolded s.max2_def]
unfolding max_fun_diff_alt by (intro trans[OF s.maxim_Int]) auto
moreover
from x0min True f have "(x0, f z) \<in> r" unfolding r.isMinim_def by auto
ultimately show ?thesis using f f0 F(1) unfolding oexp_def f0_def by auto
next
case False
with notG have *: "(z, s.maxim (SUPP f)) \<in> s" "z \<noteq> s.maxim (SUPP f)"
using zmin f unfolding s.isMinim_def G_def by auto
have f0f: "f0 (s.maxim (SUPP f)) = r.zero"
proof (rule ccontr)
assume "f0 (s.maxim (SUPP f)) \<noteq> r.zero"
with f SUPPF maxF(1) have "s.maxim (SUPP f) \<in> SUPP f0"
unfolding support_def[of _ _ f0] s.isMaxim_def by auto
with SUPPF f0 have "(s.maxim (SUPP f), z) \<in> s" unfolding maxf0[symmetric]
by (auto intro: s.maxim_greatest)
with * antisymD[OF s.ANTISYM] show False by simp
qed
moreover
have "f (s.maxim (SUPP f)) \<noteq> r.zero"
using bspec[OF maxF(1) f, unfolded s.isMaxim_def] by (auto simp: support_def)
with f0f * f f0 maxf0 SUPPF
have "s.max_fun_diff f0 f = s.maxim (SUPP f0 \<union> SUPP f)"
unfolding max_fun_diff_alt using s.maxim_Un[of "SUPP f0" "SUPP f"]
by (intro s.maxim_Int) (auto simp: s.max2_def)
moreover have "s.maxim (SUPP f0 \<union> SUPP f) = s.maxim (SUPP f)"
using s.maxim_Un[of "SUPP f0" "SUPP f"] * maxf0 SUPPF f0 f
by (auto simp: s.max2_def)
ultimately show ?thesis using f f0 F(1) maxF(1) SUPPF unfolding oexp_def Let_def
by (fastforce simp: s.isMaxim_def intro!: r.zero_smallest FINFUNCD)
qed
qed
qed
qed
qed simp
qed
qed
} note * = mp[OF this]
from A(2) obtain f where f: "f \<in> A" by blast
with A(1) show "\<exists>a\<in>A. \<forall>a'\<in>A. (a, a') \<in> oexp"
proof (cases "f = const")
case False with f A(1) show ?thesis using maxim_isMaxim_support[of "{f}"]
by (intro *[of _ "s.maxim (SUPP f)"]) (auto simp: s.isMaxim_def support_def)
qed simp
qed
qed
lemma oexp_Well_order: "Well_order oexp"
unfolding well_order_on_def using oexp_Linear_order oexp_wf_Id by blast
interpretation o: wo_rel oexp by unfold_locales (rule oexp_Well_order)
lemma zero_oexp: "Field r \<noteq> {} \<Longrightarrow> o.zero = const"
by (rule sym[OF o.leq_zero_imp[OF const_least]])
(auto intro!: o.zero_in_Field[unfolded Field_oexp] dest!: const_FINFUNC)
end
notation wo_rel2.oexp (infixl "^o" 90)
lemmas oexp_def = wo_rel2.oexp_def[unfolded wo_rel2_def, OF conjI]
lemmas oexp_Well_order = wo_rel2.oexp_Well_order[unfolded wo_rel2_def, OF conjI]
lemmas Field_oexp = wo_rel2.Field_oexp[unfolded wo_rel2_def, OF conjI]
definition "ozero = {}"
lemma ozero_Well_order[simp]: "Well_order ozero"
unfolding ozero_def by simp
lemma ozero_ordIso[simp]: "ozero =o ozero"
unfolding ozero_def ordIso_def iso_def[abs_def] embed_def bij_betw_def by auto
lemma Field_ozero[simp]: "Field ozero = {}"
unfolding ozero_def by simp
lemma iso_ozero_empty[simp]: "r =o ozero = (r = {})"
unfolding ozero_def ordIso_def iso_def[abs_def] embed_def bij_betw_def
by (auto dest: rel.well_order_on_domain)
lemma ozero_ordLeq:
assumes "Well_order r" shows "ozero \<le>o r"
using assms unfolding ozero_def ordLeq_def embed_def[abs_def] rel.under_def by auto
definition "oone = {((),())}"
lemma oone_Well_order[simp]: "Well_order oone"
unfolding oone_def unfolding well_order_on_def linear_order_on_def partial_order_on_def
preorder_on_def total_on_def refl_on_def trans_def antisym_def by auto
lemma Field_oone[simp]: "Field oone = {()}"
unfolding oone_def by simp
lemma oone_ordIso: "oone =o {(x,x)}"
unfolding ordIso_def oone_def well_order_on_def linear_order_on_def partial_order_on_def
preorder_on_def total_on_def refl_on_def trans_def antisym_def
by (auto simp: iso_def embed_def bij_betw_def rel.under_def inj_on_def intro!: exI[of _ "\<lambda>_. x"])
lemma osum_ordLeqR: "Well_order r \<Longrightarrow> Well_order s \<Longrightarrow> s \<le>o r +o s"
unfolding ordLeq_def2 rel.underS_def
by (auto intro!: exI[of _ Inr] osum_Well_order) (auto simp add: osum_def Field_def)
lemma osum_congL:
assumes "r =o s" and t: "Well_order t"
shows "r +o t =o s +o t" (is "?L =o ?R")
proof -
from assms(1) obtain f where r: "Well_order r" and s: "Well_order s" and f: "iso r s f"
unfolding ordIso_def by blast
let ?f = "sum_map f id"
from f have "inj_on ?f (Field ?L)"
unfolding Field_osum iso_def bij_betw_def inj_on_def by fastforce
with f have "bij_betw ?f (Field ?L) (Field ?R)"
unfolding Field_osum iso_def bij_betw_def image_image image_Un by auto
moreover from f have "compat ?L ?R ?f"
unfolding osum_def iso_iff3[OF r s] compat_def bij_betw_def
by (auto simp: map_pair_imageI)
ultimately have "iso ?L ?R ?f" by (subst iso_iff3) (auto intro: osum_Well_order r s t)
thus ?thesis unfolding ordIso_def by (auto intro: osum_Well_order r s t)
qed
lemma osum_congR:
assumes "r =o s" and t: "Well_order t"
shows "t +o r =o t +o s" (is "?L =o ?R")
proof -
from assms(1) obtain f where r: "Well_order r" and s: "Well_order s" and f: "iso r s f"
unfolding ordIso_def by blast
let ?f = "sum_map id f"
from f have "inj_on ?f (Field ?L)"
unfolding Field_osum iso_def bij_betw_def inj_on_def by fastforce
with f have "bij_betw ?f (Field ?L) (Field ?R)"
unfolding Field_osum iso_def bij_betw_def image_image image_Un by auto
moreover from f have "compat ?L ?R ?f"
unfolding osum_def iso_iff3[OF r s] compat_def bij_betw_def
by (auto simp: map_pair_imageI)
ultimately have "iso ?L ?R ?f" by (subst iso_iff3) (auto intro: osum_Well_order r s t)
thus ?thesis unfolding ordIso_def by (auto intro: osum_Well_order r s t)
qed
lemma osum_cong:
assumes "t =o u" and "r =o s"
shows "t +o r =o u +o s"
using ordIso_transitive[OF osum_congL[OF assms(1)] osum_congR[OF assms(2)]]
assms[unfolded ordIso_def] by auto
lemma Well_order_empty[simp]: "Well_order {}"
unfolding Field_empty by (rule well_order_on_empty)
lemma well_order_on_singleton[simp]: "well_order_on {x} {(x, x)}"
unfolding well_order_on_def linear_order_on_def partial_order_on_def preorder_on_def total_on_def
Field_def refl_on_def trans_def antisym_def by auto
lemma oexp_empty[simp]:
assumes "Well_order r"
shows "r ^o {} = {(\<lambda>x. undefined, \<lambda>x. undefined)}"
unfolding oexp_def[OF assms Well_order_empty] FinFunc_def fin_support_def support_def by auto
lemma oexp_empty2[simp]:
assumes "Well_order r" "r \<noteq> {}"
shows "{} ^o r = {}"
proof -
from assms(2) have "Field r \<noteq> {}" unfolding Field_def by auto
thus ?thesis unfolding oexp_def[OF Well_order_empty assms(1)] FinFunc_def fin_support_def support_def
by auto
qed
lemma oprod_zero[simp]: "{} *o r = {}" "r *o {} = {}"
unfolding oprod_def by simp_all
lemma oprod_congL:
assumes "r =o s" and t: "Well_order t"
shows "r *o t =o s *o t" (is "?L =o ?R")
proof -
from assms(1) obtain f where r: "Well_order r" and s: "Well_order s" and f: "iso r s f"
unfolding ordIso_def by blast
let ?f = "map_pair f id"
from f have "inj_on ?f (Field ?L)"
unfolding Field_oprod iso_def bij_betw_def inj_on_def by fastforce
with f have "bij_betw ?f (Field ?L) (Field ?R)"
unfolding Field_oprod iso_def bij_betw_def by (auto intro!: map_pair_surj_on)
moreover from f have "compat ?L ?R ?f"
unfolding iso_iff3[OF r s] compat_def oprod_def bij_betw_def
by (auto simp: map_pair_imageI)
ultimately have "iso ?L ?R ?f" by (subst iso_iff3) (auto intro: oprod_Well_order r s t)
thus ?thesis unfolding ordIso_def by (auto intro: oprod_Well_order r s t)
qed
lemma oprod_congR:
assumes "r =o s" and t: "Well_order t"
shows "t *o r =o t *o s" (is "?L =o ?R")
proof -
from assms(1) obtain f where r: "Well_order r" and s: "Well_order s" and f: "iso r s f"
unfolding ordIso_def by blast
let ?f = "map_pair id f"
from f have "inj_on ?f (Field ?L)"
unfolding Field_oprod iso_def bij_betw_def inj_on_def by fastforce
with f have "bij_betw ?f (Field ?L) (Field ?R)"
unfolding Field_oprod iso_def bij_betw_def by (auto intro!: map_pair_surj_on)
moreover from f rel.well_order_on_domain[OF r] have "compat ?L ?R ?f"
unfolding iso_iff3[OF r s] compat_def oprod_def bij_betw_def
by (auto simp: map_pair_imageI dest: inj_onD)
ultimately have "iso ?L ?R ?f" by (subst iso_iff3) (auto intro: oprod_Well_order r s t)
thus ?thesis unfolding ordIso_def by (auto intro: oprod_Well_order r s t)
qed
lemma oprod_cong:
assumes "t =o u" and "r =o s"
shows "t *o r =o u *o s"
using ordIso_transitive[OF oprod_congL[OF assms(1)] oprod_congR[OF assms(2)]]
assms[unfolded ordIso_def] by auto
lemma Field_singleton[simp]: "Field {(z,z)} = {z}"
by (metis rel.well_order_on_Field well_order_on_singleton)
lemma zero_singleton[simp]: "zero {(z,z)} = z"
using wo_rel.zero_in_Field[unfolded wo_rel_def, of "{(z, z)}"] well_order_on_singleton[of z]
by auto
lemma FinFunc_singleton: "FinFunc {(z,z)} s = {\<lambda>x. if x \<in> Field s then z else undefined}"
unfolding FinFunc_def Func_def fin_support_def support_def
by (auto simp: fun_eq_iff split: split_if_asm intro!: finite_subset[of _ "{}"])
lemma oone_ordIso_oexp:
assumes "r =o oone" and s: "Well_order s"
shows "r ^o s =o oone" (is "?L =o ?R")
proof -
from assms obtain f where *: "\<forall>x\<in>Field r. \<forall>y\<in>Field r. x = y" and "f ` Field r = {()}"
and r: "Well_order r"
unfolding ordIso_def oone_def by (auto simp: iso_def bij_betw_def inj_on_def)
then obtain x where "x \<in> Field r" by auto
with * have Fr: "Field r = {x}" by auto
interpret r: wo_rel r by unfold_locales (rule r)
from Fr r.well_order_on_domain[OF r] refl_onD[OF r.REFL, of x] have r_def: "r = {(x, x)}" by fast
interpret wo_rel2 r s by unfold_locales (rule r, rule s)
have "bij_betw (\<lambda>x. ()) (Field ?L) (Field ?R)"
unfolding bij_betw_def Field_oexp by (auto simp: r_def FinFunc_singleton)
moreover have "compat ?L ?R (\<lambda>x. ())" unfolding compat_def oone_def by auto
ultimately have "iso ?L ?R (\<lambda>x. ())" using s oone_Well_order
by (subst iso_iff3) (auto intro: oexp_Well_order)
thus ?thesis using s oone_Well_order unfolding ordIso_def by (auto intro: oexp_Well_order)
qed
(*Lemma 1.4.3 from Holz et al.*)
context
fixes r s t
assumes r: "Well_order r"
assumes s: "Well_order s"
assumes t: "Well_order t"
begin
lemma osum_ozeroL: "ozero +o r =o r"
using r unfolding osum_def ozero_def by (auto intro: map_pair_ordIso)
lemma osum_ozeroR: "r +o ozero =o r"
using r unfolding osum_def ozero_def by (auto intro: map_pair_ordIso)
lemma osum_assoc: "(r +o s) +o t =o r +o s +o t" (is "?L =o ?R")
proof -
let ?f =
"\<lambda>rst. case rst of Inl (Inl r) \<Rightarrow> Inl r | Inl (Inr s) \<Rightarrow> Inr (Inl s) | Inr t \<Rightarrow> Inr (Inr t)"
have "bij_betw ?f (Field ?L) (Field ?R)"
unfolding Field_osum bij_betw_def inj_on_def by (auto simp: image_Un image_iff)
moreover
have "compat ?L ?R ?f"
proof (unfold compat_def, safe)
fix a b
assume "(a, b) \<in> ?L"
thus "(?f a, ?f b) \<in> ?R"
unfolding osum_def[of "r +o s" t] osum_def[of r "s +o t"] Field_osum
unfolding osum_def Field_osum image_iff image_Un map_pair_def
by fastforce
qed
ultimately have "iso ?L ?R ?f" using r s t by (subst iso_iff3) (auto intro: osum_Well_order)
thus ?thesis using r s t unfolding ordIso_def by (auto intro: osum_Well_order)
qed
lemma osum_monoR:
assumes "s <o t"
shows "r +o s <o r +o t" (is "?L <o ?R")
proof -
from assms obtain f where s: "Well_order s" and t:" Well_order t" and "embedS s t f"
unfolding ordLess_def by blast
hence *: "inj_on f (Field s)" "compat s t f" "ofilter t (f ` Field s)" "f ` Field s \<subset> Field t"
using embed_iff_compat_inj_on_ofilter[OF s t, of f] embedS_iff[OF s, of t f]
unfolding embedS_def by auto
let ?f = "sum_map id f"
from *(1) have "inj_on ?f (Field ?L)" unfolding Field_osum inj_on_def by fastforce
moreover
from *(2,4) have "compat ?L ?R ?f" unfolding compat_def osum_def map_pair_def by fastforce
moreover
interpret t!: wo_rel t by unfold_locales (rule t)
interpret rt!: wo_rel ?R by unfold_locales (rule osum_Well_order[OF r t])
from *(3) have "ofilter ?R (?f ` Field ?L)"
unfolding t.ofilter_def rt.ofilter_def Field_osum image_Un image_image rel.under_def
by (auto simp: osum_def intro!: imageI) (auto simp: Field_def)
ultimately have "embed ?L ?R ?f" using embed_iff_compat_inj_on_ofilter[of ?L ?R ?f]
by (auto intro: osum_Well_order r s t)
moreover
from *(4) have "?f ` Field ?L \<subset> Field ?R" unfolding Field_osum image_Un image_image by auto
ultimately have "embedS ?L ?R ?f" using embedS_iff[OF osum_Well_order[OF r s], of ?R ?f] by auto
thus ?thesis unfolding ordLess_def by (auto intro: osum_Well_order r s t)
qed
lemma osum_monoL:
assumes "r \<le>o s"
shows "r +o t \<le>o s +o t"
proof -
from assms obtain f where f: "\<forall>a\<in>Field r. f a \<in> Field s \<and> f ` underS r a \<subseteq> underS s (f a)"
unfolding ordLeq_def2 by blast
let ?f = "sum_map f id"
from f have "\<forall>a\<in>Field (r +o t).
?f a \<in> Field (s +o t) \<and> ?f ` underS (r +o t) a \<subseteq> underS (s +o t) (?f a)"
unfolding Field_osum rel.underS_def by (fastforce simp: osum_def)
thus ?thesis unfolding ordLeq_def2 by (auto intro: osum_Well_order r s t)
qed
lemma oprod_ozeroL: "ozero *o r =o ozero"
using ozero_ordIso unfolding ozero_def by simp
lemma oprod_ozeroR: "r *o ozero =o ozero"
using ozero_ordIso unfolding ozero_def by simp
lemma oprod_ooneR: "r *o oone =o r" (is "?L =o ?R")
proof -
have "bij_betw fst (Field ?L) (Field ?R)" unfolding Field_oprod bij_betw_def inj_on_def by simp
moreover have "compat ?L ?R fst" unfolding compat_def oprod_def by auto
ultimately have "iso ?L ?R fst" using r oone_Well_order
by (subst iso_iff3) (auto intro: oprod_Well_order)
thus ?thesis using r oone_Well_order unfolding ordIso_def by (auto intro: oprod_Well_order)
qed
lemma oprod_ooneL: "oone *o r =o r" (is "?L =o ?R")
proof -
have "bij_betw snd (Field ?L) (Field ?R)" unfolding Field_oprod bij_betw_def inj_on_def by simp
moreover have "Refl r" by (rule wo_rel.REFL[unfolded wo_rel_def, OF r])
hence "compat ?L ?R snd" unfolding compat_def oprod_def refl_on_def by auto
ultimately have "iso ?L ?R snd" using r oone_Well_order
by (subst iso_iff3) (auto intro: oprod_Well_order)
thus ?thesis using r oone_Well_order unfolding ordIso_def by (auto intro: oprod_Well_order)
qed
lemma oprod_monoR:
assumes "ozero <o r" "s <o t"
shows "r *o s <o r *o t" (is "?L <o ?R")
proof -
from assms obtain f where s: "Well_order s" and t:" Well_order t" and "embedS s t f"
unfolding ordLess_def by blast
hence *: "inj_on f (Field s)" "compat s t f" "ofilter t (f ` Field s)" "f ` Field s \<subset> Field t"
using embed_iff_compat_inj_on_ofilter[OF s t, of f] embedS_iff[OF s, of t f]
unfolding embedS_def by auto
let ?f = "map_pair id f"
from *(1) have "inj_on ?f (Field ?L)" unfolding Field_oprod inj_on_def by fastforce
moreover
from *(2,4) the_inv_into_f_f[OF *(1)] have "compat ?L ?R ?f" unfolding compat_def oprod_def
by auto (metis rel.well_order_on_domain t, metis rel.well_order_on_domain s)
moreover
interpret t!: wo_rel t by unfold_locales (rule t)
interpret rt!: wo_rel ?R by unfold_locales (rule oprod_Well_order[OF r t])
from *(3) have "ofilter ?R (?f ` Field ?L)"
unfolding t.ofilter_def rt.ofilter_def Field_oprod rel.under_def
by (auto simp: oprod_def image_iff) (fast | metis r rel.well_order_on_domain)+
ultimately have "embed ?L ?R ?f" using embed_iff_compat_inj_on_ofilter[of ?L ?R ?f]
by (auto intro: oprod_Well_order r s t)
moreover
from not_ordLess_ordIso[OF assms(1)] have "r \<noteq> {}" by (metis ozero_def ozero_ordIso)
hence "Field r \<noteq> {}" unfolding Field_def by auto
with *(4) have "?f ` Field ?L \<subset> Field ?R" unfolding Field_oprod
by auto (metis SigmaD2 SigmaI map_pair_surj_on)
ultimately have "embedS ?L ?R ?f" using embedS_iff[OF oprod_Well_order[OF r s], of ?R ?f] by auto
thus ?thesis unfolding ordLess_def by (auto intro: oprod_Well_order r s t)
qed
lemma oprod_monoL:
assumes "r \<le>o s"
shows "r *o t \<le>o s *o t"
proof -
from assms obtain f where f: "\<forall>a\<in>Field r. f a \<in> Field s \<and> f ` underS r a \<subseteq> underS s (f a)"
unfolding ordLeq_def2 by blast
let ?f = "map_pair f id"
from f have "\<forall>a\<in>Field (r *o t).
?f a \<in> Field (s *o t) \<and> ?f ` underS (r *o t) a \<subseteq> underS (s *o t) (?f a)"
unfolding Field_oprod rel.underS_def unfolding map_pair_def oprod_def by auto
thus ?thesis unfolding ordLeq_def2 by (auto intro: oprod_Well_order r s t)
qed
lemma oprod_assoc: "(r *o s) *o t =o r *o s *o t" (is "?L =o ?R")
proof -
let ?f = "\<lambda>((a,b),c). (a,b,c)"
have "bij_betw ?f (Field ?L) (Field ?R)"
unfolding Field_oprod bij_betw_def inj_on_def by (auto simp: image_Un image_iff)
moreover
have "compat ?L ?R ?f"
proof (unfold compat_def, safe)
fix a1 a2 a3 b1 b2 b3
assume "(((a1, a2), a3), ((b1, b2), b3)) \<in> ?L"
thus "((a1, a2, a3), (b1, b2, b3)) \<in> ?R"
unfolding oprod_def[of "r *o s" t] oprod_def[of r "s *o t"] Field_oprod
unfolding oprod_def Field_oprod image_iff image_Un by fast
qed
ultimately have "iso ?L ?R ?f" using r s t by (subst iso_iff3) (auto intro: oprod_Well_order)
thus ?thesis using r s t unfolding ordIso_def by (auto intro: oprod_Well_order)
qed
lemma oprod_osum: "r *o (s +o t) =o r *o s +o r *o t" (is "?L =o ?R")
proof -
let ?f = "\<lambda>(a,bc). case bc of Inl b \<Rightarrow> Inl (a, b) | Inr c \<Rightarrow> Inr (a, c)"
have "bij_betw ?f (Field ?L) (Field ?R)" unfolding Field_oprod Field_osum bij_betw_def inj_on_def
by (fastforce simp: image_Un image_iff split: sum.splits)
moreover
have "compat ?L ?R ?f"
proof (unfold compat_def, intro allI impI)
fix a b
assume "(a, b) \<in> ?L"
thus "(?f a, ?f b) \<in> ?R"
unfolding oprod_def[of r "s +o t"] osum_def[of "r *o s" "r *o t"] Field_oprod Field_osum
unfolding oprod_def osum_def Field_oprod Field_osum image_iff image_Un by auto
qed
ultimately have "iso ?L ?R ?f" using r s t
by (subst iso_iff3) (auto intro: oprod_Well_order osum_Well_order)
thus ?thesis using r s t unfolding ordIso_def by (auto intro: oprod_Well_order osum_Well_order)
qed
lemma ozero_oexp: "\<not> (s =o ozero) \<Longrightarrow> ozero ^o s =o ozero"
unfolding oexp_def[OF ozero_Well_order s] FinFunc_def
by simp (metis Func_emp2 bot.extremum_uniqueI emptyE rel.well_order_on_domain s subrelI)
lemma oone_oexp: "oone ^o s =o oone" (is "?L =o ?R")
by (rule oone_ordIso_oexp[OF ordIso_reflexive[OF oone_Well_order] s])
lemma oexp_monoR:
assumes "oone <o r" "s <o t"
shows "r ^o s <o r ^o t" (is "?L <o ?R")
proof -
interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s)
interpret rt!: wo_rel2 r t by unfold_locales (rule r, rule t)
interpret rexpt!: wo_rel "r ^o t" by unfold_locales (rule rt.oexp_Well_order)
interpret r!: wo_rel r by unfold_locales (rule r)
interpret s!: wo_rel s by unfold_locales (rule s)
interpret t!: wo_rel t by unfold_locales (rule t)
have "Field r \<noteq> {}" by (metis assms(1) internalize_ordLess not_psubset_empty)
moreover
{ assume "Field r = {r.zero}"
hence "r = {(r.zero, r.zero)}" using refl_onD[OF r.REFL, of r.zero] unfolding Field_def by auto
hence "r =o oone" by (metis oone_ordIso ordIso_symmetric)
with not_ordLess_ordIso[OF assms(1)] have False by (metis ordIso_symmetric)
}
ultimately obtain x where x: "x \<in> Field r" "r.zero \<in> Field r" "x \<noteq> r.zero"
by (metis insert_iff r.zero_in_Field subsetI subset_singletonD)
moreover from assms(2) obtain f where "embedS s t f" unfolding ordLess_def by blast
hence *: "inj_on f (Field s)" "compat s t f" "ofilter t (f ` Field s)" "f ` Field s \<subset> Field t"
using embed_iff_compat_inj_on_ofilter[OF s t, of f] embedS_iff[OF s, of t f]
unfolding embedS_def by auto
note invff = the_inv_into_f_f[OF *(1)] and injfD = inj_onD[OF *(1)]
def F \<equiv> "\<lambda>g z. if z \<in> f ` Field s then g (the_inv_into (Field s) f z) else
if z \<in> Field t then r.zero else undefined"
from *(4) x(2) the_inv_into_f_eq[OF *(1)] have FLR: "F ` Field ?L \<subseteq> Field ?R"
unfolding rt.Field_oexp rs.Field_oexp FinFunc_def Func_def fin_support_def support_def F_def
by (fastforce split: option.splits split_if_asm elim!: finite_surj[of _ _ f])
have "inj_on F (Field ?L)" unfolding rs.Field_oexp inj_on_def fun_eq_iff
proof safe
fix g h x assume "g \<in> FinFunc r s" "h \<in> FinFunc r s" "\<forall>y. F g y = F h y"
with invff show "g x = h x" unfolding F_def fun_eq_iff FinFunc_def Func_def
by auto (metis image_eqI)
qed
moreover
have "compat ?L ?R F" unfolding compat_def rs.oexp_def rt.oexp_def
proof (safe elim!: bspec[OF iffD1[OF image_subset_iff FLR[unfolded rs.Field_oexp rt.Field_oexp]]])
fix g h assume gh: "g \<in> FinFunc r s" "h \<in> FinFunc r s" "F g \<noteq> F h"
"let m = s.max_fun_diff g h in (g m, h m) \<in> r"
hence "g \<noteq> h" by auto
note max_fun_diff_in = rs.max_fun_diff_in[OF `g \<noteq> h` gh(1,2)]
and max_fun_diff_max = rs.max_fun_diff_max[OF `g \<noteq> h` gh(1,2)]
with *(4) invff *(2) have "t.max_fun_diff (F g) (F h) = f (s.max_fun_diff g h)"
unfolding t.max_fun_diff_def compat_def
by (intro t.maxim_equality) (auto simp: t.isMaxim_def F_def dest: injfD)
with gh invff max_fun_diff_in
show "let m = t.max_fun_diff (F g) (F h) in (F g m, F h m) \<in> r"
unfolding F_def Let_def by (auto simp: dest: injfD)
qed
moreover
from FLR have "ofilter ?R (F ` Field ?L)"
unfolding rexpt.ofilter_def rel.under_def rs.Field_oexp rt.Field_oexp unfolding rt.oexp_def
proof (safe elim!: imageI)
fix g h assume gh: "g \<in> FinFunc r s" "h \<in> FinFunc r t" "F g \<in> FinFunc r t"
"let m = t.max_fun_diff h (F g) in (h m, F g m) \<in> r"
thus "h \<in> F ` FinFunc r s"
proof (cases "h = F g")
case False
hence max_Field: "t.max_fun_diff h (F g) \<in> {a \<in> Field t. h a \<noteq> F g a}"
by (rule rt.max_fun_diff_in[OF _ gh(2,3)])
{ assume *: "t.max_fun_diff h (F g) \<notin> f ` Field s"
with max_Field have "F g (t.max_fun_diff h (F g)) = r.zero" unfolding F_def by auto
moreover
with * gh(4) have "h (t.max_fun_diff h (F g)) = r.zero" unfolding Let_def by auto
ultimately have False using max_Field gh(2,3) unfolding FinFunc_def Func_def by auto
}
hence max_f_Field: "t.max_fun_diff h (F g) \<in> f ` Field s" by blast
{ fix z assume z: "z \<in> Field t - f ` Field s"
have "(t.max_fun_diff h (F g), z) \<in> t"
proof (rule ccontr)
assume "(t.max_fun_diff h (F g), z) \<notin> t"
hence "(z, t.max_fun_diff h (F g)) \<in> t" using t.in_notinI[of "t.max_fun_diff h (F g)" z]
z max_Field by auto
hence "z \<in> f ` Field s" using *(3) max_f_Field unfolding t.ofilter_def rel.under_def
by fastforce
with z show False by blast
qed
hence "h z = r.zero" using rt.max_fun_diff_le_eq[OF _ False gh(2,3), of z]
z max_f_Field unfolding F_def by auto
} note ** = this
with *(3) gh(2) have "h = F (\<lambda>x. if x \<in> Field s then h (f x) else undefined)" using invff
unfolding F_def fun_eq_iff FinFunc_def Func_def Let_def t.ofilter_def rel.under_def by auto
moreover from gh(2) *(1,3) have "(\<lambda>x. if x \<in> Field s then h (f x) else undefined) \<in> FinFunc r s"
unfolding FinFunc_def Func_def fin_support_def support_def t.ofilter_def rel.under_def
by (auto intro: subset_inj_on elim!: finite_imageD[OF finite_subset[rotated]])
ultimately show "?thesis" by (rule image_eqI)
qed simp
qed
ultimately have "embed ?L ?R F" using embed_iff_compat_inj_on_ofilter[of ?L ?R F]
by (auto intro: oexp_Well_order r s t)
moreover
from FLR have "F ` Field ?L \<subset> Field ?R"
proof (intro psubsetI)
from *(4) obtain z where z: "z \<in> Field t" "z \<notin> f ` Field s" by auto
def h \<equiv> "\<lambda>z'. if z' \<in> Field t then if z' = z then x else r.zero else undefined"
from z x(3) have "rt.SUPP h = {z}" unfolding support_def h_def by simp
with x have "h \<in> Field ?R" unfolding h_def rt.Field_oexp FinFunc_def Func_def fin_support_def
by auto
moreover
{ fix g
from z have "F g z = r.zero" "h z = x" unfolding support_def h_def F_def by auto
with x(3) have "F g \<noteq> h" unfolding fun_eq_iff by fastforce
}
hence "h \<notin> F ` Field ?L" by blast
ultimately show "F ` Field ?L \<noteq> Field ?R" by blast
qed
ultimately have "embedS ?L ?R F" using embedS_iff[OF rs.oexp_Well_order, of ?R F] by auto
thus ?thesis unfolding ordLess_def using r s t by (auto intro: oexp_Well_order)
qed
lemma oexp_monoL:
assumes "r \<le>o s"
shows "r ^o t \<le>o s ^o t"
proof -
interpret rt!: wo_rel2 r t by unfold_locales (rule r, rule t)
interpret st!: wo_rel2 s t by unfold_locales (rule s, rule t)
interpret r!: wo_rel r by unfold_locales (rule r)
interpret s!: wo_rel s by unfold_locales (rule s)
interpret t!: wo_rel t by unfold_locales (rule t)
show ?thesis
proof (cases "t = {}")
case True thus ?thesis using r s unfolding ordLeq_def2 rel.underS_def by auto
next
case False thus ?thesis
proof (cases "r = {}")
case True thus ?thesis using t `t \<noteq> {}` st.oexp_Well_order ozero_ordLeq[unfolded ozero_def]
by auto
next
case False
from assms obtain f where f: "embed r s f" unfolding ordLeq_def by blast
hence f_underS: "\<forall>a\<in>Field r. f a \<in> Field s \<and> f ` underS r a \<subseteq> underS s (f a)"
using embed_in_Field[OF rt.rWELL f] embed_underS2[OF rt.rWELL st.rWELL f] by auto
from f `t \<noteq> {}` False have *: "Field r \<noteq> {}" "Field s \<noteq> {}" "Field t \<noteq> {}"
unfolding Field_def embed_def rel.under_def bij_betw_def by auto
with f obtain x where "s.zero = f x" "x \<in> Field r" unfolding embed_def bij_betw_def
using embed_in_Field[OF r.WELL f] s.zero_under set_mp[OF r.under_Field] by blast
with f have fz: "f r.zero = s.zero" and inj: "inj_on f (Field r)" and compat: "compat r s f"
unfolding embed_iff_compat_inj_on_ofilter[OF r s] compat_def
by (fastforce intro: s.leq_zero_imp)+
let ?f = "\<lambda>g x. if x \<in> Field t then f (g x) else undefined"
{ fix g assume g: "g \<in> Field (r ^o t)"
with fz f_underS have Field_fg: "?f g \<in> Field (s ^o t)"
unfolding st.Field_oexp rt.Field_oexp FinFunc_def Func_def fin_support_def support_def
by (auto elim!: finite_subset[rotated])
moreover
have "?f ` underS (r ^o t) g \<subseteq> underS (s ^o t) (?f g)"
proof safe
fix h
assume h_underS: "h \<in> underS (r ^o t) g"
hence "h \<in> Field (r ^o t)" unfolding rel.underS_def Field_def by auto
with fz f_underS have Field_fh: "?f h \<in> Field (s ^o t)"
unfolding st.Field_oexp rt.Field_oexp FinFunc_def Func_def fin_support_def support_def
by (auto elim!: finite_subset[rotated])
from h_underS have "h \<noteq> g" and hg: "(h, g) \<in> rt.oexp" unfolding rel.underS_def by auto
with f inj have neq: "?f h \<noteq> ?f g"
unfolding fun_eq_iff inj_on_def rt.oexp_def Option.map_def FinFunc_def Func_def Let_def
by simp metis
moreover
with hg have "t.max_fun_diff (?f h) (?f g) = t.max_fun_diff h g" unfolding rt.oexp_def
using rt.max_fun_diff[OF `h \<noteq> g`] rt.max_fun_diff_in[OF `h \<noteq> g`]
by (subst t.max_fun_diff_def, intro t.maxim_equality)
(auto simp: t.isMaxim_def intro: inj_onD[OF inj] intro!: rt.max_fun_diff_max)
with Field_fg Field_fh hg fz f_underS compat neq have "(?f h, ?f g) \<in> st.oexp"
using rt.max_fun_diff[OF `h \<noteq> g`] rt.max_fun_diff_in[OF `h \<noteq> g`] unfolding st.Field_oexp
unfolding rt.oexp_def st.oexp_def Let_def compat_def by auto
ultimately show "?f h \<in> underS (s ^o t) (?f g)" unfolding rel.underS_def by auto
qed
ultimately have "?f g \<in> Field (s ^o t) \<and> ?f ` underS (r ^o t) g \<subseteq> underS (s ^o t) (?f g)"
by blast
}
thus ?thesis unfolding ordLeq_def2 by (fastforce intro: oexp_Well_order r s t)
qed
qed
qed
lemma ordLeq_oexp2:
assumes "oone <o r"
shows "s \<le>o r ^o s"
proof -
interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s)
interpret r!: wo_rel r by unfold_locales (rule r)
interpret s!: wo_rel s by unfold_locales (rule s)
from assms rel.well_order_on_domain[OF r] obtain x where
x: "x \<in> Field r" "r.zero \<in> Field r" "x \<noteq> r.zero"
unfolding ordLess_def oone_def embedS_def[abs_def] bij_betw_def embed_def rel.under_def
by (auto simp: image_def)
(metis equals0D insert_not_empty r.under_def r.zero_in_Field rel.under_empty)
let ?f = "\<lambda>a b. if b \<in> Field s then if b = a then x else r.zero else undefined"
from x(3) have SUPP: "\<And>y. y \<in> Field s \<Longrightarrow> rs.SUPP (?f y) = {y}" unfolding support_def by auto
{ fix y assume y: "y \<in> Field s"
with x(1,2) SUPP have "?f y \<in> Field (r ^o s)" unfolding rs.Field_oexp
by (auto simp: FinFunc_def Func_def fin_support_def)
moreover
have "?f ` underS s y \<subseteq> underS (r ^o s) (?f y)"
proof safe
fix z
assume "z \<in> underS s y"
hence z: "z \<noteq> y" "(z, y) \<in> s" "z \<in> Field s" unfolding rel.underS_def Field_def by auto
from x(3) y z(1,3) have "?f z \<noteq> ?f y" unfolding fun_eq_iff by auto
moreover
{ from x(1,2) have "?f z \<in> FinFunc r s" "?f y \<in> FinFunc r s"
unfolding FinFunc_def Func_def fin_support_def by (auto simp: SUPP[OF z(3)] SUPP[OF y])
moreover
from x(3) y z(1,2) refl_onD[OF s.REFL] have "s.max_fun_diff (?f z) (?f y) = y"
unfolding rs.max_fun_diff_alt SUPP[OF z(3)] SUPP[OF y]
by (intro s.maxim_equality) (auto simp: s.isMaxim_def)
ultimately have "(?f z, ?f y) \<in> rs.oexp" using y x(1)
unfolding rs.oexp_def Let_def by auto
}
ultimately show "?f z \<in> underS (r ^o s) (?f y)" unfolding rel.underS_def by blast
qed
ultimately have "?f y \<in> Field (r ^o s) \<and> ?f ` underS s y \<subseteq> underS (r ^o s) (?f y)" by blast
}
thus ?thesis unfolding ordLeq_def2 by (fast intro: oexp_Well_order r s)
qed
lemma FinFunc_osum:
"fg \<in> FinFunc r (s +o t) = (fg o Inl \<in> FinFunc r s \<and> fg o Inr \<in> FinFunc r t)"
(is "?L = (?R1 \<and> ?R2)")
proof safe
assume ?L
from `?L` show ?R1 unfolding FinFunc_def Field_osum Func_def Int_iff fin_support_Field_osum o_def
by (auto split: sum.splits)
from `?L` show ?R2 unfolding FinFunc_def Field_osum Func_def Int_iff fin_support_Field_osum o_def
by (auto split: sum.splits)
next
assume ?R1 ?R2
thus "?L" unfolding FinFunc_def Field_osum Func_def
by (auto simp: fin_support_Field_osum o_def image_iff split: sum.splits) (metis sumE)
qed
lemma max_fun_diff_eq_Inl:
assumes "wo_rel.max_fun_diff (s +o t) (sum_case f1 g1) (sum_case f2 g2) = Inl x"
"sum_case f1 g1 \<noteq> sum_case f2 g2"
"sum_case f1 g1 \<in> FinFunc r (s +o t)" "sum_case f2 g2 \<in> FinFunc r (s +o t)"
shows "wo_rel.max_fun_diff s f1 f2 = x" (is ?P) "g1 = g2" (is ?Q)
proof -
interpret st!: wo_rel "s +o t" by unfold_locales (rule osum_Well_order[OF s t])
interpret s!: wo_rel s by unfold_locales (rule s)
interpret rst!: wo_rel2 r "s +o t" by unfold_locales (rule r, rule osum_Well_order[OF s t])
from assms(1) have *: "st.isMaxim {a \<in> Field (s +o t). sum_case f1 g1 a \<noteq> sum_case f2 g2 a} (Inl x)"
using rst.isMaxim_max_fun_diff[OF assms(2-4)] by simp
hence "s.isMaxim {a \<in> Field s. f1 a \<noteq> f2 a} x"
unfolding st.isMaxim_def s.isMaxim_def Field_osum by (auto simp: osum_def)
thus ?P unfolding s.max_fun_diff_def by (rule s.maxim_equality)
from assms(3,4) have **: "g1 \<in> FinFunc r t" "g2 \<in> FinFunc r t" unfolding FinFunc_osum
by (auto simp: o_def)
show ?Q
proof
fix x
from * ** show "g1 x = g2 x" unfolding st.isMaxim_def Field_osum FinFunc_def Func_def fun_eq_iff
unfolding osum_def by (case_tac "x \<in> Field t") auto
qed
qed
lemma max_fun_diff_eq_Inr:
assumes "wo_rel.max_fun_diff (s +o t) (sum_case f1 g1) (sum_case f2 g2) = Inr x"
"sum_case f1 g1 \<noteq> sum_case f2 g2"
"sum_case f1 g1 \<in> FinFunc r (s +o t)" "sum_case f2 g2 \<in> FinFunc r (s +o t)"
shows "wo_rel.max_fun_diff t g1 g2 = x" (is ?P) "g1 \<noteq> g2" (is ?Q)
proof -
interpret st!: wo_rel "s +o t" by unfold_locales (rule osum_Well_order[OF s t])
interpret t!: wo_rel t by unfold_locales (rule t)
interpret rst!: wo_rel2 r "s +o t" by unfold_locales (rule r, rule osum_Well_order[OF s t])
from assms(1) have *: "st.isMaxim {a \<in> Field (s +o t). sum_case f1 g1 a \<noteq> sum_case f2 g2 a} (Inr x)"
using rst.isMaxim_max_fun_diff[OF assms(2-4)] by simp
hence "t.isMaxim {a \<in> Field t. g1 a \<noteq> g2 a} x"
unfolding st.isMaxim_def t.isMaxim_def Field_osum by (auto simp: osum_def)
thus ?P ?Q unfolding t.max_fun_diff_def fun_eq_iff
by (auto intro: t.maxim_equality simp: t.isMaxim_def)
qed
lemma oexp_osum: "r ^o (s +o t) =o (r ^o s) *o (r ^o t)" (is "?R =o ?L")
proof (rule ordIso_symmetric)
interpret rst!: wo_rel2 r "s +o t" by unfold_locales (rule r, rule osum_Well_order[OF s t])
interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s)
interpret rt!: wo_rel2 r t by unfold_locales (rule r, rule t)
let ?f = "\<lambda>(f, g). sum_case f g"
have "bij_betw ?f (Field ?L) (Field ?R)"
unfolding bij_betw_def rst.Field_oexp rs.Field_oexp rt.Field_oexp Field_oprod proof (intro conjI)
show "inj_on ?f (FinFunc r s \<times> FinFunc r t)" unfolding inj_on_def
by (auto simp: fun_eq_iff split: sum.splits)
show "?f ` (FinFunc r s \<times> FinFunc r t) = FinFunc r (s +o t)"
proof safe
fix fg assume "fg \<in> FinFunc r (s +o t)"
thus "fg \<in> ?f ` (FinFunc r s \<times> FinFunc r t)"
by (intro image_eqI[of _ _ "(fg o Inl, fg o Inr)"])
(auto simp: FinFunc_osum fun_eq_iff split: sum.splits)
qed (auto simp: FinFunc_osum o_def)
qed
moreover have "compat ?L ?R ?f"
unfolding compat_def rst.Field_oexp rs.Field_oexp rt.Field_oexp oprod_def
unfolding rst.oexp_def Let_def rs.oexp_def rt.oexp_def
by (fastforce simp: Field_osum FinFunc_osum o_def split: sum.splits
dest: max_fun_diff_eq_Inl max_fun_diff_eq_Inr)
ultimately have "iso ?L ?R ?f" using r s t
by (subst iso_iff3) (auto intro: oexp_Well_order oprod_Well_order osum_Well_order)
thus "?L =o ?R" using r s t unfolding ordIso_def
by (auto intro: oexp_Well_order oprod_Well_order osum_Well_order)
qed
definition "rev_curr f b = (if b \<in> Field t then \<lambda>a. f (a, b) else undefined)"
lemma rev_curr_FinFunc:
assumes Field: "Field r \<noteq> {}"
shows "rev_curr ` (FinFunc r (s *o t)) = FinFunc (r ^o s) t"
proof safe
interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s)
interpret rst!: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
fix g assume g: "g \<in> FinFunc r (s *o t)"
hence "finite (rst.SUPP (rev_curr g))" "\<forall>x \<in> Field t. finite (rs.SUPP (rev_curr g x))"
unfolding FinFunc_def Field_oprod rs.Field_oexp Func_def fin_support_def support_def
rs.zero_oexp[OF Field] rev_curr_def by (auto simp: fun_eq_iff rs.const_def elim!: finite_surj)
with g show "rev_curr g \<in> FinFunc (r ^o s) t"
unfolding FinFunc_def Field_oprod rs.Field_oexp Func_def
by (auto simp: rev_curr_def fin_support_def)
next
interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s)
interpret rst!: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
fix fg assume *: "fg \<in> FinFunc (r ^o s) t"
let ?g = "\<lambda>(a, b). if (a, b) \<in> Field (s *o t) then fg b a else undefined"
show "fg \<in> rev_curr ` FinFunc r (s *o t)"
proof (rule image_eqI[of _ _ ?g])
show "fg = rev_curr ?g"
proof
fix x
from * show "fg x = rev_curr ?g x"
unfolding FinFunc_def rs.Field_oexp Func_def rev_curr_def Field_oprod by auto
qed
next
have **: "(\<Union>g \<in> fg ` Field t. rs.SUPP g) =
(\<Union>g \<in> fg ` Field t - {rs.const}. rs.SUPP g)"
unfolding support_def by auto
from * have "\<forall>g \<in> fg ` Field t. finite (rs.SUPP g)" "finite (rst.SUPP fg)"
unfolding rs.Field_oexp FinFunc_def Func_def fin_support_def these_def by force+
moreover hence "finite (fg ` Field t - {rs.const})" using *
unfolding support_def rs.zero_oexp[OF Field] FinFunc_def Func_def
by (elim finite_surj[of _ _ fg]) (fastforce simp: image_iff these_def)
ultimately have "finite ((\<Union>g \<in> fg ` Field t. rs.SUPP g) \<times> rst.SUPP fg)"
by (subst **) (auto intro!: finite_cartesian_product)
with * show "?g \<in> FinFunc r (s *o t)"
unfolding Field_oprod rs.Field_oexp FinFunc_def Func_def fin_support_def these_def
support_def rs.zero_oexp[OF Field] by (auto elim!: finite_subset[rotated])
qed
qed
lemma rev_curr_app_FinFunc[elim!]:
"\<lbrakk>f \<in> FinFunc r (s *o t); z \<in> Field t\<rbrakk> \<Longrightarrow> rev_curr f z \<in> FinFunc r s"
unfolding rev_curr_def FinFunc_def Func_def Field_oprod fin_support_def support_def
by (auto elim: finite_surj)
lemma max_fun_diff_oprod:
assumes Field: "Field r \<noteq> {}" and "f \<noteq> g" "f \<in> FinFunc r (s *o t)" "g \<in> FinFunc r (s *o t)"
defines "m \<equiv> wo_rel.max_fun_diff t (rev_curr f) (rev_curr g)"
shows "wo_rel.max_fun_diff (s *o t) f g =
(wo_rel.max_fun_diff s (rev_curr f m) (rev_curr g m), m)"
proof -
interpret st!: wo_rel "s *o t" by unfold_locales (rule oprod_Well_order[OF s t])
interpret s!: wo_rel s by unfold_locales (rule s)
interpret t!: wo_rel t by unfold_locales (rule t)
interpret r_st!: wo_rel2 r "s *o t" by unfold_locales (rule r, rule oprod_Well_order[OF s t])
interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s)
interpret rst!: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
from fun_unequal_in_support[OF assms(2), of "Field (s *o t)" "Field r" "Field r"] assms(3,4)
have diff1: "rev_curr f \<noteq> rev_curr g"
"rev_curr f \<in> FinFunc (r ^o s) t" "rev_curr g \<in> FinFunc (r ^o s) t" using rev_curr_FinFunc[OF Field]
unfolding fun_eq_iff rev_curr_def[abs_def] FinFunc_def support_def Field_oprod
by auto fast
hence diff2: "rev_curr f m \<noteq> rev_curr g m" "rev_curr f m \<in> FinFunc r s" "rev_curr g m \<in> FinFunc r s"
using rst.max_fun_diff[OF diff1] assms(3,4) rst.max_fun_diff_in unfolding m_def by auto
show ?thesis unfolding st.max_fun_diff_def
proof (intro st.maxim_equality, unfold st.isMaxim_def Field_oprod, safe)
show "s.max_fun_diff (rev_curr f m) (rev_curr g m) \<in> Field s"
using rs.max_fun_diff_in[OF diff2] by auto
next
show "m \<in> Field t" using rst.max_fun_diff_in[OF diff1] unfolding m_def by auto
next
assume "f (s.max_fun_diff (rev_curr f m) (rev_curr g m), m) =
g (s.max_fun_diff (rev_curr f m) (rev_curr g m), m)"
(is "f (?x, m) = g (?x, m)")
hence "rev_curr f m ?x = rev_curr g m ?x" unfolding rev_curr_def by auto
with rs.max_fun_diff[OF diff2] show False by auto
next
fix x y assume "f (x, y) \<noteq> g (x, y)" "x \<in> Field s" "y \<in> Field t"
thus "((x, y), (s.max_fun_diff (rev_curr f m) (rev_curr g m), m)) \<in> s *o t"
using rst.max_fun_diff_in[OF diff1] rs.max_fun_diff_in[OF diff2] diff1 diff2
rst.max_fun_diff_max[OF diff1, of y] rs.max_fun_diff_le_eq[OF _ diff2, of x]
unfolding oprod_def m_def rev_curr_def fun_eq_iff by auto (metis s.in_notinI)
qed
qed
lemma oexp_oexp: "(r ^o s) ^o t =o r ^o (s *o t)" (is "?R =o ?L")
proof (cases "r = {}")
case True
interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s)
interpret rst!: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
show ?thesis
proof (cases "s = {} \<or> t = {}")
case True with `r = {}` show ?thesis
by (auto simp: oexp_empty[OF oexp_Well_order[OF Well_order_empty s]]
intro!: ordIso_transitive[OF ordIso_symmetric[OF oone_ordIso] oone_ordIso]
ordIso_transitive[OF oone_ordIso_oexp[OF ordIso_symmetric[OF oone_ordIso] t] oone_ordIso])
next
case False
moreover hence "s *o t \<noteq> {}" unfolding oprod_def Field_def by fastforce
ultimately show ?thesis using `r = {}` ozero_ordIso
by (auto simp add: s t oprod_Well_order ozero_def)
qed
next
case False
hence Field: "Field r \<noteq> {}" by (metis Field_def Range_empty_iff Un_empty)
show ?thesis
proof (rule ordIso_symmetric)
interpret r_st!: wo_rel2 r "s *o t" by unfold_locales (rule r, rule oprod_Well_order[OF s t])
interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s)
interpret rst!: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
have bij: "bij_betw rev_curr (Field ?L) (Field ?R)"
unfolding bij_betw_def r_st.Field_oexp rst.Field_oexp Field_oprod proof (intro conjI)
show "inj_on rev_curr (FinFunc r (s *o t))"
unfolding inj_on_def FinFunc_def Func_def Field_oprod rs.Field_oexp rev_curr_def[abs_def]
by (auto simp: fun_eq_iff) metis
show "rev_curr ` (FinFunc r (s *o t)) = FinFunc (r ^o s) t" by (rule rev_curr_FinFunc[OF Field])
qed
moreover
have "compat ?L ?R rev_curr"
unfolding compat_def proof safe
fix fg1 fg2 assume fg: "(fg1, fg2) \<in> r ^o (s *o t)"
show "(rev_curr fg1, rev_curr fg2) \<in> r ^o s ^o t"
proof (cases "fg1 = fg2")
assume "fg1 \<noteq> fg2"
with fg show ?thesis
using rst.max_fun_diff_in[of "rev_curr fg1" "rev_curr fg2"]
max_fun_diff_oprod[OF Field, of fg1 fg2] rev_curr_FinFunc[OF Field, symmetric]
unfolding r_st.Field_oexp rs.Field_oexp rst.Field_oexp unfolding r_st.oexp_def rst.oexp_def
by (auto simp: rs.oexp_def Let_def) (auto simp: rev_curr_def[abs_def])
next
assume "fg1 = fg2"
with fg bij show ?thesis unfolding r_st.Field_oexp rs.Field_oexp rst.Field_oexp bij_betw_def
by (auto simp: r_st.oexp_def rst.oexp_def)
qed
qed
ultimately have "iso ?L ?R rev_curr" using r s t
by (subst iso_iff3) (auto intro: oexp_Well_order oprod_Well_order)
thus "?L =o ?R" using r s t unfolding ordIso_def
by (auto intro: oexp_Well_order oprod_Well_order)
qed
qed
end (* context with 3 wellorders *)
end