62 |
62 |
63 |
63 |
64 lemma REP_ABS_rsp: |
64 lemma REP_ABS_rsp: |
65 shows "R f (REP (ABS g)) = R f g" |
65 shows "R f (REP (ABS g)) = R f g" |
66 and "R (REP (ABS g)) f = R g f" |
66 and "R (REP (ABS g)) f = R g f" |
67 apply(subst thm11) |
67 by (simp_all add: thm10 thm11) |
68 apply(simp add: thm10 thm11) |
|
69 apply(subst thm11) |
|
70 apply(simp add: thm10 thm11) |
|
71 done |
|
72 |
68 |
73 lemma QUOTIENT: |
69 lemma QUOTIENT: |
74 "QUOTIENT R ABS REP" |
70 "QUOTIENT R ABS REP" |
75 apply(unfold QUOTIENT_def) |
71 apply(unfold QUOTIENT_def) |
76 apply(simp add: thm10) |
72 apply(simp add: thm10) |
101 lemma R_trans2: |
97 lemma R_trans2: |
102 assumes ac: "R a c" |
98 assumes ac: "R a c" |
103 and bd: "R b d" |
99 and bd: "R b d" |
104 shows "R a b = R c d" |
100 shows "R a b = R c d" |
105 proof |
101 proof |
106 assume ab: "R a b" |
102 assume "R a b" |
107 then have "R b a" using R_sym by blast |
103 then have "R b a" using R_sym by blast |
108 then have "R b c" using ac R_trans by blast |
104 then have "R b c" using ac R_trans by blast |
109 then have "R c b" using R_sym by blast |
105 then have "R c b" using R_sym by blast |
110 then show "R c d" using bd R_trans by blast |
106 then show "R c d" using bd R_trans by blast |
111 next |
107 next |
112 assume ccd: "R c d" |
108 assume "R c d" |
113 then have "R a d" using ac R_trans by blast |
109 then have "R a d" using ac R_trans by blast |
114 then have "R d a" using R_sym by blast |
110 then have "R d a" using R_sym by blast |
115 then have "R b a" using bd R_trans by blast |
111 then have "R b a" using bd R_trans by blast |
116 then show "R a b" using R_sym by blast |
112 then show "R a b" using R_sym by blast |
117 qed |
113 qed |
119 lemma REPS_same: |
115 lemma REPS_same: |
120 shows "R (REP a) (REP b) = (a = b)" |
116 shows "R (REP a) (REP b) = (a = b)" |
121 proof |
117 proof |
122 assume as: "R (REP a) (REP b)" |
118 assume as: "R (REP a) (REP b)" |
123 from rep_prop |
119 from rep_prop |
124 obtain x where eq: "Rep a = R x" by auto |
120 obtain x y |
125 (*also ... not useful in the proof *) |
121 where eqs: "Rep a = R x" "Rep b = R y" by blast |
126 from rep_prop |
122 from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp |
127 obtain y where eq2: "Rep b = R y" by auto |
|
128 then have "R (Eps (R x)) (Eps (R y))" using as eq unfolding REP_def by simp |
|
129 then have "R x (Eps (R y))" using lem9 by simp |
123 then have "R x (Eps (R y))" using lem9 by simp |
130 then have "R (Eps (R y)) x" using R_sym by blast |
124 then have "R (Eps (R y)) x" using R_sym by blast |
131 then have "R y x" using lem9 by simp |
125 then have "R y x" using lem9 by simp |
132 then have "R x y" using R_sym by blast |
126 then have "R x y" using R_sym by blast |
133 then have "ABS x = ABS y" using thm11 by simp |
127 then have "ABS x = ABS y" using thm11 by simp |
134 then have "Abs (Rep a) = Abs (Rep b)" using eq eq2 unfolding ABS_def by simp |
128 then have "Abs (Rep a) = Abs (Rep b)" using eqs unfolding ABS_def by simp |
135 then show "a = b" using rep_inverse by simp |
129 then show "a = b" using rep_inverse by simp |
136 next |
130 next |
137 assume ab: "a = b" |
131 assume ab: "a = b" |
138 have "REFL R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp |
132 have "REFL R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp |
139 then show "R (REP a) (REP b)" unfolding REFL_def using ab by auto |
133 then show "R (REP a) (REP b)" unfolding REFL_def using ab by auto |
712 apply(simp) |
706 apply(simp) |
713 done |
707 done |
714 |
708 |
715 lemma |
709 lemma |
716 shows "((x=y) \<or> (IN x xs) = (IN (x::nat) (INSERT y xs))) = |
710 shows "((x=y) \<or> (IN x xs) = (IN (x::nat) (INSERT y xs))) = |
717 ((x = y) \<or> x memb REP_fset xs = x memb (y # REP_fset xs))" |
711 ((x=y) \<or> x memb REP_fset xs = x memb (y # REP_fset xs))" |
718 unfolding IN_def INSERT_def |
712 unfolding IN_def INSERT_def |
719 apply(rule_tac f="(op \<or>) (x=y)" in arg_cong) |
713 apply(rule_tac f="(op \<or>) (x=y)" in arg_cong) |
720 apply(rule_tac f="(op =) (x memb REP_fset xs)" in arg_cong) |
714 apply(rule_tac f="(op =) (x memb REP_fset xs)" in arg_cong) |
721 apply(rule mem_respects) |
715 apply(rule mem_respects) |
722 apply(rule list_eq.intros(3)) |
716 apply(rule list_eq.intros(3)) |