(* Title: HOL/ex/Recdefs.ML
ID: $Id$
Author: Konrad Slind and Lawrence C Paulson
Copyright 1997 University of Cambridge
A few proofs to demonstrate the functions defined in Recdefs.thy
Lemma statements from Konrad Slind's Web site
*)
(** The silly g function: example of nested recursion **)
Addsimps g.simps;
Goal "g x < Suc x";
by (induct_thm_tac g.induct "x" 1);
by Auto_tac;
qed "g_terminates";
Goal "g x = 0";
by (induct_thm_tac g.induct "x" 1);
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));
by (rtac 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.simps;
val mapf_Suc = lemma RS mapf_Suc;
val mapf_induct = lemma RS mapf.induct;