equal
deleted
inserted
replaced
1 (* Title: HOL/ex/Recdef.ML |
|
2 ID: $Id$ |
|
3 Author: Konrad Lawrence C Paulson |
|
4 Copyright 1997 University of Cambridge |
|
5 |
|
6 A few proofs to demonstrate the functions defined in Recdef.thy |
|
7 Lemma statements from Konrad Slind's Web site |
|
8 *) |
|
9 |
|
10 open Recdef; |
|
11 |
|
12 Addsimps qsort.rules; |
|
13 |
|
14 Goal "(x mem qsort (ord,l)) = (x mem l)"; |
|
15 by (res_inst_tac [("u","ord"),("v","l")] qsort.induct 1); |
|
16 by (ALLGOALS Asm_simp_tac); |
|
17 by (Blast_tac 1); |
|
18 qed "qsort_mem_stable"; |
|
19 |
|
20 |
|
21 (** The silly g function: example of nested recursion **) |
|
22 |
|
23 Addsimps g.rules; |
|
24 |
|
25 Goal "g x < Suc x"; |
|
26 by (res_inst_tac [("u","x")] g.induct 1); |
|
27 by Auto_tac; |
|
28 by (trans_tac 1); |
|
29 qed "g_terminates"; |
|
30 |
|
31 Goal "g x = 0"; |
|
32 by (res_inst_tac [("u","x")] g.induct 1); |
|
33 by (ALLGOALS (asm_simp_tac (simpset() addsimps [g_terminates]))); |
|
34 qed "g_zero"; |
|
35 |
|
36 (*** the contrived `mapf' ***) |
|
37 |
|
38 (* proving the termination condition: *) |
|
39 val [tc] = mapf.tcs; |
|
40 goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop tc)); |
|
41 by (rtac allI 1); |
|
42 by (case_tac "n=0" 1); |
|
43 by (ALLGOALS Asm_simp_tac); |
|
44 val lemma = result(); |
|
45 |
|
46 (* removing the termination condition from the generated thms: *) |
|
47 val [mapf_0,mapf_Suc] = mapf.rules; |
|
48 val mapf_Suc = lemma RS mapf_Suc; |
|
49 |
|
50 val mapf_induct = lemma RS mapf.induct; |
|