# HG changeset patch # User Christian Urban # Date 1260466121 -3600 # Node ID 1f4dfcd9351b2e74af316c7273c5e4aa4ca81472 # Parent 91b079db738019fdd586a466e8f6d2e1f9b9b918# Parent ed44eaaea63e19233af3ec9e813fcb621c36855d merged diff -r 91b079db7380 -r 1f4dfcd9351b Quot/QuotOption.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Quot/QuotOption.thy Thu Dec 10 18:28:41 2009 +0100 @@ -0,0 +1,82 @@ +theory QuotOption +imports QuotMain +begin + +fun + option_rel +where + "option_rel R None None = True" +| "option_rel R (Some x) None = False" +| "option_rel R None (Some x) = False" +| "option_rel R (Some x) (Some y) = R x y" + +fun + option_map +where + "option_map f None = None" +| "option_map f (Some x) = Some (f x)" + +declare [[map * = (option_map, option_rel)]] + +lemma option_quotient[quot_thm]: + assumes q: "Quotient R Abs Rep" + shows "Quotient (option_rel R) (option_map Abs) (option_map Rep)" + apply (unfold Quotient_def) + apply (rule conjI) + apply (rule allI) + apply (case_tac a) + apply (simp_all add: Quotient_abs_rep[OF q]) + apply (rule conjI) + apply (rule allI) + apply (case_tac a) + apply (simp_all add: Quotient_rel_rep[OF q]) + apply (rule allI)+ + apply (case_tac r) + apply (case_tac s) + apply (simp_all add: Quotient_abs_rep[OF q] add: Quotient_rel_rep[OF q]) + apply (case_tac s) + apply (simp_all add: Quotient_abs_rep[OF q] add: Quotient_rel_rep[OF q]) + using q + unfolding Quotient_def + apply metis +done + +lemma option_rel_some: + assumes e: "equivp R" + and a: "option_rel R (Some a) = option_rel R (Some aa)" + shows "R a aa" +using a apply(drule_tac x="Some aa" in fun_cong) +apply(simp add: equivp_reflp[OF e]) +done + +lemma option_equivp[quot_equiv]: + assumes a: "equivp R" + shows "equivp (option_rel R)" + unfolding equivp_def + apply(rule allI)+ + apply(case_tac x) + apply(case_tac y) + apply(simp_all) + apply(unfold not_def) + apply(rule impI) + apply(drule_tac x="None" in fun_cong) + apply simp + apply(case_tac y) + apply(simp_all) + apply(unfold not_def) + apply(rule impI) + apply(drule_tac x="None" in fun_cong) + apply simp + apply(rule iffI) + apply(rule ext) + apply(case_tac xa) + apply(auto) + apply(rule equivp_transp[OF a]) + apply(rule equivp_symp[OF a]) + apply(assumption)+ + apply(rule equivp_transp[OF a]) + apply(assumption)+ + apply(simp only: option_rel_some[OF a]) + done + +end \ No newline at end of file diff -r 91b079db7380 -r 1f4dfcd9351b Quot/QuotSum.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Quot/QuotSum.thy Thu Dec 10 18:28:41 2009 +0100 @@ -0,0 +1,84 @@ +theory QuotSum +imports QuotMain +begin + +fun + sum_rel +where + "sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1" +| "sum_rel R1 R2 (Inl a1) (Inr b2) = False" +| "sum_rel R1 R2 (Inr a2) (Inl b1) = False" +| "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2" + +fun + sum_map +where + "sum_map f1 f2 (Inl a) = Inl (f1 a)" +| "sum_map f1 f2 (Inr a) = Inr (f2 a)" + +declare [[map * = (sum_map, sum_rel)]] + +lemma sum_equivp[quot_equiv]: + assumes a: "equivp R1" + assumes b: "equivp R2" + shows "equivp (sum_rel R1 R2)" +unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def +apply(auto) +apply(case_tac x) +apply(auto simp add: equivp_reflp[OF a] equivp_reflp[OF b]) +apply(case_tac x) +apply(case_tac y) +prefer 3 +apply(case_tac y) +apply(auto simp add: equivp_symp[OF a] equivp_symp[OF b]) +apply(case_tac x) +apply(case_tac y) +apply(case_tac z) +prefer 3 +apply(case_tac z) +prefer 5 +apply(case_tac y) +apply(case_tac z) +prefer 3 +apply(case_tac z) +apply(auto) +apply(metis equivp_transp[OF b]) +apply(metis equivp_transp[OF a]) +done + +lemma sum_fun_fun: + assumes q1: "Quotient R1 Abs1 Rep1" + assumes q2: "Quotient R2 Abs2 Rep2" + shows "sum_rel R1 R2 r s = + (sum_rel R1 R2 r r \ sum_rel R1 R2 s s \ sum_map Abs1 Abs2 r = sum_map Abs1 Abs2 s)" + using q1 q2 + apply(case_tac r) + apply(case_tac s) + apply(simp_all) + prefer 2 + apply(case_tac s) + apply(auto) + unfolding Quotient_def + apply metis+ + done + +lemma sum_quotient[quot_thm]: + assumes q1: "Quotient R1 Abs1 Rep1" + assumes q2: "Quotient R2 Abs2 Rep2" + shows "Quotient (sum_rel R1 R2) (sum_map Abs1 Abs2) (sum_map Rep1 Rep2)" + unfolding Quotient_def + apply(rule conjI) + apply(rule allI) + apply(case_tac a) + apply(simp add: Quotient_abs_rep[OF q1]) + apply(simp add: Quotient_abs_rep[OF q2]) + apply(rule conjI) + apply(rule allI) + apply(case_tac a) + apply(simp add: Quotient_rel_rep[OF q1]) + apply(simp add: Quotient_rel_rep[OF q2]) + apply(rule allI)+ + apply(rule sum_fun_fun[OF q1 q2]) + done + +end \ No newline at end of file diff -r 91b079db7380 -r 1f4dfcd9351b Quot/Quotients.thy --- a/Quot/Quotients.thy Thu Dec 10 18:28:30 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,76 +0,0 @@ -theory Quotients -imports Main -begin - -(* Other quotients that have not been proved yet *) - -fun - option_rel -where - "option_rel R None None = True" -| "option_rel R (Some x) None = False" -| "option_rel R None (Some x) = False" -| "option_rel R (Some x) (Some y) = R x y" - -fun - option_map -where - "option_map f None = None" -| "option_map f (Some x) = Some (f x)" - -fun - prod_rel -where - "prod_rel R1 R2 (a1,a2) (b1,b2) = (R1 a1 b1 \ R2 a2 b2)" - -fun - prod_map -where - "prod_map f1 f2 (a,b) = (f1 a, f2 b)" - -fun - sum_rel -where - "sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1" -| "sum_rel R1 R2 (Inl a1) (Inr b2) = False" -| "sum_rel R1 R2 (Inr a2) (Inl b1) = False" -| "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2" - -fun - sum_map -where - "sum_map f1 f2 (Inl a) = Inl (f1 a)" -| "sum_map f1 f2 (Inr a) = Inr (f2 a)" - -fun - noption_map::"('a \ 'b) \ ('a noption) \ ('b noption)" -where - "noption_map f (nSome x) = nSome (f x)" -| "noption_map f nNone = nNone" - -fun - noption_rel -where - "noption_rel r (nSome x) (nSome y) = r x y" -| "noption_rel r _ _ = False" - -declare [[map noption = (noption_map, noption_rel)]] - -lemma "noption_map id = id" -sorry - -lemma noption_Quotient: - assumes q: "Quotient R Abs Rep" - shows "Quotient (noption_rel R) (noption_map Abs) (noption_map Rep)" - apply (unfold Quotient_def) - apply (auto) - using q - apply (unfold Quotient_def) - apply (case_tac "a :: 'b noption") - apply (simp) - apply (simp) - apply (case_tac "a :: 'b noption") - apply (simp only: option_map.simps) - apply (subst option_rel.simps) - (* Simp starts hanging so don't know how to continue *) - sorry