src/HOL/Inductive.thy
changeset 63976 c1a481bb82d3
parent 63863 d14e580c3b8f
child 63979 95c3ae4baba8
     1.1 --- a/src/HOL/Inductive.thy	Fri Sep 30 17:12:50 2016 +0100
     1.2 +++ b/src/HOL/Inductive.thy	Sat Oct 01 11:14:00 2016 +0200
     1.3 @@ -158,6 +158,10 @@
     1.4    by (rule antisym) (simp_all add: gfp_upperbound gfp_unfold[symmetric])
     1.5  
     1.6  
     1.7 +lemma lfp_le_gfp: "mono f \<Longrightarrow> lfp f \<le> gfp f"
     1.8 +  by (iprover intro: gfp_upperbound lfp_lemma3)
     1.9 +
    1.10 +
    1.11  subsection \<open>Coinduction rules for greatest fixed points\<close>
    1.12  
    1.13  text \<open>Weak version.\<close>