src/HOL/BNF_Def.thy
changeset 58104 c5316f843f72
parent 57802 9c065009cd8a
child 58106 c8cba801c483
     1.1 --- a/src/HOL/BNF_Def.thy	Mon Sep 01 13:23:05 2014 +0200
     1.2 +++ b/src/HOL/BNF_Def.thy	Mon Sep 01 13:23:39 2014 +0200
     1.3 @@ -15,6 +15,9 @@
     1.4    "bnf" :: thy_goal
     1.5  begin
     1.6  
     1.7 +lemma Collect_splitD: "x \<in> Collect (split A) \<Longrightarrow> A (fst x) (snd x)"
     1.8 +  by auto
     1.9 +
    1.10  definition
    1.11    rel_fun :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool"
    1.12  where
    1.13 @@ -30,6 +33,20 @@
    1.14    shows "B (f x) (g y)"
    1.15    using assms by (simp add: rel_fun_def)
    1.16  
    1.17 +definition rel_set :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> bool"
    1.18 +  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.19 +
    1.20 +lemma rel_setI:
    1.21 +  assumes "\<And>x. x \<in> A \<Longrightarrow> \<exists>y\<in>B. R x y"
    1.22 +  assumes "\<And>y. y \<in> B \<Longrightarrow> \<exists>x\<in>A. R x y"
    1.23 +  shows "rel_set R A B"
    1.24 +  using assms unfolding rel_set_def by simp
    1.25 +
    1.26 +lemma predicate2_transferD:
    1.27 +   "\<lbrakk>rel_fun R1 (rel_fun R2 (op =)) P Q; a \<in> A; b \<in> B; A \<subseteq> {(x, y). R1 x y}; B \<subseteq> {(x, y). R2 x y}\<rbrakk> \<Longrightarrow>
    1.28 +   P (fst a) (fst b) \<longleftrightarrow> Q (snd a) (snd b)"
    1.29 +  unfolding rel_fun_def by (blast dest!: Collect_splitD)
    1.30 +
    1.31  definition collect where
    1.32  "collect F x = (\<Union>f \<in> F. f x)"
    1.33