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