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

969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	1	(* Title: HOL/ex/sorting.ML
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	2	ID: $Id$
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	3	Author: Tobias Nipkow
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
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	9	val sorting_ss = list_ss addsimps
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	10	[Sorting.mset_Nil,Sorting.mset_Cons,
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	11	Sorting.sorted_Nil,Sorting.sorted_Cons,
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	12	Sorting.sorted1_Nil,Sorting.sorted1_One,Sorting.sorted1_Cons];
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	13
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	14	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	15	by(list.induct_tac "xs" 1);
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	16	by(ALLGOALS(asm_simp_tac (sorting_ss setloop (split_tac [expand_if]))));
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	17	qed "mset_app_distr";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	18
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	19	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	20	\ mset xs x";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	21	by(list.induct_tac "xs" 1);
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	22	by(ALLGOALS(asm_simp_tac (sorting_ss setloop (split_tac [expand_if]))));
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	23	qed "mset_compl_add";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	24
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	25	val sorting_ss = sorting_ss addsimps
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	26	[mset_app_distr, mset_compl_add];

author	clasohm
	Wed, 21 Jun 1995 15:47:10 +0200
changeset 1151	c820b3cc3df0
parent 969	b051e2fc2e34
child 1266	3ae9fe3c0f68
permissions	-rw-r--r--