Theory RefineG_Domain

section ‹General Domain Theory›
theory RefineG_Domain
imports "../Refine_Misc"
begin

  subsection ‹General Order Theory Tools›
  lemma chain_f_apply: "Complete_Partial_Order.chain (fun_ord le) F
    ⟹ Complete_Partial_Order.chain le {y . ∃f∈F. y = f x}"
    unfolding Complete_Partial_Order.chain_def 
    by (auto simp: fun_ord_def)

  lemma ccpo_lift:
    assumes "class.ccpo lub le lt"
    shows "class.ccpo (fun_lub lub) (fun_ord le) (mk_less (fun_ord le))"
  proof -
    interpret ccpo: ccpo lub le lt by fact
    show ?thesis
      apply unfold_locales
      apply (simp_all only: mk_less_def fun_ord_def fun_lub_def)
      apply simp
      using ccpo.order_trans apply blast
      using ccpo.order.antisym apply blast
      using ccpo.ccpo_Sup_upper apply (blast intro: chain_f_apply)
      using ccpo.ccpo_Sup_least apply (blast intro: chain_f_apply)
      done
  qed
  
  (* TODO: Move *)
  lemma fun_lub_simps[simp]: 
    "fun_lub lub {} = (λx. lub {})"
    "fun_lub lub {f} = (λx. lub {f x})"
    unfolding fun_lub_def by auto

  subsection ‹Flat Ordering›
  lemma flat_ord_chain_cases: 
    assumes A: "Complete_Partial_Order.chain (flat_ord b) C"
    obtains "C={}" 
    | "C={b}" 
    | x where "x≠b" and "C={x}" 
    | x where "x≠b" and "C={b,x}"
  proof -
    have "∃m1 m2. C ⊆ {m1,m2} ∧ (m1 = b ∨ m2 = b)"
      apply (rule ccontr)
    proof clarsimp
      assume "∀m1 m2. C ⊆ {m1, m2} ⟶ m1≠b ∧ m2≠b"
      then obtain m1 m2 where "m1∈C" "m2∈C" 
        "m1≠m2" "m1≠b" "m2≠b"
        by blast
      with A show False
        unfolding Complete_Partial_Order.chain_def flat_ord_def
        by auto
    qed
    then obtain m where "C ⊆ {m,b}" by blast
    thus ?thesis 
      apply (cases "m=b") 
      using that
      apply blast+
      done
  qed
    
  lemma flat_lub_simps[simp]:
    "flat_lub b {} = b"
    "flat_lub b {x} = x"
    "flat_lub b (insert b X) = flat_lub b X"
    unfolding flat_lub_def
    by auto

  lemma flat_ord_simps[simp]:
    "flat_ord b b x" 
    by (simp add: flat_ord_def)

  interpretation flat_ord: ccpo "flat_lub b" "flat_ord b" "mk_less (flat_ord b)"
    apply unfold_locales
    apply (simp_all only: mk_less_def flat_ord_def) apply auto [4]
    apply (erule flat_ord_chain_cases, auto) []
    apply (erule flat_ord_chain_cases, auto) []
    done

  interpretation flat_le_mono_setup: mono_setup_loc "flat_ord b"
    by standard auto

  subsubsection ‹Flat function Ordering›
  abbreviation "flatf_ord b == fun_ord (flat_ord b)"
  abbreviation "flatf_lub b == fun_lub (flat_lub b)"

  interpretation flatf_ord: ccpo "flatf_lub b" "flatf_ord b" "mk_less (flatf_ord b)"
    apply (rule ccpo_lift)
    apply unfold_locales
    done

  subsubsection ‹Fixed Points in Flat Ordering›
  text ‹
    Fixed points in a flat ordering are used to express recursion.
    The bottom element is interpreted as non-termination.
›  

  abbreviation "flat_mono b == monotone (flat_ord b) (flat_ord b)"
  abbreviation "flatf_mono b == monotone (flatf_ord b) (flatf_ord b)"
  abbreviation "flatf_fp b ≡ flatf_ord.fixp b"

  lemma flatf_fp_mono[refine_mono]:
    ― ‹The fixed point combinator is monotonic›
    assumes "flatf_mono b f"
      and "flatf_mono b g"
      and "⋀Z x. flat_ord b (f Z x) (g Z x)"
    shows "flat_ord b (flatf_fp b f x) (flatf_fp b g x)"
  proof -
    have "flatf_ord b (flatf_fp b f) (flatf_fp b g)"
      apply (rule flatf_ord.fixp_mono[OF assms(1,2)])
      using assms(3) by (simp add: fun_ord_def)
    thus ?thesis unfolding fun_ord_def by blast
  qed

  lemma flatf_admissible_pointwise:
    "(⋀x. P x b) ⟹ 
      ccpo.admissible (flatf_lub b) (flatf_ord b) (λg. ∀x. P x (g x))"
    apply (intro ccpo.admissibleI allI impI)
    apply (drule_tac x=x in chain_f_apply)
    apply (erule flat_ord_chain_cases)
    apply (auto simp add: fun_lub_def) [2]
    apply (force simp add: fun_lub_def) []
    apply (auto simp add: fun_lub_def) []
    done

  text ‹
    If a property is defined pointwise, and holds for the bottom element,
    we can use fixed-point induction for it. 

    In the induction step, we can assume that the function is less or equal
    to the fixed-point.

    This rule covers refinement and transfer properties, 
    such as: Refinement of fixed-point combinators and transfer of 
    fixed-point combinators to different domains.
