src/HOL/ex/Qsort.ML
author paulson
Wed Nov 05 13:23:46 1997 +0100 (1997-11-05)
changeset 4153 e534c4c32d54
parent 4089 96fba19bcbe2
child 4423 a129b817b58a
permissions -rw-r--r--
Ran expandshort, especially to introduce Safe_tac
     1 (*  Title:      HOL/ex/qsort.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1994 TU Muenchen
     5 
     6 Two verifications of Quicksort
     7 *)
     8 
     9 Addsimps [ball_Un];
    10 
    11 (* Towards a proof of qsort_ind
    12 
    13 A short proof of Konrad's wf_minimal in WF1.ML:
    14 
    15 val [p1] = goalw WF.thy [wf_def]
    16 "wf(R) ==> (!Q. (? x. Q x) --> (? min. Q min & (!b. (b,min):R --> (~ Q b))))";
    17 by (rtac allI 1);
    18 by(cut_inst_tac[("x","%u.~Q u")](p1 RS spec) 1);
    19 by (fast_tac HOL_cs 1);
    20 val wf_minimal = result();
    21 
    22 *)
    23 
    24 
    25 Addsimps ([Qsort.qsort_Nil,Qsort.qsort_Cons]@conj_comms);
    26 
    27 goal Qsort.thy "!x. mset (qsort le xs) x = mset xs x";
    28 by (res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
    29 by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
    30 qed "qsort_permutes";
    31 
    32 goal Qsort.thy "set(qsort le xs) = set xs";
    33 by(simp_tac (simpset() addsimps [set_via_mset,qsort_permutes]) 1);
    34 qed "set_qsort";
    35 Addsimps [set_qsort];
    36 
    37 goal List.thy
    38   "(!x:set[x:xs. P(x)].Q(x)) = (!x:set xs. P(x)-->Q(x))";
    39 by (list.induct_tac "xs" 1);
    40 by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
    41 qed"Ball_set_filter";
    42 Addsimps [Ball_set_filter];
    43 
    44 goal Qsort.thy
    45  "sorted le (xs@ys) = (sorted le xs & sorted le ys & \
    46 \                     (!x:set xs. !y:set ys. le x y))";
    47 by (list.induct_tac "xs" 1);
    48 by (ALLGOALS Asm_simp_tac);
    49 qed "sorted_append";
    50 Addsimps [sorted_append];
    51 
    52 goal Qsort.thy 
    53  "!!le. [| total(le); transf(le) |] ==>  sorted le (qsort le xs)";
    54 by (res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
    55 by (ALLGOALS Asm_simp_tac);
    56 by (rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]);
    57 by (Fast_tac 1);
    58 qed "sorted_qsort";