author wenzelm Wed, 14 Mar 2012 15:59:39 +0100 changeset 46921 aa862ff8a8a9 parent 46920 5f44c8bea84e child 46922 3717f3878714
some proof indentation;
```--- a/src/HOL/Library/Multiset.thy	Wed Mar 14 15:37:51 2012 +0100
+++ b/src/HOL/Library/Multiset.thy	Wed Mar 14 15:59:39 2012 +0100
@@ -118,8 +118,8 @@
lemma count_union [simp]: "count (M + N) a = count M a + count N a"
by (simp add: union_def in_multiset multiset_typedef)

-instance multiset :: (type) cancel_comm_monoid_add proof
+  by default (simp_all add: multiset_eq_iff)

subsubsection {* Difference *}
@@ -270,8 +270,8 @@
definition less_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
mset_less_def: "(A::'a multiset) < B \<longleftrightarrow> A \<le> B \<and> A \<noteq> B"

-instance proof
-qed (auto simp add: mset_le_def mset_less_def multiset_eq_iff intro: order_trans antisym)
+instance
+  by default (auto simp add: mset_le_def mset_less_def multiset_eq_iff intro: order_trans antisym)

end

@@ -377,10 +377,11 @@
definition inf_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" where
multiset_inter_def: "inf_multiset A B = A - (A - B)"

-instance proof -
+instance
+proof -
have aux: "\<And>m n q :: nat. m \<le> n \<Longrightarrow> m \<le> q \<Longrightarrow> m \<le> n - (n - q)" by arith
-  show "OFCLASS('a multiset, semilattice_inf_class)" proof
-  qed (auto simp add: multiset_inter_def mset_le_def aux)
+  show "OFCLASS('a multiset, semilattice_inf_class)"
+    by default (auto simp add: multiset_inter_def mset_le_def aux)
qed

end
@@ -822,7 +823,8 @@
lemma multiset_of_eq_length:
assumes "multiset_of xs = multiset_of ys"
shows "length xs = length ys"
-using assms proof (induct xs arbitrary: ys)
+using assms
+proof (induct xs arbitrary: ys)
case Nil then show ?case by simp
next
case (Cons x xs)
@@ -845,7 +847,8 @@
next
case True
moreover have "z \<in># multiset_of ys" using assms True by simp
-  show ?thesis using assms proof (induct xs arbitrary: ys)
+  show ?thesis using assms
+  proof (induct xs arbitrary: ys)
case Nil then show ?case by simp
next
case (Cons x xs)
@@ -864,7 +867,8 @@
assumes f: "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"
and equiv: "multiset_of xs = multiset_of ys"
shows "fold f xs = fold f ys"
-using f equiv [symmetric] proof (induct xs arbitrary: ys)
+using f equiv [symmetric]
+proof (induct xs arbitrary: ys)
case Nil then show ?case by simp
next
case (Cons x xs)
@@ -898,7 +902,8 @@
and "\<And>k. k \<in> set ys \<Longrightarrow> filter (\<lambda>x. f k = f x) ys = filter (\<lambda>x. f k = f x) xs"
and "sorted (map f ys)"
shows "sort_key f xs = ys"
-using assms proof (induct xs arbitrary: ys)
+using assms
+proof (induct xs arbitrary: ys)
case Nil then show ?case by simp
next
case (Cons x xs)
@@ -994,10 +999,12 @@
proof (cases xs)
case Nil then show ?thesis by simp
next
-  case (Cons _ ys) note hyps = Cons show ?thesis proof (cases ys)
+  case (Cons _ ys) note hyps = Cons show ?thesis
+  proof (cases ys)
case Nil with hyps show ?thesis by simp
next
-    case (Cons _ zs) note hyps = hyps Cons show ?thesis proof (cases zs)
+    case (Cons _ zs) note hyps = hyps Cons show ?thesis
+    proof (cases zs)
case Nil with hyps show ?thesis by auto
next
case Cons
@@ -1224,8 +1231,8 @@
definition
[code]: "HOL.equal A B \<longleftrightarrow> (A::'a multiset) \<le> B \<and> B \<le> A"

-instance proof
+instance
+  by default (simp add: equal_multiset_def eq_iff)

end

@@ -1512,8 +1519,8 @@
qed
have trans: "\<And>K M N :: 'a multiset. K \<subset># M \<Longrightarrow> M \<subset># N \<Longrightarrow> K \<subset># N"
unfolding less_multiset_def mult_def by (blast intro: trancl_trans)
-  show "class.order (le_multiset :: 'a multiset \<Rightarrow> _) less_multiset" proof
-  qed (auto simp add: le_multiset_def irrefl dest: trans)
+  show "class.order (le_multiset :: 'a multiset \<Rightarrow> _) less_multiset"
+    by default (auto simp add: le_multiset_def irrefl dest: trans)
qed

lemma mult_less_irrefl [elim!]: "M \<subset># (M::'a::order multiset) ==> R"
@@ -1785,14 +1792,12 @@

enriched_type image_mset: image_mset
proof -
-  fix f g
-  show "image_mset f \<circ> image_mset g = image_mset (f \<circ> g)"
+  fix f g show "image_mset f \<circ> image_mset g = image_mset (f \<circ> g)"
proof
fix A
show "(image_mset f \<circ> image_mset g) A = image_mset (f \<circ> g) A"
by (induct A) simp_all
qed
-next
show "image_mset id = id"
proof
fix A```