src/HOL/Lifting_Set.thy
changeset 58104 c5316f843f72
parent 57599 7ef939f89776
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Lifting_Set.thy	Mon Sep 01 13:23:05 2014 +0200
     1.2 +++ b/src/HOL/Lifting_Set.thy	Mon Sep 01 13:23:39 2014 +0200
     1.3 @@ -10,15 +10,6 @@
     1.4  
     1.5  subsection {* Relator and predicator properties *}
     1.6  
     1.7 -definition rel_set :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> bool"
     1.8 -  where "rel_set R = (\<lambda>A B. (\<forall>x\<in>A. \<exists>y\<in>B. R x y) \<and> (\<forall>y\<in>B. \<exists>x\<in>A. R x y))"
     1.9 -
    1.10 -lemma rel_setI:
    1.11 -  assumes "\<And>x. x \<in> A \<Longrightarrow> \<exists>y\<in>B. R x y"
    1.12 -  assumes "\<And>y. y \<in> B \<Longrightarrow> \<exists>x\<in>A. R x y"
    1.13 -  shows "rel_set R A B"
    1.14 -  using assms unfolding rel_set_def by simp
    1.15 -
    1.16  lemma rel_setD1: "\<lbrakk> rel_set R A B; x \<in> A \<rbrakk> \<Longrightarrow> \<exists>y \<in> B. R x y"
    1.17    and rel_setD2: "\<lbrakk> rel_set R A B; y \<in> B \<rbrakk> \<Longrightarrow> \<exists>x \<in> A. R x y"
    1.18  by(simp_all add: rel_set_def)