Quelle Complete_Partial_Order.thy Sprache: Isabelle

(*  Title:      HOL/Complete_Partial_Order.thy
    Author:     Brian Huffman, Portland State University
    Author:     Alexander Krauss, TU Muenchen
*)

section \<open>Chain-complete partial orders and their fixpoints\<close>

theory Complete_Partial_Order
  imports Product_Type
begin

subsection \<open>Chains\<close>

text \<open>
  A chain is a totally-ordered set. Chains are parameterized over
  the order for maximal flexibility, since type classes are not enough.
\<close>

definition chain :: "('a \ 'a \ bool) \ 'a set \ bool"
  where "chain ord S \ (\x\S. \y\S. ord x y \ ord y x)"

lemma chainI:
  assumes "\x y. x \ S \ y \ S \ ord x y \ ord y x"
  shows "chain ord S"
  using assms unfolding chain_def by fast

lemma chainD:
  assumes "chain ord S" and "x \ S" and "y \ S"
  shows "ord x y \ ord y x"
  using assms unfolding chain_def by fast

lemma chainE:
  assumes "chain ord S" and "x \ S" and "y \ S"
  obtains "ord x y" | "ord y x"
  using assms unfolding chain_def by fast

lemma chain_empty: "chain ord {}"
  by (simp add: chain_def)

lemma chain_equality: "chain (=) A \ (\x\A. \y\A. x = y)"
  by (auto simp add: chain_def)

lemma chain_subset: "chain ord A \ B \ A \ chain ord B"
  by (rule chainI) (blast dest: chainD)

lemma chain_imageI:
  assumes chain: "chain le_a Y"
    and mono: "\x y. x \ Y \ y \ Y \ le_a x y \ le_b (f x) (f y)"
  shows "chain le_b (f ` Y)"
  by (blast intro: chainI dest: chainD[OF chain] mono)

subsection \<open>Chain-complete partial orders\<close>

text \<open>
  A \<open>ccpo\<close> has a least upper bound for any chain.  In particular, the
  empty set is a chain, so every \<open>ccpo\<close> must have a bottom element.
\<close>

class ccpo = order + Sup +
  assumes ccpo_Sup_upper: "chain (\) A \ x \ A \ x \ Sup A"
  assumes ccpo_Sup_least: "chain (\) A \ (\x. x \ A \ x \ z) \ Sup A \ z"
begin

lemma chain_singleton: "Complete_Partial_Order.chain (\) {x}"
  by (rule chainI) simp

lemma ccpo_Sup_singleton [simp]: "\{x} = x"
  by (rule order.antisym) (auto intro: ccpo_Sup_least ccpo_Sup_upper simp add: chain_singleton)

subsection \<open>Transfinite iteration of a function\<close>

context notes [[inductive_internals]]
begin

inductive_set iterates :: "('a \ 'a) \ 'a set"
  for f :: "'a \ 'a"
  where
    step: "x \ iterates f \ f x \ iterates f"
  | Sup: "chain (\) M \ \x\M. x \ iterates f \ Sup M \ iterates f"

end

lemma iterates_le_f: "x \ iterates f \ monotone (\) (\) f \ x \ f x"
  by (induct x rule: iterates.induct)
    (force dest: monotoneD intro!: ccpo_Sup_upper ccpo_Sup_least)+

lemma chain_iterates:
  assumes f: "monotone (\) (\) f"
  shows "chain (\) (iterates f)" (is "chain _ ?C")
proof (rule chainI)
  fix x y
  assume "x \ ?C" "y \ ?C"
  then show "x \ y \ y \ x"
  proof (induct x arbitrary: y rule: iterates.induct)
    fix x y
    assume y: "y \ ?C"
      and IH: "\z. z \ ?C \ x \ z \ z \ x"
    from y show "f x \ y \ y \ f x"
    proof (induct y rule: iterates.induct)
      case (step y)
      with IH f show ?case by (auto dest: monotoneD)
    next
      case (Sup M)
      then have chM: "chain (\) M"
        and IH': "\z. z \ M \ f x \ z \ z \ f x" by auto
      show "f x \ Sup M \ Sup M \ f x"
      proof (cases "\z\M. f x \ z")
        case True
        then have "f x \ Sup M"
          by (blast intro: ccpo_Sup_upper[OF chM] order_trans)
        then show ?thesis ..
      next
        case False
        with IH' show ?thesis
          by (auto intro: ccpo_Sup_least[OF chM])
      qed
    qed
  next
    case (Sup M y)
    show ?case
    proof (cases "\x\M. y \ x")
      case True
      then have "y \ Sup M"
        by (blast intro: ccpo_Sup_upper[OF Sup(1)] order_trans)
      then show ?thesis ..
    next
      case False with Sup
      show ?thesis by (auto intro: ccpo_Sup_least)
    qed
  qed
