author | wenzelm |
Mon, 03 Nov 1997 12:13:18 +0100 | |
changeset 4089 | 96fba19bcbe2 |
parent 3919 | c036caebfc75 |
child 4423 | a129b817b58a |
permissions | -rw-r--r-- |
3417 | 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 thy "(x mem qsort (ord,l)) = (x mem l)"; |
|
15 |
by (res_inst_tac [("u","ord"),("v","l")] qsort.induct 1); |
|
4089 | 16 |
by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if]))); |
3417 | 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 thy "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 thy "g x = 0"; |
|
32 |
by (res_inst_tac [("u","x")] g.induct 1); |
|
4089 | 33 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [g_terminates]))); |
3417 | 34 |
qed "g_zero"; |
35 |
||
3590
4d307341d0af
Added example mapf which requires a special congruence rule.
nipkow
parents:
3417
diff
changeset
|
36 |
(*** the contrived `mapf' ***) |
4d307341d0af
Added example mapf which requires a special congruence rule.
nipkow
parents:
3417
diff
changeset
|
37 |
|
4d307341d0af
Added example mapf which requires a special congruence rule.
nipkow
parents:
3417
diff
changeset
|
38 |
(* proving the termination condition: *) |
4d307341d0af
Added example mapf which requires a special congruence rule.
nipkow
parents:
3417
diff
changeset
|
39 |
val [tc] = mapf.tcs; |
4d307341d0af
Added example mapf which requires a special congruence rule.
nipkow
parents:
3417
diff
changeset
|
40 |
goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop tc)); |
4d307341d0af
Added example mapf which requires a special congruence rule.
nipkow
parents:
3417
diff
changeset
|
41 |
br allI 1; |
4d307341d0af
Added example mapf which requires a special congruence rule.
nipkow
parents:
3417
diff
changeset
|
42 |
by(case_tac "n=0" 1); |
4d307341d0af
Added example mapf which requires a special congruence rule.
nipkow
parents:
3417
diff
changeset
|
43 |
by(ALLGOALS Asm_simp_tac); |
4d307341d0af
Added example mapf which requires a special congruence rule.
nipkow
parents:
3417
diff
changeset
|
44 |
val lemma = result(); |
4d307341d0af
Added example mapf which requires a special congruence rule.
nipkow
parents:
3417
diff
changeset
|
45 |
|
4d307341d0af
Added example mapf which requires a special congruence rule.
nipkow
parents:
3417
diff
changeset
|
46 |
(* removing the termination condition from the generated thms: *) |
4d307341d0af
Added example mapf which requires a special congruence rule.
nipkow
parents:
3417
diff
changeset
|
47 |
val [mapf_0,mapf_Suc] = mapf.rules; |
4d307341d0af
Added example mapf which requires a special congruence rule.
nipkow
parents:
3417
diff
changeset
|
48 |
val mapf_Suc = lemma RS mapf_Suc; |
4d307341d0af
Added example mapf which requires a special congruence rule.
nipkow
parents:
3417
diff
changeset
|
49 |
|
4d307341d0af
Added example mapf which requires a special congruence rule.
nipkow
parents:
3417
diff
changeset
|
50 |
val mapf_induct = lemma RS mapf.induct; |