isabelle: src/HOL/ex/Sorting.ML@5d7a7e439cec (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
1266 3ae9fe3c0f68 added local simpsets clasohm parents: 969 diff changeset	9	Addsimps [Sorting.mset_Nil,Sorting.mset_Cons,
3ae9fe3c0f68 added local simpsets clasohm parents: 969 diff changeset	10	Sorting.sorted_Nil,Sorting.sorted_Cons,
3ae9fe3c0f68 added local simpsets clasohm parents: 969 diff changeset	11	Sorting.sorted1_Nil,Sorting.sorted1_One,Sorting.sorted1_Cons];
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	12
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	13	goal Sorting.thy "!x.mset (xs@ys) x = mset xs x + mset ys x";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	14	by(list.induct_tac "xs" 1);
1266 3ae9fe3c0f68 added local simpsets clasohm parents: 969 diff changeset	15	by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	16	qed "mset_app_distr";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	17
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	18	goal Sorting.thy "!x. mset [x:xs. ~p(x)] x + mset [x:xs.p(x)] x = \
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	19	\ mset xs x";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	20	by(list.induct_tac "xs" 1);
1266 3ae9fe3c0f68 added local simpsets clasohm parents: 969 diff changeset	21	by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	22	qed "mset_compl_add";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	23
1266 3ae9fe3c0f68 added local simpsets clasohm parents: 969 diff changeset	24	Addsimps [mset_app_distr, mset_compl_add];

author	clasohm
	Tue, 30 Jan 1996 15:24:36 +0100
changeset 1465	5d7a7e439cec
parent 1266	3ae9fe3c0f68
child 2031	03a843f0f447
permissions	-rw-r--r--