isabelle: src/HOL/ex/Qsort.ML@7156b8e26a17 (annotated)

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";

author	paulson
	Mon, 13 Mar 2000 12:42:05 +0100
changeset 8421	7156b8e26a17
parent 8414	5983668cac15
child 8590	89675b444abe
permissions	-rw-r--r--