author | wenzelm |
Wed, 08 Nov 2006 13:48:29 +0100 | |
changeset 21243 | afffe1f72143 |
parent 21211 | 5370cfbf3070 |
child 21312 | 1d39091a3208 |
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 |
|
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
26 |
section {* Wellfoundedness and Accessibility: Predicate versions *} |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
27 |
|
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
28 |
|
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
29 |
constdefs |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
30 |
wfP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) => bool" |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
31 |
"wfP(r) == (!P. (!x. (!y. r y x --> P(y)) --> P(x)) --> (!x. P(x)))" |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
32 |
|
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
33 |
lemma wfP_induct: |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
34 |
"[| wfP r; |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
35 |
!!x.[| ALL y. r y x --> P(y) |] ==> P(x) |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
36 |
|] ==> P(a)" |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
37 |
by (unfold wfP_def, blast) |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
38 |
|
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
39 |
lemmas wfP_induct_rule = wfP_induct [rule_format, consumes 1, case_names less] |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
40 |
|
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
41 |
definition in_rel_def[simp]: |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
42 |
"in_rel R x y == (x, y) \<in> R" |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
43 |
|
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
44 |
lemma wf_in_rel: |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
45 |
"wf R \<Longrightarrow> wfP (in_rel R)" |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
46 |
unfolding wfP_def wf_def in_rel_def . |
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 |
inductive2 accP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
50 |
for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
51 |
intros |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
52 |
accPI: "(!!y. r y x ==> accP r y) ==> accP r x" |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
53 |
|
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
54 |
|
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
55 |
theorem accP_induct: |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
56 |
assumes major: "accP r a" |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
57 |
assumes hyp: "!!x. accP r x ==> \<forall>y. r y x --> P y ==> P x" |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
58 |
shows "P a" |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
59 |
apply (rule major [THEN accP.induct]) |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
60 |
apply (rule hyp) |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
61 |
apply (rule accPI) |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
62 |
apply fast |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
63 |
apply fast |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
64 |
done |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
65 |
|
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
66 |
theorems accP_induct_rule = accP_induct [rule_format, induct set: accP] |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
67 |
|
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
68 |
theorem accP_downward: "accP r b ==> r a b ==> accP r a" |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
69 |
apply (erule accP.cases) |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
70 |
apply fast |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
71 |
done |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
72 |
|
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
73 |
|
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
74 |
lemma accP_subset: |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
75 |
assumes sub: "\<And>x y. R1 x y \<Longrightarrow> R2 x y" |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
76 |
shows "\<And>x. accP R2 x \<Longrightarrow> accP R1 x" |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
77 |
proof- |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
78 |
fix x assume "accP R2 x" |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
79 |
then show "accP R1 x" |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
80 |
proof (induct x) |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
81 |
fix x |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
82 |
assume ih: "\<And>y. R2 y x \<Longrightarrow> accP R1 y" |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
83 |
with sub show "accP R1 x" |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
84 |
by (blast intro:accPI) |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
85 |
qed |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
86 |
qed |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
87 |
|
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
88 |
|
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
89 |
lemma accP_subset_induct: |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
90 |
assumes subset: "\<And>x. D x \<Longrightarrow> accP R x" |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
91 |
and dcl: "\<And>x z. \<lbrakk>D x; R z x\<rbrakk> \<Longrightarrow> D z" |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
92 |
and "D x" |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
93 |
and istep: "\<And>x. \<lbrakk>D x; (\<And>z. R z x \<Longrightarrow> P z)\<rbrakk> \<Longrightarrow> P x" |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
94 |
shows "P x" |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
95 |
proof - |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
96 |
from subset and `D x` |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
97 |
have "accP R x" . |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
98 |
then show "P x" using `D x` |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
99 |
proof (induct x) |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
100 |
fix x |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
101 |
assume "D x" |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
102 |
and "\<And>y. R y x \<Longrightarrow> D y \<Longrightarrow> P y" |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
103 |
with dcl and istep show "P x" by blast |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
104 |
qed |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
105 |
qed |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
106 |
|
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
107 |
|
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
108 |
section {* Definitions with default value *} |
20536
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
109 |
|
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
110 |
definition |
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
111 |
THE_default :: "'a \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a" |
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
112 |
"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
|
113 |
|
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
114 |
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
|
115 |
by (simp add:theI' THE_default_def) |
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
116 |
|
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
117 |
lemma THE_default1_equality: |
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
118 |
"\<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
|
119 |
by (simp add:the1_equality THE_default_def) |
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
120 |
|
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
121 |
lemma THE_default_none: |
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
122 |
"\<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
|
123 |
by (simp add:THE_default_def) |
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
124 |
|
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
125 |
|
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
126 |
lemma fundef_ex1_existence: |
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
127 |
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
|
128 |
assumes ex1: "\<exists>!y. G x y" |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
129 |
shows "G x (f x)" |
20536
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
130 |
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
|
131 |
|
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
132 |
|
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
133 |
|
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
134 |
|
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
135 |
|
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
136 |
lemma fundef_ex1_uniqueness: |
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
137 |
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
|
138 |
assumes ex1: "\<exists>!y. G x y" |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
139 |
assumes elm: "G x (h x)" |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
140 |
shows "h x = f x" |
20536
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
141 |
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
|
142 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
143 |
lemma fundef_ex1_iff: |
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
144 |
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
|
145 |
assumes ex1: "\<exists>!y. G x y" |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
146 |
shows "(G x y) = (f x = y)" |
20536
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
147 |
apply (auto simp:ex1 f_def THE_default1_equality) |
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
148 |
by (rule THE_defaultI', rule ex1) |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
149 |
|
20654
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset
|
150 |
lemma fundef_default_value: |
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
151 |
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
|
152 |
assumes graph: "\<And>x y. G x y \<Longrightarrow> x \<in> D" |
20654
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset
|
153 |
assumes "x \<notin> D" |
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset
|
154 |
shows "f x = d x" |
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset
|
155 |
proof - |
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
156 |
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
|
157 |
proof |
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
158 |
assume "(\<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
|
159 |
with graph and `x\<notin>D` show False by blast |
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset
|
160 |
qed |
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
161 |
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
|
162 |
|
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset
|
163 |
thus ?thesis |
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset
|
164 |
unfolding f_def |
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset
|
165 |
by (rule THE_default_none) |
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset
|
166 |
qed |
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset
|
167 |
|
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset
|
168 |
|
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset
|
169 |
|
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
170 |
section {* Projections *} |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
171 |
consts |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
172 |
lpg::"(('a + 'b) * 'a) set" |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
173 |
rpg::"(('a + 'b) * 'b) set" |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
174 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
175 |
inductive lpg |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
176 |
intros |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
177 |
"(Inl x, x) : lpg" |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
178 |
inductive rpg |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
179 |
intros |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
180 |
"(Inr y, y) : rpg" |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
181 |
definition |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
182 |
"lproj x = (THE y. (x,y) : lpg)" |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
183 |
"rproj x = (THE y. (x,y) : rpg)" |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
184 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
185 |
lemma lproj_inl: |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
186 |
"lproj (Inl x) = x" |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
187 |
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
|
188 |
lemma rproj_inr: |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
189 |
"rproj (Inr x) = x" |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
190 |
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
|
191 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
192 |
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
|
193 |
use "Tools/function_package/fundef_common.ML" |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
194 |
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
|
195 |
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
|
196 |
use "Tools/function_package/context_tree.ML" |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
197 |
use "Tools/function_package/fundef_prep.ML" |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
198 |
use "Tools/function_package/fundef_proof.ML" |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
199 |
use "Tools/function_package/termination.ML" |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
200 |
use "Tools/function_package/mutual.ML" |
20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19934
diff
changeset
|
201 |
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
|
202 |
use "Tools/function_package/fundef_package.ML" |
21211
5370cfbf3070
Preparations for making "lexicographic_order" part of "fun"
krauss
parents:
21051
diff
changeset
|
203 |
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
|
204 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
205 |
setup FundefPackage.setup |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
206 |
setup FundefAutoTerm.setup |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
207 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
208 |
lemmas [fundef_cong] = |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
209 |
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
|
210 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
211 |
|
19934 | 212 |
lemma split_cong[fundef_cong]: |
213 |
"\<lbrakk> \<And>x y. (x, y) = q \<Longrightarrow> f x y = g x y; p = q \<rbrakk> |
|
214 |
\<Longrightarrow> split f p = split g q" |
|
215 |
by (auto simp:split_def) |
|
216 |
||
217 |
||
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
218 |
end |