Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Pcpo.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/HOLCF/Pcpo.thy
    Author:     Franz Regensburger
*)

section \<open>Classes cpo and pcpo\<close>

theory Pcpo
  imports Porder
begin

subsection \<open>Complete partial orders\<close>

text \<open>The class cpo of chain complete partial orders\<close>

class cpo = po +
  assumes cpo: "chain S \ \x. range S <<| x"
begin

text \<open>in cpo's everthing equal to THE lub has lub properties for every chain\<close>

lemma cpo_lubI: "chain S \ range S <<| (\i. S i)"
  by (fast dest: cpo elim: is_lub_lub)

lemma thelubE: "\chain S; (\i. S i) = l\ \ range S <<| l"
  by (blast dest: cpo intro: is_lub_lub)

text \<open>Properties of the lub\<close>

lemma is_ub_thelub: "chain S \ S x \ (\i. S i)"
  by (blast dest: cpo intro: is_lub_lub [THEN is_lub_rangeD1])

lemma is_lub_thelub: "\chain S; range S <| x\ \ (\i. S i) \ x"
  by (blast dest: cpo intro: is_lub_lub [THEN is_lubD2])

lemma lub_below_iff: "chain S \ (\i. S i) \ x \ (\i. S i \ x)"
  by (simp add: is_lub_below_iff [OF cpo_lubI] is_ub_def)

lemma lub_below: "\chain S; \i. S i \ x\ \ (\i. S i) \ x"
  by (simp add: lub_below_iff)

lemma below_lub: "\chain S; x \ S i\ \ x \ (\i. S i)"
  by (erule below_trans, erule is_ub_thelub)

lemma lub_range_mono: "\range X \ range Y; chain Y; chain X\ \ (\i. X i) \ (\i. Y i)"
  apply (erule lub_below)
  apply (subgoal_tac "\j. X i = Y j")
   apply clarsimp
   apply (erule is_ub_thelub)
  apply auto
  done

lemma lub_range_shift: "chain Y \ (\i. Y (i + j)) = (\i. Y i)"
  apply (rule below_antisym)
   apply (rule lub_range_mono)
     apply fast
    apply assumption
   apply (erule chain_shift)
  apply (rule lub_below)
   apply assumption
  apply (rule_tac i="i" in below_lub)
   apply (erule chain_shift)
  apply (erule chain_mono)
  apply (rule le_add1)
  done

lemma maxinch_is_thelub: "chain Y \ max_in_chain i Y = ((\i. Y i) = Y i)"
  apply (rule iffI)
   apply (fast intro!: lub_eqI lub_finch1)
  apply (unfold max_in_chain_def)
  apply (safe intro!: below_antisym)
   apply (fast elim!: chain_mono)
  apply (drule sym)
  apply (force elim!: is_ub_thelub)
  done

text \<open>the \<open>\<sqsubseteq>\<close> relation between two chains is preserved by their lubs\<close>

lemma lub_mono: "\chain X; chain Y; \i. X i \ Y i\ \ (\i. X i) \ (\i. Y i)"
  by (fast elim: lub_below below_lub)

text \<open>the = relation between two chains is preserved by their lubs\<close>

lemma lub_eq: "(\i. X i = Y i) \ (\i. X i) = (\i. Y i)"
  by simp

lemma ch2ch_lub:
  assumes 1: "\j. chain (\i. Y i j)"
  assumes 2: "\i. chain (\j. Y i j)"
  shows "chain (\i. \j. Y i j)"
  apply (rule chainI)
  apply (rule lub_mono [OF 2 2])
  apply (rule chainE [OF 1])
  done

lemma diag_lub:
  assumes 1: "\j. chain (\i. Y i j)"
  assumes 2: "\i. chain (\j. Y i j)"
  shows "(\i. \j. Y i j) = (\i. Y i i)"
proof (rule below_antisym)
  have 3: "chain (\i. Y i i)"
    apply (rule chainI)
    apply (rule below_trans)
     apply (rule chainE [OF 1])
    apply (rule chainE [OF 2])
    done
  have 4: "chain (\i. \j. Y i j)"
    by (rule ch2ch_lub [OF 1 2])
  show "(\i. \j. Y i j) \ (\i. Y i i)"
    apply (rule lub_below [OF 4])
    apply (rule lub_below [OF 2])
    apply (rule below_lub [OF 3])
    apply (rule below_trans)
     apply (rule chain_mono [OF 1 max.cobounded1])
    apply (rule chain_mono [OF 2 max.cobounded2])
    done
  show "(\i. Y i i) \ (\i. \j. Y i j)"
    apply (rule lub_mono [OF 3 4])
    apply (rule is_ub_thelub [OF 2])
    done
