isabelle: src/HOL/ex/Sorting.ML@7b5ea59c0275 (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";
2031 03a843f0f447 Ran expandshort paulson parents: 1465 diff changeset	10	by (list.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";
2031 03a843f0f447 Ran expandshort paulson parents: 1465 diff changeset	16	by (list.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}";
2517 2af078382853 Modified some defs and shortened proofs. nipkow parents: 2031 diff changeset	23	by (list.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";
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
	Thu, 25 Jun 1998 13:57:34 +0200
changeset 5078	7b5ea59c0275
parent 5069	3ea049f7979d
child 5184	9b8547a9496a
permissions	-rw-r--r--