equal
deleted
inserted
replaced
126 by auto |
126 by auto |
127 |
127 |
128 lemma Domaimp_refl[transfer_domain_rule]: |
128 lemma Domaimp_refl[transfer_domain_rule]: |
129 "Domainp T = Domainp T" .. |
129 "Domainp T = Domainp T" .. |
130 |
130 |
131 lemma Domainp_prod_fun_eq[transfer_domain_rule]: |
131 lemma Domainp_prod_fun_eq[relator_domain]: |
132 assumes "Domainp T = P" |
132 "Domainp (op= ===> T) = (\<lambda>f. \<forall>x. (Domainp T) (f x))" |
133 shows "Domainp (op= ===> T) = (\<lambda>f. \<forall>x. P (f x))" |
133 by (auto intro: choice simp: Domainp_iff rel_fun_def fun_eq_iff) |
134 by (auto intro: choice simp: assms[symmetric] Domainp_iff rel_fun_def fun_eq_iff) |
|
135 |
134 |
136 subsection {* Predicates on relations, i.e. ``class constraints'' *} |
135 subsection {* Predicates on relations, i.e. ``class constraints'' *} |
137 |
136 |
138 definition left_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" |
137 definition left_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" |
139 where "left_total R \<longleftrightarrow> (\<forall>x. \<exists>y. R x y)" |
138 where "left_total R \<longleftrightarrow> (\<forall>x. \<exists>y. R x y)" |