Quelle LowerPD.thy Sprache: Isabelle

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

section \<open>Lower powerdomain\<close>

theory LowerPD
imports Compact_Basis
begin

subsection \<open>Basis preorder\<close>

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

lemma lower_le_refl [simp]: "t \\ t"
unfolding lower_le_def by fast

lemma lower_le_trans: "\t \\ u; u \\ v\ \ t \\ v"
unfolding lower_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 lower_le: preorder lower_le
by (rule preorder.intro, rule lower_le_refl, rule lower_le_trans)

lemma lower_le_minimal [simp]: "PDUnit compact_bot \\ t"
unfolding lower_le_def Rep_PDUnit
by (simp, rule Rep_pd_basis_nonempty [folded ex_in_conv])

lemma PDUnit_lower_mono: "x \ y \ PDUnit x \\ PDUnit y"
unfolding lower_le_def Rep_PDUnit by fast

lemma PDPlus_lower_mono: "\s \\ t; u \\ v\ \ PDPlus s u \\ PDPlus t v"
unfolding lower_le_def Rep_PDPlus by fast

lemma PDPlus_lower_le: "t \\ PDPlus t u"
unfolding lower_le_def Rep_PDPlus by fast

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

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

lemma lower_le_PDPlus_iff: "(PDPlus t u \\ v) = (t \\ v \ u \\ v)"
unfolding lower_le_def Rep_PDPlus by fast

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

subsection \<open>Type definition\<close>

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

instantiation lower_pd :: (bifinite) below
begin

definition
  "x \ y \ Rep_lower_pd x \ Rep_lower_pd y"

instance ..
end

instance lower_pd :: (bifinite) po
using type_definition_lower_pd below_lower_pd_def
by (rule lower_le.typedef_ideal_po)

instance lower_pd :: (bifinite) cpo
using type_definition_lower_pd below_lower_pd_def
by (rule lower_le.typedef_ideal_cpo)

definition
  lower_principal :: "'a::bifinite pd_basis \ 'a lower_pd" where
  "lower_principal t = Abs_lower_pd {u. u \\ t}"

interpretation lower_pd:
  ideal_completion lower_le lower_principal Rep_lower_pd
using type_definition_lower_pd below_lower_pd_def
using lower_principal_def pd_basis_countable
by (rule lower_le.typedef_ideal_completion)

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

lemma lower_pd_minimal: "lower_principal (PDUnit compact_bot) \ ys"
by (induct ys rule: lower_pd.principal_induct, simp, simp)

instance lower_pd :: (bifinite) pcpo
by intro_classes (fast intro: lower_pd_minimal)

lemma inst_lower_pd_pcpo: "\ = lower_principal (PDUnit compact_bot)"
by (rule lower_pd_minimal [THEN bottomI, symmetric])

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

definition
  lower_unit :: "'a::bifinite \ 'a lower_pd" where
  "lower_unit = compact_basis.extension (\a. lower_principal (PDUnit a))"

definition
  lower_plus :: "'a::bifinite lower_pd \ 'a lower_pd \ 'a lower_pd" where
  "lower_plus = lower_pd.extension (\t. lower_pd.extension (\u.
      lower_principal (PDPlus t u)))"

abbreviation
  lower_add :: "'a::bifinite lower_pd \ 'a lower_pd \ 'a lower_pd"
    (infixl \<open>\<union>\<flat>\<close> 65) where
  "xs \\ ys == lower_plus\xs\ys"

syntax
  "_lower_pd" :: "args \ logic" (\(\indent=1 notation=\mixfix lower_pd enumeration\\{_}\)\)
translations
  "{x,xs}\" == "{x}\ \\ {xs}\"
  "{x}\" == "CONST lower_unit\x"

lemma lower_unit_Rep_compact_basis [simp]:
  "{Rep_compact_basis a}\ = lower_principal (PDUnit a)"
unfolding lower_unit_def
by (simp add: compact_basis.extension_principal PDUnit_lower_mono)

