Theory Partial_Function

(* 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_defn
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 (≤) 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 (≤) (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 (≤) 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 order.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: order.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 (≤) S  finite S)
   ccpo.admissible Sup (≤) 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. fA. 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. fA. 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"
abbreviation "admissible  ccpo.admissible lub_fun le_fun"

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 adm: "ccpo.admissible lub_fun le_fun P"
    and bot: "P (λ_. lub {})"
    and step: "f. P (U f)  P (U (F f))"
  shows "P (U f)"
unfolding eq inverse
proof (rule ccpo.fixp_induct[OF ccpo adm])
  show "monotone le_fun le_fun (λf. U (F (C f)))"
    using mono by (auto simp: monotone_def fun_ord_def)
next
  show "P (lub_fun {})"
    by (auto simp: bot fun_lub_def)
next
  fix x
  assume "P x"
  then show "P (U (F (C x)))"
    using step[of "C x"] by (simp add: inverse)
qed


text Rules for termmono_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"

lemma tailrec_admissible:
  "ccpo.admissible (fun_lub (flat_lub c)) (fun_ord (flat_ord c))
     (λa. x. a x  c  P x (a x))"
proof(intro ccpo.admissibleI strip)
  fix A x
  assume chain: "Complete_Partial_Order.chain (fun_ord (flat_ord c)) A"
    and P [rule_format]: "fA. 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

lemma admissible_image:
  assumes pfun: "partial_function_definitions le lub"
  assumes adm: "ccpo.admissible lub le (P  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"
proof (rule ccpo.admissibleI)
  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: "xA. P x"
  have "(P  g) (lub (f ` A))" using adm ch'
  proof (rule ccpo.admissibleD)
    fix x assume "x  f ` A"
    with P_A show "(P  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

lemma admissible_fun:
  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))"
proof (rule ccpo.admissibleI)
  fix A :: "('b  'a) set"
  assume Q: "fA. x. Q x (f x)"
  assume ch: "chain (fun_ord le) A"
  assume "A  {}"
  hence non_empty: "a. {y. fA. 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))"
proof (rule ccpo.admissibleI)
  fix A :: "('a  'b option) set"
  assume ch: "chain option.le_fun A"
    and IH: "fA. x y. f x = Some y  P x y"
  from ch have ch': "x. chain option_ord {y. fA. 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. fA. y = f x}" by simp
    then have "fA. 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" termtailrec.fixp_fun
  termtailrec.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" termoption.fixp_fun
  termoption.mono_body @{thm option.fixp_rule_uc} @{thm option.fixp_induct_uc}
  (SOME @{thm fixp_induct_option})

hide_const (open) chain

end