src/HOL/Library/FuncSet.thy
changeset 54417 dbb8ecfe1337
parent 53381 355a4cac5440
child 56777 9c3f0ae99532
     1.1 --- a/src/HOL/Library/FuncSet.thy	Tue Nov 12 19:28:55 2013 +0100
     1.2 +++ b/src/HOL/Library/FuncSet.thy	Tue Nov 12 19:28:56 2013 +0100
     1.3 @@ -183,18 +183,20 @@
     1.4  
     1.5  subsection{*Bounded Abstraction: @{term restrict}*}
     1.6  
     1.7 -lemma restrict_in_funcset: "(!!x. x \<in> A ==> f x \<in> B) ==> (\<lambda>x\<in>A. f x) \<in> A -> B"
     1.8 +lemma restrict_in_funcset: "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> B) \<Longrightarrow> (\<lambda>x\<in>A. f x) \<in> A \<rightarrow> B"
     1.9    by (simp add: Pi_def restrict_def)
    1.10  
    1.11 -lemma restrictI[intro!]: "(!!x. x \<in> A ==> f x \<in> B x) ==> (\<lambda>x\<in>A. f x) \<in> Pi A B"
    1.12 +lemma restrictI[intro!]: "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> B x) \<Longrightarrow> (\<lambda>x\<in>A. f x) \<in> Pi A B"
    1.13    by (simp add: Pi_def restrict_def)
    1.14  
    1.15 -lemma restrict_apply [simp]:
    1.16 -    "(\<lambda>y\<in>A. f y) x = (if x \<in> A then f x else undefined)"
    1.17 +lemma restrict_apply[simp]: "(\<lambda>y\<in>A. f y) x = (if x \<in> A then f x else undefined)"
    1.18    by (simp add: restrict_def)
    1.19  
    1.20 +lemma restrict_apply': "x \<in> A \<Longrightarrow> (\<lambda>y\<in>A. f y) x = f x"
    1.21 +  by simp
    1.22 +
    1.23  lemma restrict_ext:
    1.24 -    "(!!x. x \<in> A ==> f x = g x) ==> (\<lambda>x\<in>A. f x) = (\<lambda>x\<in>A. g x)"
    1.25 +    "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> (\<lambda>x\<in>A. f x) = (\<lambda>x\<in>A. g x)"
    1.26    by (simp add: fun_eq_iff Pi_def restrict_def)
    1.27  
    1.28  lemma inj_on_restrict_eq [simp]: "inj_on (restrict f A) A = inj_on f A"
    1.29 @@ -364,6 +366,9 @@
    1.30  lemma PiE_empty_domain[simp]: "PiE {} T = {%x. undefined}"
    1.31    unfolding PiE_def by simp
    1.32  
    1.33 +lemma PiE_UNIV_domain: "PiE UNIV T = Pi UNIV T"
    1.34 +  unfolding PiE_def by simp
    1.35 +
    1.36  lemma PiE_empty_range[simp]: "i \<in> I \<Longrightarrow> F i = {} \<Longrightarrow> (PIE i:I. F i) = {}"
    1.37    unfolding PiE_def by auto
    1.38