# HG changeset patch
# User nipkow
# Date 759423637 -3600
# Node ID b503da67d2f740493eeac174831031f81f2e327f
# Parent  c1a3020635a1dbbded3fc95bc12d36cb238e9152
Verification of quicksort

diff -r c1a3020635a1 -r b503da67d2f7 ex/Qsort.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ex/Qsort.ML	Mon Jan 24 16:00:37 1994 +0100
@@ -0,0 +1,108 @@
+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();
diff -r c1a3020635a1 -r b503da67d2f7 ex/Qsort.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ex/Qsort.thy	Mon Jan 24 16:00:37 1994 +0100
@@ -0,0 +1,27 @@
+Qsort = List +
+consts
+  sorted :: "[['a,'a] => bool, 'a list] => bool"
+  mset   :: "'a list => ('a => nat)"
+  qsort  :: "[['a,'a] => bool, 'a list] => 'a list"
+
+rules
+
+sorted_Nil "sorted(le,[])"
+sorted_Cons "sorted(le,Cons(x,xs)) = ((Alls y:xs. le(x,y)) & sorted(le,xs))"
+
+mset_Nil "mset([],y) = 0"
+mset_Cons "mset(Cons(x,xs),y) = if(x=y, Suc(mset(xs,y)), mset(xs,y))"
+
+qsort_Nil  "qsort(le,[]) = []"
+qsort_Cons "qsort(le,Cons(x,xs)) = qsort(le,[y:xs . ~le(x,y)]) @ \
+\                                  Cons(x, qsort(le,[y:xs . le(x,y)]))"
+
+(* computational induction.
+   The dependence of p on x but not xs is intentional.
+*)
+qsort_ind
+ "[| P([]); \
+\    !!x xs. [| P([y:xs . ~p(x,y)]); P([y:xs . p(x,y)]) |] ==> \
+\            P(Cons(x,xs)) |] \
+\ ==> P(xs)"
+end
diff -r c1a3020635a1 -r b503da67d2f7 ex/qsort.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ex/qsort.ML	Mon Jan 24 16:00:37 1994 +0100
@@ -0,0 +1,108 @@
+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();
diff -r c1a3020635a1 -r b503da67d2f7 ex/qsort.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ex/qsort.thy	Mon Jan 24 16:00:37 1994 +0100
@@ -0,0 +1,27 @@
+Qsort = List +
+consts
+  sorted :: "[['a,'a] => bool, 'a list] => bool"
+  mset   :: "'a list => ('a => nat)"
+  qsort  :: "[['a,'a] => bool, 'a list] => 'a list"
+
+rules
+
+sorted_Nil "sorted(le,[])"
+sorted_Cons "sorted(le,Cons(x,xs)) = ((Alls y:xs. le(x,y)) & sorted(le,xs))"
+
+mset_Nil "mset([],y) = 0"
+mset_Cons "mset(Cons(x,xs),y) = if(x=y, Suc(mset(xs,y)), mset(xs,y))"
+
+qsort_Nil  "qsort(le,[]) = []"
+qsort_Cons "qsort(le,Cons(x,xs)) = qsort(le,[y:xs . ~le(x,y)]) @ \
+\                                  Cons(x, qsort(le,[y:xs . le(x,y)]))"
+
+(* computational induction.
+   The dependence of p on x but not xs is intentional.
+*)
+qsort_ind
+ "[| P([]); \
+\    !!x xs. [| P([y:xs . ~p(x,y)]); P([y:xs . p(x,y)]) |] ==> \
+\            P(Cons(x,xs)) |] \
+\ ==> P(xs)"
+end