Theory Mutual_CCPO_Recursion

(*
 * Copyright (c) 2022 Apple Inc. All rights reserved.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

chapter ‹Mutual CCPO Recursion fixed_point›

theory Mutual_CCPO_Recursion
  imports
    "HOL-Library.Complete_Partial_Order2"
    "AutoCorres_Utils"
  keywords "fixed_point" :: thy_goal_stmt
begin

section ‹Relate orders between locale and type classes›

lemma gfp_lub_fun: "gfp.lub_fun = Inf"
  unfolding fun_lub_def fun_eq_iff Inf_apply image_def by simp

lemma gfp_le_fun: "gfp.le_fun = (≥)"
  unfolding fun_ord_def le_fun_def fun_eq_iff Inf_apply image_def by simp

lemma
  shows fst_prod_lub: "fst (prod_lub luba lubb S) = luba (fst ` S)"
    and snd_prod_lub: "snd (prod_lub luba lubb S) = lubb (snd ` S)"
  by (auto simp: prod_lub_def)

lemma fun_lub_app: "fun_lub lub S x = lub ((λf. f x) ` S)"
  by (auto simp: fun_lub_def image_def)

lemma ccpo_Inf: "class.ccpo (Inf :: 'a::complete_lattice set  _) (≥) (mk_less (≥))"
  by (rule cont_intro)

lemma ccpo_Sup: "class.ccpo (Sup :: 'a::complete_lattice set  _) (≤) (mk_less (≤))"
  by (rule cont_intro)

lemma ccpo_flat: "class.ccpo (flat_lub b) (flat_ord b) (mk_less (flat_ord b))"
  using Partial_Function.ccpo[OF flat_interpretation] .

lemma monotone_pair[partial_function_mono]:
  "monotone R orda f  monotone R ordb g  monotone R (rel_prod orda ordb) (λx. (f x, g x))"
  by (simp add: monotone_def)

lemma monotone_fst'[partial_function_mono]:
  "monotone orda (rel_prod ordb ordc) f  monotone orda ordb (λx. fst (f x))"
  by (auto simp add: monotone_def rel_prod_sel)

lemma monotone_snd'[partial_function_mono]:
  "monotone orda (rel_prod ordb ordc) f  monotone orda ordc (λx. snd (f x))"
  by (auto simp add: monotone_def rel_prod_sel)

lemma monotone_id_fun_elim[partial_function_mono]:
  "monotone (≥) ord (λx. x)  monotone (≥) (fun_ord ord) (λx. x)"
  by (auto simp add: monotone_def le_fun_def fun_ord_def)

lemma monotone_id[partial_function_mono]: "monotone ord ord (λx. x)"
  by (auto simp add: monotone_def)

lemma monotone_abs:
  "(x. monotone R Q (λf. F f x))  monotone R (fun_ord Q) (λf x. F f x)"
  by (simp add: monotone_def fun_ord_def)

lemma monotone_fun_ord_applyD:
  "monotone orda (fun_ord ordb) f  monotone orda ordb (λy. f y x)"
  by(auto simp add: monotone_def fun_ord_def)

lemma admissible_snd:
  "cont luba orda (prod_lub lubb Inf) (rel_prod ordb (≥)) F 
    ccpo.admissible luba orda (λx. snd (F x))"
  unfolding ccpo.admissible_def cont_def prod_eq_iff
  by (auto simp: prod_lub_def)

lemma cont_apply_gfp: "cont gfp.lub_fun gfp.le_fun Inf (≤) (λx. x c)"
  by (rule cont_applyI) (simp add: cont_def)

lemma mcont_mem_gfp:
  "mcont gfp.lub_fun gfp.le_fun (Inf) (≥) F  gfp.admissible (λA. x  F A)"
  by (auto simp: mcont_def cont_def ccpo.admissible_def)

lemma mcont2mcont_call:
  "mcont luba orda (fun_lub lubb) (fun_ord ordb) F  mcont luba orda lubb ordb (λx. F x c)"
  by (auto simp: mcont_def monotone_def cont_def fun_lub_def fun_ord_def le_fun_def fun_eq_iff)
     (simp add: image_def)

lemma preorder_fun_ord [partial_function_mono]: "class.preorder R (mk_less R)  class.preorder (fun_ord R) (mk_less (fun_ord R))"
  by (force simp: class.preorder_def fun_ord_def mk_less_def)

lemma preorder_monotone_const'[partial_function_mono]: 
 "class.preorder leq (mk_less leq)  monotone ord leq (λ_. c)"
  by (rule preorder.monotone_const)

declare preorder_rel_prodI [partial_function_mono]
declare gfp.preorder [partial_function_mono]
declare lfp.preorder [partial_function_mono]

lemma option_ord_preorder [partial_function_mono]: "class.preorder option_ord (mk_less option_ord)" 
  by simp

section ‹Prove admissibility of corresXF›

lemma not_imp_not_iff: "(¬A  ¬B)  (B  A)"
  by auto

lemma mcont_fun_lub_call:
  "mcont luba orda (fun_lub lubb) (fun_ord ordb) f 
     mcont luba orda lubb ordb (λy. f y x)"
  by (simp add: mcont_fun_lub_apply)

lemma chain_disj_of_subsingleton:
  "Complete_Partial_Order.chain ord {r. P r} 
    Complete_Partial_Order.chain ord {r. Q r} 
    (r q. P r  Q q  r = q) 
    Complete_Partial_Order.chain ord {r. P r  Q r}"
  by (auto simp: chain_def)

definition subsingleton_set :: "'a set  bool" where
  "subsingleton_set P  (aP. bP. a = b)"

lemma subsingleton_set_empty[iff]: "subsingleton_set {}"
  by (simp add: subsingleton_set_def)

lemma subsingleton_set_singleton[iff]: "subsingleton_set {x}"
  by (simp add: subsingleton_set_def)

context ccpo
begin

lemma subsingleton_sets_imp_chain:
  "subsingleton_set ( Ps)  Complete_Partial_Order.chain (≤) ( Ps)"
  by (auto simp: subsingleton_set_def Complete_Partial_Order.chain_def Ball_def)

lemma Sup_of_subsingleton_sets_eq:
  assumes Ps: "subsingleton_set ( Ps)" and P: "P  Ps" and a: "a  P"
  shows "Sup ( Ps) = a" 
proof (intro order.antisym ccpo_Sup_least ccpo_Sup_upper subsingleton_sets_imp_chain[OF Ps])
  fix x :: 'a assume "x   Ps"
  then obtain Q where "Q  Ps" "x  Q" by auto
  with Ps P a show "x  a"
    by (auto simp add: subsingleton_set_def Ball_def)
qed (use P a in blast)

lemma monotone_Sup_of_subsingleton_sets:
  assumes Ps: "F. subsingleton_set ( (Ps F))"
    and *: "F G. ord F G  sim_set (sim_set (≤)) (Ps F) (Ps G)"
  shows "monotone ord (≤) (λF. Sup ( (Ps F)))"
proof (intro monotoneI ccpo_Sup_least subsingleton_sets_imp_chain[OF Ps])
  fix F G x assume "ord F G" "x   (Ps F)"
  with *[of F G] obtain y where "x  y" "y   (Ps G)"
    by (fastforce simp: sim_set_def)
  then show "x  Sup ( (Ps G))"
    apply (intro order_trans[OF x  y])
    apply (intro ccpo_Sup_upper subsingleton_sets_imp_chain[OF Ps])
    apply auto
    done
qed

lemma ccpo_refl: "x  x" ..

lemma fixp_unfold_def:
  fixes f :: "'a  'a"
  assumes def: "F  ccpo.fixp Sup (≤) f"
  assumes f: "monotone (≤) (≤) f"
  shows "F = f F"
  by (unfold def) (rule fixp_unfold[OF f])

lemma fixp_induct_def:
  fixes f :: "'a  'a"
  assumes def: "F  ccpo.fixp Sup (≤) f"
  assumes mono: "monotone (≤) (≤) f"
  assumes adm: "ccpo.admissible Sup (≤) P"
  assumes bot: "P (Sup {})"
  assumes step: "x. P x  P (f x)"
  shows "P F"
  by (unfold def) (rule fixp_induct[OF adm mono bot step])

lemma induct_Sup_of_subsingleton_sets:
  assumes Ps: "subsingleton_set ( Ps)"
    and adm: "ccpo.admissible Sup (≤) P"
    and bot: "P (Sup {})"
    and step: "p x. p  Ps  x  p  P x"
  shows "P (Sup ( Ps))"
proof cases
  assume *: "( Ps) = {}" from bot show ?thesis unfolding * .
next
  assume *: "( Ps)  {}"
  show ?thesis
    by (intro ccpo.admissibleD[OF adm subsingleton_sets_imp_chain[OF Ps] *])
       (blast intro: step)
qed

lemma induct_Sup_of_subsingleton_sets_def:
  assumes F: "F  Sup ( Ps)"
  assumes Ps: "subsingleton_set ( Ps)"
    and adm: "ccpo.admissible Sup (≤) P"
    and bot: "P (Sup {})"
    and step: "p x. p  Ps  x  p  P x"
  shows "P F"
  unfolding F by (rule induct_Sup_of_subsingleton_sets; fact)

end

lemma flat_lub_empty: "flat_lub x {} = x"
  by (simp add: flat_lub_def)

lemma monotone_bind_option[partial_function_mono]:
  "monotone ord option_ord f  (a. monotone ord option_ord (λx. g x a)) 
    monotone ord option_ord (λx. Option.bind (f x) (g x))"
  by (fastforce simp: monotone_def flat_ord_def bind_eq_None_conv)

lemma (in ccpo) admissible_ord: "ccpo.admissible Sup (≤) (λx. x  b)"
  by (clarsimp simp add: ccpo.admissible_def intro!: ccpo_Sup_least)

ML_file ‹mutual_ccpo_recursion.ML›

setup (Mutual_CCPO_Rec.add_ccpo "option" Mutual_CCPO_Rec.synth_option
    #> Mutual_CCPO_Rec.add_ccpo "lfp" Mutual_CCPO_Rec.synth_lfp
    #> Mutual_CCPO_Rec.add_ccpo "gfp" Mutual_CCPO_Rec.synth_gfp)
  |> Context.theory_map

no_notation top ("")
no_notation bot ("")
no_notation sup (infixl "" 65)
no_notation inf (infixl "" 70)

hide_const (open) cont

end