isabelle: src/HOL/ex/InSort.ML@b279a84ac11c (annotated)

1465 5d7a7e439cec expanded tabs clasohm parents: 1266 diff changeset	1	(* Title: HOL/ex/insort.ML
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	2	ID: $Id$
1465 5d7a7e439cec expanded tabs clasohm parents: 1266 diff changeset	3	Author: Tobias Nipkow
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
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	6	Correctness proof of insertion sort.
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	7	*)
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	8
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 4686 diff changeset	9	Goal "!y. mset(ins f x xs) y = mset (x#xs) y";
5184 9b8547a9496a Adapted to new datatype package. berghofe parents: 5143 diff changeset	10	by (induct_tac "xs" 1);
4686 74a12e86b20b Removed `addsplits [expand_if]' nipkow parents: 4089 diff changeset	11	by (ALLGOALS Asm_simp_tac);
2517 2af078382853 Modified some defs and shortened proofs. nipkow parents: 2511 diff changeset	12	qed "mset_ins";
2af078382853 Modified some defs and shortened proofs. nipkow parents: 2511 diff changeset	13	Addsimps [mset_ins];
2af078382853 Modified some defs and shortened proofs. nipkow parents: 2511 diff changeset	14
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 4686 diff changeset	15	Goal "!x. mset(insort f xs) x = mset xs x";
5184 9b8547a9496a Adapted to new datatype package. berghofe parents: 5143 diff changeset	16	by (induct_tac "xs" 1);
2517 2af078382853 Modified some defs and shortened proofs. nipkow parents: 2511 diff changeset	17	by (ALLGOALS Asm_simp_tac);
2af078382853 Modified some defs and shortened proofs. nipkow parents: 2511 diff changeset	18	qed "insort_permutes";
2af078382853 Modified some defs and shortened proofs. nipkow parents: 2511 diff changeset	19
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 4686 diff changeset	20	Goal "set(ins f x xs) = insert x (set xs)";
4686 74a12e86b20b Removed `addsplits [expand_if]' nipkow parents: 4089 diff changeset	21	by (asm_simp_tac (simpset() addsimps [set_via_mset]) 1);
2031 03a843f0f447 Ran expandshort paulson parents: 1820 diff changeset	22	by (Fast_tac 1);
3647 a64c8fbcd98f Renamed theorems of the form set_of_list_XXX to set_XXX paulson parents: 3465 diff changeset	23	qed "set_ins";
a64c8fbcd98f Renamed theorems of the form set_of_list_XXX to set_XXX paulson parents: 3465 diff changeset	24	Addsimps [set_ins];
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	25
2517 2af078382853 Modified some defs and shortened proofs. nipkow parents: 2511 diff changeset	26	val prems = goalw InSort.thy [total_def,transf_def]
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	27	"[\| total(f); transf(f) \|] ==> sorted f (ins f x xs) = sorted f xs";
5184 9b8547a9496a Adapted to new datatype package. berghofe parents: 5143 diff changeset	28	by (induct_tac "xs" 1);
4686 74a12e86b20b Removed `addsplits [expand_if]' nipkow parents: 4089 diff changeset	29	by (ALLGOALS Asm_simp_tac);
2031 03a843f0f447 Ran expandshort paulson parents: 1820 diff changeset	30	by (cut_facts_tac prems 1);
2517 2af078382853 Modified some defs and shortened proofs. nipkow parents: 2511 diff changeset	31	by (Fast_tac 1);
2511 282e9a9eae9d Got rid of Alls in favour of !x:set_of_list nipkow parents: 2031 diff changeset	32	qed "sorted_ins";
282e9a9eae9d Got rid of Alls in favour of !x:set_of_list nipkow parents: 2031 diff changeset	33	Addsimps [sorted_ins];
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	34
5143 b94cd208f073 Removal of leading "\!\!..." from most Goal commands paulson parents: 5069 diff changeset	35	Goal "[\| total(f); transf(f) \|] ==> sorted f (insort f xs)";
5184 9b8547a9496a Adapted to new datatype package. berghofe parents: 5143 diff changeset	36	by (induct_tac "xs" 1);
2031 03a843f0f447 Ran expandshort paulson parents: 1820 diff changeset	37	by (ALLGOALS Asm_simp_tac);
1750 817a34a54fb0 replaced result() by qed "sorted_insort" in last proof berghofe parents: 1465 diff changeset	38	qed "sorted_insort";

author	wenzelm
	Mon, 16 Nov 1998 10:41:08 +0100
changeset 5869	b279a84ac11c
parent 5184	9b8547a9496a
child 8422	6c6a5410a9bd
permissions	-rw-r--r--