equal
deleted
inserted
replaced
121 using sr ss |
121 using sr ss |
122 unfolding symp_def |
122 unfolding symp_def |
123 apply (metis pred_comp.intros pred_compE ss symp_def) |
123 apply (metis pred_comp.intros pred_compE ss symp_def) |
124 done |
124 done |
125 |
125 |
|
126 lemma abs_o_rep: |
|
127 assumes a: "Quotient r absf repf" |
|
128 shows "absf o repf = id" |
|
129 apply(rule ext) |
|
130 apply(simp add: Quotient_abs_rep[OF a]) |
|
131 done |
|
132 |
126 lemma bla: |
133 lemma bla: |
127 assumes a1: "Quotient (op \<approx>1) abs_fset rep_fset" |
134 assumes a1: "Quotient (op \<approx>1) abs_fset rep_fset" |
128 and a2: "Quotient r2 abs2 rep2" |
135 and a2: "Quotient r2 abs2 rep2" |
129 shows "Quotient ((list_rel r2) OO (op \<approx>1) OO (list_rel r2)) (abs_fset \<circ> (map abs2)) ((map rep2) \<circ> rep_fset)" |
136 shows "Quotient ((list_rel r2) OO (op \<approx>1) OO (list_rel r2)) (abs_fset \<circ> (map abs2)) ((map rep2) \<circ> rep_fset)" |
|
137 unfolding Quotient_def comp_def |
|
138 apply (rule)+ |
|
139 apply (simp add: abs_o_rep[OF a2] id_simps Quotient_abs_rep[OF Quotient_fset]) |
|
140 apply (rule) |
|
141 apply (rule) |
|
142 sledgehammer |
|
143 apply (metis Quotient_def a2 equivp_reflp fset_equivp list_quotient list_rel_rel pred_comp.cases pred_comp.intros rep_fset_def) |
130 using a1 |
144 using a1 |
131 apply - |
145 apply - |
132 sorry |
146 sorry |
133 |
147 |
134 lemma bla2: |
148 lemma bla2: |