# HG changeset patch
# User blanchet
# Date 1271772289 -7200
# Node ID 5563c717638aec144e0d148a1f6ed30370dd8c68
# Parent  3ff99369517516a38beb71814bdb825e4429aa80# Parent  61159615a0c5351d2611cbd2df0d48a4161d2498
merged

diff -r 61159615a0c5 -r 5563c717638a Admin/isatest/settings/cygwin-poly
--- a/Admin/isatest/settings/cygwin-poly	Tue Apr 20 16:04:36 2010 +0200
+++ b/Admin/isatest/settings/cygwin-poly	Tue Apr 20 16:04:49 2010 +0200
@@ -4,7 +4,7 @@
   ML_SYSTEM="polyml-5.3.0"
   ML_PLATFORM="x86-cygwin"
   ML_HOME="$POLYML_HOME/$ML_PLATFORM"
-  ML_OPTIONS="-H 500"
+  ML_OPTIONS="-H 200"
 
 ISABELLE_HOME_USER=~/isabelle-cygwin-poly
 
diff -r 61159615a0c5 -r 5563c717638a src/HOL/Library/Quotient_List.thy
--- a/src/HOL/Library/Quotient_List.thy	Tue Apr 20 16:04:36 2010 +0200
+++ b/src/HOL/Library/Quotient_List.thy	Tue Apr 20 16:04:49 2010 +0200
@@ -130,24 +130,24 @@
   by (induct l)
      (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
 
-
 lemma map_prs[quot_preserve]:
   assumes a: "Quotient R1 abs1 rep1"
   and     b: "Quotient R2 abs2 rep2"
   shows "((abs1 ---> rep2) ---> (map rep1) ---> (map abs2)) map = map"
-  by (simp only: expand_fun_eq fun_map_def map_prs_aux[OF a b])
-     (simp)
-
+  and   "((abs1 ---> id) ---> map rep1 ---> id) map = map"
+  by (simp_all only: expand_fun_eq fun_map_def map_prs_aux[OF a b])
+     (simp_all add: Quotient_abs_rep[OF a])
 
 lemma map_rsp[quot_respect]:
   assumes q1: "Quotient R1 Abs1 Rep1"
   and     q2: "Quotient R2 Abs2 Rep2"
   shows "((R1 ===> R2) ===> (list_rel R1) ===> list_rel R2) map map"
-  apply(simp)
-  apply(rule allI)+
-  apply(rule impI)
-  apply(rule allI)+
-  apply (induct_tac xa ya rule: list_induct2')
+  and   "((R1 ===> op =) ===> (list_rel R1) ===> op =) map map"
+  apply simp_all
+  apply(rule_tac [!] allI)+
+  apply(rule_tac [!] impI)
+  apply(rule_tac [!] allI)+
+  apply (induct_tac [!] xa ya rule: list_induct2')
   apply simp_all
   done
 
diff -r 61159615a0c5 -r 5563c717638a src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Tue Apr 20 16:04:36 2010 +0200
+++ b/src/HOL/Quotient.thy	Tue Apr 20 16:04:49 2010 +0200
@@ -585,19 +585,15 @@
   assumes q1: "Quotient R1 Abs1 Rep1"
   and     q2: "Quotient R2 Abs2 Rep2"
   and     q3: "Quotient R3 Abs3 Rep3"
-  shows "(Rep1 ---> Abs3) (((Abs2 ---> Rep3) f) o ((Abs1 ---> Rep2) g)) = f o g"
+  shows "((Abs2 ---> Rep3) ---> (Abs1 ---> Rep2) ---> (Rep1 ---> Abs3)) op \<circ> = op \<circ>"
+  and   "(id ---> (Abs1 ---> id) ---> Rep1 ---> id) op \<circ> = op \<circ>"
   using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] Quotient_abs_rep[OF q3]
-  unfolding o_def expand_fun_eq by simp
+  unfolding o_def expand_fun_eq by simp_all
 
 lemma o_rsp:
-  assumes q1: "Quotient R1 Abs1 Rep1"
-  and     q2: "Quotient R2 Abs2 Rep2"
-  and     q3: "Quotient R3 Abs3 Rep3"
-  and     a1: "(R2 ===> R3) f1 f2"
-  and     a2: "(R1 ===> R2) g1 g2"
-  shows "(R1 ===> R3) (f1 o g1) (f2 o g2)"
-  using a1 a2 unfolding o_def expand_fun_eq
-  by (auto)
+  "((R2 ===> R3) ===> (R1 ===> R2) ===> (R1 ===> R3)) op \<circ> op \<circ>"
+  "(op = ===> (R1 ===> op =) ===> R1 ===> op =) op \<circ> op \<circ>"
+  unfolding fun_rel_def o_def expand_fun_eq by auto
 
 lemma cond_prs:
   assumes a: "Quotient R absf repf"
@@ -716,8 +712,8 @@
 declare [[map "fun" = (fun_map, fun_rel)]]
 
 lemmas [quot_thm] = fun_quotient
-lemmas [quot_respect] = quot_rel_rsp if_rsp
-lemmas [quot_preserve] = if_prs
+lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp
+lemmas [quot_preserve] = if_prs o_prs
 lemmas [quot_equiv] = identity_equivp
 
 
diff -r 61159615a0c5 -r 5563c717638a src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Tue Apr 20 16:04:36 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Tue Apr 20 16:04:49 2010 +0200
@@ -653,10 +653,13 @@
 
 fun lifted qtys ctxt thm =
 let
-  val ((_, [thm']), ctxt') = Variable.import false [thm] ctxt
-  val goal = (quotient_lift_all qtys ctxt' o prop_of) thm'
+  (* When the theorem is atomized, eta redexes are contracted,
+     so we do it both in the original theorem *)
+  val thm' = Drule.eta_contraction_rule thm
+  val ((_, [thm'']), ctxt') = Variable.import false [thm'] ctxt
+  val goal = (quotient_lift_all qtys ctxt' o prop_of) thm''
 in
-  Goal.prove ctxt' [] [] goal (K (lift_tac ctxt' [thm] 1))
+  Goal.prove ctxt' [] [] goal (K (lift_tac ctxt' [thm'] 1))
   |> singleton (ProofContext.export ctxt' ctxt)
 end;