370 assumes a: "(R ===> (op =)) f g" |
370 assumes a: "(R ===> (op =)) f g" |
371 shows "(Bex1 (Respects R) f = Bex1 (Respects R) g)" |
371 shows "(Bex1 (Respects R) f = Bex1 (Respects R) g)" |
372 using a |
372 using a |
373 by (simp add: Ex1_def Bex1_def in_respects) auto |
373 by (simp add: Ex1_def Bex1_def in_respects) auto |
374 |
374 |
|
375 (* TODO/FIXME: simplify the repetitions in this proof *) |
|
376 lemma bexeq_rsp: |
|
377 assumes a: "Quotient R absf repf" |
|
378 shows "((R ===> op =) ===> op =) (Bexeq R) (Bexeq R)" |
|
379 apply simp |
|
380 unfolding Bexeq_def |
|
381 apply rule |
|
382 apply rule |
|
383 apply rule |
|
384 apply rule |
|
385 apply (erule conjE)+ |
|
386 apply (erule bexE) |
|
387 apply rule |
|
388 apply (rule_tac x="xa" in bexI) |
|
389 apply metis |
|
390 apply metis |
|
391 apply rule+ |
|
392 apply (erule_tac x="xb" in ballE) |
|
393 prefer 2 |
|
394 apply (metis in_respects) |
|
395 apply (erule_tac x="ya" in ballE) |
|
396 prefer 2 |
|
397 apply (metis in_respects) |
|
398 apply (metis in_respects) |
|
399 apply (erule conjE)+ |
|
400 apply (erule bexE) |
|
401 apply rule |
|
402 apply (rule_tac x="xa" in bexI) |
|
403 apply metis |
|
404 apply metis |
|
405 apply rule+ |
|
406 apply (erule_tac x="xb" in ballE) |
|
407 prefer 2 |
|
408 apply (metis in_respects) |
|
409 apply (erule_tac x="ya" in ballE) |
|
410 prefer 2 |
|
411 apply (metis in_respects) |
|
412 apply (metis in_respects) |
|
413 done |
|
414 |
375 lemma babs_rsp: |
415 lemma babs_rsp: |
376 assumes q: "Quotient R1 Abs1 Rep1" |
416 assumes q: "Quotient R1 Abs1 Rep1" |
377 and a: "(R1 ===> R2) f g" |
417 and a: "(R1 ===> R2) f g" |
378 shows "(R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)" |
418 shows "(R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)" |
379 apply (auto simp add: Babs_def) |
419 apply (auto simp add: Babs_def) |