# Theory Refine_Chapter

chapter ‹Refinement Framework›
(*<*)
theory Refine_Chapter
imports Main
begin
end
(*>*)


# Theory Refine_Mono_Prover

theory Refine_Mono_Prover
imports Main Automatic_Refinement.Refine_Lib
begin
ML_file ‹refine_mono_prover.ML›

setup Refine_Mono_Prover.setup
declaration Refine_Mono_Prover.decl_setup

method_setup refine_mono =
‹Scan.succeed (fn ctxt => SIMPLE_METHOD' (
Refine_Mono_Prover.untriggered_mono_tac ctxt
))›
"Refinement framework: Monotonicity prover"

locale mono_setup_loc =
― ‹Locale to set up monotonicity prover for given ordering operator›
fixes le :: "'a ⇒ 'a ⇒ bool"
assumes refl: "le x x"
begin
lemma monoI: "(⋀f g x. (⋀x. le (f x) (g x)) ⟹ le (B f x) (B g x))
⟹ monotone (fun_ord le) (fun_ord le) B"
unfolding monotone_def fun_ord_def by blast

lemma mono_if: "⟦le t t'; le e e'⟧ ⟹ le (If b t e) (If b t' e')" by auto
lemma mono_let: "(⋀x. le (f x) (f' x)) ⟹ le (Let x f) (Let x f')" by auto

lemmas mono_thms[refine_mono] = monoI mono_if mono_let refl

declaration ‹Refine_Mono_Prover.declare_mono_triggers @{thms monoI}›

end

interpretation order_mono_setup: mono_setup_loc "(≤) :: 'a::preorder ⇒ _"
by standard auto

declaration ‹Refine_Mono_Prover.declare_mono_triggers @{thms Orderings.monoI}›

lemmas [refine_mono] =
lfp_mono[OF le_funI, THEN le_funD]
gfp_mono[OF le_funI, THEN le_funD]

end



# File ‹refine_mono_prover.ML›

signature REFINE_MONO_PROVER = sig
(* A generic automatic case splitter *)
type pat_extractor =
term -> (term * ((Proof.context -> conv) -> Proof.context -> conv)) option

val gen_split_cases_tac: pat_extractor -> Proof.context -> tactic'

(* Recognizes all patterns of the form _ (case x of ...) (case x of ...) *)
val split_cases_tac: Proof.context -> tactic'

(* Monotonicity prover *)
val get_mono_thms: Proof.context -> thm list
val add_mono_thm: thm -> Context.generic -> Context.generic
val del_mono_thm: thm -> Context.generic -> Context.generic
val mono_tac: Proof.context -> tactic'

(* Monotonicity solver *)
val untriggered_mono_tac: Proof.context -> tactic'
val declare_mono_triggers: thm list -> morphism -> Context.generic -> Context.generic

(* Setup *)
val decl_setup: morphism -> Context.generic -> Context.generic
val setup: theory -> theory

end

structure Refine_Mono_Prover : REFINE_MONO_PROVER = struct
type pat_extractor =
term -> (term * ((Proof.context -> conv) -> Proof.context -> conv)) option

(* Case Splitter, taken from Krauss' partial_function. *)
local
(*rewrite conclusion with k-th assumtion*)
fun rewrite_with_asm_tac ctxt k =
Subgoal.FOCUS (fn {context = ctxt', prems, ...} =>
Local_Defs.unfold_tac ctxt' [nth prems k]) ctxt;

fun dest_case ctxt t =
case strip_comb t of
(Const (case_comb, _), args) =>
(case Ctr_Sugar.ctr_sugar_of_case ctxt case_comb of
NONE => NONE
| SOME {case_thms, ...} =>
let
val lhs = Thm.prop_of (hd case_thms)
|> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> fst;
val arity = length (snd (strip_comb lhs));
val _ = length args - arity >= 0
orelse raise TERM("dest_case: arity",[t])
(* funpow on negative argument loops until stack overflow *)
val conv = funpow (length args - arity) Conv.fun_conv
(Conv.rewrs_conv (map mk_meta_eq case_thms));
in
SOME (nth args (arity - 1), conv)
end)
| _ => NONE;
in
(*split on case expressions*)
fun gen_split_cases_tac (extract_pat:pat_extractor)
= Subgoal.FOCUS (fn {context=ctxt, ...} =>
SUBGOAL (fn (t, i) => case extract_pat t of
SOME (body, mk_conv) =>
(case dest_case ctxt body of
NONE => no_tac
| SOME (arg, conv) =>
let open Conv in
if Term.is_open arg then no_tac
else (
(DETERM o Induct.cases_tac ctxt false [[SOME arg]] NONE [])
THEN_ALL_NEW (rewrite_with_asm_tac ctxt 0)
THEN_ALL_NEW eresolve_tac ctxt @{thms thin_rl}
THEN_ALL_NEW (
CONVERSION (params_conv ~1 (mk_conv (K conv)) ctxt))
) i
end)
| _ => no_tac) 1);
end

local
open Conv
fun extract @{mpat "Trueprop (_ ?t1.0 ?t2.0)"}
= (let
val last = #2 o split_last
val (hd1,args1) = strip_comb t1
val (hd2,args2) = strip_comb t2
val x1 = last args1
val x2 = last args2
fun mk_conv conv ctxt =
arg_conv (binop_conv (conv ctxt))
in
if hd1 aconv hd2 andalso x1 aconv x2 then
SOME (t1, mk_conv)
else NONE
end
handle List.Empty => NONE)
| extract _ = NONE
in
val split_cases_tac = gen_split_cases_tac extract
end

(*
= SOME (t,fn conv => fn ctxt =>
arg_conv (arg_conv (abs_conv (#2 #> conv) ctxt)))
*)

fun split_meta_conjunction thm =
case Thm.prop_of thm of
@{const "Pure.conjunction"}$_$_ => let
val (t1,t2) = Conjunction.elim thm
in split_meta_conjunction t1 @ split_meta_conjunction t2 end
| _ => [thm]

structure Mono_Thms = Named_Sorted_Thms (
val name = @{binding refine_mono}
val description = "Refinement Framework: Monotonicity theorems"
val sort = K I
val transform = fn context => split_meta_conjunction #> map (norm_hhf (Context.proof_of context))
)

val get_mono_thms = Mono_Thms.get
val del_mono_thm = Mono_Thms.del_thm

fun mono_tac ctxt = REPEAT_ALL_NEW (
FIRST' [
Method.assm_tac ctxt,
resolve_tac ctxt (Mono_Thms.get ctxt),
split_cases_tac ctxt
]
)

fun untriggered_mono_tac ctxt = mono_tac ctxt
THEN_ALL_NEW (TRY o Tagged_Solver.solve_tac ctxt)

val mono_solver_bnd = @{binding refine_mono}
val mono_solver_name = "Refine_Mono_Prover.refine_mono" (* TODO: HACK! *)

val declare_mono_triggers =

val decl_setup =
Tagged_Solver.declare_solver
@{thms monoI monotoneI[of "(≤)" "(≤)"]} mono_solver_bnd
mono_tac

val setup = I
#> Mono_Thms.setup
end



# 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 ‹S›.
Due to the closedness property of ‹S›, it can be extended to
start at ‹x0›.
Now, we inductively construct an infinite chain in ‹S'›, such that
each element of the new chain is in relation with the corresponding
element of the original chain:
The first element is ‹x0'›.
For any element ‹i+1›, the simulation property yields the next
element.
This chain contradicts well-foundedness of ‹S'›.
›

fix f
assume CHAIN: "⋀i. (f i, f (Suc i))∈S"
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 (subgoal_tac "k = Suc i")
apply (simp add: S[symmetric] CH X)
apply simp
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 ‹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
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 (fS) ≤ 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'⊆fS"
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 (fS)"
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])
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) order.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"
lemma ccpo_monoD: "monotone (≤) (≤) f ⟹ mono f"

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

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)
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)
done

abbreviation "is_chain ≡ Complete_Partial_Order.chain (≤)"

abbreviation "is_dual_chain ≡ Complete_Partial_Order.chain (λx y. y≤x)"
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.›
"⟦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])

"⟦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 (fC)"
definition "strict f ≡ f bot = bot"
definition "inf_distrib f ≡ strict f ∧ cont f"

lemma contI[intro?]: "⟦⋀C. C≠{} ⟹ f (Sup C) = Sup (fC)⟧ ⟹ 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) = Sup (f  C)"
by (fact contD)

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 (fC)"
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 (fC)"
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 i" 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 i" 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 add: image_comp)
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

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))"
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
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


# Theory RefineG_Transfer

section ‹Transfer between Domains›
theory RefineG_Transfer
imports "../Refine_Misc"
begin
text ‹Currently, this theory is specialized to
transfers that include no data refinement.
›

definition "REFINEG_TRANSFER_POST_SIMP x y ≡ x=y"
definition [simp]: "REFINEG_TRANSFER_ALIGN x y == True"
lemma REFINEG_TRANSFER_ALIGNI: "REFINEG_TRANSFER_ALIGN x y" by simp

lemma START_REFINEG_TRANSFER:
assumes "REFINEG_TRANSFER_ALIGN d c"
assumes "c≤a"
assumes "REFINEG_TRANSFER_POST_SIMP c d"
shows "d≤a"
using assms

lemma STOP_REFINEG_TRANSFER: "REFINEG_TRANSFER_POST_SIMP c c"
unfolding REFINEG_TRANSFER_POST_SIMP_def ..

ML ‹
structure RefineG_Transfer = struct

structure Post_Processors = Theory_Data (
type T = (Proof.context -> tactic') Symtab.table
val empty = Symtab.empty
val extend = I
val merge = Symtab.join (K snd)
)

Post_Processors.map (Symtab.update_new (name,tac))
fun delete_post_processor name =
Post_Processors.map (Symtab.delete name)
val get_post_processors = Post_Processors.get #> Symtab.dest

fun post_process_tac ctxt = let
val tacs = get_post_processors (Proof_Context.theory_of ctxt)
|> map (fn (_,tac) => tac ctxt)

val tac = REPEAT_DETERM' (CHANGED o EVERY' (map (fn t => TRY o t) tacs))
in
tac
end

structure Post_Simp = Generic_Data (
type T = simpset
val empty = HOL_basic_ss
val extend = I
val merge = Raw_Simplifier.merge_ss
)

fun post_simps_op f a context = let
val ctxt = Context.proof_of context
fun do_it ss = simpset_of (f (put_simpset ss ctxt, a))
in
Post_Simp.map do_it context
end

val del_post_simps = post_simps_op (op delsimps)

fun get_post_ss ctxt = let
val ss = Post_Simp.get (Context.Proof ctxt)
val ctxt = put_simpset ss ctxt
in
ctxt
end

structure post_subst = Named_Thms
( val name = @{binding refine_transfer_post_subst}
val description = "Refinement Framework: " ^
"Transfer postprocessing substitutions" );

