Quelle UpperPD.thy Sprache: Isabelle

(*  Title:      HOL/HOLCF/UpperPD.thy
    Author:     Brian Huffman
*)

section \<open>Upper powerdomain\<close>

theory UpperPD
imports Compact_Basis
begin

subsection \<open>Basis preorder\<close>

definition
  upper_le :: "'a::bifinite pd_basis \ 'a pd_basis \ bool" (infix \\\\ 50) where
  "upper_le = (\u v. \y\Rep_pd_basis v. \x\Rep_pd_basis u. x \ y)"

lemma upper_le_refl [simp]: "t \\ t"
unfolding upper_le_def by fast

lemma upper_le_trans: "\t \\ u; u \\ v\ \ t \\ v"
unfolding upper_le_def
apply (rule ballI)
apply (drule (1) bspec, erule bexE)
apply (drule (1) bspec, erule bexE)
apply (erule rev_bexI)
apply (erule (1) below_trans)
done

interpretation upper_le: preorder upper_le
by (rule preorder.intro, rule upper_le_refl, rule upper_le_trans)

lemma upper_le_minimal [simp]: "PDUnit compact_bot \\ t"
unfolding upper_le_def Rep_PDUnit by simp

lemma PDUnit_upper_mono: "x \ y \ PDUnit x \\ PDUnit y"
unfolding upper_le_def Rep_PDUnit by simp

lemma PDPlus_upper_mono: "\s \\ t; u \\ v\ \ PDPlus s u \\ PDPlus t v"
unfolding upper_le_def Rep_PDPlus by fast

lemma PDPlus_upper_le: "PDPlus t u \\ t"
unfolding upper_le_def Rep_PDPlus by fast

lemma upper_le_PDUnit_PDUnit_iff [simp]:
  "(PDUnit a \\ PDUnit b) = (a \ b)"
unfolding upper_le_def Rep_PDUnit by fast

lemma upper_le_PDPlus_PDUnit_iff:
  "(PDPlus t u \\ PDUnit a) = (t \\ PDUnit a \ u \\ PDUnit a)"
unfolding upper_le_def Rep_PDPlus Rep_PDUnit by fast

lemma upper_le_PDPlus_iff: "(t \\ PDPlus u v) = (t \\ u \ t \\ v)"
unfolding upper_le_def Rep_PDPlus by fast

lemma upper_le_induct [induct set: upper_le]:
  assumes le: "t \\ u"
  assumes 1: "\a b. a \ b \ P (PDUnit a) (PDUnit b)"
  assumes 2: "\t u a. P t (PDUnit a) \ P (PDPlus t u) (PDUnit a)"
  assumes 3: "\t u v. \P t u; P t v\ \ P t (PDPlus u v)"
  shows "P t u"
  using le
proof (induct u arbitrary: t rule: pd_basis_induct)
  case (PDUnit a)
  then show ?case
  proof (induct t rule: pd_basis_induct)
    case PDUnit
    then show ?case by (simp add: 1)
  next
    case (PDPlus t u)
    from PDPlus(3) consider (t) "t \\ PDUnit a" | (u) "u \\ PDUnit a"
      by (auto simp: upper_le_PDPlus_PDUnit_iff)
    then show ?case
    proof cases
      case t
      then have "P t (PDUnit a)" by (rule PDPlus(1))
      then show ?thesis by (rule 2)
    next
      case u
      then have "P u (PDUnit a)" by (rule PDPlus(2))
      then have "P (PDPlus u t) (PDUnit a)" by (rule 2)
      then show ?thesis by (simp only: PDPlus_commute)
    qed
  qed
