equal
deleted
inserted
replaced
129 -- {* The general elimination rule. *} |
129 -- {* The general elimination rule. *} |
130 by (unfold Id_on_def) (iprover elim!: UN_E singletonE) |
130 by (unfold Id_on_def) (iprover elim!: UN_E singletonE) |
131 |
131 |
132 lemma Id_on_iff: "((x, y) : Id_on A) = (x = y & x : A)" |
132 lemma Id_on_iff: "((x, y) : Id_on A) = (x = y & x : A)" |
133 by blast |
133 by blast |
|
134 |
|
135 lemma Id_on_def'[nitpick_def, code]: |
|
136 "(Id_on (A :: 'a => bool)) = (%(x, y). x = y \<and> A x)" |
|
137 by (auto simp add: fun_eq_iff |
|
138 elim: Id_onE[unfolded mem_def] intro: Id_onI[unfolded mem_def]) |
134 |
139 |
135 lemma Id_on_subset_Times: "Id_on A \<subseteq> A \<times> A" |
140 lemma Id_on_subset_Times: "Id_on A \<subseteq> A \<times> A" |
136 by blast |
141 by blast |
137 |
142 |
138 |
143 |