src/HOL/Nat.thy
changeset 66386 962c12353c67
parent 66295 1ec601d9c829
child 66810 cc2b490f9dc4
     1.1 --- a/src/HOL/Nat.thy	Tue Aug 08 23:55:03 2017 +0200
     1.2 +++ b/src/HOL/Nat.thy	Wed Aug 09 12:01:16 2017 +0200
     1.3 @@ -764,6 +764,16 @@
     1.4  lemma All_less_Suc: "(\<forall>i < Suc n. P i) = (P n \<and> (\<forall>i < n. P i))"
     1.5  by (auto simp: less_Suc_eq)
     1.6  
     1.7 +lemma All_less_Suc2: "(\<forall>i < Suc n. P i) = (P 0 \<and> (\<forall>i < n. P(Suc i)))"
     1.8 +by (auto simp: less_Suc_eq_0_disj)
     1.9 +
    1.10 +lemma Ex_less_Suc: "(\<exists>i < Suc n. P i) = (P n \<or> (\<exists>i < n. P i))"
    1.11 +by (auto simp: less_Suc_eq)
    1.12 +
    1.13 +lemma Ex_less_Suc2: "(\<exists>i < Suc n. P i) = (P 0 \<or> (\<exists>i < n. P(Suc i)))"
    1.14 +by (auto simp: less_Suc_eq_0_disj)
    1.15 +
    1.16 +
    1.17  subsubsection \<open>Monotonicity of Addition\<close>
    1.18  
    1.19  lemma Suc_pred [simp]: "n > 0 \<Longrightarrow> Suc (n - Suc 0) = n"