Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Cont.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/HOLCF/Cont.thy
    Author:     Franz Regensburger
    Author:     Brian Huffman
*)

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

theory Cont
  imports Pcpo
begin

text \<open>
   Now we change the default class! Form now on all untyped type variables are
   of default class po
\<close>

default_sort po

subsection \<open>Definitions\<close>

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

definition cont :: "('a::cpo \ 'b::cpo) \ 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::cpo \ 'b::cpo"
  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::cpo \ 'b::cpo \ 'c::cpo" 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::cpo"
  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::cpo"
  apply (rule contI)
  apply (drule discrete_chain_const, clarify)
  apply simp
  done

end

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