# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1256130110 -7200
# Node ID 1d0692e7ddd49501edf6de4358df3972e54d01c2
# Parent  ec772b461e26f4bbaf32331c17efc1a15803f9c9
Simplified proof more

diff -r ec772b461e26 -r 1d0692e7ddd4 QuotMain.thy
--- a/QuotMain.thy	Wed Oct 21 14:30:29 2009 +0200
+++ b/QuotMain.thy	Wed Oct 21 15:01:50 2009 +0200
@@ -1164,7 +1164,19 @@
   apply (metis)
   done
 
-ML {* val thm = @{thm list_induct_r} OF [li] *}
+ML {*
+fun instantiate_tac thm = (Subgoal.FOCUS (fn {concl, context, ...} =>
+let
+ val pat = cterm_of (ProofContext.theory_of context) (concl_of thm)
+ val insts = Thm.match (pat, concl)
+in
+ rtac (Drule.instantiate insts thm) 1
+end))
+*}
+
+
+
+ML {* val thm = @{thm list_induct_r} OF [atomize_thm @{thm list_induct_hol4}] *}
 ML {* val trm_r = build_repabs_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *}
 lemmas APPLY_RSP_I = APPLY_RSP[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id" "op =" "id" "id"]
 lemmas REP_ABS_RSP_I = REP_ABS_RSP(1)[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id"]
@@ -1178,33 +1190,18 @@
 apply (simp only: id_def[symmetric])
 
 (* APPLY_RSP_TAC *)
-ML_prf {*
-  val (_, gc') = Thm.dest_comb (Subgoal.focus @{context} 1 (Isar.goal ()) |> fst |> #concl)
-  val (_, tc') = Thm.dest_comb (cterm_of @{theory} (concl_of @{thm "APPLY_RSP_I" }))
-  val m = Thm.match (tc', gc')
-  val t2 = Drule.instantiate m @{thm "APPLY_RSP_I" }
- *}
-thm APPLY_RSP_I
-apply (tactic {* rtac t2 1 *})
+apply (tactic {* instantiate_tac @{thm APPLY_RSP[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id" "op =" "id" "id"]} @{context} 1 *})
 prefer 2
 apply (rule IDENTITY_QUOTIENT)
 prefer 3
 (* ABS_REP_RSP_TAC *)
-ML_prf {*
-  val (_, gc') = Thm.dest_comb (Subgoal.focus @{context} 1 (Isar.goal ()) |> fst |> #concl)
-  val (_, tc') = Thm.dest_comb (cterm_of @{theory} (concl_of @{thm "REP_ABS_RSP_I" }))
-  val m = Thm.match (tc', gc')
-  val t2 = Drule.instantiate m @{thm "REP_ABS_RSP_I" }
- *}
-apply (tactic {* rtac t2 1 *})
+apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id"]} @{context} 1 *})
 prefer 2
-
 (* LAMBDA_RES_TAC *)
 apply (simp only: FUN_REL.simps)
 apply (rule allI)
 apply (rule allI)
 apply (rule impI)
-
 (* MK_COMB_TAC *)
 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
 (* MK_COMB_TAC *)
@@ -1218,23 +1215,20 @@
 (* REFL_TAC *)
 apply (simp)
 (* APPLY_RSP_TAC *)
-apply (rule_tac 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"])
 apply (rule QUOTIENT_fset)
 apply (rule IDENTITY_QUOTIENT)
+apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *})
+prefer 2
+apply (simp only: FUN_REL.simps)
 prefer 2
 (* ABS_REP_RSP *)
 apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"])
 apply (rule QUOTIENT_fset)
 (* MINE *)
 apply (rule list_eq_refl )
-(* 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 2
-(* APPLY_RSP *)
-apply (rule_tac APPLY_RSP[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id" "op =" "id" "id" "Ball (Respects op \<approx>)" "Ball (Respects op \<approx>)"])
+apply (tactic {* instantiate_tac @{thm APPLY_RSP[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id" "op =" "id" "id"]} @{context} 1 *})
 prefer 2
 apply (rule IDENTITY_QUOTIENT)
 (* 2: ho_respects *)
@@ -1284,47 +1278,10 @@
 apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"])
 apply (rule QUOTIENT_fset)
 (* APPLY_RSP *)
-
-
-
-ML_prf {*
-  val goal = hd (prems_of (Isar.goal ()));
-  val goalc = Logic.strip_assums_concl goal
-  val ps = rev (map Free (Logic.strip_params goal));
-  val (_, gc') = Thm.dest_comb (cterm_of @{theory} (Term.subst_bounds (ps, goalc)));
-  val (_, tc') = Thm.dest_comb (cterm_of @{theory} (concl_of @{thm "APPLY_RSP_II" }))
-*}
-ML_prf fold
-ML_prf {*
-  val m = Thm.match (tc', gc')
-  val l = map (fst) (snd m);
-  val f_inst = map (term_of o snd) (snd m);
-  val f_abs = map (fold lambda ps) f_inst
-*}
-ML_prf {* val f_abs_c = map (cterm_of @{theory}) f_abs *}
-ML_prf {* val insts = l ~~ f_abs_c *}
-ML_prf {* val t = Thm.lift_rule (hd (cprems_of (Isar.goal ()))) @{thm "APPLY_RSP_II" } *}
-ML_prf {* Toplevel.program (fn () => cterm_instantiate insts t) *}
-
-
-
-
-.
-(*  FAILS: t2 = Drule.instantiate m @{thm "APPLY_RSP_II" }; rtac t2 1 *)
-(* Works but why does it take a string? *)
-ML_prf {*
-  val t_inst = snd m;
-  val t_insts = map (fn (a, b) => (fst (dest_Var (term_of a)), (Syntax.string_of_term @{context} (term_of b)))) t_inst
-  
-*}
-ML_prf dest_Var
-apply (tactic {* res_inst_tac @{context} [(("f",0),"op # h"),(("g",0),"op # h")] @{thm "APPLY_RSP_II" } 1 *})
-ML_prf induct_tac
-(*apply (rule_tac ?f="\<lambda>x. h # x" and ?g="\<lambda>x. h # x" in APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op \<approx>" "ABS_fset" "REP_fset"] )*)
-
+apply (tactic {* instantiate_tac @{thm APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op \<approx>" "ABS_fset" "REP_fset"]} @{context} 1 *})
 apply (rule QUOTIENT_fset)
 apply (rule QUOTIENT_fset)
-apply (rule_tac ?f="op #" and ?g="op #" in APPLY_RSP[of "op =" "id" "id" "op \<approx> ===> op \<approx>" "REP_fset ---> ABS_fset" "ABS_fset ---> REP_fset"])
+apply (tactic {* instantiate_tac @{thm APPLY_RSP[of "op =" "id" "id" "op \<approx> ===> op \<approx>" "REP_fset ---> ABS_fset" "ABS_fset ---> REP_fset"]} @{context} 1 *})
 apply (rule IDENTITY_QUOTIENT)
 (* CONS respects *)
 prefer 2
@@ -1337,6 +1294,10 @@
 apply (assumption)
 prefer 2
 apply (simp)
+prefer 2
+apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"])
+apply (rule QUOTIENT_fset)
+apply (assumption)
 sorry
 
 prove list_induct_t: trm