Theory Partial_Function_Set

(* Title: Partial_Function_Set.thy
  Author: Andreas Lochbihler, ETH Zurich *)

theory Partial_Function_Set imports Main begin

subsection ‹Setup for ‹partial_function› for sets›

lemma (in complete_lattice) lattice_partial_function_definition:
  "partial_function_definitions (≤) Sup"
by(unfold_locales)(auto intro: Sup_upper Sup_least)

interpretation set: partial_function_definitions "(⊆)" Union
by(rule lattice_partial_function_definition)

lemma fun_lub_Sup: "fun_lub Sup = (Sup :: _ ⇒ _ :: complete_lattice)"
by(fastforce simp add: fun_lub_def fun_eq_iff Sup_fun_def intro: Sup_eqI SUP_upper SUP_least)

lemma set_admissible: "set.admissible (λf :: 'a ⇒ 'b set. ∀x y. y ∈ f x ⟶ P x y)"
by(rule ccpo.admissibleI)(auto simp add: fun_lub_Sup)

abbreviation "mono_set ≡ monotone (fun_ord (⊆)) (⊆)"

lemma fixp_induct_set_scott:
  fixes F :: "'c ⇒ 'c"
  and U :: "'c ⇒ 'b ⇒ 'a set"
  and C :: "('b ⇒ 'a set) ⇒ 'c"
  and P :: "'b ⇒ 'a ⇒ bool"
  and x and y
  assumes mono: "⋀x. mono_set (λf. U (F (C f)) x)"
  and eq: "f ≡ C (ccpo.fixp (fun_lub Sup) (fun_ord (≤)) (λf. U (F (C f))))"
  and inverse2: "⋀f. U (C f) = f"
  and step: "⋀f x y. ⟦ ⋀x y. y ∈ U f x ⟹ P x y; y ∈ U (F f) x ⟧ ⟹ P x y"
  and enforce_variable_ordering: "x = x"
  and elem: "y ∈ U f x"
  shows "P x y"
using step elem set.fixp_induct_uc[of U F C, OF mono eq inverse2 set_admissible, of P]
by blast


lemma fixp_Sup_le:
  defines "le ≡ ((≤) :: _ :: complete_lattice ⇒ _)"
  shows "ccpo.fixp Sup le = ccpo_class.fixp"
proof -
  have "class.ccpo Sup le (<)" unfolding le_def by unfold_locales
  thus ?thesis
    by(simp add: ccpo.fixp_def fixp_def ccpo.iterates_def iterates_def ccpo.iteratesp_def iteratesp_def fun_eq_iff le_def)
qed

lemma fun_ord_le: "fun_ord (≤) = (≤)"
by(auto simp add: fun_ord_def fun_eq_iff le_fun_def)

lemma fixp_induct_set:
  fixes F :: "'c ⇒ 'c"
  and U :: "'c ⇒ 'b ⇒ 'a set"
  and C :: "('b ⇒ 'a set) ⇒ 'c"
  and P :: "'b ⇒ 'a ⇒ bool"
  and x and y
  assumes mono: "⋀x. mono_set (λf. U (F (C f)) x)"
  and eq: "f ≡ C (ccpo.fixp (fun_lub Sup) (fun_ord (≤)) (λf. U (F (C f))))"
  and inverse2: "⋀f. U (C f) = f"

  and step: "⋀f' x y. ⟦ ⋀x. U f' x = U f' x; y ∈ U (F (C (inf (U f) (λx. {y. P x y})))) x ⟧ ⟹ P x y"
    ― ‹partial\_function requires a quantifier over f', so let's have a fake one›
  and elem: "y ∈ U f x"
  shows "P x y"
