Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/Isabelle/HOL/HOLCF/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 49 kB

Quelle Cpo.thy Sprache: Isabelle

(*  Title:      HOL/HOLCF/Cpo.thy
    Author:     Franz Regensburger
    Author:     Tobias Nipkow
    Author:     Brian Huffman

Foundations of HOLCF: complete partial orders etc.
*)

theory Cpo
  imports Main
begin

section \<open>Partial orders\<close>

declare [[typedef_overloaded]]

subsection \<open>Type class for partial orders\<close>

class below =
  fixes below :: "'a \ 'a \ bool"
begin

notation (ASCII)
  below (infix \<open><<\<close> 50)

notation
  below (infix \<open>\<sqsubseteq>\<close> 50)

abbreviation not_below :: "'a \ 'a \ bool" (infix \\\ 50)
  where "not_below x y \ \ below x y"

notation (ASCII)
  not_below  (infix \<open>~<<\<close> 50)

lemma below_eq_trans: "a \ b \ b = c \ a \ c"
  by (rule subst)

lemma eq_below_trans: "a = b \ b \ c \ a \ c"
  by (rule ssubst)

end

class po = below +
  assumes below_refl [iff]: "x \ x"
  assumes below_trans: "x \ y \ y \ z \ x \ z"
  assumes below_antisym: "x \ y \ y \ x \ x = y"
begin

lemma eq_imp_below: "x = y \ x \ y"
  by simp

lemma box_below: "a \ b \ c \ a \ b \ d \ c \ d"
  by (rule below_trans [OF below_trans])

lemma po_eq_conv: "x = y \ x \ y \ y \ x"
  by (fast intro!: below_antisym)

lemma rev_below_trans: "y \ z \ x \ y \ x \ z"
  by (rule below_trans)

lemma not_below2not_eq: "x \ y \ x \ y"
  by auto

end

lemmas HOLCF_trans_rules [trans] =
  below_trans
  below_antisym
  below_eq_trans
  eq_below_trans

context po
begin

subsection \<open>Upper bounds\<close>

definition is_ub :: "'a set \ 'a \ bool" (infix \<|\ 55)
  where "S <| x \ (\y\S. y \ x)"

lemma is_ubI: "(\x. x \ S \ x \ u) \ S <| u"
  by (simp add: is_ub_def)

lemma is_ubD: "\S <| u; x \ S\ \ x \ u"
  by (simp add: is_ub_def)

lemma ub_imageI: "(\x. x \ S \ f x \ u) \ (\x. f x) ` S <| u"
  unfolding is_ub_def by fast

lemma ub_imageD: "\f ` S <| u; x \ S\ \ f x \ u"
  unfolding is_ub_def by fast

lemma ub_rangeI: "(\i. S i \ x) \ range S <| x"
  unfolding is_ub_def by fast

lemma ub_rangeD: "range S <| x \ S i \ x"
  unfolding is_ub_def by fast

lemma is_ub_empty [simp]: "{} <| u"
  unfolding is_ub_def by fast

lemma is_ub_insert [simp]: "(insert x A) <| y = (x \ y \ A <| y)"
  unfolding is_ub_def by fast

lemma is_ub_upward: "\S <| x; x \ y\ \ S <| y"
  unfolding is_ub_def by (fast intro: below_trans)

subsection \<open>Least upper bounds\<close>

definition is_lub :: "'a set \ 'a \ bool" (infix \<<|\ 55)
  where "S <<| x \ S <| x \ (\u. S <| u \ x \ u)"

definition lub :: "'a set \ 'a"
  where "lub S = (THE x. S <<| x)"

end

syntax (ASCII)
  "_BLub" :: "[pttrn, 'a set, 'b] \ 'b" (\(\indent=3 notation=\binder LUB\\LUB _:_./ _)\ [0,0, 10] 10)

syntax
  "_BLub" :: "[pttrn, 'a set, 'b] \ 'b" (\(\indent=3 notation=\binder \\\\_\_./ _)\ [0,0, 10] 10)

syntax_consts
  "_BLub" \<rightleftharpoons> lub

translations
  "LUB x:A. t" \<rightleftharpoons> "CONST lub ((\<lambda>x. t) ` A)"

context po
begin

abbreviation Lub  (binder \<open>\<Squnion>\<close> 10)
  where "\n. t n \ lub (range t)"

notation (ASCII)
  Lub  (binder \<open>LUB \<close> 10)

text \<open>access to some definition as inference rule\<close>

lemma is_lubD1: "S <<| x \ S <| x"
  unfolding is_lub_def by fast

lemma is_lubD2: "\S <<| x; S <| u\ \ x \ u"
  unfolding is_lub_def by fast

lemma is_lubI: "\S <| x; \u. S <| u \ x \ u\ \ S <<| x"
  unfolding is_lub_def by fast

lemma is_lub_below_iff: "S <<| x \ x \ u \ S <| u"
  unfolding is_lub_def is_ub_def by (metis below_trans)

text \<open>lubs are unique\<close>

lemma is_lub_unique: "S <<| x \ S <<| y \ x = y"
  unfolding is_lub_def is_ub_def by (blast intro: below_antisym)

text \<open>technical lemmas about \<^term>\<open>lub\<close> and \<^term>\<open>is_lub\<close>\<close>

lemma is_lub_lub: "M <<| x \ M <<| lub M"
  unfolding lub_def by (rule theI [OF _ is_lub_unique])

lemma lub_eqI: "M <<| l \ lub M = l"
  by (rule is_lub_unique [OF is_lub_lub])

lemma is_lub_singleton [simp]: "{x} <<| x"
  by (simp add: is_lub_def)

lemma lub_singleton [simp]: "lub {x} = x"
  by (rule is_lub_singleton [THEN lub_eqI])