next
  case (PDPlus t t' u)
  then show ?case by (simp add: upper_le_PDPlus_iff 3)
qed

subsection \<open>Type definition\<close>

typedef 'a::bifinite upper_pd (\(\notation=\postfix upper_pd\\'(_')\)\) =
  "{S::'a pd_basis set. upper_le.ideal S}"
by (rule upper_le.ex_ideal)

instantiation upper_pd :: (bifinite) below
begin

definition
  "x \ y \ Rep_upper_pd x \ Rep_upper_pd y"

instance ..
end

instance upper_pd :: (bifinite) po
using type_definition_upper_pd below_upper_pd_def
by (rule upper_le.typedef_ideal_po)

instance upper_pd :: (bifinite) cpo
using type_definition_upper_pd below_upper_pd_def
by (rule upper_le.typedef_ideal_cpo)

definition
  upper_principal :: "'a::bifinite pd_basis \ 'a upper_pd" where
  "upper_principal t = Abs_upper_pd {u. u \\ t}"

interpretation upper_pd:
  ideal_completion upper_le upper_principal Rep_upper_pd
using type_definition_upper_pd below_upper_pd_def
using upper_principal_def pd_basis_countable
by (rule upper_le.typedef_ideal_completion)

text \<open>Upper powerdomain is pointed\<close>

lemma upper_pd_minimal: "upper_principal (PDUnit compact_bot) \ ys"
by (induct ys rule: upper_pd.principal_induct, simp, simp)

instance upper_pd :: (bifinite) pcpo
by intro_classes (fast intro: upper_pd_minimal)

lemma inst_upper_pd_pcpo: "\ = upper_principal (PDUnit compact_bot)"
by (rule upper_pd_minimal [THEN bottomI, symmetric])

subsection \<open>Monadic unit and plus\<close>

definition
  upper_unit :: "'a::bifinite \ 'a upper_pd" where
  "upper_unit = compact_basis.extension (\a. upper_principal (PDUnit a))"

definition
  upper_plus :: "'a::bifinite upper_pd \ 'a upper_pd \ 'a upper_pd" where
  "upper_plus = upper_pd.extension (\t. upper_pd.extension (\u.
      upper_principal (PDPlus t u)))"

abbreviation
  upper_add :: "'a::bifinite upper_pd \ 'a upper_pd \ 'a upper_pd"
    (infixl \<open>\<union>\<sharp>\<close> 65) where
  "xs \\ ys == upper_plus\xs\ys"

syntax
  "_upper_pd" :: "args \ logic" (\(\indent=1 notation=\mixfix upper_pd enumeration\\{_}\)\)
translations
  "{x,xs}\" == "{x}\ \\ {xs}\"
  "{x}\" == "CONST upper_unit\x"

lemma upper_unit_Rep_compact_basis [simp]:
  "{Rep_compact_basis a}\ = upper_principal (PDUnit a)"
unfolding upper_unit_def
by (simp add: compact_basis.extension_principal PDUnit_upper_mono)

lemma upper_plus_principal [simp]:
  "upper_principal t \\ upper_principal u = upper_principal (PDPlus t u)"
unfolding upper_plus_def
by (simp add: upper_pd.extension_principal
    upper_pd.extension_mono PDPlus_upper_mono)

interpretation upper_add: semilattice upper_add proof
  fix xs ys zs :: "'a upper_pd"
  show "(xs \\ ys) \\ zs = xs \\ (ys \\ zs)"
    apply (induct xs rule: upper_pd.principal_induct, simp)
    apply (induct ys rule: upper_pd.principal_induct, simp)
    apply (induct zs rule: upper_pd.principal_induct, simp)
    apply (simp add: PDPlus_assoc)
    done
  show "xs \\ ys = ys \\ xs"
    apply (induct xs rule: upper_pd.principal_induct, simp)
    apply (induct ys rule: upper_pd.principal_induct, simp)
    apply (simp add: PDPlus_commute)
    done
  show "xs \\ xs = xs"
    apply (induct xs rule: upper_pd.principal_induct, simp)
    apply (simp add: PDPlus_absorb)
    done
qed

lemmas upper_plus_assoc = upper_add.assoc
lemmas upper_plus_commute = upper_add.commute
lemmas upper_plus_absorb = upper_add.idem
lemmas upper_plus_left_commute = upper_add.left_commute
lemmas upper_plus_left_absorb = upper_add.left_idem

text \<open>Useful for \<open>simp add: upper_plus_ac\<close>\<close>
lemmas upper_plus_ac =
  upper_plus_assoc upper_plus_commute upper_plus_left_commute

text \<open>Useful for \<open>simp only: upper_plus_aci\<close>\<close>
lemmas upper_plus_aci =
  upper_plus_ac upper_plus_absorb upper_plus_left_absorb

lemma upper_plus_below1: "xs \\ ys \ xs"
apply (induct xs rule: upper_pd.principal_induct, simp)
apply (induct ys rule: upper_pd.principal_induct, simp)
apply (simp add: PDPlus_upper_le)
done

lemma upper_plus_below2: "xs \\ ys \ ys"
by (subst upper_plus_commute, rule upper_plus_below1)

lemma upper_plus_greatest: "\xs \ ys; xs \ zs\ \ xs \ ys \\ zs"
apply (subst upper_plus_absorb [of xs, symmetric])
apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
done

lemma upper_below_plus_iff [simp]:
  "xs \ ys \\ zs \ xs \ ys \ xs \ zs"
