equal
deleted
inserted
replaced
147 apply (auto simp:ex1 f_def THE_default1_equality) |
147 apply (auto simp:ex1 f_def THE_default1_equality) |
148 by (rule THE_defaultI', rule ex1) |
148 by (rule THE_defaultI', rule ex1) |
149 |
149 |
150 lemma fundef_default_value: |
150 lemma fundef_default_value: |
151 assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))" |
151 assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))" |
152 assumes graph: "\<And>x y. G x y \<Longrightarrow> x \<in> D" |
152 assumes graph: "\<And>x y. G x y \<Longrightarrow> D x" |
153 assumes "x \<notin> D" |
153 assumes "\<not> D x" |
154 shows "f x = d x" |
154 shows "f x = d x" |
155 proof - |
155 proof - |
156 have "\<not>(\<exists>y. G x y)" |
156 have "\<not>(\<exists>y. G x y)" |
157 proof |
157 proof |
158 assume "(\<exists>y. G x y)" |
158 assume "\<exists>y. G x y" |
159 with graph and `x\<notin>D` show False by blast |
159 hence "D x" using graph .. |
|
160 with `\<not> D x` show False .. |
160 qed |
161 qed |
161 hence "\<not>(\<exists>!y. G x y)" by blast |
162 hence "\<not>(\<exists>!y. G x y)" by blast |
162 |
163 |
163 thus ?thesis |
164 thus ?thesis |
164 unfolding f_def |
165 unfolding f_def |