src/HOL/Nat.thy
changeset 64447 e44f5c123f26
parent 63979 95c3ae4baba8
child 64712 38adf0c59c35
     1.1 --- a/src/HOL/Nat.thy	Tue Nov 22 16:22:05 2016 +0100
     1.2 +++ b/src/HOL/Nat.thy	Tue Nov 22 18:36:59 2016 +0100
     1.3 @@ -10,7 +10,7 @@
     1.4  section \<open>Natural numbers\<close>
     1.5  
     1.6  theory Nat
     1.7 -  imports Inductive Typedef Fun Rings
     1.8 +imports Inductive Typedef Fun Rings
     1.9  begin
    1.10  
    1.11  named_theorems arith "arith facts -- only ground formulas"
    1.12 @@ -742,6 +742,8 @@
    1.13  lemma less_Suc_eq_0_disj: "m < Suc n \<longleftrightarrow> m = 0 \<or> (\<exists>j. m = Suc j \<and> j < n)"
    1.14    by (cases m) simp_all
    1.15  
    1.16 +lemma All_less_Suc: "(\<forall>i < Suc n. P i) = (P n \<and> (\<forall>i < n. P i))"
    1.17 +by (auto simp: less_Suc_eq)
    1.18  
    1.19  subsubsection \<open>Monotonicity of Addition\<close>
    1.20