lemma lower_plus_principal [simp]:
  "lower_principal t \\ lower_principal u = lower_principal (PDPlus t u)"
unfolding lower_plus_def
by (simp add: lower_pd.extension_principal
    lower_pd.extension_mono PDPlus_lower_mono)

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

lemmas lower_plus_assoc = lower_add.assoc
lemmas lower_plus_commute = lower_add.commute
lemmas lower_plus_absorb = lower_add.idem
lemmas lower_plus_left_commute = lower_add.left_commute
lemmas lower_plus_left_absorb = lower_add.left_idem

text \<open>Useful for \<open>simp add: lower_plus_ac\<close>\<close>
lemmas lower_plus_ac =
  lower_plus_assoc lower_plus_commute lower_plus_left_commute

text \<open>Useful for \<open>simp only: lower_plus_aci\<close>\<close>
lemmas lower_plus_aci =
  lower_plus_ac lower_plus_absorb lower_plus_left_absorb

lemma lower_plus_below1: "xs \ xs \\ ys"
apply (induct xs rule: lower_pd.principal_induct, simp)
apply (induct ys rule: lower_pd.principal_induct, simp)
apply (simp add: PDPlus_lower_le)
done

lemma lower_plus_below2: "ys \ xs \\ ys"
by (subst lower_plus_commute, rule lower_plus_below1)

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

lemma lower_plus_below_iff [simp]:
  "xs \\ ys \ zs \ xs \ zs \ ys \ zs"
apply safe
apply (erule below_trans [OF lower_plus_below1])
apply (erule below_trans [OF lower_plus_below2])
apply (erule (1) lower_plus_least)
done

lemma lower_unit_below_plus_iff [simp]:
  "{x}\ \ ys \\ zs \ {x}\ \ ys \ {x}\ \ zs"
apply (induct x rule: compact_basis.principal_induct, simp)
apply (induct ys rule: lower_pd.principal_induct, simp)
apply (induct zs rule: lower_pd.principal_induct, simp)
apply (simp add: lower_le_PDUnit_PDPlus_iff)
done

lemma lower_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 lower_pd_below_simps =
  lower_unit_below_iff
  lower_plus_below_iff
  lower_unit_below_plus_iff

lemma lower_unit_eq_iff [simp]: "{x}\ = {y}\ \ x = y"
by (simp add: po_eq_conv)

lemma lower_unit_strict [simp]: "{\}\ = \"
using lower_unit_Rep_compact_basis [of compact_bot]
by (simp add: inst_lower_pd_pcpo)

lemma lower_unit_bottom_iff [simp]: "{x}\ = \ \ x = \"
unfolding lower_unit_strict [symmetric] by (rule lower_unit_eq_iff)

lemma lower_plus_bottom_iff [simp]:
  "xs \\ ys = \ \ xs = \ \ ys = \"
apply safe
apply (rule bottomI, erule subst, rule lower_plus_below1)
apply (rule bottomI, erule subst, rule lower_plus_below2)
apply (rule lower_plus_absorb)
done

lemma lower_plus_strict1 [simp]: "\ \\ ys = ys"
apply (rule below_antisym [OF _ lower_plus_below2])
apply (simp add: lower_plus_least)
done

lemma lower_plus_strict2 [simp]: "xs \\ \ = xs"
apply (rule below_antisym [OF _ lower_plus_below1])
apply (simp add: lower_plus_least)
done

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

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

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

subsection \<open>Induction rules\<close>

lemma lower_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 lower_pd)"
proof (induct xs rule: lower_pd.principal_induct)
  have *: "P {Rep_compact_basis a}\" for a
    by (rule unit)
  show "P (lower_principal a)" for a
  proof (induct a rule: pd_basis_induct1)
    case PDUnit
    from * show ?case
      by (simp only: lower_unit_Rep_compact_basis [symmetric])
  next
    case (PDPlus a t)
    with * have "P ({Rep_compact_basis a}\ \\ lower_principal t)"
      by (rule insert)
    then show ?case
      by (simp only: lower_unit_Rep_compact_basis [symmetric] lower_plus_principal [symmetric])
  qed