fun post_subst_tac ctxt = let
val s_thms = post_subst.get ctxt
val dis_tac = (ALLGOALS (Tagged_Solver.solve_tac ctxt))
val cnv = Cond_Rewr_Conv.cond_rewrs_conv dis_tac s_thms
val ts_conv = Conv.top_sweep_conv cnv ctxt
val ss = get_post_ss ctxt
in
REPEAT o CHANGED o
(Simplifier.simp_tac ss THEN' CONVERSION ts_conv)
end

structure transfer = Named_Thms
( val name = @{binding refine_transfer}
val description = "Refinement Framework: " ^
"Transfer rules" );

fun transfer_tac thms ctxt i st = let
val thms = thms @ transfer.get ctxt;
val ss = put_simpset HOL_basic_ss ctxt addsimps @{thms nested_case_prod_simp}
in
REPEAT_DETERM1 (
COND (has_fewer_prems (Thm.nprems_of st)) no_tac (
FIRST [
Method.assm_tac ctxt i,
resolve_tac ctxt thms i,
Tagged_Solver.solve_tac ctxt i,
CHANGED_PROP (simp_tac ss i)]
)) st
end

(* Adjust right term to have same structure as left one *)
fun align_tac ctxt = IF_EXGOAL (fn i => fn st =>
case Logic.concl_of_goal (Thm.prop_of st) i of
@{mpat "Trueprop (REFINEG_TRANSFER_ALIGN ?c _)"} => let
val c = Thm.cterm_of ctxt c
val cT = Thm.ctyp_of_cterm c

val rl = @{thm REFINEG_TRANSFER_ALIGNI}
|> Thm.incr_indexes (Thm.maxidx_of st + 1)
|> Thm.instantiate' [NONE,SOME cT] [NONE,SOME c]
(*val _ = tracing (@{make_string} rl)*)
in
resolve_tac ctxt [rl] i st
end
| _ => Seq.empty
)

fun post_transfer_tac thms ctxt = let open Autoref_Tacticals in
resolve_tac ctxt @{thms START_REFINEG_TRANSFER}
THEN' align_tac ctxt
THEN' IF_SOLVED (transfer_tac thms ctxt)
(post_process_tac ctxt THEN' resolve_tac ctxt @{thms STOP_REFINEG_TRANSFER})
(K all_tac)

end

fun get_post_simp_rules context = Context.proof_of context
|> get_post_ss
|> simpset_of
|> Raw_Simplifier.dest_ss
|> #simps |> map snd

local
val del_ps = Thm.declaration_attribute (del_post_simps o single)
in
val setup = I
#> post_subst.setup
#> transfer.setup
#> Attrib.setup @{binding refine_transfer_post_simp}
("declaration of transfer post simplification rules")
@{binding refine_transfer_post_simps}, get_post_simp_rules)

end
end
›

setup ‹RefineG_Transfer.setup›
method_setup refine_transfer =
‹Scan.lift (Args.mode "post") -- Attrib.thms
>> (fn (post,thms) => fn ctxt => SIMPLE_METHOD'
( if post then RefineG_Transfer.post_transfer_tac thms ctxt
else RefineG_Transfer.transfer_tac thms ctxt))
› "Invoke transfer rules"

locale transfer = fixes α :: "'c ⇒ 'a::complete_lattice"
begin

text ‹
In the following, we define some transfer lemmas for general
HOL - constructs.
›

lemma transfer_if[refine_transfer]:
assumes "b ⟹ α s1 ≤ S1"
assumes "¬b ⟹ α s2 ≤ S2"
shows "α (if b then s1 else s2) ≤ (if b then S1 else S2)"
using assms by auto

lemma transfer_prod[refine_transfer]:
assumes "⋀a b. α (f a b) ≤ F a b"
shows "α (case_prod f x) ≤ (case_prod F x)"
using assms by (auto split: prod.split)

lemma transfer_Let[refine_transfer]:
assumes "⋀x. α (f x) ≤ F x"
shows "α (Let x f) ≤ Let x F"
using assms by auto

lemma transfer_option[refine_transfer]:
assumes "α fa ≤ Fa"
assumes "⋀x. α (fb x) ≤ Fb x"
shows "α (case_option fa fb x) ≤ case_option Fa Fb x"
using assms by (auto split: option.split)

lemma transfer_sum[refine_transfer]:
assumes "⋀l. α (fl l) ≤ Fl l"
assumes "⋀r. α (fr r) ≤ Fr r"
shows "α (case_sum fl fr x) ≤ (case_sum Fl Fr x)"
using assms by (auto split: sum.split)

lemma transfer_list[refine_transfer]:
assumes "α fn ≤ Fn"
assumes "⋀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 transfer_rec_list[refine_transfer]:
assumes FN: "⋀s. α (fn s) ≤ fn' s"
assumes FC: "⋀x l rec rec' s. ⟦ ⋀s. α (rec s) ≤ (rec' s) ⟧
⟹ α (fc x l rec s) ≤ fc' x l rec' s"
shows "α (rec_list fn fc l s) ≤ rec_list fn' fc' l s"
apply (induct l arbitrary: s)
done

lemma transfer_rec_nat[refine_transfer]:
assumes FN: "⋀s. α (fn s) ≤ fn' s"
assumes FC: "⋀n rec rec' s. ⟦ ⋀s. α (rec s) ≤ rec' s ⟧
⟹ α (fs n rec s) ≤ fs' n rec' s"
shows "α (rec_nat fn fs n s) ≤ rec_nat fn' fs' n s"
apply (induct n arbitrary: s)
done

end

text ‹Transfer into complete lattice structure›
locale ordered_transfer = transfer +
constrains α :: "'c::complete_lattice ⇒ 'a::complete_lattice"

text ‹Transfer into complete lattice structure with distributive
transfer function.›
locale dist_transfer = ordered_transfer +
constrains α :: "'c::complete_lattice ⇒ 'a::complete_lattice"
assumes α_dist: "⋀A. is_chain A ⟹ α (Sup A) = Sup (αA)"
begin
lemma α_mono[simp, intro!]: "mono α"
apply rule
apply (subgoal_tac "is_chain {x,y}")
apply (drule α_dist)
apply (auto simp: le_iff_sup) []
apply (rule chainI)
apply auto
done

lemma α_strict[simp]: "α bot = bot"
using α_dist[of "{}"] by simp
end

text ‹Transfer into ccpo›
locale ccpo_transfer = transfer α for
α :: "'c::ccpo ⇒ 'a::complete_lattice"

text ‹Transfer into ccpo with distributive
transfer function.›
locale dist_ccpo_transfer = ccpo_transfer α
for α :: "'c::ccpo ⇒ 'a::complete_lattice" +
assumes α_dist: "⋀A. is_chain A ⟹ α (Sup A) = Sup (αA)"
begin

lemma α_mono[simp, intro!]: "mono α"
proof
fix x y :: 'c
assume LE: "x≤y"
hence C[simp, intro!]: "is_chain {x,y}" by (auto intro: chainI)
from LE have "α x ≤ sup (α x) (α y)" by simp
also have "… = Sup (α{x,y})" by simp
also have "… = α (Sup {x,y})"
by (rule α_dist[symmetric]) simp
also have "Sup {x,y} = y"
apply (rule antisym)
apply (rule ccpo_Sup_least[OF C]) using LE apply auto []
apply (rule ccpo_Sup_upper[OF C]) by auto
finally show "α x ≤ α y" .
qed

lemma α_strict[simp]: "α (Sup {}) = bot"
using α_dist[of "{}"] by simp
end

end


# 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"

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

"(⋀x. P x b) ⟹
ccpo.admissible (flatf_lub b) (flatf_ord b) (λg. ∀x. P x (g x))"
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 (blast intro: cond_bot)
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



# Theory RefineG_Recursion

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_ordtriords. 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 = 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



# Theory RefineG_Assert

section ‹{Assert and Assume}›
theory RefineG_Assert
imports RefineG_Transfer
begin

definition "iASSERT return Φ ≡ if Φ then return () else top"
definition "iASSUME return Φ ≡ if Φ then return () else bot"

locale generic_Assert =
fixes bind ::
"('mu::complete_lattice) ⇒ (unit ⇒ ('ma::complete_lattice)) ⇒ 'ma"
fixes return :: "unit ⇒ 'mu"
fixes ASSERT
fixes ASSUME
assumes ibind_strict:
"bind bot f = bot"
"bind top f = top"
assumes imonad1: "bind (return u) f = f u"
assumes ASSERT_eq: "ASSERT ≡ iASSERT return"
assumes ASSUME_eq: "ASSUME ≡ iASSUME return"
begin
lemma ASSERT_simps[simp,code]:
"ASSERT True = return ()"
"ASSERT False = top"
unfolding ASSERT_eq iASSERT_def by auto

lemma ASSUME_simps[simp,code]:
"ASSUME True = return ()"
"ASSUME False = bot"
unfolding ASSUME_eq iASSUME_def by auto

lemma le_ASSERTI: "⟦ Φ ⟹ M≤M' ⟧ ⟹ M ≤ bind (ASSERT Φ) (λ_. M')"
apply (cases Φ) by (auto simp: ibind_strict imonad1)

lemma le_ASSERTI_pres: "⟦ Φ ⟹ M≤bind (ASSERT Φ) (λ_. M') ⟧
⟹ M ≤ bind (ASSERT Φ) (λ_. M')"
apply (cases Φ) by (auto simp: ibind_strict imonad1)

lemma ASSERT_leI: "⟦ Φ; Φ ⟹ M≤M' ⟧ ⟹ bind (ASSERT Φ) (λ_. M) ≤ M'"
apply (cases Φ) by (auto simp: ibind_strict imonad1)

lemma ASSUME_leI: "⟦ Φ ⟹ M≤M' ⟧ ⟹ bind (ASSUME Φ) (λ_. M) ≤ M'"
apply (cases Φ) by (auto simp: ibind_strict imonad1)
lemma ASSUME_leI_pres: "⟦ Φ ⟹ bind (ASSUME Φ) (λ_. M)≤M' ⟧
⟹ bind (ASSUME Φ) (λ_. M) ≤ M'"
apply (cases Φ) by (auto simp: ibind_strict imonad1)
lemma le_ASSUMEI: "⟦ Φ; Φ ⟹ M≤M' ⟧ ⟹ M ≤ bind (ASSUME Φ) (λ_. M')"
apply (cases Φ) by (auto simp: ibind_strict imonad1)

text ‹The order of these declarations does matter!›
lemmas [intro?] = ASSERT_leI le_ASSUMEI
lemmas [intro?] = le_ASSERTI ASSUME_leI

lemma ASSERT_le_iff:
"bind (ASSERT Φ) (λ_. S) ≤ S' ⟷ (S'≠top ⟶ Φ) ∧ S≤S'"
by (cases Φ) (auto simp: ibind_strict imonad1 simp: top_unique)

lemma ASSUME_le_iff:
"bind (ASSUME Φ) (λ_. S) ≤ S' ⟷ (Φ ⟶ S≤S')"
by (cases Φ) (auto simp: ibind_strict imonad1)

lemma le_ASSERT_iff:
"S ≤ bind (ASSERT Φ) (λ_. S') ⟷ (Φ ⟶ S≤S')"
by (cases Φ) (auto simp: ibind_strict imonad1)

lemma le_ASSUME_iff:
"S ≤ bind (ASSUME Φ) (λ_. S') ⟷ (S≠bot ⟶ Φ) ∧ S≤S'"
by (cases Φ) (auto simp: ibind_strict imonad1 simp: bot_unique)
end

text ‹
This locale transfer's asserts and assumes.
To remove them, use the next locale.
›
locale transfer_generic_Assert =
c: generic_Assert cbind creturn cASSERT cASSUME +
a: generic_Assert abind areturn aASSERT aASSUME +
ordered_transfer α
for cbind :: "('muc::complete_lattice)
⇒ (unit⇒'mac) ⇒ ('mac::complete_lattice)"
and creturn :: "unit ⇒ 'muc" and cASSERT and cASSUME
and abind :: "('mua::complete_lattice)
⇒ (unit⇒'maa) ⇒ ('maa::complete_lattice)"
and areturn :: "unit ⇒ 'mua" and aASSERT and aASSUME
and α :: "'mac ⇒ 'maa"
begin
lemma transfer_ASSERT[refine_transfer]:
"⟦Φ ⟹ α M ≤ M'⟧
⟹ α (cbind (cASSERT Φ) (λ_. M)) ≤ (abind (aASSERT Φ) (λ_. M'))"
apply (cases Φ)
done

lemma transfer_ASSUME[refine_transfer]:
"⟦Φ; Φ ⟹ α M ≤ M'⟧
⟹ α (cbind (cASSUME Φ) (λ_. M)) ≤ (abind (aASSUME Φ) (λ_. M'))"
done

end

locale transfer_generic_Assert_remove =
a: generic_Assert abind areturn aASSERT aASSUME +
transfer α
for abind :: "('mua::complete_lattice)
⇒ (unit⇒'maa) ⇒ ('maa::complete_lattice)"
and areturn :: "unit ⇒ 'mua" and aASSERT and aASSUME
and α :: "'mac ⇒ 'maa"
begin
lemma transfer_ASSERT_remove[refine_transfer]:
"⟦ Φ ⟹ α M ≤ M' ⟧ ⟹ α M ≤ abind (aASSERT Φ) (λ_. M')"
by (rule a.le_ASSERTI)

lemma transfer_ASSUME_remove[refine_transfer]:
"⟦ Φ; Φ ⟹ α M ≤ M' ⟧ ⟹ α M ≤ abind (aASSUME Φ) (λ_. M')"
by (rule a.le_ASSUMEI)
end

end


# Theory Refine_Basic

section ‹Basic Concepts›
theory Refine_Basic
imports Main
Refine_Misc
"Generic/RefineG_Recursion"
"Generic/RefineG_Assert"
begin

subsection ‹Nondeterministic Result Lattice and Monad›
text ‹
In this section we introduce a complete lattice of result sets with an
additional top element that represents failure. On this lattice, we define
a monad: The return operator models a result that consists of a single value,
and the bind operator models applying a function to all results.
Binding a failure yields always a failure.

In addition to the return operator, we also introduce the operator
‹RES›, that embeds a set of results into our lattice. Its synonym for
a predicate is ‹SPEC›.

Program correctness is expressed by refinement, i.e., the expression
‹M ≤ SPEC Φ› means that ‹M› is correct w.r.t.\
specification ‹Φ›. This suggests the following view on the program
lattice: The top-element is the result that is never correct. We call this
result ‹FAIL›. The bottom element is the program that is always correct.
It is called ‹SUCCEED›. An assertion can be encoded by failing if the
asserted predicate is not true. Symmetrically, an assumption is encoded by
succeeding if the predicate is not true.
›

datatype 'a nres = FAILi | RES "'a set"
text ‹
‹FAILi› is only an internal notation, that should not be exposed to
the user.
Instead, ‹FAIL› should be used, that is defined later as abbreviation
for the top element of the lattice.
›
instantiation nres :: (type) complete_lattice
begin
fun less_eq_nres where
"_ ≤ FAILi ⟷ True" |
"(RES a) ≤ (RES b) ⟷ a⊆b" |
"FAILi ≤ (RES _) ⟷ False"

fun less_nres where
"FAILi < _ ⟷ False" |
"(RES _) < FAILi ⟷ True" |
"(RES a) < (RES b) ⟷ a⊂b"

fun sup_nres where
"sup _ FAILi = FAILi" |
"sup FAILi _ = FAILi" |
"sup (RES a) (RES b) = RES (a∪b)"

fun inf_nres where
"inf x FAILi = x" |
"inf FAILi x = x" |
"inf (RES a) (RES b) = RES (a∩b)"

definition "Sup X ≡ if FAILi∈X then FAILi else RES (⋃{x . RES x ∈ X})"
definition "Inf X ≡ if ∃x. RES x∈X then RES (⋂{x . RES x ∈ X}) else FAILi"

definition "bot ≡ RES {}"
definition "top ≡ FAILi"

instance
apply (intro_classes)
unfolding Sup_nres_def Inf_nres_def bot_nres_def top_nres_def
apply (case_tac x, case_tac [!] y, auto) []
apply (case_tac x, auto) []
apply (case_tac x, case_tac [!] y, case_tac [!] z, auto) []
apply (case_tac x, (case_tac [!] y)?, auto) []
apply (case_tac x, (case_tac [!] y)?, simp_all) []
apply (case_tac x, (case_tac [!] y)?, auto) []
apply (case_tac x, case_tac [!] y, case_tac [!] z, auto) []
apply (case_tac x, (case_tac [!] y)?, auto) []
apply (case_tac x, (case_tac [!] y)?, auto) []
apply (case_tac x, case_tac [!] y, case_tac [!] z, auto) []
apply (case_tac x, auto) []
apply (case_tac z, fastforce+) []
apply (case_tac x, auto) []
apply (case_tac z, fastforce+) []
apply auto []
apply auto []
done

end

abbreviation "FAIL ≡ top::'a nres"
abbreviation "SUCCEED ≡ bot::'a nres"
abbreviation "SPEC Φ ≡ RES (Collect Φ)"
definition "RETURN x ≡ RES {x}"

text ‹We try to hide the original ‹FAILi›-element as well as possible.
›
lemma nres_cases[case_names FAIL RES, cases type]:
obtains "M=FAIL" | X where "M=RES X"
apply (cases M, fold top_nres_def) by auto

lemma nres_simp_internals:
"RES {} = SUCCEED"
"FAILi = FAIL"
unfolding top_nres_def bot_nres_def by simp_all

lemma nres_inequalities[simp]:
"FAIL ≠ RES X"
"FAIL ≠ SUCCEED"
"FAIL ≠ RETURN x"
"SUCCEED ≠ FAIL"
"SUCCEED ≠ RETURN x"
"RES X ≠ FAIL"
"RETURN x ≠ FAIL"
"RETURN x ≠ SUCCEED"
unfolding top_nres_def bot_nres_def RETURN_def
by auto

lemma nres_more_simps[simp]:
"SUCCEED = RES X ⟷ X={}"
"RES X = SUCCEED ⟷ X={}"
"RES X = RETURN x ⟷ X={x}"
"RES X = RES Y ⟷ X=Y"
"RETURN x = RES X ⟷ {x}=X"
"RETURN x = RETURN y ⟷ x=y"
unfolding top_nres_def bot_nres_def RETURN_def by auto

lemma nres_order_simps[simp]:
"⋀M. SUCCEED ≤ M"
"⋀M. M ≤ SUCCEED ⟷ M=SUCCEED"
"⋀M. M ≤ FAIL"
"⋀M. FAIL ≤ M ⟷ M=FAIL"
"⋀X Y. RES X ≤ RES Y ⟷ X≤Y"
"⋀X. Sup X = FAIL ⟷ FAIL∈X"
"⋀X f. Sup (f  X) = FAIL ⟷ FAIL ∈ f  X"
"⋀X. FAIL = Sup X ⟷ FAIL∈X"
"⋀X f. FAIL = Sup (f  X) ⟷ FAIL ∈ f  X"
"⋀X. FAIL∈X ⟹ Sup X = FAIL"
"⋀X. FAIL∈f  X ⟹ Sup (f  X) = FAIL"
"⋀A. Sup (RES  A) = RES (Sup A)"
"⋀A. Sup (RES  A) = RES (Sup A)"
"⋀A. A≠{} ⟹ Inf (RESA) = RES (Inf A)"
"⋀A. A≠{} ⟹ Inf (RES  A) = RES (Inf A)"
"Inf {} = FAIL"
"Inf UNIV = SUCCEED"
"Sup {} = SUCCEED"
"Sup UNIV = FAIL"
"⋀x y. RETURN x ≤ RETURN y ⟷ x=y"
"⋀x Y. RETURN x ≤ RES Y ⟷ x∈Y"
"⋀X y. RES X ≤ RETURN y ⟷ X ⊆ {y}"
unfolding Sup_nres_def Inf_nres_def RETURN_def
by (auto simp add: bot_unique top_unique nres_simp_internals)

lemma Sup_eq_RESE:
assumes "Sup A = RES B"
obtains C where "A=RESC" and "B=Sup C"
proof -
show ?thesis
using assms unfolding Sup_nres_def
apply (simp split: if_split_asm)
apply (rule_tac C="{X. RES X ∈ A}" in that)
apply auto []
apply (case_tac x, auto simp: nres_simp_internals) []
apply (auto simp: nres_simp_internals) []
done
qed

declare nres_simp_internals[simp]

subsubsection ‹Pointwise Reasoning›

ML ‹
structure refine_pw_simps = Named_Thms
( val name = @{binding refine_pw_simps}
val description = "Refinement Framework: " ^
"Simplifier rules for pointwise reasoning" )
›
setup ‹refine_pw_simps.setup›

definition "nofail S ≡ S≠FAIL"
definition "inres S x ≡ RETURN x ≤ S"

lemma nofail_simps[simp, refine_pw_simps]:
"nofail FAIL ⟷ False"
"nofail (RES X) ⟷ True"
"nofail (RETURN x) ⟷ True"
"nofail SUCCEED ⟷ True"
unfolding nofail_def

lemma inres_simps[simp, refine_pw_simps]:
"inres FAIL = (λ_. True)"
"inres (RES X) = (λx. x∈X)"
"inres (RETURN x) = (λy. x=y)"
"inres SUCCEED = (λ_. False)"
unfolding inres_def [abs_def]

lemma not_nofail_iff:
"¬nofail S ⟷ S=FAIL" by (cases S) auto

lemma not_nofail_inres[simp, refine_pw_simps]:
"¬nofail S ⟹ inres S x"
apply (cases S) by auto

lemma intro_nofail[refine_pw_simps]:
"S≠FAIL ⟷ nofail S"
"FAIL≠S ⟷ nofail S"
by (cases S, simp_all)+

text ‹The following two lemmas will introduce pointwise reasoning for
orderings and equalities.›
lemma pw_le_iff:
"S ≤ S' ⟷ (nofail S'⟶ (nofail S ∧ (∀x. inres S x ⟶ inres S' x)))"
apply (cases S, simp_all)
apply (case_tac [!] S', auto)
done

lemma pw_eq_iff:
"S=S' ⟷ (nofail S = nofail S' ∧ (∀x. inres S x ⟷ inres S' x))"
apply (rule iffI)
apply simp
apply (rule antisym)
done

lemma pw_flat_le_iff: "flat_le S S' ⟷
(∃x. inres S x) ⟶ (nofail S ⟷ nofail S') ∧ (∀x. inres S x ⟷ inres S' x)"
by (auto simp : flat_ord_def pw_eq_iff)

lemma pw_flat_ge_iff: "flat_ge S S' ⟷
(nofail S) ⟶ nofail S' ∧ (∀x. inres S x ⟷ inres S' x)"
apply (simp add: flat_ord_def pw_eq_iff) apply safe
apply simp
apply simp
apply simp
apply (rule ccontr)
apply simp
done

lemmas pw_ords_iff = pw_le_iff pw_flat_le_iff pw_flat_ge_iff

lemma pw_leI:
"(nofail S'⟶ (nofail S ∧ (∀x. inres S x ⟶ inres S' x))) ⟹ S ≤ S'"

lemma pw_leI':
assumes "nofail S' ⟹ nofail S"
assumes "⋀x. ⟦nofail S'; inres S x⟧ ⟹ inres S' x"
shows "S ≤ S'"
using assms

lemma pw_eqI:
assumes "nofail S = nofail S'"
assumes "⋀x. inres S x ⟷ inres S' x"
shows "S=S'"
using assms by (simp add: pw_eq_iff)

lemma pwD1:
assumes "S≤S'" "nofail S'"
shows "nofail S"
using assms by (simp add: pw_le_iff)

lemma pwD2:
assumes "S≤S'" "inres S x"
shows "inres S' x"
using assms

lemmas pwD = pwD1 pwD2

text ‹
When proving refinement, we may assume that the refined program does not
fail.›
lemma le_nofailI: "⟦ nofail M' ⟹ M ≤ M' ⟧ ⟹ M ≤ M'"
by (cases M') auto

text ‹The following lemmas push pointwise reasoning over operators,
thus converting an expression over lattice operators into a logical
formula.›

lemma pw_sup_nofail[refine_pw_simps]:
"nofail (sup a b) ⟷ nofail a ∧ nofail b"
apply (cases a, simp)
apply (cases b, simp_all)
done

lemma pw_sup_inres[refine_pw_simps]:
"inres (sup a b) x ⟷ inres a x ∨ inres b x"
apply (cases a, simp)
apply (cases b, simp)
apply (simp)
done

lemma pw_Sup_inres[refine_pw_simps]: "inres (Sup X) r ⟷ (∃M∈X. inres M r)"
apply (cases "Sup X")
apply (simp)
apply (erule bexI[rotated])
apply simp
apply (erule Sup_eq_RESE)
apply (simp)
done

lemma pw_SUP_inres [refine_pw_simps]: "inres (Sup (f  X)) r ⟷ (∃M∈X. inres (f M) r)"
using pw_Sup_inres [of "f  X"] by simp

lemma pw_Sup_nofail[refine_pw_simps]: "nofail (Sup X) ⟷ (∀x∈X. nofail x)"
apply (cases "Sup X")
apply force
apply simp
apply (erule Sup_eq_RESE)
apply auto
done

lemma pw_SUP_nofail [refine_pw_simps]: "nofail (Sup (f  X)) ⟷ (∀x∈X. nofail (f x))"
using pw_Sup_nofail [of "f  X"] by simp

lemma pw_inf_nofail[refine_pw_simps]:
"nofail (inf a b) ⟷ nofail a ∨ nofail b"
apply (cases a, simp)
apply (cases b, simp_all)
done

lemma pw_inf_inres[refine_pw_simps]:
"inres (inf a b) x ⟷ inres a x ∧ inres b x"
apply (cases a, simp)
apply (cases b, simp)
apply (simp)
done

lemma pw_Inf_nofail[refine_pw_simps]: "nofail (Inf C) ⟷ (∃x∈C. nofail x)"
apply (cases "C={}")
apply simp
apply (cases "Inf C")
apply (subgoal_tac "C={FAIL}")
apply simp
apply auto []
apply (subgoal_tac "C≠{FAIL}")
apply (auto simp: not_nofail_iff) []
apply auto []
done

lemma pw_INF_nofail [refine_pw_simps]: "nofail (Inf (f  C)) ⟷ (∃x∈C. nofail (f x))"
using pw_Inf_nofail [of "f  C"] by simp

lemma pw_Inf_inres[refine_pw_simps]: "inres (Inf C) r ⟷ (∀M∈C. inres M r)"
apply (unfold Inf_nres_def)
apply auto
apply (case_tac M)
apply force
apply force
apply (case_tac M)
apply force
apply force
done

lemma pw_INF_inres [refine_pw_simps]: "inres (Inf (f  C)) r ⟷ (∀M∈C. inres (f M) r)"
using pw_Inf_inres [of "f  C"] by simp

lemma nofail_RES_conv: "nofail m ⟷ (∃M. m=RES M)" by (cases m) auto

primrec the_RES where "the_RES (RES X) = X"
lemma the_RES_inv[simp]: "nofail m ⟹ RES (the_RES m) = m"
by (cases m) auto

definition [refine_pw_simps]: "nf_inres m x ≡ nofail m ∧ inres m x"

lemma nf_inres_RES[simp]: "nf_inres (RES X) x ⟷ x∈X"

lemma nf_inres_SPEC[simp]: "nf_inres (SPEC Φ) x ⟷ Φ x"

lemma nofail_antimono_fun: "f ≤ g ⟹ (nofail (g x) ⟶ nofail (f x))"
by (auto simp: pw_le_iff dest: le_funD)

definition bind where "bind M f ≡ case M of
FAILi ⇒ FAIL |
RES X ⇒ Sup (fX)"

lemma bind_FAIL[simp]: "bind FAIL f = FAIL"
unfolding bind_def by (auto split: nres.split)

lemma bind_SUCCEED[simp]: "bind SUCCEED f = SUCCEED"
unfolding bind_def by (auto split: nres.split)

lemma bind_RES: "bind (RES X) f = Sup (fX)" unfolding bind_def
by (auto)

lemma pw_bind_nofail[refine_pw_simps]:
"nofail (bind M f) ⟷ (nofail M ∧ (∀x. inres M x ⟶ nofail (f x)))"
apply (cases M)
by (auto simp: bind_RES refine_pw_simps)

lemma pw_bind_inres[refine_pw_simps]:
"inres (bind M f) = (λx. nofail M ⟶ (∃y. (inres M y ∧ inres (f y) x)))"
apply (rule ext)
apply (cases M)
apply (auto simp add: bind_RES refine_pw_simps)
done

lemma pw_bind_le_iff:
"bind M f ≤ S ⟷ (nofail S ⟶ nofail M) ∧
(∀x. nofail M ∧ inres M x ⟶ f x ≤ S)"
by (auto simp: pw_le_iff refine_pw_simps)

lemma pw_bind_leI: "⟦
nofail S ⟹ nofail M; ⋀x. ⟦nofail M; inres M x⟧ ⟹ f x ≤ S⟧
⟹ bind M f ≤ S"

lemma nres_monad1[simp]: "bind (RETURN x) f = f x"
by (rule pw_eqI) (auto simp: refine_pw_simps)
lemma nres_monad2[simp]: "bind M RETURN = M"
by (rule pw_eqI) (auto simp: refine_pw_simps)
lemma nres_monad3[simp]: "bind (bind M f) g = bind M (λx. bind (f x) g)"
by (rule pw_eqI) (auto simp: refine_pw_simps)

text ‹\paragraph{Congruence rule for bind}›
lemma bind_cong:
assumes "m=m'"
assumes "⋀x. RETURN x ≤ m' ⟹ f x = f' x"
shows "bind m f = bind m' f'"
using assms
by (auto simp: refine_pw_simps pw_eq_iff pw_le_iff)

text ‹\paragraph{Monotonicity and Related Properties}›
lemma bind_mono[refine_mono]:
"⟦ M ≤ M'; ⋀x. RETURN x ≤ M ⟹ f x ≤ f' x ⟧ ⟹ bind M f ≤ bind M' f'"
(*"⟦ flat_le M M'; ⋀x. flat_le (f x) (f' x) ⟧ ⟹ flat_le (bind M f) (bind M' f')"*)
"⟦ flat_ge M M'; ⋀x. flat_ge (f x) (f' x) ⟧ ⟹ flat_ge (bind M f) (bind M' f')"
apply (auto simp: refine_pw_simps pw_ords_iff) []
apply (auto simp: refine_pw_simps pw_ords_iff) []
done

lemma bind_mono1[simp, intro!]: "mono (λM. bind M f)"
apply (rule monoI)
apply (rule bind_mono)
by auto

lemma bind_mono1'[simp, intro!]: "mono bind"
apply (rule monoI)
apply (rule le_funI)
apply (rule bind_mono)
by auto

lemma bind_mono2'[simp, intro!]: "mono (bind M)"
apply (rule monoI)
apply (rule bind_mono)
by (auto dest: le_funD)

lemma bind_distrib_sup1: "bind (sup M N) f = sup (bind M f) (bind N f)"
by (auto simp add: pw_eq_iff refine_pw_simps)

lemma  bind_distrib_sup2: "bind m (λx. sup (f x) (g x)) = sup (bind m f) (bind m g)"
by (auto simp: pw_eq_iff refine_pw_simps)

lemma bind_distrib_Sup1: "bind (Sup M) f = (SUP m∈M. bind m f)"
by (auto simp: pw_eq_iff refine_pw_simps)

lemma bind_distrib_Sup2: "F≠{} ⟹ bind m (Sup F) = (SUP f∈F. bind m f)"
by (auto simp: pw_eq_iff refine_pw_simps)

lemma RES_Sup_RETURN: "Sup (RETURNX) = RES X"
by (rule pw_eqI) (auto simp add: refine_pw_simps)

subsection ‹VCG Setup›

lemma SPEC_cons_rule:
assumes "m ≤ SPEC Φ"
assumes "⋀x. Φ x ⟹ Ψ x"
shows "m ≤ SPEC Ψ"
using assms by (auto simp: pw_le_iff)

lemmas SPEC_trans = order_trans[where z="SPEC Postcond" for Postcond, zero_var_indexes]

ML ‹
structure Refine = struct

structure vcg = Named_Thms
( val name = @{binding refine_vcg}
val description = "Refinement Framework: " ^
"Verification condition generation rules (intro)" )

structure vcg_cons = Named_Thms
( val name = @{binding refine_vcg_cons}
val description = "Refinement Framework: " ^
"Consequence rules tried by VCG" )

structure refine0 = Named_Thms
( val name = @{binding refine0}
val description = "Refinement Framework: " ^
"Refinement rules applied first (intro)" )

structure refine = Named_Thms
( val name = @{binding refine}
val description = "Refinement Framework: Refinement rules (intro)" )

structure refine2 = Named_Thms
( val name = @{binding refine2}
val description = "Refinement Framework: " ^
"Refinement rules 2nd stage (intro)" )

(* If set to true, the product splitter of refine_rcg is disabled. *)
val no_prod_split =
Attrib.setup_config_bool @{binding refine_no_prod_split} (K false);

let
val cons_thms = vcg_cons.get ctxt
val ref_thms = (refine0.get ctxt
@ add_thms @ refine.get ctxt @ refine2.get ctxt);
val prod_ss = (Splitter.add_split @{thm prod.split}
(put_simpset HOL_basic_ss ctxt));
val prod_simp_tac =
if Config.get ctxt no_prod_split then
K no_tac
else
(simp_tac prod_ss THEN'
REPEAT_ALL_NEW (resolve_tac ctxt @{thms impI allI}));
in
REPEAT_ALL_NEW_FWD (DETERM o FIRST' [
resolve_tac ctxt ref_thms,
resolve_tac ctxt cons_thms THEN' resolve_tac ctxt ref_thms,
prod_simp_tac
])
end;

fun post_tac ctxt = REPEAT_ALL_NEW_FWD (FIRST' [
eq_assume_tac,
(*match_tac ctxt thms,*)
SOLVED' (Tagged_Solver.solve_tac ctxt)])

end;
›
setup ‹Refine.vcg.setup›
setup ‹Refine.vcg_cons.setup›
setup ‹Refine.refine0.setup›
setup ‹Refine.refine.setup›
setup ‹Refine.refine2.setup›
(*setup {* Refine.refine_post.setup *}*)

method_setup refine_rcg =
‹Attrib.thms >> (fn add_thms => fn ctxt => SIMPLE_METHOD' (
Refine.rcg_tac add_thms ctxt THEN_ALL_NEW_FWD (TRY o Refine.post_tac ctxt)
))›
"Refinement framework: Generate refinement conditions"

method_setup refine_vcg =
‹Attrib.thms >> (fn add_thms => fn ctxt => SIMPLE_METHOD' (
Refine.rcg_tac (add_thms @ Refine.vcg.get ctxt) ctxt THEN_ALL_NEW_FWD (TRY o Refine.post_tac ctxt)
))›
"Refinement framework: Generate refinement and verification conditions"

method_setup refine_post =
{* Scan.succeed (fn ctxt => SIMPLE_METHOD' (
Refine.post_tac ctxt
)) *}
"Refinement framework: Postprocessing of refinement goals"
*)

declare SPEC_cons_rule[refine_vcg_cons]

subsection ‹Data Refinement›
text ‹
In this section we establish a notion of pointwise data refinement, by
lifting a relation ‹R› between concrete and abstract values to
our result lattice.

Given a relation ‹R›, we define a {\em concretization function}
‹⇓R› that takes an abstract result, and returns a concrete result.
The concrete result contains all values that are mapped by ‹R› to
a value in the abstract result.

Note that our concretization function forms no Galois connection, i.e.,
in general there is no ‹α› such that
‹m ≤⇓ R m'› is equivalent to ‹α m ≤ m'›.
However, we get a Galois connection for the special case of
single-valued relations.

Regarding data refinement as Galois connections is inspired by \cite{mmo97},
that also uses the adjuncts of
a Galois connection to express data refinement by program refinement.
›

definition conc_fun ("⇓") where
"conc_fun R m ≡ case m of FAILi ⇒ FAIL | RES X ⇒ RES (R¯X)"

definition abs_fun ("⇑") where
"abs_fun R m ≡ case m of FAILi ⇒ FAIL
| RES X ⇒ if X⊆Domain R then RES (RX) else FAIL"

lemma
conc_fun_FAIL[simp]: "⇓R FAIL = FAIL" and
conc_fun_RES: "⇓R (RES X) = RES (R¯X)"
unfolding conc_fun_def by (auto split: nres.split)

lemma abs_fun_simps[simp]:
"⇑R FAIL = FAIL"
"X⊆Domain R ⟹ ⇑R (RES X) = RES (RX)"
"¬(X⊆Domain R) ⟹ ⇑R (RES X) = FAIL"
unfolding abs_fun_def by (auto split: nres.split)

context fixes R assumes SV: "single_valued R" begin
lemma conc_abs_swap: "m' ≤ ⇓R m ⟷ ⇑R m' ≤ m"
unfolding conc_fun_def abs_fun_def using SV
by (auto split: nres.split)
(metis ImageE converseD single_valuedD subsetD)

lemma ac_galois: "galois_connection (⇑R) (⇓R)"
apply (unfold_locales)
by (rule conc_abs_swap)

end

lemma pw_abs_nofail[refine_pw_simps]:
"nofail (⇑R M) ⟷ (nofail M ∧ (∀x. inres M x ⟶ x∈Domain R))"
apply (cases M)
apply simp
apply (auto simp: abs_fun_simps abs_fun_def)
done

lemma pw_abs_inres[refine_pw_simps]:
"inres (⇑R M) a ⟷ (nofail (⇑R M) ⟶ (∃c. inres M c ∧ (c,a)∈R))"
apply (cases M)
apply simp
apply (auto simp: abs_fun_def)
done

lemma pw_conc_nofail[refine_pw_simps]:
"nofail (⇓R S) = nofail S"
by (cases S) (auto simp: conc_fun_RES)

lemma pw_conc_inres[refine_pw_simps]:
"inres (⇓R S') = (λs. nofail S'
⟶ (∃s'. (s,s')∈R ∧ inres S' s'))"
apply (rule ext)
apply (cases S')
apply (auto simp: conc_fun_RES)
done

lemma abs_fun_strict[simp]:
"⇑ R SUCCEED = SUCCEED"
unfolding abs_fun_def by (auto split: nres.split)

lemma conc_fun_strict[simp]:
"⇓ R SUCCEED = SUCCEED"
unfolding conc_fun_def by (auto split: nres.split)

lemma conc_fun_mono[simp, intro!]: "mono (⇓R)"
by rule (auto simp: pw_le_iff refine_pw_simps)

lemma abs_fun_mono[simp, intro!]: "mono (⇑R)"
by rule (auto simp: pw_le_iff refine_pw_simps)

lemma conc_fun_R_mono:
assumes "R ⊆ R'"
shows "⇓R M ≤ ⇓R' M"
using assms
by (auto simp: pw_le_iff refine_pw_simps)

lemma conc_fun_chain: "⇓R (⇓S M) = ⇓(R O S) M"
unfolding conc_fun_def
by (auto split: nres.split)

lemma conc_Id[simp]: "⇓Id = id"
unfolding conc_fun_def [abs_def] by (auto split: nres.split)

lemma abs_Id[simp]: "⇑Id = id"
unfolding abs_fun_def [abs_def] by (auto split: nres.split)

lemma conc_fun_fail_iff[simp]:
"⇓R S = FAIL ⟷ S=FAIL"
"FAIL = ⇓R S ⟷ S=FAIL"
by (auto simp add: pw_eq_iff refine_pw_simps)

lemma conc_trans[trans]:
assumes A: "C ≤ ⇓R B" and B: "B ≤ ⇓R' A"
shows "C ≤ ⇓R (⇓R' A)"
using assms by (fastforce simp: pw_le_iff refine_pw_simps)

lemma abs_trans[trans]:
assumes A: "⇑R C ≤ B" and B: "⇑R' B ≤ A"
shows "⇑R' (⇑R C) ≤ A"
using assms by (fastforce simp: pw_le_iff refine_pw_simps)

subsubsection ‹Transitivity Reasoner Setup›

text ‹WARNING: The order of the single statements is important here!›
"⋀A B C. A≤⇓R  B ⟹ B≤    C ⟹ A≤⇓R  C"
"⋀A B C. A≤⇓Id B ⟹ B≤⇓R  C ⟹ A≤⇓R  C"
"⋀A B C. A≤⇓R  B ⟹ B≤⇓Id C ⟹ A≤⇓R  C"

"⋀A B C. A≤⇓Id B ⟹ B≤⇓Id C ⟹ A≤    C"
"⋀A B C. A≤⇓Id B ⟹ B≤    C ⟹ A≤    C"
"⋀A B C. A≤    B ⟹ B≤⇓Id C ⟹ A≤    C"
using conc_trans[where R=R and R'=Id]
by (auto intro: order_trans)

text ‹WARNING: The order of the single statements is important here!›
"⋀A B C. ⟦ A ≤ B; ⇑ R B ≤ C⟧ ⟹ ⇑ R A ≤ C"
"⋀A B C. ⟦⇑ Id A ≤ B; ⇑ R B ≤ C⟧ ⟹ ⇑ R A ≤ C"
"⋀A B C. ⟦⇑ R A ≤ B; ⇑ Id B ≤ C⟧ ⟹ ⇑ R A ≤ C"

"⋀A B C. ⟦⇑ Id A ≤ B; ⇑ Id B ≤ C⟧ ⟹ A ≤ C"
"⋀A B C. ⟦⇑ Id A ≤ B; B ≤ C⟧ ⟹ A ≤ C"
"⋀A B C. ⟦A ≤ B; ⇑ Id B ≤ C⟧ ⟹ A ≤ C"

apply (auto simp: refine_pw_simps pw_le_iff)
apply fastforce+
done

subsection ‹Derived Program Constructs›
text ‹
In this section, we introduce some programming constructs that are derived
›
subsubsection ‹ASSUME and ASSERT›

definition ASSERT where "ASSERT ≡ iASSERT RETURN"
definition ASSUME where "ASSUME ≡ iASSUME RETURN"
interpretation assert?: generic_Assert bind RETURN ASSERT ASSUME
apply unfold_locales

text ‹Order matters! ›
lemmas [refine_vcg] = ASSERT_leI
lemmas [refine_vcg] = le_ASSUMEI
lemmas [refine_vcg] = le_ASSERTI
lemmas [refine_vcg] = ASSUME_leI

lemma pw_ASSERT[refine_pw_simps]:
"nofail (ASSERT Φ) ⟷ Φ"
"inres (ASSERT Φ) x"
by (cases Φ, simp_all)+

lemma pw_ASSUME[refine_pw_simps]:
"nofail (ASSUME Φ)"
"inres (ASSUME Φ) x ⟷ Φ"
by (cases Φ, simp_all)+

subsubsection ‹Recursion›
lemma pw_REC_nofail:
shows "nofail (REC B x) ⟷ trimono B ∧
(∃F. (∀x.
nofail (F x) ⟶ nofail (B F x)
∧ (∀x'. inres (B F x) x' ⟶ inres (F x) x')
) ∧ nofail (F x))"
proof -
have "nofail (REC B x) ⟷ trimono B ∧
(∃F. (∀x. B F x ≤ F x) ∧ nofail (F x))"
unfolding REC_def lfp_def
apply (auto simp: refine_pw_simps intro: le_funI dest: le_funD)
done
thus ?thesis
unfolding pw_le_iff .
qed

lemma pw_REC_inres:
"inres (REC B x) x' = (trimono B ⟶
(∀F. (∀x''.
nofail (F x'') ⟶ nofail (B F x'')
∧ (∀x. inres (B F x'') x ⟶ inres (F x'') x))
⟶ inres (F x) x'))"
proof -
have "inres (REC B x) x'
⟷ (trimono B ⟶ (∀F. (∀x''. B F x'' ≤ F x'') ⟶ inres (F x) x'))"
unfolding REC_def lfp_def
by (auto simp: refine_pw_simps intro: le_funI dest: le_funD)
thus ?thesis unfolding pw_le_iff .
qed

lemmas pw_REC = pw_REC_inres pw_REC_nofail

lemma pw_RECT_nofail:
shows "nofail (RECT B x) ⟷ trimono B ∧
(∀F. (∀y. nofail (B F y) ⟶
nofail (F y) ∧ (∀x. inres (F y) x ⟶ inres (B F y) x)) ⟶
nofail (F x))"
proof -
have "nofail (RECT B x) ⟷ (trimono B ∧ (∀F. (∀y. F y ≤ B F y) ⟶ nofail (F x)))"
unfolding RECT_gfp_def gfp_def
by (auto simp: refine_pw_simps intro: le_funI dest: le_funD)
thus ?thesis
unfolding pw_le_iff .
qed

lemma pw_RECT_inres:
shows "inres (RECT B x) x' = (trimono B ⟶
(∃M. (∀y. nofail (B M y) ⟶
nofail (M y) ∧ (∀x. inres (M y) x ⟶ inres (B M y) x)) ∧
inres (M x) x'))"
proof -
have "inres (RECT B x) x' ⟷ trimono B ⟶ (∃M. (∀y. M y ≤ B M y) ∧ inres (M x) x')"
unfolding RECT_gfp_def gfp_def
by (auto simp: refine_pw_simps intro: le_funI dest: le_funD)
thus ?thesis unfolding pw_le_iff .
qed

lemmas pw_RECT = pw_RECT_inres pw_RECT_nofail

subsection ‹Proof Rules›

subsubsection ‹Proving Correctness›
text ‹
In this section, we establish Hoare-like rules to prove that a program
meets its specification.
›
lemma le_SPEC_UNIV_rule [refine_vcg]:
"m ≤ SPEC (λ_. True) ⟹ m ≤ RES UNIV" by auto

lemma RETURN_rule[refine_vcg]: "Φ x ⟹ RETURN x ≤ SPEC Φ"
by (auto simp: RETURN_def)
lemma RES_rule[refine_vcg]: "⟦⋀x. x∈S ⟹ Φ x⟧ ⟹ RES S ≤ SPEC Φ"
by auto
lemma SUCCEED_rule[refine_vcg]: "SUCCEED ≤ SPEC Φ" by auto
lemma FAIL_rule: "False ⟹ FAIL ≤ SPEC Φ" by auto
lemma SPEC_rule[refine_vcg]: "⟦⋀x. Φ x ⟹ Φ' x⟧ ⟹ SPEC Φ ≤ SPEC Φ'" by auto

lemma RETURN_to_SPEC_rule[refine_vcg]: "m≤SPEC ((=) v) ⟹ m≤RETURN v"

lemma Sup_img_rule_complete:
"(∀x. x∈S ⟶ f x ≤ SPEC Φ) ⟷ Sup (fS) ≤ SPEC Φ"
apply rule
apply (rule pw_leI)
apply (auto simp: pw_le_iff refine_pw_simps) []
apply (intro allI impI)
apply (rule pw_leI)
apply (auto simp: pw_le_iff refine_pw_simps) []
done

lemma SUP_img_rule_complete:
"(∀x. x∈S ⟶ f x ≤ SPEC Φ) ⟷ Sup (f  S) ≤ SPEC Φ"
using Sup_img_rule_complete [of S f] by simp

lemma Sup_img_rule[refine_vcg]:
"⟦ ⋀x. x∈S ⟹ f x ≤ SPEC Φ ⟧ ⟹ Sup(fS) ≤ SPEC Φ"
by (auto simp: SUP_img_rule_complete[symmetric])

text ‹This lemma is just to demonstrate that our rule is complete.›
lemma bind_rule_complete: "bind M f ≤ SPEC Φ ⟷ M ≤ SPEC (λx. f x ≤ SPEC Φ)"
by (auto simp: pw_le_iff refine_pw_simps)
lemma bind_rule[refine_vcg]:
"⟦ M ≤ SPEC (λx. f x ≤ SPEC Φ) ⟧ ⟹ bind M (λx. f x) ≤ SPEC Φ"
― ‹Note: @{text "η"}-expanded version helps Isabelle's unification to keep meaningful
variable names from the program›
by (auto simp: bind_rule_complete)

lemma ASSUME_rule[refine_vcg]: "⟦Φ ⟹ Ψ ()⟧ ⟹ ASSUME Φ ≤ SPEC Ψ"
by (cases Φ) auto

lemma ASSERT_rule[refine_vcg]: "⟦Φ; Φ ⟹ Ψ ()⟧ ⟹ ASSERT Φ ≤ SPEC Ψ" by auto

lemma prod_rule[refine_vcg]:
"⟦⋀a b. p=(a,b) ⟹ S a b ≤ SPEC Φ⟧ ⟹ case_prod S p ≤ SPEC Φ"
by (auto split: prod.split)

(* TODO: Add a simplifier setup that normalizes nested case-expressions to
the vcg! *)
lemma prod2_rule[refine_vcg]:
assumes "⋀a b c d. ⟦ab=(a,b); cd=(c,d)⟧ ⟹ f a b c d ≤ SPEC Φ"
shows "(λ(a,b) (c,d). f a b c d) ab cd ≤ SPEC Φ"
using assms
by (auto split: prod.split)

lemma if_rule[refine_vcg]:
"⟦ b ⟹ S1 ≤ SPEC Φ; ¬b ⟹ S2 ≤ SPEC Φ⟧
⟹ (if b then S1 else S2) ≤ SPEC Φ"
by (auto)

lemma option_rule[refine_vcg]:
"⟦ v=None ⟹ S1 ≤ SPEC Φ; ⋀x. v=Some x ⟹ f2 x ≤ SPEC Φ⟧
⟹ case_option S1 f2 v ≤ SPEC Φ"
by (auto split: option.split)

lemma Let_rule[refine_vcg]:
"f x ≤ SPEC Φ ⟹ Let x f ≤ SPEC Φ" by auto

lemma Let_rule':
assumes "⋀x. x=v ⟹ f x ≤ SPEC Φ"
shows "Let v (λx. f x) ≤ SPEC Φ"
using assms by simp

text {* The following lemma shows that greatest and least fixed point are equal,
if we can provide a variant. *}
thm RECT_eq_REC
lemma RECT_eq_REC_old:
assumes WF: "wf V"
assumes I0: "I x"
assumes IS: "⋀f x. I x ⟹
body (λx'. do { ASSERT (I x' ∧ (x',x)∈V); f x'}) x ≤ body f x"
shows "REC⇩T body x = REC body x"
apply (rule RECT_eq_REC)
apply (rule WF)
apply (rule I0)
apply (rule order_trans[OF _ IS])
apply (subgoal_tac "(λx'. if I x' ∧ (x', x) ∈ V then f x' else FAIL) =
(λx'. ASSERT (I x' ∧ (x', x) ∈ V) ⤜ (λ_. f x'))")
apply simp
apply (rule ext)
apply (rule pw_eqI)
done
*)

(* TODO: Also require RECT_le_rule. Derive RECT_invisible_refine from that. *)
lemma REC_le_rule:
assumes M: "trimono body"
assumes I0: "(x,x')∈R"
assumes IS: "⋀f x x'. ⟦ ⋀x x'. (x,x')∈R ⟹ f x ≤ M x'; (x,x')∈R ⟧
⟹ body f x ≤ M x'"
shows "REC body x ≤ M x'"
by (rule REC_rule_arb[OF M, where pre="λx' x. (x,x')∈R", OF I0 IS])

(* TODO: Invariant annotations and vcg-rule
Possibility 1: Semantically alter the program, such that it fails if the
invariant does not hold
Possibility 2: Only syntactically annotate the invariant, as hint for the VCG.
*)

subsubsection ‹Proving Monotonicity›

lemma nr_mono_bind:
assumes MA: "mono A" and MB: "⋀s. mono (B s)"
shows "mono (λF s. bind (A F s) (λs'. B s F s'))"
apply (rule monoI)
apply (rule le_funI)
apply (rule bind_mono)
apply (auto dest: monoD[OF MA, THEN le_funD]) []
apply (auto dest: monoD[OF MB, THEN le_funD]) []
done

lemma nr_mono_bind': "mono (λF s. bind (f s) F)"
apply rule
apply (rule le_funI)
apply (rule bind_mono)
apply (auto dest: le_funD)
done

lemmas nr_mono = nr_mono_bind nr_mono_bind' mono_const mono_if mono_id

subsubsection ‹Proving Refinement›
text ‹In this subsection, we establish rules to prove refinement between
structurally similar programs. All rules are formulated including a possible
data refinement via a refinement relation. If this is not required, the
refinement relation can be chosen to be the identity relation.
›

text ‹If we have two identical programs, this rule solves the refinement goal
immediately, using the identity refinement relation.›
lemma Id_refine[refine0]: "S ≤ ⇓Id S" by auto

lemma RES_refine:
"⟦ ⋀s. s∈S ⟹ ∃s'∈S'. (s,s')∈R⟧ ⟹ RES S ≤ ⇓R (RES S')"
by (auto simp: conc_fun_RES)

lemma SPEC_refine:
assumes "S ≤ SPEC (λx. ∃x'. (x,x')∈R ∧ Φ x')"
shows "S ≤ ⇓R (SPEC Φ)"
using assms
by (force simp: pw_le_iff refine_pw_simps)

(* TODO/FIXME: This is already part of a type-based heuristics! *)
lemma Id_SPEC_refine[refine]:
"S ≤ SPEC Φ ⟹ S ≤ ⇓Id (SPEC Φ)" by simp

lemma RETURN_refine[refine]:
assumes "(x,x')∈R"
shows "RETURN x ≤ ⇓R (RETURN x')"
using assms
by (auto simp: RETURN_def conc_fun_RES)

lemma RETURN_SPEC_refine:
assumes "∃x'. (x,x')∈R ∧ Φ x'"
shows "RETURN x ≤ ⇓R (SPEC Φ)"
using assms
by (auto simp: pw_le_iff refine_pw_simps)

lemma FAIL_refine[refine]: "X ≤ ⇓R FAIL" by auto
lemma SUCCEED_refine[refine]: "SUCCEED ≤ ⇓R X'" by auto

lemma sup_refine[refine]:
assumes "ai ≤⇓R a"
assumes "bi ≤⇓R b"
shows "sup ai bi ≤⇓R (sup a b)"
using assms by (auto simp: pw_le_iff refine_pw_simps)

text ‹The next two rules are incomplete, but a good approximation for refining
structurally similar programs.›
lemma bind_refine':
fixes R' :: "('a×'b) set" and R::"('c×'d) set"
assumes R1: "M ≤ ⇓ R' M'"
assumes R2: "⋀x x'. ⟦ (x,x')∈R'; inres M x; inres M' x';
nofail M; nofail M'
⟧ ⟹ f x ≤ ⇓ R (f' x')"
shows "bind M (λx. f x) ≤ ⇓ R (bind M' (λx'. f' x'))"
using assms
apply fast
done

lemma bind_refine[refine]:
fixes R' :: "('a×'b) set" and R::"('c×'d) set"
assumes R1: "M ≤ ⇓ R' M'"
assumes R2: "⋀x x'. ⟦ (x,x')∈R' ⟧
⟹ f x ≤ ⇓ R (f' x')"
shows "bind M (λx. f x) ≤ ⇓ R (bind M' (λx'. f' x'))"
apply (rule bind_refine') using assms by auto

lemma bind_refine_abs': (* Only keep nf_inres-information for abstract *)
fixes R' :: "('a×'b) set" and R::"('c×'d) set"
assumes R1: "M ≤ ⇓ R' M'"
assumes R2: "⋀x x'. ⟦ (x,x')∈R'; nf_inres M' x'
⟧ ⟹ f x ≤ ⇓ R (f' x')"
shows "bind M (λx. f x) ≤ ⇓ R (bind M' (λx'. f' x'))"
using assms
apply blast
done

text ‹Special cases for refinement of binding to ‹RES›
statements›
lemma bind_refine_RES:
"⟦RES X ≤ ⇓ R' M';
⋀x x'. ⟦(x, x') ∈ R'; x ∈ X ⟧ ⟹ f x ≤ ⇓ R (f' x')⟧
⟹ RES X ⤜ (λx. f x) ≤ ⇓ R (M' ⤜ (λx'. f' x'))"

"⟦M ≤ ⇓ R' (RES X');
⋀x x'. ⟦(x, x') ∈ R'; x' ∈ X' ⟧ ⟹ f x ≤ ⇓ R (f' x')⟧
⟹ M ⤜ (λx. f x) ≤ ⇓ R (RES X' ⤜ (λx'. f' x'))"

"⟦RES X ≤ ⇓ R' (RES X');
⋀x x'. ⟦(x, x') ∈ R'; x ∈ X; x' ∈ X'⟧ ⟹ f x ≤ ⇓ R (f' x')⟧
⟹ RES X ⤜ (λx. f x) ≤ ⇓ R (RES X' ⤜ (λx'. f' x'))"
by (auto intro!: bind_refine')

declare bind_refine_RES(1,2)[refine]
declare bind_refine_RES(3)[refine]

lemma ASSERT_refine[refine]:
"⟦ Φ'⟹Φ ⟧ ⟹ ASSERT Φ ≤ ⇓Id (ASSERT Φ')"
by (cases Φ') auto

lemma ASSUME_refine[refine]:
"⟦ Φ ⟹ Φ' ⟧ ⟹ ASSUME Φ ≤ ⇓Id (ASSUME Φ')"
by (cases Φ) auto

text ‹
Assertions and assumptions are treated specially in bindings
›
lemma ASSERT_refine_right:
assumes "Φ ⟹ S ≤⇓R S'"
shows "S ≤⇓R (do {ASSERT Φ; S'})"
using assms by (cases Φ) auto
lemma ASSERT_refine_right_pres:
assumes "Φ ⟹ S ≤⇓R (do {ASSERT Φ; S'})"
shows "S ≤⇓R (do {ASSERT Φ; S'})"
using assms by (cases Φ) auto

lemma ASSERT_refine_left:
assumes "Φ"
assumes "Φ ⟹ S ≤ ⇓R S'"
shows "do{ASSERT Φ; S} ≤ ⇓R S'"
using assms by (cases Φ) auto

lemma ASSUME_refine_right:
assumes "Φ"
assumes "Φ ⟹ S ≤⇓R S'"
shows "S ≤⇓R (do {ASSUME Φ; S'})"
using assms by (cases Φ) auto

lemma ASSUME_refine_left:
assumes "Φ ⟹ S ≤ ⇓R S'"
shows "do {ASSUME Φ; S} ≤ ⇓R S'"
using assms by (cases Φ) auto

lemma ASSUME_refine_left_pres:
assumes "Φ ⟹ do {ASSUME Φ; S} ≤ ⇓R S'"
shows "do {ASSUME Φ; S} ≤ ⇓R S'"
using assms by (cases Φ) auto

text ‹Warning: The order of ‹[refine]›-declarations is
important here, as preconditions should be generated before
lemmas [refine0] = ASSUME_refine_right
lemmas [refine0] = ASSERT_refine_left
lemmas [refine0] = ASSUME_refine_left
lemmas [refine0] = ASSERT_refine_right

text ‹For backward compatibility, as ‹intro refine› still
seems to be used instead of ‹refine_rcg›.›
lemmas [refine] = ASSUME_refine_right
lemmas [refine] = ASSERT_refine_left
lemmas [refine] = ASSUME_refine_left
lemmas [refine] = ASSERT_refine_right

definition lift_assn :: "('a × 'b) set ⇒ ('b ⇒ bool) ⇒ ('a ⇒ bool)"
― ‹Lift assertion over refinement relation›
where "lift_assn R Φ s ≡ ∃s'. (s,s')∈R ∧ Φ s'"
lemma lift_assnI: "⟦(s,s')∈R; Φ s'⟧ ⟹ lift_assn R Φ s"
unfolding lift_assn_def by auto

lemma REC_refine[refine]:
assumes M: "trimono body"
assumes R0: "(x,x')∈R"
assumes RS: "⋀f f' x x'. ⟦ ⋀x x'. (x,x')∈R ⟹ f x ≤⇓S (f' x'); (x,x')∈R;
REC body' = f' ⟧
⟹ body f x ≤⇓S (body' f' x')"
shows "REC (λf x. body f x) x ≤⇓S (REC (λf' x'. body' f' x') x')"
unfolding REC_def
apply (rule lfp_induct_pointwise[where pre="λx' x. (x,x')∈R" and B=body])

apply rule
apply clarsimp
apply (blast intro: SUP_least)

apply simp

apply (rule R0)

apply (subst lfp_unfold, simp add: trimonoD)
apply (rule RS)
apply blast
apply blast
done

lemma RECT_refine[refine]:
assumes M: "trimono body"
assumes R0: "(x,x')∈R"
assumes RS: "⋀f f' x x'. ⟦ ⋀x x'. (x,x')∈R ⟹ f x ≤⇓S (f' x'); (x,x')∈R ⟧
⟹ body f x ≤⇓S (body' f' x')"
shows "RECT (λf x. body f x) x ≤⇓S (RECT (λf' x'. body' f' x') x')"
unfolding RECT_def

apply (rule flatf_fixp_transfer[where
fp'="flatf_gfp body"
and B'=body
and P="λx x'. (x',x)∈R",
OF _ _ flatf_ord.fixp_unfold[OF M[THEN trimonoD_flatf_ge]] R0])
apply simp
by (rule RS)

lemma if_refine[refine]:
assumes "b ⟷ b'"
assumes "⟦b;b'⟧ ⟹ S1 ≤ ⇓R S1'"
assumes "⟦¬b;¬b'⟧ ⟹ S2 ≤ ⇓R S2'"
shows "(if b then S1 else S2) ≤ ⇓R (if b' then S1' else S2')"
using assms by auto

lemma Let_unfold_refine[refine]:
assumes "f x ≤ ⇓R (f' x')"
shows "Let x f ≤ ⇓R (Let x' f')"
using assms by auto

text ‹The next lemma is sometimes more convenient, as it prevents
large let-expressions from exploding by being completely unfolded.›
lemma Let_refine:
assumes "(m,m')∈R'"
assumes "⋀x x'. (x,x')∈R' ⟹ f x ≤ ⇓R (f' x')"
shows "Let m (λx. f x) ≤⇓R (Let m' (λx'. f' x'))"
using assms by auto

lemma Let_refine':
assumes "(m,m')∈R"
assumes "(m,m')∈R ⟹ f m ≤⇓S (f' m')"
shows "Let m f ≤ ⇓S (Let m' f')"
using assms by simp

lemma case_option_refine[refine]:
assumes "(v,v')∈⟨Ra⟩option_rel"
assumes "⟦v=None; v'=None⟧ ⟹ n ≤ ⇓ Rb n'"
assumes "⋀x x'. ⟦ v=Some x; v'=Some x'; (x, x') ∈ Ra ⟧
⟹ f x ≤ ⇓ Rb (f' x')"
shows "case_option n f v ≤⇓Rb (case_option n' f' v')"
using assms
by (auto split: option.split simp: option_rel_def)

lemma list_case_refine[refine]:
assumes "(li,l)∈⟨S⟩list_rel"
assumes "fni ≤⇓R fn"
assumes "⋀xi x xsi xs. ⟦ (xi,x)∈S; (xsi,xs)∈⟨S⟩list_rel; li=xi#xsi; l=x#xs ⟧ ⟹ fci xi xsi ≤⇓R (fc x xs)"
shows "(case li of [] ⇒ fni | xi#xsi ⇒ fci xi xsi) ≤ ⇓R (case l of [] ⇒ fn | x#xs ⇒ fc x xs)"
using assms by (auto split: list.split)

text ‹It is safe to split conjunctions in refinement goals.›
declare conjI[refine]

text ‹The following rules try to compensate for some structural changes,
like inlining lets or converting binds to lets.›
lemma remove_Let_refine[refine2]:
assumes "M ≤ ⇓R (f x)"
shows "M ≤ ⇓R (Let x f)" using assms by auto

lemma intro_Let_refine[refine2]:
assumes "f x ≤ ⇓R M'"
shows "Let x f ≤ ⇓R M'" using assms by auto

lemma bind2let_refine[refine2]:
assumes "RETURN x ≤ ⇓R' M'"
assumes "⋀x'. (x,x')∈R' ⟹ f x ≤ ⇓R (f' x')"
shows "Let x f ≤ ⇓R (bind M' (λx'. f' x'))"
using assms
apply fast
done

lemma bind_Let_refine2[refine2]: "⟦
m' ≤⇓R' (RETURN x);
⋀x'. ⟦inres m' x'; (x',x)∈R'⟧ ⟹ f' x' ≤ ⇓R (f x)
⟧ ⟹ m'⤜(λx'. f' x') ≤ ⇓R (Let x (λx. f x))"
apply blast
done

lemma bind2letRETURN_refine[refine2]:
assumes "RETURN x ≤ ⇓R' M'"
assumes "⋀x'. (x,x')∈R' ⟹ RETURN (f x) ≤ ⇓R (f' x')"
shows "RETURN (Let x f) ≤ ⇓R (bind M' (λx'. f' x'))"
using assms
apply fast
done

lemma RETURN_as_SPEC_refine[refine2]:
assumes "M ≤ SPEC (λc. (c,a)∈R)"
shows "M ≤ ⇓R (RETURN a)"
using assms

lemma RETURN_as_SPEC_refine_old:
"⋀M R. M ≤ ⇓R (SPEC (λx. x=v)) ⟹ M ≤⇓R (RETURN v)"

lemma if_RETURN_refine [refine2]:
assumes "b ⟷ b'"
assumes "⟦b;b'⟧ ⟹ RETURN S1 ≤ ⇓R S1'"
assumes "⟦¬b;¬b'⟧ ⟹ RETURN S2 ≤ ⇓R S2'"
shows "RETURN (if b then S1 else S2) ≤ ⇓R (if b' then S1' else S2')"
(* this is nice to have for small functions, hence keep it in refine2 *)
using assms

lemma RES_sng_as_SPEC_refine[refine2]:
assumes "M ≤ SPEC (λc. (c,a)∈R)"
shows "M ≤ ⇓R (RES {a})"
using assms

lemma intro_spec_refine_iff:
"(bind (RES X) f ≤ ⇓R M) ⟷ (∀x∈X. f x ≤ ⇓R M)"
apply blast
done

lemma intro_spec_refine[refine2]:
assumes "⋀x. x∈X ⟹ f x ≤ ⇓R M"
shows "bind (RES X) (λx. f x) ≤ ⇓R M"
using assms

text ‹The following rules are intended for manual application, to reflect
some common structural changes, that, however, are not suited to be applied
automatically.›

text ‹Replacing a let by a deterministic computation›
lemma let2bind_refine:
assumes "m ≤ ⇓R' (RETURN m')"
assumes "⋀x x'. (x,x')∈R' ⟹ f x ≤ ⇓R (f' x')"
shows "bind m (λx. f x) ≤ ⇓R (Let m' (λx'. f' x'))"
using assms
apply blast
done

text ‹Introduce a new binding, without a structural match in the abstract
program›
lemma intro_bind_refine:
assumes "m ≤ ⇓R' (RETURN m')"
assumes "⋀x. (x,m')∈R' ⟹ f x ≤ ⇓R m''"
shows "bind m (λx. f x) ≤ ⇓R m''"
using assms
apply blast
done

lemma intro_bind_refine_id:
assumes "m ≤ (SPEC ((=) m'))"
assumes "f m' ≤ ⇓R m''"
shows "bind m f ≤ ⇓R m''"
using assms
apply blast
done

text ‹The following set of rules executes a step on the LHS or RHS of
a refinement proof obligation, without changing the other side.
These kind of rules is useful for performing refinements with
invisible steps.›
lemma lhs_step_If:
"⟦ b ⟹ t ≤ m; ¬b ⟹ e ≤ m ⟧ ⟹ If b t e ≤ m" by simp

lemma lhs_step_RES:
"⟦ ⋀x. x∈X ⟹ RETURN x ≤ m  ⟧ ⟹ RES X ≤ m"

lemma lhs_step_SPEC:
"⟦ ⋀x. Φ x ⟹ RETURN x ≤ m ⟧ ⟹ SPEC (λx. Φ x) ≤ m"

lemma lhs_step_bind:
fixes m :: "'a nres" and f :: "'a ⇒ 'b nres"
assumes "nofail m' ⟹ nofail m"
assumes "⋀x. nf_inres m x ⟹ f x ≤ m'"
shows "do {x←m; f x} ≤ m'"
using assms
by (simp add: pw_le_iff refine_pw_simps) blast

lemma rhs_step_bind:
assumes "m ≤ ⇓R m'" "inres m x" "⋀x'. (x,x')∈R ⟹ lhs ≤⇓S (f' x')"
shows "lhs ≤ ⇓S (m' ⤜ f')"
using assms
by (simp add: pw_le_iff refine_pw_simps) blast

lemma rhs_step_bind_RES:
assumes "x'∈X'"
assumes "m ≤ ⇓R (f' x')"
shows "m ≤ ⇓R (RES X' ⤜ f')"
using assms by (simp add: pw_le_iff refine_pw_simps) blast

lemma rhs_step_bind_SPEC:
assumes "Φ x'"
assumes "m ≤ ⇓R (f' x')"
shows "m ≤ ⇓R (SPEC Φ ⤜ f')"
using assms by (simp add: pw_le_iff refine_pw_simps) blast

lemma RES_bind_choose:
assumes "x∈X"
assumes "m ≤ f x"
shows "m ≤ RES X ⤜ f"
using assms by (auto simp: pw_le_iff refine_pw_simps)

lemma pw_RES_bind_choose:
"nofail (RES X ⤜ f) ⟷ (∀x∈X. nofail (f x))"
"inres (RES X ⤜ f) y ⟷ (∃x∈X. inres (f x) y)"
by (auto simp: refine_pw_simps)

lemma prod_case_refine:
assumes "(p',p)∈R1×⇩rR2"
assumes "⋀x1' x2' x1 x2. ⟦ p'=(x1',x2'); p=(x1,x2); (x1',x1)∈R1; (x2',x2)∈R2⟧ ⟹ f' x1' x2' ≤ ⇓R (f x1 x2)"
shows "(case p' of (x1',x2') ⇒ f' x1' x2') ≤⇓R (case p of (x1,x2) ⇒ f x1 x2)"
using assms by (auto split: prod.split)

subsection ‹Relators›
declare fun_relI[refine]

definition nres_rel where
nres_rel_def_internal: "nres_rel R ≡ {(c,a). c ≤ ⇓R a}"

lemma nres_rel_def: "⟨R⟩nres_rel ≡ {(c,a). c ≤ ⇓R a}"

lemma nres_relD: "(c,a)∈⟨R⟩nres_rel ⟹ c ≤⇓R a" by (simp add: nres_rel_def)
lemma nres_relI[refine]: "c ≤⇓R a ⟹ (c,a)∈⟨R⟩nres_rel" by (simp add: nres_rel_def)

lemma nres_rel_comp: "⟨A⟩nres_rel O ⟨B⟩nres_rel = ⟨A O B⟩nres_rel"
by (auto simp: nres_rel_def conc_fun_chain[symmetric] conc_trans)

lemma pw_nres_rel_iff: "(a,b)∈⟨A⟩nres_rel ⟷ nofail (⇓ A b) ⟶ nofail a ∧ (∀x. inres a x ⟶ inres (⇓ A b) x)"

lemma param_SUCCEED[param]: "(SUCCEED,SUCCEED) ∈ ⟨R⟩nres_rel"
by (auto simp: nres_rel_def)

lemma param_FAIL[param]: "(FAIL,FAIL) ∈ ⟨R⟩nres_rel"
by (auto simp: nres_rel_def)

lemma param_RES[param]:
"(RES,RES) ∈ ⟨R⟩set_rel → ⟨R⟩nres_rel"
unfolding set_rel_def nres_rel_def
by (fastforce intro: RES_refine)

lemma param_RETURN[param]:
"(RETURN,RETURN) ∈ R → ⟨R⟩nres_rel"
by (auto simp: nres_rel_def RETURN_refine)

lemma param_bind[param]:
"(bind,bind) ∈ ⟨Ra⟩nres_rel → (Ra→⟨Rb⟩nres_rel) → ⟨Rb⟩nres_rel"
by (auto simp: nres_rel_def intro: bind_refine dest: fun_relD)

lemma param_ASSERT_bind[param]: "⟦
(Φ,Ψ) ∈ bool_rel;
⟦ Φ; Ψ ⟧ ⟹ (f,g)∈⟨R⟩nres_rel
⟧ ⟹ (ASSERT Φ ⪢ f, ASSERT Ψ ⪢ g) ∈ ⟨R⟩nres_rel"
by (auto intro: nres_relI)

subsection ‹Autoref Setup›

consts i_nres :: "interface ⇒ interface"
lemmas [autoref_rel_intf] = REL_INTFI[of nres_rel i_nres]

(*lemma id_nres[autoref_id_self]: "ID_LIST
(l SUCCEED FAIL bind (REC::_ ⇒ _ ⇒ _ nres,1) (RECT::_ ⇒ _ ⇒ _ nres,1))"
by simp_all
*)
(*definition [simp]: "op_RETURN x ≡ RETURN x"
lemma [autoref_op_pat_def]: "RETURN x ≡ op_RETURN x" by simp
*)

definition [simp]: "op_nres_ASSERT_bnd Φ m ≡ do {ASSERT Φ; m}"

lemma param_op_nres_ASSERT_bnd[param]:
assumes "Φ' ⟹ Φ"
assumes "⟦Φ'; Φ⟧ ⟹ (m,m')∈⟨R⟩nres_rel"
shows "(op_nres_ASSERT_bnd Φ m, op_nres_ASSERT_bnd Φ' m') ∈ ⟨R⟩nres_rel"
using assms
by (auto simp: pw_le_iff refine_pw_simps nres_rel_def)

context begin interpretation autoref_syn .
lemma id_ASSERT[autoref_op_pat_def]:
"do {ASSERT Φ; m} ≡ OP (op_nres_ASSERT_bnd Φ)$m" by simp definition [simp]: "op_nres_ASSUME_bnd Φ m ≡ do {ASSUME Φ; m}" lemma id_ASSUME[autoref_op_pat_def]: "do {ASSUME Φ; m} ≡ OP (op_nres_ASSUME_bnd Φ)$m"
by simp

end

lemma autoref_SUCCEED[autoref_rules]: "(SUCCEED,SUCCEED) ∈ ⟨R⟩nres_rel"
by (auto simp: nres_rel_def)

lemma autoref_FAIL[autoref_rules]: "(FAIL,FAIL) ∈ ⟨R⟩nres_rel"
by (auto simp: nres_rel_def)

lemma autoref_RETURN[autoref_rules]:
"(RETURN,RETURN) ∈ R → ⟨R⟩nres_rel"
by (auto simp: nres_rel_def RETURN_refine)

lemma autoref_bind[autoref_rules]:
"(bind,bind) ∈ ⟨R1⟩nres_rel → (R1→⟨R2⟩nres_rel) → ⟨R2⟩nres_rel"
apply (intro fun_relI)
apply (rule nres_relI)
apply (rule bind_refine)
apply (erule nres_relD)
apply (erule (1) fun_relD[THEN nres_relD])
done

context begin interpretation autoref_syn .
lemma autoref_ASSERT[autoref_rules]:
assumes "Φ ⟹ (m',m)∈⟨R⟩nres_rel"
shows "(
m',
(OP (op_nres_ASSERT_bnd Φ) ::: ⟨R⟩nres_rel → ⟨R⟩nres_rel) $m)∈⟨R⟩nres_rel" using assms unfolding nres_rel_def by (simp add: ASSERT_refine_right) lemma autoref_ASSUME[autoref_rules]: assumes "SIDE_PRECOND Φ" assumes "Φ ⟹ (m',m)∈⟨R⟩nres_rel" shows "( m', (OP (op_nres_ASSUME_bnd Φ) ::: ⟨R⟩nres_rel → ⟨R⟩nres_rel)$ m)∈⟨R⟩nres_rel"
using assms unfolding nres_rel_def

lemma autoref_REC[autoref_rules]:
assumes "(B,B')∈(Ra→⟨Rr⟩nres_rel) → Ra → ⟨Rr⟩nres_rel"
assumes "DEFER trimono B"
shows "(REC B,
(OP REC
::: ((Ra→⟨Rr⟩nres_rel) → Ra → ⟨Rr⟩nres_rel) → Ra → ⟨Rr⟩nres_rel)$B' ) ∈ Ra → ⟨Rr⟩nres_rel" apply (intro fun_relI) using assms apply (auto simp: nres_rel_def intro!: REC_refine) apply (simp add: fun_rel_def) apply blast done theorem param_RECT[param]: assumes "(B, B') ∈ (Ra → ⟨Rr⟩nres_rel) → Ra → ⟨Rr⟩nres_rel" and "trimono B" shows "(REC⇩T B, REC⇩T B')∈ Ra → ⟨Rr⟩nres_rel" apply (intro fun_relI) using assms apply (auto simp: nres_rel_def intro!: RECT_refine) apply (simp add: fun_rel_def) apply blast done lemma autoref_RECT[autoref_rules]: assumes "(B,B') ∈ (Ra→⟨Rr⟩nres_rel) → Ra→⟨Rr⟩nres_rel" assumes "DEFER trimono B" shows "(RECT B, (OP RECT ::: ((Ra→⟨Rr⟩nres_rel) → Ra → ⟨Rr⟩nres_rel) → Ra → ⟨Rr⟩nres_rel)$B'
) ∈ Ra → ⟨Rr⟩nres_rel"
using assms
unfolding autoref_tag_defs
by (rule param_RECT)

end

subsection ‹Convenience Rules›
text ‹
In this section, we define some lemmas that simplify common prover tasks.
›

lemma ref_two_step: "A≤⇓R  B ⟹ B≤C ⟹ A≤⇓R  C"

lemma pw_ref_iff:
shows "S ≤ ⇓R S'
⟷ (nofail S'
⟶ nofail S ∧ (∀x. inres S x ⟶ (∃s'. (x, s') ∈ R ∧ inres S' s')))"

lemma pw_ref_I:
assumes "nofail S'
⟶ nofail S ∧ (∀x. inres S x ⟶ (∃s'. (x, s') ∈ R ∧ inres S' s'))"
shows "S ≤ ⇓R S'"
using assms

text ‹Introduce an abstraction relation. Usage:
‹rule introR[where R=absRel]›
›
lemma introR: "(a,a')∈R ⟹ (a,a')∈R" .

lemma intro_prgR: "c ≤ ⇓R a ⟹ c ≤ ⇓R a" by auto

lemma refine_IdI: "m ≤ m' ⟹ m ≤ ⇓Id m'" by simp

lemma le_ASSERTI_pres:
assumes "Φ ⟹ S ≤ do {ASSERT Φ; S'}"
shows "S ≤ do {ASSERT Φ; S'}"
using assms by (auto intro: le_ASSERTI)

lemma RETURN_ref_SPECD:
assumes "RETURN c ≤ ⇓R (SPEC Φ)"
obtains a where "(c,a)∈R" "Φ a"
using assms
by (auto simp: pw_le_iff refine_pw_simps)

lemma RETURN_ref_RETURND:
assumes "RETURN c ≤ ⇓R (RETURN a)"
shows "(c,a)∈R"
using assms
apply (auto simp: pw_le_iff refine_pw_simps)
done

lemma return_refine_prop_return:
assumes "nofail m"
assumes "RETURN x ≤ ⇓R m"
obtains x' where "(x,x')∈R" "RETURN x' ≤ m"
using assms
by (auto simp: refine_pw_simps pw_le_iff)

