--- a/FSet.thy	Wed Dec 02 12:07:54 2009 +0100
+++ b/FSet.thy	Wed Dec 02 14:11:46 2009 +0100
@@ -333,6 +333,8 @@
 apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *})
 done
 
+ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *}
+
 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"
 apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *})
 done
@@ -343,7 +345,6 @@
 
 lemma cheat: "P" sorry
 
-ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *}
 
 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *})
@@ -396,6 +397,28 @@
 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 done
 
+lemma list_induct_part:
+  assumes a: "P (x :: 'a list) ([] :: 'c list)"
+  assumes b: "\<And>e t. P x t \<Longrightarrow> P x (e # t)"
+  shows "P x l"
+  apply (rule_tac P="P x" in list.induct)
+  apply (rule a)
+  apply (rule b)
+  apply (assumption)
+  done
+
+lemma "P (x :: 'a list) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
+apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *})
+done
+
+lemma "P (x :: 'a fset) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
+apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *})
+done
+
+lemma "P (x :: 'a fset) ([] :: 'c list) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (e # t)) \<Longrightarrow> P x l"
+apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *})
+done
+
 quotient_def
   fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
 where
@@ -431,115 +454,6 @@
 apply (tactic {* lift_tac_fset @{context} @{thm list.cases(2)} 1 *})
 done
 
-lemma list_induct_part:
-  assumes a: "P (x :: 'a list) ([] :: 'c list)"
-  assumes b: "\<And>e t. P x t \<Longrightarrow> P x (e # t)"
-  shows "P x l"
-  apply (rule_tac P="P x" in list.induct)
-  apply (rule a)
-  apply (rule b)
-  apply (assumption)
-  done
-
-ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *}
+thm all_prs
 
-(* Construction site starts here *)
-lemma "P (x :: 'a list) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
-apply (tactic {* procedure_tac @{context} @{thm list_induct_part} 1 *})
-apply (tactic {* regularize_tac @{context} [rel_eqv] 1 *})
-prefer 2
-apply (tactic {* clean_tac @{context} [quot] defs 1 *})
-apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
-apply (rule FUN_QUOTIENT)
-apply (rule FUN_QUOTIENT)
-apply (rule IDENTITY_QUOTIENT)
-apply (rule FUN_QUOTIENT)
-apply (rule QUOTIENT_fset)
-apply (rule IDENTITY_QUOTIENT)
-apply (rule IDENTITY_QUOTIENT)
-apply (rule IDENTITY_QUOTIENT)
-prefer 2 apply(tactic{* quot_true_tac @{context} (snd o dest_comb) 1*})
-prefer 2 apply(tactic{* quot_true_tac @{context} (fst o dest_comb) 1*})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
-apply (rule IDENTITY_QUOTIENT)
-apply (rule FUN_QUOTIENT)
-apply (rule QUOTIENT_fset)
-apply (rule IDENTITY_QUOTIENT)
-prefer 2 apply(tactic{* quot_true_tac @{context} (snd o dest_comb) 1*})
-prefer 2 apply(tactic{* quot_true_tac @{context} (fst o dest_comb) 1*})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *})
-apply (rule IDENTITY_QUOTIENT)
-apply (rule FUN_QUOTIENT)
-apply (rule QUOTIENT_fset)
-apply (rule IDENTITY_QUOTIENT)
-prefer 2 apply(tactic{* quot_true_tac @{context} (snd o dest_comb) 1*})
-prefer 2 apply(tactic{* quot_true_tac @{context} (fst o dest_comb) 1*})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply assumption
-apply (rule refl)
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply assumption
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *})
-apply (rule IDENTITY_QUOTIENT)
-apply (rule FUN_QUOTIENT)
-apply (rule QUOTIENT_fset)
-apply (rule IDENTITY_QUOTIENT)
-prefer 2 apply(tactic{* quot_true_tac @{context} (snd o dest_comb) 1*})
-prefer 2 apply(tactic{* quot_true_tac @{context} (fst o dest_comb) 1*})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply assumption
-apply (rule refl)
-apply (tactic {* REPEAT_ALL_NEW (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *})
-apply (rule IDENTITY_QUOTIENT)
-apply (rule FUN_QUOTIENT)
-apply (rule QUOTIENT_fset)
-apply (rule IDENTITY_QUOTIENT)
-prefer 2 apply(tactic{* quot_true_tac @{context} (snd o dest_comb) 1*})
-prefer 2 apply(tactic{* quot_true_tac @{context} (fst o dest_comb) 1*})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-done
-
-ML {* #quot_thm (hd (quotdata_dest @{theory})) *}
-print_quotients
-thm QUOTIENT_fset
 end

--- a/QuotMain.thy	Wed Dec 02 12:07:54 2009 +0100
+++ b/QuotMain.thy	Wed Dec 02 14:11:46 2009 +0100
@@ -875,6 +875,33 @@
 *}
 
 ML {*
+val APPLY_RSP_TAC' =
+  Subgoal.FOCUS (fn {concl, asms, context,...} =>
+    case ((HOLogic.dest_Trueprop (term_of concl))) of
+       ((R2 $ (f $ x) $ (g $ y))) =>
+          let
+            val (asmf, asma) = find_qt_asm (map term_of asms);
+          in
+            if (fastype_of asmf) = (fastype_of f) then no_tac else let
+              val ty_a = fastype_of x;
+              val ty_b = fastype_of asma;
+              val ty_c = range_type (type_of f);
+              val ty_d = range_type (type_of asmf);
+              val thy = ProofContext.theory_of context;
+              val ty_inst = map (fn x => SOME (ctyp_of thy x)) [ty_a, ty_b, ty_c, ty_d];
+              val [R2, f, g, x, y] = map (cterm_of thy) [R2, f, g, x, y];
+              val t_inst = [NONE, NONE, NONE, SOME R2, NONE, NONE, SOME f, SOME g, SOME x, SOME y];
+              val thm = Drule.instantiate' ty_inst t_inst @{thm APPLY_RSP}
+              (*val _ = tracing (Syntax.string_of_term @{context} (prop_of thm))*)
+            in
+              rtac thm 1
+            end
+          end
+     | _ => no_tac)
+*}
+
+
+ML {*
 fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
 *}
 
@@ -1019,7 +1046,8 @@
   (FIRST' [
     (* "cong" rule of the of the relation / transitivity*)
     (* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *)
-    NDT ctxt "1" (resolve_tac trans2),
+    NDT ctxt "1" (resolve_tac trans2 THEN' RANGE [
+      quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]),
 
     (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *)
     NDT ctxt "2" (lambda_rsp_tac THEN' quot_true_tac ctxt unlam),
@@ -1049,7 +1077,7 @@
                   THEN' (RANGE [SOLVES' (quotient_tac ctxt quot_thms)]))),
 
     (* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP   provided type of t needs lifting *)
-    NDT ctxt "A" (APPLY_RSP_TAC rty ctxt THEN' 
+    NDT ctxt "A" (APPLY_RSP_TAC' ctxt THEN'
                 (RANGE [SOLVES' (quotient_tac ctxt quot_thms), SOLVES' (quotient_tac ctxt quot_thms),
                         quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),