src/HOL/ex/Recdefs.ML

author | nipkow |

Wed, 30 Aug 2000 10:21:19 +0200 | |

changeset 9736 | 332fab43628f |

parent 8683 | 9d3e8c4a0287 |

child 9747 | 043098ba5098 |

permissions | -rw-r--r-- |

Fixed rulify.
As a result ?-vars in some recdef induction schemas were renamed.

(* 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 (res_inst_tac [("x","x")] g.induct 1); by Auto_tac; qed "g_terminates"; Goal "g x = 0"; by (res_inst_tac [("x","x")] g.induct 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;