apply safe
apply (erule below_trans [OF _ upper_plus_below1])
apply (erule below_trans [OF _ upper_plus_below2])
apply (erule (1) upper_plus_greatest)
done

lemma upper_plus_below_unit_iff [simp]:
  "xs \\ ys \ {z}\ \ xs \ {z}\ \ ys \ {z}\"
apply (induct xs rule: upper_pd.principal_induct, simp)
apply (induct ys rule: upper_pd.principal_induct, simp)
apply (induct z rule: compact_basis.principal_induct, simp)
apply (simp add: upper_le_PDPlus_PDUnit_iff)
done

lemma upper_unit_below_iff [simp]: "{x}\ \ {y}\ \ x \ y"
apply (induct x rule: compact_basis.principal_induct, simp)
apply (induct y rule: compact_basis.principal_induct, simp)
apply simp
done

lemmas upper_pd_below_simps =
  upper_unit_below_iff
  upper_below_plus_iff
  upper_plus_below_unit_iff

lemma upper_unit_eq_iff [simp]: "{x}\ = {y}\ \ x = y"
unfolding po_eq_conv by simp

lemma upper_unit_strict [simp]: "{\}\ = \"
using upper_unit_Rep_compact_basis [of compact_bot]
by (simp add: inst_upper_pd_pcpo)

lemma upper_plus_strict1 [simp]: "\ \\ ys = \"
by (rule bottomI, rule upper_plus_below1)

lemma upper_plus_strict2 [simp]: "xs \\ \ = \"
by (rule bottomI, rule upper_plus_below2)

lemma upper_unit_bottom_iff [simp]: "{x}\ = \ \ x = \"
unfolding upper_unit_strict [symmetric] by (rule upper_unit_eq_iff)

lemma upper_plus_bottom_iff [simp]:
  "xs \\ ys = \ \ xs = \ \ ys = \"
apply (induct xs rule: upper_pd.principal_induct, simp)
apply (induct ys rule: upper_pd.principal_induct, simp)
apply (simp add: inst_upper_pd_pcpo upper_pd.principal_eq_iff
                 upper_le_PDPlus_PDUnit_iff)
done

lemma compact_upper_unit: "compact x \ compact {x}\"
by (auto dest!: compact_basis.compact_imp_principal)

lemma compact_upper_unit_iff [simp]: "compact {x}\ \ compact x"
apply (safe elim!: compact_upper_unit)
apply (simp only: compact_def upper_unit_below_iff [symmetric])
apply (erule adm_subst [OF cont_Rep_cfun2])
done

lemma compact_upper_plus [simp]:
  "\compact xs; compact ys\ \ compact (xs \\ ys)"
by (auto dest!: upper_pd.compact_imp_principal)

subsection \<open>Induction rules\<close>

lemma upper_pd_induct1:
  assumes P: "adm P"
  assumes unit: "\x. P {x}\"
  assumes insert: "\x ys. \P {x}\; P ys\ \ P ({x}\ \\ ys)"
  shows "P (xs::'a::bifinite upper_pd)"
proof (induct xs rule: upper_pd.principal_induct)
  have *: "P {Rep_compact_basis a}\" for a
    by (rule unit)
  show "P (upper_principal a)" for a
  proof (induct a rule: pd_basis_induct1)
    case (PDUnit a)
    with * show ?case
      by (simp only: upper_unit_Rep_compact_basis [symmetric])
  next
    case (PDPlus a t)
    with * have "P ({Rep_compact_basis a}\ \\ upper_principal t)"
      by (rule insert)
    then show ?case
      by (simp only: upper_unit_Rep_compact_basis [symmetric]
          upper_plus_principal [symmetric])
  qed
qed (rule P)

lemma upper_pd_induct [case_names adm upper_unit upper_plus, induct type: upper_pd]:
  assumes P: "adm P"
  assumes unit: "\x. P {x}\"
  assumes plus: "\xs ys. \P xs; P ys\ \ P (xs \\ ys)"
  shows "P (xs::'a::bifinite upper_pd)"
proof (induct xs rule: upper_pd.principal_induct)
  show "P (upper_principal a)" for a
  proof (induct a rule: pd_basis_induct)
    case PDUnit
    then show ?case
      by (simp only: upper_unit_Rep_compact_basis [symmetric] unit)
  next
    case PDPlus
    then show ?case
      by (simp only: upper_plus_principal [symmetric] plus)
  qed
qed (rule P)

subsection \<open>Monadic bind\<close>