lemma ignore_snd_refine_conv:
"(m ≤ ⇓(R×⇩rUNIV) m') ⟷ m⤜(RETURN o fst) ≤⇓R (m'⤜(RETURN o fst))"
by (auto simp: pw_le_iff refine_pw_simps)

lemma ret_le_down_conv:
"nofail m ⟹ RETURN c ≤ ⇓R m ⟷ (∃a. (c,a)∈R ∧ RETURN a ≤ m)"
by (auto simp: pw_le_iff refine_pw_simps)

lemma SPEC_eq_is_RETURN:
"SPEC ((=) x) = RETURN x"
"SPEC (λx. x=y) = RETURN y"
by (auto simp: RETURN_def)

lemma RETURN_SPEC_conv: "RETURN r = SPEC (λx. x=r)"

lemma refine2spec_aux:
"a ≤ ⇓R b ⟷ ( (nofail b ⟶ a ≤ SPEC ( λr. (∃x. inres b x ∧ (r,x)∈R) )) )"
by (auto simp: pw_le_iff refine_pw_simps)

lemma refine2specI:
assumes "nofail b ⟹ a ≤ SPEC (λr. (∃x. inres b x ∧ (r,x)∈R) )"
shows "a ≤ ⇓R b"
using assms by (simp add: refine2spec_aux)

