src/HOL/ex/Sorting.ML
author paulson
Wed Nov 05 13:23:46 1997 +0100 (1997-11-05)
changeset 4153 e534c4c32d54
parent 4089 96fba19bcbe2
child 4686 74a12e86b20b
permissions -rw-r--r--
Ran expandshort, especially to introduce Safe_tac
clasohm@1465
     1
(*  Title:      HOL/ex/sorting.ML
clasohm@969
     2
    ID:         $Id$
clasohm@1465
     3
    Author:     Tobias Nipkow
clasohm@969
     4
    Copyright   1994 TU Muenchen
clasohm@969
     5
clasohm@969
     6
Some general lemmas
clasohm@969
     7
*)
clasohm@969
     8
wenzelm@3842
     9
goal Sorting.thy "!x. mset (xs@ys) x = mset xs x + mset ys x";
paulson@2031
    10
by (list.induct_tac "xs" 1);
wenzelm@4089
    11
by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
nipkow@2517
    12
qed "mset_append";
clasohm@969
    13
wenzelm@3842
    14
goal Sorting.thy "!x. mset [x:xs. ~p(x)] x + mset [x:xs. p(x)] x = \
clasohm@969
    15
\                     mset xs x";
paulson@2031
    16
by (list.induct_tac "xs" 1);
wenzelm@4089
    17
by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
clasohm@969
    18
qed "mset_compl_add";
clasohm@969
    19
nipkow@2517
    20
Addsimps [mset_append, mset_compl_add];
nipkow@2517
    21
wenzelm@3842
    22
goal Sorting.thy "set xs = {x. mset xs x ~= 0}";
nipkow@2517
    23
by (list.induct_tac "xs" 1);
wenzelm@4089
    24
by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
nipkow@2517
    25
by (Fast_tac 1);
paulson@3647
    26
qed "set_via_mset";
nipkow@2517
    27
nipkow@2517
    28
(* Equivalence of two definitions of `sorted' *)
nipkow@2517
    29
nipkow@2517
    30
val prems = goalw Sorting.thy [transf_def]
nipkow@2517
    31
  "transf(le) ==> sorted1 le xs = sorted le xs";
nipkow@2517
    32
by (list.induct_tac "xs" 1);
wenzelm@4089
    33
by (ALLGOALS(asm_simp_tac (simpset() addsplits [split_list_case])));
nipkow@2517
    34
by (cut_facts_tac prems 1);
nipkow@2517
    35
by (Fast_tac 1);
nipkow@2517
    36
qed "sorted1_is_sorted";