# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260171904 -3600
# Node ID 18eac4596ef1c155586b54d3a49470a192944c86
# Parent  66f39908df953ba55e7c556b0c33a1841218b924
QuotProd with product_quotient and a 3 respects and preserves lemmas.

diff -r 66f39908df95 -r 18eac4596ef1 IntEx.thy
--- a/IntEx.thy	Mon Dec 07 04:41:42 2009 +0100
+++ b/IntEx.thy	Mon Dec 07 08:45:04 2009 +0100
@@ -246,18 +246,11 @@
 
 lemma "(\<lambda>x. (x, x)) (y::my_int) = (y, y)"
 apply(tactic {* procedure_tac @{context} @{thm lam_tst} 1 *})
-defer
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(simp only: prod_rel.simps)
+(*apply(tactic {* regularize_tac @{context} 1 *}) *)
 defer
-apply(tactic {* clean_tac @{context} 1 *})
-apply(simp add: prod_rel.simps)
+apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *})
-apply(simp)
-(*apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})*)
+apply(simp add: prod_fun_def) (* Should be pair_prs *)
 sorry
 
 lemma lam_tst2: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)"
diff -r 66f39908df95 -r 18eac4596ef1 QuotMain.thy
--- a/QuotMain.thy	Mon Dec 07 04:41:42 2009 +0100
+++ b/QuotMain.thy	Mon Dec 07 08:45:04 2009 +0100
@@ -1,5 +1,5 @@
 theory QuotMain
-imports QuotScript QuotList Prove
+imports QuotScript QuotList QuotProd Prove
 uses ("quotient_info.ML")
      ("quotient.ML")
      ("quotient_def.ML")
@@ -146,15 +146,17 @@
 declare [[map * = (prod_fun, prod_rel)]]
 declare [[map "fun" = (fun_map, fun_rel)]]
 
+(* identity quotient is not here as it has to be applied first *)
 lemmas [quotient_thm] =
-  fun_quotient list_quotient
+  fun_quotient list_quotient prod_quotient
 
 lemmas [quotient_rsp] =
-  quot_rel_rsp nil_rsp cons_rsp foldl_rsp
+  quot_rel_rsp nil_rsp cons_rsp foldl_rsp pair_rsp
 
-(* OPTION, PRODUCTS *)
+(* fun_map is not here since equivp is not true *)
+(* TODO: option, ... *)
 lemmas [quotient_equiv] =
-  identity_equivp list_equivp
+  identity_equivp list_equivp prod_equivp
 
 
 ML {* maps_lookup @{theory} "List.list" *}
@@ -708,9 +710,10 @@
   let val gl = hd (Drule.strip_imp_prems (cprop_of thm)) in
   thm OF [Goal.prove_internal [] gl (fn _ => quotient_tac ctxt 1)]
   end
-  handle _ => error "solve_quotient_assums"
+  handle _ => error "solve_quotient_assums failed. Maybe a quotient_thm is missing"
 *}
 
+(* Not used *)
 (* It proves the Quotient assumptions by calling quotient_tac *)
 ML {*
 fun solve_quotient_assum i ctxt thm =
@@ -917,11 +920,17 @@
           (resolve_tac trans2 THEN' RANGE [
             quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])
 
+(* TODO: These patterns should should be somehow combined and generalized... *)
 | (Const (@{const_name fun_rel}, _) $ _ $ _) $
     (Const (@{const_name fun_rel}, _) $ _ $ _) $
     (Const (@{const_name fun_rel}, _) $ _ $ _)
     => rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt
 
+| (Const (@{const_name fun_rel}, _) $ _ $ _) $
+    (Const (@{const_name prod_rel}, _) $ _ $ _) $
+    (Const (@{const_name prod_rel}, _) $ _ $ _)
+    => rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt
+
    (* respectfulness of constants; in particular of a simple relation *)
 | _ $ (Const _) $ (Const _)  (* fun_rel, list_rel, etc but not equality *)
     => resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt
