Lemma "fundef_default_value" uses predicate instead of set.
authorkrauss
Fri Nov 24 13:44:51 2006 +0100 (2006-11-24)
changeset 215123786eb1b69d6
parent 21511 16c62deb1adf
child 21513 9e9fff87dc6c
Lemma "fundef_default_value" uses predicate instead of set.
src/HOL/FunDef.thy
     1.1 --- a/src/HOL/FunDef.thy	Fri Nov 24 13:43:44 2006 +0100
     1.2 +++ b/src/HOL/FunDef.thy	Fri Nov 24 13:44:51 2006 +0100
     1.3 @@ -149,14 +149,15 @@
     1.4  
     1.5  lemma fundef_default_value:
     1.6  assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
     1.7 -assumes graph: "\<And>x y. G x y \<Longrightarrow> x \<in> D"
     1.8 -assumes "x \<notin> D"
     1.9 +assumes graph: "\<And>x y. G x y \<Longrightarrow> D x"
    1.10 +assumes "\<not> D x"
    1.11  shows "f x = d x"
    1.12  proof -
    1.13    have "\<not>(\<exists>y. G x y)"
    1.14    proof
    1.15 -    assume "(\<exists>y. G x y)"
    1.16 -    with graph and `x\<notin>D` show False by blast
    1.17 +    assume "\<exists>y. G x y"
    1.18 +    hence "D x" using graph ..
    1.19 +    with `\<not> D x` show False ..
    1.20    qed
    1.21    hence "\<not>(\<exists>!y. G x y)" by blast
    1.22