src/HOLCF/Fix.thy
changeset 40774 0437dbc127b3
parent 40773 6c12f5e24e34
child 40775 ed7a4eadb2f6
     1.1 --- a/src/HOLCF/Fix.thy	Sat Nov 27 14:34:54 2010 -0800
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,229 +0,0 @@
     1.4 -(*  Title:      HOLCF/Fix.thy
     1.5 -    Author:     Franz Regensburger
     1.6 -    Author:     Brian Huffman
     1.7 -*)
     1.8 -
     1.9 -header {* Fixed point operator and admissibility *}
    1.10 -
    1.11 -theory Fix
    1.12 -imports Cfun
    1.13 -begin
    1.14 -
    1.15 -default_sort pcpo
    1.16 -
    1.17 -subsection {* Iteration *}
    1.18 -
    1.19 -primrec iterate :: "nat \<Rightarrow> ('a::cpo \<rightarrow> 'a) \<rightarrow> ('a \<rightarrow> 'a)" where
    1.20 -    "iterate 0 = (\<Lambda> F x. x)"
    1.21 -  | "iterate (Suc n) = (\<Lambda> F x. F\<cdot>(iterate n\<cdot>F\<cdot>x))"
    1.22 -
    1.23 -text {* Derive inductive properties of iterate from primitive recursion *}
    1.24 -
    1.25 -lemma iterate_0 [simp]: "iterate 0\<cdot>F\<cdot>x = x"
    1.26 -by simp
    1.27 -
    1.28 -lemma iterate_Suc [simp]: "iterate (Suc n)\<cdot>F\<cdot>x = F\<cdot>(iterate n\<cdot>F\<cdot>x)"
    1.29 -by simp
    1.30 -
    1.31 -declare iterate.simps [simp del]
    1.32 -
    1.33 -lemma iterate_Suc2: "iterate (Suc n)\<cdot>F\<cdot>x = iterate n\<cdot>F\<cdot>(F\<cdot>x)"
    1.34 -by (induct n) simp_all
    1.35 -
    1.36 -lemma iterate_iterate:
    1.37 -  "iterate m\<cdot>F\<cdot>(iterate n\<cdot>F\<cdot>x) = iterate (m + n)\<cdot>F\<cdot>x"
    1.38 -by (induct m) simp_all
    1.39 -
    1.40 -text {* The sequence of function iterations is a chain. *}
    1.41 -
    1.42 -lemma chain_iterate [simp]: "chain (\<lambda>i. iterate i\<cdot>F\<cdot>\<bottom>)"
    1.43 -by (rule chainI, unfold iterate_Suc2, rule monofun_cfun_arg, rule minimal)
    1.44 -
    1.45 -
    1.46 -subsection {* Least fixed point operator *}
    1.47 -
    1.48 -definition
    1.49 -  "fix" :: "('a \<rightarrow> 'a) \<rightarrow> 'a" where
    1.50 -  "fix = (\<Lambda> F. \<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>)"
    1.51 -
    1.52 -text {* Binder syntax for @{term fix} *}
    1.53 -
    1.54 -abbreviation
    1.55 -  fix_syn :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"  (binder "FIX " 10) where
    1.56 -  "fix_syn (\<lambda>x. f x) \<equiv> fix\<cdot>(\<Lambda> x. f x)"
    1.57 -
    1.58 -notation (xsymbols)
    1.59 -  fix_syn  (binder "\<mu> " 10)
    1.60 -
    1.61 -text {* Properties of @{term fix} *}
    1.62 -
    1.63 -text {* direct connection between @{term fix} and iteration *}
    1.64 -
    1.65 -lemma fix_def2: "fix\<cdot>F = (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>)"
    1.66 -unfolding fix_def by simp
    1.67 -
    1.68 -lemma iterate_below_fix: "iterate n\<cdot>f\<cdot>\<bottom> \<sqsubseteq> fix\<cdot>f"
    1.69 -  unfolding fix_def2
    1.70 -  using chain_iterate by (rule is_ub_thelub)
    1.71 -
    1.72 -text {*
    1.73 -  Kleene's fixed point theorems for continuous functions in pointed
    1.74 -  omega cpo's
    1.75 -*}
    1.76 -
    1.77 -lemma fix_eq: "fix\<cdot>F = F\<cdot>(fix\<cdot>F)"
    1.78 -apply (simp add: fix_def2)
    1.79 -apply (subst lub_range_shift [of _ 1, symmetric])
    1.80 -apply (rule chain_iterate)
    1.81 -apply (subst contlub_cfun_arg)
    1.82 -apply (rule chain_iterate)
    1.83 -apply simp
    1.84 -done
    1.85 -
    1.86 -lemma fix_least_below: "F\<cdot>x \<sqsubseteq> x \<Longrightarrow> fix\<cdot>F \<sqsubseteq> x"
    1.87 -apply (simp add: fix_def2)
    1.88 -apply (rule lub_below)
    1.89 -apply (rule chain_iterate)
    1.90 -apply (induct_tac i)
    1.91 -apply simp
    1.92 -apply simp
    1.93 -apply (erule rev_below_trans)
    1.94 -apply (erule monofun_cfun_arg)
    1.95 -done
    1.96 -
    1.97 -lemma fix_least: "F\<cdot>x = x \<Longrightarrow> fix\<cdot>F \<sqsubseteq> x"
    1.98 -by (rule fix_least_below, simp)
    1.99 -
   1.100 -lemma fix_eqI:
   1.101 -  assumes fixed: "F\<cdot>x = x" and least: "\<And>z. F\<cdot>z = z \<Longrightarrow> x \<sqsubseteq> z"
   1.102 -  shows "fix\<cdot>F = x"
   1.103 -apply (rule below_antisym)
   1.104 -apply (rule fix_least [OF fixed])
   1.105 -apply (rule least [OF fix_eq [symmetric]])
   1.106 -done
   1.107 -
   1.108 -lemma fix_eq2: "f \<equiv> fix\<cdot>F \<Longrightarrow> f = F\<cdot>f"
   1.109 -by (simp add: fix_eq [symmetric])
   1.110 -
   1.111 -lemma fix_eq3: "f \<equiv> fix\<cdot>F \<Longrightarrow> f\<cdot>x = F\<cdot>f\<cdot>x"
   1.112 -by (erule fix_eq2 [THEN cfun_fun_cong])
   1.113 -
   1.114 -lemma fix_eq4: "f = fix\<cdot>F \<Longrightarrow> f = F\<cdot>f"
   1.115 -apply (erule ssubst)
   1.116 -apply (rule fix_eq)
   1.117 -done
   1.118 -
   1.119 -lemma fix_eq5: "f = fix\<cdot>F \<Longrightarrow> f\<cdot>x = F\<cdot>f\<cdot>x"
   1.120 -by (erule fix_eq4 [THEN cfun_fun_cong])
   1.121 -
   1.122 -text {* strictness of @{term fix} *}
   1.123 -
   1.124 -lemma fix_bottom_iff: "(fix\<cdot>F = \<bottom>) = (F\<cdot>\<bottom> = \<bottom>)"
   1.125 -apply (rule iffI)
   1.126 -apply (erule subst)
   1.127 -apply (rule fix_eq [symmetric])
   1.128 -apply (erule fix_least [THEN UU_I])
   1.129 -done
   1.130 -
   1.131 -lemma fix_strict: "F\<cdot>\<bottom> = \<bottom> \<Longrightarrow> fix\<cdot>F = \<bottom>"
   1.132 -by (simp add: fix_bottom_iff)
   1.133 -
   1.134 -lemma fix_defined: "F\<cdot>\<bottom> \<noteq> \<bottom> \<Longrightarrow> fix\<cdot>F \<noteq> \<bottom>"
   1.135 -by (simp add: fix_bottom_iff)
   1.136 -
   1.137 -text {* @{term fix} applied to identity and constant functions *}
   1.138 -
   1.139 -lemma fix_id: "(\<mu> x. x) = \<bottom>"
   1.140 -by (simp add: fix_strict)
   1.141 -
   1.142 -lemma fix_const: "(\<mu> x. c) = c"
   1.143 -by (subst fix_eq, simp)
   1.144 -
   1.145 -subsection {* Fixed point induction *}
   1.146 -
   1.147 -lemma fix_ind: "\<lbrakk>adm P; P \<bottom>; \<And>x. P x \<Longrightarrow> P (F\<cdot>x)\<rbrakk> \<Longrightarrow> P (fix\<cdot>F)"
   1.148 -unfolding fix_def2
   1.149 -apply (erule admD)
   1.150 -apply (rule chain_iterate)
   1.151 -apply (rule nat_induct, simp_all)
   1.152 -done
   1.153 -
   1.154 -lemma def_fix_ind:
   1.155 -  "\<lbrakk>f \<equiv> fix\<cdot>F; adm P; P \<bottom>; \<And>x. P x \<Longrightarrow> P (F\<cdot>x)\<rbrakk> \<Longrightarrow> P f"
   1.156 -by (simp add: fix_ind)
   1.157 -
   1.158 -lemma fix_ind2:
   1.159 -  assumes adm: "adm P"
   1.160 -  assumes 0: "P \<bottom>" and 1: "P (F\<cdot>\<bottom>)"
   1.161 -  assumes step: "\<And>x. \<lbrakk>P x; P (F\<cdot>x)\<rbrakk> \<Longrightarrow> P (F\<cdot>(F\<cdot>x))"
   1.162 -  shows "P (fix\<cdot>F)"
   1.163 -unfolding fix_def2
   1.164 -apply (rule admD [OF adm chain_iterate])
   1.165 -apply (rule nat_less_induct)
   1.166 -apply (case_tac n)
   1.167 -apply (simp add: 0)
   1.168 -apply (case_tac nat)
   1.169 -apply (simp add: 1)
   1.170 -apply (frule_tac x=nat in spec)
   1.171 -apply (simp add: step)
   1.172 -done
   1.173 -
   1.174 -lemma parallel_fix_ind:
   1.175 -  assumes adm: "adm (\<lambda>x. P (fst x) (snd x))"
   1.176 -  assumes base: "P \<bottom> \<bottom>"
   1.177 -  assumes step: "\<And>x y. P x y \<Longrightarrow> P (F\<cdot>x) (G\<cdot>y)"
   1.178 -  shows "P (fix\<cdot>F) (fix\<cdot>G)"
   1.179 -proof -
   1.180 -  from adm have adm': "adm (split P)"
   1.181 -    unfolding split_def .
   1.182 -  have "\<And>i. P (iterate i\<cdot>F\<cdot>\<bottom>) (iterate i\<cdot>G\<cdot>\<bottom>)"
   1.183 -    by (induct_tac i, simp add: base, simp add: step)
   1.184 -  hence "\<And>i. split P (iterate i\<cdot>F\<cdot>\<bottom>, iterate i\<cdot>G\<cdot>\<bottom>)"
   1.185 -    by simp
   1.186 -  hence "split P (\<Squnion>i. (iterate i\<cdot>F\<cdot>\<bottom>, iterate i\<cdot>G\<cdot>\<bottom>))"
   1.187 -    by - (rule admD [OF adm'], simp, assumption)
   1.188 -  hence "split P (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>, \<Squnion>i. iterate i\<cdot>G\<cdot>\<bottom>)"
   1.189 -    by (simp add: lub_Pair)
   1.190 -  hence "P (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>) (\<Squnion>i. iterate i\<cdot>G\<cdot>\<bottom>)"
   1.191 -    by simp
   1.192 -  thus "P (fix\<cdot>F) (fix\<cdot>G)"
   1.193 -    by (simp add: fix_def2)
   1.194 -qed
   1.195 -
   1.196 -subsection {* Fixed-points on product types *}
   1.197 -
   1.198 -text {*
   1.199 -  Bekic's Theorem: Simultaneous fixed points over pairs
   1.200 -  can be written in terms of separate fixed points.
   1.201 -*}
   1.202 -
   1.203 -lemma fix_cprod:
   1.204 -  "fix\<cdot>(F::'a \<times> 'b \<rightarrow> 'a \<times> 'b) =
   1.205 -   (\<mu> x. fst (F\<cdot>(x, \<mu> y. snd (F\<cdot>(x, y)))),
   1.206 -    \<mu> y. snd (F\<cdot>(\<mu> x. fst (F\<cdot>(x, \<mu> y. snd (F\<cdot>(x, y)))), y)))"
   1.207 -  (is "fix\<cdot>F = (?x, ?y)")
   1.208 -proof (rule fix_eqI)
   1.209 -  have 1: "fst (F\<cdot>(?x, ?y)) = ?x"
   1.210 -    by (rule trans [symmetric, OF fix_eq], simp)
   1.211 -  have 2: "snd (F\<cdot>(?x, ?y)) = ?y"
   1.212 -    by (rule trans [symmetric, OF fix_eq], simp)
   1.213 -  from 1 2 show "F\<cdot>(?x, ?y) = (?x, ?y)" by (simp add: Pair_fst_snd_eq)
   1.214 -next
   1.215 -  fix z assume F_z: "F\<cdot>z = z"
   1.216 -  obtain x y where z: "z = (x,y)" by (rule prod.exhaust)
   1.217 -  from F_z z have F_x: "fst (F\<cdot>(x, y)) = x" by simp
   1.218 -  from F_z z have F_y: "snd (F\<cdot>(x, y)) = y" by simp
   1.219 -  let ?y1 = "\<mu> y. snd (F\<cdot>(x, y))"
   1.220 -  have "?y1 \<sqsubseteq> y" by (rule fix_least, simp add: F_y)
   1.221 -  hence "fst (F\<cdot>(x, ?y1)) \<sqsubseteq> fst (F\<cdot>(x, y))"
   1.222 -    by (simp add: fst_monofun monofun_cfun)
   1.223 -  hence "fst (F\<cdot>(x, ?y1)) \<sqsubseteq> x" using F_x by simp
   1.224 -  hence 1: "?x \<sqsubseteq> x" by (simp add: fix_least_below)
   1.225 -  hence "snd (F\<cdot>(?x, y)) \<sqsubseteq> snd (F\<cdot>(x, y))"
   1.226 -    by (simp add: snd_monofun monofun_cfun)
   1.227 -  hence "snd (F\<cdot>(?x, y)) \<sqsubseteq> y" using F_y by simp
   1.228 -  hence 2: "?y \<sqsubseteq> y" by (simp add: fix_least_below)
   1.229 -  show "(?x, ?y) \<sqsubseteq> z" using z 1 2 by simp
   1.230 -qed
   1.231 -
   1.232 -end