diff -r 66f39908df95 -r 18eac4596ef1 QuotProd.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/QuotProd.thy	Mon Dec 07 08:45:04 2009 +0100
@@ -0,0 +1,80 @@
+theory QuotProd
+imports QuotScript
+begin
+
+fun
+  prod_rel
+where
+  "prod_rel r1 r2 = (\<lambda>(a,b) (c,d). r1 a c \<and> r2 b d)"
+
+(* prod_fun is a good mapping function *)
+
+lemma prod_equivp:
+  assumes a: "equivp R1"
+  assumes b: "equivp R2"
+  shows "equivp (prod_rel R1 R2)"
+unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def
+apply(auto simp add: equivp_reflp[OF a] equivp_reflp[OF b])
+apply(simp only: equivp_symp[OF a])
+apply(simp only: equivp_symp[OF b])
+using equivp_transp[OF a] apply blast
+using equivp_transp[OF b] apply blast
+done
+
+lemma prod_quotient:
+  assumes q1: "Quotient R1 Abs1 Rep1"
+  assumes q2: "Quotient R2 Abs2 Rep2"
+  shows "Quotient (prod_rel R1 R2) (prod_fun Abs1 Abs2) (prod_fun Rep1 Rep2)"
+unfolding Quotient_def
+apply (simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] Quotient_rel_rep[OF q1] Quotient_rel_rep[OF q2])
+using Quotient_rel[OF q1] Quotient_rel[OF q2] by blast
+
+lemma pair_rsp:
+  assumes q1: "Quotient R1 Abs1 Rep1"
+  assumes q2: "Quotient R2 Abs2 Rep2"
+  shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair"
+by auto
+
+lemma pair_prs:
+  assumes q1: "Quotient R1 Abs1 Rep1"
+  assumes q2: "Quotient R2 Abs2 Rep2"
+  shows "(prod_fun Abs1 Abs2) (Rep1 l, Rep2 r) \<equiv> (l, r)"
+  by (simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
+
+(* TODO: Is the quotient assumption q1 necessary? *)
+(* TODO: Aren't there hard to use later? *)
+lemma fst_rsp:
+  assumes q1: "Quotient R1 Abs1 Rep1"
+  assumes q2: "Quotient R2 Abs2 Rep2"
+  assumes a: "(prod_rel R1 R2) p1 p2"
+  shows "R1 (fst p1) (fst p2)"
+  using a
+  apply(case_tac p1)
+  apply(case_tac p2)
+  apply(auto)
+  done
+
+lemma snd_rsp:
+  assumes q1: "Quotient R1 Abs1 Rep1"
+  assumes q2: "Quotient R2 Abs2 Rep2"
+  assumes a: "(prod_rel R1 R2) p1 p2"
+  shows "R2 (snd p1) (snd p2)"
+  using a
+  apply(case_tac p1)
+  apply(case_tac p2)
+  apply(auto)
+  done
+
+lemma fst_prs:
+  assumes q1: "Quotient R1 Abs1 Rep1"
+  assumes q2: "Quotient R2 Abs2 Rep2"
+  shows "Abs1 (fst ((prod_fun Rep1 Rep2) p)) = fst p"
+by (case_tac p) (auto simp add: Quotient_abs_rep[OF q1])
+
+lemma snd_prs:
+  assumes q1: "Quotient R1 Abs1 Rep1"
+  assumes q2: "Quotient R2 Abs2 Rep2"
+  shows "Abs2 (snd ((prod_fun Rep1 Rep2) p)) = snd p"
+by (case_tac p) (auto simp add: Quotient_abs_rep[OF q2])
+
+end
diff -r 66f39908df95 -r 18eac4596ef1 QuotScript.thy
--- a/QuotScript.thy	Mon Dec 07 04:41:42 2009 +0100
+++ b/QuotScript.thy	Mon Dec 07 08:45:04 2009 +0100
@@ -19,13 +19,17 @@
   unfolding equivp_def reflp_def symp_def transp_def expand_fun_eq
   by (blast)
 
-lemma equivp_refl:
-  shows "equivp R \<Longrightarrow> (\<And>x. R x x)"
-  by (simp add: equivp_reflp_symp_transp reflp_def)
-
 lemma equivp_reflp:
   shows "equivp E \<Longrightarrow> (\<And>x. E x x)"
-  by (simp add: equivp_reflp_symp_transp reflp_def)
+  by (simp only: equivp_reflp_symp_transp reflp_def)
+
+lemma equivp_symp:
+  shows "equivp E \<Longrightarrow> (\<And>x y. E x y \<Longrightarrow> E y x)"
+  by (metis equivp_reflp_symp_transp symp_def)
+
+lemma equivp_transp:
+  shows "equivp E \<Longrightarrow> (\<And>x y z. E x y \<Longrightarrow> E y z \<Longrightarrow> E x z)"
+by (metis equivp_reflp_symp_transp transp_def)
 
 definition
   "part_equivp E \<equiv> (\<exists>x. E x x) \<and> (\<forall>x y. E x y = (E x x \<and> E y y \<and> (E x = E y)))"
@@ -95,11 +99,6 @@
   by metis
 
 fun
-  prod_rel
-where
-  "prod_rel r1 r2 = (\<lambda>(a,b) (c,d). r1 a c \<and> r2 b d)"
-
-fun
   fun_map
 where
   "fun_map f g h x = g (h (f x))"