39 "\<not>(\<exists>!x. P x) \<Longrightarrow> THE_default d P = d" |
39 "\<not>(\<exists>!x. P x) \<Longrightarrow> THE_default d P = d" |
40 by (simp add:THE_default_def) |
40 by (simp add:THE_default_def) |
41 |
41 |
42 |
42 |
43 lemma fundef_ex1_existence: |
43 lemma fundef_ex1_existence: |
44 assumes f_def: "f \<equiv> \<lambda>x. THE_default d (\<lambda>y. (x,y)\<in>G)" |
44 assumes f_def: "f \<equiv> \<lambda>x. THE_default (d x) (\<lambda>y. (x,y)\<in>G)" |
45 assumes ex1: "\<exists>!y. (x,y)\<in>G" |
45 assumes ex1: "\<exists>!y. (x,y)\<in>G" |
46 shows "(x, f x)\<in>G" |
46 shows "(x, f x)\<in>G" |
47 by (simp only:f_def, rule THE_defaultI', rule ex1) |
47 by (simp only:f_def, rule THE_defaultI', rule ex1) |
48 |
48 |
49 lemma fundef_ex1_uniqueness: |
49 lemma fundef_ex1_uniqueness: |
50 assumes f_def: "f \<equiv> \<lambda>x. THE_default d (\<lambda>y. (x,y)\<in>G)" |
50 assumes f_def: "f \<equiv> \<lambda>x. THE_default (d x) (\<lambda>y. (x,y)\<in>G)" |
51 assumes ex1: "\<exists>!y. (x,y)\<in>G" |
51 assumes ex1: "\<exists>!y. (x,y)\<in>G" |
52 assumes elm: "(x, h x)\<in>G" |
52 assumes elm: "(x, h x)\<in>G" |
53 shows "h x = f x" |
53 shows "h x = f x" |
54 by (simp only:f_def, rule THE_default1_equality[symmetric], rule ex1, rule elm) |
54 by (simp only:f_def, rule THE_default1_equality[symmetric], rule ex1, rule elm) |
55 |
55 |
56 lemma fundef_ex1_iff: |
56 lemma fundef_ex1_iff: |
57 assumes f_def: "f \<equiv> \<lambda>x. THE_default d (\<lambda>y. (x,y)\<in>G)" |
57 assumes f_def: "f \<equiv> \<lambda>x. THE_default (d x) (\<lambda>y. (x,y)\<in>G)" |
58 assumes ex1: "\<exists>!y. (x,y)\<in>G" |
58 assumes ex1: "\<exists>!y. (x,y)\<in>G" |
59 shows "((x, y)\<in>G) = (f x = y)" |
59 shows "((x, y)\<in>G) = (f x = y)" |
60 apply (auto simp:ex1 f_def THE_default1_equality) |
60 apply (auto simp:ex1 f_def THE_default1_equality) |
61 by (rule THE_defaultI', rule ex1) |
61 by (rule THE_defaultI', rule ex1) |
|
62 |
|
63 lemma fundef_default_value: |
|
64 assumes f_def: "f \<equiv> \<lambda>x. THE_default (d x) (\<lambda>y. (x,y)\<in>G)" |
|
65 assumes graph: "\<And>x y. (x,y) \<in> G \<Longrightarrow> x \<in> D" |
|
66 assumes "x \<notin> D" |
|
67 shows "f x = d x" |
|
68 proof - |
|
69 have "\<not>(\<exists>y. (x, y) \<in> G)" |
|
70 proof |
|
71 assume "(\<exists>y. (x, y) \<in> G)" |
|
72 with graph and `x\<notin>D` show False by blast |
|
73 qed |
|
74 hence "\<not>(\<exists>!y. (x, y) \<in> G)" by blast |
|
75 |
|
76 thus ?thesis |
|
77 unfolding f_def |
|
78 by (rule THE_default_none) |
|
79 qed |
|
80 |
|
81 |
62 |
82 |
63 |
83 |
64 subsection {* Projections *} |
84 subsection {* Projections *} |
65 consts |
85 consts |
66 lpg::"(('a + 'b) * 'a) set" |
86 lpg::"(('a + 'b) * 'a) set" |