src/HOL/ex/Qsort.ML
author paulson
Mon, 13 Mar 2000 12:42:05 +0100
changeset 8421 7156b8e26a17
parent 8414 5983668cac15
child 8590 89675b444abe
permissions -rw-r--r--
fixed the goal statement of sorted_qsort
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1266
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
8414
5983668cac15 now uses recdef instead of "rules"
paulson
parents: 6434
diff changeset
     9
Addsimps qsort.rules;
2511
282e9a9eae9d Got rid of Alls in favour of !x:set_of_list
nipkow
parents: 2031
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";
5983668cac15 now uses recdef instead of "rules"
paulson
parents: 6434
diff changeset
    12
by (res_inst_tac [("v","xs"),("u","le")] qsort.induct 1);
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))";
8414
5983668cac15 now uses recdef instead of "rules"
paulson
parents: 6434
diff changeset
    24
by (res_inst_tac [("v","xs"),("u","le")] qsort.induct 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";