--- a/QuotMain.thy	Sat Oct 17 12:19:06 2009 +0200
+++ b/QuotMain.thy	Sat Oct 17 12:31:48 2009 +0200
@@ -1217,75 +1217,27 @@
 (* REFL_TAC *)
 apply (simp)
 (* APPLY_RSP_TAC *)
-ML_prf {* Isar.goal () *}
-ML_prf {* val t = Thm.lift_rule (hd (cprems_of (Isar.goal ()))) @{thm "APPLY_RSP_I2" } *}
-ML_prf {*
-  val (tc') = (Logic.strip_assums_concl (prop_of t));
-  val ps = Logic.strip_params (prop_of t)
-  val tt = Term.list_abs (ps, tc')
-  val ct = cterm_of @{theory} tt
-*}
-ML_prf {*
-  val goal = hd (prems_of (Isar.goal ()))
-  val goalc = Logic.strip_assums_concl goal
-*}
-ML_prf {*
-  val goalct = cterm_of @{theory} (hd ( prems_of (Isar.goal ())))
-*}
-
-ML_prf {*
-  val ps = Logic.strip_params goal
-  val goal' = cterm_of @{theory} (Term.list_abs (ps, goalc))
-  val goal'' = cterm_of @{theory} (Term.subst_bounds ((map Free ps), goalc))
-*}
-ML_prf {* ct; goal'' *}
-
-ML_prf {* val nlct = cterm_of @{theory} (concl_of @{thm "APPLY_RSP_I2" }) *}
-
-ML_prf {* Thm.match (nlct, goal'') *}
-ML_prf {* ct *}
-
-
-(*apply (tactic {*Cong_Tac.cong_tac @{thm APPLY_RSP_I2} 1 *}) *)
-ML_prf {* t *}
-ML_prf {*
-  val man_inst =
-    Drule.instantiate' [SOME @{ctyp 'a}, SOME @{ctyp bool}] 
-      [
-       SOME @{cterm "\<lambda>(x\<Colon>'a list \<Rightarrow> bool) (y\<Colon>'a list \<Rightarrow> bool). x"},
-       SOME @{cterm "\<lambda>(x\<Colon>'a list \<Rightarrow> bool) (y\<Colon>'a list \<Rightarrow> bool). (ABS_fset ---> id) ((REP_fset ---> id) y)"},
-       SOME @{cterm "\<lambda>(x\<Colon>'a list \<Rightarrow> bool) (y\<Colon>'a list \<Rightarrow> bool). ([]::'a list)"},
-       SOME @{cterm "\<lambda>(x\<Colon>'a list \<Rightarrow> bool) (y\<Colon>'a list \<Rightarrow> bool). (REP_fset (ABS_fset ([]::'a list)))"}
-      ] t
-*}
-ML_prf {*
-  val (tc') = (Logic.strip_assums_concl (prop_of man_inst));
-  val ps = Logic.strip_params (prop_of man_inst)
-  val tt = Term.list_abs (ps, tc')
-  val ct = cterm_of @{theory} tt
-*}
-ML_prf {*
-  fun dest_cbinop t =
-    let
-      val (t2, rhs) = Thm.dest_comb t;
-      val (bop, lhs) = Thm.dest_comb t2;
-    in
-      (bop, (lhs, rhs))
-    end
-*}
-
-
-ML_prf {* val (a, b) = (snd (Thm.dest_abs NONE ct), (snd (Thm.dest_abs NONE goal'))) *}
-ML_prf {* val (a, b) = (snd (Thm.dest_abs NONE a), (snd (Thm.dest_abs NONE b))) *}
-ML_prf {* val (a, b) = (snd (Thm.dest_comb a), snd (Thm.dest_comb b)) *}
-ML_prf {* val (a, b) = ((fst o snd) (dest_cbinop a), (fst o snd) (dest_cbinop b)) *}
-ML_prf {* (term_of a, term_of b) *}
-ML_prf {* (Envir.beta_norm (term_of a), term_of b) *}
-ML_prf {* Thm.beta_conv *}
-ML_prf man_inst
-thm APPLY_RSP_I2
-apply (tactic {* compose_tac (false,man_inst,0) 1 *})
-
+thm APPLY_RSP
+apply (rule_tac APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"])
+(* MINE *)
+apply (rule QUOTIENT_fset)
+prefer 3
+(* ABS_REP_RSP *)
+apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"])
+(* MINE *)
+apply (rule QUOTIENT_fset)
+(* MINE *)
+apply (rule list_eq_refl )
+prefer 2
+(* ABS_REP_RSP *)
+apply (rule REP_ABS_RSP(1)[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id"])
+prefer 2
+(* MINE *)
+apply (simp only: FUN_REL.simps)
+prefer 3
+(* APPLY_RSP *)
+thm APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"]
+apply (rule APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"])
 sorry
 
 thm list.recs(2)