qed

lemma bot_in_iterates: "Sup {} \ iterates f"
  by (auto intro: iterates.Sup simp add: chain_empty)

subsection \<open>Fixpoint combinator\<close>

definition fixp :: "('a \ 'a) \ 'a"
  where "fixp f = Sup (iterates f)"

lemma iterates_fixp:
  assumes f: "monotone (\) (\) f"
  shows "fixp f \ iterates f"
  unfolding fixp_def
  by (simp add: iterates.Sup chain_iterates f)

lemma fixp_unfold:
  assumes f: "monotone (\) (\) f"
  shows "fixp f = f (fixp f)"
proof (rule order.antisym)
  show "fixp f \ f (fixp f)"
    by (intro iterates_le_f iterates_fixp f)
  have "f (fixp f) \ Sup (iterates f)"
    by (intro ccpo_Sup_upper chain_iterates f iterates.step iterates_fixp)
  then show "f (fixp f) \ fixp f"
    by (simp only: fixp_def)
qed

lemma fixp_lowerbound:
  assumes f: "monotone (\) (\) f"
    and z: "f z \ z"
  shows "fixp f \ z"
  unfolding fixp_def
proof (rule ccpo_Sup_least[OF chain_iterates[OF f]])
  fix x
  assume "x \ iterates f"
  then show "x \ z"
  proof (induct x rule: iterates.induct)
    case (step x)
    from f \<open>x \<le> z\<close> have "f x \<le> f z" by (rule monotoneD)
    also note z
    finally show "f x \ z" .
  next
    case (Sup M)
    then show ?case
      by (auto intro: ccpo_Sup_least)
  qed
qed

end

subsection \<open>Fixpoint induction\<close>

setup \<open>Sign.map_naming (Name_Space.mandatory_path "ccpo")\<close>

definition admissible :: "('a set \ 'a) \ ('a \ 'a \ bool) \ ('a \ bool) \ bool"
  where "admissible lub ord P \ (\A. chain ord A \ A \ {} \ (\x\A. P x) \ P (lub A))"

lemma admissibleI:
  assumes "\A. chain ord A \ A \ {} \ \x\A. P x \ P (lub A)"
  shows "ccpo.admissible lub ord P"
  using assms unfolding ccpo.admissible_def by fast

lemma admissibleD:
  assumes "ccpo.admissible lub ord P"
  assumes "chain ord A"
  assumes "A \ {}"
  assumes "\x. x \ A \ P x"
  shows "P (lub A)"
  using assms by (auto simp: ccpo.admissible_def)

setup \<open>Sign.map_naming Name_Space.parent_path\<close>

lemma (in ccpo) fixp_induct:
  assumes adm: "ccpo.admissible Sup (\) P"
  assumes mono: "monotone (\) (\) f"
  assumes bot: "P (Sup {})"
  assumes step: "\x. P x \ P (f x)"
  shows "P (fixp f)"
  unfolding fixp_def
  using adm chain_iterates[OF mono]
proof (rule ccpo.admissibleD)
  show "iterates f \ {}"
    using bot_in_iterates by auto
next
  fix x
  assume "x \ iterates f"
  then show "P x"
  proof (induct rule: iterates.induct)
    case prems: (step x)
    from this(2) show ?case by (rule step)
  next
    case (Sup M)
    then show ?case by (cases "M = {}") (auto intro: step bot ccpo.admissibleD adm)
  qed
qed

lemma admissible_True: "ccpo.admissible lub ord (\x. True)"
  unfolding ccpo.admissible_def by simp

(*lemma admissible_False: "\<not> ccpo.admissible lub ord (\<lambda>x. False)"
unfolding ccpo.admissible_def chain_def by simp
*)
lemma admissible_const: "ccpo.admissible lub ord (\x. t)"
  by (auto intro: ccpo.admissibleI)

lemma admissible_conj:
  assumes "ccpo.admissible lub ord (\x. P x)"
  assumes "ccpo.admissible lub ord (\x. Q x)"
  shows "ccpo.admissible lub ord (\x. P x \ Q x)"
  using assms unfolding ccpo.admissible_def by simp

