Theory Refine_Misc

section {* Miscellanneous Lemmas and Tools *}
theory Refine_Misc
imports 
  Automatic_Refinement.Automatic_Refinement
  Refine_Mono_Prover
begin

text {* Basic configuration for monotonicity prover: *}
lemmas [refine_mono] = monoI monotoneI[of "(≤)" "(≤)"]
lemmas [refine_mono] = TrueI le_funI order_refl

lemma case_prod_mono[refine_mono]: 
  "⟦⋀a b. p=(a,b) ⟹ f a b ≤ f' a b⟧ ⟹ case_prod f p ≤ case_prod f' p"
  by (auto split: prod.split)

lemma case_option_mono[refine_mono]:
  assumes "fn ≤ fn'"
  assumes "⋀v. x=Some v ⟹ fs v ≤ fs' v"
  shows "case_option fn fs x ≤ case_option fn' fs' x"
  using assms by (auto split: option.split)

lemma case_list_mono[refine_mono]:
  assumes "fn ≤ fn'"
  assumes "⋀x xs. l=x#xs ⟹ fc x xs ≤ fc' x xs"
  shows "case_list fn fc l ≤ case_list fn' fc' l"
  using assms by (auto split: list.split)

lemma if_mono[refine_mono]:
  assumes "b ⟹ m1 ≤ m1'"
  assumes "¬b ⟹ m2 ≤ m2'"
  shows "(if b then m1 else m2) ≤ (if b then m1' else m2')"
  using assms by auto

lemma let_mono[refine_mono]:
  "f x ≤ f' x' ⟹ Let x f ≤ Let x' f'" by auto


subsection {* Uncategorized Lemmas *}
lemma all_nat_split_at: "∀i::'a::linorder<k. P i ⟹ P k ⟹ ∀i>k. P i 
  ⟹ ∀i. P i"
  by (metis linorder_neq_iff)

subsection {* Well-Foundedness *}

lemma wf_no_infinite_down_chainI:
  assumes "⋀f. ⟦⋀i. (f (Suc i), f i)∈r⟧ ⟹ False"
  shows "wf r"
  by (metis assms wf_iff_no_infinite_down_chain)

