author | krauss |
Wed, 13 Sep 2006 12:05:50 +0200 | |
changeset 20523 | 36a59e5d0039 |
parent 20324 | 71d63a30cc96 |
child 20536 | f088edff8af8 |
permissions | -rw-r--r-- |
20324 | 1 |
(* Title: HOL/FunDef.thy |
2 |
ID: $Id$ |
|
3 |
Author: Alexander Krauss, TU Muenchen |
|
4 |
||
5 |
A package for general recursive function definitions. |
|
6 |
*) |
|
7 |
||
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
8 |
theory FunDef |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
9 |
imports Accessible_Part Datatype Recdef |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
10 |
uses |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
11 |
("Tools/function_package/sum_tools.ML") |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
12 |
("Tools/function_package/fundef_common.ML") |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
13 |
("Tools/function_package/fundef_lib.ML") |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20324
diff
changeset
|
14 |
("Tools/function_package/inductive_wrap.ML") |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
15 |
("Tools/function_package/context_tree.ML") |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
16 |
("Tools/function_package/fundef_prep.ML") |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
17 |
("Tools/function_package/fundef_proof.ML") |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
18 |
("Tools/function_package/termination.ML") |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
19 |
("Tools/function_package/mutual.ML") |
20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19934
diff
changeset
|
20 |
("Tools/function_package/pattern_split.ML") |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
21 |
("Tools/function_package/fundef_package.ML") |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
22 |
("Tools/function_package/fundef_datatype.ML") |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
23 |
("Tools/function_package/auto_term.ML") |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
24 |
begin |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
25 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
26 |
lemma fundef_ex1_existence: |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20324
diff
changeset
|
27 |
assumes f_def: "f \<equiv> \<lambda>x. THE y. (x,y)\<in>G" |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
28 |
assumes ex1: "\<exists>!y. (x,y)\<in>G" |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
29 |
shows "(x, f x)\<in>G" |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
30 |
by (simp only:f_def, rule theI', rule ex1) |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
31 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
32 |
lemma fundef_ex1_uniqueness: |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20324
diff
changeset
|
33 |
assumes f_def: "f \<equiv> \<lambda>x. THE y. (x,y)\<in>G" |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
34 |
assumes ex1: "\<exists>!y. (x,y)\<in>G" |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
35 |
assumes elm: "(x, h x)\<in>G" |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
36 |
shows "h x = f x" |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
37 |
by (simp only:f_def, rule the1_equality[symmetric], rule ex1, rule elm) |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
38 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
39 |
lemma fundef_ex1_iff: |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20324
diff
changeset
|
40 |
assumes f_def: "f \<equiv> \<lambda>x. THE y. (x,y)\<in>G" |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
41 |
assumes ex1: "\<exists>!y. (x,y)\<in>G" |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
42 |
shows "((x, y)\<in>G) = (f x = y)" |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
43 |
apply (auto simp:ex1 f_def the1_equality) |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
44 |
by (rule theI', rule ex1) |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
45 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
46 |
|
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
47 |
subsection {* Projections *} |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
48 |
consts |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
49 |
lpg::"(('a + 'b) * 'a) set" |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
50 |
rpg::"(('a + 'b) * 'b) set" |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
51 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
52 |
inductive lpg |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
53 |
intros |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
54 |
"(Inl x, x) : lpg" |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
55 |
inductive rpg |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
56 |
intros |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
57 |
"(Inr y, y) : rpg" |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
58 |
definition |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
59 |
"lproj x = (THE y. (x,y) : lpg)" |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
60 |
"rproj x = (THE y. (x,y) : rpg)" |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
61 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
62 |
lemma lproj_inl: |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
63 |
"lproj (Inl x) = x" |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
64 |
by (auto simp:lproj_def intro: the_equality lpg.intros elim: lpg.cases) |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
65 |
lemma rproj_inr: |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
66 |
"rproj (Inr x) = x" |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
67 |
by (auto simp:rproj_def intro: the_equality rpg.intros elim: rpg.cases) |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
68 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
69 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
70 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
71 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
72 |
use "Tools/function_package/sum_tools.ML" |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
73 |
use "Tools/function_package/fundef_common.ML" |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
74 |
use "Tools/function_package/fundef_lib.ML" |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20324
diff
changeset
|
75 |
use "Tools/function_package/inductive_wrap.ML" |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
76 |
use "Tools/function_package/context_tree.ML" |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
77 |
use "Tools/function_package/fundef_prep.ML" |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
78 |
use "Tools/function_package/fundef_proof.ML" |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
79 |
use "Tools/function_package/termination.ML" |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
80 |
use "Tools/function_package/mutual.ML" |
20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19934
diff
changeset
|
81 |
use "Tools/function_package/pattern_split.ML" |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
82 |
use "Tools/function_package/fundef_package.ML" |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
83 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
84 |
setup FundefPackage.setup |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
85 |
|
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
86 |
use "Tools/function_package/fundef_datatype.ML" |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
87 |
setup FundefDatatype.setup |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
88 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
89 |
use "Tools/function_package/auto_term.ML" |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
90 |
setup FundefAutoTerm.setup |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
91 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
92 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
93 |
lemmas [fundef_cong] = |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
94 |
let_cong if_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
95 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
96 |
|
19934 | 97 |
lemma split_cong[fundef_cong]: |
98 |
"\<lbrakk> \<And>x y. (x, y) = q \<Longrightarrow> f x y = g x y; p = q \<rbrakk> |
|
99 |
\<Longrightarrow> split f p = split g q" |
|
100 |
by (auto simp:split_def) |
|
101 |
||
102 |
||
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
103 |
end |