Theory RefineG_Recursion

header {* \isaheader{Generic Recursion Combinator for Complete Lattice Structured Domains} *}
theory RefineG_Recursion
imports "../Refine_Misc" RefineG_Transfer RefineG_Domain
begin

text {*
  We define a recursion combinator that asserts monotonicity.
*}


(* TODO: Move to Domain.*)
text {*
  The following lemma allows to compare least fixed points wrt.\ different flat
  orderings. At any point, the fixed points are either equal or have their 
  orderings bottom values.
*}
lemma fp_compare:
  -- {*At any point, fixed points wrt.\ different orderings are either equal, 
    or both bottom.*}
  assumes M1: "flatf_mono b1 B" and M2: "flatf_mono b2 B"
  shows "flatf_fp b1 B x = flatf_fp b2 B x 
    ∨ (flatf_fp b1 B x = b1 ∧ flatf_fp b2 B x = b2)"
proof -
  note UNF1 = flatf_ord.fixp_unfold[OF M1, symmetric]
  note UNF2 = flatf_ord.fixp_unfold[OF M2, symmetric]

  from UNF1 have 1: "flatf_ord b2 (B (flatf_fp b1 B)) (flatf_fp b1 B)" by simp
  from UNF2 have 2: "flatf_ord b1 (B (flatf_fp b2 B)) (flatf_fp b2 B)" by simp

  from flatf_ord.fixp_lowerbound[OF M2 1] flatf_ord.fixp_lowerbound[OF M1 2]
    show ?thesis unfolding fun_ord_def flat_ord_def by auto
qed

(* TODO: Move *)
lemma flat_ord_top[simp]: "flat_ord b b x" by (simp add: flat_ord_def)


(* TODO: Move to Domain.*)
lemma lfp_gfp_compare:
  -- "Least and greatest fixed point are either equal, or bot and top"
  assumes MLE: "flatf_mono_le B" and MGE: "flatf_mono_ge B"
  shows "flatf_lfp B x = flatf_gfp B x 
    ∨ (flatf_lfp B x = bot ∧ flatf_gfp B x = top)"
  using fp_compare[OF MLE MGE] .


(* TODO: Move to Domain *)
definition trimono :: "(('a => 'b) => 'a => ('b::{bot,order,top})) => bool" 
  where "trimono B ≡ (*flatf_mono_le B ∧*) flatf_mono_ge B ∧ mono B"
lemma trimonoI[refine_mono]: 
  "[|flatf_mono_ge B; mono B|] ==> trimono B"
  unfolding trimono_def by auto

lemma trimono_trigger: "trimono B ==> trimono B" .

declaration {* Refine_Mono_Prover.declare_mono_triggers @{thms trimono_trigger} *}

(*lemma trimonoD_flatf_le: "trimono B ==> flatf_mono_le B"
  unfolding trimono_def by auto*)

lemma trimonoD_flatf_ge: "trimono B ==> flatf_mono_ge B"
  unfolding trimono_def by auto

lemma trimonoD_mono: "trimono B ==> mono B"
  unfolding trimono_def by auto

lemmas trimonoD = trimonoD_flatf_ge trimonoD_mono

(* TODO: Optimize mono-prover to only do derivations once. 
  Will cause problem with higher-order unification on ord - variable! *)
definition "triords ≡ {flat_ge,op ≤}"
lemma trimono_alt: 
  "trimono B <-> (∀ord∈fun_ord`triords. monotone ord ord B)"
  unfolding trimono_def
  by (auto simp: ccpo_mono_simp[symmetric] triords_def 
    fun_ord_def[abs_def] le_fun_def[abs_def])

lemma trimonoI': 
  assumes "!!ord. ord∈triords ==> monotone (fun_ord ord) (fun_ord ord) B"
  shows "trimono B"
  unfolding trimono_alt using assms by blast


(* TODO: Once complete_lattice and ccpo typeclass are unified,
  we should also define a REC-combinator for ccpos! *)

