src/HOLCF/Fix.thy
 author haftmann Tue Jul 10 17:30:50 2007 +0200 (2007-07-10) changeset 23709 fd31da8f752a parent 18095 4328356ab7e6 child 25131 2c8caac48ade permissions -rw-r--r--
moved lfp_induct2 here
```     1 (*  Title:      HOLCF/Fix.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Franz Regensburger
```
```     4
```
```     5 Definitions for fixed point operator and admissibility.
```
```     6 *)
```
```     7
```
```     8 header {* Fixed point operator and admissibility *}
```
```     9
```
```    10 theory Fix
```
```    11 imports Cfun Cprod Adm
```
```    12 begin
```
```    13
```
```    14 defaultsort pcpo
```
```    15
```
```    16 subsection {* Iteration *}
```
```    17
```
```    18 consts
```
```    19   iterate :: "nat \<Rightarrow> ('a::cpo \<rightarrow> 'a) \<rightarrow> ('a \<rightarrow> 'a)"
```
```    20
```
```    21 primrec
```
```    22   "iterate 0 = (\<Lambda> F x. x)"
```
```    23   "iterate (Suc n) = (\<Lambda> F x. F\<cdot>(iterate n\<cdot>F\<cdot>x))"
```
```    24
```
```    25 text {* Derive inductive properties of iterate from primitive recursion *}
```
```    26
```
```    27 lemma iterate_0 [simp]: "iterate 0\<cdot>F\<cdot>x = x"
```
```    28 by simp
```
```    29
```
```    30 lemma iterate_Suc [simp]: "iterate (Suc n)\<cdot>F\<cdot>x = F\<cdot>(iterate n\<cdot>F\<cdot>x)"
```
```    31 by simp
```
```    32
```
```    33 declare iterate.simps [simp del]
```
```    34
```
```    35 lemma iterate_Suc2: "iterate (Suc n)\<cdot>F\<cdot>x = iterate n\<cdot>F\<cdot>(F\<cdot>x)"
```
```    36 by (induct_tac n, auto)
```
```    37
```
```    38 text {*
```
```    39   The sequence of function iterations is a chain.
```
```    40   This property is essential since monotonicity of iterate makes no sense.
```
```    41 *}
```
```    42
```
```    43 lemma chain_iterate2: "x \<sqsubseteq> F\<cdot>x \<Longrightarrow> chain (\<lambda>i. iterate i\<cdot>F\<cdot>x)"
```
```    44 by (rule chainI, induct_tac i, auto elim: monofun_cfun_arg)
```
```    45
```
```    46 lemma chain_iterate [simp]: "chain (\<lambda>i. iterate i\<cdot>F\<cdot>\<bottom>)"
```
```    47 by (rule chain_iterate2 [OF minimal])
```
```    48
```
```    49
```
```    50 subsection {* Least fixed point operator *}
```
```    51
```
```    52 constdefs
```
```    53   "fix" :: "('a \<rightarrow> 'a) \<rightarrow> 'a"
```
```    54   "fix \<equiv> \<Lambda> F. \<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>"
```
```    55
```
```    56 text {* Binder syntax for @{term fix} *}
```
```    57
```
```    58 syntax
```
```    59   "_FIX" :: "['a, 'a] \<Rightarrow> 'a" ("(3FIX _./ _)" [1000, 10] 10)
```
```    60
```
```    61 syntax (xsymbols)
```
```    62   "_FIX" :: "['a, 'a] \<Rightarrow> 'a" ("(3\<mu>_./ _)" [1000, 10] 10)
```
```    63
```
```    64 translations
```
```    65   "\<mu> x. t" == "fix\<cdot>(\<Lambda> x. t)"
```
```    66
```
```    67 text {* Properties of @{term fix} *}
```
```    68
```
```    69 text {* direct connection between @{term fix} and iteration *}
```
```    70
```
```    71 lemma fix_def2: "fix\<cdot>F = (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>)"
```
```    72 apply (unfold fix_def)
```
```    73 apply (rule beta_cfun)
```
```    74 apply (rule cont2cont_lub)
```
```    75 apply (rule ch2ch_lambda)
```
```    76 apply (rule chain_iterate)
```
```    77 apply simp
```
```    78 done
```
```    79
```
```    80 text {*
```
```    81   Kleene's fixed point theorems for continuous functions in pointed
```
```    82   omega cpo's
```
```    83 *}
```
```    84
```
```    85 lemma fix_eq: "fix\<cdot>F = F\<cdot>(fix\<cdot>F)"
```
```    86 apply (simp add: fix_def2)
```
```    87 apply (subst lub_range_shift [of _ 1, symmetric])
```
```    88 apply (rule chain_iterate)
```
```    89 apply (subst contlub_cfun_arg)
```
```    90 apply (rule chain_iterate)
```
```    91 apply simp
```
```    92 done
```
```    93
```
```    94 lemma fix_least_less: "F\<cdot>x \<sqsubseteq> x \<Longrightarrow> fix\<cdot>F \<sqsubseteq> x"
```
```    95 apply (simp add: fix_def2)
```
```    96 apply (rule is_lub_thelub)
```
```    97 apply (rule chain_iterate)
```
```    98 apply (rule ub_rangeI)
```
```    99 apply (induct_tac i)
```
```   100 apply simp
```
```   101 apply simp
```
```   102 apply (erule rev_trans_less)
```
```   103 apply (erule monofun_cfun_arg)
```
```   104 done
```
```   105
```
```   106 lemma fix_least: "F\<cdot>x = x \<Longrightarrow> fix\<cdot>F \<sqsubseteq> x"
```
```   107 by (rule fix_least_less, simp)
```
```   108
```
```   109 lemma fix_eqI: "\<lbrakk>F\<cdot>x = x; \<forall>z. F\<cdot>z = z \<longrightarrow> x \<sqsubseteq> z\<rbrakk> \<Longrightarrow> x = fix\<cdot>F"
```
```   110 apply (rule antisym_less)
```
```   111 apply (simp add: fix_eq [symmetric])
```
```   112 apply (erule fix_least)
```
```   113 done
```
```   114
```
```   115 lemma fix_eq2: "f \<equiv> fix\<cdot>F \<Longrightarrow> f = F\<cdot>f"
```
```   116 by (simp add: fix_eq [symmetric])
```
```   117
```
```   118 lemma fix_eq3: "f \<equiv> fix\<cdot>F \<Longrightarrow> f\<cdot>x = F\<cdot>f\<cdot>x"
```
```   119 by (erule fix_eq2 [THEN cfun_fun_cong])
```
```   120
```
```   121 lemma fix_eq4: "f = fix\<cdot>F \<Longrightarrow> f = F\<cdot>f"
```
```   122 apply (erule ssubst)
```
```   123 apply (rule fix_eq)
```
```   124 done
```
```   125
```
```   126 lemma fix_eq5: "f = fix\<cdot>F \<Longrightarrow> f\<cdot>x = F\<cdot>f\<cdot>x"
```
```   127 by (erule fix_eq4 [THEN cfun_fun_cong])
```
```   128
```
```   129 text {* strictness of @{term fix} *}
```
```   130
```
```   131 lemma fix_defined_iff: "(fix\<cdot>F = \<bottom>) = (F\<cdot>\<bottom> = \<bottom>)"
```
```   132 apply (rule iffI)
```
```   133 apply (erule subst)
```
```   134 apply (rule fix_eq [symmetric])
```
```   135 apply (erule fix_least [THEN UU_I])
```
```   136 done
```
```   137
```
```   138 lemma fix_strict: "F\<cdot>\<bottom> = \<bottom> \<Longrightarrow> fix\<cdot>F = \<bottom>"
```
```   139 by (simp add: fix_defined_iff)
```
```   140
```
```   141 lemma fix_defined: "F\<cdot>\<bottom> \<noteq> \<bottom> \<Longrightarrow> fix\<cdot>F \<noteq> \<bottom>"
```
```   142 by (simp add: fix_defined_iff)
```
```   143
```
```   144 text {* @{term fix} applied to identity and constant functions *}
```
```   145
```
```   146 lemma fix_id: "(\<mu> x. x) = \<bottom>"
```
```   147 by (simp add: fix_strict)
```
```   148
```
```   149 lemma fix_const: "(\<mu> x. c) = c"
```
```   150 by (subst fix_eq, simp)
```
```   151
```
```   152 subsection {* Fixed point induction *}
```
```   153
```
```   154 lemma fix_ind: "\<lbrakk>adm P; P \<bottom>; \<And>x. P x \<Longrightarrow> P (F\<cdot>x)\<rbrakk> \<Longrightarrow> P (fix\<cdot>F)"
```
```   155 apply (subst fix_def2)
```
```   156 apply (erule admD [rule_format])
```
```   157 apply (rule chain_iterate)
```
```   158 apply (induct_tac "i", simp_all)
```
```   159 done
```
```   160
```
```   161 lemma def_fix_ind:
```
```   162   "\<lbrakk>f \<equiv> fix\<cdot>F; adm P; P \<bottom>; \<And>x. P x \<Longrightarrow> P (F\<cdot>x)\<rbrakk> \<Longrightarrow> P f"
```
```   163 by (simp add: fix_ind)
```
```   164
```
```   165 subsection {* Recursive let bindings *}
```
```   166
```
```   167 constdefs
```
```   168   CLetrec :: "('a \<rightarrow> 'a \<times> 'b) \<rightarrow> 'b"
```
```   169   "CLetrec \<equiv> \<Lambda> F. csnd\<cdot>(F\<cdot>(\<mu> x. cfst\<cdot>(F\<cdot>x)))"
```
```   170
```
```   171 nonterminals
```
```   172   recbinds recbindt recbind
```
```   173
```
```   174 syntax
```
```   175   "_recbind"  :: "['a, 'a] \<Rightarrow> recbind"               ("(2_ =/ _)" 10)
```
```   176   ""          :: "recbind \<Rightarrow> recbindt"               ("_")
```
```   177   "_recbindt" :: "[recbind, recbindt] \<Rightarrow> recbindt"   ("_,/ _")
```
```   178   ""          :: "recbindt \<Rightarrow> recbinds"              ("_")
```
```   179   "_recbinds" :: "[recbindt, recbinds] \<Rightarrow> recbinds"  ("_;/ _")
```
```   180   "_Letrec"   :: "[recbinds, 'a] \<Rightarrow> 'a"      ("(Letrec (_)/ in (_))" 10)
```
```   181
```
```   182 translations
```
```   183   (recbindt) "x = a, \<langle>y,ys\<rangle> = \<langle>b,bs\<rangle>" == (recbindt) "\<langle>x,y,ys\<rangle> = \<langle>a,b,bs\<rangle>"
```
```   184   (recbindt) "x = a, y = b"           == (recbindt) "\<langle>x,y\<rangle> = \<langle>a,b\<rangle>"
```
```   185
```
```   186 translations
```
```   187   "_Letrec (_recbinds b bs) e" == "_Letrec b (_Letrec bs e)"
```
```   188   "Letrec xs = a in \<langle>e,es\<rangle>"    == "CLetrec\<cdot>(\<Lambda> xs. \<langle>a,e,es\<rangle>)"
```
```   189   "Letrec xs = a in e"         == "CLetrec\<cdot>(\<Lambda> xs. \<langle>a,e\<rangle>)"
```
```   190
```
```   191 text {*
```
```   192   Bekic's Theorem: Simultaneous fixed points over pairs
```
```   193   can be written in terms of separate fixed points.
```
```   194 *}
```
```   195
```
```   196 lemma fix_cprod:
```
```   197   "fix\<cdot>(F::'a \<times> 'b \<rightarrow> 'a \<times> 'b) =
```
```   198    \<langle>\<mu> x. cfst\<cdot>(F\<cdot>\<langle>x, \<mu> y. csnd\<cdot>(F\<cdot>\<langle>x, y\<rangle>)\<rangle>),
```
```   199     \<mu> y. csnd\<cdot>(F\<cdot>\<langle>\<mu> x. cfst\<cdot>(F\<cdot>\<langle>x, \<mu> y. csnd\<cdot>(F\<cdot>\<langle>x, y\<rangle>)\<rangle>), y\<rangle>)\<rangle>"
```
```   200   (is "fix\<cdot>F = \<langle>?x, ?y\<rangle>")
```
```   201 proof (rule fix_eqI [rule_format, symmetric])
```
```   202   have 1: "cfst\<cdot>(F\<cdot>\<langle>?x, ?y\<rangle>) = ?x"
```
```   203     by (rule trans [symmetric, OF fix_eq], simp)
```
```   204   have 2: "csnd\<cdot>(F\<cdot>\<langle>?x, ?y\<rangle>) = ?y"
```
```   205     by (rule trans [symmetric, OF fix_eq], simp)
```
```   206   from 1 2 show "F\<cdot>\<langle>?x, ?y\<rangle> = \<langle>?x, ?y\<rangle>" by (simp add: eq_cprod)
```
```   207 next
```
```   208   fix z assume F_z: "F\<cdot>z = z"
```
```   209   then obtain x y where z: "z = \<langle>x,y\<rangle>" by (rule_tac p=z in cprodE)
```
```   210   from F_z z have F_x: "cfst\<cdot>(F\<cdot>\<langle>x, y\<rangle>) = x" by simp
```
```   211   from F_z z have F_y: "csnd\<cdot>(F\<cdot>\<langle>x, y\<rangle>) = y" by simp
```
```   212   let ?y1 = "\<mu> y. csnd\<cdot>(F\<cdot>\<langle>x, y\<rangle>)"
```
```   213   have "?y1 \<sqsubseteq> y" by (rule fix_least, simp add: F_y)
```
```   214   hence "cfst\<cdot>(F\<cdot>\<langle>x, ?y1\<rangle>) \<sqsubseteq> cfst\<cdot>(F\<cdot>\<langle>x, y\<rangle>)" by (simp add: monofun_cfun)
```
```   215   hence "cfst\<cdot>(F\<cdot>\<langle>x, ?y1\<rangle>) \<sqsubseteq> x" using F_x by simp
```
```   216   hence 1: "?x \<sqsubseteq> x" by (simp add: fix_least_less)
```
```   217   hence "csnd\<cdot>(F\<cdot>\<langle>?x, y\<rangle>) \<sqsubseteq> csnd\<cdot>(F\<cdot>\<langle>x, y\<rangle>)" by (simp add: monofun_cfun)
```
```   218   hence "csnd\<cdot>(F\<cdot>\<langle>?x, y\<rangle>) \<sqsubseteq> y" using F_y by simp
```
```   219   hence 2: "?y \<sqsubseteq> y" by (simp add: fix_least_less)
```
```   220   show "\<langle>?x, ?y\<rangle> \<sqsubseteq> z" using z 1 2 by simp
```
```   221 qed
```
```   222
```
```   223 subsection {* Weak admissibility *}
```
```   224
```
```   225 constdefs
```
```   226   admw :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
```
```   227   "admw P \<equiv> \<forall>F. (\<forall>n. P (iterate n\<cdot>F\<cdot>\<bottom>)) \<longrightarrow> P (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>)"
```
```   228
```
```   229 text {* an admissible formula is also weak admissible *}
```
```   230
```
```   231 lemma adm_impl_admw: "adm P \<Longrightarrow> admw P"
```
```   232 apply (unfold admw_def)
```
```   233 apply (intro strip)
```
```   234 apply (erule admD)
```
```   235 apply (rule chain_iterate)
```
```   236 apply assumption
```
```   237 done
```
```   238
```
```   239 text {* computational induction for weak admissible formulae *}
```
```   240
```
```   241 lemma wfix_ind: "\<lbrakk>admw P; \<forall>n. P (iterate n\<cdot>F\<cdot>\<bottom>)\<rbrakk> \<Longrightarrow> P (fix\<cdot>F)"
```
```   242 by (simp add: fix_def2 admw_def)
```
```   243
```
```   244 lemma def_wfix_ind:
```
```   245   "\<lbrakk>f \<equiv> fix\<cdot>F; admw P; \<forall>n. P (iterate n\<cdot>F\<cdot>\<bottom>)\<rbrakk> \<Longrightarrow> P f"
```
```   246 by (simp, rule wfix_ind)
```
```   247
```
```   248 end
```