# HG changeset patch
# User nipkow
# Date 870790937 -7200
# Node ID 4d307341d0af6f6332040ebbc24cbdef58b45158
# Parent  244daa75f8903cb3f3ab9426273d7913ab34f46c
Added example mapf which requires a special congruence rule.

diff -r 244daa75f890 -r 4d307341d0af src/HOL/ex/Recdef.ML
--- a/src/HOL/ex/Recdef.ML	Tue Aug 05 16:21:45 1997 +0200
+++ b/src/HOL/ex/Recdef.ML	Tue Aug 05 16:22:17 1997 +0200
@@ -33,3 +33,18 @@
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [g_terminates])));
 qed "g_zero";
 
+(*** the contrived `mapf' ***)
+
+(* proving the termination condition: *)
+val [tc] = mapf.tcs;
+goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop tc));
+br allI 1;
+by(case_tac "n=0" 1);
+by(ALLGOALS Asm_simp_tac);
+val lemma = result();
+
+(* removing the termination condition from the generated thms: *)
+val [mapf_0,mapf_Suc] = mapf.rules;
+val mapf_Suc = lemma RS mapf_Suc;
+
+val mapf_induct = lemma RS mapf.induct;
diff -r 244daa75f890 -r 4d307341d0af src/HOL/ex/Recdef.thy
--- a/src/HOL/ex/Recdef.thy	Tue Aug 05 16:21:45 1997 +0200
+++ b/src/HOL/ex/Recdef.thy	Tue Aug 05 16:22:17 1997 +0200
@@ -87,4 +87,16 @@
       in  
       fqsort(ord,less)@[x]@fqsort(ord,more))"
 
+(* silly example which demonstrates the occasional need for additional
+   congruence rules (here: map_cong from List). If the congruence rule is
+   removed, an unprovable termination condition is generated!
+   Termination not proved automatically; see the ML file.
+   TFL requires (%x.mapf x) instead of mapf.
+*)
+consts mapf :: nat => nat list
+recdef mapf "measure(%m.m)"
+congs "[map_cong]"
+"mapf 0 = []"
+"mapf (Suc n) = concat(map (%x.mapf x) (replicate n n))"
+
 end