cleaned up Fun_Cpo.thy; deprecated a few theorem names
authorhuffman
Wed Oct 13 10:56:42 2010 -0700 (2010-10-13)
changeset 40011b974cf829099
parent 40010 d7fdd84b959f
child 40012 f13341a45407
cleaned up Fun_Cpo.thy; deprecated a few theorem names
src/HOLCF/Cfun.thy
src/HOLCF/Fun_Cpo.thy
src/HOLCF/HOLCF.thy
     1.1 --- a/src/HOLCF/Cfun.thy	Wed Oct 13 10:27:26 2010 -0700
     1.2 +++ b/src/HOLCF/Cfun.thy	Wed Oct 13 10:56:42 2010 -0700
     1.3 @@ -13,14 +13,8 @@
     1.4  
     1.5  subsection {* Definition of continuous function type *}
     1.6  
     1.7 -lemma Ex_cont: "\<exists>f. cont f"
     1.8 -by (rule exI, rule cont_const)
     1.9 -
    1.10 -lemma adm_cont: "adm cont"
    1.11 -by (rule admI, rule cont_lub_fun)
    1.12 -
    1.13  cpodef (CFun)  ('a, 'b) cfun (infixr "->" 0) = "{f::'a => 'b. cont f}"
    1.14 -by (simp_all add: Ex_cont adm_cont)
    1.15 +by (auto intro: cont_const adm_cont)
    1.16  
    1.17  type_notation (xsymbols)
    1.18    cfun  ("(_ \<rightarrow>/ _)" [1, 0] 0)
     2.1 --- a/src/HOLCF/Fun_Cpo.thy	Wed Oct 13 10:27:26 2010 -0700
     2.2 +++ b/src/HOLCF/Fun_Cpo.thy	Wed Oct 13 10:56:42 2010 -0700
     2.3 @@ -6,7 +6,7 @@
     2.4  header {* Class instances for the full function space *}
     2.5  
     2.6  theory Fun_Cpo
     2.7 -imports Cont
     2.8 +imports Adm
     2.9  begin
    2.10  
    2.11  subsection {* Full function space is a partial order *}
    2.12 @@ -41,14 +41,20 @@
    2.13  lemma fun_belowI: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g"
    2.14  by (simp add: below_fun_def)
    2.15  
    2.16 +lemma fun_belowD: "f \<sqsubseteq> g \<Longrightarrow> f x \<sqsubseteq> g x"
    2.17 +by (simp add: below_fun_def)
    2.18 +
    2.19  subsection {* Full function space is chain complete *}
    2.20  
    2.21 -text {* function application is monotone *}
    2.22 +text {* Function application is monotone. *}
    2.23  
    2.24  lemma monofun_app: "monofun (\<lambda>f. f x)"
    2.25  by (rule monofunI, simp add: below_fun_def)
    2.26  
    2.27 -text {* chains of functions yield chains in the po range *}
    2.28 +text {* Properties of chains of functions. *}
    2.29 +
    2.30 +lemma fun_chain_iff: "chain S \<longleftrightarrow> (\<forall>x. chain (\<lambda>i. S i x))"
    2.31 +unfolding chain_def fun_below_iff by auto
    2.32  
    2.33  lemma ch2ch_fun: "chain S \<Longrightarrow> chain (\<lambda>i. S i x)"
    2.34  by (simp add: chain_def below_fun_def)
    2.35 @@ -65,16 +71,8 @@
    2.36  text {* Type @{typ "'a::type => 'b::cpo"} is chain complete *}
    2.37  
    2.38  lemma is_lub_lambda:
    2.39 -  assumes f: "\<And>x. range (\<lambda>i. Y i x) <<| f x"
    2.40 -  shows "range Y <<| f"
    2.41 -apply (rule is_lubI)
    2.42 -apply (rule ub_rangeI)
    2.43 -apply (rule fun_belowI)
    2.44 -apply (rule is_ub_lub [OF f])
    2.45 -apply (rule fun_belowI)
    2.46 -apply (rule is_lub_lub [OF f])
    2.47 -apply (erule ub2ub_fun)
    2.48 -done
    2.49 +  "(\<And>x. range (\<lambda>i. Y i x) <<| f x) \<Longrightarrow> range Y <<| f"
    2.50 +unfolding is_lub_def is_ub_def below_fun_def by simp
    2.51  
    2.52  lemma lub_fun:
    2.53    "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
    2.54 @@ -92,17 +90,7 @@
    2.55  instance "fun"  :: (type, cpo) cpo
    2.56  by intro_classes (rule exI, erule lub_fun)
    2.57  
    2.58 -instance "fun" :: (finite, finite_po) finite_po ..
    2.59 -
    2.60 -instance "fun" :: (type, discrete_cpo) discrete_cpo
    2.61 -proof
    2.62 -  fix f g :: "'a \<Rightarrow> 'b"
    2.63 -  show "f \<sqsubseteq> g \<longleftrightarrow> f = g" 
    2.64 -    unfolding fun_below_iff fun_eq_iff
    2.65 -    by simp
    2.66 -qed
    2.67 -
    2.68 -text {* chain-finite function spaces *}
    2.69 +subsection {* Chain-finiteness of function space *}
    2.70  
    2.71  lemma maxinch2maxinch_lambda:
    2.72    "(\<And>x. max_in_chain n (\<lambda>i. S i x)) \<Longrightarrow> max_in_chain n S"
    2.73 @@ -140,94 +128,68 @@
    2.74    thus "\<exists>n. max_in_chain n Y" ..
    2.75  qed
    2.76  
    2.77 +instance "fun" :: (finite, finite_po) finite_po ..
    2.78 +
    2.79 +instance "fun" :: (type, discrete_cpo) discrete_cpo
    2.80 +proof
    2.81 +  fix f g :: "'a \<Rightarrow> 'b"
    2.82 +  show "f \<sqsubseteq> g \<longleftrightarrow> f = g" 
    2.83 +    unfolding fun_below_iff fun_eq_iff
    2.84 +    by simp
    2.85 +qed
    2.86 +
    2.87  subsection {* Full function space is pointed *}
    2.88  
    2.89  lemma minimal_fun: "(\<lambda>x. \<bottom>) \<sqsubseteq> f"
    2.90  by (simp add: below_fun_def)
    2.91  
    2.92 -lemma least_fun: "\<exists>x::'a::type \<Rightarrow> 'b::pcpo. \<forall>y. x \<sqsubseteq> y"
    2.93 -apply (rule_tac x = "\<lambda>x. \<bottom>" in exI)
    2.94 -apply (rule minimal_fun [THEN allI])
    2.95 -done
    2.96 +instance "fun"  :: (type, pcpo) pcpo
    2.97 +by default (fast intro: minimal_fun)
    2.98  
    2.99 -instance "fun"  :: (type, pcpo) pcpo
   2.100 -by intro_classes (rule least_fun)
   2.101 -
   2.102 -text {* for compatibility with old HOLCF-Version *}
   2.103  lemma inst_fun_pcpo: "\<bottom> = (\<lambda>x. \<bottom>)"
   2.104  by (rule minimal_fun [THEN UU_I, symmetric])
   2.105  
   2.106 -text {* function application is strict in the left argument *}
   2.107  lemma app_strict [simp]: "\<bottom> x = \<bottom>"
   2.108  by (simp add: inst_fun_pcpo)
   2.109  
   2.110 -text {*
   2.111 -  The following results are about application for functions in @{typ "'a=>'b"}
   2.112 -*}
   2.113 -
   2.114 -lemma monofun_fun_fun: "f \<sqsubseteq> g \<Longrightarrow> f x \<sqsubseteq> g x"
   2.115 -by (simp add: below_fun_def)
   2.116 -
   2.117 -lemma monofun_fun_arg: "\<lbrakk>monofun f; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> f y"
   2.118 -by (rule monofunE)
   2.119 -
   2.120 -lemma monofun_fun: "\<lbrakk>monofun f; monofun g; f \<sqsubseteq> g; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> g y"
   2.121 -by (rule below_trans [OF monofun_fun_arg monofun_fun_fun])
   2.122 +lemma lambda_strict: "(\<lambda>x. \<bottom>) = \<bottom>"
   2.123 +by (rule UU_I, rule minimal_fun)
   2.124  
   2.125  subsection {* Propagation of monotonicity and continuity *}
   2.126  
   2.127 -text {* the lub of a chain of monotone functions is monotone *}
   2.128 +text {* The lub of a chain of monotone functions is monotone. *}
   2.129 +
   2.130 +lemma adm_monofun: "adm monofun"
   2.131 +by (rule admI, simp add: thelub_fun fun_chain_iff monofun_def lub_mono)
   2.132  
   2.133 -lemma monofun_lub_fun:
   2.134 -  "\<lbrakk>chain (F::nat \<Rightarrow> 'a \<Rightarrow> 'b::cpo); \<forall>i. monofun (F i)\<rbrakk>
   2.135 -    \<Longrightarrow> monofun (\<Squnion>i. F i)"
   2.136 -apply (rule monofunI)
   2.137 -apply (simp add: thelub_fun)
   2.138 -apply (rule lub_mono)
   2.139 -apply (erule ch2ch_fun)
   2.140 -apply (erule ch2ch_fun)
   2.141 -apply (simp add: monofunE)
   2.142 -done
   2.143 +text {* The lub of a chain of continuous functions is continuous. *}
   2.144  
   2.145 -text {* the lub of a chain of continuous functions is continuous *}
   2.146 +lemma adm_cont: "adm cont"
   2.147 +by (rule admI, simp add: thelub_fun fun_chain_iff)
   2.148  
   2.149 -lemma cont_lub_fun:
   2.150 -  "\<lbrakk>chain F; \<forall>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<Squnion>i. F i)"
   2.151 -apply (rule contI2)
   2.152 -apply (erule monofun_lub_fun)
   2.153 -apply (simp add: cont2mono)
   2.154 -apply (simp add: thelub_fun cont2contlubE)
   2.155 -apply (simp add: diag_lub ch2ch_fun ch2ch_cont)
   2.156 -done
   2.157 +text {* Function application preserves monotonicity and continuity. *}
   2.158  
   2.159  lemma mono2mono_fun: "monofun f \<Longrightarrow> monofun (\<lambda>x. f x y)"
   2.160 -apply (rule monofunI)
   2.161 -apply (erule (1) monofun_fun_arg [THEN monofun_fun_fun])
   2.162 -done
   2.163 +by (simp add: monofun_def fun_below_iff)
   2.164  
   2.165  lemma cont2cont_fun: "cont f \<Longrightarrow> cont (\<lambda>x. f x y)"
   2.166  apply (rule contI2)
   2.167  apply (erule cont2mono [THEN mono2mono_fun])
   2.168 -apply (simp add: cont2contlubE)
   2.169 -apply (simp add: thelub_fun ch2ch_cont)
   2.170 +apply (simp add: cont2contlubE thelub_fun ch2ch_cont)
   2.171  done
   2.172  
   2.173 -text {* Note @{text "(\<lambda>x. \<lambda>y. f x y) = f"} *}
   2.174 +text {*
   2.175 +  Lambda abstraction preserves monotonicity and continuity.
   2.176 +  (Note @{text "(\<lambda>x. \<lambda>y. f x y) = f"}.)
   2.177 +*}
   2.178  
   2.179  lemma mono2mono_lambda:
   2.180    assumes f: "\<And>y. monofun (\<lambda>x. f x y)" shows "monofun f"
   2.181 -apply (rule monofunI)
   2.182 -apply (rule fun_belowI)
   2.183 -apply (erule monofunE [OF f])
   2.184 -done
   2.185 +using f by (simp add: monofun_def fun_below_iff)
   2.186  
   2.187  lemma cont2cont_lambda [simp]:
   2.188    assumes f: "\<And>y. cont (\<lambda>x. f x y)" shows "cont f"
   2.189 -apply (rule contI2)
   2.190 -apply (simp add: mono2mono_lambda cont2mono f)
   2.191 -apply (rule fun_belowI)
   2.192 -apply (simp add: thelub_fun cont2contlubE [OF f])
   2.193 -done
   2.194 +by (rule contI, rule is_lub_lambda, rule contE [OF f])
   2.195  
   2.196  text {* What D.A.Schmidt calls continuity of abstraction; never used here *}
   2.197  
     3.1 --- a/src/HOLCF/HOLCF.thy	Wed Oct 13 10:27:26 2010 -0700
     3.2 +++ b/src/HOLCF/HOLCF.thy	Wed Oct 13 10:56:42 2010 -0700
     3.3 @@ -23,6 +23,10 @@
     3.4  lemmas ext_cfun = cfun_eqI
     3.5  lemmas expand_cfun_below = cfun_below_iff
     3.6  lemmas below_cfun_ext = cfun_belowI
     3.7 +lemmas monofun_fun_fun = fun_belowD
     3.8 +lemmas monofun_fun_arg = monofunE
     3.9 +lemmas monofun_lub_fun = adm_monofun [THEN admD]
    3.10 +lemmas cont_lub_fun = adm_cont [THEN admD]
    3.11  
    3.12  text {* Older legacy theorem names: *}
    3.13