diff -r b441019d457d -r 25268329d3b7 QuotMain.thy
--- a/QuotMain.thy	Sat Oct 17 12:20:56 2009 +0200
+++ b/QuotMain.thy	Sat Oct 17 12:31:36 2009 +0200
@@ -1240,89 +1240,12 @@
 (* 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 {* val man_inst_norm_r = Drule.beta_eta_conversion (cprop_of man_inst) *}
-ML_prf {* val man_inst_norm = MetaSimplifier.rewrite_rule [man_inst_norm_r] man_inst *}
-ML_prf {*
-  val (tc') = (Logic.strip_assums_concl (prop_of man_inst_norm));
-  val ps = Logic.strip_params (prop_of man_inst_norm)
-  val tt = Term.list_abs (ps, tc')
-  val ct = cterm_of @{theory} tt
-*}
-ML_prf {* Thm.match (ct, goal') *}
-ML_prf {* PRIMSEQ *}
-ML_prf {* man_inst_norm *}
-apply (tactic {* compose_tac (false, man_inst_norm, 4) 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 *)
-thm REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"]
 apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"])
 (* MINE *)
 apply (rule QUOTIENT_fset)
@@ -1336,7 +1259,8 @@
 apply (simp only: FUN_REL.simps)
 prefer 3
 (* APPLY_RSP *)
-thm 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)