Theory HOL.BNF_Greatest_Fixpoint

(*  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 ‹Greatest Fixpoint (Codatatype) Operation on Bounded Natural Functors›

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 ‹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"
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 <o card_suc 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 <o card_suc r"
  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 <o r"
  using natLeq_ordLess_cinfinite by blast

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