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);
-qed "mset_compl_add";
+by Auto_tac;
+qed "multiset_compl_add";
 
-Addsimps [mset_append, mset_compl_add];
+Addsimps [multiset_append, multiset_compl_add];
 
-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 (ALLGOALS(asm_simp_tac (simpset() addsplits [list.split])));
-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";
+Addsimps [sorted_append];
+