# Theory Partial_Function

theory Partial_Function
imports Complete_Partial_Order Option
```(* Title:    HOL/Partial_Function.thy
Author:   Alexander Krauss, TU Muenchen
*)

section ‹Partial Function Definitions›

theory Partial_Function
imports Complete_Partial_Order Option
keywords "partial_function" :: thy_decl
begin

named_theorems partial_function_mono "monotonicity rules for partial function definitions"
ML_file "Tools/Function/partial_function.ML"

lemma (in ccpo) in_chain_finite:
assumes "Complete_Partial_Order.chain op ≤ A" "finite A" "A ≠ {}"
shows "⨆A ∈ A"
using assms(2,1,3)
proof induction
case empty thus ?case by simp
next
case (insert x A)
note chain = ‹Complete_Partial_Order.chain op ≤ (insert x A)›
show ?case
proof(cases "A = {}")
case True thus ?thesis by simp
next
case False
from chain have chain': "Complete_Partial_Order.chain op ≤ A"
by(rule chain_subset) blast
hence "⨆A ∈ A" using False by(rule insert.IH)
show ?thesis
proof(cases "x ≤ ⨆A")
case True
have "⨆insert x A ≤ ⨆A" using chain
by(rule ccpo_Sup_least)(auto simp add: True intro: ccpo_Sup_upper[OF chain'])
hence "⨆insert x A = ⨆A"
by(rule antisym)(blast intro: ccpo_Sup_upper[OF chain] ccpo_Sup_least[OF chain'])
with ‹⨆A ∈ A› show ?thesis by simp
next
case False
with chainD[OF chain, of x "⨆A"] ‹⨆A ∈ A›
have "⨆insert x A = x"
by(auto intro: antisym ccpo_Sup_least[OF chain] order_trans[OF ccpo_Sup_upper[OF chain']] ccpo_Sup_upper[OF chain])
thus ?thesis by simp
qed
qed
qed

lemma (in ccpo) admissible_chfin:
"(∀S. Complete_Partial_Order.chain op ≤ S ⟶ finite S)
⟹ ccpo.admissible Sup op ≤ P"
using in_chain_finite by (blast intro: ccpo.admissibleI)

subsection ‹Axiomatic setup›

text ‹This techical locale constains the requirements for function
definitions with ccpo fixed points.›

definition "fun_ord ord f g ⟷ (∀x. ord (f x) (g x))"
definition "fun_lub L A = (λx. L {y. ∃f∈A. y = f x})"
definition "img_ord f ord = (λx y. ord (f x) (f y))"
definition "img_lub f g Lub = (λA. g (Lub (f ` A)))"

lemma chain_fun:
assumes A: "chain (fun_ord ord) A"
shows "chain ord {y. ∃f∈A. y = f a}" (is "chain ord ?C")
proof (rule chainI)
fix x y assume "x ∈ ?C" "y ∈ ?C"
then obtain f g where fg: "f ∈ A" "g ∈ A"
and [simp]: "x = f a" "y = g a" by blast
from chainD[OF A fg]
show "ord x y ∨ ord y x" unfolding fun_ord_def by auto
qed

lemma call_mono[partial_function_mono]: "monotone (fun_ord ord) ord (λf. f t)"
by (rule monotoneI) (auto simp: fun_ord_def)

lemma let_mono[partial_function_mono]:
"(⋀x. monotone orda ordb (λf. b f x))
⟹ monotone orda ordb (λf. Let t (b f))"
by (simp add: Let_def)

lemma if_mono[partial_function_mono]: "monotone orda ordb F
⟹ monotone orda ordb G
⟹ monotone orda ordb (λf. if c then F f else G f)"
unfolding monotone_def by simp

definition "mk_less R = (λx y. R x y ∧ ¬ R y x)"

locale partial_function_definitions =
fixes leq :: "'a ⇒ 'a ⇒ bool"
fixes lub :: "'a set ⇒ 'a"
assumes leq_refl: "leq x x"
assumes leq_trans: "leq x y ⟹ leq y z ⟹ leq x z"
assumes leq_antisym: "leq x y ⟹ leq y x ⟹ x = y"
assumes lub_upper: "chain leq A ⟹ x ∈ A ⟹ leq x (lub A)"
assumes lub_least: "chain leq A ⟹ (⋀x. x ∈ A ⟹ leq x z) ⟹ leq (lub A) z"

