src/HOL/ex/Recdef.ML
author paulson
Wed Dec 24 10:02:30 1997 +0100 (1997-12-24 ago)
changeset 4477 b3e5857d8d99
parent 4423 a129b817b58a
child 4686 74a12e86b20b
permissions -rw-r--r--
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson@3417
     1
(*  Title:      HOL/ex/Recdef.ML
paulson@3417
     2
    ID:         $Id$
paulson@3417
     3
    Author:     Konrad Lawrence C Paulson
paulson@3417
     4
    Copyright   1997  University of Cambridge
paulson@3417
     5
paulson@3417
     6
A few proofs to demonstrate the functions defined in Recdef.thy
paulson@3417
     7
Lemma statements from Konrad Slind's Web site
paulson@3417
     8
*)
paulson@3417
     9
paulson@3417
    10
open Recdef;
paulson@3417
    11
paulson@3417
    12
Addsimps qsort.rules;
paulson@3417
    13
paulson@3417
    14
goal thy "(x mem qsort (ord,l)) = (x mem l)";
paulson@3417
    15
by (res_inst_tac [("u","ord"),("v","l")] qsort.induct 1);
wenzelm@4089
    16
by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
paulson@3417
    17
by (Blast_tac 1);
paulson@3417
    18
qed "qsort_mem_stable";
paulson@3417
    19
paulson@3417
    20
paulson@3417
    21
(** The silly g function: example of nested recursion **)
paulson@3417
    22
paulson@3417
    23
Addsimps g.rules;
paulson@3417
    24
paulson@3417
    25
goal thy "g x < Suc x";
paulson@3417
    26
by (res_inst_tac [("u","x")] g.induct 1);
paulson@4477
    27
by Auto_tac;
paulson@3417
    28
by (trans_tac 1);
paulson@3417
    29
qed "g_terminates";
paulson@3417
    30
paulson@3417
    31
goal thy "g x = 0";
paulson@3417
    32
by (res_inst_tac [("u","x")] g.induct 1);
wenzelm@4089
    33
by (ALLGOALS (asm_simp_tac (simpset() addsimps [g_terminates])));
paulson@3417
    34
qed "g_zero";
paulson@3417
    35
nipkow@3590
    36
(*** the contrived `mapf' ***)
nipkow@3590
    37
nipkow@3590
    38
(* proving the termination condition: *)
nipkow@3590
    39
val [tc] = mapf.tcs;
nipkow@3590
    40
goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop tc));
wenzelm@4423
    41
by (rtac allI 1);
wenzelm@4423
    42
by (case_tac "n=0" 1);
wenzelm@4423
    43
by (ALLGOALS Asm_simp_tac);
nipkow@3590
    44
val lemma = result();
nipkow@3590
    45
nipkow@3590
    46
(* removing the termination condition from the generated thms: *)
nipkow@3590
    47
val [mapf_0,mapf_Suc] = mapf.rules;
nipkow@3590
    48
val mapf_Suc = lemma RS mapf_Suc;
nipkow@3590
    49
nipkow@3590
    50
val mapf_induct = lemma RS mapf.induct;