lemma specify_left:
assumes "m ≤ SPEC Φ"
assumes "⋀x. Φ x ⟹ f x ≤ M"
shows "do { x ← m; f x } ≤ M"
using assms by (auto simp: pw_le_iff refine_pw_simps)

lemma build_rel_SPEC:
"M ≤ SPEC ( λx. Φ (α x) ∧ I x) ⟹ M ≤ ⇓(build_rel α I) (SPEC Φ)"
by (auto simp: pw_le_iff refine_pw_simps build_rel_def)

lemma build_rel_SPEC_conv: "⇓(br α I) (SPEC Φ) = SPEC (λx. I x ∧ Φ (α x))"
by (auto simp: br_def pw_eq_iff refine_pw_simps)

lemma refine_IdD: "c ≤ ⇓Id a ⟹ c ≤ a" by simp

lemma bind_sim_select_rule:
assumes "m⤜f' ≤ SPEC Ψ"
assumes "⋀x. ⟦nofail m; inres m x; f' x≤SPEC Ψ⟧ ⟹ f x≤SPEC Φ"
shows "m⤜f ≤ SPEC Φ"
― ‹Simultaneously select a result from assumption and verification goal.
Useful to work with assumptions that restrict the current program to
be verified.›
using assms
by (auto simp: pw_le_iff refine_pw_simps)