lemma partial_function_lift:
assumes "partial_function_definitions ord lb"
shows "partial_function_definitions (fun_ord ord) (fun_lub lb)" (is "partial_function_definitions ?ordf ?lubf")
proof -
interpret partial_function_definitions ord lb by fact

show ?thesis
proof
fix x show "?ordf x x"
unfolding fun_ord_def by (auto simp: leq_refl)
next
fix x y z assume "?ordf x y" "?ordf y z"
thus "?ordf x z" unfolding fun_ord_def
by (force dest: leq_trans)
next
fix x y assume "?ordf x y" "?ordf y x"
thus "x = y" unfolding fun_ord_def
by (force intro!: dest: leq_antisym)
next
fix A f assume f: "f ∈ A" and A: "chain ?ordf A"
thus "?ordf f (?lubf A)"
unfolding fun_lub_def fun_ord_def
by (blast intro: lub_upper chain_fun[OF A] f)
next
fix A :: "('b ⇒ 'a) set" and g :: "'b ⇒ 'a"
assume A: "chain ?ordf A" and g: "⋀f. f ∈ A ⟹ ?ordf f g"
show "?ordf (?lubf A) g" unfolding fun_lub_def fun_ord_def
by (blast intro: lub_least chain_fun[OF A] dest: g[unfolded fun_ord_def])
qed
qed

lemma ccpo: assumes "partial_function_definitions ord lb"
shows "class.ccpo lb ord (mk_less ord)"
using assms unfolding partial_function_definitions_def mk_less_def
by unfold_locales blast+

lemma partial_function_image:
assumes "partial_function_definitions ord Lub"
assumes inj: "⋀x y. f x = f y ⟹ x = y"
assumes inv: "⋀x. f (g x) = x"
shows "partial_function_definitions (img_ord f ord) (img_lub f g Lub)"
proof -
let ?iord = "img_ord f ord"
let ?ilub = "img_lub f g Lub"

interpret partial_function_definitions ord Lub by fact
show ?thesis
proof
fix A x assume "chain ?iord A" "x ∈ A"
then have "chain ord (f ` A)" "f x ∈ f ` A"
by (auto simp: img_ord_def intro: chainI dest: chainD)
thus "?iord x (?ilub A)"
unfolding inv img_lub_def img_ord_def by (rule lub_upper)
next
fix A x assume "chain ?iord A"
and 1: "⋀z. z ∈ A ⟹ ?iord z x"
then have "chain ord (f ` A)"
by (auto simp: img_ord_def intro: chainI dest: chainD)
thus "?iord (?ilub A) x"
unfolding inv img_lub_def img_ord_def
by (rule lub_least) (auto dest: 1[unfolded img_ord_def])
qed (auto simp: img_ord_def intro: leq_refl dest: leq_trans leq_antisym inj)
qed

context partial_function_definitions
begin

abbreviation "le_fun ≡ fun_ord leq"
abbreviation "lub_fun ≡ fun_lub lub"
abbreviation "fixp_fun ≡ ccpo.fixp lub_fun le_fun"
abbreviation "mono_body ≡ monotone le_fun leq"

text ‹Interpret manually, to avoid flooding everything with facts about
orders›

lemma ccpo: "class.ccpo lub_fun le_fun (mk_less le_fun)"
apply (rule ccpo)
apply (rule partial_function_lift)
apply (rule partial_function_definitions_axioms)
done

text ‹The crucial fixed-point theorem›

lemma mono_body_fixp:
"(⋀x. mono_body (λf. F f x)) ⟹ fixp_fun F = F (fixp_fun F)"
by (rule ccpo.fixp_unfold[OF ccpo]) (auto simp: monotone_def fun_ord_def)

text ‹Version with curry/uncurry combinators, to be used by package›

