21 ("Tools/function_package/fundef_package.ML") |
21 ("Tools/function_package/fundef_package.ML") |
22 ("Tools/function_package/fundef_datatype.ML") |
22 ("Tools/function_package/fundef_datatype.ML") |
23 ("Tools/function_package/auto_term.ML") |
23 ("Tools/function_package/auto_term.ML") |
24 begin |
24 begin |
25 |
25 |
|
26 section {* Wellfoundedness and Accessibility: Predicate versions *} |
|
27 |
|
28 |
|
29 constdefs |
|
30 wfP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) => bool" |
|
31 "wfP(r) == (!P. (!x. (!y. r y x --> P(y)) --> P(x)) --> (!x. P(x)))" |
|
32 |
|
33 lemma wfP_induct: |
|
34 "[| wfP r; |
|
35 !!x.[| ALL y. r y x --> P(y) |] ==> P(x) |
|
36 |] ==> P(a)" |
|
37 by (unfold wfP_def, blast) |
|
38 |
|
39 lemmas wfP_induct_rule = wfP_induct [rule_format, consumes 1, case_names less] |
|
40 |
|
41 definition in_rel_def[simp]: |
|
42 "in_rel R x y == (x, y) \<in> R" |
|
43 |
|
44 lemma wf_in_rel: |
|
45 "wf R \<Longrightarrow> wfP (in_rel R)" |
|
46 unfolding wfP_def wf_def in_rel_def . |
|
47 |
|
48 |
|
49 inductive2 accP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" |
|
50 for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
|
51 intros |
|
52 accPI: "(!!y. r y x ==> accP r y) ==> accP r x" |
|
53 |
|
54 |
|
55 theorem accP_induct: |
|
56 assumes major: "accP r a" |
|
57 assumes hyp: "!!x. accP r x ==> \<forall>y. r y x --> P y ==> P x" |
|
58 shows "P a" |
|
59 apply (rule major [THEN accP.induct]) |
|
60 apply (rule hyp) |
|
61 apply (rule accPI) |
|
62 apply fast |
|
63 apply fast |
|
64 done |
|
65 |
|
66 theorems accP_induct_rule = accP_induct [rule_format, induct set: accP] |
|
67 |
|
68 theorem accP_downward: "accP r b ==> r a b ==> accP r a" |
|
69 apply (erule accP.cases) |
|
70 apply fast |
|
71 done |
|
72 |
|
73 |
|
74 lemma accP_subset: |
|
75 assumes sub: "\<And>x y. R1 x y \<Longrightarrow> R2 x y" |
|
76 shows "\<And>x. accP R2 x \<Longrightarrow> accP R1 x" |
|
77 proof- |
|
78 fix x assume "accP R2 x" |
|
79 then show "accP R1 x" |
|
80 proof (induct x) |
|
81 fix x |
|
82 assume ih: "\<And>y. R2 y x \<Longrightarrow> accP R1 y" |
|
83 with sub show "accP R1 x" |
|
84 by (blast intro:accPI) |
|
85 qed |
|
86 qed |
|
87 |
|
88 |
|
89 lemma accP_subset_induct: |
|
90 assumes subset: "\<And>x. D x \<Longrightarrow> accP R x" |
|
91 and dcl: "\<And>x z. \<lbrakk>D x; R z x\<rbrakk> \<Longrightarrow> D z" |
|
92 and "D x" |
|
93 and istep: "\<And>x. \<lbrakk>D x; (\<And>z. R z x \<Longrightarrow> P z)\<rbrakk> \<Longrightarrow> P x" |
|
94 shows "P x" |
|
95 proof - |
|
96 from subset and `D x` |
|
97 have "accP R x" . |
|
98 then show "P x" using `D x` |
|
99 proof (induct x) |
|
100 fix x |
|
101 assume "D x" |
|
102 and "\<And>y. R y x \<Longrightarrow> D y \<Longrightarrow> P y" |
|
103 with dcl and istep show "P x" by blast |
|
104 qed |
|
105 qed |
|
106 |
|
107 |
|
108 section {* Definitions with default value *} |
26 |
109 |
27 definition |
110 definition |
28 THE_default :: "'a \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a" |
111 THE_default :: "'a \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a" |
29 "THE_default d P = (if (\<exists>!x. P x) then (THE x. P x) else d)" |
112 "THE_default d P = (if (\<exists>!x. P x) then (THE x. P x) else d)" |
30 |
113 |
39 "\<not>(\<exists>!x. P x) \<Longrightarrow> THE_default d P = d" |
122 "\<not>(\<exists>!x. P x) \<Longrightarrow> THE_default d P = d" |
40 by (simp add:THE_default_def) |
123 by (simp add:THE_default_def) |
41 |
124 |
42 |
125 |
43 lemma fundef_ex1_existence: |
126 lemma fundef_ex1_existence: |
44 assumes f_def: "f \<equiv> \<lambda>x. THE_default (d x) (\<lambda>y. (x,y)\<in>G)" |
127 assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))" |
45 assumes ex1: "\<exists>!y. (x,y)\<in>G" |
128 assumes ex1: "\<exists>!y. G x y" |
46 shows "(x, f x)\<in>G" |
129 shows "G x (f x)" |
47 by (simp only:f_def, rule THE_defaultI', rule ex1) |
130 by (simp only:f_def, rule THE_defaultI', rule ex1) |
48 |
131 |
|
132 |
|
133 |
|
134 |
|
135 |
49 lemma fundef_ex1_uniqueness: |
136 lemma fundef_ex1_uniqueness: |
50 assumes f_def: "f \<equiv> \<lambda>x. THE_default (d x) (\<lambda>y. (x,y)\<in>G)" |
137 assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))" |
51 assumes ex1: "\<exists>!y. (x,y)\<in>G" |
138 assumes ex1: "\<exists>!y. G x y" |
52 assumes elm: "(x, h x)\<in>G" |
139 assumes elm: "G x (h x)" |
53 shows "h x = f x" |
140 shows "h x = f x" |
54 by (simp only:f_def, rule THE_default1_equality[symmetric], rule ex1, rule elm) |
141 by (simp only:f_def, rule THE_default1_equality[symmetric], rule ex1, rule elm) |
55 |
142 |
56 lemma fundef_ex1_iff: |
143 lemma fundef_ex1_iff: |
57 assumes f_def: "f \<equiv> \<lambda>x. THE_default (d x) (\<lambda>y. (x,y)\<in>G)" |
144 assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))" |
58 assumes ex1: "\<exists>!y. (x,y)\<in>G" |
145 assumes ex1: "\<exists>!y. G x y" |
59 shows "((x, y)\<in>G) = (f x = y)" |
146 shows "(G x y) = (f x = y)" |
60 apply (auto simp:ex1 f_def THE_default1_equality) |
147 apply (auto simp:ex1 f_def THE_default1_equality) |
61 by (rule THE_defaultI', rule ex1) |
148 by (rule THE_defaultI', rule ex1) |
62 |
149 |
63 lemma fundef_default_value: |
150 lemma fundef_default_value: |
64 assumes f_def: "f \<equiv> \<lambda>x. THE_default (d x) (\<lambda>y. (x,y)\<in>G)" |
151 assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))" |
65 assumes graph: "\<And>x y. (x,y) \<in> G \<Longrightarrow> x \<in> D" |
152 assumes graph: "\<And>x y. G x y \<Longrightarrow> x \<in> D" |
66 assumes "x \<notin> D" |
153 assumes "x \<notin> D" |
67 shows "f x = d x" |
154 shows "f x = d x" |
68 proof - |
155 proof - |
69 have "\<not>(\<exists>y. (x, y) \<in> G)" |
156 have "\<not>(\<exists>y. G x y)" |
70 proof |
157 proof |
71 assume "(\<exists>y. (x, y) \<in> G)" |
158 assume "(\<exists>y. G x y)" |
72 with graph and `x\<notin>D` show False by blast |
159 with graph and `x\<notin>D` show False by blast |
73 qed |
160 qed |
74 hence "\<not>(\<exists>!y. (x, y) \<in> G)" by blast |
161 hence "\<not>(\<exists>!y. G x y)" by blast |
75 |
162 |
76 thus ?thesis |
163 thus ?thesis |
77 unfolding f_def |
164 unfolding f_def |
78 by (rule THE_default_none) |
165 by (rule THE_default_none) |
79 qed |
166 qed |
80 |
167 |
81 |
168 |
82 |
169 |
83 |
170 section {* Projections *} |
84 subsection {* Projections *} |
|
85 consts |
171 consts |
86 lpg::"(('a + 'b) * 'a) set" |
172 lpg::"(('a + 'b) * 'a) set" |
87 rpg::"(('a + 'b) * 'b) set" |
173 rpg::"(('a + 'b) * 'b) set" |
88 |
174 |
89 inductive lpg |
175 inductive lpg |