header {* Greatest Fixed Point Operation on Bounded Natural Functors *}
theory BNF_GFP
imports BNF_FP_Base String
keywords
"codatatype" :: thy_decl and
"primcorecursive" :: thy_goal and
"primcorec" :: thy_decl
begin
setup {*
Sign.const_alias @{binding proj} @{const_name Equiv_Relations.proj}
*}
lemma one_pointE: "[|!!x. s = x ==> P|] ==> P"
by simp
lemma obj_sumE: "[|∀x. s = Inl x --> P; ∀x. s = Inr x --> P|] ==> P"
by (cases s) auto
lemma not_TrueE: "¬ True ==> P"
by (erule notE, rule TrueI)
lemma neq_eq_eq_contradict: "[|t ≠ u; s = t; s = u|] ==> P"
by fast
lemma case_sum_expand_Inr: "f o Inl = g ==> f x = case_sum g (f o Inr) x"
by (auto split: sum.splits)
lemma case_sum_expand_Inr': "f o Inl = g ==> h = f o Inr <-> case_sum g h = f"
apply rule
apply (rule ext, force split: sum.split)
by (rule ext, metis case_sum_o_inj(2))
lemma converse_Times: "(A × B) ^-1 = B × A"
by fast
lemma equiv_proj:
assumes e: "equiv A R" and "z ∈ R"
shows "(proj R o fst) z = (proj R o snd) z"
proof -
from assms(2) have z: "(fst z, snd z) ∈ R" by auto
with e have "!!x. (fst z, x) ∈ R ==> (snd z, x) ∈ R" "!!x. (snd z, x) ∈ R ==> (fst z, x) ∈ R"
unfolding equiv_def sym_def trans_def by blast+
then show ?thesis unfolding proj_def[abs_def] by auto
qed
definition image2 where "image2 A f g = {(f a, g a) | a. a ∈ A}"
lemma Id_on_Gr: "Id_on A = Gr A id"
unfolding Id_on_def Gr_def by auto
lemma image2_eqI: "[|b = f x; c = g x; x ∈ A|] ==> (b, c) ∈ image2 A f g"
unfolding image2_def by auto
lemma IdD: "(a, b) ∈ Id ==> a = b"
by auto
lemma image2_Gr: "image2 A f g = (Gr A f)^-1 O (Gr A g)"
unfolding image2_def Gr_def by auto
lemma GrD1: "(x, fx) ∈ Gr A f ==> x ∈ A"
unfolding Gr_def by simp
lemma GrD2: "(x, fx) ∈ Gr A f ==> f x = fx"
unfolding Gr_def by simp
lemma Gr_incl: "Gr A f ⊆ A <*> B <-> f ` A ⊆ B"
unfolding Gr_def by auto
lemma subset_Collect_iff: "B ⊆ A ==> (B ⊆ {x ∈ A. P x}) = (∀x ∈ B. P x)"
by blast
lemma subset_CollectI: "B ⊆ A ==> (!!x. x ∈ B ==> Q x ==> P x) ==> ({x ∈ B. Q x} ⊆ {x ∈ A. P x})"
by blast
lemma in_rel_Collect_split_eq: "in_rel (Collect (split X)) = X"
unfolding fun_eq_iff by auto
lemma Collect_split_in_rel_leI: "X ⊆ Y ==> X ⊆ Collect (split (in_rel Y))"
by auto
lemma Collect_split_in_rel_leE: "X ⊆ Collect (split (in_rel Y)) ==> (X ⊆ Y ==> R) ==> R"
by force
lemma conversep_in_rel: "(in_rel R)¯¯ = in_rel (R¯)"
unfolding fun_eq_iff by auto
lemma relcompp_in_rel: "in_rel R OO in_rel S = in_rel (R O S)"
unfolding fun_eq_iff by auto
lemma in_rel_Gr: "in_rel (Gr A f) = Grp A f"
unfolding Gr_def Grp_def fun_eq_iff by auto
definition relImage where
"relImage R f ≡ {(f a1, f a2) | a1 a2. (a1,a2) ∈ R}"
definition relInvImage where
"relInvImage A R f ≡ {(a1, a2) | a1 a2. a1 ∈ A ∧ a2 ∈ A ∧ (f a1, f a2) ∈ R}"
lemma relImage_Gr:
"[|R ⊆ A × A|] ==> relImage R f = (Gr A f)^-1 O R O Gr A f"
unfolding relImage_def Gr_def relcomp_def by auto
lemma relInvImage_Gr: "[|R ⊆ B × B|] ==> relInvImage A R f = Gr A f O R O (Gr A f)^-1"
unfolding Gr_def relcomp_def image_def relInvImage_def by auto
lemma relImage_mono:
"R1 ⊆ R2 ==> relImage R1 f ⊆ relImage R2 f"
unfolding relImage_def by auto
lemma relInvImage_mono:
"R1 ⊆ R2 ==> relInvImage A R1 f ⊆ relInvImage A R2 f"
unfolding relInvImage_def by auto
lemma relInvImage_Id_on:
"(!!a1 a2. f a1 = f a2 <-> a1 = a2) ==> relInvImage A (Id_on B) f ⊆ Id"
unfolding relInvImage_def Id_on_def by auto
lemma relInvImage_UNIV_relImage:
"R ⊆ relInvImage UNIV (relImage R f) f"
unfolding relInvImage_def relImage_def by auto
lemma relImage_proj:
assumes "equiv A R"
shows "relImage R (proj R) ⊆ Id_on (A//R)"
unfolding relImage_def Id_on_def
using proj_iff[OF assms] equiv_class_eq_iff[OF assms]
by (auto simp: proj_preserves)
lemma relImage_relInvImage:
assumes "R ⊆ f ` A <*> f ` A"
shows "relImage (relInvImage A R f) f = R"
using assms unfolding relImage_def relInvImage_def by fast
lemma subst_Pair: "P x y ==> a = (x, y) ==> P (fst a) (snd a)"
by simp
lemma fst_diag_id: "(fst o (%x. (x, x))) z = id z" by simp
lemma snd_diag_id: "(snd o (%x. (x, x))) z = id z" by simp
lemma fst_diag_fst: "fst o ((λx. (x, x)) o fst) = fst" by auto
lemma snd_diag_fst: "snd o ((λx. (x, x)) o fst) = fst" by auto
lemma fst_diag_snd: "fst o ((λx. (x, x)) o snd) = snd" by auto
lemma snd_diag_snd: "snd o ((λx. (x, x)) o snd) = snd" by auto
definition Succ where "Succ Kl kl = {k . kl @ [k] ∈ Kl}"
definition Shift where "Shift Kl k = {kl. k # kl ∈ Kl}"
definition shift where "shift lab k = (λkl. lab (k # kl))"
lemma empty_Shift: "[|[] ∈ Kl; k ∈ Succ Kl []|] ==> [] ∈ Shift Kl k"
unfolding Shift_def Succ_def by simp
lemma SuccD: "k ∈ Succ Kl kl ==> kl @ [k] ∈ Kl"
unfolding Succ_def by simp
lemmas SuccE = SuccD[elim_format]
lemma SuccI: "kl @ [k] ∈ Kl ==> k ∈ Succ Kl kl"
unfolding Succ_def by simp
lemma ShiftD: "kl ∈ Shift Kl k ==> k # kl ∈ Kl"
unfolding Shift_def by simp
lemma Succ_Shift: "Succ (Shift Kl k) kl = Succ Kl (k # kl)"
unfolding Succ_def Shift_def by auto
lemma length_Cons: "length (x # xs) = Suc (length xs)"
by simp
lemma length_append_singleton: "length (xs @ [x]) = Suc (length xs)"
by simp
definition "toCard_pred A r f ≡ inj_on f A ∧ f ` A ⊆ Field r ∧ Card_order r"
definition "toCard A r ≡ SOME f. toCard_pred A r f"
lemma ex_toCard_pred:
"[||A| ≤o r; Card_order r|] ==> ∃ f. toCard_pred A r f"
unfolding toCard_pred_def
using card_of_ordLeq[of A "Field r"]
ordLeq_ordIso_trans[OF _ card_of_unique[of "Field r" r], of "|A|"]
by blast
lemma toCard_pred_toCard:
"[||A| ≤o r; Card_order r|] ==> toCard_pred A r (toCard A r)"
unfolding toCard_def using someI_ex[OF ex_toCard_pred] .
lemma toCard_inj: "[||A| ≤o r; Card_order r; x ∈ A; y ∈ A|] ==>
toCard A r x = toCard A r y <-> x = y"
using toCard_pred_toCard unfolding inj_on_def toCard_pred_def by blast
definition "fromCard A r k ≡ SOME b. b ∈ A ∧ toCard A r b = k"
lemma fromCard_toCard:
"[||A| ≤o r; Card_order r; b ∈ A|] ==> fromCard A r (toCard A r b) = b"
unfolding fromCard_def by (rule some_equality) (auto simp add: toCard_inj)
lemma Inl_Field_csum: "a ∈ Field r ==> Inl a ∈ Field (r +c s)"
unfolding Field_card_of csum_def by auto
lemma Inr_Field_csum: "a ∈ Field s ==> Inr a ∈ Field (r +c s)"
unfolding Field_card_of csum_def by auto
lemma rec_nat_0_imp: "f = rec_nat f1 (%n rec. f2 n rec) ==> f 0 = f1"
by auto
lemma rec_nat_Suc_imp: "f = rec_nat f1 (%n rec. f2 n rec) ==> f (Suc n) = f2 n (f n)"
by auto
lemma rec_list_Nil_imp: "f = rec_list f1 (%x xs rec. f2 x xs rec) ==> f [] = f1"
by auto
lemma rec_list_Cons_imp: "f = rec_list f1 (%x xs rec. f2 x xs rec) ==> f (x # xs) = f2 x xs (f xs)"
by auto
lemma not_arg_cong_Inr: "x ≠ y ==> Inr x ≠ Inr y"
by simp
lemma Collect_splitD: "x ∈ Collect (split A) ==> A (fst x) (snd x)"
by auto
definition image2p where
"image2p f g R = (λx y. ∃x' y'. R x' y' ∧ f x' = x ∧ g y' = y)"
lemma image2pI: "R x y ==> image2p f g R (f x) (g y)"
unfolding image2p_def by blast
lemma image2pE: "[|image2p f g R fx gy; (!!x y. fx = f x ==> gy = g y ==> R x y ==> P)|] ==> P"
unfolding image2p_def by blast
lemma rel_fun_iff_geq_image2p: "rel_fun R S f g = (image2p f g R ≤ S)"
unfolding rel_fun_def image2p_def by auto
lemma rel_fun_image2p: "rel_fun R (image2p f g R) f g"
unfolding rel_fun_def image2p_def by auto
subsection {* Equivalence relations, quotients, and Hilbert's choice *}
lemma equiv_Eps_in:
"[|equiv A r; X ∈ A//r|] ==> Eps (%x. x ∈ X) ∈ X"
apply (rule someI2_ex)
using in_quotient_imp_non_empty by blast
lemma equiv_Eps_preserves:
assumes ECH: "equiv A r" and X: "X ∈ A//r"
shows "Eps (%x. x ∈ X) ∈ A"
apply (rule in_mono[rule_format])
using assms apply (rule in_quotient_imp_subset)
by (rule equiv_Eps_in) (rule assms)+
lemma proj_Eps:
assumes "equiv A r" and "X ∈ A//r"
shows "proj r (Eps (%x. x ∈ X)) = X"
unfolding proj_def proof auto
fix x assume x: "x ∈ X"
thus "(Eps (%x. x ∈ X), x) ∈ r" using assms equiv_Eps_in in_quotient_imp_in_rel by fast
next
fix x assume "(Eps (%x. x ∈ X),x) ∈ r"
thus "x ∈ X" using in_quotient_imp_closed[OF assms equiv_Eps_in[OF assms]] by fast
qed
definition univ where "univ f X == f (Eps (%x. x ∈ X))"
lemma univ_commute:
assumes ECH: "equiv A r" and RES: "f respects r" and x: "x ∈ A"
shows "(univ f) (proj r x) = f x"
unfolding univ_def proof -
have prj: "proj r x ∈ A//r" using x proj_preserves by fast
hence "Eps (%y. y ∈ proj r x) ∈ A" using ECH equiv_Eps_preserves by fast
moreover have "proj r (Eps (%y. y ∈ proj r x)) = proj r x" using ECH prj proj_Eps by fast
ultimately have "(x, Eps (%y. y ∈ proj r x)) ∈ r" using x ECH proj_iff by fast
thus "f (Eps (%y. y ∈ proj r x)) = f x" using RES unfolding congruent_def by fastforce
qed
lemma univ_preserves:
assumes ECH: "equiv A r" and RES: "f respects r" and
PRES: "∀ x ∈ A. f x ∈ B"
shows "∀X ∈ A//r. univ f X ∈ B"
proof
fix X assume "X ∈ A//r"
then obtain x where x: "x ∈ A" and X: "X = proj r x" using ECH proj_image[of r A] by blast
hence "univ f X = f x" using assms univ_commute by fastforce
thus "univ f X ∈ B" using x PRES by simp
qed
ML_file "Tools/BNF/bnf_gfp_util.ML"
ML_file "Tools/BNF/bnf_gfp_tactics.ML"
ML_file "Tools/BNF/bnf_gfp.ML"
ML_file "Tools/BNF/bnf_gfp_rec_sugar_tactics.ML"
ML_file "Tools/BNF/bnf_gfp_rec_sugar.ML"
end