isabelle: src/HOL/ex/Sorting.ML@e534c4c32d54 (annotated)

1465 5d7a7e439cec expanded tabs clasohm parents: 1266 diff changeset	1	(* Title: HOL/ex/sorting.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	Some general lemmas
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	7	*)
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	8
3842 b55686a7b22c fixed dots; wenzelm parents: 3647 diff changeset	9	goal Sorting.thy "!x. mset (xs@ys) x = mset xs x + mset ys x";
2031 03a843f0f447 Ran expandshort paulson parents: 1465 diff changeset	10	by (list.induct_tac "xs" 1);
4089 96fba19bcbe2 isatool fixclasimp; wenzelm parents: 4069 diff changeset	11	by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
2517 2af078382853 Modified some defs and shortened proofs. nipkow parents: 2031 diff changeset	12	qed "mset_append";
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	13
3842 b55686a7b22c fixed dots; wenzelm parents: 3647 diff changeset	14	goal Sorting.thy "!x. mset [x:xs. ~p(x)] x + mset [x:xs. p(x)] x = \
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	15	\ mset xs x";
2031 03a843f0f447 Ran expandshort paulson parents: 1465 diff changeset	16	by (list.induct_tac "xs" 1);
4089 96fba19bcbe2 isatool fixclasimp; wenzelm parents: 4069 diff changeset	17	by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	18	qed "mset_compl_add";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	19
2517 2af078382853 Modified some defs and shortened proofs. nipkow parents: 2031 diff changeset	20	Addsimps [mset_append, mset_compl_add];
2af078382853 Modified some defs and shortened proofs. nipkow parents: 2031 diff changeset	21
3842 b55686a7b22c fixed dots; wenzelm parents: 3647 diff changeset	22	goal Sorting.thy "set xs = {x. mset xs x ~= 0}";
2517 2af078382853 Modified some defs and shortened proofs. nipkow parents: 2031 diff changeset	23	by (list.induct_tac "xs" 1);
4089 96fba19bcbe2 isatool fixclasimp; wenzelm parents: 4069 diff changeset	24	by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
2517 2af078382853 Modified some defs and shortened proofs. nipkow parents: 2031 diff changeset	25	by (Fast_tac 1);
3647 a64c8fbcd98f Renamed theorems of the form set_of_list_XXX to set_XXX paulson parents: 3465 diff changeset	26	qed "set_via_mset";
2517 2af078382853 Modified some defs and shortened proofs. nipkow parents: 2031 diff changeset	27
2af078382853 Modified some defs and shortened proofs. nipkow parents: 2031 diff changeset	28	(* Equivalence of two definitions of `sorted' *)
2af078382853 Modified some defs and shortened proofs. nipkow parents: 2031 diff changeset	29
2af078382853 Modified some defs and shortened proofs. nipkow parents: 2031 diff changeset	30	val prems = goalw Sorting.thy [transf_def]
2af078382853 Modified some defs and shortened proofs. nipkow parents: 2031 diff changeset	31	"transf(le) ==> sorted1 le xs = sorted le xs";
2af078382853 Modified some defs and shortened proofs. nipkow parents: 2031 diff changeset	32	by (list.induct_tac "xs" 1);
4089 96fba19bcbe2 isatool fixclasimp; wenzelm parents: 4069 diff changeset	33	by (ALLGOALS(asm_simp_tac (simpset() addsplits [split_list_case])));
2517 2af078382853 Modified some defs and shortened proofs. nipkow parents: 2031 diff changeset	34	by (cut_facts_tac prems 1);
2af078382853 Modified some defs and shortened proofs. nipkow parents: 2031 diff changeset	35	by (Fast_tac 1);
2af078382853 Modified some defs and shortened proofs. nipkow parents: 2031 diff changeset	36	qed "sorted1_is_sorted";

author	paulson
	Wed, 05 Nov 1997 13:23:46 +0100
changeset 4153	e534c4c32d54
parent 4089	96fba19bcbe2
child 4686	74a12e86b20b
permissions	-rw-r--r--