src/HOL/Inductive.thy
changeset 63979 95c3ae4baba8
parent 63976 c1a481bb82d3
child 63980 f8e556c8ad6f
     1.1 --- a/src/HOL/Inductive.thy	Sat Oct 01 12:03:27 2016 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Sat Oct 01 17:16:35 2016 +0200
     1.3 @@ -14,22 +14,14 @@
     1.4      "primrec" :: thy_decl
     1.5  begin
     1.6  
     1.7 -subsection \<open>Least and greatest fixed points\<close>
     1.8 +subsection \<open>Least fixed points\<close>
     1.9  
    1.10  context complete_lattice
    1.11  begin
    1.12  
    1.13 -definition lfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"  \<comment> \<open>least fixed point\<close>
    1.14 +definition lfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"
    1.15    where "lfp f = Inf {u. f u \<le> u}"
    1.16  
    1.17 -definition gfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"  \<comment> \<open>greatest fixed point\<close>
    1.18 -  where "gfp f = Sup {u. u \<le> f u}"
    1.19 -
    1.20 -
    1.21 -subsection \<open>Proof of Knaster-Tarski Theorem using @{term lfp}\<close>
    1.22 -
    1.23 -text \<open>@{term "lfp f"} is the least upper bound of the set @{term "{u. f u \<le> u}"}\<close>
    1.24 -
    1.25  lemma lfp_lowerbound: "f A \<le> A \<Longrightarrow> lfp f \<le> A"
    1.26    by (auto simp add: lfp_def intro: Inf_lower)
    1.27  
    1.28 @@ -38,14 +30,31 @@
    1.29  
    1.30  end
    1.31  
    1.32 -lemma lfp_lemma2: "mono f \<Longrightarrow> f (lfp f) \<le> lfp f"
    1.33 -  by (iprover intro: lfp_greatest order_trans monoD lfp_lowerbound)
    1.34 -
    1.35 -lemma lfp_lemma3: "mono f \<Longrightarrow> lfp f \<le> f (lfp f)"
    1.36 -  by (iprover intro: lfp_lemma2 monoD lfp_lowerbound)
    1.37 +lemma lfp_fixpoint:
    1.38 +  assumes "mono f"
    1.39 +  shows "f (lfp f) = lfp f"
    1.40 +  unfolding lfp_def
    1.41 +proof (rule order_antisym)
    1.42 +  let ?H = "{u. f u \<le> u}"
    1.43 +  let ?a = "\<Sqinter>?H"
    1.44 +  show "f ?a \<le> ?a"
    1.45 +  proof (rule Inf_greatest)
    1.46 +    fix x
    1.47 +    assume "x \<in> ?H"
    1.48 +    then have "?a \<le> x" by (rule Inf_lower)
    1.49 +    with \<open>mono f\<close> have "f ?a \<le> f x" ..
    1.50 +    also from \<open>x \<in> ?H\<close> have "f x \<le> x" ..
    1.51 +    finally show "f ?a \<le> x" .
    1.52 +  qed
    1.53 +  show "?a \<le> f ?a"
    1.54 +  proof (rule Inf_lower)
    1.55 +    from \<open>mono f\<close> and \<open>f ?a \<le> ?a\<close> have "f (f ?a) \<le> f ?a" ..
    1.56 +    then show "f ?a \<in> ?H" ..
    1.57 +  qed
    1.58 +qed
    1.59  
    1.60  lemma lfp_unfold: "mono f \<Longrightarrow> lfp f = f (lfp f)"
    1.61 -  by (iprover intro: order_antisym lfp_lemma2 lfp_lemma3)
    1.62 +  by (rule lfp_fixpoint [symmetric])
    1.63  
    1.64  lemma lfp_const: "lfp (\<lambda>x. t) = t"
    1.65    by (rule lfp_unfold) (simp add: mono_def)
    1.66 @@ -132,9 +141,13 @@
    1.67    by (rule lfp_lowerbound [THEN lfp_greatest]) (blast intro: order_trans)
    1.68  
    1.69  
    1.70 -subsection \<open>Proof of Knaster-Tarski Theorem using \<open>gfp\<close>\<close>
    1.71 +subsection \<open>Greatest fixed points\<close>
    1.72  
    1.73 -text \<open>@{term "gfp f"} is the greatest lower bound of the set @{term "{u. u \<le> f u}"}\<close>
    1.74 +context complete_lattice
    1.75 +begin
    1.76 +
    1.77 +definition gfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"
    1.78 +  where "gfp f = Sup {u. u \<le> f u}"
    1.79  
    1.80  lemma gfp_upperbound: "X \<le> f X \<Longrightarrow> X \<le> gfp f"
    1.81    by (auto simp add: gfp_def intro: Sup_upper)
    1.82 @@ -142,14 +155,36 @@
    1.83  lemma gfp_least: "(\<And>u. u \<le> f u \<Longrightarrow> u \<le> X) \<Longrightarrow> gfp f \<le> X"
    1.84    by (auto simp add: gfp_def intro: Sup_least)
    1.85  
    1.86 -lemma gfp_lemma2: "mono f \<Longrightarrow> gfp f \<le> f (gfp f)"
    1.87 -  by (iprover intro: gfp_least order_trans monoD gfp_upperbound)
    1.88 +end
    1.89 +
    1.90 +lemma lfp_le_gfp: "mono f \<Longrightarrow> lfp f \<le> gfp f"
    1.91 +  by (rule gfp_upperbound) (simp add: lfp_fixpoint)
    1.92  
    1.93 -lemma gfp_lemma3: "mono f \<Longrightarrow> f (gfp f) \<le> gfp f"
    1.94 -  by (iprover intro: gfp_lemma2 monoD gfp_upperbound)
    1.95 +lemma gfp_fixpoint:
    1.96 +  assumes "mono f"
    1.97 +  shows "f (gfp f) = gfp f"
    1.98 +  unfolding gfp_def
    1.99 +proof (rule order_antisym)
   1.100 +  let ?H = "{u. u \<le> f u}"
   1.101 +  let ?a = "\<Squnion>?H"
   1.102 +  show "?a \<le> f ?a"
   1.103 +  proof (rule Sup_least)
   1.104 +    fix x
   1.105 +    assume "x \<in> ?H"
   1.106 +    then have "x \<le> f x" ..
   1.107 +    also from \<open>x \<in> ?H\<close> have "x \<le> ?a" by (rule Sup_upper)
   1.108 +    with \<open>mono f\<close> have "f x \<le> f ?a" ..
   1.109 +    finally show "x \<le> f ?a" .
   1.110 +  qed
   1.111 +  show "f ?a \<le> ?a"
   1.112 +  proof (rule Sup_upper)
   1.113 +    from \<open>mono f\<close> and \<open>?a \<le> f ?a\<close> have "f ?a \<le> f (f ?a)" ..
   1.114 +    then show "f ?a \<in> ?H" ..
   1.115 +  qed
   1.116 +qed
   1.117  
   1.118  lemma gfp_unfold: "mono f \<Longrightarrow> gfp f = f (gfp f)"
   1.119 -  by (iprover intro: order_antisym gfp_lemma2 gfp_lemma3)
   1.120 +  by (rule gfp_fixpoint [symmetric])
   1.121  
   1.122  lemma gfp_const: "gfp (\<lambda>x. t) = t"
   1.123    by (rule gfp_unfold) (simp add: mono_def)
   1.124 @@ -158,10 +193,6 @@
   1.125    by (rule antisym) (simp_all add: gfp_upperbound gfp_unfold[symmetric])
   1.126  
   1.127  
   1.128 -lemma lfp_le_gfp: "mono f \<Longrightarrow> lfp f \<le> gfp f"
   1.129 -  by (iprover intro: gfp_upperbound lfp_lemma3)
   1.130 -
   1.131 -
   1.132  subsection \<open>Coinduction rules for greatest fixed points\<close>
   1.133  
   1.134  text \<open>Weak version.\<close>
   1.135 @@ -174,7 +205,7 @@
   1.136    done
   1.137  
   1.138  lemma coinduct_lemma: "X \<le> f (sup X (gfp f)) \<Longrightarrow> mono f \<Longrightarrow> sup X (gfp f) \<le> f (sup X (gfp f))"
   1.139 -  apply (frule gfp_lemma2)
   1.140 +  apply (frule gfp_unfold [THEN eq_refl])
   1.141    apply (drule mono_sup)
   1.142    apply (rule le_supI)
   1.143     apply assumption
   1.144 @@ -190,7 +221,7 @@
   1.145    by (rule weak_coinduct[rotated], rule coinduct_lemma) blast+
   1.146  
   1.147  lemma gfp_fun_UnI2: "mono f \<Longrightarrow> a \<in> gfp f \<Longrightarrow> a \<in> f (X \<union> gfp f)"
   1.148 -  by (blast dest: gfp_lemma2 mono_Un)
   1.149 +  by (blast dest: gfp_fixpoint mono_Un)
   1.150  
   1.151  lemma gfp_ordinal_induct[case_names mono step union]:
   1.152    fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
   1.153 @@ -248,7 +279,7 @@
   1.154    "X \<subseteq> f (lfp (\<lambda>x. f x \<union> X \<union> gfp f)) \<Longrightarrow> mono f \<Longrightarrow>
   1.155      lfp (\<lambda>x. f x \<union> X \<union> gfp f) \<subseteq> f (lfp (\<lambda>x. f x \<union> X \<union> gfp f))"
   1.156    apply (rule subset_trans)
   1.157 -   apply (erule coinduct3_mono_lemma [THEN lfp_lemma3])
   1.158 +   apply (erule coinduct3_mono_lemma [THEN lfp_unfold [THEN eq_refl]])
   1.159    apply (rule Un_least [THEN Un_least])
   1.160      apply (rule subset_refl, assumption)
   1.161    apply (rule gfp_unfold [THEN equalityD1, THEN subset_trans], assumption)