src/HOL/Library/FuncSet.thy
changeset 61359 e985b52c3eb3
parent 59425 c5e79df8cc21
child 61378 3e04c9ca001a
     1.1 --- a/src/HOL/Library/FuncSet.thy	Wed Oct 07 15:31:59 2015 +0200
     1.2 +++ b/src/HOL/Library/FuncSet.thy	Wed Oct 07 17:11:16 2015 +0200
     1.3 @@ -184,6 +184,9 @@
     1.4  
     1.5  subsection \<open>Bounded Abstraction: @{term restrict}\<close>
     1.6  
     1.7 +lemma restrict_cong: "I = J \<Longrightarrow> (\<And>i. i \<in> J =simp=> f i = g i) \<Longrightarrow> restrict f I = restrict g J"
     1.8 +  by (auto simp: restrict_def fun_eq_iff simp_implies_def)
     1.9 +
    1.10  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.11    by (simp add: Pi_def restrict_def)
    1.12