Quelle Partial_Function.thy Sprache: Isabelle

(* Title:    HOL/Partial_Function.thy
   Author:   Alexander Krauss, TU Muenchen
*)

section \<open>Partial Function Definitions\<close>

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 \<open>Tools/Function/partial_function.ML\<close>

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 = \<open>Complete_Partial_Order.chain (\<le>) (insert x A)\<close>
  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 \<open>\<Squnion>A \<in> A\<close> 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)
  \<Longrightarrow> ccpo.admissible Sup (\<le>) P"
using in_chain_finite by (blast intro: ccpo.admissibleI)

subsection \<open>Axiomatic setup\<close>

text \<open>This techical locale constains the requirements for function
  definitions with ccpo fixed points.\<close>

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))
  \<Longrightarrow> monotone orda ordb (\<lambda>f. Let t (b f))"
by (simp add: Let_def)

lemma if_mono[partial_function_mono]: "monotone orda ordb F
\<Longrightarrow> monotone orda ordb G
\<Longrightarrow> monotone orda ordb (\<lambda>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 \<open>Interpret manually, to avoid flooding everything with facts about
  orders\<close>

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 \<open>The crucial fixed-point theorem\<close>

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 \<open>Version with curry/uncurry combinators, to be used by package\<close>

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 \<open>Fixpoint induction rule\<close>

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 \<open>Rules for \<^term>\<open>mono_body\<close>:\<close>

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

end

subsection \<open>Flat interpretation: tailrec and option\<close>

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))
     (\<lambda>a. \<forall>x. a x \<noteq> c \<longrightarrow> 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]: "\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

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: "\x\A. 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: \<open>A \<noteq> {}\<close>)
  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: "\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 \<open>c \<in> A\<close> this] have "z = c \<or> z = b"
      unfolding flat_ord_def using \<open>c \<noteq> b\<close> 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 \<open>c \<in> A\<close> lub show ?thesis by simp
qed

lemma option_admissible: "option.admissible (%(f::'a \ 'b option).
  (\<forall>x y. f x = Some y \<longrightarrow> P x y))"
proof (rule ccpo.admissibleI)
  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 \<open>Partial_Function.init "tailrec" \<^term>\<open>tailrec.fixp_fun\<close>
  \<^term>\<open>tailrec.mono_body\<close> @{thm tailrec.fixp_rule_uc} @{thm tailrec.fixp_induct_uc}
  (SOME @{thm fixp_induct_tailrec[where c = undefined]})\<close>

declaration \<open>Partial_Function.init "option" \<^term>\<open>option.fixp_fun\<close>
  \<^term>\<open>option.mono_body\<close> @{thm option.fixp_rule_uc} @{thm option.fixp_induct_uc}
  (SOME @{thm fixp_induct_option})\<close>

hide_const (open) chain

end

quality98%

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.