SSL BNF_Greatest_Fixpoint.thy Sprache: Isabelle

(*  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

lemma card_suc_ordLess_imp_ordLeq:
  assumes ORD: "Card_order r" "Card_order r'" "card_order r'"
  and LESS: "r
shows "r \o r'"
proof -
  have "Card_order (card_suc r')" by (rule Card_order_card_suc[OF ORD(3)])
  then have "cardSuc r \o card_suc r'" using cardSuc_least ORD LESS by blast
  then have "cardSuc r \o cardSuc r'" using cardSuc_ordIso_card_suc ordIso_symmetric
      ordLeq_ordIso_trans ORD(3) by blast
  then show ?thesis using cardSuc_mono_ordLeq ORD by blast
qed

lemma natLeq_ordLess_cinfinite: "\Cinfinite r; card_order r\ \ natLeq
  using natLeq_ordLeq_cinfinite card_suc_greater ordLeq_ordLess_trans by blast

corollary natLeq_ordLess_cinfinite': "\Cinfinite r'; card_order r'; r \ card_suc r'\ \ natLeq
  using natLeq_ordLess_cinfinite by blast

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

quality100%

¤ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.