author hoelzl Mon May 04 18:04:01 2015 +0200 (2015-05-04) changeset 60173 6a61bb577d5b parent 60172 423273355b55 child 60174 70d8f7abde8f
add rules for least/greatest fixed point calculus
 src/HOL/Inductive.thy file | annotate | diff | revisions
```     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
```