author paulson Fri Jun 06 10:18:46 1997 +0200 (1997-06-06) changeset 3417 58ccb80eb50a parent 3416 6d9e0cca6083 child 3418 f060dc3f15a8
New example theory: Recdef
 src/HOL/IsaMakefile file | annotate | diff | revisions src/HOL/ex/Recdef.ML file | annotate | diff | revisions
```     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.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 +