(* Title: HOL/BNF_Greatest_Fixpoint.thy
Author: Dmitriy Traytel, TU Muenchen
Author: Lorenz Panny, TU Muenchen
Author: Jasmin Blanchette, TU Muenchen
Copyright 2012, 2013, 2014
Greatest fixpoint (codatatype) operation on bounded natural functors.
*)
section \<open>Greatest Fixpoint (Codatatype) Operation on Bounded Natural Functors\<close>
theory BNF_Greatest_Fixpoint
imports BNF_Fixpoint_Base String
keywords
"codatatype" :: thy_defn and
"primcorecursive" :: thy_goal_defn and
"primcorec" :: thy_defn
begin
alias proj = 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 converse_Times: "(A \ B)\ = B \ A"
by fast
lemma equiv_proj:
assumes e: "equiv A R" and m: "z \ R"
shows "(proj R \ fst) z = (proj R \ snd) z"
proof -
from m 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
(* Operators: *)
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)\ 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_case_prod_eq: "in_rel (Collect (case_prod X)) = X"
unfolding fun_eq_iff by auto
lemma Collect_case_prod_in_rel_leI: "X \ Y \ X \ Collect (case_prod (in_rel Y))"
by auto
lemma Collect_case_prod_in_rel_leE: "X \ Collect (case_prod (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)\ 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)\"
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 \ (\x. (x, x))) z = id z" by simp
lemma snd_diag_id: "(snd \ (\x. (x, x))) z = id z" by simp
lemma fst_diag_fst: "fst \ ((\x. (x, x)) \ fst) = fst" by auto
lemma snd_diag_fst: "snd \ ((\x. (x, x)) \ fst) = fst" by auto
lemma fst_diag_snd: "fst \ ((\x. (x, x)) \ snd) = snd" by auto
lemma snd_diag_snd: "snd \ ((\x. (x, x)) \ 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
(*injection into the field of a cardinal*)
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
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 \<open>Equivalence relations, quotients, and Hilbert's choice\<close>
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"
proof (unfold univ_def)
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 ECH RES univ_commute by fastforce
thus "univ f X \ B" using x PRES by simp
qed
ML_file \<open>Tools/BNF/bnf_gfp_util.ML\<close>
ML_file \<open>Tools/BNF/bnf_gfp_tactics.ML\<close>
ML_file \<open>Tools/BNF/bnf_gfp.ML\<close>
ML_file \<open>Tools/BNF/bnf_gfp_rec_sugar_tactics.ML\<close>
ML_file \<open>Tools/BNF/bnf_gfp_rec_sugar.ML\<close>
end
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
