Theory Complete_Lattice_Prop

section ‹Fixpoints and Complete Lattices›

(*
    Author: Viorel Preoteasa
*)

theory Complete_Lattice_Prop
imports WellFoundedTransitive
begin

text‹
This theory introduces some results about fixpoints of functions on 
complete lattices. The main result is that a monotonic function 
mapping momotonic functions to monotonic functions has the least 
fixpoint monotonic.
›

context complete_lattice begin

lemma inf_Inf: assumes nonempty: "A ≠ {}"
  shows "inf x (Inf A) = Inf ((inf x) ` A)"
  using assms by (auto simp add: INF_inf_const1 nonempty) 

end


(*
Monotonic applications which map monotonic to monotonic have monotonic fixpoints
*)

definition
  "mono_mono F = (mono F ∧ (∀ f . mono f ⟶ mono (F f)))"

theorem lfp_mono [simp]:
  "mono_mono F ⟹ mono (lfp F)"
  apply (simp add: mono_mono_def)
  apply (rule_tac f="F" and P = "mono" in lfp_ordinal_induct)
  apply (simp_all add: mono_def)
  apply (intro allI impI SUP_least)
  apply (rule_tac y = "f y" in order_trans)
  apply (auto intro: SUP_upper)
  done

lemma gfp_ordinal_induct:
  fixes f :: "'a::complete_lattice => 'a"
  assumes mono: "mono f"
  and P_f: "!!S. P S ==> P (f S)"
  and P_Union: "!!M. ∀S∈M. P S ==> P (Inf M)"
  shows "P (gfp f)"
proof -
  let ?M = "{S. gfp f ≤ S ∧ P S}"
  have "P (Inf ?M)" using P_Union by simp
  also have "Inf ?M = gfp f"
  proof (rule antisym)
    show "gfp f ≤ Inf ?M" by (blast intro: Inf_greatest)
    hence "f (gfp f) ≤ f (Inf ?M)" by (rule mono [THEN monoD])
    hence "gfp f ≤ f (Inf ?M)" using mono [THEN gfp_unfold] by simp
    hence "f (Inf ?M) ∈ ?M" using P_f P_Union by simp
    hence "Inf ?M ≤ f (Inf ?M)" by (rule Inf_lower)
    thus "Inf ?M ≤ gfp f" by (rule gfp_upperbound)
  qed
  finally show ?thesis .
qed 
theorem gfp_mono [simp]:
  "mono_mono F ⟹ mono (gfp F)"
  apply (simp add: mono_mono_def)
  apply (rule_tac f="F" and P = "mono" in gfp_ordinal_induct)
  apply (simp_all, safe)
  apply (simp_all add: mono_def)
  apply (intro allI impI INF_greatest)
  apply (rule_tac y = "f x" in order_trans)
  apply (auto intro: INF_lower)
  done

context complete_lattice begin

definition
  "Sup_less x (w::'b::well_founded) = Sup {y ::'a . ∃ v < w . y = x v}"

lemma Sup_less_upper:
  "v < w ⟹ P v ≤ Sup_less P w"
  by (simp add: Sup_less_def, rule Sup_upper, blast)


lemma Sup_less_least:
  "(!! v . v < w ⟹ P v ≤ Q) ⟹ Sup_less P w ≤ Q"
  by (simp add: Sup_less_def, rule Sup_least, blast)

end

lemma Sup_less_fun_eq:
  "((Sup_less P w) i) = (Sup_less (λ v . P v i)) w"
  apply (simp add: Sup_less_def fun_eq_iff)
  apply (rule arg_cong [of _ _ Sup])
  apply auto
  done

theorem fp_wf_induction:
  "f x  = x ⟹ mono f ⟹ (∀ w . (y w) ≤ f (Sup_less y w)) ⟹ Sup (range y) ≤ x"
  apply (rule Sup_least)
  apply (simp add: image_def, safe, simp)
  apply (rule less_induct1, simp_all)
  apply (rule_tac y = "f (Sup_less y xa)" in order_trans, simp)
  apply (drule_tac x = "Sup_less y xa" and y = "x" in monoD)
  by (simp add: Sup_less_least, auto)



end