src/HOL/ex/InSort.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/insort.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
Correctness proof of insertion sort.
clasohm@969
     7
*)
clasohm@969
     8
nipkow@2517
     9
goal thy "!y. mset(ins f x xs) y = mset (x#xs) y";
paulson@2031
    10
by (list.induct_tac "xs" 1);
paulson@2031
    11
by (Asm_simp_tac 1);
wenzelm@4089
    12
by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
nipkow@2517
    13
qed "mset_ins";
nipkow@2517
    14
Addsimps [mset_ins];
nipkow@2517
    15
nipkow@2517
    16
goal thy "!x. mset(insort f xs) x = mset xs x";
nipkow@2517
    17
by (list.induct_tac "xs" 1);
nipkow@2517
    18
by (ALLGOALS Asm_simp_tac);
nipkow@2517
    19
qed "insort_permutes";
nipkow@2517
    20
nipkow@3465
    21
goal thy "set(ins f x xs) = insert x (set xs)";
wenzelm@4089
    22
by (asm_simp_tac (simpset() addsimps [set_via_mset]
nipkow@3919
    23
                           addsplits [expand_if]) 1);
paulson@2031
    24
by (Fast_tac 1);
paulson@3647
    25
qed "set_ins";
paulson@3647
    26
Addsimps [set_ins];
clasohm@969
    27
nipkow@2517
    28
val prems = goalw InSort.thy [total_def,transf_def]
clasohm@969
    29
  "[| total(f); transf(f) |] ==>  sorted f (ins f x xs) = sorted f xs";
paulson@2031
    30
by (list.induct_tac "xs" 1);
wenzelm@4089
    31
by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
paulson@2031
    32
by (cut_facts_tac prems 1);
nipkow@2517
    33
by (Fast_tac 1);
nipkow@2511
    34
qed "sorted_ins";
nipkow@2511
    35
Addsimps [sorted_ins];
clasohm@969
    36
clasohm@969
    37
goal InSort.thy "!!f. [| total(f); transf(f) |] ==>  sorted f (insort f xs)";
paulson@2031
    38
by (list.induct_tac "xs" 1);
paulson@2031
    39
by (ALLGOALS Asm_simp_tac);
berghofe@1750
    40
qed "sorted_insort";