ex/qsort.ML

Verification 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];


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);
by(ALLGOALS(asm_simp_tac (ss setloop (split_tac [expand_if]))));
result();


goal Qsort.thy "(Alls x:[x:xs.P(x)].Q(x)) = (Alls x:xs. P(x)-->Q(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
 "((Alls x:xs.P(x)) & (Alls x:xs.Q(x))) = (Alls x:xs. P(x)&Q(x))";
by(list_ind_tac "xs" 1);
by(ALLGOALS(asm_simp_tac ss));
by(fast_tac HOL_cs 1);
val ss = ss addsimps [result()];

goal Qsort.thy "(list_all(p,xs) & Q & list_all(q,ys)) = \
\               (Q & list_all(p,xs) & list_all(q,ys))";
by(fast_tac HOL_cs 1);
val lemma1 = result();

goal HOL.thy "((~P --> Q) & (P --> Q)) = Q";
by(fast_tac HOL_cs 1);
val lemma2 = result();

goal Qsort.thy "(Alls x:qsort(le,xs).P(x))  =  (Alls x:xs.P(x))";
by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
by(ALLGOALS(asm_simp_tac (ss addsimps [lemma1,lemma2])));
val ss = ss addsimps [result()];

goal Qsort.thy
 "sorted(le,xs@ys) = (sorted(le,xs) & sorted(le,ys) & \
\                     (Alls x:xs. Alls y:ys. le(x,y)))";
by(list_ind_tac "xs" 1);
by(ALLGOALS(asm_simp_tac ss));
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))";
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(fast_tac HOL_cs 1);
result();


(* A verification based on predicate calculus rather than combinators *)

val sorted_Cons =
  rewrite_rule [list_all_mem_conv RS eq_reflection] Qsort.sorted_Cons;

val ss = list_ss addsimps
 [Qsort.sorted_Nil,sorted_Cons,
  Qsort.qsort_Nil,Qsort.qsort_Cons];


goal List.thy "x mem [x:xs.P(x)] = (x mem xs & P(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 mem qsort(le,xs)  =  x mem xs";
by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
by(ALLGOALS(asm_simp_tac (ss setloop (split_tac [expand_if]))));
by(fast_tac HOL_cs 1);
val ss = ss addsimps [result()];

goal Qsort.thy
 "sorted(le,xs@ys) = (sorted(le,xs) & sorted(le,ys) & \
\                     (!x. x mem xs --> (!y. y mem ys --> le(x,y))))";
by(list_ind_tac "xs" 1);
by(ALLGOALS(asm_simp_tac (ss setloop (split_tac [expand_if]))));
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))";
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(fast_tac HOL_cs 1);
result();