src/HOL/FunDef.thy
changeset 20523 36a59e5d0039
parent 20324 71d63a30cc96
child 20536 f088edff8af8
     1.1 --- a/src/HOL/FunDef.thy	Wed Sep 13 00:38:38 2006 +0200
     1.2 +++ b/src/HOL/FunDef.thy	Wed Sep 13 12:05:50 2006 +0200
     1.3 @@ -11,6 +11,7 @@
     1.4  ("Tools/function_package/sum_tools.ML")
     1.5  ("Tools/function_package/fundef_common.ML")
     1.6  ("Tools/function_package/fundef_lib.ML")
     1.7 +("Tools/function_package/inductive_wrap.ML")
     1.8  ("Tools/function_package/context_tree.ML")
     1.9  ("Tools/function_package/fundef_prep.ML")
    1.10  ("Tools/function_package/fundef_proof.ML")
    1.11 @@ -23,20 +24,20 @@
    1.12  begin
    1.13  
    1.14  lemma fundef_ex1_existence:
    1.15 -assumes f_def: "\<And>x. f x \<equiv> THE y. (x,y)\<in>G"
    1.16 +assumes f_def: "f \<equiv> \<lambda>x. THE y. (x,y)\<in>G"
    1.17  assumes ex1: "\<exists>!y. (x,y)\<in>G"
    1.18  shows "(x, f x)\<in>G"
    1.19    by (simp only:f_def, rule theI', rule ex1)
    1.20  
    1.21  lemma fundef_ex1_uniqueness:
    1.22 -assumes f_def: "\<And>x. f x \<equiv> THE y. (x,y)\<in>G"
    1.23 +assumes f_def: "f \<equiv> \<lambda>x. THE y. (x,y)\<in>G"
    1.24  assumes ex1: "\<exists>!y. (x,y)\<in>G"
    1.25  assumes elm: "(x, h x)\<in>G"
    1.26  shows "h x = f x"
    1.27    by (simp only:f_def, rule the1_equality[symmetric], rule ex1, rule elm)
    1.28  
    1.29  lemma fundef_ex1_iff:
    1.30 -assumes f_def: "\<And>x. f x \<equiv> THE y. (x,y)\<in>G"
    1.31 +assumes f_def: "f \<equiv> \<lambda>x. THE y. (x,y)\<in>G"
    1.32  assumes ex1: "\<exists>!y. (x,y)\<in>G"
    1.33  shows "((x, y)\<in>G) = (f x = y)"
    1.34    apply (auto simp:ex1 f_def the1_equality)
    1.35 @@ -71,6 +72,7 @@
    1.36  use "Tools/function_package/sum_tools.ML"
    1.37  use "Tools/function_package/fundef_common.ML"
    1.38  use "Tools/function_package/fundef_lib.ML"
    1.39 +use "Tools/function_package/inductive_wrap.ML"
    1.40  use "Tools/function_package/context_tree.ML"
    1.41  use "Tools/function_package/fundef_prep.ML"
    1.42  use "Tools/function_package/fundef_proof.ML"