equal
deleted
inserted
replaced
45 then show "R (Eps (R x)) = R x" |
45 then show "R (Eps (R x)) = R x" |
46 using equivp unfolding equivp_def by simp |
46 using equivp unfolding equivp_def by simp |
47 qed |
47 qed |
48 |
48 |
49 theorem thm10: |
49 theorem thm10: |
50 shows "abs (rep a) \<equiv> a" |
50 shows "abs (rep a) = a" |
51 apply (rule eq_reflection) |
|
52 unfolding abs_def rep_def |
51 unfolding abs_def rep_def |
53 proof - |
52 proof - |
54 from rep_prop |
53 from rep_prop |
55 obtain x where eq: "Rep a = R x" by auto |
54 obtain x where eq: "Rep a = R x" by auto |
56 have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp |
55 have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp |
110 |
109 |
111 |
110 |
112 text {* Lemmas about simplifying id's. *} |
111 text {* Lemmas about simplifying id's. *} |
113 lemmas [id_simps] = |
112 lemmas [id_simps] = |
114 id_def[symmetric] |
113 id_def[symmetric] |
115 fun_map_id[THEN eq_reflection] |
114 fun_map_id |
116 id_apply[THEN eq_reflection] |
115 id_apply[THEN eq_reflection] |
117 id_o[THEN eq_reflection] |
116 id_o |
118 o_id[THEN eq_reflection] |
117 o_id |
119 eq_comp_r |
118 eq_comp_r |
120 |
119 |
121 text {* Translation functions for the lifting process. *} |
120 text {* Translation functions for the lifting process. *} |
122 use "quotient_term.ML" |
121 use "quotient_term.ML" |
123 |
122 |