equal
deleted
inserted
replaced
13 and abs_inverse: "\<And>x. (Rep (Abs (R x))) = (R x)" |
13 and abs_inverse: "\<And>x. (Rep (Abs (R x))) = (R x)" |
14 and rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)" |
14 and rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)" |
15 begin |
15 begin |
16 |
16 |
17 definition |
17 definition |
|
18 ABS::"'a \<Rightarrow> 'b" |
|
19 where |
18 "ABS x \<equiv> Abs (R x)" |
20 "ABS x \<equiv> Abs (R x)" |
19 |
21 |
20 definition |
22 definition |
|
23 REP::"'b \<Rightarrow> 'a" |
|
24 where |
21 "REP a = Eps (Rep a)" |
25 "REP a = Eps (Rep a)" |
22 |
26 |
23 lemma lem9: |
27 lemma lem9: |
24 shows "R (Eps (R x)) = R x" |
28 shows "R (Eps (R x)) = R x" |
25 proof - |
29 proof - |
98 |
102 |
99 lemma R_trans2: |
103 lemma R_trans2: |
100 assumes ac: "R a c" |
104 assumes ac: "R a c" |
101 and bd: "R b d" |
105 and bd: "R b d" |
102 shows "R a b = R c d" |
106 shows "R a b = R c d" |
103 proof |
107 using ac bd |
104 assume "R a b" |
108 by (blast intro: R_trans R_sym) |
105 then have "R b a" using R_sym by blast |
|
106 then have "R b c" using ac R_trans by blast |
|
107 then have "R c b" using R_sym by blast |
|
108 then show "R c d" using bd R_trans by blast |
|
109 next |
|
110 assume "R c d" |
|
111 then have "R a d" using ac R_trans by blast |
|
112 then have "R d a" using R_sym by blast |
|
113 then have "R b a" using bd R_trans by blast |
|
114 then show "R a b" using R_sym by blast |
|
115 qed |
|
116 |
109 |
117 lemma REPS_same: |
110 lemma REPS_same: |
118 shows "R (REP a) (REP b) \<equiv> (a = b)" |
111 shows "R (REP a) (REP b) \<equiv> (a = b)" |
119 proof - |
112 proof - |
120 have "R (REP a) (REP b) = (a = b)" |
113 have "R (REP a) (REP b) = (a = b)" |