src/HOL/ex/Qsort.ML
author paulson
Mon Mar 13 12:42:05 2000 +0100 (2000-03-13)
changeset 8421 7156b8e26a17
parent 8414 5983668cac15
child 8590 89675b444abe
permissions -rw-r--r--
fixed the goal statement of sorted_qsort
clasohm@1465
     1
(*  Title:      HOL/ex/qsort.ML
clasohm@969
     2
    ID:         $Id$
paulson@8414
     3
    Author:     Tobias Nipkow (tidied by lcp)
clasohm@969
     4
    Copyright   1994 TU Muenchen
clasohm@969
     5
paulson@8414
     6
The verification of Quicksort
clasohm@969
     7
*)
clasohm@969
     8
paulson@8414
     9
Addsimps qsort.rules;
nipkow@2511
    10
paulson@8414
    11
Goal "multiset (qsort(le,xs)) x = multiset xs x";
paulson@8414
    12
by (res_inst_tac [("v","xs"),("u","le")] qsort.induct 1);
paulson@8414
    13
by Auto_tac;
paulson@8414
    14
qed "qsort_permutes";
paulson@8414
    15
Addsimps [qsort_permutes];
clasohm@969
    16
paulson@8414
    17
(*Also provable by induction*)
paulson@8414
    18
Goal "set (qsort(le,xs)) = set xs";
paulson@8414
    19
by (simp_tac (simpset() addsimps [set_via_multiset]) 1);
paulson@3647
    20
qed "set_qsort";
paulson@3647
    21
Addsimps [set_qsort];
clasohm@969
    22
paulson@8421
    23
Goal "total(le) --> transf(le) --> sorted le (qsort(le,xs))";
paulson@8414
    24
by (res_inst_tac [("v","xs"),("u","le")] qsort.induct 1);
nipkow@2511
    25
by (ALLGOALS Asm_simp_tac);
paulson@8414
    26
by (rewrite_goals_tac [Sorting.total_def, Sorting.transf_def]);
paulson@8414
    27
by (Blast_tac 1);
paulson@8414
    28
qed_spec_mp "sorted_qsort";