Mercurial Mercurial > repos > Old_HOL / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ex/Sorting.ML
author nipkow
Fri, 02 Dec 1994 16:09:49 +0100
changeset 195 df6b3bd14dcb
parent 171 16c4ea954511
permissions -rw-r--r--
Moved HOL/List to HOL/ex/SList (strict list). Modified sons on (S)List accordingly.

(*  Title: 	HOL/ex/sorting.ML
    ID:         $Id$
    Author: 	Tobias Nipkow
    Copyright   1994 TU Muenchen

Some general lemmas
*)

val sorting_ss = list_ss addsimps
      [Sorting.mset_Nil,Sorting.mset_Cons,
       Sorting.sorted_Nil,Sorting.sorted_Cons,
       Sorting.sorted1_Nil,Sorting.sorted1_One,Sorting.sorted1_Cons];

goal Sorting.thy "!x.mset(xs@ys,x) = mset(xs,x)+mset(ys,x)";
by(list.induct_tac "xs" 1);
by(ALLGOALS(asm_simp_tac (sorting_ss setloop (split_tac [expand_if]))));
qed "mset_app_distr";

goal Sorting.thy "!x. mset([x:xs. ~p(x)], x) + mset([x:xs.p(x)], x) = \
\                     mset(xs, x)";
by(list.induct_tac "xs" 1);
by(ALLGOALS(asm_simp_tac (sorting_ss setloop (split_tac [expand_if]))));
qed "mset_compl_add";

val sorting_ss = sorting_ss addsimps
      [mset_app_distr, mset_compl_add];
Old_HOL