author | wenzelm |
Mon, 03 Nov 1997 12:13:18 +0100 | |
changeset 4089 | 96fba19bcbe2 |
parent 4069 | d6d06a03a2e9 |
child 4686 | 74a12e86b20b |
permissions | -rw-r--r-- |
1465 | 1 |
(* Title: HOL/ex/sorting.ML |
969 | 2 |
ID: $Id$ |
1465 | 3 |
Author: Tobias Nipkow |
969 | 4 |
Copyright 1994 TU Muenchen |
5 |
||
6 |
Some general lemmas |
|
7 |
*) |
|
8 |
||
3842 | 9 |
goal Sorting.thy "!x. mset (xs@ys) x = mset xs x + mset ys x"; |
2031 | 10 |
by (list.induct_tac "xs" 1); |
4089 | 11 |
by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if]))); |
2517 | 12 |
qed "mset_append"; |
969 | 13 |
|
3842 | 14 |
goal Sorting.thy "!x. mset [x:xs. ~p(x)] x + mset [x:xs. p(x)] x = \ |
969 | 15 |
\ mset xs x"; |
2031 | 16 |
by (list.induct_tac "xs" 1); |
4089 | 17 |
by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if]))); |
969 | 18 |
qed "mset_compl_add"; |
19 |
||
2517 | 20 |
Addsimps [mset_append, mset_compl_add]; |
21 |
||
3842 | 22 |
goal Sorting.thy "set xs = {x. mset xs x ~= 0}"; |
2517 | 23 |
by (list.induct_tac "xs" 1); |
4089 | 24 |
by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if]))); |
2517 | 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 | 27 |
|
28 |
(* Equivalence of two definitions of `sorted' *) |
|
29 |
||
30 |
val prems = goalw Sorting.thy [transf_def] |
|
31 |
"transf(le) ==> sorted1 le xs = sorted le xs"; |
|
32 |
by (list.induct_tac "xs" 1); |
|
4089 | 33 |
by (ALLGOALS(asm_simp_tac (simpset() addsplits [split_list_case]))); |
2517 | 34 |
by (cut_facts_tac prems 1); |
35 |
by (Fast_tac 1); |
|
36 |
qed "sorted1_is_sorted"; |