src/HOL/ex/Sorting.ML
 changeset 8415 852c63072334 parent 5184 9b8547a9496a child 8525 209eb2db72e6
```--- a/src/HOL/ex/Sorting.ML	Fri Mar 10 17:52:48 2000 +0100
+++ b/src/HOL/ex/Sorting.ML	Fri Mar 10 17:53:16 2000 +0100
@@ -6,31 +6,36 @@
Some general lemmas
*)

-Goal "!x. mset (xs@ys) x = mset xs x + mset ys x";
+Goal "multiset (xs@ys) x = multiset xs x + multiset ys x";
by (induct_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "mset_append";
+by Auto_tac;
+qed "multiset_append";

-Goal "!x. mset [x:xs. ~p(x)] x + mset [x:xs. p(x)] x = \
-\                     mset xs x";
+Goal "multiset [x:xs. ~p(x)] x + multiset [x:xs. p(x)] x = multiset xs x";
by (induct_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
+by Auto_tac;

-Goal "set xs = {x. mset xs x ~= 0}";
+Goal "set xs = {x. multiset xs x ~= 0}";
by (induct_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
-by (Fast_tac 1);
-qed "set_via_mset";
+by Auto_tac;
+qed "set_via_multiset";

(* Equivalence of two definitions of `sorted' *)

-val prems = goalw Sorting.thy [transf_def]
-  "transf(le) ==> sorted1 le xs = sorted le xs";
+Goal "transf(le) ==> sorted1 le xs = sorted le xs";
by (induct_tac "xs" 1);
-by (cut_facts_tac prems 1);
-by (Fast_tac 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsplits [list.split])));
+by (rewrite_goals_tac [transf_def]);
+by (Blast_tac 1);
qed "sorted1_is_sorted";
+
+Goal "sorted le (xs@ys) = (sorted le xs & sorted le ys & \
+\                         (ALL x:set xs. ALL y:set ys. le x y))";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed "sorted_append";