src/HOL/ex/Recdef.ML
author paulson
Fri Jun 06 10:18:46 1997 +0200 (1997-06-06)
changeset 3417 58ccb80eb50a
child 3590 4d307341d0af
permissions -rw-r--r--
New example theory: Recdef
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);
paulson@3417
    16
by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac[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@3417
    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);
paulson@3417
    33
by (ALLGOALS (asm_simp_tac (!simpset addsimps [g_terminates])));
paulson@3417
    34
qed "g_zero";
paulson@3417
    35