author | paulson |
Thu, 21 Aug 1997 12:53:23 +0200 | |
changeset 3647 | a64c8fbcd98f |
parent 3465 | e85c24717cad |
child 3842 | b55686a7b22c |
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 |
||
9 |
goal Sorting.thy "!x.mset (xs@ys) x = mset xs x + mset ys x"; |
|
2031 | 10 |
by (list.induct_tac "xs" 1); |
11 |
by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])))); |
|
2517 | 12 |
qed "mset_append"; |
969 | 13 |
|
14 |
goal Sorting.thy "!x. mset [x:xs. ~p(x)] x + mset [x:xs.p(x)] x = \ |
|
15 |
\ mset xs x"; |
|
2031 | 16 |
by (list.induct_tac "xs" 1); |
17 |
by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])))); |
|
969 | 18 |
qed "mset_compl_add"; |
19 |
||
2517 | 20 |
Addsimps [mset_append, mset_compl_add]; |
21 |
||
3465 | 22 |
goal Sorting.thy "set xs = {x.mset xs x ~= 0}"; |
2517 | 23 |
by (list.induct_tac "xs" 1); |
24 |
by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])))); |
|
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); |
|
33 |
by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_list_case])))); |
|
34 |
by (cut_facts_tac prems 1); |
|
35 |
by (Fast_tac 1); |
|
36 |
qed "sorted1_is_sorted"; |