equal
deleted
inserted
replaced
79 shows "EQUIV (op =)" |
79 shows "EQUIV (op =)" |
80 unfolding EQUIV_def |
80 unfolding EQUIV_def |
81 by auto |
81 by auto |
82 |
82 |
83 lemma IDENTITY_QUOTIENT: |
83 lemma IDENTITY_QUOTIENT: |
84 shows "QUOTIENT (op =) (\<lambda>x. x) (\<lambda>x. x)" |
84 shows "QUOTIENT (op =) id id" |
85 unfolding QUOTIENT_def |
85 unfolding QUOTIENT_def id_def |
86 by blast |
86 by blast |
87 |
87 |
88 lemma QUOTIENT_SYM: |
88 lemma QUOTIENT_SYM: |
89 assumes a: "QUOTIENT E Abs Rep" |
89 assumes a: "QUOTIENT E Abs Rep" |
90 shows "SYM E" |
90 shows "SYM E" |
112 fun_map_syn (infixr "--->" 55) |
112 fun_map_syn (infixr "--->" 55) |
113 where |
113 where |
114 "f ---> g \<equiv> fun_map f g" |
114 "f ---> g \<equiv> fun_map f g" |
115 |
115 |
116 lemma FUN_MAP_I: |
116 lemma FUN_MAP_I: |
117 shows "((\<lambda>x. x) ---> (\<lambda>x. x)) = (\<lambda>x. x)" |
117 shows "(id ---> id) = id" |
118 by (simp add: expand_fun_eq) |
118 by (simp add: expand_fun_eq id_def) |
119 |
119 |
120 lemma IN_FUN: |
120 lemma IN_FUN: |
121 shows "x \<in> ((f ---> g) s) = g (f x \<in> s)" |
121 shows "x \<in> ((f ---> g) s) = g (f x \<in> s)" |
122 by (simp add: mem_def) |
122 by (simp add: mem_def) |
123 |
123 |
380 |
380 |
381 (* combinators: I, K, o, C, W *) |
381 (* combinators: I, K, o, C, W *) |
382 |
382 |
383 lemma I_PRS: |
383 lemma I_PRS: |
384 assumes q: "QUOTIENT R Abs Rep" |
384 assumes q: "QUOTIENT R Abs Rep" |
385 shows "(\<lambda>x. x) e = Abs ((\<lambda> x. x) (Rep e))" |
385 shows "id e = Abs (id (Rep e))" |
386 using QUOTIENT_ABS_REP[OF q] by auto |
386 using QUOTIENT_ABS_REP[OF q] by auto |
387 |
387 |
388 lemma I_RSP: |
388 lemma I_RSP: |
389 assumes q: "QUOTIENT R Abs Rep" |
389 assumes q: "QUOTIENT R Abs Rep" |
390 and a: "R e1 e2" |
390 and a: "R e1 e2" |
391 shows "R ((\<lambda>x. x) e1) ((\<lambda> x. x) e2)" |
391 shows "R (id e1) (id e2)" |
392 using a by auto |
392 using a by auto |
393 |
393 |
394 lemma o_PRS: |
394 lemma o_PRS: |
395 assumes q1: "QUOTIENT R1 Abs1 Rep1" |
395 assumes q1: "QUOTIENT R1 Abs1 Rep1" |
396 and q2: "QUOTIENT R2 Abs2 Rep2" |
396 and q2: "QUOTIENT R2 Abs2 Rep2" |