definition
  upper_bind_basis ::
  "'a::bifinite pd_basis \ ('a \ 'b upper_pd) \ 'b::bifinite upper_pd" where
  "upper_bind_basis = fold_pd
    (\<lambda>a. \<Lambda> f. f\<cdot>(Rep_compact_basis a))
    (\<lambda>x y. \<Lambda> f. x\<cdot>f \<union>\<sharp> y\<cdot>f)"

lemma ACI_upper_bind:
  "semilattice (\x y. \ f. x\f \\ y\f)"
apply unfold_locales
apply (simp add: upper_plus_assoc)
apply (simp add: upper_plus_commute)
apply (simp add: eta_cfun)
done

lemma upper_bind_basis_simps [simp]:
  "upper_bind_basis (PDUnit a) =
    (\<Lambda> f. f\<cdot>(Rep_compact_basis a))"
  "upper_bind_basis (PDPlus t u) =
    (\<Lambda> f. upper_bind_basis t\<cdot>f \<union>\<sharp> upper_bind_basis u\<cdot>f)"
unfolding upper_bind_basis_def
apply -
apply (rule fold_pd_PDUnit [OF ACI_upper_bind])
apply (rule fold_pd_PDPlus [OF ACI_upper_bind])
done

lemma upper_bind_basis_mono:
  "t \\ u \ upper_bind_basis t \ upper_bind_basis u"
unfolding cfun_below_iff
apply (erule upper_le_induct, safe)
apply (simp add: monofun_cfun)
apply (simp add: below_trans [OF upper_plus_below1])
apply simp
done

definition
  upper_bind :: "'a::bifinite upper_pd \ ('a \ 'b upper_pd) \ 'b::bifinite upper_pd" where
  "upper_bind = upper_pd.extension upper_bind_basis"

syntax
  "_upper_bind" :: "[logic, logic, logic] \ logic"
    (\<open>(\<open>indent=3 notation=\<open>binder upper_bind\<close>\<close>\<Union>\<sharp>_\<in>_./ _)\<close> [0, 0, 10] 10)

translations
  "\\x\xs. e" == "CONST upper_bind\xs\(\ x. e)"

lemma upper_bind_principal [simp]:
  "upper_bind\(upper_principal t) = upper_bind_basis t"
unfolding upper_bind_def
apply (rule upper_pd.extension_principal)
apply (erule upper_bind_basis_mono)
done

lemma upper_bind_unit [simp]:
  "upper_bind\{x}\\f = f\x"
by (induct x rule: compact_basis.principal_induct, simp, simp)

lemma upper_bind_plus [simp]:
  "upper_bind\(xs \\ ys)\f = upper_bind\xs\f \\ upper_bind\ys\f"
by (induct xs rule: upper_pd.principal_induct, simp,
    induct ys rule: upper_pd.principal_induct, simp, simp)

lemma upper_bind_strict [simp]: "upper_bind\\\f = f\\"
unfolding upper_unit_strict [symmetric] by (rule upper_bind_unit)

lemma upper_bind_bind:
  "upper_bind\(upper_bind\xs\f)\g = upper_bind\xs\(\ x. upper_bind\(f\x)\g)"
by (induct xs, simp_all)

subsection \<open>Map\<close>

definition
  upper_map :: "('a::bifinite \ 'b::bifinite) \ 'a upper_pd \ 'b upper_pd" where
  "upper_map = (\ f xs. upper_bind\xs\(\ x. {f\x}\))"

lemma upper_map_unit [simp]:
  "upper_map\f\{x}\ = {f\x}\"
unfolding upper_map_def by simp

lemma upper_map_plus [simp]:
  "upper_map\f\(xs \\ ys) = upper_map\f\xs \\ upper_map\f\ys"
unfolding upper_map_def by simp

lemma upper_map_bottom [simp]: "upper_map\f\\ = {f\\}\"
unfolding upper_map_def by simp

lemma upper_map_ident: "upper_map\(\ x. x)\xs = xs"
by (induct xs rule: upper_pd_induct, simp_all)

lemma upper_map_ID: "upper_map\ID = ID"
by (simp add: cfun_eq_iff ID_def upper_map_ident)

lemma upper_map_map:
  "upper_map\f\(upper_map\g\xs) = upper_map\(\ x. f\(g\x))\xs"
by (induct xs rule: upper_pd_induct, simp_all)

lemma upper_bind_map:
  "upper_bind\(upper_map\f\xs)\g = upper_bind\xs\(\ x. g\(f\x))"
by (simp add: upper_map_def upper_bind_bind)

lemma upper_map_bind:
  "upper_map\f\(upper_bind\xs\g) = upper_bind\xs\(\ x. upper_map\f\(g\x))"
by (simp add: upper_map_def upper_bind_bind)

