src/HOL/ex/Sorting.ML
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 8525 209eb2db72e6
child 12486 0ed8bdd883e0
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
8415
paulson
parents: 5184
diff changeset
     9
Goal "multiset (xs@ys) x = multiset xs x + multiset ys x";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5069
diff changeset
    10
by (induct_tac "xs" 1);
8415
paulson
parents: 5184
diff changeset
    11
by Auto_tac;
paulson
parents: 5184
diff changeset
    12
qed "multiset_append";
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    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
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5069
diff changeset
    15
by (induct_tac "xs" 1);
8415
paulson
parents: 5184
diff changeset
    16
by Auto_tac;
paulson
parents: 5184
diff changeset
    17
qed "multiset_compl_add";
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    18
8415
paulson
parents: 5184
diff changeset
    19
Addsimps [multiset_append, multiset_compl_add];
2517
2af078382853 Modified some defs and shortened proofs.
nipkow
parents: 2031
diff changeset
    20
8415
paulson
parents: 5184
diff changeset
    21
Goal "set xs = {x. multiset xs x ~= 0}";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5069
diff changeset
    22
by (induct_tac "xs" 1);
8415
paulson
parents: 5184
diff changeset
    23
by Auto_tac;
paulson
parents: 5184
diff changeset
    24
qed "set_via_multiset";
2517
2af078382853 Modified some defs and shortened proofs.
nipkow
parents: 2031
diff changeset
    25
2af078382853 Modified some defs and shortened proofs.
nipkow
parents: 2031
diff changeset
    26
(* Equivalence of two definitions of `sorted' *)
2af078382853 Modified some defs and shortened proofs.
nipkow
parents: 2031
diff changeset
    27
8415
paulson
parents: 5184
diff changeset
    28
Goal "transf(le) ==> sorted1 le xs = sorted le xs";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5069
diff changeset
    29
by (induct_tac "xs" 1);
8415
paulson
parents: 5184
diff changeset
    30
by (ALLGOALS (asm_simp_tac (simpset() addsplits [list.split])));
paulson
parents: 5184
diff changeset
    31
by (rewrite_goals_tac [transf_def]);
paulson
parents: 5184
diff changeset
    32
by (Blast_tac 1);
2517
2af078382853 Modified some defs and shortened proofs.
nipkow
parents: 2031
diff changeset
    33
qed "sorted1_is_sorted";
8415
paulson
parents: 5184
diff changeset
    34
paulson
parents: 5184
diff changeset
    35
Goal "sorted le (xs@ys) = (sorted le xs & sorted le ys & \
paulson
parents: 5184
diff changeset
    36
\                         (ALL x:set xs. ALL y:set ys. le x y))";
paulson
parents: 5184
diff changeset
    37
by (induct_tac "xs" 1);
paulson
parents: 5184
diff changeset
    38
by Auto_tac;
paulson
parents: 5184
diff changeset
    39
qed "sorted_append";
paulson
parents: 5184
diff changeset
    40
Addsimps [sorted_append];
paulson
parents: 5184
diff changeset
    41