lemma is_lub_bin: "x \ y \ {x, y} <<| y"
  by (simp add: is_lub_def)

lemma lub_bin: "x \ y \ lub {x, y} = y"
  by (rule is_lub_bin [THEN lub_eqI])

lemma is_lub_maximal: "S <| x \ x \ S \ S <<| x"
  by (erule is_lubI, erule (1) is_ubD)

lemma lub_maximal: "S <| x \ x \ S \ lub S = x"
  by (rule is_lub_maximal [THEN lub_eqI])

subsection \<open>Countable chains\<close>

definition chain :: "(nat \ 'a) \ bool"
  where \<comment> \<open>Here we use countable chains and I prefer to code them as functions!\<close>
  "chain Y = (\i. Y i \ Y (Suc i))"

lemma chainI: "(\i. Y i \ Y (Suc i)) \ chain Y"
  unfolding chain_def by fast

lemma chainE: "chain Y \ Y i \ Y (Suc i)"
  unfolding chain_def by fast

text \<open>chains are monotone functions\<close>

lemma chain_mono_less: "chain Y \ i < j \ Y i \ Y j"
  by (erule less_Suc_induct, erule chainE, erule below_trans)

lemma chain_mono: "chain Y \ i \ j \ Y i \ Y j"
  by (cases "i = j") (simp_all add: chain_mono_less)

lemma chain_shift: "chain Y \ chain (\i. Y (i + j))"
  by (rule chainI, simp, erule chainE)

text \<open>technical lemmas about (least) upper bounds of chains\<close>

lemma is_lub_rangeD1: "range S <<| x \ S i \ x"
  by (rule is_lubD1 [THEN ub_rangeD])

lemma is_ub_range_shift: "chain S \ range (\i. S (i + j)) <| x = range S <| x"
  apply (rule iffI)
   apply (rule ub_rangeI)
   apply (rule_tac y="S (i + j)" in below_trans)
    apply (erule chain_mono)
    apply (rule le_add1)
   apply (erule ub_rangeD)
  apply (rule ub_rangeI)
  apply (erule ub_rangeD)
  done

lemma is_lub_range_shift: "chain S \ range (\i. S (i + j)) <<| x = range S <<| x"
  by (simp add: is_lub_def is_ub_range_shift)

text \<open>the lub of a constant chain is the constant\<close>

lemma chain_const [simp]: "chain (\i. c)"
  by (simp add: chainI)

lemma is_lub_const: "range (\x. c) <<| c"
by (blast dest: ub_rangeD intro: is_lubI ub_rangeI)

lemma lub_const [simp]: "(\i. c) = c"
  by (rule is_lub_const [THEN lub_eqI])

subsection \<open>Finite chains\<close>

definition max_in_chain :: "nat \ (nat \ 'a) \ bool"
  where \<comment> \<open>finite chains, needed for monotony of continuous functions\<close>
  "max_in_chain i C \ (\j. i \ j \ C i = C j)"

definition finite_chain :: "(nat \ 'a) \ bool"
  where "finite_chain C = (chain C \ (\i. max_in_chain i C))"

text \<open>results about finite chains\<close>

lemma max_in_chainI: "(\j. i \ j \ Y i = Y j) \ max_in_chain i Y"
  unfolding max_in_chain_def by fast

lemma max_in_chainD: "max_in_chain i Y \ i \ j \ Y i = Y j"
  unfolding max_in_chain_def by fast

lemma finite_chainI: "chain C \ max_in_chain i C \ finite_chain C"
  unfolding finite_chain_def by fast

lemma finite_chainE: "\finite_chain C; \i. \chain C; max_in_chain i C\ \ R\ \ R"
  unfolding finite_chain_def by fast

lemma lub_finch1: "chain C \ max_in_chain i C \ range C <<| C i"
  apply (rule is_lubI)
   apply (rule ub_rangeI, rename_tac j)
   apply (rule_tac x=i and y=j in linorder_le_cases)
    apply (drule (1) max_in_chainD, simp)
   apply (erule (1) chain_mono)
  apply (erule ub_rangeD)
  done

lemma lub_finch2: "finite_chain C \ range C <<| C (LEAST i. max_in_chain i C)"
  apply (erule finite_chainE)
  apply (erule LeastI2 [where Q="\i. range C <<| C i"])
  apply (erule (1) lub_finch1)
  done

lemma finch_imp_finite_range: "finite_chain Y \ finite (range Y)"
  apply (erule finite_chainE)
  apply (rule_tac B="Y ` {..i}" in finite_subset)
   apply (rule subsetI)
   apply (erule rangeE, rename_tac j)
   apply (rule_tac x=i and y=j in linorder_le_cases)
    apply (subgoal_tac "Y j = Y i", simp)
    apply (simp add: max_in_chain_def)
   apply simp
  apply simp
  done

lemma finite_range_has_max:
  fixes f :: "nat \ 'a"
    and r :: "'a \ 'a \ bool"
  assumes mono: "\i j. i \ j \ r (f i) (f j)"
  assumes finite_range: "finite (range f)"
  shows "\k. \i. r (f i) (f k)"
proof (intro exI allI)
  fix i :: nat
  let ?j = "LEAST k. f k = f i"
  let ?k = "Max ((\x. LEAST k. f k = x) ` range f)"
  have "?j \ ?k"
  proof (rule Max_ge)
    show "finite ((\x. LEAST k. f k = x) ` range f)"
      using finite_range by (rule finite_imageI)
    show "?j \ (\x. LEAST k. f k = x) ` range f"
      by (intro imageI rangeI)
  qed
  hence "r (f ?j) (f ?k)"
    by (rule mono)
  also have "f ?j = f i"
    by (rule LeastI, rule refl)
  finally show "r (f i) (f ?k)" .
