New example theory: Recdef
authorpaulson
Fri Jun 06 10:18:46 1997 +0200 (1997-06-06)
changeset 341758ccb80eb50a
parent 3416 6d9e0cca6083
child 3418 f060dc3f15a8
New example theory: Recdef
src/HOL/IsaMakefile
src/HOL/ex/Recdef.ML
     1.1 --- a/src/HOL/IsaMakefile	Thu Jun 05 19:44:13 1997 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Jun 06 10:18:46 1997 +0200
     1.3 @@ -200,7 +200,7 @@
     1.4  
     1.5  ## Miscellaneous examples
     1.6  
     1.7 -EX_NAMES = Fib Primes Primrec NatSum String BT InSort Qsort Puzzle MT
     1.8 +EX_NAMES = Recdef Fib Primes Primrec NatSum String BT InSort Qsort Puzzle MT
     1.9  
    1.10  EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
    1.11  	   ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/ex/Recdef.ML	Fri Jun 06 10:18:46 1997 +0200
     2.3 @@ -0,0 +1,35 @@
     2.4 +(*  Title:      HOL/ex/Recdef.ML
     2.5 +    ID:         $Id$
     2.6 +    Author:     Konrad Lawrence C Paulson
     2.7 +    Copyright   1997  University of Cambridge
     2.8 +
     2.9 +A few proofs to demonstrate the functions defined in Recdef.thy
    2.10 +Lemma statements from Konrad Slind's Web site
    2.11 +*)
    2.12 +
    2.13 +open Recdef;
    2.14 +
    2.15 +Addsimps qsort.rules;
    2.16 +
    2.17 +goal thy "(x mem qsort (ord,l)) = (x mem l)";
    2.18 +by (res_inst_tac [("u","ord"),("v","l")] qsort.induct 1);
    2.19 +by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac[expand_if])));
    2.20 +by (Blast_tac 1);
    2.21 +qed "qsort_mem_stable";
    2.22 +
    2.23 +
    2.24 +(** The silly g function: example of nested recursion **)
    2.25 +
    2.26 +Addsimps g.rules;
    2.27 +
    2.28 +goal thy "g x < Suc x";
    2.29 +by (res_inst_tac [("u","x")] g.induct 1);
    2.30 +by (Auto_tac());
    2.31 +by (trans_tac 1);
    2.32 +qed "g_terminates";
    2.33 +
    2.34 +goal thy "g x = 0";
    2.35 +by (res_inst_tac [("u","x")] g.induct 1);
    2.36 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [g_terminates])));
    2.37 +qed "g_zero";
    2.38 +