isabelle: src/HOL/ex/Sorting.ML@7da8033264fa (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
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 4686 diff changeset	9	Goal "!x. mset (xs@ys) x = mset xs x + mset ys x";
5184 9b8547a9496a Adapted to new datatype package. berghofe parents: 5069 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: 2031 diff changeset	12	qed "mset_append";
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	13
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 4686 diff changeset	14	Goal "!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";
5184 9b8547a9496a Adapted to new datatype package. berghofe parents: 5069 diff changeset	16	by (induct_tac "xs" 1);
4686 74a12e86b20b Removed `addsplits [expand_if]' nipkow parents: 4089 diff changeset	17	by (ALLGOALS Asm_simp_tac);
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
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 4686 diff changeset	22	Goal "set xs = {x. mset xs x ~= 0}";
5184 9b8547a9496a Adapted to new datatype package. berghofe parents: 5069 diff changeset	23	by (induct_tac "xs" 1);
4686 74a12e86b20b Removed `addsplits [expand_if]' nipkow parents: 4089 diff changeset	24	by (ALLGOALS Asm_simp_tac);
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";
5184 9b8547a9496a Adapted to new datatype package. berghofe parents: 5069 diff changeset	32	by (induct_tac "xs" 1);
9b8547a9496a Adapted to new datatype package. berghofe parents: 5069 diff changeset	33	by (ALLGOALS(asm_simp_tac (simpset() addsplits [list.split])));
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	wenzelm
	Tue, 17 Nov 1998 14:10:40 +0100
changeset 5911	7da8033264fa
parent 5184	9b8547a9496a
child 8415	852c63072334
permissions	-rw-r--r--