qed

lemma finite_range_imp_finch: "chain Y \ finite (range Y) \ finite_chain Y"
  apply (subgoal_tac "\k. \i. Y i \ Y k")
   apply (erule exE)
   apply (rule finite_chainI, assumption)
   apply (rule max_in_chainI)
   apply (rule below_antisym)
    apply (erule (1) chain_mono)
   apply (erule spec)
  apply (rule finite_range_has_max)
   apply (erule (1) chain_mono)
  apply assumption
  done

lemma bin_chain: "x \ y \ chain (\i. if i=0 then x else y)"
  by (rule chainI) simp

lemma bin_chainmax: "x \ y \ max_in_chain (Suc 0) (\i. if i=0 then x else y)"
  by (simp add: max_in_chain_def)

lemma is_lub_bin_chain: "x \ y \ range (\i::nat. if i=0 then x else y) <<| y"
  apply (frule bin_chain)
  apply (drule bin_chainmax)
  apply (drule (1) lub_finch1)
  apply simp
  done

text \<open>the maximal element in a chain is its lub\<close>

lemma lub_chain_maxelem: "Y i = c \ \i. Y i \ c \ lub (range Y) = c"
  by (blast dest: ub_rangeD intro: lub_eqI is_lubI ub_rangeI)

end

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

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"

default_sort cpo

context cpo
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"  (\<open>\<bottom>\<close>)
  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>
abbreviation (input) "UU \ 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_>\<open>bottom _\<close> => true | _ => false)\<close>
simproc_setup reorient_bottom ("\ = x") = \K 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

section \<open>Continuity and monotonicity\<close>

subsection \<open>Definitions\<close>

definition monofun :: "('a::po \ 'b::po) \ bool" \ \monotonicity\
  where "monofun f \ (\x y. x \ y \ f x \ f y)"

definition cont :: "('a \ 'b) \ bool"
  where "cont f = (\Y. chain Y \ range (\i. f (Y i)) <<| f (\i. Y i))"

lemma contI: "(\Y. chain Y \ range (\i. f (Y i)) <<| f (\i. Y i)) \ cont f"
  by (simp add: cont_def)

lemma contE: "cont f \ chain Y \ range (\i. f (Y i)) <<| f (\i. Y i)"
  by (simp add: cont_def)

lemma monofunI: "(\x y. x \ y \ f x \ f y) \ monofun f"
  by (simp add: monofun_def)

lemma monofunE: "monofun f \ x \ y \ f x \ f y"
  by (simp add: monofun_def)

subsection \<open>Equivalence of alternate definition\<close>

text \<open>monotone functions map chains to chains\<close>

lemma ch2ch_monofun: "monofun f \ chain Y \ chain (\i. f (Y i))"
  apply (rule chainI)
  apply (erule monofunE)
  apply (erule chainE)
  done

text \<open>monotone functions map upper bound to upper bounds\<close>

lemma ub2ub_monofun: "monofun f \ range Y <| u \ range (\i. f (Y i)) <| f u"
  apply (rule ub_rangeI)
  apply (erule monofunE)
  apply (erule ub_rangeD)
  done

text \<open>a lemma about binary chains\<close>

lemma binchain_cont: "cont f \ x \ y \ range (\i::nat. f (if i = 0 then x else y)) <<| f y"
  apply (subgoal_tac "f (\i::nat. if i = 0 then x else y) = f y")
   apply (erule subst)
   apply (erule contE)
   apply (erule bin_chain)
  apply (rule_tac f=f in arg_cong)
  apply (erule is_lub_bin_chain [THEN lub_eqI])
  done

text \<open>continuity implies monotonicity\<close>

lemma cont2mono: "cont f \ monofun f"
  apply (rule monofunI)
  apply (drule (1) binchain_cont)
  apply (drule_tac i=0 in is_lub_rangeD1)
  apply simp
  done

lemmas cont2monofunE = cont2mono [THEN monofunE]

lemmas ch2ch_cont = cont2mono [THEN ch2ch_monofun]

text \<open>continuity implies preservation of lubs\<close>

lemma cont2contlubE: "cont f \ chain Y \ f (\i. Y i) = (\i. f (Y i))"
  apply (rule lub_eqI [symmetric])
  apply (erule (1) contE)
  done

lemma contI2:
  fixes f :: "'a \ 'b"
  assumes mono: "monofun f"
  assumes below: "\Y. \chain Y; chain (\i. f (Y i))\ \ f (\i. Y i) \ (\i. f (Y i))"
  shows "cont f"
proof (rule contI)
  fix Y :: "nat \ 'a"
  assume Y: "chain Y"
  with mono have fY: "chain (\i. f (Y i))"
    by (rule ch2ch_monofun)
  have "(\i. f (Y i)) = f (\i. Y i)"
    apply (rule below_antisym)
     apply (rule lub_below [OF fY])
     apply (rule monofunE [OF mono])
     apply (rule is_ub_thelub [OF Y])
    apply (rule below [OF Y fY])
    done
  with fY show "range (\i. f (Y i)) <<| f (\i. Y i)"
    by (rule thelubE)
qed

subsection \<open>Collection of continuity rules\<close>

named_theorems cont2cont "continuity intro rule"

subsection \<open>Continuity of basic functions\<close>

text \<open>The identity function is continuous\<close>

lemma cont_id [simp, cont2cont]: "cont (\x. x)"
  apply (rule contI)
  apply (erule cpo_lubI)
  done

text \<open>constant functions are continuous\<close>

lemma cont_const [simp, cont2cont]: "cont (\x. c)"
  using is_lub_const by (rule contI)

