equal
deleted
inserted
replaced
11 definition |
11 definition |
12 prod_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool" |
12 prod_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool" |
13 where |
13 where |
14 "prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)" |
14 "prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)" |
15 |
15 |
16 declare [[map prod = (map_pair, prod_rel)]] |
16 declare [[map prod = prod_rel]] |
17 |
17 |
18 lemma prod_rel_apply [simp]: |
18 lemma prod_rel_apply [simp]: |
19 "prod_rel R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d" |
19 "prod_rel R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d" |
20 by (simp add: prod_rel_def) |
20 by (simp add: prod_rel_def) |
21 |
21 |