lemma fixp_rule_uc:
fixes F :: "'c ⇒ 'c" and
U :: "'c ⇒ 'b ⇒ 'a" and
C :: "('b ⇒ 'a) ⇒ 'c"
assumes mono: "⋀x. mono_body (λf. U (F (C f)) x)"
assumes eq: "f ≡ C (fixp_fun (λf. U (F (C f))))"
assumes inverse: "⋀f. C (U f) = f"
shows "f = F f"
proof -
have "f = C (fixp_fun (λf. U (F (C f))))" by (simp add: eq)
also have "... = C (U (F (C (fixp_fun (λf. U (F (C f)))))))"
by (subst mono_body_fixp[of "%f. U (F (C f))", OF mono]) (rule refl)
also have "... = F (C (fixp_fun (λf. U (F (C f)))))" by (rule inverse)
also have "... = F f" by (simp add: eq)
finally show "f = F f" .
qed

text ‹Fixpoint induction rule›

lemma fixp_induct_uc:
fixes F :: "'c ⇒ 'c"
and U :: "'c ⇒ 'b ⇒ 'a"
and C :: "('b ⇒ 'a) ⇒ 'c"
and P :: "('b ⇒ 'a) ⇒ bool"
assumes mono: "⋀x. mono_body (λf. U (F (C f)) x)"
and eq: "f ≡ C (fixp_fun (λf. U (F (C f))))"
and inverse: "⋀f. U (C f) = f"
and bot: "P (λ_. lub {})"
and step: "⋀f. P (U f) ⟹ P (U (F f))"
shows "P (U f)"
unfolding eq inverse
apply (rule ccpo.fixp_induct[OF ccpo adm])
apply (insert mono, auto simp: monotone_def fun_ord_def bot fun_lub_def)[2]
apply (rule_tac f5="C x" in step)
apply (simp add: inverse)
done

text ‹Rules for @{term mono_body}:›

lemma const_mono[partial_function_mono]: "monotone ord leq (λf. c)"
by (rule monotoneI) (rule leq_refl)

end

subsection ‹Flat interpretation: tailrec and option›

definition
"flat_ord b x y ⟷ x = b ∨ x = y"

definition
"flat_lub b A = (if A ⊆ {b} then b else (THE x. x ∈ A - {b}))"

lemma flat_interpretation:
"partial_function_definitions (flat_ord b) (flat_lub b)"
proof
fix A x assume 1: "chain (flat_ord b) A" "x ∈ A"
show "flat_ord b x (flat_lub b A)"
proof cases
assume "x = b"
thus ?thesis by (simp add: flat_ord_def)
next
assume "x ≠ b"
with 1 have "A - {b} = {x}"
by (auto elim: chainE simp: flat_ord_def)
then have "flat_lub b A = x"
by (auto simp: flat_lub_def)
thus ?thesis by (auto simp: flat_ord_def)
qed
next
fix A z assume A: "chain (flat_ord b) A"
and z: "⋀x. x ∈ A ⟹ flat_ord b x z"
show "flat_ord b (flat_lub b A) z"
proof cases
assume "A ⊆ {b}"
thus ?thesis
by (auto simp: flat_lub_def flat_ord_def)
next
assume nb: "¬ A ⊆ {b}"
then obtain y where y: "y ∈ A" "y ≠ b" by auto
with A have "A - {b} = {y}"
by (auto elim: chainE simp: flat_ord_def)
with nb have "flat_lub b A = y"
by (auto simp: flat_lub_def)
with z y show ?thesis by auto
qed
qed (auto simp: flat_ord_def)

lemma flat_ordI: "(x ≠ a ⟹ x = y) ⟹ flat_ord a x y"
by(auto simp add: flat_ord_def)

lemma flat_ord_antisym: "⟦ flat_ord a x y; flat_ord a y x ⟧ ⟹ x = y"
by(auto simp add: flat_ord_def)

lemma antisymp_flat_ord: "antisymp (flat_ord a)"
by(rule antisympI)(auto dest: flat_ord_antisym)

interpretation tailrec:
partial_function_definitions "flat_ord undefined" "flat_lub undefined"
rewrites "flat_lub undefined {} ≡ undefined"
by (rule flat_interpretation)(simp add: flat_lub_def)

interpretation option:
partial_function_definitions "flat_ord None" "flat_lub None"
rewrites "flat_lub None {} ≡ None"
by (rule flat_interpretation)(simp add: flat_lub_def)

