src/HOL/ex/Qsort.ML
author paulson
Thu Aug 06 15:48:13 1998 +0200 (1998-08-06)
changeset 5278 a903b66822e2
parent 5184 9b8547a9496a
child 6434 f2a2a40e56c8
permissions -rw-r--r--
even more tidying of Goal commands
     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 "!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);
    30 qed "qsort_permutes";
    31 
    32 Goal "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 (induct_tac "xs" 1);
    40 by (ALLGOALS Asm_simp_tac);
    41 qed"Ball_set_filter";
    42 Addsimps [Ball_set_filter];
    43 
    44 Goal "sorted le (xs@ys) = (sorted le xs & sorted le ys & \
    45 \                     (!x:set xs. !y:set ys. le x y))";
    46 by (induct_tac "xs" 1);
    47 by (ALLGOALS Asm_simp_tac);
    48 qed "sorted_append";
    49 Addsimps [sorted_append];
    50 
    51 Goal "[| total(le); transf(le) |] ==>  sorted le (qsort le xs)";
    52 by (res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
    53 by (ALLGOALS Asm_simp_tac);
    54 by (rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]);
    55 by (Fast_tac 1);
    56 qed "sorted_qsort";