# HG changeset patch # User Cezary Kaliszyk # Date 1262711420 -3600 # Node ID 77506496e6fd4cd691be3b24ea541994b2ac9337 # Parent 18b71981c1f0fbecdb42148a2e785af9b04abc4f# Parent e038928daa678ce3ebad7a56038a034a6d3cba3b merge diff -r e038928daa67 -r 77506496e6fd Quot/Examples/AbsRepTest.thy --- a/Quot/Examples/AbsRepTest.thy Tue Jan 05 17:12:35 2010 +0100 +++ b/Quot/Examples/AbsRepTest.thy Tue Jan 05 18:10:20 2010 +0100 @@ -128,11 +128,25 @@ apply (metis pred_comp.intros pred_compE ss symp_def) done +lemma abs_o_rep: + assumes a: "Quotient r absf repf" + shows "absf o repf = id" + apply(rule ext) + apply(simp add: Quotient_abs_rep[OF a]) +done + lemma bla: assumes a1: "Quotient (op \1) abs_fset rep_fset" and a2: "Quotient r2 abs2 rep2" shows "Quotient ((list_rel r2) OO (op \1) OO (list_rel r2)) (abs_fset \ (map abs2)) ((map rep2) \ rep_fset)" + unfolding Quotient_def comp_def +apply (rule)+ +apply (simp add: abs_o_rep[OF a2] id_simps Quotient_abs_rep[OF Quotient_fset]) +apply (rule) +apply (rule) +sledgehammer +apply (metis Quotient_def a2 equivp_reflp fset_equivp list_quotient list_rel_rel pred_comp.cases pred_comp.intros rep_fset_def) using a1 apply - sorry