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
clasohm@1465
     1
(*  Title:      HOL/ex/qsort.ML
clasohm@969
     2
    ID:         $Id$
clasohm@1465
     3
    Author:     Tobias Nipkow
clasohm@969
     4
    Copyright   1994 TU Muenchen
clasohm@969
     5
clasohm@969
     6
Two verifications of Quicksort
clasohm@969
     7
*)
clasohm@969
     8
nipkow@2526
     9
Addsimps [ball_Un];
nipkow@2511
    10
nipkow@2511
    11
(* Towards a proof of qsort_ind
nipkow@2511
    12
nipkow@2511
    13
A short proof of Konrad's wf_minimal in WF1.ML:
nipkow@2511
    14
nipkow@2511
    15
val [p1] = goalw WF.thy [wf_def]
nipkow@2511
    16
"wf(R) ==> (!Q. (? x. Q x) --> (? min. Q min & (!b. (b,min):R --> (~ Q b))))";
nipkow@2511
    17
by (rtac allI 1);
wenzelm@4423
    18
by (cut_inst_tac[("x","%u.~Q u")](p1 RS spec) 1);
nipkow@2511
    19
by (fast_tac HOL_cs 1);
nipkow@2511
    20
val wf_minimal = result();
nipkow@2511
    21
nipkow@2511
    22
*)
nipkow@2511
    23
nipkow@2511
    24
clasohm@1266
    25
Addsimps ([Qsort.qsort_Nil,Qsort.qsort_Cons]@conj_comms);
clasohm@969
    26
wenzelm@5069
    27
Goal "!x. mset (qsort le xs) x = mset xs x";
paulson@2031
    28
by (res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
nipkow@4686
    29
by (ALLGOALS Asm_simp_tac);
nipkow@2511
    30
qed "qsort_permutes";
clasohm@969
    31
wenzelm@5069
    32
Goal "set(qsort le xs) = set xs";
wenzelm@4423
    33
by (simp_tac (simpset() addsimps [set_via_mset,qsort_permutes]) 1);
paulson@3647
    34
qed "set_qsort";
paulson@3647
    35
Addsimps [set_qsort];
clasohm@969
    36
nipkow@2511
    37
goal List.thy
wenzelm@3842
    38
  "(!x:set[x:xs. P(x)].Q(x)) = (!x:set xs. P(x)-->Q(x))";
berghofe@5184
    39
by (induct_tac "xs" 1);
nipkow@4686
    40
by (ALLGOALS Asm_simp_tac);
paulson@3647
    41
qed"Ball_set_filter";
paulson@3647
    42
Addsimps [Ball_set_filter];
clasohm@969
    43
paulson@5278
    44
Goal "sorted le (xs@ys) = (sorted le xs & sorted le ys & \
nipkow@3465
    45
\                     (!x:set xs. !y:set ys. le x y))";
berghofe@5184
    46
by (induct_tac "xs" 1);
nipkow@2511
    47
by (ALLGOALS Asm_simp_tac);
nipkow@2511
    48
qed "sorted_append";
nipkow@2511
    49
Addsimps [sorted_append];
oheimb@1673
    50
paulson@5148
    51
Goal "[| total(le); transf(le) |] ==>  sorted le (qsort le xs)";
paulson@2031
    52
by (res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
nipkow@2511
    53
by (ALLGOALS Asm_simp_tac);
paulson@2031
    54
by (rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]);
paulson@2031
    55
by (Fast_tac 1);
nipkow@2511
    56
qed "sorted_qsort";