qed

lemma ex_lub:
  assumes 1: "\j. chain (\i. Y i j)"
  assumes 2: "\i. chain (\j. Y i j)"
  shows "(\i. \j. Y i j) = (\j. \i. Y i j)"
  by (simp add: diag_lub 1 2)

end

subsection \<open>Pointed cpos\<close>

text \<open>The class pcpo of pointed cpos\<close>

class pcpo = cpo +
  assumes least: "\x. \y. x \ y"
begin

definition bottom :: "'a"  ("\")
  where "bottom = (THE x. \y. x \ y)"

lemma minimal [iff]: "\ \ x"
  unfolding bottom_def
  apply (rule the1I2)
   apply (rule ex_ex1I)
    apply (rule least)
   apply (blast intro: below_antisym)
  apply simp
  done

end

text \<open>Old "UU" syntax:\<close>

syntax UU :: logic
translations "UU" \<rightharpoonup> "CONST bottom"

text \<open>Simproc to rewrite \<^term>\<open>\<bottom> = x\<close> to \<^term>\<open>x = \<bottom>\<close>.\<close>
setup \<open>Reorient_Proc.add (fn Const(\<^const_name>\<open>bottom\<close>, _) => true | _ => false)\<close>
simproc_setup reorient_bottom ("\ = x") = Reorient_Proc.proc

text \<open>useful lemmas about \<^term>\<open>\<bottom>\<close>\<close>

lemma below_bottom_iff [simp]: "x \ \ \ x = \"
  by (simp add: po_eq_conv)

lemma eq_bottom_iff: "x = \ \ x \ \"
  by simp

lemma bottomI: "x \ \ \ x = \"
  by (subst eq_bottom_iff)

lemma lub_eq_bottom_iff: "chain Y \ (\i. Y i) = \ \ (\i. Y i = \)"
  by (simp only: eq_bottom_iff lub_below_iff)

subsection \<open>Chain-finite and flat cpos\<close>

text \<open>further useful classes for HOLCF domains\<close>

class chfin = po +
  assumes chfin: "chain Y \ \n. max_in_chain n Y"
begin

subclass cpo
  apply standard
  apply (frule chfin)
  apply (blast intro: lub_finch1)
  done

lemma chfin2finch: "chain Y \ finite_chain Y"
  by (simp add: chfin finite_chain_def)

end

class flat = pcpo +
  assumes ax_flat: "x \ y \ x = \ \ x = y"
begin

subclass chfin
proof
  fix Y
  assume *: "chain Y"
  show "\n. max_in_chain n Y"
    apply (unfold max_in_chain_def)
    apply (cases "\i. Y i = \")
     apply simp
    apply simp
    apply (erule exE)
    apply (rule_tac x="i" in exI)
    apply clarify
    using * apply (blast dest: chain_mono ax_flat)
    done
qed

lemma flat_below_iff: "x \ y \ x = \ \ x = y"
  by (safe dest!: ax_flat)

lemma flat_eq: "a \ \ \ a \ b = (a = b)"
  by (safe dest!: ax_flat)

end

subsection \<open>Discrete cpos\<close>

class discrete_cpo = below +
  assumes discrete_cpo [simp]: "x \ y \ x = y"
begin

subclass po
  by standard simp_all

text \<open>In a discrete cpo, every chain is constant\<close>

lemma discrete_chain_const:
  assumes S: "chain S"
  shows "\x. S = (\i. x)"
proof (intro exI ext)
  fix i :: nat
  from S le0 have "S 0 \ S i" by (rule chain_mono)
  then have "S 0 = S i" by simp
  then show "S i = S 0" by (rule sym)
qed

subclass chfin
proof
  fix S :: "nat \ 'a"
  assume S: "chain S"
  then have "\x. S = (\i. x)"
    by (rule discrete_chain_const)
  then have "max_in_chain 0 S"
    by (auto simp: max_in_chain_def)
  then show "\i. max_in_chain i S" ..
qed

end

end

¤ Dauer der Verarbeitung: 0.21 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.