summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/ex/Recdefs.ML

author | nipkow |

Wed, 30 Aug 2000 16:29:21 +0200 | |

changeset 9747 | 043098ba5098 |

parent 9736 | 332fab43628f |

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

introduced induct_thm_tac

(* 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;