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