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

src/HOL/ex/Recdefs.ML

author | wenzelm |

Sat, 08 Apr 2000 19:38:19 +0200 | |

changeset 8683 | 9d3e8c4a0287 |

parent 8624 | 69619f870939 |

child 9736 | 332fab43628f |

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

fixed comment;

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