src/HOL/ex/Qsort.ML
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 9747 043098ba5098
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
8590
89675b444abe added an order-sorted version of quickSort
paulson
parents: 8421
diff changeset
     1
(*  Title:      HOL/ex/Qsort.ML
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     2
    ID:         $Id$
8414
5983668cac15 now uses recdef instead of "rules"
paulson
parents: 6434
diff changeset
     3
    Author:     Tobias Nipkow (tidied by lcp)
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     4
    Copyright   1994 TU Muenchen
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     5
8414
5983668cac15 now uses recdef instead of "rules"
paulson
parents: 6434
diff changeset
     6
The verification of Quicksort
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     7
*)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     8
8590
89675b444abe added an order-sorted version of quickSort
paulson
parents: 8421
diff changeset
     9
(*** Version one: higher-order ***)
89675b444abe added an order-sorted version of quickSort
paulson
parents: 8421
diff changeset
    10
8414
5983668cac15 now uses recdef instead of "rules"
paulson
parents: 6434
diff changeset
    11
Goal "multiset (qsort(le,xs)) x = multiset xs x";
9747
043098ba5098 introduced induct_thm_tac
nipkow
parents: 9736
diff changeset
    12
by (induct_thm_tac qsort.induct "le xs" 1);
8414
5983668cac15 now uses recdef instead of "rules"
paulson
parents: 6434
diff changeset
    13
by Auto_tac;
5983668cac15 now uses recdef instead of "rules"
paulson
parents: 6434
diff changeset
    14
qed "qsort_permutes";
5983668cac15 now uses recdef instead of "rules"
paulson
parents: 6434
diff changeset
    15
Addsimps [qsort_permutes];
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    16
8414
5983668cac15 now uses recdef instead of "rules"
paulson
parents: 6434
diff changeset
    17
(*Also provable by induction*)
5983668cac15 now uses recdef instead of "rules"
paulson
parents: 6434
diff changeset
    18
Goal "set (qsort(le,xs)) = set xs";
5983668cac15 now uses recdef instead of "rules"
paulson
parents: 6434
diff changeset
    19
by (simp_tac (simpset() addsimps [set_via_multiset]) 1);
3647
a64c8fbcd98f Renamed theorems of the form set_of_list_XXX to set_XXX
paulson
parents: 3465
diff changeset
    20
qed "set_qsort";
a64c8fbcd98f Renamed theorems of the form set_of_list_XXX to set_XXX
paulson
parents: 3465
diff changeset
    21
Addsimps [set_qsort];
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    22
8421
7156b8e26a17 fixed the goal statement of sorted_qsort
paulson
parents: 8414
diff changeset
    23
Goal "total(le) --> transf(le) --> sorted le (qsort(le,xs))";
9747
043098ba5098 introduced induct_thm_tac
nipkow
parents: 9736
diff changeset
    24
by (induct_thm_tac qsort.induct "le xs" 1);
2511
282e9a9eae9d Got rid of Alls in favour of !x:set_of_list
nipkow
parents: 2031
diff changeset
    25
by (ALLGOALS Asm_simp_tac);
8414
5983668cac15 now uses recdef instead of "rules"
paulson
parents: 6434
diff changeset
    26
by (rewrite_goals_tac [Sorting.total_def, Sorting.transf_def]);
5983668cac15 now uses recdef instead of "rules"
paulson
parents: 6434
diff changeset
    27
by (Blast_tac 1);
5983668cac15 now uses recdef instead of "rules"
paulson
parents: 6434
diff changeset
    28
qed_spec_mp "sorted_qsort";
8590
89675b444abe added an order-sorted version of quickSort
paulson
parents: 8421
diff changeset
    29
89675b444abe added an order-sorted version of quickSort
paulson
parents: 8421
diff changeset
    30
89675b444abe added an order-sorted version of quickSort
paulson
parents: 8421
diff changeset
    31
(*** Version two: type classes ***)
89675b444abe added an order-sorted version of quickSort
paulson
parents: 8421
diff changeset
    32
89675b444abe added an order-sorted version of quickSort
paulson
parents: 8421
diff changeset
    33
Goal "multiset (quickSort xs) z = multiset xs z";
9736
332fab43628f Fixed rulify.
nipkow
parents: 8624
diff changeset
    34
by (res_inst_tac [("x","xs")] quickSort.induct 1);
8590
89675b444abe added an order-sorted version of quickSort
paulson
parents: 8421
diff changeset
    35
by Auto_tac;
89675b444abe added an order-sorted version of quickSort
paulson
parents: 8421
diff changeset
    36
qed "quickSort_permutes";
89675b444abe added an order-sorted version of quickSort
paulson
parents: 8421
diff changeset
    37
Addsimps [quickSort_permutes];
89675b444abe added an order-sorted version of quickSort
paulson
parents: 8421
diff changeset
    38
89675b444abe added an order-sorted version of quickSort
paulson
parents: 8421
diff changeset
    39
(*Also provable by induction*)
89675b444abe added an order-sorted version of quickSort
paulson
parents: 8421
diff changeset
    40
Goal "set (quickSort xs) = set xs";
89675b444abe added an order-sorted version of quickSort
paulson
parents: 8421
diff changeset
    41
by (simp_tac (simpset() addsimps [set_via_multiset]) 1);
89675b444abe added an order-sorted version of quickSort
paulson
parents: 8421
diff changeset
    42
qed "set_quickSort";
89675b444abe added an order-sorted version of quickSort
paulson
parents: 8421
diff changeset
    43
Addsimps [set_quickSort];
89675b444abe added an order-sorted version of quickSort
paulson
parents: 8421
diff changeset
    44
89675b444abe added an order-sorted version of quickSort
paulson
parents: 8421
diff changeset
    45
Goal "sorted (op <=) (quickSort xs)";
9736
332fab43628f Fixed rulify.
nipkow
parents: 8624
diff changeset
    46
by (res_inst_tac [("x","xs")] quickSort.induct 1);
8590
89675b444abe added an order-sorted version of quickSort
paulson
parents: 8421
diff changeset
    47
by (ALLGOALS Asm_simp_tac);
89675b444abe added an order-sorted version of quickSort
paulson
parents: 8421
diff changeset
    48
by (blast_tac (claset() addIs [linorder_linear RS disjE, order_trans]) 1);
89675b444abe added an order-sorted version of quickSort
paulson
parents: 8421
diff changeset
    49
qed_spec_mp "sorted_quickSort";