text \<open>application of functions is continuous\<close>

lemma cont_apply:
  fixes f :: "'a \ 'b \ 'c" and t :: "'a \ 'b"
  assumes 1: "cont (\x. t x)"
  assumes 2: "\x. cont (\y. f x y)"
  assumes 3: "\y. cont (\x. f x y)"
  shows "cont (\x. (f x) (t x))"
proof (rule contI2 [OF monofunI])
  fix x y :: "'a"
  assume "x \ y"
  then show "f x (t x) \ f y (t y)"
    by (auto intro: cont2monofunE [OF 1]
        cont2monofunE [OF 2]
        cont2monofunE [OF 3]
        below_trans)
next
  fix Y :: "nat \ 'a"
  assume "chain Y"
  then show "f (\i. Y i) (t (\i. Y i)) \ (\i. f (Y i) (t (Y i)))"
    by (simp only: cont2contlubE [OF 1] ch2ch_cont [OF 1]
        cont2contlubE [OF 2] ch2ch_cont [OF 2]
        cont2contlubE [OF 3] ch2ch_cont [OF 3]
        diag_lub below_refl)
qed

lemma cont_compose: "cont c \ cont (\x. f x) \ cont (\x. c (f x))"
  by (rule cont_apply [OF _ _ cont_const])

text \<open>Least upper bounds preserve continuity\<close>

lemma cont2cont_lub [simp]:
  assumes chain: "\x. chain (\i. F i x)"
    and cont: "\i. cont (\x. F i x)"
  shows "cont (\x. \i. F i x)"
  apply (rule contI2)
   apply (simp add: monofunI cont2monofunE [OF cont] lub_mono chain)
  apply (simp add: cont2contlubE [OF cont])
  apply (simp add: diag_lub ch2ch_cont [OF cont] chain)
  done

text \<open>if-then-else is continuous\<close>

lemma cont_if [simp, cont2cont]: "cont f \ cont g \ cont (\x. if b then f x else g x)"
  by (induct b) simp_all

subsection \<open>Finite chains and flat pcpos\<close>

text \<open>Monotone functions map finite chains to finite chains.\<close>

lemma monofun_finch2finch: "monofun f \ finite_chain Y \ finite_chain (\n. f (Y n))"
  by (force simp add: finite_chain_def ch2ch_monofun max_in_chain_def)

text \<open>The same holds for continuous functions.\<close>

lemma cont_finch2finch: "cont f \ finite_chain Y \ finite_chain (\n. f (Y n))"
  by (rule cont2mono [THEN monofun_finch2finch])

text \<open>All monotone functions with chain-finite domain are continuous.\<close>

lemma chfindom_monofun2cont: "monofun f \ cont f"
  for f :: "'a::chfin \ 'b"
  apply (erule contI2)
  apply (frule chfin2finch)
  apply (clarsimp simp add: finite_chain_def)
  apply (subgoal_tac "max_in_chain i (\i. f (Y i))")
   apply (simp add: maxinch_is_thelub ch2ch_monofun)
  apply (force simp add: max_in_chain_def)
  done

text \<open>All strict functions with flat domain are continuous.\<close>

lemma flatdom_strict2mono: "f \ = \ \ monofun f"
  for f :: "'a::flat \ 'b::pcpo"
  apply (rule monofunI)
  apply (drule ax_flat)
  apply auto
  done

lemma flatdom_strict2cont: "f \ = \ \ cont f"
  for f :: "'a::flat \ 'b::pcpo"
  by (rule flatdom_strict2mono [THEN chfindom_monofun2cont])

text \<open>All functions with discrete domain are continuous.\<close>

lemma cont_discrete_cpo [simp, cont2cont]: "cont f"
  for f :: "'a::discrete_cpo \ 'b"
  apply (rule contI)
  apply (drule discrete_chain_const, clarify)
  apply simp
  done

section \<open>Admissibility and compactness\<close>

subsection \<open>Definitions\<close>

context cpo
begin

definition adm :: "('a \ bool) \ bool"
  where "adm P \ (\Y. chain Y \ (\i. P (Y i)) \ P (\i. Y i))"

lemma admI: "(\Y. \chain Y; \i. P (Y i)\ \ P (\i. Y i)) \ adm P"
  unfolding adm_def by fast

lemma admD: "adm P \ chain Y \ (\i. P (Y i)) \ P (\i. Y i)"
  unfolding adm_def by fast

lemma admD2: "adm (\x. \ P x) \ chain Y \ P (\i. Y i) \ \i. P (Y i)"
  unfolding adm_def by fast

lemma triv_admI: "\x. P x \ adm P"
  by (rule admI) (erule spec)

end

subsection \<open>Admissibility on chain-finite types\<close>

text \<open>For chain-finite (easy) types every formula is admissible.\<close>

lemma adm_chfin [simp]: "adm P" for P :: "'a::chfin \ bool"
  by (rule admI, frule chfin, auto simp add: maxinch_is_thelub)

subsection \<open>Admissibility of special formulae and propagation\<close>

context cpo
begin

lemma adm_const [simp]: "adm (\x. t)"
  by (rule admI, simp)

lemma adm_conj [simp]: "adm (\x. P x) \ adm (\x. Q x) \ adm (\x. P x \ Q x)"
  by (fast intro: admI elim: admD)

lemma adm_all [simp]: "(\y. adm (\x. P x y)) \ adm (\x. \y. P x y)"
  by (fast intro: admI elim: admD)

lemma adm_ball [simp]: "(\y. y \ A \ adm (\x. P x y)) \ adm (\x. \y\A. P x y)"
  by (fast intro: admI elim: admD)

text \<open>Admissibility for disjunction is hard to prove. It requires 2 lemmas.\<close>