lemma assert_bind_spec_conv: "ASSERT Φ ⪢ m ≤ SPEC Ψ ⟷ (Φ ∧ m ≤ SPEC Ψ)"
― ‹Simplify a bind-assert verification condition.
Useful if this occurs in the assumptions, and considerably faster than
using pointwise reasoning, which may causes a blowup for many chained
assertions.›
by (auto simp: pw_le_iff refine_pw_simps)

lemma summarize_ASSERT_conv: "do {ASSERT Φ; ASSERT Ψ; m} = do {ASSERT (Φ ∧ Ψ); m}"
by (auto simp: pw_eq_iff refine_pw_simps)

lemma bind_ASSERT_eq_if: "do { ASSERT Φ; m } = (if Φ then m else FAIL)"
by auto

lemma le_RES_nofailI:
assumes "a≤RES x"
shows "nofail a"
using assms
by (metis nofail_simps(2) pwD1)

assumes "f x ≤⇓R (f' x')"
and "nofail (f x) ⟹ f x ≤ SPEC I"
shows "f x ≤ ⇓ {(c, a). (c, a) ∈ R ∧ I c} (f' x')"
using assms

lemma bind_RES_RETURN_eq: "bind (RES X) (λx. RETURN (f x)) =
RES { f x | x. x∈X }"
blast

