# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260444312 -3600
# Node ID 57944c1ef72817b0629f553c93f3d312d48cea9b
# Parent  fd718dde1d61e5aaabe491a7a8521dd0eced7e4c
Regularized the hard lemma.

diff -r fd718dde1d61 -r 57944c1ef728 Quot/Examples/FSet.thy
--- a/Quot/Examples/FSet.thy	Thu Dec 10 11:19:34 2009 +0100
+++ b/Quot/Examples/FSet.thy	Thu Dec 10 12:25:12 2009 +0100
@@ -351,14 +351,23 @@
 apply(regularize)
 apply(auto simp add: cons_rsp)
 done
-
 lemma hard: "(\<lambda>P. \<lambda>Q. P (Q (x::'a list))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a list)))"
 sorry
 
 lemma hard_lift: "(\<lambda>P. \<lambda>Q. P (Q (x::'a fset))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a fset)))"
 apply(lifting hard)
 apply(regularize)
-apply(auto)
-sorry
+apply(rule fun_rel_id_asm)
+apply(subst babs_simp)
+apply(tactic {* quotient_tac @{context} 1 *})
+apply(rule fun_rel_id_asm)
+apply(rule impI)
+apply(rule mp[OF eq_imp_rel[OF fset_equivp]])
+apply(drule fun_cong)
+apply(drule fun_cong)
+apply(assumption)
+done
+
+
 
 end
diff -r fd718dde1d61 -r 57944c1ef728 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Thu Dec 10 11:19:34 2009 +0100
+++ b/Quot/QuotMain.thy	Thu Dec 10 12:25:12 2009 +0100
@@ -435,6 +435,15 @@
 (* 5. then simplification like 0 *)
 (* finally jump back to 1 *)
 
+ML {*
+fun quotient_tac ctxt =
+  REPEAT_ALL_NEW (FIRST'
+    [rtac @{thm identity_quotient},
+     resolve_tac (quotient_rules_get ctxt)])
+
+fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
+val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac
+*}
 
 ML {*
 fun regularize_tac ctxt =
@@ -444,8 +453,8 @@
   val pat_bex  = @{term "Bex (Respects (R1 ===> R2)) P"}
   val simproc = Simplifier.simproc_i thy "" [pat_ball, pat_bex] (K (ball_bex_range_simproc))
   val simpset = (mk_minimal_ss ctxt) 
-                       addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv}
-                       addsimprocs [simproc] addSolver equiv_solver
+                       addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp}
+                       addsimprocs [simproc] addSolver equiv_solver addSolver quotient_solver
   (* TODO: Make sure that there are no list_rel, pair_rel etc involved *)
   (* can this cause loops in equiv_tac ? *)
   val eq_eqvs = map (OF1 @{thm eq_imp_rel}) (equiv_rules_get ctxt)
@@ -549,16 +558,6 @@
 section {* Injection Tactic *}
 
 ML {*
-fun quotient_tac ctxt =
-  REPEAT_ALL_NEW (FIRST'
-    [rtac @{thm identity_quotient},
-     resolve_tac (quotient_rules_get ctxt)])
-
-fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
-val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac
-*}
-
-ML {*
 fun solve_quotient_assums ctxt thm =
 let 
   val goal = hd (Drule.strip_imp_prems (cprop_of thm)) 
@@ -619,6 +618,9 @@
 lemma QUOT_TRUE_imp: "QUOT_TRUE a \<equiv> QUOT_TRUE b"
 by (simp add: QUOT_TRUE_def)
 
+lemma regularize_to_injection: "(QUOT_TRUE l \<Longrightarrow> y) \<Longrightarrow> (l = r) \<longrightarrow> y"
+  by(auto simp add: QUOT_TRUE_def)
+
 ML {*
 fun quot_true_conv1 ctxt fnctn ctrm =
   case (term_of ctrm) of
diff -r fd718dde1d61 -r 57944c1ef728 Quot/QuotScript.thy
--- a/Quot/QuotScript.thy	Thu Dec 10 11:19:34 2009 +0100
+++ b/Quot/QuotScript.thy	Thu Dec 10 12:25:12 2009 +0100
@@ -386,6 +386,11 @@
   shows "(R1 ===> R2) f g"
 using a by simp
 
+lemma fun_rel_id_asm:
+  assumes a: "\<And>x y. R1 x y \<Longrightarrow> (A \<longrightarrow> R2 (f x) (g y))"
+  shows "A \<longrightarrow> (R1 ===> R2) f g"
+using a by auto
+
 lemma quot_rel_rsp:
   assumes a: "Quotient R Abs Rep"
   shows "(R ===> R ===> op =) R R"