qed (rule P)

lemma lower_pd_induct [case_names adm lower_unit lower_plus, induct type: lower_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 lower_pd)"
proof (induct xs rule: lower_pd.principal_induct)
  show "P (lower_principal a)" for a
  proof (induct a rule: pd_basis_induct)
    case PDUnit
    then show ?case
      by (simp only: lower_unit_Rep_compact_basis [symmetric] unit)
  next
    case PDPlus
    then show ?case
      by (simp only: lower_plus_principal [symmetric] plus)
  qed
qed (rule P)

subsection \<open>Monadic bind\<close>

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

lemma ACI_lower_bind:
  "semilattice (\x y. \ f. x\f \\ y\f)"
apply unfold_locales
apply (simp add: lower_plus_assoc)
apply (simp add: lower_plus_commute)
apply (simp add: eta_cfun)
done

lemma lower_bind_basis_simps [simp]:
  "lower_bind_basis (PDUnit a) =
    (\<Lambda> f. f\<cdot>(Rep_compact_basis a))"
  "lower_bind_basis (PDPlus t u) =
    (\<Lambda> f. lower_bind_basis t\<cdot>f \<union>\<flat> lower_bind_basis u\<cdot>f)"
unfolding lower_bind_basis_def
apply -
apply (rule fold_pd_PDUnit [OF ACI_lower_bind])
apply (rule fold_pd_PDPlus [OF ACI_lower_bind])
done

lemma lower_bind_basis_mono:
  "t \\ u \ lower_bind_basis t \ lower_bind_basis u"
unfolding cfun_below_iff
apply (erule lower_le_induct, safe)
apply (simp add: monofun_cfun)
apply (simp add: rev_below_trans [OF lower_plus_below1])
apply simp
done

definition
  lower_bind :: "'a::bifinite lower_pd \ ('a \ 'b lower_pd) \ 'b::bifinite lower_pd" where
  "lower_bind = lower_pd.extension lower_bind_basis"

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

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

lemma lower_bind_principal [simp]:
  "lower_bind\(lower_principal t) = lower_bind_basis t"
unfolding lower_bind_def
apply (rule lower_pd.extension_principal)
apply (erule lower_bind_basis_mono)
done

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

lemma lower_bind_plus [simp]:
  "lower_bind\(xs \\ ys)\f = lower_bind\xs\f \\ lower_bind\ys\f"
by (induct xs rule: lower_pd.principal_induct, simp,
    induct ys rule: lower_pd.principal_induct, simp, simp)

lemma lower_bind_strict [simp]: "lower_bind\\\f = f\\"
unfolding lower_unit_strict [symmetric] by (rule lower_bind_unit)

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

subsection \<open>Map\<close>

definition
  lower_map :: "('a::bifinite \ 'b::bifinite) \ 'a lower_pd \ 'b lower_pd" where
  "lower_map = (\ f xs. lower_bind\xs\(\ x. {f\x}\))"

lemma lower_map_unit [simp]:
  "lower_map\f\{x}\ = {f\x}\"
unfolding lower_map_def by simp

lemma lower_map_plus [simp]:
  "lower_map\f\(xs \\ ys) = lower_map\f\xs \\ lower_map\f\ys"
unfolding lower_map_def by simp

lemma lower_map_bottom [simp]: "lower_map\f\\ = {f\\}\"
unfolding lower_map_def by simp

lemma lower_map_ident: "lower_map\(\ x. x)\xs = xs"
by (induct xs rule: lower_pd_induct, simp_all)

lemma lower_map_ID: "lower_map\ID = ID"
by (simp add: cfun_eq_iff ID_def lower_map_ident)

