src/HOL/ex/InSort.ML

--- a/src/HOL/ex/InSort.ML	Mon Mar 13 12:42:05 2000 +0100
+++ b/src/HOL/ex/InSort.ML	Mon Mar 13 12:42:41 2000 +0100
@@ -6,33 +6,32 @@
 Correctness proof of insertion sort.
 *)
 
-Goal "!y. mset(ins f x xs) y = mset (x#xs) y";
+Goal "!y. multiset(ins le x xs) y = multiset (x#xs) y";
 by (induct_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "mset_ins";
-Addsimps [mset_ins];
+by Auto_tac;
+qed_spec_mp "multiset_ins";
+Addsimps [multiset_ins];
 
-Goal "!x. mset(insort f xs) x = mset xs x";
+Goal "!x. multiset(insort le xs) x = multiset xs x";
 by (induct_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "insort_permutes";
+by Auto_tac;
+qed_spec_mp "insort_permutes";
 
-Goal "set(ins f x xs) = insert x (set xs)";
-by (asm_simp_tac (simpset() addsimps [set_via_mset]) 1);
+Goal "set(ins le x xs) = insert x (set xs)";
+by (asm_simp_tac (simpset() addsimps [set_via_multiset]) 1);
 by (Fast_tac 1);
 qed "set_ins";
 Addsimps [set_ins];
 
-val prems = goalw InSort.thy [total_def,transf_def]
-  "[| total(f); transf(f) |] ==>  sorted f (ins f x xs) = sorted f xs";
+Goal "total(le) --> transf(le) --> sorted le (ins le x xs) = sorted le xs";
 by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
-by (cut_facts_tac prems 1);
-by (Fast_tac 1);
-qed "sorted_ins";
+by (rewrite_goals_tac [Sorting.total_def, Sorting.transf_def]);
+by (Blast_tac 1);
+qed_spec_mp "sorted_ins";
 Addsimps [sorted_ins];
 
-Goal "[| total(f); transf(f) |] ==>  sorted f (insort f xs)";
+Goal "[| total(le); transf(le) |] ==>  sorted le (insort le xs)";
 by (induct_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
+by Auto_tac;
 qed "sorted_insort";