```section ‹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,(≤)}"
lemma trimono_alt:
"trimono B ⟷ (∀ord∈fun_ord`triords. monotone ord ord B)"
unfolding trimono_def
by (auto simp: 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 = B (REC B)"
unfolding REC_def [abs_def]
by (simp add: lfp_unfold[OF trimonoD_mono, symmetric])

lemma RECT_unfold: "⟦trimono B⟧ ⟹ RECT B = B (RECT B)"
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: "REC body x ≤ RECT body x"
unfolding REC_def RECT_gfp_def
apply (cases "trimono body")
apply clarsimp
apply (rule lfp_le_gfp[THEN le_funD])
apply simp
done

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 -
define u where "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)
apply (blast intro: Sup_least)
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 (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 RECT_unfold)
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; f ≤ REC body ⟧
⟹ 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="case_prod pre" and M="case_prod 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="case_prod pre" and M="case_prod 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="case_prod pre" and M="case_prod 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="case_prod pre" and M="case_prod 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
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 NT: "RECT body x ≠ top"
shows "RECT body x = REC body x"
proof (cases "trimono body")
case M: True
show ?thesis
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
next
case False thus ?thesis unfolding RECT_def REC_def by auto
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)
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="(=)",
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, THEN fun_cong])
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="(=)"])
apply (rule)
apply clarsimp
apply (subst α_dist)
apply (auto simp add: chain_def le_fun_def) []
apply (rule Sup_least)
apply auto []
apply simp
apply (rule refl)
apply (subst lfp_unfold)
apply (rule REF)
apply blast
done

(* TODO: Could we base the whole refine_transfer-stuff on arbitrary relations *)
(* TODO: For enres-breakdown, we had to do antisymmetry, in order to get TR_top.
What is the general shape of tr-relations for that, such that we could show equality directly?
*)
lemma RECT_transfer_rel:
assumes [simp]: "trimono F" "trimono F'"
assumes TR_top[simp]: "⋀x. tr x top"
assumes P_start[simp]: "P x x'"
assumes IS: "⋀D D' x x'. ⟦ ⋀x x'. P x x' ⟹ tr (D x) (D' x'); P x x'; RECT F = D ⟧ ⟹ tr (F D x) (F' D' x')"
shows "tr (RECT F x) (RECT F' x')"
unfolding RECT_def
apply auto
apply (rule flatf_gfp_transfer[where tr=tr and P=P])
apply (auto simp: trimonoD_flatf_ge)
apply (rule IS)
apply (auto simp: RECT_def)
done

lemma RECT_transfer_rel':
assumes [simp]: "trimono F" "trimono F'"
assumes TR_top[simp]: "⋀x. tr x top"
assumes P_start[simp]: "P x x'"
assumes IS: "⋀D D' x x'. ⟦ ⋀x x'. P x x' ⟹ tr (D x) (D' x'); P x x' ⟧ ⟹ tr (F D x) (F' D' x')"
shows "tr (RECT F x) (RECT F' x')"
using RECT_transfer_rel[where tr=tr and P=P,OF assms(1,2,3,4)] IS by blast

end

```