abbreviation "tailrec_ord ≡ flat_ord undefined"
abbreviation "mono_tailrec ≡ monotone (fun_ord tailrec_ord) tailrec_ord"

"ccpo.admissible (fun_lub (flat_lub c)) (fun_ord (flat_ord c))
(λa. ∀x. a x ≠ c ⟶ P x (a x))"
fix A x
assume chain: "Complete_Partial_Order.chain (fun_ord (flat_ord c)) A"
and P [rule_format]: "∀f∈A. ∀x. f x ≠ c ⟶ P x (f x)"
and defined: "fun_lub (flat_lub c) A x ≠ c"
from defined obtain f where f: "f ∈ A" "f x ≠ c"
by(auto simp add: fun_lub_def flat_lub_def split: if_split_asm)
hence "P x (f x)" by(rule P)
moreover from chain f have "∀f' ∈ A. f' x = c ∨ f' x = f x"
by(auto 4 4 simp add: Complete_Partial_Order.chain_def flat_ord_def fun_ord_def)
hence "fun_lub (flat_lub c) A x = f x"
using f by(auto simp add: fun_lub_def flat_lub_def)
ultimately show "P x (fun_lub (flat_lub c) A x)" by simp
qed

lemma fixp_induct_tailrec:
fixes F :: "'c ⇒ 'c" and
U :: "'c ⇒ 'b ⇒ 'a" and
C :: "('b ⇒ 'a) ⇒ 'c" and
P :: "'b ⇒ 'a ⇒ bool" and
x :: "'b"
assumes mono: "⋀x. monotone (fun_ord (flat_ord c)) (flat_ord c) (λf. U (F (C f)) x)"
assumes eq: "f ≡ C (ccpo.fixp (fun_lub (flat_lub c)) (fun_ord (flat_ord c)) (λf. U (F (C f))))"
assumes inverse2: "⋀f. U (C f) = f"
assumes step: "⋀f x y. (⋀x y. U f x = y ⟹ y ≠ c ⟹ P x y) ⟹ U (F f) x = y ⟹ y ≠ c ⟹ P x y"
assumes result: "U f x = y"
assumes defined: "y ≠ c"
shows "P x y"
proof -
have "∀x y. U f x = y ⟶ y ≠ c ⟶ P x y"
by(rule partial_function_definitions.fixp_induct_uc[OF flat_interpretation, of _ U F C, OF mono eq inverse2])
(auto intro: step tailrec_admissible simp add: fun_lub_def flat_lub_def)
thus ?thesis using result defined by blast
qed

assumes pfun: "partial_function_definitions le lub"
assumes adm: "ccpo.admissible lub le (P o g)"
assumes inj: "⋀x y. f x = f y ⟹ x = y"
assumes inv: "⋀x. f (g x) = x"
shows "ccpo.admissible (img_lub f g lub) (img_ord f le) P"
fix A assume "chain (img_ord f le) A"
then have ch': "chain le (f ` A)"
by (auto simp: img_ord_def intro: chainI dest: chainD)
assume "A ≠ {}"
assume P_A: "∀x∈A. P x"
have "(P o g) (lub (f ` A))" using adm ch'
fix x assume "x ∈ f ` A"
with P_A show "(P o g) x" by (auto simp: inj[OF inv])
qed(simp add: ‹A ≠ {}›)
thus "P (img_lub f g lub A)" unfolding img_lub_def by simp
qed

assumes pfun: "partial_function_definitions le lub"
assumes adm: "⋀x. ccpo.admissible lub le (Q x)"
shows "ccpo.admissible  (fun_lub lub) (fun_ord le) (λf. ∀x. Q x (f x))"
fix A :: "('b ⇒ 'a) set"
assume Q: "∀f∈A. ∀x. Q x (f x)"
assume ch: "chain (fun_ord le) A"
assume "A ≠ {}"
hence non_empty: "⋀a. {y. ∃f∈A. y = f a} ≠ {}" by auto
show "∀x. Q x (fun_lub lub A x)"
unfolding fun_lub_def
by (rule allI, rule ccpo.admissibleD[OF adm chain_fun[OF ch] non_empty])
(auto simp: Q)
qed

