diff -r f04b33ce250f -r a4dc62a46ee4 ex/Qsort.ML --- a/ex/Qsort.ML Tue Oct 24 14:59:17 1995 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,84 +0,0 @@ -(* Title: HOL/ex/qsort.ML - ID: $Id$ - Author: Tobias Nipkow - Copyright 1994 TU Muenchen - -Two verifications of Quicksort -*) - -val ss = sorting_ss addsimps ([Qsort.qsort_Nil,Qsort.qsort_Cons]@conj_comms); - -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.induct_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.induct_tac "xs" 1); -by(ALLGOALS(asm_simp_tac ss)); -val ss = ss addsimps [result()]; - -goal HOL.thy "((~P --> Q) & (P --> Q)) = Q"; -by(fast_tac HOL_cs 1); -qed "lemma"; - -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 [lemma]))); -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.induct_tac "xs" 1); -by(ALLGOALS(asm_simp_tac ss)); -val ss = ss addsimps [result()]; - -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 [list_all_mem_conv]) )); -by(rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]); -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] Sorting.sorted_Cons; - -val ss = list_ss addsimps - [Sorting.sorted_Nil,sorted_Cons, - Qsort.qsort_Nil,Qsort.qsort_Cons]; - - -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.induct_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()]; - -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 setloop (split_tac [expand_if])) 1); -by(rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]); -by(fast_tac HOL_cs 1); -result();