9 imports Accessible_Part Datatype Recdef |
9 imports Accessible_Part Datatype Recdef |
10 uses |
10 uses |
11 ("Tools/function_package/sum_tools.ML") |
11 ("Tools/function_package/sum_tools.ML") |
12 ("Tools/function_package/fundef_common.ML") |
12 ("Tools/function_package/fundef_common.ML") |
13 ("Tools/function_package/fundef_lib.ML") |
13 ("Tools/function_package/fundef_lib.ML") |
|
14 ("Tools/function_package/inductive_wrap.ML") |
14 ("Tools/function_package/context_tree.ML") |
15 ("Tools/function_package/context_tree.ML") |
15 ("Tools/function_package/fundef_prep.ML") |
16 ("Tools/function_package/fundef_prep.ML") |
16 ("Tools/function_package/fundef_proof.ML") |
17 ("Tools/function_package/fundef_proof.ML") |
17 ("Tools/function_package/termination.ML") |
18 ("Tools/function_package/termination.ML") |
18 ("Tools/function_package/mutual.ML") |
19 ("Tools/function_package/mutual.ML") |
21 ("Tools/function_package/fundef_datatype.ML") |
22 ("Tools/function_package/fundef_datatype.ML") |
22 ("Tools/function_package/auto_term.ML") |
23 ("Tools/function_package/auto_term.ML") |
23 begin |
24 begin |
24 |
25 |
25 lemma fundef_ex1_existence: |
26 lemma fundef_ex1_existence: |
26 assumes f_def: "\<And>x. f x \<equiv> THE y. (x,y)\<in>G" |
27 assumes f_def: "f \<equiv> \<lambda>x. THE y. (x,y)\<in>G" |
27 assumes ex1: "\<exists>!y. (x,y)\<in>G" |
28 assumes ex1: "\<exists>!y. (x,y)\<in>G" |
28 shows "(x, f x)\<in>G" |
29 shows "(x, f x)\<in>G" |
29 by (simp only:f_def, rule theI', rule ex1) |
30 by (simp only:f_def, rule theI', rule ex1) |
30 |
31 |
31 lemma fundef_ex1_uniqueness: |
32 lemma fundef_ex1_uniqueness: |
32 assumes f_def: "\<And>x. f x \<equiv> THE y. (x,y)\<in>G" |
33 assumes f_def: "f \<equiv> \<lambda>x. THE y. (x,y)\<in>G" |
33 assumes ex1: "\<exists>!y. (x,y)\<in>G" |
34 assumes ex1: "\<exists>!y. (x,y)\<in>G" |
34 assumes elm: "(x, h x)\<in>G" |
35 assumes elm: "(x, h x)\<in>G" |
35 shows "h x = f x" |
36 shows "h x = f x" |
36 by (simp only:f_def, rule the1_equality[symmetric], rule ex1, rule elm) |
37 by (simp only:f_def, rule the1_equality[symmetric], rule ex1, rule elm) |
37 |
38 |
38 lemma fundef_ex1_iff: |
39 lemma fundef_ex1_iff: |
39 assumes f_def: "\<And>x. f x \<equiv> THE y. (x,y)\<in>G" |
40 assumes f_def: "f \<equiv> \<lambda>x. THE y. (x,y)\<in>G" |
40 assumes ex1: "\<exists>!y. (x,y)\<in>G" |
41 assumes ex1: "\<exists>!y. (x,y)\<in>G" |
41 shows "((x, y)\<in>G) = (f x = y)" |
42 shows "((x, y)\<in>G) = (f x = y)" |
42 apply (auto simp:ex1 f_def the1_equality) |
43 apply (auto simp:ex1 f_def the1_equality) |
43 by (rule theI', rule ex1) |
44 by (rule theI', rule ex1) |
44 |
45 |
69 |
70 |
70 |
71 |
71 use "Tools/function_package/sum_tools.ML" |
72 use "Tools/function_package/sum_tools.ML" |
72 use "Tools/function_package/fundef_common.ML" |
73 use "Tools/function_package/fundef_common.ML" |
73 use "Tools/function_package/fundef_lib.ML" |
74 use "Tools/function_package/fundef_lib.ML" |
|
75 use "Tools/function_package/inductive_wrap.ML" |
74 use "Tools/function_package/context_tree.ML" |
76 use "Tools/function_package/context_tree.ML" |
75 use "Tools/function_package/fundef_prep.ML" |
77 use "Tools/function_package/fundef_prep.ML" |
76 use "Tools/function_package/fundef_proof.ML" |
78 use "Tools/function_package/fundef_proof.ML" |
77 use "Tools/function_package/termination.ML" |
79 use "Tools/function_package/termination.ML" |
78 use "Tools/function_package/mutual.ML" |
80 use "Tools/function_package/mutual.ML" |