# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1256211948 -7200
# Node ID 0288dd5b7ed406fddad01bd648b026eb73c63d5d
# Parent  53277fbb2dba0307a453fab3dd5016ea07ae3dff
The problems with 'abs' term.

diff -r 53277fbb2dba -r 0288dd5b7ed4 QuotMain.thy
--- a/QuotMain.thy	Thu Oct 22 11:43:12 2009 +0200
+++ b/QuotMain.thy	Thu Oct 22 13:45:48 2009 +0200
@@ -1088,6 +1088,35 @@
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
 (* TODO don't know how to handle ho_respects *)
+apply (simp only: FUN_REL.simps)
+apply (rule allI)
+apply (rule allI)
+apply (rule impI)
+ML_prf {*
+  val concl = (#concl o fst) (Subgoal.focus @{context} 1 (Isar.goal ()));
+  val pat = Drule.strip_imp_concl (cprop_of @{thm RES_FORALL_RSP});
+  val ((_,p),(_,c)) = (Thm.dest_comb pat, Thm.dest_comb concl);
+  val ((_,p),(_,c)) = (Thm.dest_comb p, Thm.dest_comb c);
+*}
+ML_prf {*
+  val ((_,pn),(_,cn)) = (Thm.dest_comb p, Thm.dest_comb c);
+  val (pnm, cnm) = (@{cpat "?a"}, @{cterm "b::('a List.list \<Rightarrow> bool)"});
+  val (pp, cc) = (term_of pn, term_of cn);
+  val (ppt, cct) = (type_of pp, type_of cc);
+  val (ppm, ccm) = (term_of pnm, term_of cnm);
+  val i = Pattern.first_order_match @{theory} (ppm, ccm) (Vartab.empty, Vartab.empty);
+  val (ppmt, ccmt) = (type_of ppm, type_of ccm);
+  val ii = Sign.typ_match @{theory} (ppmt, cct) (Vartab.empty);
+  val ii = Sign.typ_match @{theory} (ppt, cct) (Vartab.empty);
+*}
+.
+  val pat = Drule.strip_imp_concl (cprop_of thm)
+  val insts = Thm.match (pat, concl)
+
+apply (tactic {* instantiate_tac @{thm RES_FORALL_RSP} @{context} 1 *})
+thm RES_FORALL_RSP
+apply (rule_tac RES_FORALL_RSP)
+
 prefer 2
 (* ABS_REP_RSP *)
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
diff -r 53277fbb2dba -r 0288dd5b7ed4 QuotScript.thy
--- a/QuotScript.thy	Thu Oct 22 11:43:12 2009 +0200
+++ b/QuotScript.thy	Thu Oct 22 13:45:48 2009 +0200
@@ -473,5 +473,11 @@
   shows "Ex P \<Longrightarrow> Bex R Q"
   using a by (metis COMBC_def Collect_def Collect_mem_eq)
 
+lemma RES_FORALL_RSP:
+  assumes a: "QUOTIENT R abs rep"
+  shows "\<And>f g. (R ===> (op =)) f g ==>
+        (Ball (Respects R) f = Ball (Respects R) g)"
+  sorry
+
 end