abbreviation "option_ord ≡ flat_ord None"
abbreviation "mono_option ≡ monotone (fun_ord option_ord) option_ord"

lemma bind_mono[partial_function_mono]:
assumes mf: "mono_option B" and mg: "⋀y. mono_option (λf. C y f)"
shows "mono_option (λf. Option.bind (B f) (λy. C y f))"
proof (rule monotoneI)
fix f g :: "'a ⇒ 'b option" assume fg: "fun_ord option_ord f g"
with mf
have "option_ord (B f) (B g)" by (rule monotoneD[of _ _ _ f g])
then have "option_ord (Option.bind (B f) (λy. C y f)) (Option.bind (B g) (λy. C y f))"
unfolding flat_ord_def by auto
also from mg
have "⋀y'. option_ord (C y' f) (C y' g)"
by (rule monotoneD) (rule fg)
then have "option_ord (Option.bind (B g) (λy'. C y' f)) (Option.bind (B g) (λy'. C y' g))"
unfolding flat_ord_def by (cases "B g") auto
finally (option.leq_trans)
show "option_ord (Option.bind (B f) (λy. C y f)) (Option.bind (B g) (λy'. C y' g))" .
qed

lemma flat_lub_in_chain:
assumes ch: "chain (flat_ord b) A "
assumes lub: "flat_lub b A = a"
shows "a = b ∨ a ∈ A"
proof (cases "A ⊆ {b}")
case True
then have "flat_lub b A = b" unfolding flat_lub_def by simp
with lub show ?thesis by simp
next
case False
then obtain c where "c ∈ A" and "c ≠ b" by auto
{ fix z assume "z ∈ A"
from chainD[OF ch ‹c ∈ A› this] have "z = c ∨ z = b"
unfolding flat_ord_def using ‹c ≠ b› by auto }
with False have "A - {b} = {c}" by auto
with False have "flat_lub b A = c" by (auto simp: flat_lub_def)
with ‹c ∈ A› lub show ?thesis by simp
qed

lemma option_admissible: "option.admissible (%(f::'a ⇒ 'b option).
(∀x y. f x = Some y ⟶ P x y))"
fix A :: "('a ⇒ 'b option) set"
assume ch: "chain option.le_fun A"
and IH: "∀f∈A. ∀x y. f x = Some y ⟶ P x y"
from ch have ch': "⋀x. chain option_ord {y. ∃f∈A. y = f x}" by (rule chain_fun)
show "∀x y. option.lub_fun A x = Some y ⟶ P x y"
proof (intro allI impI)
fix x y assume "option.lub_fun A x = Some y"
from flat_lub_in_chain[OF ch' this[unfolded fun_lub_def]]
have "Some y ∈ {y. ∃f∈A. y = f x}" by simp
then have "∃f∈A. f x = Some y" by auto
with IH show "P x y" by auto
qed
qed

lemma fixp_induct_option:
fixes F :: "'c ⇒ 'c" and
U :: "'c ⇒ 'b ⇒ 'a option" and
C :: "('b ⇒ 'a option) ⇒ 'c" and
P :: "'b ⇒ 'a ⇒ bool"
assumes mono: "⋀x. mono_option (λf. U (F (C f)) x)"
assumes eq: "f ≡ C (ccpo.fixp (fun_lub (flat_lub None)) (fun_ord option_ord) (λf. U (F (C f))))"
assumes inverse2: "⋀f. U (C f) = f"
assumes step: "⋀f x y. (⋀x y. U f x = Some y ⟹ P x y) ⟹ U (F f) x = Some y ⟹ P x y"
assumes defined: "U f x = Some y"
shows "P x y"
using step defined option.fixp_induct_uc[of U F C, OF mono eq inverse2 option_admissible]
unfolding fun_lub_def flat_lub_def by(auto 9 2)

declaration ‹Partial_Function.init "tailrec" @{term tailrec.fixp_fun}
@{term tailrec.mono_body} @{thm tailrec.fixp_rule_uc} @{thm tailrec.fixp_induct_uc}
(SOME @{thm fixp_induct_tailrec[where c = undefined]})›

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

hide_const (open) chain

end
```