src/HOL/ex/Recdefs.ML

author | wenzelm |

Fri, 03 Jul 1998 17:35:39 +0200 | |

changeset 5124 | 1ce3cccfacdb |

child 5518 | 654ead0ba4f7 |

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

stepping stones: Recdef, Main;
String now part of main HOL;

(* Title: HOL/ex/Recdefs.ML ID: $Id$ Author: Konrad 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 *) Addsimps qsort.rules; Goal "(x mem qsort (ord,l)) = (x mem l)"; by (res_inst_tac [("u","ord"),("v","l")] qsort.induct 1); by (ALLGOALS Asm_simp_tac); by (Blast_tac 1); qed "qsort_mem_stable"; (** The silly g function: example of nested recursion **) Addsimps g.rules; Goal "g x < Suc x"; by (res_inst_tac [("u","x")] g.induct 1); by Auto_tac; by (trans_tac 1); 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.rules; val mapf_Suc = lemma RS mapf_Suc; val mapf_induct = lemma RS mapf.induct;