src/HOL/FunDef.thy
changeset 20654 d80502f0d701
parent 20536 f088edff8af8
child 21051 c49467a9c1e1
     1.1 --- a/src/HOL/FunDef.thy	Thu Sep 21 03:17:51 2006 +0200
     1.2 +++ b/src/HOL/FunDef.thy	Thu Sep 21 12:22:05 2006 +0200
     1.3 @@ -41,25 +41,45 @@
     1.4  
     1.5  
     1.6  lemma fundef_ex1_existence:
     1.7 -assumes f_def: "f \<equiv> \<lambda>x. THE_default d (\<lambda>y. (x,y)\<in>G)"
     1.8 +assumes f_def: "f \<equiv> \<lambda>x. THE_default (d x) (\<lambda>y. (x,y)\<in>G)"
     1.9  assumes ex1: "\<exists>!y. (x,y)\<in>G"
    1.10  shows "(x, f x)\<in>G"
    1.11    by (simp only:f_def, rule THE_defaultI', rule ex1)
    1.12  
    1.13  lemma fundef_ex1_uniqueness:
    1.14 -assumes f_def: "f \<equiv> \<lambda>x. THE_default d (\<lambda>y. (x,y)\<in>G)"
    1.15 +assumes f_def: "f \<equiv> \<lambda>x. THE_default (d x) (\<lambda>y. (x,y)\<in>G)"
    1.16  assumes ex1: "\<exists>!y. (x,y)\<in>G"
    1.17  assumes elm: "(x, h x)\<in>G"
    1.18  shows "h x = f x"
    1.19    by (simp only:f_def, rule THE_default1_equality[symmetric], rule ex1, rule elm)
    1.20  
    1.21  lemma fundef_ex1_iff:
    1.22 -assumes f_def: "f \<equiv> \<lambda>x. THE_default d (\<lambda>y. (x,y)\<in>G)"
    1.23 +assumes f_def: "f \<equiv> \<lambda>x. THE_default (d x) (\<lambda>y. (x,y)\<in>G)"
    1.24  assumes ex1: "\<exists>!y. (x,y)\<in>G"
    1.25  shows "((x, y)\<in>G) = (f x = y)"
    1.26    apply (auto simp:ex1 f_def THE_default1_equality)
    1.27    by (rule THE_defaultI', rule ex1)
    1.28  
    1.29 +lemma fundef_default_value:
    1.30 +assumes f_def: "f \<equiv> \<lambda>x. THE_default (d x) (\<lambda>y. (x,y)\<in>G)"
    1.31 +assumes graph: "\<And>x y. (x,y) \<in> G \<Longrightarrow> x \<in> D"
    1.32 +assumes "x \<notin> D"
    1.33 +shows "f x = d x"
    1.34 +proof -
    1.35 +  have "\<not>(\<exists>y. (x, y) \<in> G)"
    1.36 +  proof
    1.37 +    assume "(\<exists>y. (x, y) \<in> G)"
    1.38 +    with graph and `x\<notin>D` show False by blast
    1.39 +  qed
    1.40 +  hence "\<not>(\<exists>!y. (x, y) \<in> G)" by blast
    1.41 +  
    1.42 +  thus ?thesis
    1.43 +    unfolding f_def
    1.44 +    by (rule THE_default_none)
    1.45 +qed
    1.46 +
    1.47 +
    1.48 +
    1.49  
    1.50  subsection {* Projections *}
    1.51  consts