src/HOLCF/Fun_Cpo.thy
author huffman
Wed Nov 10 17:56:08 2010 -0800 (2010-11-10)
changeset 40502 8e92772bc0e8
parent 40091 1ca61fbd8a79
child 40622 e40e9e9769f4
permissions -rw-r--r--
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
     1 (*  Title:      HOLCF/Fun_Cpo.thy
     2     Author:     Franz Regensburger
     3     Author:     Brian Huffman
     4 *)
     5 
     6 header {* Class instances for the full function space *}
     7 
     8 theory Fun_Cpo
     9 imports Adm
    10 begin
    11 
    12 subsection {* Full function space is a partial order *}
    13 
    14 instantiation "fun"  :: (type, below) below
    15 begin
    16 
    17 definition
    18   below_fun_def: "(op \<sqsubseteq>) \<equiv> (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x)"
    19 
    20 instance ..
    21 end
    22 
    23 instance "fun" :: (type, po) po
    24 proof
    25   fix f :: "'a \<Rightarrow> 'b"
    26   show "f \<sqsubseteq> f"
    27     by (simp add: below_fun_def)
    28 next
    29   fix f g :: "'a \<Rightarrow> 'b"
    30   assume "f \<sqsubseteq> g" and "g \<sqsubseteq> f" thus "f = g"
    31     by (simp add: below_fun_def fun_eq_iff below_antisym)
    32 next
    33   fix f g h :: "'a \<Rightarrow> 'b"
    34   assume "f \<sqsubseteq> g" and "g \<sqsubseteq> h" thus "f \<sqsubseteq> h"
    35     unfolding below_fun_def by (fast elim: below_trans)
    36 qed
    37 
    38 lemma fun_below_iff: "f \<sqsubseteq> g \<longleftrightarrow> (\<forall>x. f x \<sqsubseteq> g x)"
    39 by (simp add: below_fun_def)
    40 
    41 lemma fun_belowI: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g"
    42 by (simp add: below_fun_def)
    43 
    44 lemma fun_belowD: "f \<sqsubseteq> g \<Longrightarrow> f x \<sqsubseteq> g x"
    45 by (simp add: below_fun_def)
    46 
    47 subsection {* Full function space is chain complete *}
    48 
    49 text {* Function application is monotone. *}
    50 
    51 lemma monofun_app: "monofun (\<lambda>f. f x)"
    52 by (rule monofunI, simp add: below_fun_def)
    53 
    54 text {* Properties of chains of functions. *}
    55 
    56 lemma fun_chain_iff: "chain S \<longleftrightarrow> (\<forall>x. chain (\<lambda>i. S i x))"
    57 unfolding chain_def fun_below_iff by auto
    58 
    59 lemma ch2ch_fun: "chain S \<Longrightarrow> chain (\<lambda>i. S i x)"
    60 by (simp add: chain_def below_fun_def)
    61 
    62 lemma ch2ch_lambda: "(\<And>x. chain (\<lambda>i. S i x)) \<Longrightarrow> chain S"
    63 by (simp add: chain_def below_fun_def)
    64 
    65 text {* upper bounds of function chains yield upper bound in the po range *}
    66 
    67 lemma ub2ub_fun:
    68   "range S <| u \<Longrightarrow> range (\<lambda>i. S i x) <| u x"
    69 by (auto simp add: is_ub_def below_fun_def)
    70 
    71 text {* Type @{typ "'a::type => 'b::cpo"} is chain complete *}
    72 
    73 lemma is_lub_lambda:
    74   "(\<And>x. range (\<lambda>i. Y i x) <<| f x) \<Longrightarrow> range Y <<| f"
    75 unfolding is_lub_def is_ub_def below_fun_def by simp
    76 
    77 lemma lub_fun:
    78   "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
    79     \<Longrightarrow> range S <<| (\<lambda>x. \<Squnion>i. S i x)"
    80 apply (rule is_lub_lambda)
    81 apply (rule cpo_lubI)
    82 apply (erule ch2ch_fun)
    83 done
    84 
    85 lemma thelub_fun:
    86   "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
    87     \<Longrightarrow> (\<Squnion>i. S i) = (\<lambda>x. \<Squnion>i. S i x)"
    88 by (rule lub_fun [THEN thelubI])
    89 
    90 instance "fun"  :: (type, cpo) cpo
    91 by intro_classes (rule exI, erule lub_fun)
    92 
    93 subsection {* Chain-finiteness of function space *}
    94 
    95 lemma maxinch2maxinch_lambda:
    96   "(\<And>x. max_in_chain n (\<lambda>i. S i x)) \<Longrightarrow> max_in_chain n S"
    97 unfolding max_in_chain_def fun_eq_iff by simp
    98 
    99 lemma maxinch_mono:
   100   "\<lbrakk>max_in_chain i Y; i \<le> j\<rbrakk> \<Longrightarrow> max_in_chain j Y"
   101 unfolding max_in_chain_def
   102 proof (intro allI impI)
   103   fix k
   104   assume Y: "\<forall>n\<ge>i. Y i = Y n"
   105   assume ij: "i \<le> j"
   106   assume jk: "j \<le> k"
   107   from ij jk have ik: "i \<le> k" by simp
   108   from Y ij have Yij: "Y i = Y j" by simp
   109   from Y ik have Yik: "Y i = Y k" by simp
   110   from Yij Yik show "Y j = Y k" by auto
   111 qed
   112 
   113 instance "fun" :: (type, discrete_cpo) discrete_cpo
   114 proof
   115   fix f g :: "'a \<Rightarrow> 'b"
   116   show "f \<sqsubseteq> g \<longleftrightarrow> f = g" 
   117     unfolding fun_below_iff fun_eq_iff
   118     by simp
   119 qed
   120 
   121 subsection {* Full function space is pointed *}
   122 
   123 lemma minimal_fun: "(\<lambda>x. \<bottom>) \<sqsubseteq> f"
   124 by (simp add: below_fun_def)
   125 
   126 instance "fun"  :: (type, pcpo) pcpo
   127 by default (fast intro: minimal_fun)
   128 
   129 lemma inst_fun_pcpo: "\<bottom> = (\<lambda>x. \<bottom>)"
   130 by (rule minimal_fun [THEN UU_I, symmetric])
   131 
   132 lemma app_strict [simp]: "\<bottom> x = \<bottom>"
   133 by (simp add: inst_fun_pcpo)
   134 
   135 lemma lambda_strict: "(\<lambda>x. \<bottom>) = \<bottom>"
   136 by (rule UU_I, rule minimal_fun)
   137 
   138 subsection {* Propagation of monotonicity and continuity *}
   139 
   140 text {* The lub of a chain of monotone functions is monotone. *}
   141 
   142 lemma adm_monofun: "adm monofun"
   143 by (rule admI, simp add: thelub_fun fun_chain_iff monofun_def lub_mono)
   144 
   145 text {* The lub of a chain of continuous functions is continuous. *}
   146 
   147 lemma adm_cont: "adm cont"
   148 by (rule admI, simp add: thelub_fun fun_chain_iff)
   149 
   150 text {* Function application preserves monotonicity and continuity. *}
   151 
   152 lemma mono2mono_fun: "monofun f \<Longrightarrow> monofun (\<lambda>x. f x y)"
   153 by (simp add: monofun_def fun_below_iff)
   154 
   155 lemma cont2cont_fun: "cont f \<Longrightarrow> cont (\<lambda>x. f x y)"
   156 apply (rule contI2)
   157 apply (erule cont2mono [THEN mono2mono_fun])
   158 apply (simp add: cont2contlubE thelub_fun ch2ch_cont)
   159 done
   160 
   161 text {*
   162   Lambda abstraction preserves monotonicity and continuity.
   163   (Note @{text "(\<lambda>x. \<lambda>y. f x y) = f"}.)
   164 *}
   165 
   166 lemma mono2mono_lambda:
   167   assumes f: "\<And>y. monofun (\<lambda>x. f x y)" shows "monofun f"
   168 using f by (simp add: monofun_def fun_below_iff)
   169 
   170 lemma cont2cont_lambda [simp]:
   171   assumes f: "\<And>y. cont (\<lambda>x. f x y)" shows "cont f"
   172 by (rule contI, rule is_lub_lambda, rule contE [OF f])
   173 
   174 text {* What D.A.Schmidt calls continuity of abstraction; never used here *}
   175 
   176 lemma contlub_lambda:
   177   "(\<And>x::'a::type. chain (\<lambda>i. S i x::'b::cpo))
   178     \<Longrightarrow> (\<lambda>x. \<Squnion>i. S i x) = (\<Squnion>i. (\<lambda>x. S i x))"
   179 by (simp add: thelub_fun ch2ch_lambda)
   180 
   181 end