equal
deleted
inserted
replaced
46 shows "R (REP a) (REP a)" |
46 shows "R (REP a) (REP a)" |
47 unfolding REP_def |
47 unfolding REP_def |
48 by (simp add: equiv[simplified EQUIV_def]) |
48 by (simp add: equiv[simplified EQUIV_def]) |
49 |
49 |
50 lemma lem7: |
50 lemma lem7: |
51 "(R x = R y) = (Abs (R x) = Abs (R y))" |
51 shows "(R x = R y) = (Abs (R x) = Abs (R y))" |
52 apply(rule iffI) |
52 apply(rule iffI) |
53 apply(simp) |
53 apply(simp) |
54 apply(drule rep_inject[THEN iffD2]) |
54 apply(drule rep_inject[THEN iffD2]) |
55 apply(simp add: abs_inverse) |
55 apply(simp add: abs_inverse) |
56 done |
56 done |
78 apply(subst thm11[symmetric]) |
78 apply(subst thm11[symmetric]) |
79 apply(simp add: equiv[simplified EQUIV_def]) |
79 apply(simp add: equiv[simplified EQUIV_def]) |
80 done |
80 done |
81 |
81 |
82 lemma R_trans: |
82 lemma R_trans: |
83 assumes ab: "R a b" and bc: "R b c" shows "R a c" |
83 assumes ab: "R a b" |
|
84 and bc: "R b c" |
|
85 shows "R a c" |
84 proof - |
86 proof - |
85 have tr: "TRANS R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp |
87 have tr: "TRANS R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp |
86 moreover have ab: "R a b" by fact |
88 moreover have ab: "R a b" by fact |
87 moreover have bc: "R b c" by fact |
89 moreover have bc: "R b c" by fact |
88 ultimately show ?thesis unfolding TRANS_def by blast |
90 ultimately show "R a c" unfolding TRANS_def by blast |
89 qed |
91 qed |
90 |
92 |
91 lemma R_sym: |
93 lemma R_sym: |
92 assumes ab: "R a b" shows "R b a" |
94 assumes ab: "R a b" |
|
95 shows "R b a" |
93 proof - |
96 proof - |
94 have re: "SYM R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp |
97 have re: "SYM R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp |
95 then show ?thesis using ab unfolding SYM_def by blast |
98 then show "R b a" using ab unfolding SYM_def by blast |
96 qed |
99 qed |
97 |
100 |
98 lemma R_trans2: |
101 lemma R_trans2: |
99 assumes ac: "R a c" and bd: "R b d" |
102 assumes ac: "R a c" |
|
103 and bd: "R b d" |
100 shows "R a b = R c d" |
104 shows "R a b = R c d" |
101 proof |
105 proof |
102 assume ab: "R a b" |
106 assume ab: "R a b" |
103 then have "R b a" using R_sym by blast |
107 then have "R b a" using R_sym by blast |
104 then have "R b c" using ac R_trans by blast |
108 then have "R b c" using ac R_trans by blast |
116 shows "R (REP a) (REP b) = (a = b)" |
120 shows "R (REP a) (REP b) = (a = b)" |
117 proof |
121 proof |
118 assume as: "R (REP a) (REP b)" |
122 assume as: "R (REP a) (REP b)" |
119 from rep_prop |
123 from rep_prop |
120 obtain x where eq: "Rep a = R x" by auto |
124 obtain x where eq: "Rep a = R x" by auto |
121 also |
125 (*also ... not useful in the proof *) |
122 from rep_prop |
126 from rep_prop |
123 obtain y where eq2: "Rep b = R y" by auto |
127 obtain y where eq2: "Rep b = R y" by auto |
124 then have "R (Eps (R x)) (Eps (R y))" using as eq unfolding REP_def by simp |
128 then have "R (Eps (R x)) (Eps (R y))" using as eq unfolding REP_def by simp |
125 then have "R x (Eps (R y))" using lem9 by simp |
129 then have "R x (Eps (R y))" using lem9 by simp |
126 then have "R (Eps (R y)) x" using R_sym by blast |
130 then have "R (Eps (R y)) x" using R_sym by blast |