author | paulson |
Mon, 20 Mar 2000 10:32:02 +0100 | |
changeset 8525 | 209eb2db72e6 |
parent 8415 | 852c63072334 |
child 12486 | 0ed8bdd883e0 |
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 |
||
8415 | 9 |
Goal "multiset (xs@ys) x = multiset xs x + multiset ys x"; |
5184 | 10 |
by (induct_tac "xs" 1); |
8415 | 11 |
by Auto_tac; |
12 |
qed "multiset_append"; |
|
969 | 13 |
|
8525
209eb2db72e6
renamed a variable to avoid possible free/bound confusion
paulson
parents:
8415
diff
changeset
|
14 |
Goal "multiset [x:xs. ~p(x)] z + multiset [x:xs. p(x)] z = multiset xs z"; |
5184 | 15 |
by (induct_tac "xs" 1); |
8415 | 16 |
by Auto_tac; |
17 |
qed "multiset_compl_add"; |
|
969 | 18 |
|
8415 | 19 |
Addsimps [multiset_append, multiset_compl_add]; |
2517 | 20 |
|
8415 | 21 |
Goal "set xs = {x. multiset xs x ~= 0}"; |
5184 | 22 |
by (induct_tac "xs" 1); |
8415 | 23 |
by Auto_tac; |
24 |
qed "set_via_multiset"; |
|
2517 | 25 |
|
26 |
(* Equivalence of two definitions of `sorted' *) |
|
27 |
||
8415 | 28 |
Goal "transf(le) ==> sorted1 le xs = sorted le xs"; |
5184 | 29 |
by (induct_tac "xs" 1); |
8415 | 30 |
by (ALLGOALS (asm_simp_tac (simpset() addsplits [list.split]))); |
31 |
by (rewrite_goals_tac [transf_def]); |
|
32 |
by (Blast_tac 1); |
|
2517 | 33 |
qed "sorted1_is_sorted"; |
8415 | 34 |
|
35 |
Goal "sorted le (xs@ys) = (sorted le xs & sorted le ys & \ |
|
36 |
\ (ALL x:set xs. ALL y:set ys. le x y))"; |
|
37 |
by (induct_tac "xs" 1); |
|
38 |
by Auto_tac; |
|
39 |
qed "sorted_append"; |
|
40 |
Addsimps [sorted_append]; |
|
41 |