definition REC where "REC B x ≡ 
  if (trimono B) then (lfp B x) else (top::'a::complete_lattice)"
definition RECT ("REC⇩T") where "RECT B x ≡ 
  if (trimono B) then (flatf_gfp B x) else (top::'a::complete_lattice)"

lemma RECT_gfp_def: "RECT B x = 
  (if (trimono B) then (gfp B x) else (top::'a::complete_lattice))"
  unfolding RECT_def
  by (auto simp: gfp_eq_flatf_gfp[OF trimonoD_flatf_ge trimonoD_mono])

lemma REC_unfold: "trimono B ==> REC B x = B (REC B) x"
  unfolding REC_def [abs_def]
  by (simp add: lfp_unfold[OF trimonoD_mono, symmetric])

lemma RECT_unfold: "[|trimono B|] ==> RECT B x = B (RECT B) x"
  unfolding RECT_def [abs_def]
  by (simp add: flatf_ord.fixp_unfold[OF trimonoD_flatf_ge, symmetric])

lemma REC_mono[refine_mono]:
  assumes [simp]: "trimono B"
  assumes LE: "!!F x. (B F x) ≤ (B' F x)"
  shows "(REC B x) ≤ (REC B' x)"
  unfolding REC_def
  apply clarsimp
  apply (rule lfp_mono[THEN le_funD])
  apply (rule LE[THEN le_funI])
  done

lemma RECT_mono[refine_mono]:
  assumes [simp]: "trimono B'"
  assumes LE: "!!F x. flat_ge (B F x) (B' F x)"
  shows "flat_ge (RECT B x) (RECT B' x)"
  unfolding RECT_def
  apply clarsimp
  apply (rule flatf_fp_mono, (simp_all add: trimonoD) [2])
  apply (rule LE)
  done

lemma REC_le_RECT: "trimono body ==> REC body x ≤ RECT body x"
  unfolding REC_def RECT_gfp_def
  apply clarsimp
  apply (rule lfp_le_gfp[THEN le_funD])
  by (simp add: trimonoD)

print_statement flatf_fp_induct_pointwise
theorem lfp_induct_pointwise:
  fixes a::'a
  assumes ADM1: "!!a x. chain_admissible (λb. ∀a x. pre a x --> post a x (b x))"
  assumes ADM2: "!!a x. pre a x --> post a x bot"
  assumes MONO: "mono B"
  assumes P0: "pre a x"
  assumes IS: 
    "!!f a x.
        [|!!a' x'. pre a' x' ==> post a' x' (f x'); pre a x;
         f ≤ (lfp B)|]
        ==> post a x (B f x)"
  shows "post a x (lfp B x)"
proof -
  def u≡"lfp B"

  have [simp]: "!!f. f≤lfp B ==> B f ≤ lfp B"
    by (metis (poly_guards_query) MONO lfp_unfold monoD)

  have "(∀a x. pre a x --> post a x (lfp B x)) ∧ lfp B ≤ u"
    apply (rule lfp_cadm_induct[where f=B])
    apply (rule admissible_conj)
    apply (rule ADM1)
    apply (rule)
    apply (blast intro: Sup_least)
    apply (simp add: le_fun_def ADM2) []
    apply fact
    apply (intro conjI allI impI)
    unfolding u_def
    apply (blast intro: IS)
    apply simp
    done
  with P0 show ?thesis by blast
qed


lemma REC_rule_arb:
  fixes x::"'x" and arb::'arb
  assumes M: "trimono body"
  assumes I0: "pre arb x"
  assumes IS: "!!f arb x. [|
    !!arb' x. pre arb' x ==> f x ≤ M arb' x; pre arb x; f ≤ REC body
  |] ==> body f x ≤ M arb x"
  shows "REC body x ≤ M arb x"
  unfolding REC_def
  apply (clarsimp simp: M)
  apply (rule lfp_induct_pointwise[where pre=pre])
  apply (auto intro!: chain_admissibleI SUP_least) [2]
  apply (simp add: trimonoD[OF M])
  apply (rule I0)
  apply (rule IS, assumption+)
  apply (auto simp: REC_def[abs_def] intro!: le_funI dest: le_funD) []
  done

lemma RECT_rule_arb:
  assumes M: "trimono body"
  assumes WF: "wf (V::('x×'x) set)"
  assumes I0: "pre (arb::'arb) (x::'x)"
  assumes IS: "!!f arb x. [| 
      !!arb' x'. [|pre arb' x'; (x',x)∈V|] ==> f x' ≤ M arb' x'; 
      pre arb x;
      RECT body = f
    |]  ==> body f x ≤ M arb x"
  shows "RECT body x ≤ M arb x"
  apply (rule wf_fixp_induct[where fp=RECT and pre=pre and B=body])
  apply (rule ext)
  apply (rule RECT_unfold)
  apply (simp_all add: M) [2]
  apply (rule WF)
  apply fact
  apply (rule IS)
  apply assumption
  apply assumption
  apply assumption
  done

lemma REC_rule:
  fixes x::"'x"
  assumes M: "trimono body"
  assumes I0: "pre x"
  assumes IS: "!!f x. [| !!x. pre x ==> f x ≤ M x; pre x |] 
    ==> body f x ≤ M x"
  shows "REC body x ≤ M x"
  by (rule REC_rule_arb[where pre="λ_. pre" and M="λ_. M", OF assms])

lemma RECT_rule:
  assumes M: "trimono body"
  assumes WF: "wf (V::('x×'x) set)"
  assumes I0: "pre (x::'x)"
  assumes IS: "!!f x. [| !!x'. [|pre x'; (x',x)∈V|] ==> f x' ≤ M x'; pre x; 
                        RECT body = f
    |] ==> body f x ≤ M x"
  shows "RECT body x ≤ M x"
  by (rule RECT_rule_arb[where pre="λ_. pre" and M="λ_. M", OF assms])




(* TODO: Can we set-up induction method to work with such goals? *)
lemma REC_rule_arb2:
  assumes M: "trimono body"
  assumes I0: "pre (arb::'arb) (arc::'arc) (x::'x)"
  assumes IS: "!!f arb arc x. [| 
      !!arb' arc' x'. [|pre arb' arc' x' |] ==> f x' ≤ M arb' arc' x'; 
      pre arb arc x
    |]  ==> body f x ≤ M arb arc x"
  shows "REC body x ≤ M arb arc x"
  apply (rule order_trans)
  apply (rule REC_rule_arb[
    where pre="split pre" and M="split M" and arb="(arb, arc)", 
    OF M])
  by (auto intro: assms)

lemma REC_rule_arb3:
  assumes M: "trimono body"
  assumes I0: "pre (arb::'arb) (arc::'arc) (ard::'ard) (x::'x)"
  assumes IS: "!!f arb arc ard x. [| 
      !!arb' arc' ard' x'. [|pre arb' arc' ard' x'|] ==> f x' ≤ M arb' arc' ard' x';
      pre arb arc ard x 
    |]  ==> body f x ≤ M arb arc ard x"
  shows "REC body x ≤ M arb arc ard x"
  apply (rule order_trans)
  apply (rule REC_rule_arb2[
    where pre="split pre" and M="split M" and arb="(arb, arc)" and arc="ard", 
    OF M])
  by (auto intro: assms)

lemma RECT_rule_arb2:
  assumes M: "trimono body"
  assumes WF: "wf (V::'x rel)"
  assumes I0: "pre (arb::'arb) (arc::'arc) (x::'x)"
  assumes IS: "!!f arb arc x. [| 
      !!arb' arc' x'. [|pre arb' arc' x'; (x',x)∈V|] ==> f x' ≤ M arb' arc' x'; 
      pre arb arc x;
      f ≤ RECT body
    |]  ==> body f x ≤ M arb arc x"
  shows "RECT body x ≤ M arb arc x"
  apply (rule order_trans)
  apply (rule RECT_rule_arb[
    where pre="split pre" and M="split M" and arb="(arb, arc)", 
    OF M WF])
  by (auto intro: assms)

lemma RECT_rule_arb3:
  assumes M: "trimono body"
  assumes WF: "wf (V::'x rel)"
  assumes I0: "pre (arb::'arb) (arc::'arc) (ard::'ard) (x::'x)"
  assumes IS: "!!f arb arc ard x. [| 
      !!arb' arc' ard' x'. [|pre arb' arc' ard' x'; (x',x)∈V|] ==> f x' ≤ M arb' arc' ard' x'; 
    pre arb arc ard x;
    f ≤ RECT body
  |]  ==> body f x ≤ M arb arc ard x"
  shows "RECT body x ≤ M arb arc ard x"
  apply (rule order_trans)
  apply (rule RECT_rule_arb2[
    where pre="split pre" and M="split M" and arb="(arb, arc)" and arc="ard", 
    OF M WF])
  by (auto intro: assms)



(* Obsolete, provide a variant to show nofail.
text {* The following lemma shows that greatest and least fixed point are equal,
  if we can provide a variant. *}
lemma RECT_eq_REC:
  assumes MONO: "flatf_mono_le body"
  assumes MONO_GE: "flatf_mono_ge body"
  assumes WF: "wf V"
  assumes I0: "I x"
  assumes IS: "!!f x. I x ==> 
    body (λx'. if (I x' ∧ (x',x)∈V) then f x' else top) x ≤ body f x"
  shows "RECT body x = REC body x"
  unfolding RECT_def REC_def 
proof (simp add: MONO MONO_GE)
  have "I x --> flatf_gfp body x ≤ flatf_lfp body x"
    using WF
    apply (induct rule: wf_induct_rule)
    apply (rule impI)
    apply (subst flatf_ord.fixp_unfold[OF MONO])
    apply (subst flatf_ord.fixp_unfold[OF MONO_GE])
    apply (rule order_trans[OF _ IS])
    apply (rule monoD[OF MONO,THEN le_funD])
    apply (rule le_funI)
    apply simp
    apply simp
    done
  


  from lfp_le_gfp' MONO have "lfp body x ≤ gfp body x" .
  moreover have "I x --> gfp body x ≤ lfp body x"
    using WF
    apply (induct rule: wf_induct[consumes 1])
    apply (rule impI)
    apply (subst lfp_unfold[OF MONO])
    apply (subst gfp_unfold[OF MONO])
    apply (rule order_trans[OF _ IS])
    apply (rule monoD[OF MONO,THEN le_funD])
    apply (rule le_funI)
    apply simp
    apply simp
    done
  ultimately show ?thesis
    unfolding REC_def RECT_def gfp_eq_flatf_gfp[OF MONO_GE MONO, symmetric]
    apply (rule_tac antisym)
    using I0 MONO MONO_GE by auto
qed
*)

lemma RECT_eq_REC: 
  -- "Partial and total correct recursion are equal if total 
    recursion does not fail."
  assumes M: "trimono body"
  assumes NT: "RECT body x ≠ top"
  shows "RECT body x = REC body x"
  using NT M
  unfolding RECT_def REC_def
proof clarsimp
  from lfp_unfold[OF trimonoD_mono[OF M], symmetric]
  have "flatf_ge (body (lfp body)) (lfp body)" by simp
  note flatf_ord.fixp_lowerbound[
    OF trimonoD_flatf_ge[OF M], of "lfp body", OF this]
  moreover assume "flatf_gfp body x ≠ top"
  ultimately show "flatf_gfp body x = lfp body x"
    by (auto simp add: fun_ord_def flat_ord_def)
qed

lemma RECT_eq_REC_tproof:
  -- "Partial and total correct recursion are equal if we can provide a 
    termination proof."
  fixes a :: 'a
  assumes M: "trimono body"
  assumes WF: "wf V"
  assumes I0: "pre a x"
  assumes IS: "!!f arb x.
          [|!!arb' x'. [|pre arb' x'; (x', x) ∈ V|] ==> f x' ≤ M arb' x'; 
            pre arb x; REC⇩T body = f|]
          ==> body f x ≤ M arb x"
  assumes NT: "M a x ≠ top"
  shows "RECT body x = REC body x ∧ RECT body x ≤ M a x"
proof
  show "RECT body x ≤ M a x"
    by (rule RECT_rule_arb[OF M WF, where pre=pre, OF I0 IS])
  
  with NT have "RECT body x ≠ top" by (metis top.extremum_unique)
  thus "RECT body x = REC body x" by (rule RECT_eq_REC[OF M])
qed


subsection {* Transfer *}

lemma (in transfer) transfer_RECT'[refine_transfer]:
  assumes REC_EQ: "!!x. fr x = b fr x"
  assumes REF: "!!F f x. [|!!x. α (f x) ≤ F x |] ==> α (b f x) ≤ B F x"
  shows "α (fr x) ≤ RECT B x"
  unfolding RECT_def
proof clarsimp
  assume MONO: "trimono B"
  show "α (fr x) ≤ flatf_gfp B x"
    apply (rule flatf_fixp_transfer[where B=B and fp'=fr and P="op =", 
        OF _ trimonoD_flatf_ge[OF MONO]])
    apply simp
    apply (rule ext, fact)
    apply (simp)
    apply (simp,rule REF, blast)    
    done
qed

lemma (in ordered_transfer) transfer_RECT[refine_transfer]:
  assumes REF: "!!F f x. [|!!x. α (f x) ≤ F x |] ==> α (b f x) ≤ B F x"
  assumes M: "trimono b"
  shows "α (RECT b x) ≤ RECT B x"
  apply (rule transfer_RECT')
  apply (rule RECT_unfold[OF M])
  by fact

lemma (in dist_transfer) transfer_REC[refine_transfer]:
  assumes REF: "!!F f x. [|!!x. α (f x) ≤ F x |] ==> α (b f x) ≤ B F x"
  assumes M: "trimono b"
  shows "α (REC b x) ≤ REC B x"
  unfolding REC_def
  (* TODO: Clean up *)
  apply (clarsimp simp: M)
  apply (rule lfp_induct_pointwise[where B=b and pre="op="])
  apply (rule)
  apply clarsimp
  apply (subst SUP_def)
  apply (subst α_dist)
  apply (auto simp add: chain_def le_fun_def) []
  apply (rule Sup_least)
  apply auto []
  apply simp
  apply (simp add: trimonoD[OF M])
  apply (rule refl)
  apply (subst lfp_unfold)
  apply (simp add: trimonoD)
  apply (rule REF)
  apply blast
  done


end