src/HOL/FunDef.thy
 changeset 20523 36a59e5d0039 parent 20324 71d63a30cc96 child 20536 f088edff8af8
```--- a/src/HOL/FunDef.thy	Wed Sep 13 00:38:38 2006 +0200
+++ b/src/HOL/FunDef.thy	Wed Sep 13 12:05:50 2006 +0200
@@ -11,6 +11,7 @@
("Tools/function_package/sum_tools.ML")
("Tools/function_package/fundef_common.ML")
("Tools/function_package/fundef_lib.ML")
+("Tools/function_package/inductive_wrap.ML")
("Tools/function_package/context_tree.ML")
("Tools/function_package/fundef_prep.ML")
("Tools/function_package/fundef_proof.ML")
@@ -23,20 +24,20 @@
begin

lemma fundef_ex1_existence:
-assumes f_def: "\<And>x. f x \<equiv> THE y. (x,y)\<in>G"
+assumes f_def: "f \<equiv> \<lambda>x. THE y. (x,y)\<in>G"
assumes ex1: "\<exists>!y. (x,y)\<in>G"
shows "(x, f x)\<in>G"
by (simp only:f_def, rule theI', rule ex1)

lemma fundef_ex1_uniqueness:
-assumes f_def: "\<And>x. f x \<equiv> THE y. (x,y)\<in>G"
+assumes f_def: "f \<equiv> \<lambda>x. THE y. (x,y)\<in>G"
assumes ex1: "\<exists>!y. (x,y)\<in>G"
assumes elm: "(x, h x)\<in>G"
shows "h x = f x"
by (simp only:f_def, rule the1_equality[symmetric], rule ex1, rule elm)

lemma fundef_ex1_iff:
-assumes f_def: "\<And>x. f x \<equiv> THE y. (x,y)\<in>G"
+assumes f_def: "f \<equiv> \<lambda>x. THE y. (x,y)\<in>G"
assumes ex1: "\<exists>!y. (x,y)\<in>G"
shows "((x, y)\<in>G) = (f x = y)"
apply (auto simp:ex1 f_def the1_equality)
@@ -71,6 +72,7 @@
use "Tools/function_package/sum_tools.ML"
use "Tools/function_package/fundef_common.ML"
use "Tools/function_package/fundef_lib.ML"
+use "Tools/function_package/inductive_wrap.ML"
use "Tools/function_package/context_tree.ML"
use "Tools/function_package/fundef_prep.ML"
use "Tools/function_package/fundef_proof.ML"```