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
     1 (*  Title:      HOL/ex/insort.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1994 TU Muenchen
     5 
     6 Correctness proof of insertion sort.
     7 *)
     8 
     9 goal thy "!y. mset(ins f x xs) y = mset (x#xs) y";
    10 by (list.induct_tac "xs" 1);
    11 by (Asm_simp_tac 1);
    12 by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
    13 qed "mset_ins";
    14 Addsimps [mset_ins];
    15 
    16 goal thy "!x. mset(insort f xs) x = mset xs x";
    17 by (list.induct_tac "xs" 1);
    18 by (ALLGOALS Asm_simp_tac);
    19 qed "insort_permutes";
    20 
    21 goal thy "set(ins f x xs) = insert x (set xs)";
    22 by (asm_simp_tac (simpset() addsimps [set_via_mset]
    23                            addsplits [expand_if]) 1);
    24 by (Fast_tac 1);
    25 qed "set_ins";
    26 Addsimps [set_ins];
    27 
    28 val prems = goalw InSort.thy [total_def,transf_def]
    29   "[| total(f); transf(f) |] ==>  sorted f (ins f x xs) = sorted f xs";
    30 by (list.induct_tac "xs" 1);
    31 by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
    32 by (cut_facts_tac prems 1);
    33 by (Fast_tac 1);
    34 qed "sorted_ins";
    35 Addsimps [sorted_ins];
    36 
    37 goal InSort.thy "!!f. [| total(f); transf(f) |] ==>  sorted f (insort f xs)";
    38 by (list.induct_tac "xs" 1);
    39 by (ALLGOALS Asm_simp_tac);
    40 qed "sorted_insort";