author haftmann Mon, 19 Jan 2009 08:16:42 +0100 changeset 29557 5362cc5ee3a8 parent 29556 7c128276aa93 child 29558 9846af6c6d6a
tuned proof
 src/HOL/OrderedGroup.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/OrderedGroup.thy	Sun Jan 18 21:40:53 2009 +0100
+++ b/src/HOL/OrderedGroup.thy	Mon Jan 19 08:16:42 2009 +0100
@@ -1231,7 +1231,7 @@
qed

-proof -
+proof
have abs_ge_zero [simp]: "\<And>a. 0 \<le> \<bar>a\<bar>"
proof -
fix a b
@@ -1240,37 +1240,26 @@
qed
have abs_leI: "\<And>a b. a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
-  show ?thesis
-  proof
-    fix a
-    show "0 \<le> \<bar>a\<bar>" by simp
-  next
-    fix a
-    show "a \<le> \<bar>a\<bar>"
-      by (auto simp add: abs_lattice)
-  next
-    fix a
-    show "\<bar>-a\<bar> = \<bar>a\<bar>"
-      by (simp add: abs_lattice sup_commute)
-  next
-    fix a b
-    show "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b" by (erule abs_leI)
-  next
-    fix a b
-    show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
-    proof -
-      have g:"abs a + abs b = sup (a+b) (sup (-a-b) (sup (-a+b) (a + (-b))))" (is "_=sup ?m ?n")
-      have a:"a+b <= sup ?m ?n" by (simp)
-      have b:"-a-b <= ?n" by (simp)
-      have c:"?n <= sup ?m ?n" by (simp)
-      from b c have d: "-a-b <= sup ?m ?n" by(rule order_trans)
-      have e:"-a-b = -(a+b)" by (simp add: diff_minus)
-      from a d e have "abs(a+b) <= sup ?m ?n"
-        by (drule_tac abs_leI, auto)
-      with g[symmetric] show ?thesis by simp
-    qed
-  qed auto
+  fix a b
+  show "0 \<le> \<bar>a\<bar>" by simp
+  show "a \<le> \<bar>a\<bar>"
+    by (auto simp add: abs_lattice)
+  show "\<bar>-a\<bar> = \<bar>a\<bar>"
+    by (simp add: abs_lattice sup_commute)
+  show "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b" by (fact abs_leI)
+  show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
+  proof -
+    have g:"abs a + abs b = sup (a+b) (sup (-a-b) (sup (-a+b) (a + (-b))))" (is "_=sup ?m ?n")
+    have a:"a+b <= sup ?m ?n" by (simp)
+    have b:"-a-b <= ?n" by (simp)
+    have c:"?n <= sup ?m ?n" by (simp)
+    from b c have d: "-a-b <= sup ?m ?n" by(rule order_trans)
+    have e:"-a-b = -(a+b)" by (simp add: diff_minus)
+    from a d e have "abs(a+b) <= sup ?m ?n"
+      by (drule_tac abs_leI, auto)
+    with g[symmetric] show ?thesis by simp
+  qed
qed

end```