author | haftmann |
Fri, 16 Mar 2007 21:32:10 +0100 | |
changeset 22454 | c3654ba76a09 |
parent 22325 | be61bd159a99 |
child 22622 | 25693088396b |
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") |
22166 | 16 |
("Tools/function_package/fundef_core.ML") |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
17 |
("Tools/function_package/mutual.ML") |
20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19934
diff
changeset
|
18 |
("Tools/function_package/pattern_split.ML") |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
19 |
("Tools/function_package/fundef_package.ML") |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
20 |
("Tools/function_package/auto_term.ML") |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
21 |
begin |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
22 |
|
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
23 |
section {* Definitions with default value *} |
20536
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
24 |
|
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
25 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21364
diff
changeset
|
26 |
THE_default :: "'a \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a" where |
20536
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
27 |
"THE_default d P = (if (\<exists>!x. P x) then (THE x. P x) else d)" |
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
28 |
|
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
29 |
lemma THE_defaultI': "\<exists>!x. P x \<Longrightarrow> P (THE_default d P)" |
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
30 |
by (simp add:theI' THE_default_def) |
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
31 |
|
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
32 |
lemma THE_default1_equality: |
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
33 |
"\<lbrakk>\<exists>!x. P x; P a\<rbrakk> \<Longrightarrow> THE_default d P = a" |
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
34 |
by (simp add:the1_equality THE_default_def) |
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
35 |
|
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
36 |
lemma THE_default_none: |
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
37 |
"\<not>(\<exists>!x. P x) \<Longrightarrow> THE_default d P = d" |
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
38 |
by (simp add:THE_default_def) |
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
39 |
|
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
40 |
|
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
41 |
lemma fundef_ex1_existence: |
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
42 |
assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))" |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
43 |
assumes ex1: "\<exists>!y. G x y" |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
44 |
shows "G x (f x)" |
20536
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
45 |
by (simp only:f_def, rule THE_defaultI', rule ex1) |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
46 |
|
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
47 |
|
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
48 |
|
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
49 |
|
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
50 |
|
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
51 |
lemma fundef_ex1_uniqueness: |
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
52 |
assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))" |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
53 |
assumes ex1: "\<exists>!y. G x y" |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
54 |
assumes elm: "G x (h x)" |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
55 |
shows "h x = f x" |
20536
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
56 |
by (simp only:f_def, rule THE_default1_equality[symmetric], rule ex1, rule elm) |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
57 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
58 |
lemma fundef_ex1_iff: |
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
59 |
assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))" |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
60 |
assumes ex1: "\<exists>!y. G x y" |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
61 |
shows "(G x y) = (f x = y)" |
20536
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
62 |
apply (auto simp:ex1 f_def THE_default1_equality) |
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
63 |
by (rule THE_defaultI', rule ex1) |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
64 |
|
20654
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset
|
65 |
lemma fundef_default_value: |
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
66 |
assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))" |
21512
3786eb1b69d6
Lemma "fundef_default_value" uses predicate instead of set.
krauss
parents:
21404
diff
changeset
|
67 |
assumes graph: "\<And>x y. G x y \<Longrightarrow> D x" |
3786eb1b69d6
Lemma "fundef_default_value" uses predicate instead of set.
krauss
parents:
21404
diff
changeset
|
68 |
assumes "\<not> D x" |
20654
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset
|
69 |
shows "f x = d x" |
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset
|
70 |
proof - |
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
71 |
have "\<not>(\<exists>y. G x y)" |
20654
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset
|
72 |
proof |
21512
3786eb1b69d6
Lemma "fundef_default_value" uses predicate instead of set.
krauss
parents:
21404
diff
changeset
|
73 |
assume "\<exists>y. G x y" |
3786eb1b69d6
Lemma "fundef_default_value" uses predicate instead of set.
krauss
parents:
21404
diff
changeset
|
74 |
hence "D x" using graph .. |
3786eb1b69d6
Lemma "fundef_default_value" uses predicate instead of set.
krauss
parents:
21404
diff
changeset
|
75 |
with `\<not> D x` show False .. |
20654
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset
|
76 |
qed |
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
77 |
hence "\<not>(\<exists>!y. G x y)" by blast |
20654
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset
|
78 |
|
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset
|
79 |
thus ?thesis |
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset
|
80 |
unfolding f_def |
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset
|
81 |
by (rule THE_default_none) |
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset
|
82 |
qed |
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset
|
83 |
|
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset
|
84 |
|
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset
|
85 |
|
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
86 |
section {* Projections *} |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
87 |
|
22268
ee2619267dca
- wfP has been moved to theory Wellfounded_Recursion
berghofe
parents:
22166
diff
changeset
|
88 |
inductive2 lpg :: "('a + 'b) \<Rightarrow> 'a \<Rightarrow> bool" |
ee2619267dca
- wfP has been moved to theory Wellfounded_Recursion
berghofe
parents:
22166
diff
changeset
|
89 |
where |
ee2619267dca
- wfP has been moved to theory Wellfounded_Recursion
berghofe
parents:
22166
diff
changeset
|
90 |
"lpg (Inl x) x" |
ee2619267dca
- wfP has been moved to theory Wellfounded_Recursion
berghofe
parents:
22166
diff
changeset
|
91 |
inductive2 rpg :: "('a + 'b) \<Rightarrow> 'b \<Rightarrow> bool" |
ee2619267dca
- wfP has been moved to theory Wellfounded_Recursion
berghofe
parents:
22166
diff
changeset
|
92 |
where |
ee2619267dca
- wfP has been moved to theory Wellfounded_Recursion
berghofe
parents:
22166
diff
changeset
|
93 |
"rpg (Inr y) y" |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21364
diff
changeset
|
94 |
|
22268
ee2619267dca
- wfP has been moved to theory Wellfounded_Recursion
berghofe
parents:
22166
diff
changeset
|
95 |
definition "lproj x = (THE y. lpg x y)" |
ee2619267dca
- wfP has been moved to theory Wellfounded_Recursion
berghofe
parents:
22166
diff
changeset
|
96 |
definition "rproj x = (THE y. rpg x y)" |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
97 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
98 |
lemma lproj_inl: |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
99 |
"lproj (Inl x) = x" |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
100 |
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
|
101 |
lemma rproj_inr: |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
102 |
"rproj (Inr x) = x" |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
103 |
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
|
104 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
105 |
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
|
106 |
use "Tools/function_package/fundef_common.ML" |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
107 |
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
|
108 |
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
|
109 |
use "Tools/function_package/context_tree.ML" |
22166 | 110 |
use "Tools/function_package/fundef_core.ML" |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
111 |
use "Tools/function_package/mutual.ML" |
20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19934
diff
changeset
|
112 |
use "Tools/function_package/pattern_split.ML" |
21319
cf814e36f788
replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents:
21312
diff
changeset
|
113 |
use "Tools/function_package/auto_term.ML" |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
114 |
use "Tools/function_package/fundef_package.ML" |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
115 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
116 |
setup FundefPackage.setup |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
117 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
118 |
lemmas [fundef_cong] = |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
119 |
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
|
120 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
121 |
|
19934 | 122 |
lemma split_cong[fundef_cong]: |
123 |
"\<lbrakk> \<And>x y. (x, y) = q \<Longrightarrow> f x y = g x y; p = q \<rbrakk> |
|
124 |
\<Longrightarrow> split f p = split g q" |
|
125 |
by (auto simp:split_def) |
|
126 |
||
22324 | 127 |
lemma comp_cong[fundef_cong]: |
128 |
"f (g x) = f' (g' x') |
|
129 |
==> (f o g) x = (f' o g') x'" |
|
130 |
unfolding o_apply . |
|
19934 | 131 |
|
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
132 |
end |