lemma ep_pair_upper_map: "ep_pair e p \ ep_pair (upper_map\e) (upper_map\p)"
apply standard
apply (induct_tac x rule: upper_pd_induct, simp_all add: ep_pair.e_inverse)
apply (induct_tac y rule: upper_pd_induct)
apply (simp_all add: ep_pair.e_p_below monofun_cfun del: upper_below_plus_iff)
done

lemma deflation_upper_map: "deflation d \ deflation (upper_map\d)"
apply standard
apply (induct_tac x rule: upper_pd_induct, simp_all add: deflation.idem)
apply (induct_tac x rule: upper_pd_induct)
apply (simp_all add: deflation.below monofun_cfun del: upper_below_plus_iff)
done

(* FIXME: long proof! *)
lemma finite_deflation_upper_map:
  assumes "finite_deflation d" shows "finite_deflation (upper_map\d)"
proof (rule finite_deflation_intro)
  interpret d: finite_deflation d by fact
  from d.deflation_axioms show "deflation (upper_map\d)"
    by (rule deflation_upper_map)
  have "finite (range (\x. d\x))" by (rule d.finite_range)
  hence "finite (Rep_compact_basis -` range (\x. d\x))"
    by (rule finite_vimageI, simp add: inj_on_def Rep_compact_basis_inject)
  hence "finite (Pow (Rep_compact_basis -` range (\x. d\x)))" by simp
  hence "finite (Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\x. d\x))))"
    by (rule finite_vimageI, simp add: inj_on_def Rep_pd_basis_inject)
  hence *: "finite (upper_principal ` Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\x. d\x))))" by simp
  hence "finite (range (\xs. upper_map\d\xs))"
    apply (rule rev_finite_subset)
    apply clarsimp
    apply (induct_tac xs rule: upper_pd.principal_induct)
    apply (simp add: adm_mem_finite *)
    apply (rename_tac t, induct_tac t rule: pd_basis_induct)
    apply (simp only: upper_unit_Rep_compact_basis [symmetric] upper_map_unit)
    apply simp
    apply (subgoal_tac "\b. d\(Rep_compact_basis a) = Rep_compact_basis b")
    apply clarsimp
    apply (rule imageI)
    apply (rule vimageI2)
    apply (simp add: Rep_PDUnit)
    apply (rule range_eqI)
    apply (erule sym)
    apply (rule exI)
    apply (rule Abs_compact_basis_inverse [symmetric])
    apply (simp add: d.compact)
    apply (simp only: upper_plus_principal [symmetric] upper_map_plus)
    apply clarsimp
    apply (rule imageI)
    apply (rule vimageI2)
    apply (simp add: Rep_PDPlus)
    done
  thus "finite {xs. upper_map\d\xs = xs}"
    by (rule finite_range_imp_finite_fixes)
qed

subsection \<open>Upper powerdomain is bifinite\<close>

lemma approx_chain_upper_map:
  assumes "approx_chain a"
  shows "approx_chain (\i. upper_map\(a i))"
  using assms unfolding approx_chain_def
  by (simp add: lub_APP upper_map_ID finite_deflation_upper_map)

instance upper_pd :: (bifinite) bifinite
proof
  show "\(a::nat \ 'a upper_pd \ 'a upper_pd). approx_chain a"
    using bifinite [where 'a='a]
    by (fast intro!: approx_chain_upper_map)
qed

subsection \<open>Join\<close>

definition
  upper_join :: "'a::bifinite upper_pd upper_pd \ 'a upper_pd" where
  "upper_join = (\ xss. upper_bind\xss\(\ xs. xs))"

lemma upper_join_unit [simp]:
  "upper_join\{xs}\ = xs"
unfolding upper_join_def by simp

lemma upper_join_plus [simp]:
  "upper_join\(xss \\ yss) = upper_join\xss \\ upper_join\yss"
unfolding upper_join_def by simp

lemma upper_join_bottom [simp]: "upper_join\\ = \"
unfolding upper_join_def by simp

lemma upper_join_map_unit:
  "upper_join\(upper_map\upper_unit\xs) = xs"
by (induct xs rule: upper_pd_induct, simp_all)

lemma upper_join_map_join:
  "upper_join\(upper_map\upper_join\xsss) = upper_join\(upper_join\xsss)"
by (induct xsss rule: upper_pd_induct, simp_all)

lemma upper_join_map_map:
  "upper_join\(upper_map\(upper_map\f)\xss) =
   upper_map\<cdot>f\<cdot>(upper_join\<cdot>xss)"
by (induct xss rule: upper_pd_induct, simp_all)

end

quality100%

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