add rules for least/greatest fixed point calculus
authorhoelzl
Mon May 04 18:04:01 2015 +0200 (2015-05-04)
changeset 601736a61bb577d5b
parent 60172 423273355b55
child 60174 70d8f7abde8f
add rules for least/greatest fixed point calculus
src/HOL/Inductive.thy
     1.1 --- a/src/HOL/Inductive.thy	Mon May 04 17:35:31 2015 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Mon May 04 18:04:01 2015 +0200
     1.3 @@ -248,6 +248,103 @@
     1.4  lemma gfp_mono: "(!!Z. f Z \<le> g Z) ==> gfp f \<le> gfp g"
     1.5    by (rule gfp_upperbound [THEN gfp_least], blast intro: order_trans)
     1.6  
     1.7 +subsection {* Rules for fixed point calculus *}
     1.8 +
     1.9 +
    1.10 +lemma lfp_rolling:
    1.11 +  assumes "mono g" "mono f"
    1.12 +  shows "g (lfp (\<lambda>x. f (g x))) = lfp (\<lambda>x. g (f x))"
    1.13 +proof (rule antisym)
    1.14 +  have *: "mono (\<lambda>x. f (g x))"
    1.15 +    using assms by (auto simp: mono_def)
    1.16 +
    1.17 +  show "lfp (\<lambda>x. g (f x)) \<le> g (lfp (\<lambda>x. f (g x)))"
    1.18 +    by (rule lfp_lowerbound) (simp add: lfp_unfold[OF *, symmetric])
    1.19 +
    1.20 +  show "g (lfp (\<lambda>x. f (g x))) \<le> lfp (\<lambda>x. g (f x))"
    1.21 +  proof (rule lfp_greatest)
    1.22 +    fix u assume "g (f u) \<le> u"
    1.23 +    moreover then have "g (lfp (\<lambda>x. f (g x))) \<le> g (f u)"
    1.24 +      by (intro assms[THEN monoD] lfp_lowerbound)
    1.25 +    ultimately show "g (lfp (\<lambda>x. f (g x))) \<le> u"
    1.26 +      by auto
    1.27 +  qed
    1.28 +qed
    1.29 +
    1.30 +lemma lfp_square:
    1.31 +  assumes "mono f" shows "lfp f = lfp (\<lambda>x. f (f x))"
    1.32 +proof (rule antisym)
    1.33 +  show "lfp f \<le> lfp (\<lambda>x. f (f x))"
    1.34 +    by (intro lfp_lowerbound) (simp add: assms lfp_rolling)
    1.35 +  show "lfp (\<lambda>x. f (f x)) \<le> lfp f"
    1.36 +    by (intro lfp_lowerbound) (simp add: lfp_unfold[OF assms, symmetric])
    1.37 +qed
    1.38 +
    1.39 +lemma lfp_lfp:
    1.40 +  assumes f: "\<And>x y w z. x \<le> y \<Longrightarrow> w \<le> z \<Longrightarrow> f x w \<le> f y z"
    1.41 +  shows "lfp (\<lambda>x. lfp (f x)) = lfp (\<lambda>x. f x x)"
    1.42 +proof (rule antisym)
    1.43 +  have *: "mono (\<lambda>x. f x x)"
    1.44 +    by (blast intro: monoI f)
    1.45 +  show "lfp (\<lambda>x. lfp (f x)) \<le> lfp (\<lambda>x. f x x)"
    1.46 +    by (intro lfp_lowerbound) (simp add: lfp_unfold[OF *, symmetric])
    1.47 +  show "lfp (\<lambda>x. lfp (f x)) \<ge> lfp (\<lambda>x. f x x)" (is "?F \<ge> _")
    1.48 +  proof (intro lfp_lowerbound)
    1.49 +    have *: "?F = lfp (f ?F)"
    1.50 +      by (rule lfp_unfold) (blast intro: monoI lfp_mono f)
    1.51 +    also have "\<dots> = f ?F (lfp (f ?F))"
    1.52 +      by (rule lfp_unfold) (blast intro: monoI lfp_mono f)
    1.53 +    finally show "f ?F ?F \<le> ?F"
    1.54 +      by (simp add: *[symmetric])
    1.55 +  qed
    1.56 +qed
    1.57 +
    1.58 +lemma gfp_rolling:
    1.59 +  assumes "mono g" "mono f"
    1.60 +  shows "g (gfp (\<lambda>x. f (g x))) = gfp (\<lambda>x. g (f x))"
    1.61 +proof (rule antisym)
    1.62 +  have *: "mono (\<lambda>x. f (g x))"
    1.63 +    using assms by (auto simp: mono_def)
    1.64 +  show "g (gfp (\<lambda>x. f (g x))) \<le> gfp (\<lambda>x. g (f x))"
    1.65 +    by (rule gfp_upperbound) (simp add: gfp_unfold[OF *, symmetric])
    1.66 +
    1.67 +  show "gfp (\<lambda>x. g (f x)) \<le> g (gfp (\<lambda>x. f (g x)))"
    1.68 +  proof (rule gfp_least)
    1.69 +    fix u assume "u \<le> g (f u)"
    1.70 +    moreover then have "g (f u) \<le> g (gfp (\<lambda>x. f (g x)))"
    1.71 +      by (intro assms[THEN monoD] gfp_upperbound)
    1.72 +    ultimately show "u \<le> g (gfp (\<lambda>x. f (g x)))"
    1.73 +      by auto
    1.74 +  qed
    1.75 +qed
    1.76 +
    1.77 +lemma gfp_square:
    1.78 +  assumes "mono f" shows "gfp f = gfp (\<lambda>x. f (f x))"
    1.79 +proof (rule antisym)
    1.80 +  show "gfp (\<lambda>x. f (f x)) \<le> gfp f"
    1.81 +    by (intro gfp_upperbound) (simp add: assms gfp_rolling)
    1.82 +  show "gfp f \<le> gfp (\<lambda>x. f (f x))"
    1.83 +    by (intro gfp_upperbound) (simp add: gfp_unfold[OF assms, symmetric])
    1.84 +qed
    1.85 +
    1.86 +lemma gfp_gfp:
    1.87 +  assumes f: "\<And>x y w z. x \<le> y \<Longrightarrow> w \<le> z \<Longrightarrow> f x w \<le> f y z"
    1.88 +  shows "gfp (\<lambda>x. gfp (f x)) = gfp (\<lambda>x. f x x)"
    1.89 +proof (rule antisym)
    1.90 +  have *: "mono (\<lambda>x. f x x)"
    1.91 +    by (blast intro: monoI f)
    1.92 +  show "gfp (\<lambda>x. f x x) \<le> gfp (\<lambda>x. gfp (f x))"
    1.93 +    by (intro gfp_upperbound) (simp add: gfp_unfold[OF *, symmetric])
    1.94 +  show "gfp (\<lambda>x. gfp (f x)) \<le> gfp (\<lambda>x. f x x)" (is "?F \<le> _")
    1.95 +  proof (intro gfp_upperbound)
    1.96 +    have *: "?F = gfp (f ?F)"
    1.97 +      by (rule gfp_unfold) (blast intro: monoI gfp_mono f)
    1.98 +    also have "\<dots> = f ?F (gfp (f ?F))"
    1.99 +      by (rule gfp_unfold) (blast intro: monoI gfp_mono f)
   1.100 +    finally show "?F \<le> f ?F ?F"
   1.101 +      by (simp add: *[symmetric])
   1.102 +  qed
   1.103 +qed
   1.104  
   1.105  subsection {* Inductive predicates and sets *}
   1.106