author wenzelm Tue, 13 Aug 2019 20:17:02 +0200 changeset 70523 1182ea5c9a6e parent 70522 f2d58cafbc13 child 70524 7783bece74b4
more compact proof terms;
 src/HOL/Enum.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Enum.thy	Tue Aug 13 20:16:03 2019 +0200
+++ b/src/HOL/Enum.thy	Tue Aug 13 20:17:02 2019 +0200
@@ -696,11 +696,12 @@
definition "sgn = (\<lambda>x :: finite_2. x)"
instance
by standard
-    (simp_all add: plus_finite_2_def uminus_finite_2_def minus_finite_2_def
-      times_finite_2_def
-      inverse_finite_2_def divide_finite_2_def modulo_finite_2_def
-      abs_finite_2_def sgn_finite_2_def
-      split: finite_2.splits)
+    (subproofs
+      \<open>simp_all add: plus_finite_2_def uminus_finite_2_def minus_finite_2_def
+        times_finite_2_def
+        inverse_finite_2_def divide_finite_2_def modulo_finite_2_def
+        abs_finite_2_def sgn_finite_2_def
+        split: finite_2.splits\<close>)
end

lemma two_finite_2 [simp]:
@@ -718,8 +719,9 @@
definition [simp]: "division_segment (x :: finite_2) = 1"
instance
by standard
-    (auto simp add: divide_finite_2_def times_finite_2_def dvd_finite_2_unfold
-    split: finite_2.splits)
+    (subproofs
+      \<open>auto simp add: divide_finite_2_def times_finite_2_def dvd_finite_2_unfold
+        split: finite_2.splits\<close>)
end

@@ -930,12 +932,13 @@
definition "sgn = (\<lambda>x :: finite_3. x)"
instance
by standard
-    (simp_all add: plus_finite_3_def uminus_finite_3_def minus_finite_3_def
-      times_finite_3_def
-      inverse_finite_3_def divide_finite_3_def modulo_finite_3_def
-      abs_finite_3_def sgn_finite_3_def
-      less_finite_3_def
-      split: finite_3.splits)
+    (subproofs
+      \<open>simp_all add: plus_finite_3_def uminus_finite_3_def minus_finite_3_def
+        times_finite_3_def
+        inverse_finite_3_def divide_finite_3_def modulo_finite_3_def
+        abs_finite_3_def sgn_finite_3_def
+        less_finite_3_def
+        split: finite_3.splits\<close>)
end

lemma two_finite_3 [simp]:
@@ -951,14 +954,17 @@
definition [simp]: "unit_factor = (id :: finite_3 \<Rightarrow> _)"
definition [simp]: "euclidean_size x = (case x of a\<^sub>1 \<Rightarrow> 0 | _ \<Rightarrow> 1)"
definition [simp]: "division_segment (x :: finite_3) = 1"
-instance proof
+instance
+proof
fix x :: finite_3
assume "x \<noteq> 0"
then show "is_unit (unit_factor x)"
by (cases x) (simp_all add: dvd_finite_3_unfold)
-qed (auto simp add: divide_finite_3_def times_finite_3_def
-  dvd_finite_3_unfold inverse_finite_3_def plus_finite_3_def
-  split: finite_3.splits)
+qed
+  (subproofs
+    \<open>auto simp add: divide_finite_3_def times_finite_3_def
+      dvd_finite_3_unfold inverse_finite_3_def plus_finite_3_def
+      split: finite_3.splits\<close>)
end

hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3
@@ -1029,9 +1035,11 @@
| (a\<^sub>3, _) \<Rightarrow> a\<^sub>3 | (_, a\<^sub>3) \<Rightarrow> a\<^sub>3
| _ \<Rightarrow> a\<^sub>1)"

-instance proof
-qed(auto simp add: less_finite_4_def less_eq_finite_4_def Inf_finite_4_def Sup_finite_4_def
-    inf_finite_4_def sup_finite_4_def split: finite_4.splits)
+instance
+  by standard
+    (subproofs
+      \<open>auto simp add: less_finite_4_def less_eq_finite_4_def Inf_finite_4_def Sup_finite_4_def
+        inf_finite_4_def sup_finite_4_def split: finite_4.splits\<close>)
end

instance finite_4 :: complete_lattice ..
@@ -1042,9 +1050,10 @@
definition "- x = (case x of a\<^sub>1 \<Rightarrow> a\<^sub>4 | a\<^sub>2 \<Rightarrow> a\<^sub>3 | a\<^sub>3 \<Rightarrow> a\<^sub>2 | a\<^sub>4 \<Rightarrow> a\<^sub>1)"
definition "x - y = x \<sqinter> - (y :: finite_4)"
instance
-by intro_classes
-  (simp_all add: inf_finite_4_def sup_finite_4_def uminus_finite_4_def minus_finite_4_def
-    split: finite_4.splits)
+  by standard
+    (subproofs
+      \<open>simp_all add: inf_finite_4_def sup_finite_4_def uminus_finite_4_def minus_finite_4_def
+        split: finite_4.splits\<close>)
end

hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3 a\<^sub>4
@@ -1130,10 +1139,11 @@
| (a\<^sub>4, _) \<Rightarrow> a\<^sub>4 | (_, a\<^sub>4) \<Rightarrow> a\<^sub>4
| _ \<Rightarrow> a\<^sub>1)"

-instance
-proof
-qed (auto simp add: less_eq_finite_5_def less_finite_5_def inf_finite_5_def sup_finite_5_def
-    Inf_finite_5_def Sup_finite_5_def split: finite_5.splits if_split_asm)
+instance
+  by standard
+    (subproofs
+      \<open>auto simp add: less_eq_finite_5_def less_finite_5_def inf_finite_5_def sup_finite_5_def
+        Inf_finite_5_def Sup_finite_5_def split: finite_5.splits if_split_asm\<close>)
end

```