lemma bind_RES_RETURN2_eq: "bind (RES X) (λ(x,y). RETURN (f x y)) =
RES { f x y | x y. (x,y)∈X }"
apply blast
done

lemma le_SPEC_bindI:
assumes "Φ x"
assumes "m ≤ f x"
shows "m ≤ SPEC Φ ⤜ f"
using assms by (auto simp add: pw_le_iff refine_pw_simps)

lemma bind_assert_refine:
assumes "m1 ≤ SPEC Φ"
assumes "⋀x. Φ x ⟹ m2 x ≤ m'"
shows "do {x←m1; ASSERT (Φ x); m2 x} ≤ m'"
using assms
by (simp add: pw_le_iff refine_pw_simps) blast

lemma RETURN_refine_iff[simp]: "RETURN x ≤⇓R (RETURN y) ⟷ (x,y)∈R"
by (auto simp: pw_le_iff refine_pw_simps)

lemma RETURN_RES_refine_iff:
"RETURN x ≤⇓R (RES Y) ⟷ (∃y∈Y. (x,y)∈R)"
by (auto simp: pw_le_iff refine_pw_simps)

lemma RETURN_RES_refine:
assumes "∃x'. (x,x')∈R ∧ x'∈X"
shows "RETURN x ≤ ⇓R (RES X)"
using assms
by (auto simp: pw_le_iff refine_pw_simps)

