author haftmann Sun, 09 Feb 2020 21:58:42 +0000 changeset 71425 f2da99316b86 parent 71424 e83fe2c31088 child 71426 745e518d3d0b
more rules for natural deduction from inequalities
 src/HOL/Groups.thy file | annotate | diff | comparison | revisions src/HOL/Nat.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Groups.thy	Sun Feb 09 10:46:32 2020 +0000
+++ b/src/HOL/Groups.thy	Sun Feb 09 21:58:42 2020 +0000
@@ -1413,6 +1413,25 @@
lemma zero_eq_add_iff_both_eq_0[simp]: "0 = x + y \<longleftrightarrow> x = 0 \<and> y = 0"
using add_eq_0_iff_both_eq_0[of x y] unfolding eq_commute[of 0] .

+lemma less_eqE:
+  assumes \<open>a \<le> b\<close>
+  obtains c where \<open>b = a + c\<close>
+
+lemma lessE:
+  assumes \<open>a < b\<close>
+  obtains c where \<open>b = a + c\<close> and \<open>c \<noteq> 0\<close>
+proof -
+  from assms have \<open>a \<le> b\<close> \<open>a \<noteq> b\<close>
+    by simp_all
+  from \<open>a \<le> b\<close> obtain c where \<open>b = a + c\<close>
+    by (rule less_eqE)
+  moreover have \<open>c \<noteq> 0\<close> using \<open>a \<noteq> b\<close> \<open>b = a + c\<close>
+    by auto
+  ultimately show ?thesis
+    by (rule that)
+qed
+
lemmas zero_order = zero_le le_zero_eq not_less_zero zero_less_iff_neq_zero not_gr_zero
\<comment> \<open>This should be attributed with \<open>[iff]\<close>, but then \<open>blast\<close> fails in \<open>Set\<close>.\<close>
```
```--- a/src/HOL/Nat.thy	Sun Feb 09 10:46:32 2020 +0000
+++ b/src/HOL/Nat.thy	Sun Feb 09 21:58:42 2020 +0000
@@ -793,7 +793,6 @@
apply simp_all
done

-text \<open>Deleted \<open>less_natE\<close>; use \<open>less_imp_Suc_add RS exE\<close>\<close>
lemma less_imp_Suc_add: "m < n \<Longrightarrow> \<exists>k. n = Suc (m + k)"
proof (induct n)
case 0
@@ -809,6 +808,11 @@
for k l :: nat
by (auto simp: less_Suc_eq_le[symmetric] dest: less_imp_Suc_add)

+lemma less_natE:
+  assumes \<open>m < n\<close>
+  obtains q where \<open>n = Suc (m + q)\<close>
+  using assms by (auto dest: less_imp_Suc_add intro: that)
+
text \<open>strict, in 1st argument; proof is by induction on \<open>k > 0\<close>\<close>
lemma mult_less_mono2:
fixes i j :: nat```