lemma admissible_all:
  assumes "\y. ccpo.admissible lub ord (\x. P x y)"
  shows "ccpo.admissible lub ord (\x. \y. P x y)"
  using assms unfolding ccpo.admissible_def by fast

lemma admissible_ball:
  assumes "\y. y \ A \ ccpo.admissible lub ord (\x. P x y)"
  shows "ccpo.admissible lub ord (\x. \y\A. P x y)"
  using assms unfolding ccpo.admissible_def by fast

lemma chain_compr: "chain ord A \ chain ord {x \ A. P x}"
  unfolding chain_def by fast

context ccpo
begin

lemma admissible_disj:
  fixes P Q :: "'a \ bool"
  assumes P: "ccpo.admissible Sup (\) (\x. P x)"
  assumes Q: "ccpo.admissible Sup (\) (\x. Q x)"
  shows "ccpo.admissible Sup (\) (\x. P x \ Q x)"
proof (rule ccpo.admissibleI)
  fix A :: "'a set"
  assume chain: "chain (\) A"
  assume A: "A \ {}" and P_Q: "\x\A. P x \ Q x"
  have "(\x\A. P x) \ (\x\A. \y\A. x \ y \ P y) \ (\x\A. Q x) \ (\x\A. \y\A. x \ y \ Q y)"
    (is "?P \ ?Q" is "?P1 \ ?P2 \ _")
  proof (rule disjCI)
    assume "\ ?Q"
    then consider "\x\A. \ Q x" | a where "a \ A" "\y\A. a \ y \ \ Q y"
      by blast
    then show ?P
    proof cases
      case 1
      with P_Q have "\x\A. P x" by blast
      with A show ?P by blast
    next
      case 2
      note a = \<open>a \<in> A\<close>
      show ?P
      proof
        from P_Q 2 have *: "\y\A. a \ y \ P y" by blast
        with a have "P a" by blast
        with a show ?P1 by blast
        show ?P2
        proof
          fix x
          assume x: "x \ A"
          with chain a show "\y\A. x \ y \ P y"
          proof (rule chainE)
            assume le: "a \ x"
            with * a x have "P x" by blast
            with x le show ?thesis by blast
          next
            assume "a \ x"
            with a \<open>P a\<close> show ?thesis by blast
          qed
        qed
      qed
    qed
  qed
  moreover
  have "Sup A = Sup {x \ A. P x}" if "\x. x\A \ \y\A. x \ y \ P y" for P
  proof (rule order.antisym)
    have chain_P: "chain (\) {x \ A. P x}"
      by (rule chain_compr [OF chain])
    show "Sup A \ Sup {x \ A. P x}"
    proof (rule ccpo_Sup_least [OF chain])
      show "\x. x \ A \ x \ \ {x \ A. P x}"
          by (blast intro: ccpo_Sup_upper[OF chain_P] order_trans dest: that)
      qed
    show "Sup {x \ A. P x} \ Sup A"
      apply (rule ccpo_Sup_least [OF chain_P])
      apply (simp add: ccpo_Sup_upper [OF chain])
      done
  qed
  ultimately
  consider "\x. x \ A \ P x" "Sup A = Sup {x \ A. P x}"
    | "\x. x \ A \ Q x" "Sup A = Sup {x \ A. Q x}"
    by blast
  then show "P (Sup A) \ Q (Sup A)"
  proof cases
    case 1
    then show ?thesis
      using ccpo.admissibleD [OF P chain_compr [OF chain]] by force
  next
    case 2
    then show ?thesis
      using ccpo.admissibleD [OF Q chain_compr [OF chain]] by force
  qed
qed

end

instance complete_lattice \<subseteq> ccpo
  by standard (fast intro: Sup_upper Sup_least)+

lemma lfp_eq_fixp:
  assumes mono: "mono f"
  shows "lfp f = fixp f"
proof (rule order.antisym)
  from mono have f': "monotone (\) (\) f"
    unfolding mono_def monotone_def .
  show "lfp f \ fixp f"
    by (rule lfp_lowerbound, subst fixp_unfold [OF f'], rule order_refl)
  show "fixp f \ lfp f"
    by (rule fixp_lowerbound [OF f']) (simp add: lfp_fixpoint [OF mono])
qed

hide_const (open) iterates fixp

end

quality100%

¤ Dauer der Verarbeitung: 0.9 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.