lemma in_nres_rel_iff: "(a,b)∈⟨R⟩nres_rel ⟷ a ≤⇓R b"
by (auto simp: nres_rel_def)

lemma inf_RETURN_RES:
"inf (RETURN x) (RES X) = (if x∈X then RETURN x else SUCCEED)"
"inf (RES X) (RETURN x) = (if x∈X then RETURN x else SUCCEED)"
by (auto simp: pw_eq_iff refine_pw_simps)

lemma inf_RETURN_SPEC[simp]:
"inf (RETURN x) (SPEC (λy. Φ y)) = SPEC (λy. y=x ∧ Φ x)"
"inf (SPEC (λy. Φ y)) (RETURN x) = SPEC (λy. y=x ∧ Φ x)"
by (auto simp: pw_eq_iff refine_pw_simps)

lemma RES_sng_eq_RETURN: "RES {x} = RETURN x"
by simp

lemma nofail_inf_serialize:
"⟦nofail a; nofail b⟧ ⟹ inf a b = do {x←a; ASSUME (inres b x); RETURN x}"
by (auto simp: pw_eq_iff refine_pw_simps)

lemma conc_fun_SPEC:
"⇓R (SPEC (λx. Φ x)) = SPEC (λy. ∃x. (y,x)∈R ∧ Φ x)"
by (auto simp: pw_eq_iff refine_pw_simps)

lemma conc_fun_RETURN:
"⇓R (RETURN x) = SPEC (λy. (y,x)∈R)"
by (auto simp: pw_eq_iff refine_pw_simps)

lemma use_spec_rule:
assumes "m ≤ SPEC Ψ"
assumes "m ≤ SPEC (λs. Ψ s ⟶ Φ s)"
shows "m ≤ SPEC Φ"
using assms
by (auto simp: pw_le_iff refine_pw_simps)

lemma strengthen_SPEC: "m ≤ SPEC Φ ⟹ m ≤ SPEC(λs. inres m s ∧ nofail m ∧ Φ s)"
― ‹Strengthen SPEC by adding trivial upper bound for result›
by (auto simp: pw_le_iff refine_pw_simps)

lemma weaken_SPEC:
"m ≤ SPEC Φ ⟹ (⋀x. Φ x ⟹ Ψ x) ⟹ m ≤ SPEC Ψ"
by (force elim!: order_trans)

lemma bind_le_nofailI:
assumes "nofail m"
assumes "⋀x. RETURN x ≤ m ⟹ f x ≤ m'"
shows "m⤜f ≤ m'"
using assms
by (simp add: refine_pw_simps pw_le_iff) blast

lemma bind_le_shift:
"bind m f ≤ m'
⟷ m ≤ (if nofail m' then SPEC (λx. f x ≤ m') else FAIL)"
by (auto simp: pw_le_iff refine_pw_simps)

lemma If_bind_distrib[simp]:
fixes t e :: "'a nres"
shows "(If b t e ⤜ (λx. f x)) = (If b (t⤜(λx. f x)) (e⤜(λx. f x)))"
by simp

(* TODO: Can we make this a simproc, using NO_MATCH? *)
lemma unused_bind_conv:
assumes "NO_MATCH (ASSERT Φ) m"
assumes "NO_MATCH (ASSUME Φ) m"
shows "(m⤜(λx. c))  = (ASSERT (nofail m) ⤜ (λ_. ASSUME (∃x. inres m x) ⤜ (λx. c)))"
by (auto simp: pw_eq_iff refine_pw_simps)

text ‹The following rules are useful for massaging programs before the
refinement takes place›
lemma let_to_bind_conv:
"Let x f = RETURN x⤜f"
by simp

lemmas bind_to_let_conv = let_to_bind_conv[symmetric]

lemma pull_out_let_conv: "RETURN (Let x f) = Let x (λx. RETURN (f x))"
by simp

lemma push_in_let_conv:
"Let x (λx. RETURN (f x)) = RETURN (Let x f)"
"Let x (RETURN o f) = RETURN (Let x f)"
by simp_all

lemma pull_out_RETURN_case_option:
"case_option (RETURN a) (λv. RETURN (f v)) x = RETURN (case_option a f x)"
by (auto split: option.splits)

lemma if_bind_cond_refine:
assumes "ci ≤ RETURN b"
assumes "b ⟹ ti≤⇓R t"
assumes "¬b ⟹ ei≤⇓R e"
shows "do {b←ci; if b then ti else ei} ≤ ⇓R (if b then t else e)"
using assms
by (auto simp add: refine_pw_simps pw_le_iff)