›
  lemma flatf_fp_induct_pointwise:
    ― ‹Fixed-point induction for pointwise properties›
    fixes a :: 'a
    assumes cond_bot: "⋀a x. pre a x ⟹ post a x b"
    assumes MONO: "flatf_mono b B"
    assumes PRE0: "pre a x"
    assumes STEP: "⋀f a x. 
      ⟦⋀a' x'. pre a' x' ⟹ post a' x' (f x'); pre a x; 
        flatf_ord b f (flatf_fp b B) ⟧ 
      ⟹ post a x (B f x)"
    shows "post a x (flatf_fp b B x)"
  proof -
    define ub where "ub = flatf_fp b B"

    have "(∀x a. pre a x ⟶ post a x (flatf_fp b B x)) 
      ∧ flatf_ord b (flatf_fp b B) ub"
      apply (rule flatf_ord.fixp_induct[OF _ MONO])
      apply (rule admissible_conj)
      apply (rule flatf_admissible_pointwise)
      apply (blast intro: cond_bot)
      apply (rule ccpo.admissibleI)
      apply (blast intro: flatf_ord.ccpo_Sup_least)

      apply (auto intro: cond_bot simp: fun_ord_def flat_ord_def) []

      apply (rule conjI)
      unfolding ub_def

      apply (blast intro: STEP)

      apply (subst flatf_ord.fixp_unfold[OF MONO])
      apply (blast intro: monotoneD[OF MONO])
      done
    with PRE0 show ?thesis by blast
  qed
  
  text ‹
    The next rule covers transfer between fixed points.
    It allows to lift a pointwise transfer condition 
    ‹P x y ⟶ tr (f x) (f y)› to fixed points.
    Note that one of the fixed points may be an arbitrary fixed point.
›
  lemma flatf_fixp_transfer:
    ― ‹Transfer rule for fixed points›
    assumes TR_BOT[simp]: "⋀x'. tr b x'"
    assumes MONO: "flatf_mono b B"
    assumes FP': "fp' = B' fp'"
    assumes R0: "P x x'"
    assumes RS: "⋀f f' x x'.
       ⟦⋀x x'. P x x' ⟹ tr (f x) (f' x'); P x x'; fp' = f'⟧
       ⟹ tr (B f x) (B' f' x')"
    shows "tr (flatf_fp b B x) (fp' x')"
    apply (rule flatf_fp_induct_pointwise[where pre="λx y. P y x", OF _ MONO])
    apply simp
    apply (rule R0)
    apply (subst FP')
    apply (blast intro: RS)
    done

  subsubsection ‹Relation of Flat Ordering to Complete Lattices›
  text ‹
    In this section, we establish the relation between flat orderings 
    and complete lattices. This relation is exploited to show properties
    of fixed points wrt. a refinement ordering.
›

  abbreviation "flat_le ≡ flat_ord bot"
  abbreviation "flat_ge ≡ flat_ord top"
  abbreviation "flatf_le ≡ flatf_ord bot"
  abbreviation "flatf_ge ≡ flatf_ord top"

  text ‹The flat ordering implies the lattice ordering›
  lemma flat_ord_compat: 
    fixes x y :: "'a :: complete_lattice"
    shows 
    "flat_le x y ⟹ x ≤ y"
    "flat_ge x y ⟹ x ≥ y"
    unfolding flat_ord_def by auto

  lemma flatf_ord_compat: 
    fixes x y :: "'a ⇒ ('b :: complete_lattice)"
    shows 
    "flatf_le x y ⟹ x ≤ y"
    "flatf_ge x y ⟹ x ≥ y"
    by (auto simp: flat_ord_compat le_fun_def fun_ord_def)
  
  abbreviation "flat_mono_le ≡ flat_mono bot"
  abbreviation "flat_mono_ge ≡ flat_mono top"

  abbreviation "flatf_mono_le ≡ flatf_mono bot"
  abbreviation "flatf_mono_ge ≡ flatf_mono top"

  abbreviation "flatf_gfp ≡ flatf_ord.fixp top"
  abbreviation "flatf_lfp ≡ flatf_ord.fixp bot"

  text ‹If a functor is monotonic wrt. both the flat and the 
    lattice ordering, the fixed points wrt. these orderings coincide. 
›
  lemma lfp_eq_flatf_lfp:
    assumes FM: "flatf_mono_le B" and M: "mono B"
    shows "lfp B = flatf_lfp B"
  proof -
    from lfp_unfold[OF M, symmetric] have "B (lfp B) = lfp B" .
    hence "flatf_le (B (lfp B)) (lfp B)" by simp
    with flatf_ord.fixp_lowerbound[OF FM] have "flatf_le (flatf_lfp B) (lfp B)" .
    with flatf_ord_compat have "flatf_lfp B ≤ lfp B" by blast
    also
    from flatf_ord.fixp_unfold[OF FM, symmetric] have "B (flatf_lfp B) = flatf_lfp B" .
    hence "B (flatf_lfp B) ≤ flatf_lfp B" by simp
    with lfp_lowerbound[where A="flatf_lfp B"] have "lfp B ≤ flatf_lfp B" .
    finally show "lfp B = flatf_lfp B" ..
  qed

  lemma gfp_eq_flatf_gfp:
    assumes FM: "flatf_mono_ge B" and M: "mono B"
    shows "gfp B = flatf_gfp B"
  proof -
    from gfp_unfold[OF M, symmetric] have "B (gfp B) = gfp B" .
    hence "flatf_ge (B (gfp B)) (gfp B)" by simp
    with flatf_ord.fixp_lowerbound[OF FM] have "flatf_ge (flatf_gfp B) (gfp B)" .
    with flatf_ord_compat have "gfp B ≤ flatf_gfp B" by blast
    also
    from flatf_ord.fixp_unfold[OF FM, symmetric] have "B (flatf_gfp B) = flatf_gfp B" .
    hence "flatf_gfp B ≤ B (flatf_gfp B)" by simp
    with gfp_upperbound[where X="flatf_gfp B"] have "flatf_gfp B ≤ gfp B" .
    finally show "gfp B = flatf_gfp B" .
  qed
  

  (* TODO: This belongs to "General Recursion"*)
  text ‹
    The following lemma provides a well-founded induction scheme for arbitrary 
    fixed point combinators.
›
  lemma wf_fixp_induct:
    ― ‹Well-Founded induction for arbitrary fixed points›
    fixes a :: 'a
    assumes fixp_unfold: "fp B = B (fp B)"
    assumes WF: "wf V"
    assumes P0: "pre a x"
    assumes STEP: "⋀f a x. ⟦ 
      ⋀a' x'. ⟦ pre a' x'; (x',x)∈V ⟧ ⟹ post a' x' (f x'); fp B = f; pre a x 
    ⟧ ⟹ post a x (B f x)"
    shows "post a x (fp B x)"
  proof -
    have "∀a. pre a x ⟶ post a x (fp B x)"
      using WF
      apply (induct x rule: wf_induct_rule)
      apply (intro allI impI)
      apply (subst fixp_unfold)
      apply (rule STEP)
      apply (simp)
      apply (simp)
      apply (simp)
      done
    with P0 show ?thesis by blast
  qed


  lemma flatf_lfp_transfer:
    ― ‹Transfer rule for least fixed points›
    fixes B::"(_ ⇒ 'a::order_bot) ⇒ _"
    assumes TR_BOT[simp]: "⋀x. tr bot x"
    assumes MONO: "flatf_mono_le B"
    assumes MONO': "flatf_mono_le B'"
    assumes R0: "P x x'"
    assumes RS: "⋀f f' x x'.
       ⟦⋀x x'. P x x' ⟹ tr (f x) (f' x'); P x x'; flatf_lfp B' = f'⟧
       ⟹ tr (B f x) (B' f' x')"
    shows "tr (flatf_lfp B x) (flatf_lfp B' x')"
    apply (rule flatf_fixp_transfer[where tr=tr and fp'="flatf_lfp B'" and P=P])
    apply (fact|rule flatf_ord.fixp_unfold[OF MONO'])+
    done

  lemma flatf_gfp_transfer:
    ― ‹Transfer rule for greatest fixed points›
    fixes B::"(_ ⇒ 'a::order_top) ⇒ _"
    assumes TR_TOP[simp]: "⋀x. tr x top"
    assumes MONO: "flatf_mono_ge B"
    assumes MONO': "flatf_mono_ge B'"
    assumes R0: "P x x'"
    assumes RS: "⋀f f' x x'.
       ⟦⋀x x'. P x x' ⟹ tr (f x) (f' x'); P x x'; flatf_gfp B = f⟧
       ⟹ tr (B f x) (B' f' x')"
    shows "tr (flatf_gfp B x) (flatf_gfp B' x')"
    apply (rule flatf_fixp_transfer[where 
        tr="λx y. tr y x" and fp'="flatf_gfp B" and P="λx y. P y x"])
    apply (fact|assumption|rule flatf_ord.fixp_unfold[OF MONO] RS)+
    done

  lemma meta_le_everything_if_top: "(m=top) ⟹ (⋀x. x ≤ (m::'a::order_top))"
    by auto

  lemmas flatf_lfp_refine = flatf_lfp_transfer[
    where tr = "λa b. a ≤ cf b" for cf, OF bot_least]
  lemmas flatf_gfp_refine = flatf_gfp_transfer[
    where tr = "λa b. a ≤ cf b" for cf, OF meta_le_everything_if_top]


  lemma flat_ge_sup_mono[refine_mono]: "⋀a a'::'a::complete_lattice. 
    flat_ge a a' ⟹ flat_ge b b' ⟹ flat_ge (sup a b) (sup a' b')"
    by (auto simp: flat_ord_def)
  
  declare sup_mono[refine_mono]


end