paulson@3417: (* Title: HOL/ex/Recdef.ML paulson@3417: ID: $Id$ paulson@3417: Author: Konrad Lawrence C Paulson paulson@3417: Copyright 1997 University of Cambridge paulson@3417: paulson@3417: A few proofs to demonstrate the functions defined in Recdef.thy paulson@3417: Lemma statements from Konrad Slind's Web site paulson@3417: *) paulson@3417: paulson@3417: open Recdef; paulson@3417: paulson@3417: Addsimps qsort.rules; paulson@3417: paulson@3417: goal thy "(x mem qsort (ord,l)) = (x mem l)"; paulson@3417: by (res_inst_tac [("u","ord"),("v","l")] qsort.induct 1); wenzelm@4089: by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if]))); paulson@3417: by (Blast_tac 1); paulson@3417: qed "qsort_mem_stable"; paulson@3417: paulson@3417: paulson@3417: (** The silly g function: example of nested recursion **) paulson@3417: paulson@3417: Addsimps g.rules; paulson@3417: paulson@3417: goal thy "g x < Suc x"; paulson@3417: by (res_inst_tac [("u","x")] g.induct 1); paulson@3417: by (Auto_tac()); paulson@3417: by (trans_tac 1); paulson@3417: qed "g_terminates"; paulson@3417: paulson@3417: goal thy "g x = 0"; paulson@3417: by (res_inst_tac [("u","x")] g.induct 1); wenzelm@4089: by (ALLGOALS (asm_simp_tac (simpset() addsimps [g_terminates]))); paulson@3417: qed "g_zero"; paulson@3417: nipkow@3590: (*** the contrived `mapf' ***) nipkow@3590: nipkow@3590: (* proving the termination condition: *) nipkow@3590: val [tc] = mapf.tcs; nipkow@3590: goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop tc)); nipkow@3590: br allI 1; nipkow@3590: by(case_tac "n=0" 1); nipkow@3590: by(ALLGOALS Asm_simp_tac); nipkow@3590: val lemma = result(); nipkow@3590: nipkow@3590: (* removing the termination condition from the generated thms: *) nipkow@3590: val [mapf_0,mapf_Suc] = mapf.rules; nipkow@3590: val mapf_Suc = lemma RS mapf_Suc; nipkow@3590: nipkow@3590: val mapf_induct = lemma RS mapf.induct;