lemma intro_RETURN_Let_refine:
assumes "RETURN (f x) ≤ ⇓R M'"
shows "RETURN (Let x f) ≤ ⇓R M'"
(* this should be needed very rarely - so don't add it *)
using assms by auto

lemma ife_FAIL_to_ASSERT_cnv:
"(if Φ then m else FAIL) = op_nres_ASSERT_bnd Φ m"
by (cases Φ, auto)

lemma nres_bind_let_law: "(do { x ← do { let y=v; f y }; g x } :: _ nres)
= do { let y=v; x← f y; g x }" by auto

lemma unused_bind_RES_ne[simp]: "X≠{} ⟹ do { _ ← RES X; m} = m"
by (auto simp: pw_eq_iff refine_pw_simps)

lemma le_ASSERT_defI1:
assumes "c ≡ do {ASSERT Φ; m}"
assumes "Φ ⟹ m' ≤ c"
shows "m' ≤ c"
using assms

lemma refine_ASSERT_defI1:
assumes "c ≡ do {ASSERT Φ; m}"
assumes "Φ ⟹ m' ≤ ⇓R c"
shows "m' ≤ ⇓R c"
using assms
by (simp, refine_vcg)

lemma le_ASSERT_defI2:
assumes "c ≡ do {ASSERT Φ; ASSERT Ψ; m}"
assumes "⟦Φ; Ψ⟧ ⟹ m' ≤ c"
shows "m' ≤ c"
using assms

lemma refine_ASSERT_defI2:
assumes "c ≡ do {ASSERT Φ; ASSERT Ψ; m}"
assumes "⟦Φ; Ψ⟧ ⟹ m' ≤ ⇓R c"
shows "m' ≤ ⇓R c"
using assms
by (simp, refine_vcg)

lemma ASSERT_le_defI:
assumes "c ≡ do { ASSERT Φ; m'}"
assumes "Φ"
assumes "Φ ⟹ m' ≤ m"
shows "c ≤ m"
using assms by (auto)

lemma ASSERT_same_eq_conv: "(ASSERT Φ ⪢ m) = (ASSERT Φ ⪢ n) ⟷ (Φ ⟶ m=n)"
by auto

lemma case_prod_bind_simp[simp]: "
(λx. (case x of (a, b) ⇒ f a b) ≤ SPEC Φ) = (λ(a,b). f a b ≤ SPEC Φ)"
by auto

lemma RECT_eq_REC': "nofail (RECT B x) ⟹ RECT B x = REC B x"
by (subst RECT_eq_REC; simp_all add: nofail_def)

lemma rel2p_nres_RETURN[rel2p]: "rel2p (⟨A⟩nres_rel) (RETURN x) (RETURN y) = rel2p A x y"
by (auto simp: rel2p_def dest: nres_relD intro: nres_relI)

subsubsection ‹Boolean Operations on Specifications›
lemma SPEC_iff:
assumes "P ≤ SPEC (λs. Q s ⟶ R s)"
and "P ≤ SPEC (λs. ¬ Q s ⟶ ¬ R s)"
shows "P ≤ SPEC (λs. Q s ⟷ R s)"
using assms[THEN pw_le_iff[THEN iffD1]]
by (auto intro!: pw_leI)

lemma SPEC_rule_conjI:
assumes "A ≤ SPEC P" and "A ≤ SPEC Q"
shows "A ≤ SPEC (λv. P v ∧ Q v)"
proof -
have "A ≤ inf (SPEC P) (SPEC Q)" using assms by (rule_tac inf_greatest) assumption
thus ?thesis by (auto simp add:Collect_conj_eq)
qed

lemma SPEC_rule_conjunct1:
assumes "A ≤ SPEC (λv. P v ∧ Q v)"
shows "A ≤ SPEC P"
proof -
note assms
also have "… ≤ SPEC P" by (rule SPEC_rule) auto
finally show ?thesis .
qed

lemma SPEC_rule_conjunct2:
assumes "A ≤ SPEC (λv. P v ∧ Q v)"
shows "A ≤ SPEC Q"
proof -
note assms
also have "… ≤ SPEC Q" by (rule SPEC_rule) auto
finally show ?thesis .
qed

subsubsection ‹Pointwise Reasoning›
lemma inres_if:
"⟦ inres (if P then Q else R) x; ⟦P; inres Q x⟧ ⟹ S; ⟦¬ P; inres R x⟧ ⟹ S ⟧ ⟹ S"
by (metis (full_types))

lemma inres_SPEC:
"inres M x ⟹ M ≤ SPEC Φ ⟹ Φ x"
by (auto dest: pwD2)

lemma SPEC_nofail:
"X ≤ SPEC Φ ⟹ nofail X"
by (auto dest: pwD1)

lemma nofail_SPEC: "nofail m ⟹ m ≤ SPEC (λ_. True)"

lemma nofail_SPEC_iff: "nofail m ⟷ m ≤ SPEC (λ_. True)"

lemma nofail_SPEC_triv_refine: "⟦ nofail m; ⋀x. Φ x ⟧ ⟹ m ≤ SPEC Φ"

end


# Theory Refine_Leof

section ‹Less-Equal or Fail›
(* TODO: Move to Refinement Framework *)
theory Refine_Leof
imports Refine_Basic
begin
text ‹A predicate that states refinement or that the LHS fails.›

definition le_or_fail :: "'a nres ⇒ 'a nres ⇒ bool" (infix "≤⇩n" 50) where
"m ≤⇩n m' ≡ nofail m ⟶ m ≤ m'"

lemma leofI[intro?]:
assumes "nofail m ⟹ m ≤ m'" shows "m ≤⇩n m'"
using assms unfolding le_or_fail_def by auto

lemma leofD:
assumes "nofail m"
assumes "m ≤⇩n m'"
shows "m ≤ m'"
using assms unfolding le_or_fail_def by blast

lemma pw_leof_iff:
"m ≤⇩n m' ⟷ (nofail m ⟶ (∀x. inres m x ⟶ inres m' x))"
unfolding le_or_fail_def by (auto simp add: pw_le_iff refine_pw_simps)

lemma le_by_leofI: "⟦ nofail m' ⟹ nofail m; m≤⇩nm' ⟧ ⟹ m ≤ m'"
by (auto simp: pw_le_iff pw_leof_iff)

lemma inres_leof_mono: "m≤⇩nm' ⟹ nofail m ⟹ inres m x ⟹ inres m' x"
by (auto simp: pw_leof_iff)

lemma leof_trans[trans]: "⟦a ≤⇩n RES X; RES X ≤⇩n c⟧ ⟹ a ≤⇩n c"
by (auto simp: pw_leof_iff)

lemma leof_trans_nofail: "⟦ a≤⇩nb; nofail b; b≤⇩nc ⟧ ⟹ a ≤⇩n c"
by (auto simp: pw_leof_iff)

lemma leof_refl[simp]: "a ≤⇩n a"
by (auto simp: pw_leof_iff)

lemma leof_RES_UNIV[simp, intro!]: "m ≤⇩n RES UNIV"
by (auto simp: pw_leof_iff)

lemma leof_FAIL[simp, intro!]: "m ≤⇩n FAIL" by (auto simp: pw_leof_iff)
lemma FAIL_leof[simp, intro!]: "FAIL ≤⇩n m"
by (auto simp: le_or_fail_def)

lemma leof_lift:
"m ≤ F ⟹ m ≤⇩n F"
by (auto simp add: pw_leof_iff pw_le_iff)

lemma leof_RETURN_rule[refine_vcg]:
"Φ m ⟹ RETURN m ≤⇩n SPEC Φ" by (simp add: pw_leof_iff)

lemma leof_bind_rule[refine_vcg]:
"⟦ m ≤⇩n SPEC (λx. f x ≤⇩n SPEC Φ) ⟧ ⟹ m⤜f ≤⇩n SPEC Φ"
by (auto simp add: pw_leof_iff refine_pw_simps)

lemma RETURN_leof_RES_iff[simp]: "RETURN x ≤⇩n RES Y ⟷ x∈Y"
by (auto simp add: pw_leof_iff refine_pw_simps)

lemma RES_leof_RES_iff[simp]: "RES X ≤⇩n RES Y ⟷ X ⊆ Y"
by (auto simp add: pw_leof_iff refine_pw_simps)

lemma leof_Let_rule[refine_vcg]: "f x ≤⇩n SPEC Φ ⟹ Let x f ≤⇩n SPEC Φ"
by simp

lemma leof_If_rule[refine_vcg]:
"⟦c ⟹ t ≤⇩n SPEC Φ; ¬c ⟹ e ≤⇩n SPEC Φ⟧ ⟹ If c t e ≤⇩n SPEC Φ"
by simp

lemma leof_RES_rule[refine_vcg]:
"⟦⋀x. Ψ x ⟹ Φ x⟧ ⟹ SPEC Ψ ≤⇩n SPEC Φ"
"⟦⋀x. x∈X ⟹ Φ x⟧ ⟹ RES X ≤⇩n SPEC Φ"
by auto

lemma leof_True_rule: "⟦⋀x. Φ x⟧ ⟹ m ≤⇩n SPEC Φ"
by (auto simp add: pw_leof_iff refine_pw_simps)

lemma sup_leof_iff: "(sup a b ≤⇩n m) ⟷ (nofail a ∧ nofail b ⟶ a≤⇩nm ∧ b≤⇩nm)"
by (auto simp: pw_leof_iff refine_pw_simps)

lemma sup_leof_rule[refine_vcg]:
assumes "⟦nofail a; nofail b⟧ ⟹ a≤⇩nm"
assumes "⟦nofail a; nofail b⟧ ⟹ b≤⇩nm"
shows "sup a b ≤⇩n m"
using assms by (auto simp: pw_leof_iff refine_pw_simps)

lemma leof_option_rule[refine_vcg]:
"⟦v = None ⟹ S1 ≤⇩n SPEC Φ; ⋀x. v = Some x ⟹ f2 x ≤⇩n SPEC Φ⟧
⟹ (case v of None ⇒ S1 | Some x ⇒ f2 x) ≤⇩n SPEC Φ"
by (cases v) auto

lemma ASSERT_leof_rule[refine_vcg]:
assumes "Φ ⟹ m ≤⇩n m'"
shows "do {ASSERT Φ; m} ≤⇩n m'"
using assms
by (cases Φ, auto simp: pw_leof_iff)

lemma leof_ASSERT_rule[refine_vcg]: "⟦Φ ⟹ m ≤⇩n m'⟧ ⟹ m ≤⇩n ASSERT Φ ⪢ m'"
by (auto simp: pw_leof_iff refine_pw_simps)

lemma leof_ASSERT_refine_rule[refine]: "⟦Φ ⟹ m ≤⇩n ⇓R m'⟧ ⟹ m ≤⇩n ⇓R (ASSERT Φ ⪢ m')"
by (auto simp: pw_leof_iff refine_pw_simps)

lemma ASSUME_leof_iff: "(ASSUME Φ ≤⇩n SPEC Ψ) ⟷ (Φ ⟶ Ψ ())"
by (auto simp: pw_leof_iff)

lemma ASSUME_leof_rule[refine_vcg]:
assumes "Φ ⟹ Ψ ()"
shows "ASSUME Φ ≤⇩n SPEC Ψ"
using assms
by (auto simp: ASSUME_leof_iff)

lemma SPEC_rule_conj_leofI1:
assumes "m ≤ SPEC Φ"
assumes "m ≤⇩n SPEC Ψ"
shows "m ≤ SPEC (λs. Φ s ∧ Ψ s)"
using assms by (auto simp: pw_le_iff pw_leof_iff)

lemma SPEC_rule_conj_leofI2:
assumes "m ≤⇩n SPEC Φ"
assumes "m ≤ SPEC Ψ"
shows "m ≤ SPEC (λs. Φ s ∧ Ψ s)"
using assms by (auto simp: pw_le_iff pw_leof_iff)

lemma SPEC_rule_leof_conjI:
assumes "m ≤⇩n SPEC Φ" "m ≤⇩n SPEC Ψ"
shows "m ≤⇩n SPEC (λx. Φ x ∧ Ψ x)"
using assms by (auto simp: pw_leof_iff)

lemma leof_use_spec_rule:
assumes "m ≤⇩n SPEC Ψ"
assumes "m ≤⇩n SPEC (λs. Ψ s ⟶ Φ s)"
shows "m ≤⇩n SPEC Φ"
using assms by (auto simp: pw_leof_iff refine_pw_simps)

lemma use_spec_leof_rule:
assumes "m ≤⇩n SPEC Ψ"
assumes "m ≤ SPEC (λs. Ψ s ⟶ Φ s)"
shows "m ≤ SPEC Φ"
using assms by (auto simp: pw_leof_iff pw_le_iff refine_pw_simps)

lemma leof_strengthen_SPEC:
"m ≤⇩n SPEC Φ ⟹ m ≤⇩n SPEC (λx. inres m x ∧ Φ x)"
by (auto simp: pw_leof_iff)

lemma build_rel_SPEC_leof:
assumes "m ≤⇩n SPEC (λx. I x ∧ Φ (α x))"
shows "m ≤⇩n ⇓(br α I) (SPEC Φ)"
using assms by (auto simp: build_rel_SPEC_conv)

lemma RETURN_as_SPEC_refine_leof[refine2]:
assumes "M ≤⇩n SPEC (λc. (c,a)∈R)"
shows "M ≤⇩n ⇓R (RETURN a)"
using assms

lemma ASSERT_leof_defI:
assumes "c ≡ do { ASSERT Φ; m'}"
assumes "Φ ⟹ m' ≤⇩n m"
shows "c ≤⇩n m"
using assms by (auto simp: pw_leof_iff refine_pw_simps)

lemma leof_fun_conv_le:
"(f x ≤⇩n M x) ⟷ (f x ≤ (if nofail (f x) then M x else FAIL))"
by (auto simp: pw_le_iff pw_leof_iff)

lemma leof_add_nofailI: "⟦ nofail m ⟹ m≤⇩nm' ⟧ ⟹ m≤⇩nm'"
by (auto simp: pw_le_iff pw_leof_iff)

lemma leof_cons_rule[refine_vcg_cons]:
assumes "m ≤⇩n SPEC Q"
assumes "⋀x. Q x ⟹ P x"
shows "m ≤⇩n SPEC P"
using assms
by (auto simp: pw_le_iff pw_leof_iff)

lemma RECT_rule_leof:
assumes WF: "wf (V::('x×'x) set)"
assumes I0: "pre (x::'x)"
assumes IS: "⋀f x. ⟦ ⋀x'. ⟦pre x'; (x',x)∈V⟧ ⟹ f x' ≤⇩n M x'; pre x;
RECT body = f
⟧ ⟹ body f x ≤⇩n M x"
shows "RECT body x ≤⇩n M x"
apply (cases "¬trimono body")
using assms
unfolding leof_fun_conv_le
apply -
apply (rule RECT_rule[where pre=pre and V=V])
apply clarsimp_all
proof -
fix xa :: 'x
assume a1: "⋀x'. ⟦pre x'; (x', xa) ∈ V⟧ ⟹ REC⇩T body x' ≤ (if nofail (REC⇩T body x') then M x' else FAIL)"
assume a2: "⋀x f. ⟦⋀x'. ⟦pre x'; (x', x) ∈ V⟧ ⟹ f x' ≤ (if nofail (f x') then M x' else FAIL); pre x; REC⇩T body = f⟧ ⟹ body f x ≤ (if nofail (body f x) then M x else FAIL)"
assume a3: "pre xa"
assume a4: "nofail (REC⇩T body xa)"
assume a5: "trimono body"
have f6: "∀x. ¬ pre x ∨ (x, xa) ∉ V ∨ (if nofail (REC⇩T body x) then REC⇩T body x ≤ M x else REC⇩T body x ≤ FAIL)"
using a1 by presburger
have f7: "∀x f. ((∃xa. (pre xa ∧ (xa, x) ∈ V) ∧ ¬ f xa ≤ (if nofail (f xa) then M xa else FAIL)) ∨ ¬ pre x ∨ REC⇩T body ≠ f) ∨ body f x ≤ (if nofail (body f x) then M x else FAIL)"
using a2 by blast
obtain xx :: "('x ⇒ 'a nres) ⇒ 'x ⇒ 'x" where
f8: "∀x0 x1. (∃v2. (pre v2 ∧ (v2, x1) ∈ V) ∧ ¬ x0 v2 ≤ (if nofail (x0 v2) then M v2 else FAIL)) = ((pre (xx x0 x1) ∧ (xx x0 x1, x1) ∈ V) ∧ ¬ x0 (xx x0 x1) ≤ (if nofail (x0 (xx x0 x1)) then M (xx x0 x1) else FAIL))"
by moura
have f9: "∀x0 x1. (x0 (xx x0 x1) ≤ (if nofail (x0 (xx x0 x1)) then M (xx x0 x1) else FAIL)) = (if nofail (x0 (xx x0 x1)) then x0 (xx x0 x1) ≤ M (xx x0 x1) else x0 (xx x0 x1) ≤ FAIL)"
by presburger
have "nofail (body (REC⇩T body) xa)"
using a5 a4 by (metis (no_types) RECT_unfold)
then show "body (REC⇩T body) xa ≤ M xa"
using f9 f8 f7 f6 a3 by fastforce
qed

(* TODO: REC_rule_leof! (However, this may require some fix
to the domain theory model of Refine_Monadic!) *)

end



# Theory Refine_Heuristics

section ‹Data Refinement Heuristics›
theory Refine_Heuristics
imports Refine_Basic
begin

text ‹
This theory contains some heuristics to automatically prove
data refinement goals that are left over by the refinement condition
generator.
›

text ‹
The theorem collection ‹refine_hsimp› contains additional simplifier
rules that are useful to discharge typical data refinement goals.
›

ML ‹
structure refine_heuristics_simps = Named_Thms
( val name = @{binding refine_hsimp}
val description = "Refinement Framework: " ^
"Data refinement heuristics simp rules" );
›

setup ‹refine_heuristics_simps.setup›

subsection ‹Type Based Heuristics›
text ‹
This heuristics instantiates schematic data refinement relations based
on their type. Both, the left hand side and right hand side type are
considered.
›

text ‹The heuristics works by proving goals of the form
‹RELATES ?R›, thereby instantiating ‹?R›.›
definition RELATES :: "('a×'b) set ⇒ bool" where "RELATES R ≡ True"
lemma RELATESI: "RELATES R" by (simp add: RELATES_def)

ML ‹
structure Refine_dref_type = struct
structure pattern_rules = Named_Thms
( val name = @{binding refine_dref_pattern}
val description = "Refinement Framework: " ^
"Pattern rules to recognize refinement goal" );

structure RELATES_rules = Named_Thms (
val name = @{binding refine_dref_RELATES}
val description = "Refinement Framework: " ^
"Type based heuristics introduction rules"
);

val tracing =
`