equal
deleted
inserted
replaced
129 FUN_REL |
129 FUN_REL |
130 where |
130 where |
131 "FUN_REL E1 E2 f g = (\<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))" |
131 "FUN_REL E1 E2 f g = (\<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))" |
132 |
132 |
133 abbreviation |
133 abbreviation |
134 FUN_REL_syn ("_ ===> _") |
134 FUN_REL_syn (infixr "===>" 55) |
135 where |
135 where |
136 "E1 ===> E2 \<equiv> FUN_REL E1 E2" |
136 "E1 ===> E2 \<equiv> FUN_REL E1 E2" |
137 |
137 |
138 lemma FUN_REL_EQ: |
138 lemma FUN_REL_EQ: |
139 "(op =) ===> (op =) = (op =)" |
139 "(op =) ===> (op =) = (op =)" |
140 by (simp add: expand_fun_eq) |
140 by (simp add: expand_fun_eq) |
141 |
141 |
510 shows "(if a then b else c) = absf (if a then repf b else repf c)" |
510 shows "(if a then b else c) = absf (if a then repf b else repf c)" |
511 using a unfolding QUOTIENT_def by auto |
511 using a unfolding QUOTIENT_def by auto |
512 |
512 |
513 (* These are the fixed versions, general ones need to be proved. *) |
513 (* These are the fixed versions, general ones need to be proved. *) |
514 lemma ho_all_prs: |
514 lemma ho_all_prs: |
515 shows "op = ===> op = ===> op = All All" |
515 shows "((op = ===> op =) ===> op =) All All" |
516 by auto |
516 by auto |
517 |
517 |
518 lemma ho_ex_prs: |
518 lemma ho_ex_prs: |
519 shows "op = ===> op = ===> op = Ex Ex" |
519 shows "((op = ===> op =) ===> op =) Ex Ex" |
520 by auto |
520 by auto |
521 |
521 |
522 end |
522 end |
523 |
523 |