ex/qsort.ML

--- a/ex/qsort.ML	Wed Feb 16 15:13:53 1994 +0100
+++ b/ex/qsort.ML	Wed Feb 23 10:05:35 1994 +0100
@@ -6,22 +6,8 @@
 Two verifications of Quicksort
 *)
 
-val ss = list_ss addsimps
- [Qsort.mset_Nil,Qsort.mset_Cons,
-  Qsort.sorted_Nil,Qsort.sorted_Cons,
-  Qsort.qsort_Nil,Qsort.qsort_Cons];
-
+val ss = sorting_ss addsimps [Qsort.qsort_Nil,Qsort.qsort_Cons];
 
-goal Qsort.thy "!x.mset(xs@ys,x) = mset(xs,x)+mset(ys,x)";
-by(list_ind_tac "xs" 1);
-by(ALLGOALS(asm_simp_tac (ss setloop (split_tac [expand_if]))));
-val ss = ss addsimps [result()];
-
-goal Qsort.thy "!x. mset([x:xs. ~p(x)], x) + mset([x:xs.p(x)], x) = \
-\                   mset(xs, x)";
-by(list_ind_tac "xs" 1);
-by(ALLGOALS(asm_simp_tac (ss setloop (split_tac [expand_if]))));
-val ss = ss addsimps [result()];
 
 goal Qsort.thy "!x. mset(qsort(le,xs),x) = mset(xs,x)";
 by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
@@ -63,13 +49,11 @@
 by(fast_tac HOL_cs 1);
 val ss = ss addsimps [result()];
 
-val prems = goal Qsort.thy
- "[| !x y. (~le(x,y)) = le(y,x); \
-\    !x y z. le(x,y) & le(y,z) --> le(x,z) |] ==> \
-\ sorted(le,qsort(le,xs))";
+goal Qsort.thy 
+ "!!le. [| total(le); transf(le) |] ==>  sorted(le,qsort(le,xs))";
 by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
-by(ALLGOALS(asm_full_simp_tac (ss addsimps [hd prems,list_all_mem_conv]) ));
-by(cut_facts_tac (tl prems) 1);
+by(ALLGOALS(asm_full_simp_tac (ss addsimps [list_all_mem_conv]) ));
+by(rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]);
 by(fast_tac HOL_cs 1);
 result();
 
@@ -77,10 +61,10 @@
 (* A verification based on predicate calculus rather than combinators *)
 
 val sorted_Cons =
-  rewrite_rule [list_all_mem_conv RS eq_reflection] Qsort.sorted_Cons;
+  rewrite_rule [list_all_mem_conv RS eq_reflection] Sorting.sorted_Cons;
 
 val ss = list_ss addsimps
- [Qsort.sorted_Nil,sorted_Cons,
+ [Sorting.sorted_Nil,sorted_Cons,
   Qsort.qsort_Nil,Qsort.qsort_Cons];
 
 
@@ -98,14 +82,11 @@
 by(fast_tac HOL_cs 1);
 val ss = ss addsimps [result()];
 
-val prems = goal Qsort.thy
- "[| !x y. (~le(x,y)) = le(y,x); \
-\    !x y z. le(x,y) & le(y,z) --> le(x,z) |] ==> \
-\ sorted(le,qsort(le,xs))";
+goal Qsort.thy
+  "!!xs. [| total(le); transf(le) |] ==>  sorted(le,qsort(le,xs))";
 by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
 by(simp_tac ss 1);
-by(asm_full_simp_tac (ss addsimps [hd prems]
-                         setloop (split_tac [expand_if])) 1);
-by(cut_facts_tac (tl prems) 1);
+by(asm_full_simp_tac (ss setloop (split_tac [expand_if])) 1);
+by(rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]);
 by(fast_tac HOL_cs 1);
 result();