equal
deleted
inserted
replaced
125 FUN_REL |
125 FUN_REL |
126 where |
126 where |
127 "FUN_REL E1 E2 f g = (\<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))" |
127 "FUN_REL E1 E2 f g = (\<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))" |
128 |
128 |
129 abbreviation |
129 abbreviation |
130 FUN_REL_syn ("_ ===> _") |
130 FUN_REL_syn (infixr "===>" 55) |
131 where |
131 where |
132 "E1 ===> E2 \<equiv> FUN_REL E1 E2" |
132 "E1 ===> E2 \<equiv> FUN_REL E1 E2" |
133 |
133 |
134 lemma FUN_REL_EQ: |
134 lemma FUN_REL_EQ: |
135 "(op =) ===> (op =) = (op =)" |
135 "(op =) ===> (op =) = (op =)" |
507 lemma EXISTS_PRS: |
507 lemma EXISTS_PRS: |
508 assumes a: "QUOTIENT R absf repf" |
508 assumes a: "QUOTIENT R absf repf" |
509 shows "!f. Ex f = Bex (Respects R) ((absf ---> id) f)" |
509 shows "!f. Ex f = Bex (Respects R) ((absf ---> id) f)" |
510 sorry |
510 sorry |
511 |
511 |
|
512 (* Currently fixed, should be general *) |
512 lemma ho_all_prs: "op = ===> op = ===> op = All All" |
513 lemma ho_all_prs: "op = ===> op = ===> op = All All" |
513 apply (auto) |
514 apply (auto) |
514 done |
515 done |
515 |
516 |
516 lemma ho_ex_prs: "op = ===> op = ===> op = Ex Ex" |
517 lemma ho_ex_prs: "op = ===> op = ===> op = Ex Ex" |