# HG changeset patch
# User paulson
# Date 865585126 -7200
# Node ID 58ccb80eb50aa58232f95c07922304fd059073d2
# Parent  6d9e0cca6083828ddadbf03ba636998ea17aec60
New example theory: Recdef

diff -r 6d9e0cca6083 -r 58ccb80eb50a src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Jun 05 19:44:13 1997 +0200
+++ b/src/HOL/IsaMakefile	Fri Jun 06 10:18:46 1997 +0200
@@ -200,7 +200,7 @@
 
 ## Miscellaneous examples
 
-EX_NAMES = Fib Primes Primrec NatSum String BT InSort Qsort Puzzle MT
+EX_NAMES = Recdef Fib Primes Primrec NatSum String BT InSort Qsort Puzzle MT
 
 EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
 	   ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
diff -r 6d9e0cca6083 -r 58ccb80eb50a src/HOL/ex/Recdef.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Recdef.ML	Fri Jun 06 10:18:46 1997 +0200
@@ -0,0 +1,35 @@
+(*  Title:      HOL/ex/Recdef.ML
+    ID:         $Id$
+    Author:     Konrad Lawrence C Paulson
+    Copyright   1997  University of Cambridge
+
+A few proofs to demonstrate the functions defined in Recdef.thy
+Lemma statements from Konrad Slind's Web site
+*)
+
+open Recdef;
+
+Addsimps qsort.rules;
+
+goal thy "(x mem qsort (ord,l)) = (x mem l)";
+by (res_inst_tac [("u","ord"),("v","l")] qsort.induct 1);
+by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac[expand_if])));
+by (Blast_tac 1);
+qed "qsort_mem_stable";
+
+
+(** The silly g function: example of nested recursion **)
+
+Addsimps g.rules;
+
+goal thy "g x < Suc x";
+by (res_inst_tac [("u","x")] g.induct 1);
+by (Auto_tac());
+by (trans_tac 1);
+qed "g_terminates";
+
+goal thy "g x = 0";
+by (res_inst_tac [("u","x")] g.induct 1);
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [g_terminates])));
+qed "g_zero";
+