lemma adm_disj_lemma1:
  assumes adm: "adm P"
  assumes chain: "chain Y"
  assumes P: "\i. \j\i. P (Y j)"
  shows "P (\i. Y i)"
proof -
  define f where "f i = (LEAST j. i \ j \ P (Y j))" for i
  have chain': "chain (\i. Y (f i))"
    unfolding f_def
    apply (rule chainI)
    apply (rule chain_mono [OF chain])
    apply (rule Least_le)
    apply (rule LeastI2_ex)
     apply (simp_all add: P)
    done
  have f1: "\i. i \ f i" and f2: "\i. P (Y (f i))"
    using LeastI_ex [OF P [rule_format]] by (simp_all add: f_def)
  have lub_eq: "(\i. Y i) = (\i. Y (f i))"
    apply (rule below_antisym)
     apply (rule lub_mono [OF chain chain'])
     apply (rule chain_mono [OF chain f1])
    apply (rule lub_range_mono [OF _ chain chain'])
    apply clarsimp
    done
  show "P (\i. Y i)"
    unfolding lub_eq using adm chain' f2 by (rule admD)
qed

lemma adm_disj_lemma2: "\n::nat. P n \ Q n \ (\i. \j\i. P j) \ (\i. \j\i. Q j)"
  apply (erule contrapos_pp)
  apply (clarsimp, rename_tac a b)
  apply (rule_tac x="max a b" in exI)
  apply simp
  done

lemma adm_disj [simp]: "adm (\x. P x) \ adm (\x. Q x) \ adm (\x. P x \ Q x)"
  apply (rule admI)
  apply (erule adm_disj_lemma2 [THEN disjE])
   apply (erule (2) adm_disj_lemma1 [THEN disjI1])
  apply (erule (2) adm_disj_lemma1 [THEN disjI2])
  done

lemma adm_imp [simp]: "adm (\x. \ P x) \ adm (\x. Q x) \ adm (\x. P x \ Q x)"
  by (subst imp_conv_disj) (rule adm_disj)

lemma adm_iff [simp]: "adm (\x. P x \ Q x) \ adm (\x. Q x \ P x) \ adm (\x. P x \ Q x)"
  by (subst iff_conv_conj_imp) (rule adm_conj)

end

text \<open>admissibility and continuity\<close>

lemma adm_below [simp]: "cont (\x. u x) \ cont (\x. v x) \ adm (\x. u x \ v x)"
  by (simp add: adm_def cont2contlubE lub_mono ch2ch_cont)

lemma adm_eq [simp]: "cont (\x. u x) \ cont (\x. v x) \ adm (\x. u x = v x)"
  by (simp add: po_eq_conv)

lemma adm_subst: "cont (\x. t x) \ adm P \ adm (\x. P (t x))"
  by (simp add: adm_def cont2contlubE ch2ch_cont)

lemma adm_not_below [simp]: "cont (\x. t x) \ adm (\x. t x \ u)"
  by (rule admI) (simp add: cont2contlubE ch2ch_cont lub_below_iff)

subsection \<open>Compactness\<close>

context cpo
begin

definition compact :: "'a \ bool"
  where "compact k = adm (\x. k \ x)"

lemma compactI: "adm (\x. k \ x) \ compact k"
  unfolding compact_def .

lemma compactD: "compact k \ adm (\x. k \ x)"
  unfolding compact_def .

lemma compactI2: "(\Y. \chain Y; x \ (\i. Y i)\ \ \i. x \ Y i) \ compact x"
  unfolding compact_def adm_def by fast

lemma compactD2: "compact x \ chain Y \ x \ (\i. Y i) \ \i. x \ Y i"
  unfolding compact_def adm_def by fast

lemma compact_below_lub_iff: "compact x \ chain Y \ x \ (\i. Y i) \ (\i. x \ Y i)"
  by (fast intro: compactD2 elim: below_lub)

end

lemma compact_chfin [simp]: "compact x" for x :: "'a::chfin"
  by (rule compactI [OF adm_chfin])

lemma compact_imp_max_in_chain: "chain Y \ compact (\i. Y i) \ \i. max_in_chain i Y"
  apply (drule (1) compactD2, simp)
  apply (erule exE, rule_tac x=i in exI)
  apply (rule max_in_chainI)
  apply (rule below_antisym)
   apply (erule (1) chain_mono)
  apply (erule (1) below_trans [OF is_ub_thelub])
  done

text \<open>admissibility and compactness\<close>

lemma adm_compact_not_below [simp]:
  "compact k \ cont (\x. t x) \ adm (\x. k \ t x)"
  unfolding compact_def by (rule adm_subst)

lemma adm_neq_compact [simp]: "compact k \ cont (\x. t x) \ adm (\x. t x \ k)"
  by (simp add: po_eq_conv)

lemma adm_compact_neq [simp]: "compact k \ cont (\x. t x) \ adm (\x. k \ t x)"
  by (simp add: po_eq_conv)

lemma compact_bottom [simp, intro]: "compact \"
  by (rule compactI) simp

text \<open>Any upward-closed predicate is admissible.\<close>

lemma adm_upward:
  assumes P: "\x y. \P x; x \ y\ \ P y"
  shows "adm P"
  by (rule admI, drule spec, erule P, erule is_ub_thelub)

lemmas adm_lemmas =
  adm_const adm_conj adm_all adm_ball adm_disj adm_imp adm_iff
  adm_below adm_eq adm_not_below
  adm_compact_not_below adm_compact_neq adm_neq_compact

section \<open>Class instances for the full function space\<close>

subsection \<open>Full function space is a partial order\<close>

instantiation "fun"  :: (type, below) below
begin

definition below_fun_def: "(\) \ (\f g. \x. f x \ g x)"

instance ..
end

instance "fun" :: (type, po) po
proof
  fix f g h :: "'a \ 'b"
  show "f \ f"
    by (simp add: below_fun_def)
  show "f \ g \ g \ f \ f = g"
    by (simp add: below_fun_def fun_eq_iff below_antisym)
  show "f \ g \ g \ h \ f \ h"
    unfolding below_fun_def by (fast elim: below_trans)
qed

lemma fun_below_iff: "f \ g \ (\x. f x \ g x)"
  by (simp add: below_fun_def)

lemma fun_belowI: "(\x. f x \ g x) \ f \ g"
  by (simp add: below_fun_def)

lemma fun_belowD: "f \ g \ f x \ g x"
  by (simp add: below_fun_def)

subsection \<open>Full function space is chain complete\<close>

text \<open>Properties of chains of functions.\<close>

lemma fun_chain_iff: "chain S \ (\x. chain (\i. S i x))"
  by (auto simp: chain_def fun_below_iff)

lemma ch2ch_fun: "chain S \ chain (\i. S i x)"
  by (simp add: chain_def below_fun_def)

lemma ch2ch_lambda: "(\x. chain (\i. S i x)) \ chain S"
  by (simp add: chain_def below_fun_def)

text \<open>Type \<^typ>\<open>'a::type \<Rightarrow> 'b::cpo\<close> is chain complete\<close>

lemma is_lub_lambda: "(\x. range (\i. Y i x) <<| f x) \ range Y <<| f"
  by (simp add: is_lub_def is_ub_def below_fun_def)

lemma is_lub_fun: "chain S \ range S <<| (\x. \i. S i x)"
  for S :: "nat \ 'a::type \ 'b"
  apply (rule is_lub_lambda)
  apply (rule cpo_lubI)
  apply (erule ch2ch_fun)
  done

lemma lub_fun: "chain S \ (\i. S i) = (\x. \i. S i x)"
  for S :: "nat \ 'a::type \ 'b"
  by (rule is_lub_fun [THEN lub_eqI])

instance "fun"  :: (type, cpo) cpo
  by intro_classes (rule exI, erule is_lub_fun)

instance "fun" :: (type, discrete_cpo) discrete_cpo
proof
  fix f g :: "'a \ 'b"
  show "f \ g \ f = g"
    by (simp add: fun_below_iff fun_eq_iff)
qed

subsection \<open>Full function space is pointed\<close>

lemma minimal_fun: "(\x. \) \ f"
  by (simp add: below_fun_def)

instance "fun"  :: (type, pcpo) pcpo
  by standard (fast intro: minimal_fun)

lemma inst_fun_pcpo: "\ = (\x. \)"
  by (rule minimal_fun [THEN bottomI, symmetric])

lemma app_strict [simp]: "\ x = \"
  by (simp add: inst_fun_pcpo)

lemma lambda_strict: "(\x. \) = \"
  by (rule bottomI, rule minimal_fun)

subsection \<open>Propagation of monotonicity and continuity\<close>

text \<open>The lub of a chain of monotone functions is monotone.\<close>

lemma adm_monofun: "adm monofun"
  by (rule admI) (simp add: lub_fun fun_chain_iff monofun_def lub_mono)

text \<open>The lub of a chain of continuous functions is continuous.\<close>

lemma adm_cont: "adm cont"
  by (rule admI) (simp add: lub_fun fun_chain_iff)

text \<open>Function application preserves monotonicity and continuity.\<close>

lemma mono2mono_fun: "monofun f \ monofun (\x. f x y)"
  by (simp add: monofun_def fun_below_iff)

lemma cont2cont_fun: "cont f \ cont (\x. f x y)"
  apply (rule contI2)
   apply (erule cont2mono [THEN mono2mono_fun])
  apply (simp add: cont2contlubE lub_fun ch2ch_cont)
  done

lemma cont_fun: "cont (\f. f x)"
  using cont_id by (rule cont2cont_fun)

simproc_setup apply_cont (\<open>cont (\<lambda>f. E f)\<close>) = \<open>
  fn _ => fn ctxt => fn lhs =>
    (case Thm.term_of lhs of
      \<^Const_>\<open>cont _ _ for \<open>Abs (_, _, expr)\<close>\<close> =>
        if case strip_comb expr of (f, args) =>
              f = Bound 0 andalso not (exists Term.is_dependent args)
        (* since \<open>\<lambda>f. E f\<close> is too permissive, we ensure here that the term
           is of the form \<open>\<lambda>f. f \<dots>\<close>, with \<open>f\<close> no longer appearing in \<open>\<dots>\<close> *)
        then
          let
            val tac = Metis_Tactic.metis_tac ["no_types"] "combs" ctxt @{thms cont2cont_fun cont_id}
            val thm =
              Goal.prove_internal ctxt [] \<^instantiate>\<open>lhs in cprop \<open>lhs = True\<close>\<close>
                (fn _ => tac 1)
          in SOME (mk_meta_eq thm) end
        else NONE
    | _ => NONE)
\<close>

lemma "cont (\f. f x)" and "cont (\f. f x y)" and "cont (\f. f x y z)"
  by simp_all

text \<open>
  Lambda abstraction preserves monotonicity and continuity.
  (Note \<open>(\<lambda>x. \<lambda>y. f x y) = f\<close>.)
\<close>

lemma mono2mono_lambda: "(\y. monofun (\x. f x y)) \ monofun f"
  by (simp add: monofun_def fun_below_iff)

lemma cont2cont_lambda [simp]:
  assumes f: "\y. cont (\x. f x y)"
  shows "cont f"
  by (rule contI, rule is_lub_lambda, rule contE [OF f])

text \<open>What D.A.Schmidt calls continuity of abstraction; never used here\<close>

lemma contlub_lambda: "(\x. chain (\i. S i x)) \ (\x. \i. S i x) = (\i. (\x. S i x))"
  for S :: "nat \ 'a::type \ 'b"
  by (simp add: lub_fun ch2ch_lambda)

section \<open>The cpo of cartesian products\<close>

subsection \<open>Unit type is a pcpo\<close>

instantiation unit :: discrete_cpo
begin

definition below_unit_def [simp]: "x \ (y::unit) \ True"

instance
  by standard simp

end

instance unit :: pcpo
  by standard simp

subsection \<open>Product type is a partial order\<close>

instantiation prod :: (below, below) below
begin

definition below_prod_def: "(\) \ \p1 p2. (fst p1 \ fst p2 \ snd p1 \ snd p2)"

instance ..

end

instance prod :: (po, po) po
proof
  fix x y z :: "'a \ 'b"
  show "x \ x"
    by (simp add: below_prod_def)
  show "x \ y \ y \ x \ x = y"
    unfolding below_prod_def prod_eq_iff
    by (fast intro: below_antisym)
  show "x \ y \ y \ z \ x \ z"
    unfolding below_prod_def
    by (fast intro: below_trans)
qed

subsection \<open>Monotonicity of \emph{Pair}, \emph{fst}, \emph{snd}\<close>

lemma prod_belowI: "fst p \ fst q \ snd p \ snd q \ p \ q"
  by (simp add: below_prod_def)

lemma Pair_below_iff [simp]: "(a, b) \ (c, d) \ a \ c \ b \ d"
  by (simp add: below_prod_def)

text \<open>Pair \<open>(_,_)\<close>  is monotone in both arguments\<close>

lemma monofun_pair1: "monofun (\x. (x, y))"
  by (simp add: monofun_def)

lemma monofun_pair2: "monofun (\y. (x, y))"
  by (simp add: monofun_def)

lemma monofun_pair: "x1 \ x2 \ y1 \ y2 \ (x1, y1) \ (x2, y2)"
  by simp

lemma ch2ch_Pair [simp]: "chain X \ chain Y \ chain (\i. (X i, Y i))"
  by (rule chainI, simp add: chainE)

text \<open>\<^term>\<open>fst\<close> and \<^term>\<open>snd\<close> are monotone\<close>

lemma fst_monofun: "x \ y \ fst x \ fst y"
  by (simp add: below_prod_def)

lemma snd_monofun: "x \ y \ snd x \ snd y"
  by (simp add: below_prod_def)

lemma monofun_fst: "monofun fst"
  by (simp add: monofun_def below_prod_def)

lemma monofun_snd: "monofun snd"
  by (simp add: monofun_def below_prod_def)

lemmas ch2ch_fst [simp] = ch2ch_monofun [OF monofun_fst]

lemmas ch2ch_snd [simp] = ch2ch_monofun [OF monofun_snd]

lemma prod_chain_cases:
  assumes chain: "chain Y"
  obtains A B
  where "chain A" and "chain B" and "Y = (\i. (A i, B i))"
proof
  from chain show "chain (\i. fst (Y i))"
    by (rule ch2ch_fst)
  from chain show "chain (\i. snd (Y i))"
    by (rule ch2ch_snd)
  show "Y = (\i. (fst (Y i), snd (Y i)))"
    by simp
qed

subsection \<open>Product type is a cpo\<close>

lemma is_lub_Pair: "range A <<| x \ range B <<| y \ range (\i. (A i, B i)) <<| (x, y)"
  by (simp add: is_lub_def is_ub_def below_prod_def)

lemma lub_Pair: "chain A \ chain B \ (\i. (A i, B i)) = (\i. A i, \i. B i)"
  for A :: "nat \ 'a" and B :: "nat \ 'b"
  by (fast intro: lub_eqI is_lub_Pair elim: thelubE)

lemma is_lub_prod:
  fixes S :: "nat \ ('a \ 'b)"
  assumes "chain S"
  shows "range S <<| (\i. fst (S i), \i. snd (S i))"
  using assms by (auto elim: prod_chain_cases simp: is_lub_Pair cpo_lubI)

lemma lub_prod: "chain S \ (\i. S i) = (\i. fst (S i), \i. snd (S i))"
  for S :: "nat \ 'a \ 'b"
  by (rule is_lub_prod [THEN lub_eqI])

instance prod :: (cpo, cpo) cpo
proof
  fix S :: "nat \ ('a \ 'b)"
  assume "chain S"
  then have "range S <<| (\i. fst (S i), \i. snd (S i))"
    by (rule is_lub_prod)
  then show "\x. range S <<| x" ..
qed

instance prod :: (discrete_cpo, discrete_cpo) discrete_cpo
proof
  show "x \ y \ x = y" for x y :: "'a \ 'b"
    by (simp add: below_prod_def prod_eq_iff)
qed

subsection \<open>Product type is pointed\<close>

lemma minimal_prod: "(\, \) \ p"
  by (simp add: below_prod_def)

instance prod :: (pcpo, pcpo) pcpo
  by intro_classes (fast intro: minimal_prod)

lemma inst_prod_pcpo: "\ = (\, \)"
  by (rule minimal_prod [THEN bottomI, symmetric])

lemma Pair_bottom_iff [simp]: "(x, y) = \ \ x = \ \ y = \"
  by (simp add: inst_prod_pcpo)

lemma fst_strict [simp]: "fst \ = \"
  unfolding inst_prod_pcpo by (rule fst_conv)

lemma snd_strict [simp]: "snd \ = \"
  unfolding inst_prod_pcpo by (rule snd_conv)

lemma Pair_strict [simp]: "(\, \) = \"
  by simp

lemma split_strict [simp]: "case_prod f \ = f \ \"
  by (simp add: split_def)

subsection \<open>Continuity of \emph{Pair}, \emph{fst}, \emph{snd}\<close>

lemma cont_pair1: "cont (\x. (x, y))"
  apply (rule contI)
  apply (rule is_lub_Pair)
   apply (erule cpo_lubI)
  apply (rule is_lub_const)
  done

lemma cont_pair2: "cont (\y. (x, y))"
  apply (rule contI)
  apply (rule is_lub_Pair)
   apply (rule is_lub_const)
  apply (erule cpo_lubI)
  done

lemma cont_fst: "cont fst"
  apply (rule contI)
  apply (simp add: lub_prod)
  apply (erule cpo_lubI [OF ch2ch_fst])
  done

lemma cont_snd: "cont snd"
  apply (rule contI)
  apply (simp add: lub_prod)
  apply (erule cpo_lubI [OF ch2ch_snd])
  done

lemma cont2cont_Pair [simp, cont2cont]:
  assumes f: "cont (\x. f x)"
  assumes g: "cont (\x. g x)"
  shows "cont (\x. (f x, g x))"
  apply (rule cont_apply [OF f cont_pair1])
  apply (rule cont_apply [OF g cont_pair2])
  apply (rule cont_const)
  done

lemmas cont2cont_fst [simp, cont2cont] = cont_compose [OF cont_fst]

lemmas cont2cont_snd [simp, cont2cont] = cont_compose [OF cont_snd]

lemma cont2cont_case_prod:
  assumes f1: "\a b. cont (\x. f x a b)"
  assumes f2: "\x b. cont (\a. f x a b)"
  assumes f3: "\x a. cont (\b. f x a b)"
  assumes g: "cont (\x. g x)"
  shows "cont (\x. case g x of (a, b) \ f x a b)"
  unfolding split_def
  apply (rule cont_apply [OF g])
   apply (rule cont_apply [OF cont_fst f2])
   apply (rule cont_apply [OF cont_snd f3])
   apply (rule cont_const)
  apply (rule f1)
  done

lemma prod_contI:
  assumes f1: "\y. cont (\x. f (x, y))"
  assumes f2: "\x. cont (\y. f (x, y))"
  shows "cont f"
proof -
  have "cont (\(x, y). f (x, y))"
    by (intro cont2cont_case_prod f1 f2 cont2cont)
  then show "cont f"
    by (simp only: case_prod_eta)
qed

lemma prod_cont_iff: "cont f \ (\y. cont (\x. f (x, y))) \ (\x. cont (\y. f (x, y)))"
  apply safe
    apply (erule cont_compose [OF _ cont_pair1])
   apply (erule cont_compose [OF _ cont_pair2])
  apply (simp only: prod_contI)
  done

lemma cont2cont_case_prod' [simp, cont2cont]:
  assumes f: "cont (\p. f (fst p) (fst (snd p)) (snd (snd p)))"
  assumes g: "cont (\x. g x)"
  shows "cont (\x. case_prod (f x) (g x))"
  using assms by (simp add: cont2cont_case_prod prod_cont_iff)

text \<open>The simple version (due to Joachim Breitner) is needed if
  either element type of the pair is not a cpo.\<close>

lemma cont2cont_split_simple [simp, cont2cont]:
  assumes "\a b. cont (\x. f x a b)"
  shows "cont (\x. case p of (a, b) \ f x a b)"
  using assms by (cases p) auto

text \<open>Admissibility of predicates on product types.\<close>

lemma adm_case_prod [simp]:
  assumes "adm (\x. P x (fst (f x)) (snd (f x)))"
  shows "adm (\x. case f x of (a, b) \ P x a b)"
  unfolding case_prod_beta using assms .

subsection \<open>Compactness and chain-finiteness\<close>

lemma fst_below_iff: "fst x \ y \ x \ (y, snd x)" for x :: "'a \ 'b"
  by (simp add: below_prod_def)

lemma snd_below_iff: "snd x \ y \ x \ (fst x, y)" for x :: "'a \ 'b"
  by (simp add: below_prod_def)

lemma compact_fst: "compact x \ compact (fst x)"
  by (rule compactI) (simp add: fst_below_iff)

lemma compact_snd: "compact x \ compact (snd x)"
  by (rule compactI) (simp add: snd_below_iff)

lemma compact_Pair: "compact x \ compact y \ compact (x, y)"
  by (rule compactI) (simp add: below_prod_def)

lemma compact_Pair_iff [simp]: "compact (x, y) \ compact x \ compact y"
  apply (safe intro!: compact_Pair)
   apply (drule compact_fst, simp)
  apply (drule compact_snd, simp)
  done

instance prod :: (chfin, chfin) chfin
  apply intro_classes
  apply (erule compact_imp_max_in_chain)
  apply (case_tac "\i. Y i", simp)
  done

section \<open>Discrete cpo types\<close>

datatype 'a discr = Discr "'a::type"

subsection \<open>Discrete cpo class instance\<close>

instantiation discr :: (type) discrete_cpo
begin

definition "((\) :: 'a discr \ 'a discr \ bool) = (=)"

instance
  by standard (simp add: below_discr_def)

end

subsection \<open>\emph{undiscr}\<close>

definition undiscr :: "'a::type discr \ 'a"
  where "undiscr x = (case x of Discr y \ y)"

lemma undiscr_Discr [simp]: "undiscr (Discr x) = x"
  by (simp add: undiscr_def)

lemma Discr_undiscr [simp]: "Discr (undiscr y) = y"
  by (induct y) simp

end

quality99%

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