# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260309880 -3600
# Node ID fac547bde4c49fcf5ba6aa8de3cbd48dbb18a217
# Parent  bbaa07eea39673648d064b6b719a030d726a7da6# Parent  0b29650e3fd8bff03966535924b0a9ec06a9c786
merge

diff -r bbaa07eea396 -r fac547bde4c4 Quot/Examples/IntEx.thy
--- a/Quot/Examples/IntEx.thy	Tue Dec 08 23:04:25 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Tue Dec 08 23:04:40 2009 +0100
@@ -1,5 +1,5 @@
 theory IntEx
-imports "../QuotList" Nitpick
+imports "../QuotList" "../QuotProd" Nitpick
 begin
 
 fun
@@ -204,30 +204,23 @@
 
 lemma "foldl PLUS x [] = x"
 apply(lifting ho_tst)
-apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] nil_prs[OF Quotient_my_int])
-apply(tactic {* clean_tac @{context} 1 *})
 done
 
 lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)"
 sorry
 
 lemma "foldl PLUS x (h # t) = PLUS h (foldl PLUS x t)"
-apply(tactic {* procedure_tac @{context} @{thm ho_tst2} 1 *})
-apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} 1*})
-apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] cons_prs[OF Quotient_my_int])
-apply(tactic {* clean_tac @{context} 1 *})
+apply(lifting_setup ho_tst2)
+apply(regularize)
+apply(injection)
+apply(cleaning)
 done
 
 lemma ho_tst3: "foldl f (s::nat \<times> nat) ([]::(nat \<times> nat) list) = s"
 by simp
 
 lemma "foldl f (x::my_int) ([]::my_int list) = x"
-apply(tactic {* procedure_tac @{context} @{thm ho_tst3} 1 *})
-apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} 1*})
-apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] nil_prs[OF Quotient_my_int])
-apply(tactic {* clean_tac @{context} 1 *})
+apply(lifting ho_tst3)
 done
 
 lemma lam_tst: "(\<lambda>x. (x, x)) y = (y, (y :: nat \<times> nat))"
@@ -235,11 +228,7 @@
 
 (* Don't know how to keep the goal non-contracted... *)
 lemma "(\<lambda>x. (x, x)) (y::my_int) = (y, y)"
-apply(tactic {* procedure_tac @{context} @{thm lam_tst} 1 *})
-apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} 1*})
-apply(tactic {* clean_tac @{context} 1 *})
-apply(simp add: pair_prs)
+apply(lifting lam_tst)
 done
 
 lemma lam_tst2: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)"
@@ -308,7 +297,6 @@
 apply(rule impI)
 apply(rule lam_tst3a_reg)
 apply(tactic {* all_inj_repabs_tac @{context} 1*})
-apply(simp only: babs_prs[OF Quotient_my_int Quotient_my_int])
 apply(tactic {* clean_tac  @{context} 1 *})
 done
 
@@ -316,19 +304,10 @@
 by auto
 
 lemma "(\<lambda>(y :: my_int => my_int). y) = (\<lambda>(x :: my_int => my_int). x)"
-apply(tactic {* procedure_tac @{context} @{thm lam_tst3b} 1 *})
+apply(lifting lam_tst3b)
 apply(rule impI)
-apply (rule babs_rsp[OF fun_quotient[OF Quotient_my_int Quotient_my_int]])
-apply (simp add: id_rsp)
-apply(tactic {* all_inj_repabs_tac @{context} 1*})
-apply(tactic {* clean_tac  @{context} 1 *})
-apply(subst babs_prs)
-apply(tactic {* quotient_tac @{context} 1 *})
-apply(tactic {* quotient_tac @{context} 1 *})
-apply(subst babs_prs)
-apply(tactic {* quotient_tac @{context} 1 *})
-apply(tactic {* quotient_tac @{context} 1 *})
-apply(rule refl)
+apply(rule babs_rsp[OF fun_quotient[OF Quotient_my_int Quotient_my_int]])
+apply(simp add: id_rsp)
 done
 
 term map
@@ -342,9 +321,6 @@
 
 lemma "map (\<lambda>x. PLUS x ZERO) l = l"
 apply(lifting lam_tst4)
-apply(simp only: babs_prs[OF Quotient_my_int Quotient_my_int])
-apply(simp only: map_prs[OF Quotient_my_int Quotient_my_int])
-apply(cleaning)
 done
 
 end
diff -r bbaa07eea396 -r fac547bde4c4 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Tue Dec 08 23:04:25 2009 +0100
+++ b/Quot/QuotMain.thy	Tue Dec 08 23:04:40 2009 +0100
@@ -1,5 +1,5 @@
 theory QuotMain
-imports QuotScript QuotProd Prove
+imports QuotScript Prove
 uses ("quotient_info.ML")
      ("quotient.ML")
      ("quotient_def.ML")
@@ -142,22 +142,19 @@
 (* the auxiliary data for the quotient types *)
 use "quotient_info.ML"
 
-declare [[map * = (prod_fun, prod_rel)]]
+
 declare [[map "fun" = (fun_map, fun_rel)]]
 
 (* Throws now an exception:              *)
 (* declare [[map "option" = (bla, blu)]] *)
 
-lemmas [quot_thm] =
-  fun_quotient prod_quotient
+lemmas [quot_thm] = fun_quotient 
 
-lemmas [quot_respect] =
-  quot_rel_rsp pair_rsp
+lemmas [quot_respect] = quot_rel_rsp
 
 (* fun_map is not here since equivp is not true *)
 (* TODO: option, ... *)
-lemmas [quot_equiv] =
-  identity_equivp prod_equivp
+lemmas [quot_equiv] = identity_equivp
 
 (* definition of the quotient types *)
 (* FIXME: should be called quotient_typ.ML *)
@@ -1056,12 +1053,13 @@
     val thy = ProofContext.theory_of lthy;
     val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy)
       (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *)
-    val thms1 = @{thms all_prs ex_prs} @ defs
-    val thms2 = @{thms fun_map.simps Quotient_abs_rep Quotient_rel_rep} @ (id_simps_get lthy)
+    val thms1 = defs @ (prs_rules_get lthy)
+    val thms2 = @{thms fun_map.simps Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs} 
+                @ (id_simps_get lthy)
     fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
   in
-    EVERY' [lambda_prs_tac lthy,
-            simp_tac (simps thms1),
+    EVERY' [simp_tac (simps thms1),
+            lambda_prs_tac lthy,
             simp_tac (simps thms2),
             lambda_prs_tac lthy,
             TRY o rtac refl]
diff -r bbaa07eea396 -r fac547bde4c4 Quot/QuotProd.thy
--- a/Quot/QuotProd.thy	Tue Dec 08 23:04:25 2009 +0100
+++ b/Quot/QuotProd.thy	Tue Dec 08 23:04:40 2009 +0100
@@ -1,5 +1,5 @@
 theory QuotProd
-imports QuotScript
+imports QuotMain
 begin
 
 fun
@@ -35,12 +35,25 @@
   shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair"
 by auto
 
-lemma pair_prs:
+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])
 
+term Pair
+
+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.simps pair_prs_aux[OF q1 q2])
+apply(simp)
+done
+
+
+
+
 (* TODO: Is the quotient assumption q1 necessary? *)
 (* TODO: Aren't there hard to use later? *)
 lemma fst_rsp:
@@ -77,4 +90,13 @@
   shows "Abs2 (snd ((prod_fun Rep1 Rep2) p)) = snd p"
 by (case_tac p) (auto simp add: Quotient_abs_rep[OF q2])
 
+
+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