clarified lfp/gfp statements and proofs;
authorwenzelm
Sat Oct 01 17:16:35 2016 +0200 (2016-10-01)
changeset 6397995c3ae4baba8
parent 63977 ec0fb01c6d50
child 63980 f8e556c8ad6f
clarified lfp/gfp statements and proofs;
NEWS
src/HOL/Complete_Partial_Order.thy
src/HOL/Inductive.thy
src/HOL/Library/Extended_Nonnegative_Real.thy
src/HOL/Library/Order_Continuity.thy
src/HOL/Nat.thy
     1.1 --- a/NEWS	Sat Oct 01 12:03:27 2016 +0200
     1.2 +++ b/NEWS	Sat Oct 01 17:16:35 2016 +0200
     1.3 @@ -336,6 +336,12 @@
     1.4  eliminates the need to qualify any of those names in the presence of
     1.5  infix "mod" syntax. INCOMPATIBILITY.
     1.6  
     1.7 +* Statements and proofs of Knaster-Tarski fixpoint combinators lfp/gfp
     1.8 +have been clarified. The fixpoint properties are lfp_fixpoint, its
     1.9 +symmetric lfp_unfold (as before), and the duals for gfp. Auxiliary items
    1.10 +for the proof (lfp_lemma2 etc.) are no longer exported, but can be
    1.11 +easily recovered by composition with eq_refl. Minor INCOMPATIBILITY.
    1.12 +
    1.13  * Constant "surj" is a mere input abbreviation, to avoid hiding an
    1.14  equation in term output. Minor INCOMPATIBILITY.
    1.15  
     2.1 --- a/src/HOL/Complete_Partial_Order.thy	Sat Oct 01 12:03:27 2016 +0200
     2.2 +++ b/src/HOL/Complete_Partial_Order.thy	Sat Oct 01 17:16:35 2016 +0200
     2.3 @@ -365,15 +365,15 @@
     2.4    by standard (fast intro: Sup_upper Sup_least)+
     2.5  
     2.6  lemma lfp_eq_fixp:
     2.7 -  assumes f: "mono f"
     2.8 +  assumes mono: "mono f"
     2.9    shows "lfp f = fixp f"
    2.10  proof (rule antisym)
    2.11 -  from f have f': "monotone (op \<le>) (op \<le>) f"
    2.12 +  from mono have f': "monotone (op \<le>) (op \<le>) f"
    2.13      unfolding mono_def monotone_def .
    2.14    show "lfp f \<le> fixp f"
    2.15      by (rule lfp_lowerbound, subst fixp_unfold [OF f'], rule order_refl)
    2.16    show "fixp f \<le> lfp f"
    2.17 -    by (rule fixp_lowerbound [OF f'], subst lfp_unfold [OF f], rule order_refl)
    2.18 +    by (rule fixp_lowerbound [OF f']) (simp add: lfp_fixpoint [OF mono])
    2.19  qed
    2.20  
    2.21  hide_const (open) iterates fixp
     3.1 --- a/src/HOL/Inductive.thy	Sat Oct 01 12:03:27 2016 +0200
     3.2 +++ b/src/HOL/Inductive.thy	Sat Oct 01 17:16:35 2016 +0200
     3.3 @@ -14,22 +14,14 @@
     3.4      "primrec" :: thy_decl
     3.5  begin
     3.6  
     3.7 -subsection \<open>Least and greatest fixed points\<close>
     3.8 +subsection \<open>Least fixed points\<close>
     3.9  
    3.10  context complete_lattice
    3.11  begin
    3.12  
    3.13 -definition lfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"  \<comment> \<open>least fixed point\<close>
    3.14 +definition lfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"
    3.15    where "lfp f = Inf {u. f u \<le> u}"
    3.16  
    3.17 -definition gfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"  \<comment> \<open>greatest fixed point\<close>
    3.18 -  where "gfp f = Sup {u. u \<le> f u}"
    3.19 -
    3.20 -
    3.21 -subsection \<open>Proof of Knaster-Tarski Theorem using @{term lfp}\<close>
    3.22 -
    3.23 -text \<open>@{term "lfp f"} is the least upper bound of the set @{term "{u. f u \<le> u}"}\<close>
    3.24 -
    3.25  lemma lfp_lowerbound: "f A \<le> A \<Longrightarrow> lfp f \<le> A"
    3.26    by (auto simp add: lfp_def intro: Inf_lower)
    3.27  
    3.28 @@ -38,14 +30,31 @@
    3.29  
    3.30  end
    3.31  
    3.32 -lemma lfp_lemma2: "mono f \<Longrightarrow> f (lfp f) \<le> lfp f"
    3.33 -  by (iprover intro: lfp_greatest order_trans monoD lfp_lowerbound)
    3.34 -
    3.35 -lemma lfp_lemma3: "mono f \<Longrightarrow> lfp f \<le> f (lfp f)"
    3.36 -  by (iprover intro: lfp_lemma2 monoD lfp_lowerbound)
    3.37 +lemma lfp_fixpoint:
    3.38 +  assumes "mono f"
    3.39 +  shows "f (lfp f) = lfp f"
    3.40 +  unfolding lfp_def
    3.41 +proof (rule order_antisym)
    3.42 +  let ?H = "{u. f u \<le> u}"
    3.43 +  let ?a = "\<Sqinter>?H"
    3.44 +  show "f ?a \<le> ?a"
    3.45 +  proof (rule Inf_greatest)
    3.46 +    fix x
    3.47 +    assume "x \<in> ?H"
    3.48 +    then have "?a \<le> x" by (rule Inf_lower)
    3.49 +    with \<open>mono f\<close> have "f ?a \<le> f x" ..
    3.50 +    also from \<open>x \<in> ?H\<close> have "f x \<le> x" ..
    3.51 +    finally show "f ?a \<le> x" .
    3.52 +  qed
    3.53 +  show "?a \<le> f ?a"
    3.54 +  proof (rule Inf_lower)
    3.55 +    from \<open>mono f\<close> and \<open>f ?a \<le> ?a\<close> have "f (f ?a) \<le> f ?a" ..
    3.56 +    then show "f ?a \<in> ?H" ..
    3.57 +  qed
    3.58 +qed
    3.59  
    3.60  lemma lfp_unfold: "mono f \<Longrightarrow> lfp f = f (lfp f)"
    3.61 -  by (iprover intro: order_antisym lfp_lemma2 lfp_lemma3)
    3.62 +  by (rule lfp_fixpoint [symmetric])
    3.63  
    3.64  lemma lfp_const: "lfp (\<lambda>x. t) = t"
    3.65    by (rule lfp_unfold) (simp add: mono_def)
    3.66 @@ -132,9 +141,13 @@
    3.67    by (rule lfp_lowerbound [THEN lfp_greatest]) (blast intro: order_trans)
    3.68  
    3.69  
    3.70 -subsection \<open>Proof of Knaster-Tarski Theorem using \<open>gfp\<close>\<close>
    3.71 +subsection \<open>Greatest fixed points\<close>
    3.72  
    3.73 -text \<open>@{term "gfp f"} is the greatest lower bound of the set @{term "{u. u \<le> f u}"}\<close>
    3.74 +context complete_lattice
    3.75 +begin
    3.76 +
    3.77 +definition gfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"
    3.78 +  where "gfp f = Sup {u. u \<le> f u}"
    3.79  
    3.80  lemma gfp_upperbound: "X \<le> f X \<Longrightarrow> X \<le> gfp f"
    3.81    by (auto simp add: gfp_def intro: Sup_upper)
    3.82 @@ -142,14 +155,36 @@
    3.83  lemma gfp_least: "(\<And>u. u \<le> f u \<Longrightarrow> u \<le> X) \<Longrightarrow> gfp f \<le> X"
    3.84    by (auto simp add: gfp_def intro: Sup_least)
    3.85  
    3.86 -lemma gfp_lemma2: "mono f \<Longrightarrow> gfp f \<le> f (gfp f)"
    3.87 -  by (iprover intro: gfp_least order_trans monoD gfp_upperbound)
    3.88 +end
    3.89 +
    3.90 +lemma lfp_le_gfp: "mono f \<Longrightarrow> lfp f \<le> gfp f"
    3.91 +  by (rule gfp_upperbound) (simp add: lfp_fixpoint)
    3.92  
    3.93 -lemma gfp_lemma3: "mono f \<Longrightarrow> f (gfp f) \<le> gfp f"
    3.94 -  by (iprover intro: gfp_lemma2 monoD gfp_upperbound)
    3.95 +lemma gfp_fixpoint:
    3.96 +  assumes "mono f"
    3.97 +  shows "f (gfp f) = gfp f"
    3.98 +  unfolding gfp_def
    3.99 +proof (rule order_antisym)
   3.100 +  let ?H = "{u. u \<le> f u}"
   3.101 +  let ?a = "\<Squnion>?H"
   3.102 +  show "?a \<le> f ?a"
   3.103 +  proof (rule Sup_least)
   3.104 +    fix x
   3.105 +    assume "x \<in> ?H"
   3.106 +    then have "x \<le> f x" ..
   3.107 +    also from \<open>x \<in> ?H\<close> have "x \<le> ?a" by (rule Sup_upper)
   3.108 +    with \<open>mono f\<close> have "f x \<le> f ?a" ..
   3.109 +    finally show "x \<le> f ?a" .
   3.110 +  qed
   3.111 +  show "f ?a \<le> ?a"
   3.112 +  proof (rule Sup_upper)
   3.113 +    from \<open>mono f\<close> and \<open>?a \<le> f ?a\<close> have "f ?a \<le> f (f ?a)" ..
   3.114 +    then show "f ?a \<in> ?H" ..
   3.115 +  qed
   3.116 +qed
   3.117  
   3.118  lemma gfp_unfold: "mono f \<Longrightarrow> gfp f = f (gfp f)"
   3.119 -  by (iprover intro: order_antisym gfp_lemma2 gfp_lemma3)
   3.120 +  by (rule gfp_fixpoint [symmetric])
   3.121  
   3.122  lemma gfp_const: "gfp (\<lambda>x. t) = t"
   3.123    by (rule gfp_unfold) (simp add: mono_def)
   3.124 @@ -158,10 +193,6 @@
   3.125    by (rule antisym) (simp_all add: gfp_upperbound gfp_unfold[symmetric])
   3.126  
   3.127  
   3.128 -lemma lfp_le_gfp: "mono f \<Longrightarrow> lfp f \<le> gfp f"
   3.129 -  by (iprover intro: gfp_upperbound lfp_lemma3)
   3.130 -
   3.131 -
   3.132  subsection \<open>Coinduction rules for greatest fixed points\<close>
   3.133  
   3.134  text \<open>Weak version.\<close>
   3.135 @@ -174,7 +205,7 @@
   3.136    done
   3.137  
   3.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))"
   3.139 -  apply (frule gfp_lemma2)
   3.140 +  apply (frule gfp_unfold [THEN eq_refl])
   3.141    apply (drule mono_sup)
   3.142    apply (rule le_supI)
   3.143     apply assumption
   3.144 @@ -190,7 +221,7 @@
   3.145    by (rule weak_coinduct[rotated], rule coinduct_lemma) blast+
   3.146  
   3.147  lemma gfp_fun_UnI2: "mono f \<Longrightarrow> a \<in> gfp f \<Longrightarrow> a \<in> f (X \<union> gfp f)"
   3.148 -  by (blast dest: gfp_lemma2 mono_Un)
   3.149 +  by (blast dest: gfp_fixpoint mono_Un)
   3.150  
   3.151  lemma gfp_ordinal_induct[case_names mono step union]:
   3.152    fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
   3.153 @@ -248,7 +279,7 @@
   3.154    "X \<subseteq> f (lfp (\<lambda>x. f x \<union> X \<union> gfp f)) \<Longrightarrow> mono f \<Longrightarrow>
   3.155      lfp (\<lambda>x. f x \<union> X \<union> gfp f) \<subseteq> f (lfp (\<lambda>x. f x \<union> X \<union> gfp f))"
   3.156    apply (rule subset_trans)
   3.157 -   apply (erule coinduct3_mono_lemma [THEN lfp_lemma3])
   3.158 +   apply (erule coinduct3_mono_lemma [THEN lfp_unfold [THEN eq_refl]])
   3.159    apply (rule Un_least [THEN Un_least])
   3.160      apply (rule subset_refl, assumption)
   3.161    apply (rule gfp_unfold [THEN equalityD1, THEN subset_trans], assumption)
     4.1 --- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Sat Oct 01 12:03:27 2016 +0200
     4.2 +++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Sat Oct 01 17:16:35 2016 +0200
     4.3 @@ -99,7 +99,7 @@
     4.4         (auto intro!: mono_funpow sup_continuous_mono[OF f] SUP_least)
     4.5  
     4.6    show "lfp g \<le> \<alpha> (lfp f)"
     4.7 -    by (rule lfp_lowerbound) (simp add: eq[symmetric] lfp_unfold[OF mf, symmetric])
     4.8 +    by (rule lfp_lowerbound) (simp add: eq[symmetric] lfp_fixpoint[OF mf])
     4.9  qed
    4.10  
    4.11  lemma sup_continuous_applyD: "sup_continuous f \<Longrightarrow> sup_continuous (\<lambda>x. f x h)"
     5.1 --- a/src/HOL/Library/Order_Continuity.thy	Sat Oct 01 12:03:27 2016 +0200
     5.2 +++ b/src/HOL/Library/Order_Continuity.thy	Sat Oct 01 17:16:35 2016 +0200
     5.3 @@ -123,7 +123,7 @@
     5.4        case (Suc i)
     5.5        have "(F ^^ Suc i) bot = F ((F ^^ i) bot)" by simp
     5.6        also have "\<dots> \<le> F (lfp F)" by (rule monoD[OF mono Suc])
     5.7 -      also have "\<dots> = lfp F" by (simp add: lfp_unfold[OF mono, symmetric])
     5.8 +      also have "\<dots> = lfp F" by (simp add: lfp_fixpoint[OF mono])
     5.9        finally show ?case .
    5.10      qed simp
    5.11    qed
    5.12 @@ -287,7 +287,7 @@
    5.13      fix i show "gfp F \<le> (F ^^ i) top"
    5.14      proof (induct i)
    5.15        case (Suc i)
    5.16 -      have "gfp F = F (gfp F)" by (simp add: gfp_unfold[OF mono, symmetric])
    5.17 +      have "gfp F = F (gfp F)" by (simp add: gfp_fixpoint[OF mono])
    5.18        also have "\<dots> \<le> F ((F ^^ i) top)" by (rule monoD[OF mono Suc])
    5.19        also have "\<dots> = (F ^^ Suc i) top" by simp
    5.20        finally show ?case .
     6.1 --- a/src/HOL/Nat.thy	Sat Oct 01 12:03:27 2016 +0200
     6.2 +++ b/src/HOL/Nat.thy	Sat Oct 01 17:16:35 2016 +0200
     6.3 @@ -1554,7 +1554,7 @@
     6.4        by (simp add: comp_def)
     6.5    qed
     6.6    have "(f ^^ n) (lfp f) = lfp f" for n
     6.7 -    by (induct n) (auto intro: f lfp_unfold[symmetric])
     6.8 +    by (induct n) (auto intro: f lfp_fixpoint)
     6.9    then show "lfp (f ^^ Suc n) \<le> lfp f"
    6.10      by (intro lfp_lowerbound) (simp del: funpow.simps)
    6.11  qed
    6.12 @@ -1571,7 +1571,7 @@
    6.13        by (simp add: comp_def)
    6.14    qed
    6.15    have "(f ^^ n) (gfp f) = gfp f" for n
    6.16 -    by (induct n) (auto intro: f gfp_unfold[symmetric])
    6.17 +    by (induct n) (auto intro: f gfp_fixpoint)
    6.18    then show "gfp (f ^^ Suc n) \<ge> gfp f"
    6.19      by (intro gfp_upperbound) (simp del: funpow.simps)
    6.20  qed