text {* This lemma transfers well-foundedness over a simulation relation. *}
lemma sim_wf:
  assumes WF: "wf (S'¯)"
  assumes STARTR: "(x0,x0')∈R"
  assumes SIM: "⋀s s' t. ⟦ (s,s')∈R; (s,t)∈S; (x0',s')∈S'⇧* ⟧ 
    ⟹ ∃t'. (s',t')∈S' ∧ (t,t')∈R"
  assumes CLOSED: "Domain S  ⊆ S⇧*``{x0}"
  shows "wf (S¯)"
proof (rule wf_no_infinite_down_chainI, simp)
  txt {*
    Informal proof:
    Assume there is an infinite chain in @{text "S"}.
    Due to the closedness property of @{text "S"}, it can be extended to 
    start at @{text x0}.
    Now, we inductively construct an infinite chain in @{text "S'"}, such that
    each element of the new chain is in relation with the corresponding 
    element of the original chain:
      The first element is @{text "x0'"}. 
      For any element @{text "i+1"}, the simulation property yields the next
      element.
    This chain contradicts well-foundedness of @{text "S'"}.
    *}

  fix f
  assume CHAIN: "⋀i. (f i, f (Suc i))∈S"
  txt {* Extend to start with @{text "x0"} *}
  obtain f' where CHAIN': "⋀i. (f' i, f' (Suc i))∈S" and [simp]: "f' 0 = x0"
  proof -
    {
      fix x
      assume S: "x = f 0"
      from CHAIN have "f 0 ∈ Domain S" by auto
      with CLOSED have "(x0,x)∈S⇧*" by (auto simp: S)
      then obtain g k where G0: "g 0 = x0" and X: "x = g k" 
        and CH: "(∀i<k. (g i, g (Suc i))∈S)"
      proof induct
        case base thus ?case by force
      next
        case (step y z) show ?case proof (rule step.hyps(3))
          fix g k 
          assume "g 0 = x0" and "y = g k" 
            and "∀i<k. (g i, g (Suc i))∈S"
          thus ?case using `(y,z)∈S`
            by (rule_tac step.prems[where g="g(Suc k := z)" and k="Suc k"])
              auto
        qed
      qed
      define f' where "f' i = (if i<k then g i else f (i-k))" for i
      have "∃f'. f' 0 = x0 ∧ (∀i. (f' i, f' (Suc i))∈S)"
        apply (rule_tac x=f' in exI)
        apply (unfold f'_def)
        apply (rule conjI)
        using S X G0 apply (auto) []
        apply (rule_tac k=k in all_nat_split_at)
        apply (auto)
        apply (simp add: CH)
        apply (subgoal_tac "k = Suc i")
        apply (simp add: S[symmetric] CH X)
        apply simp
        apply (simp add: CHAIN)
        apply (subgoal_tac "Suc i - k = Suc (i-k)")
        using CHAIN apply simp
        apply simp
        done
    }
    then obtain f' where "∀i. (f' i,f' (Suc i))∈S" and "f' 0 = x0" by blast
    thus ?thesis by (blast intro!: that)
  qed

  txt {* Construct chain in @{text "S'"}*}
  define g' where "g' = rec_nat x0' (λi x. SOME x'. 
          (x,x')∈S' ∧ (f' (Suc i),x')∈R ∧ (x0', x')∈S'⇧* )"
  {
    fix i
    note [simp] = g'_def
    have "(g' i, g' (Suc i))∈S' ∧ (f' (Suc i),g' (Suc i))∈R 
      ∧ (x0',g' (Suc i))∈S'⇧*"
    proof (induct i)
      case 0 
      from SIM[OF STARTR] CHAIN'[of 0] obtain t' where 
        "(x0',t')∈S'" and "(f' (Suc 0),t')∈R" by auto
      moreover hence "(x0',t')∈S'⇧*" by auto
      ultimately show ?case
        by (auto intro: someI2 simp: STARTR)
    next
      case (Suc i)
      with SIM[OF _ CHAIN'[of "Suc i"]] 
      obtain t' where LS: "(g' (Suc i),t')∈S'" and "(f' (Suc (Suc i)),t')∈R"
        by auto
      moreover from LS Suc have "(x0', t')∈S'⇧*" by auto
      ultimately show ?case
        apply simp
        apply (rule_tac a="t'" in someI2)
        apply auto
        done
    qed
  } hence S'CHAIN: "∀i. (g' i, g'(Suc i))∈S'" by simp
  txt {* This contradicts well-foundedness *}
  with WF show False 
    by (erule_tac wf_no_infinite_down_chainE[where f=g']) simp
qed

text {* Well-founded relation that approximates a finite set from below. *}
definition "finite_psupset S ≡ { (Q',Q). Q⊂Q' ∧ Q' ⊆ S }"
lemma finite_psupset_wf[simp, intro]: "finite S ⟹ wf (finite_psupset S)"
  unfolding finite_psupset_def by (blast intro: wf_bounded_supset)

definition "less_than_bool ≡ {(a,b). a<(b::bool)}"
lemma wf_less_than_bool[simp, intro!]: "wf (less_than_bool)"
  unfolding less_than_bool_def
  by (auto simp: wf_def)
lemma less_than_bool_iff[simp]:
  "(x,y)∈less_than_bool ⟷ x=False ∧ y=True"  
  by (auto simp: less_than_bool_def)

definition "greater_bounded N ≡ inv_image less_than (λx. N-x)" 
lemma wf_greater_bounded[simp, intro!]: "wf (greater_bounded N)" by (auto simp: greater_bounded_def)

lemma greater_bounded_Suc_iff[simp]: "(Suc x,x)∈greater_bounded N ⟷ Suc x ≤ N"
  by (auto simp: greater_bounded_def)

    
    
subsection {* Monotonicity and Orderings *}

lemma mono_const[simp, intro!]: "mono (λ_. c)" by (auto intro: monoI)
lemma mono_if: "⟦mono S1; mono S2⟧ ⟹
  mono (λF s. if b s then S1 F s else S2 F s)"
  apply rule
  apply (rule le_funI)
  apply (auto dest: monoD[THEN le_funD])
  done

lemma mono_infI: "mono f ⟹ mono g ⟹ mono (inf f g)"
  unfolding inf_fun_def
  apply (rule monoI)
  apply (metis inf_mono monoD)
  done

lemma mono_infI': 
  "mono f ⟹ mono g ⟹ mono (λx. inf (f x) (g x) :: 'b::lattice)"
  by (rule mono_infI[unfolded inf_fun_def])

lemma mono_infArg: 
  fixes f :: "'a::lattice ⇒ 'b::order"
  shows "mono f ⟹ mono (λx. f (inf x X))"
  apply (rule monoI)
  apply (erule monoD)
  apply (metis inf_mono order_refl) 
  done

lemma mono_Sup:
  fixes f :: "'a::complete_lattice ⇒ 'b::complete_lattice"
  shows "mono f ⟹ Sup (f`S) ≤ f (Sup S)"
  apply (rule Sup_least)
  apply (erule imageE)
  apply simp
  apply (erule monoD)
  apply (erule Sup_upper)
  done

lemma mono_SupI:
  fixes f :: "'a::complete_lattice ⇒ 'b::complete_lattice"
  assumes "mono f"
  assumes "S'⊆f`S"
  shows "Sup S' ≤ f (Sup S)"
  by (metis Sup_subset_mono assms mono_Sup order_trans)

lemma mono_Inf:
  fixes f :: "'a::complete_lattice ⇒ 'b::complete_lattice"
  shows "mono f ⟹ f (Inf S) ≤ Inf (f`S)"
  apply (rule Inf_greatest)
  apply (erule imageE)
  apply simp
  apply (erule monoD)
  apply (erule Inf_lower)
  done

lemma mono_funpow: "mono (f::'a::order ⇒ 'a) ⟹ mono (f^^i)"
  apply (induct i)
  apply (auto intro!: monoI) 
  apply (auto dest: monoD)
  done

lemma mono_id[simp, intro!]:
  "mono id"
  "mono (λx. x)"
  by (auto intro: monoI)

declare SUP_insert[simp]

lemma (in semilattice_inf) le_infD1:
  "a ≤ inf b c ⟹ a ≤ b" by (rule le_infE)
lemma (in semilattice_inf) le_infD2:
  "a ≤ inf b c ⟹ a ≤ c" by (rule le_infE)
lemma (in semilattice_inf) inf_leI:
  "⟦ ⋀x. ⟦ x≤a; x≤b ⟧ ⟹ x≤c ⟧ ⟹ inf a b ≤ c"
  by (metis inf_le1 inf_le2)

lemma top_Sup: "(top::'a::complete_lattice)∈A ⟹ Sup A = top"
  by (metis Sup_upper top_le)
lemma bot_Inf: "(bot::'a::complete_lattice)∈A ⟹ Inf A = bot"
  by (metis Inf_lower le_bot)

lemma mono_compD: "mono f ⟹ x≤y ⟹ f o x ≤ f o y"
  apply (rule le_funI)
  apply (auto dest: monoD le_funD)
  done


subsubsection {* Galois Connections *}
locale galois_connection =
  fixes α::"'a::complete_lattice ⇒ 'b::complete_lattice" and γ
  assumes galois: "c ≤ γ(a) ⟷ α(c) ≤ a"
begin
  lemma αγ_defl: "α(γ(x)) ≤ x"
  proof -
    have "γ x ≤ γ x" by simp
    with galois show "α(γ(x)) ≤ x" by blast
  qed
  lemma γα_infl: "x ≤ γ(α(x))"
  proof -
    have "α x ≤ α x" by simp
    with galois show "x ≤ γ(α(x))" by blast
  qed
    
  lemma α_mono: "mono α"
  proof 
    fix x::'a and y::'a
    assume "x≤y"
    also note γα_infl[of y]
    finally show "α x ≤ α y" by (simp add: galois)
  qed

  lemma γ_mono: "mono γ"
    by rule (metis αγ_defl galois inf_absorb1 le_infE)

  lemma dist_γ[simp]: 
    "γ (inf a b) = inf (γ a) (γ b)"
    apply (rule order_antisym)
    apply (rule mono_inf[OF γ_mono])
    apply (simp add: galois)
    apply (simp add: galois[symmetric])
    done

  lemma dist_α[simp]: 
    "α (sup a b) = sup (α a) (α b)"
    by (metis (no_types) α_mono galois mono_sup order_antisym 
      sup_ge1 sup_ge2 sup_least)

end

subsubsection {* Fixed Points *}
lemma mono_lfp_eqI:
  assumes MONO: "mono f"
  assumes FIXP: "f a ≤ a"
  assumes LEAST: "⋀x. f x = x ⟹ a≤x"
  shows "lfp f = a"
  apply (rule antisym)
  apply (rule lfp_lowerbound)
  apply (rule FIXP)
  by (metis LEAST MONO lfp_unfold)

lemma mono_gfp_eqI:
  assumes MONO: "mono f"
  assumes FIXP: "a ≤ f a"
  assumes GREATEST: "⋀x. f x = x ⟹ x≤a"
  shows "gfp f = a"
  apply (rule antisym)
  apply (metis GREATEST MONO gfp_unfold)
  apply (rule gfp_upperbound)
  apply (rule FIXP)
  done

lemma lfp_le_gfp': "mono f ⟹ lfp f x ≤ gfp f x"
  by (rule le_funD[OF lfp_le_gfp])

(* Just a reformulation of lfp_induct *)
lemma lfp_induct':
  assumes M: "mono f"
  assumes IS: "⋀m. ⟦ m ≤ lfp f; m ≤ P ⟧ ⟹ f m ≤ P"
  shows "lfp f ≤ P"
  apply (rule lfp_induct[OF M])
  apply (rule IS)
  by simp_all

lemma lfp_gen_induct:
  ― ‹Induction lemma for generalized lfps›
  assumes M: "mono f"
  notes MONO'[refine_mono] = monoD[OF M]
  assumes I0: "m0 ≤ P"
  assumes IS: "⋀m. ⟦
      m ≤ lfp (λs. sup m0 (f s));  ― ‹Assume already established invariants›
      m ≤ P;                       ― ‹Assume invariant›
      f m ≤ lfp (λs. sup m0 (f s)) ― ‹Assume that step preserved est. invars›
    ⟧ ⟹ f m ≤ P"                 ― ‹Show that step preserves invariant›
  shows "lfp (λs. sup m0 (f s)) ≤ P"
  apply (rule lfp_induct')
  apply (meson MONO' monoI order_mono_setup.refl sup_mono)
  apply (rule sup_least)
  apply (rule I0)
  apply (rule IS, assumption+)
  apply (subst lfp_unfold)
  apply (meson MONO' monoI order_mono_setup.refl sup_mono)
  apply (rule le_supI2)
  apply (rule monoD[OF M])
  .



subsubsection {* Connecting Complete Lattices and 
  Chain-Complete Partial Orders *}
(* Note: Also connected by subclass now. However, we need both directions
  of embedding*)
lemma (in complete_lattice) is_ccpo: "class.ccpo Sup (≤) (<)"
  apply unfold_locales
  apply (erule Sup_upper)
  apply (erule Sup_least)
  done

lemma (in complete_lattice) is_dual_ccpo: "class.ccpo Inf (≥) (>)"
  apply unfold_locales
  apply (rule less_le_not_le)
  apply (rule order_refl)
  apply (erule (1) order_trans)
  apply (erule (1) antisym)
  apply (erule Inf_lower)
  apply (erule Inf_greatest)
  done
  
  
lemma ccpo_mono_simp: "monotone (≤) (≤) f ⟷ mono f"
  unfolding monotone_def mono_def by simp
lemma ccpo_monoI: "mono f ⟹ monotone (≤) (≤) f" 
  by (simp add: ccpo_mono_simp) 
lemma ccpo_monoD: "monotone (≤) (≤) f ⟹ mono f" 
  by (simp add: ccpo_mono_simp) 

lemma dual_ccpo_mono_simp: "monotone (≥) (≥) f ⟷ mono f"
  unfolding monotone_def mono_def by auto
lemma dual_ccpo_monoI: "mono f ⟹ monotone (≥) (≥) f" 
  by (simp add: dual_ccpo_mono_simp) 
lemma dual_ccpo_monoD: "monotone (≥) (≥) f ⟹ mono f" 
  by (simp add: dual_ccpo_mono_simp) 

lemma ccpo_lfp_simp: "⋀f. mono f ⟹ ccpo.fixp Sup (≤) f = lfp f"
  apply (rule antisym)
  defer
  apply (rule lfp_lowerbound)
  apply (drule ccpo.fixp_unfold[OF is_ccpo ccpo_monoI, symmetric])
  apply simp

  apply (rule ccpo.fixp_lowerbound[OF is_ccpo ccpo_monoI], assumption)
  apply (simp add: lfp_unfold[symmetric])
  done

lemma ccpo_gfp_simp: "⋀f. mono f ⟹ ccpo.fixp Inf (≥) f = gfp f"
  apply (rule antisym)
  apply (rule gfp_upperbound)
  apply (drule ccpo.fixp_unfold[OF is_dual_ccpo dual_ccpo_monoI, symmetric])
  apply simp

  apply (rule ccpo.fixp_lowerbound[OF is_dual_ccpo dual_ccpo_monoI], assumption)
  apply (simp add: gfp_unfold[symmetric])
  done

abbreviation "chain_admissible P ≡ ccpo.admissible Sup (≤) P"
abbreviation "is_chain ≡ Complete_Partial_Order.chain (≤)"
lemmas chain_admissibleI[intro?] = ccpo.admissibleI[where lub=Sup and ord="(≤)"]


abbreviation "dual_chain_admissible P ≡ ccpo.admissible Inf (λx y. y≤x) P"
abbreviation "is_dual_chain ≡ Complete_Partial_Order.chain (λx y. y≤x)"
lemmas dual_chain_admissibleI[intro?] = 
  ccpo.admissibleI[where lub=Inf and ord="(λx y. y≤x)"]

lemma dual_chain_iff[simp]: "is_dual_chain C = is_chain C"
  unfolding chain_def
  apply auto
  done

lemmas chain_dualI = iffD1[OF dual_chain_iff]
lemmas dual_chainI = iffD2[OF dual_chain_iff]

lemma is_chain_empty[simp, intro!]: "is_chain {}"
  by (rule chainI) auto
lemma is_dual_chain_empty[simp, intro!]: "is_dual_chain {}"
  by (rule dual_chainI) auto

lemma point_chainI: "is_chain M ⟹ is_chain ((λf. f x)`M)"
  by (auto intro: chainI le_funI dest: chainD le_funD)


text {* We transfer the admissible induction lemmas to complete
  lattices. *}
lemma lfp_cadm_induct:
  "⟦chain_admissible P; P (Sup {}); mono f; ⋀x. P x ⟹ P (f x)⟧ ⟹ P (lfp f)"
  by (simp only: ccpo_mono_simp[symmetric] ccpo_lfp_simp[symmetric])
     (rule ccpo.fixp_induct[OF is_ccpo])

lemma gfp_cadm_induct:
  "⟦dual_chain_admissible P; P (Inf {}); mono f; ⋀x. P x ⟹ P (f x)⟧ ⟹ P (gfp f)"
  by (simp only: dual_ccpo_mono_simp[symmetric] ccpo_gfp_simp[symmetric])
     (rule ccpo.fixp_induct[OF is_dual_ccpo])

subsubsection {* Continuity and Kleene Fixed Point Theorem *}
definition "cont f ≡ ∀C. C≠{} ⟶ f (Sup C) = Sup (f`C)"
definition "strict f ≡ f bot = bot"
definition "inf_distrib f ≡ strict f ∧ cont f"

lemma contI[intro?]: "⟦⋀C. C≠{} ⟹ f (Sup C) = Sup (f`C)⟧ ⟹ cont f" 
  unfolding cont_def by auto
lemma contD: "cont f ⟹ C≠{} ⟹ f (Sup C) = Sup (f`C)" 
  unfolding cont_def by auto
lemma contD': "cont f ⟹ C≠{} ⟹ f (Sup C) = SUPREMUM C f" 
  using contD by simp

lemma strictD[dest]: "strict f ⟹ f bot = bot" 
  unfolding strict_def by auto
― ‹We only add this lemma to the simpset for functions on the same type. 
    Otherwise, the simplifier tries it much too often.›
lemma strictD_simp[simp]: "strict f ⟹ f (bot::'a::bot) = (bot::'a)" 
  unfolding strict_def by auto

lemma strictI[intro?]: "f bot = bot ⟹ strict f"
  unfolding strict_def by auto

lemma inf_distribD[simp]: 
  "inf_distrib f ⟹ strict f"
  "inf_distrib f ⟹ cont f"
  unfolding inf_distrib_def by auto

lemma inf_distribI[intro?]: "⟦strict f; cont f⟧ ⟹ inf_distrib f"
  unfolding inf_distrib_def by auto

lemma inf_distribD'[simp]:
  fixes f :: "'a::complete_lattice ⇒ 'b::complete_lattice"
  shows "inf_distrib f ⟹ f (Sup C) = Sup (f`C)"
  apply (cases "C={}")
  apply (auto dest: inf_distribD contD')
  done

lemma inf_distribI':
  fixes f :: "'a::complete_lattice ⇒ 'b::complete_lattice"
  assumes B: "⋀C. f (Sup C) = Sup (f`C)"
  shows "inf_distrib f"
  apply (rule)
  apply (rule)
  apply (rule B[of "{}", simplified])
  apply (rule)
  apply (rule B)
  done
  
lemma cont_is_mono[simp]: 
  fixes f :: "'a::complete_lattice ⇒ 'b::complete_lattice"
  shows "cont f ⟹ mono f"
  apply (rule monoI)
  apply (drule_tac C="{x,y}" in contD)
  apply (auto simp: le_iff_sup)
  done

lemma inf_distrib_is_mono[simp]: 
  fixes f :: "'a::complete_lattice ⇒ 'b::complete_lattice"
  shows "inf_distrib f ⟹ mono f"
  by simp

text {* Only proven for complete lattices here. Also holds for CCPOs. *}

theorem gen_kleene_lfp:
  fixes f:: "'a::complete_lattice ⇒ 'a"
  assumes CONT: "cont f"
  shows "lfp (λx. sup m (f x)) = (SUP i. (f^^i) m)"
proof (rule antisym)
  let ?f = "(λx. sup m (f x))"
  let ?K="{ (f^^i) m | i . True}"
  note MONO=cont_is_mono[OF CONT]
  note MONO'[refine_mono] = monoD[OF MONO]
  {
    fix i
    have "(f^^i) m ≤ lfp ?f"
      apply (induct i)
      apply simp
      apply (subst lfp_unfold)
      apply (meson MONO' monoI order_mono_setup.refl sup_mono) 
      apply simp
      
      apply (subst lfp_unfold)
      apply (meson MONO' monoI order_mono_setup.refl sup_mono) 
      apply simp
      by (metis MONO' le_supI2)
  } thus "(SUP i. (f^^i) m) ≤ lfp ?f" by (blast intro: SUP_least)
next
  let ?f = "(λx. sup m (f x))"
  show "lfp ?f ≤ (SUP i. (f^^i) m)"
    apply (rule lfp_lowerbound)
    apply (rule sup_least)
    apply (rule order_trans[OF _ SUP_upper[where i=0]], simp_all) []
    apply (simp add: contD [OF CONT])
    apply (rule Sup_subset_mono)
    apply (auto)
    apply (rule_tac x="Suc xa" in range_eqI)
    apply simp
    done
qed

theorem kleene_lfp:
  fixes f:: "'a::complete_lattice ⇒ 'a"
  assumes CONT: "cont f"
  shows "lfp f = (SUP i. (f^^i) bot)"
  using gen_kleene_lfp[OF CONT,where m=bot] by simp

theorem (* Detailed proof *)
  fixes f:: "'a::complete_lattice ⇒ 'a"
  assumes CONT: "cont f"
  shows "lfp f = (SUP i. (f^^i) bot)"
proof (rule antisym)
  let ?K="{ (f^^i) bot | i . True}"
  note MONO=cont_is_mono[OF CONT]
  {
    fix i
    have "(f^^i) bot ≤ lfp f"
      apply (induct i)
      apply simp
      apply simp
      by (metis MONO lfp_unfold monoD)
  } thus "(SUP i. (f^^i) bot) ≤ lfp f" by (blast intro: SUP_least)
next
  show "lfp f ≤ (SUP i. (f^^i) bot)"
    apply (rule lfp_lowerbound)
    apply (simp add: contD [OF CONT])
    apply (rule Sup_subset_mono)
    apply auto
    apply (rule_tac x="Suc xa" in range_eqI)
    apply auto
    done
qed

(* Alternative proof of gen_kleene_lfp that re-uses standard Kleene, but is more tedious *)
lemma SUP_funpow_contracting:
  fixes f :: "'a ⇒ ('a::complete_lattice)"
  assumes C: "cont f" 
  shows "f (SUP i. (f^^i) m) ≤ (SUP i. (f^^i) m)"
proof -
  have 1: "⋀i x. f ((f^^i) x) = (f^^(Suc i)) x"
    by simp

  have "f (SUP i. (f^^i) m) = (SUP i. f ((f ^^ i) m))"
    by (subst contD[OF C]) (simp_all)
  also have "… ≤ (SUP i. (f^^i) m)"
    apply (rule SUP_least)
    apply (simp, subst 1)
    apply (rule SUP_upper)
    ..
  finally show ?thesis .
qed

lemma gen_kleene_chain_conv:
  fixes f :: "'a::complete_lattice ⇒ 'a"
  assumes C: "cont f"
  shows "(SUP i. (f^^i) m) = (SUP i. ((λx. sup m (f x))^^i) bot)"
proof -
  let ?f' = "λx. sup m (f x)"
  show ?thesis
  proof (intro antisym SUP_least)
    from C have C': "cont ?f'"
      unfolding cont_def
      by (simp add: SUP_sup_distrib[symmetric])
  
    fix i
    show "(f ^^ i) m ≤ (SUP i. (?f' ^^ i) bot)"
    proof (induction i)
      case 0 show ?case
        by (rule order_trans[OF _ SUP_upper[where i=1]]) auto
    next
      case (Suc i)
      from cont_is_mono[OF C, THEN monoD, OF Suc]
      have "(f ^^ (Suc i)) m ≤ f (SUP i. ((λx. sup m (f x)) ^^ i) bot)"
        by simp
      also have "… ≤ sup m …" by simp
      also note SUP_funpow_contracting[OF C']
      finally show ?case .
    qed
  next
    fix i
    show "(?f'^^i) bot ≤ (SUP i. (f^^i) m)"
    proof (induction i)
      case 0 thus ?case by simp
    next
      case (Suc i)
      from monoD[OF cont_is_mono[OF C] Suc]
      have "(?f'^^Suc i) bot ≤ sup m (f (SUP i. (f ^^ i) m))" 
        by (simp add: le_supI2)
      also have "… ≤ (SUP i. (f ^^ i) m)"
        apply (rule sup_least)
        apply (rule order_trans[OF _ SUP_upper[where i=0]], simp_all) []
        apply (rule SUP_funpow_contracting[OF C])
        done
      finally show ?case .
    qed
  qed
qed
   
theorem 
  assumes C: "cont f"
  shows "lfp (λx. sup m (f x)) = (SUP i. (f^^i) m)"
  apply (subst gen_kleene_chain_conv[OF C])
  apply (rule kleene_lfp)
    using C
    unfolding cont_def
    apply (simp add: SUP_sup_distrib[symmetric])
  done



lemma (in galois_connection) dual_inf_dist_γ: "γ (Inf C) = Inf (γ`C)"
  apply (rule antisym)
  apply (rule Inf_greatest)
  apply clarify
  apply (rule monoD[OF γ_mono])
  apply (rule Inf_lower)
  apply simp

  apply (subst galois)
  apply (rule Inf_greatest)
  apply (subst galois[symmetric])
  apply (rule Inf_lower)
  apply simp
  done

lemma (in galois_connection) inf_dist_α: "inf_distrib α"
  apply (rule inf_distribI')
  apply (rule antisym)

  apply (subst galois[symmetric])
  apply (rule Sup_least)
  apply (subst galois)
  apply (rule Sup_upper)
  apply simp

  apply (rule Sup_least)
  apply clarify
  apply (rule monoD[OF α_mono])
  apply (rule Sup_upper)
  apply simp
  done

subsection {* Maps *}
subsubsection {* Key-Value Set *}
  
  lemma map_to_set_simps[simp]: 
    "map_to_set Map.empty = {}"
    "map_to_set [a↦b] = {(a,b)}"
    "map_to_set (m|`K) = map_to_set m ∩ K×UNIV"
    "map_to_set (m(x:=None)) = map_to_set m - {x}×UNIV"
    "map_to_set (m(x↦v)) = map_to_set m - {x}×UNIV ∪ {(x,v)}"
    "map_to_set m ∩ dom m×UNIV = map_to_set m"
    "m k = Some v ⟹ (k,v)∈map_to_set m"
    "single_valued (map_to_set m)"
    apply (simp_all)
    by (auto simp: map_to_set_def restrict_map_def split: if_split_asm
      intro: single_valuedI)
      
  lemma map_to_set_inj:     
    "(k,v)∈map_to_set m ⟹ (k,v')∈map_to_set m ⟹ v = v'"
    by (auto simp: map_to_set_def)


end