# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1264443286 -3600
# Node ID a2589b4bc442fcb6ee914f615b527c66a896da40
# Parent  dae038c8cd69671494c97c69cff528b9ef14379c
tuned proofs (mainly in QuotProd)

diff -r dae038c8cd69 -r a2589b4bc442 Quot/Examples/AbsRepTest.thy
--- a/Quot/Examples/AbsRepTest.thy	Mon Jan 25 18:52:22 2010 +0100
+++ b/Quot/Examples/AbsRepTest.thy	Mon Jan 25 19:14:46 2010 +0100
@@ -2,8 +2,11 @@
 imports "../QuotMain" "../QuotList" "../QuotOption" "../QuotSum" "../QuotProd" List
 begin
 
+
+(*
 ML_command "ProofContext.debug := false"
 ML_command "ProofContext.verbose := false"
+*)
 
 ML {*
 val ctxt0 = @{context}
diff -r dae038c8cd69 -r a2589b4bc442 Quot/QuotList.thy
--- a/Quot/QuotList.thy	Mon Jan 25 18:52:22 2010 +0100
+++ b/Quot/QuotList.thy	Mon Jan 25 19:14:46 2010 +0100
@@ -161,7 +161,7 @@
   assumes q1: "Quotient R1 Abs1 Rep1"
   and     q2: "Quotient R2 Abs2 Rep2"
   shows "((R1 ===> R2 ===> R1) ===> R1 ===> list_rel R2 ===> R1) foldl foldl"
-apply auto
+apply(auto)
 apply (subgoal_tac "R1 xa ya \<longrightarrow> list_rel R2 xb yb \<longrightarrow> R1 (foldl x xa xb) (foldl y ya yb)")
 apply simp
 apply (rule_tac x="xa" in spec)
@@ -192,11 +192,13 @@
 apply(simp_all)
 done
 
+
 (* Rest are unused *)
-
+text {*
 lemma list_rel_refl:
   assumes a: "\<And>x y. R x y = (R x = R y)"
   shows "list_rel R x x"
 by (induct x) (auto simp add: a)
+*}
 
 end
diff -r dae038c8cd69 -r a2589b4bc442 Quot/QuotProd.thy
--- a/Quot/QuotProd.thy	Mon Jan 25 18:52:22 2010 +0100
+++ b/Quot/QuotProd.thy	Mon Jan 25 19:14:46 2010 +0100
@@ -5,11 +5,12 @@
 fun
   prod_rel
 where
-  "prod_rel r1 r2 = (\<lambda>(a,b) (c,d). r1 a c \<and> r2 b d)"
+  "prod_rel R1 R2 = (\<lambda>(a,b) (c,d). R1 a c \<and> R2 b d)"
 
-(* prod_fun is a good mapping function *)
+declare [[map * = (prod_fun, prod_rel)]]
 
-lemma prod_equivp:
+
+lemma prod_equivp[quot_equiv]:
   assumes a: "equivp R1"
   assumes b: "equivp R2"
   shows "equivp (prod_rel R1 R2)"
@@ -21,87 +22,68 @@
 using equivp_transp[OF b] apply blast
 done
 
-lemma prod_quotient:
+lemma prod_quotient[quot_thm]:
   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
 using q1 q2
 apply (simp add: Quotient_abs_rep Quotient_abs_rep Quotient_rel_rep Quotient_rel_rep)
-using Quotient_rel[OF q1] Quotient_rel[OF q2] by blast
+using Quotient_rel[OF q1] Quotient_rel[OF q2] 
+by blast
 
-lemma pair_rsp:
+lemma pair_rsp[quot_respect]:
   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_aux:
-  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])
+by simp
 
 lemma pair_prs[quot_preserve]:
   assumes q1: "Quotient R1 Abs1 Rep1"
   assumes q2: "Quotient R2 Abs2 Rep2"
   shows "(Rep1 ---> Rep2 ---> (prod_fun Abs1 Abs2)) Pair = Pair"
-apply(simp only: expand_fun_eq fun_map_def pair_prs_aux[OF q1 q2])
-apply(simp)
+apply(simp add: expand_fun_eq)
+apply(simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
 done
 
-
-
+lemma fst_rsp[quot_respect]:
+  assumes "Quotient R1 Abs1 Rep1"
+  assumes "Quotient R2 Abs2 Rep2"
+  shows "(prod_rel R1 R2 ===> R1) fst fst"
+  by simp
 
-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:
+lemma fst_prs[quot_preserve]:
   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
+  shows "(prod_fun Rep1 Rep2 ---> Abs1) fst = fst"
+apply(simp add: expand_fun_eq)
+apply(simp add: Quotient_abs_rep[OF q1])
+done
 
-lemma fst_prs:
+lemma snd_rsp[quot_respect]:
+  assumes "Quotient R1 Abs1 Rep1"
+  assumes "Quotient R2 Abs2 Rep2"
+  shows "(prod_rel R1 R2 ===> R2) snd snd"
+  by simp
+  
+lemma snd_prs[quot_preserve]:
   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])
+  shows "(prod_fun Rep1 Rep2 ---> Abs2) snd = snd"
+apply(simp add: expand_fun_eq)
+apply(simp add: Quotient_abs_rep[OF q2])
+done
 
-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])
+lemma prod_fun_id[id_simps]: 
+  shows "prod_fun id id \<equiv> id"
+  by (rule eq_reflection) 
+     (simp add: prod_fun_def)
 
-lemma prod_fun_id[id_simps]: "prod_fun id id \<equiv> id"
-  by (rule eq_reflection) (simp add: prod_fun_def)
-
-lemma prod_rel_eq[id_simps]: "prod_rel op = op = \<equiv> op ="
+lemma prod_rel_eq[id_simps]: 
+  shows "prod_rel op = op = \<equiv> op ="
   apply (rule eq_reflection)
   apply (rule ext)+
   apply auto
   done
 
-section {* general setup for products *}
-
-declare [[map * = (prod_fun, prod_rel)]]
-
-lemmas [quot_thm] = prod_quotient
-lemmas [quot_respect] = pair_rsp
-lemmas [quot_equiv] = prod_equivp
-
 end