Theory Lib

theory "Lib"
imports
  Complex_Main
begin 
section ‹Generic Mathematical Background Lemmas›

lemma finite_subset [simp]: "finite M ⟹ finite {x∈M. P x}"
  by simp

lemma finite_powerset [simp]: "finite M ⟹ finite {S. S⊆M}"
  by simp

definition fst_proj:: "('a*'b) set ⇒ 'a set"
  where "fst_proj M ≡ {A. ∃B. (A,B)∈M}"

definition snd_proj:: "('a*'b) set ⇒ 'b set"
  where "snd_proj M ≡ {B. ∃A. (A,B)∈M}"

lemma fst_proj_mem [simp]: "(A ∈ fst_proj M) = (∃B. (A,B)∈M)"
  unfolding fst_proj_def by auto
  
lemma snd_proj_mem [simp]: "(B ∈ snd_proj M) = (∃A. (A,B)∈M)"
  unfolding snd_proj_def by auto

lemma fst_proj_prop: "∀x∈fst_proj {(A,B)| A B. P A ∧ R A B}. P(x)"
  unfolding fst_proj_def by auto

lemma snd_proj_prop: "∀x∈snd_proj {(A,B) | A B. P B ∧ R A B}. P(x)"
  unfolding snd_proj_def by auto

lemma map_cons: "map f (Cons x xs) = Cons (f x) (map f xs)"
  by (rule List.list.map)
lemma map_append: "map f (append xs ys) = append (map f xs) (map f ys)"
  by simp
  


text‹Lockstep induction schema for two simultaneous least fixpoints.
  If the successor step and supremum step of two least fixpoint inflations
  preserve a relation, then that relation holds of the two respective least fixpoints.›

lemma lfp_lockstep_induct [case_names monof monog step union]:
  fixes f :: "'a::complete_lattice ⇒ 'a"
    and g :: "'b::complete_lattice ⇒ 'b"
  assumes monof: "mono f" 
    and monog: "mono g"
    and R_step: "⋀A B. A ≤ lfp(f) ⟹ B ≤ lfp(g) ⟹ R A B ⟹ R (f(A)) (g(B))"
    and R_Union: "⋀M::('a*'b) set. (∀(A,B)∈M. R A B) ⟹ R (Sup (fst_proj M)) (Sup (snd_proj M))"
  shows "R (lfp f) (lfp g)"
proof-
  (*using idea of proof of "Inductive.thy:lfp_ordinal_induct"*)
  let ?M = "{(A,B). A ≤ lfp f ∧ B ≤ lfp g ∧ R A B}"
  from R_Union have supdoes: "R (Sup (fst_proj ?M)) (Sup (snd_proj ?M))" by simp
  also have "Sup (fst_proj ?M) = lfp f" and "Sup (snd_proj ?M) = lfp g"
  proof (rule antisym)
    show fle: "Sup (fst_proj ?M) ≤ lfp f"
      using fst_proj_prop Sup_le_iff by fastforce
    then have "f (Sup (fst_proj ?M)) ≤ f (lfp f)"
      by (rule monof [THEN monoD])
    then have fsup: "f (Sup (fst_proj ?M)) ≤ lfp f"
      using monof [THEN lfp_unfold] by simp

    have gle: "Sup (snd_proj ?M) ≤ lfp g"
      using snd_proj_prop Sup_le_iff by fastforce
    then have "g (Sup (snd_proj ?M)) ≤ g (lfp g)"
      by (rule monog [THEN monoD])
    then have gsup: "g (Sup (snd_proj ?M)) ≤ lfp g"
      using monog [THEN lfp_unfold] by simp

    from fsup and gsup have fgsup: "(f(Sup(fst_proj ?M)), g(Sup(snd_proj ?M))) ∈ ?M"
      using R_Union R_step Sup_le_iff
      using calculation fle gle by blast 

    from fgsup have "f (Sup (fst_proj ?M)) ≤ Sup (fst_proj ?M)"
      using Sup_upper by (metis (mono_tags, lifting) fst_proj_def mem_Collect_eq) 
    then show fge: "lfp f ≤ Sup (fst_proj ?M)"
      by (rule lfp_lowerbound)
    show "Sup (snd_proj ?M) = lfp g"
    proof (rule antisym)
      show "Sup (snd_proj ?M) ≤ lfp g" by (rule gle)
      from fgsup have "g (Sup (snd_proj ?M)) ≤ Sup (snd_proj ?M)"
        using Sup_upper by (metis (mono_tags, lifting) snd_proj_def mem_Collect_eq)
      then show gge: "lfp g ≤ Sup (snd_proj ?M)"
        by (rule lfp_lowerbound)
    qed
  qed
  then show ?thesis using supdoes by simp
qed


lemma sup_eq_all: "(⋀A. (A∈M ⟹ f(A)=g(A)))
  ⟹ Sup {f(A) | A. A∈M} = Sup {g(A) | A. A∈M}"
  by metis

lemma sup_corr_eq_chain: "⋀M::('a::complete_lattice*'a) set. (∀(A,B)∈M. f(A)=g(B)) ⟹ (Sup {f(A) | A. A∈fst_proj M} = Sup {g(B) | B. B∈snd_proj M})"
  by (metis (mono_tags, lifting) case_prod_conv fst_proj_mem snd_proj_mem)

end