308 |
308 |
309 lemma bex_ex_comm: |
309 lemma bex_ex_comm: |
310 "((\<exists>y. \<exists>x. A x y) \<longrightarrow> (\<exists>y. \<exists>x\<in>P. B x y)) \<Longrightarrow> ((\<exists>x. \<exists>y. A x y) \<longrightarrow> (\<exists>x\<in>P. \<exists>y. B x y))" |
310 "((\<exists>y. \<exists>x. A x y) \<longrightarrow> (\<exists>y. \<exists>x\<in>P. B x y)) \<Longrightarrow> ((\<exists>x. \<exists>y. A x y) \<longrightarrow> (\<exists>x\<in>P. \<exists>y. B x y))" |
311 by auto |
311 by auto |
312 |
312 |
313 (* 2 lemmas needed for proving repabs_inj *) |
313 (* Bounded abstraction *) |
|
314 definition |
|
315 Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" |
|
316 where |
|
317 "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)" |
|
318 |
|
319 (* 3 lemmas needed for proving repabs_inj *) |
314 lemma ball_rsp: |
320 lemma ball_rsp: |
315 assumes a: "(R ===> (op =)) f g" |
321 assumes a: "(R ===> (op =)) f g" |
316 shows "Ball (Respects R) f = Ball (Respects R) g" |
322 shows "Ball (Respects R) f = Ball (Respects R) g" |
317 using a by (simp add: Ball_def in_respects) |
323 using a by (simp add: Ball_def in_respects) |
318 |
324 |
319 lemma bex_rsp: |
325 lemma bex_rsp: |
320 assumes a: "(R ===> (op =)) f g" |
326 assumes a: "(R ===> (op =)) f g" |
321 shows "(Bex (Respects R) f = Bex (Respects R) g)" |
327 shows "(Bex (Respects R) f = Bex (Respects R) g)" |
322 using a by (simp add: Bex_def in_respects) |
328 using a by (simp add: Bex_def in_respects) |
|
329 |
|
330 lemma babs_rsp: |
|
331 assumes q: "Quotient R1 Abs1 Rep1" |
|
332 and a: "(R1 ===> R2) f g" |
|
333 shows "(R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)" |
|
334 apply (auto simp add: Babs_def) |
|
335 apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1") |
|
336 using a apply (simp add: Babs_def) |
|
337 apply (simp add: in_respects) |
|
338 using Quotient_rel[OF q] |
|
339 by metis |
323 |
340 |
324 (* 2 lemmas needed for cleaning of quantifiers *) |
341 (* 2 lemmas needed for cleaning of quantifiers *) |
325 lemma all_prs: |
342 lemma all_prs: |
326 assumes a: "Quotient R absf repf" |
343 assumes a: "Quotient R absf repf" |
327 shows "Ball (Respects R) ((absf ---> id) f) = All f" |
344 shows "Ball (Respects R) ((absf ---> id) f) = All f" |