lemma lower_map_map:
  "lower_map\f\(lower_map\g\xs) = lower_map\(\ x. f\(g\x))\xs"
by (induct xs rule: lower_pd_induct, simp_all)

lemma lower_bind_map:
  "lower_bind\(lower_map\f\xs)\g = lower_bind\xs\(\ x. g\(f\x))"
by (simp add: lower_map_def lower_bind_bind)

lemma lower_map_bind:
  "lower_map\f\(lower_bind\xs\g) = lower_bind\xs\(\ x. lower_map\f\(g\x))"
by (simp add: lower_map_def lower_bind_bind)

lemma ep_pair_lower_map: "ep_pair e p \ ep_pair (lower_map\e) (lower_map\p)"
apply standard
apply (induct_tac x rule: lower_pd_induct, simp_all add: ep_pair.e_inverse)
apply (induct_tac y rule: lower_pd_induct)
apply (simp_all add: ep_pair.e_p_below monofun_cfun del: lower_plus_below_iff)
done

lemma deflation_lower_map: "deflation d \ deflation (lower_map\d)"
apply standard
apply (induct_tac x rule: lower_pd_induct, simp_all add: deflation.idem)
apply (induct_tac x rule: lower_pd_induct)
apply (simp_all add: deflation.below monofun_cfun del: lower_plus_below_iff)
done

(* FIXME: long proof! *)
lemma finite_deflation_lower_map:
  assumes "finite_deflation d" shows "finite_deflation (lower_map\d)"
proof (rule finite_deflation_intro)
  interpret d: finite_deflation d by fact
  from d.deflation_axioms show "deflation (lower_map\d)"
    by (rule deflation_lower_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 (lower_principal ` Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\x. d\x))))" by simp
  hence "finite (range (\xs. lower_map\d\xs))"
    apply (rule rev_finite_subset)
    apply clarsimp
    apply (induct_tac xs rule: lower_pd.principal_induct)
    apply (simp add: adm_mem_finite *)
    apply (rename_tac t, induct_tac t rule: pd_basis_induct)
    apply (simp only: lower_unit_Rep_compact_basis [symmetric] lower_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: lower_plus_principal [symmetric] lower_map_plus)
    apply clarsimp
    apply (rule imageI)
    apply (rule vimageI2)
    apply (simp add: Rep_PDPlus)
    done
  thus "finite {xs. lower_map\d\xs = xs}"
    by (rule finite_range_imp_finite_fixes)
qed

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

lemma approx_chain_lower_map:
  assumes "approx_chain a"
  shows "approx_chain (\i. lower_map\(a i))"
  using assms unfolding approx_chain_def
  by (simp add: lub_APP lower_map_ID finite_deflation_lower_map)

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

subsection \<open>Join\<close>

definition
  lower_join :: "'a::bifinite lower_pd lower_pd \ 'a lower_pd" where
  "lower_join = (\ xss. lower_bind\xss\(\ xs. xs))"

lemma lower_join_unit [simp]:
  "lower_join\{xs}\ = xs"
unfolding lower_join_def by simp

lemma lower_join_plus [simp]:
  "lower_join\(xss \\ yss) = lower_join\xss \\ lower_join\yss"
unfolding lower_join_def by simp

lemma lower_join_bottom [simp]: "lower_join\\ = \"
unfolding lower_join_def by simp

lemma lower_join_map_unit:
  "lower_join\(lower_map\lower_unit\xs) = xs"
by (induct xs rule: lower_pd_induct, simp_all)

lemma lower_join_map_join:
  "lower_join\(lower_map\lower_join\xsss) = lower_join\(lower_join\xsss)"
by (induct xsss rule: lower_pd_induct, simp_all)

lemma lower_join_map_map:
  "lower_join\(lower_map\(lower_map\f)\xss) =
   lower_map\<cdot>f\<cdot>(lower_join\<cdot>xss)"
by (induct xss rule: lower_pd_induct, simp_all)

end

quality100%

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