ex/sorting.ML
author clasohm
Wed, 02 Mar 1994 12:26:55 +0100
changeset 48 21291189b51e
parent 46 a73f8a7784bd
permissions -rw-r--r--
changed "." to "$" and Cons to infix "#" to eliminate ambiguity
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
46
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
     1
(*  Title: 	HOL/ex/sorting.ML
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
     2
    ID:         $Id$
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
     3
    Author: 	Tobias Nipkow
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
     4
    Copyright   1994 TU Muenchen
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
     5
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
     6
Some general lemmas
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
     7
*)
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
     8
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
     9
val sorting_ss = list_ss addsimps
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
    10
      [Sorting.mset_Nil,Sorting.mset_Cons,
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
    11
       Sorting.sorted_Nil,Sorting.sorted_Cons,
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
    12
       Sorting.sorted1_Nil,Sorting.sorted1_One,Sorting.sorted1_Cons];
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
    13
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
    14
goal Sorting.thy "!x.mset(xs@ys,x) = mset(xs,x)+mset(ys,x)";
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
    15
by(list_ind_tac "xs" 1);
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
    16
by(ALLGOALS(asm_simp_tac (sorting_ss setloop (split_tac [expand_if]))));
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
    17
val mset_app_distr = result();
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
    18
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
    19
goal Sorting.thy "!x. mset([x:xs. ~p(x)], x) + mset([x:xs.p(x)], x) = \
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
    20
\                     mset(xs, x)";
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
    21
by(list_ind_tac "xs" 1);
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
    22
by(ALLGOALS(asm_simp_tac (sorting_ss setloop (split_tac [expand_if]))));
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
    23
val mset_compl_add = result();
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
    24
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
    25
val sorting_ss = sorting_ss addsimps
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
    26
      [mset_app_distr, mset_compl_add];