proof -
  from mono
  have mono': "mono (λf. U (F (C f)))"
    by(simp add: fun_ord_le mono_def le_fun_def)
  hence eq': "f ≡ C (lfp (λf. U (F (C f))))"
    using eq unfolding fun_ord_le fun_lub_Sup fixp_Sup_le by(simp add: lfp_eq_fixp)

  let ?f = "C (lfp (λf. U (F (C f))))"
  have step': "⋀x y. ⟦ y ∈ U (F (C (inf (U ?f) (λx. {y. P x y})))) x ⟧ ⟹ P x y"
    unfolding eq'[symmetric] by(rule step[OF refl])

  let ?P = "λx. {y. P x y}"
  from mono' have "lfp (λf. U (F (C f))) ≤ ?P"
    by(rule lfp_induct)(auto intro!: le_funI step' simp add: inverse2)
  with elem show ?thesis
    by(subst (asm) eq')(auto simp add: inverse2 le_fun_def)
qed

declaration ‹Partial_Function.init "set" @{term set.fixp_fun}
  @{term set.mono_body} @{thm set.fixp_rule_uc} @{thm set.fixp_induct_uc}
  (SOME @{thm fixp_induct_set})›

lemma [partial_function_mono]:
  shows insert_mono: "mono_set A ⟹ mono_set (λf. insert x (A f))"
  and UNION_mono: "⟦mono_set B; ⋀y. mono_set (λf. C y f)⟧ ⟹ mono_set (λf. ⋃y∈B f. C y f)"
  and set_bind_mono: "⟦mono_set B; ⋀y. mono_set (λf. C y f)⟧ ⟹ mono_set (λf. Set.bind (B f) (λy. C y f))"
  and Un_mono: "⟦ mono_set A; mono_set B ⟧ ⟹ mono_set (λf. A f ∪ B f)"
  and Int_mono: "⟦ mono_set A; mono_set B ⟧ ⟹ mono_set (λf. A f ∩ B f)"
  and Diff_mono1: "mono_set A ⟹ mono_set (λf. A f - X)"
  and image_mono: "mono_set A ⟹ mono_set (λf. g ` A f)"
  and vimage_mono: "mono_set A ⟹ mono_set (λf. g -` A f)"
unfolding bind_UNION by(fast intro!: monotoneI dest: monotoneD)+

partial_function (set) test :: "'a list ⇒ nat ⇒ bool ⇒ int set"
where
  "test xs i j = insert 4 (test [] 0 j ∪ test [] 1 True ∩ test [] 2 False - {5} ∪ uminus ` test [undefined] 0 True ∪ uminus -` test [] 1 False)"

interpretation coset: partial_function_definitions "(⊇)" Inter
by(rule complete_lattice.lattice_partial_function_definition[OF dual_complete_lattice])

lemma fun_lub_Inf: "fun_lub Inf = (Inf :: _ ⇒ _ :: complete_lattice)"
by(auto simp add: fun_lub_def fun_eq_iff Inf_fun_def intro: Inf_eqI INF_lower INF_greatest)

lemma fun_ord_ge: "fun_ord (≥) = (≥)"
by(auto simp add: fun_ord_def fun_eq_iff le_fun_def)

lemma coset_admissible: "coset.admissible (λf :: 'a ⇒ 'b set. ∀x y. P x y ⟶ y ∈ f x)"
by(rule ccpo.admissibleI)(auto simp add: fun_lub_Inf)

abbreviation "mono_coset ≡ monotone (fun_ord (⊇)) (⊇)"

lemma gfp_eq_fixp:
  fixes f :: "'a :: complete_lattice ⇒ 'a"
  assumes f: "monotone (≥) (≥) f"
  shows "gfp f = ccpo.fixp Inf (≥) f"
proof (rule antisym)
  from f have f': "mono f" by(simp add: mono_def monotone_def)

  interpret ccpo Inf "(≥)" "mk_less (≥) :: 'a ⇒ _"
    by(rule ccpo)(rule complete_lattice.lattice_partial_function_definition[OF dual_complete_lattice])
  show "ccpo.fixp Inf (≥) f ≤ gfp f"
    by(rule gfp_upperbound)(subst fixp_unfold[OF f], rule order_refl)

  show "gfp f ≤ ccpo.fixp Inf (≥) f"
    by(rule fixp_lowerbound[OF f])(subst gfp_unfold[OF f'], rule order_refl)
qed

lemma fixp_coinduct_set:
  fixes F :: "'c ⇒ 'c"
  and U :: "'c ⇒ 'b ⇒ 'a set"
  and C :: "('b ⇒ 'a set) ⇒ 'c"
  and P :: "'b ⇒ 'a ⇒ bool"
  and x and y
  assumes mono: "⋀x. mono_coset (λf. U (F (C f)) x)"
  and eq: "f ≡ C (ccpo.fixp (fun_lub Inter) (fun_ord (≥)) (λf. U (F (C f))))"
  and inverse2: "⋀f. U (C f) = f"

  and step: "⋀f' x y. ⟦ ⋀x. U f' x = U f' x; ¬ P x y ⟧ ⟹ y ∈ U (F (C (sup (λx. {y. ¬ P x y}) (U f)))) x"
    ― ‹partial\_function requires a quantifier over f', so let's have a fake one›
  and elem: "y ∉ U f x"
  shows "P x y"
using elem
proof(rule contrapos_np)
  have mono': "monotone (≥) (≥) (λf. U (F (C f)))"
    and mono'': "mono (λf. U (F (C f)))"
    using mono by(simp_all add: monotone_def fun_ord_def le_fun_def mono_def)
  hence eq': "U f = gfp (λf. U (F (C f)))"
    by(subst eq)(simp add: fun_lub_Inf fun_ord_ge gfp_eq_fixp inverse2)

  let ?P = "λx. {y. ¬ P x y}"
  have "?P ≤ gfp (λf. U (F (C f)))"
    using mono'' by(rule coinduct)(auto intro!:  le_funI dest: step[OF refl] simp add: eq')
  moreover
  assume "¬ P x y"
  ultimately show "y ∈ U f x" by(auto simp add: le_fun_def eq')
qed

declaration ‹Partial_Function.init "coset" @{term coset.fixp_fun}
  @{term coset.mono_body} @{thm coset.fixp_rule_uc} @{thm coset.fixp_induct_uc}
  (SOME @{thm fixp_coinduct_set})›

abbreviation "mono_set' ≡ monotone (fun_ord (⊇)) (⊇)"

lemma [partial_function_mono]:
  shows insert_mono': "mono_set' A ⟹ mono_set' (λf. insert x (A f))"
  and UNION_mono': "⟦mono_set' B; ⋀y. mono_set' (λf. C y f)⟧ ⟹ mono_set' (λf. ⋃y∈B f. C y f)"
  and set_bind_mono': "⟦mono_set' B; ⋀y. mono_set' (λf. C y f)⟧ ⟹ mono_set' (λf. Set.bind (B f) (λy. C y f))"
  and Un_mono': "⟦ mono_set' A; mono_set' B ⟧ ⟹ mono_set' (λf. A f ∪ B f)"
  and Int_mono': "⟦ mono_set' A; mono_set' B ⟧ ⟹ mono_set' (λf. A f ∩ B f)"
unfolding bind_UNION by(fast intro!: monotoneI dest: monotoneD)+

context begin
private partial_function (coset) test2 :: "nat ⇒ nat set"
where "test2 x = insert x (test2 (Suc x))"

private lemma test2_coinduct:
  assumes "P x y"
  and *: "⋀x y. P x y ⟹ y = x ∨ (P (Suc x) y ∨ y ∈ test2 (Suc x))"
  shows "y ∈ test2 x"
using ‹P x y›
apply(rule contrapos_pp)
apply(erule test2.raw_induct[rotated])
apply(simp add: *)
done

end

end