# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1256200680 -7200
# Node ID 9802d961344627755b2c121d2076f5fb28bf229a
# Parent  7cf1d7adfc5fc2d741d258cffc26836f77414e57
Got rid of instantiations in the proof

diff -r 7cf1d7adfc5f -r 9802d9613446 QuotMain.thy
--- a/QuotMain.thy	Thu Oct 22 06:51:27 2009 +0200
+++ b/QuotMain.thy	Thu Oct 22 10:38:00 2009 +0200
@@ -1030,15 +1030,22 @@
 prove list_induct_tr: trm_r
 apply (atomize(full))
 apply (simp only: id_def[symmetric])
-
 (* APPLY_RSP_TAC *)
-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 (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *})
+apply (rule FUN_QUOTIENT)
+apply (rule FUN_QUOTIENT)
+apply (rule QUOTIENT_fset)
+apply (rule IDENTITY_QUOTIENT)
+apply (rule IDENTITY_QUOTIENT)
 apply (rule IDENTITY_QUOTIENT)
-prefer 3
+prefer 2
 (* ABS_REP_RSP_TAC *)
-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
+apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *})
+apply (rule FUN_QUOTIENT)
+apply (rule FUN_QUOTIENT)
+apply (rule QUOTIENT_fset)
+apply (rule IDENTITY_QUOTIENT)
+apply (rule IDENTITY_QUOTIENT)
 (* LAMBDA_RES_TAC *)
 apply (simp only: FUN_REL.simps)
 apply (rule allI)
@@ -1057,27 +1064,30 @@
 (* REFL_TAC *)
 apply (simp)
 (* APPLY_RSP_TAC *)
-apply (rule APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"])
+apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *})
 apply (rule QUOTIENT_fset)
 apply (rule IDENTITY_QUOTIENT)
 apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *})
-prefer 2
+apply (rule FUN_QUOTIENT)
+apply (rule QUOTIENT_fset)
+apply (rule IDENTITY_QUOTIENT)
 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 (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *})
 apply (rule QUOTIENT_fset)
 (* MINE *)
 apply (rule list_eq_refl )
-prefer 2
-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 (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *})
+apply (rule FUN_QUOTIENT)
+apply (rule QUOTIENT_fset)
+apply (rule IDENTITY_QUOTIENT)
 apply (rule IDENTITY_QUOTIENT)
-(* 2: ho_respects *)
-prefer 3
+(* TODO don't know how to handle ho_respects *)
+prefer 2
 (* ABS_REP_RSP *)
-apply (rule REP_ABS_RSP(1)[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id"])
-prefer 2
+apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *})
+apply (rule FUN_QUOTIENT)
+apply (rule QUOTIENT_fset)
+apply (rule IDENTITY_QUOTIENT)
 (* LAMBDA_RSP *)
 apply (simp only: FUN_REL.simps)
 apply (rule allI)
@@ -1090,19 +1100,19 @@
 (* REFL_TAC *)
 apply (simp)
 (* APPLY_RSP *)
-apply (rule APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"])
+apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *})
 apply (rule QUOTIENT_fset)
 apply (rule IDENTITY_QUOTIENT)
-apply (rule REP_ABS_RSP(1)[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id"])
-prefer 2
+apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *})
+apply (rule FUN_QUOTIENT)
+apply (rule QUOTIENT_fset)
+apply (rule IDENTITY_QUOTIENT)
 (* MINE *)
 apply (simp only: FUN_REL.simps)
-prefer 2
-apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"])
+apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *})
 apply (rule QUOTIENT_fset)
 (* FIRST_ASSUM MATCH_ACCEPT_TAC *)
 apply (assumption)
-prefer 2
 (* MK_COMB_TAC *)
 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
 (* REFL_TAC *)
@@ -1110,23 +1120,26 @@
 (* W(C (curry op THEN) (G... *)
 apply (rule ext)
 (* APPLY_RSP *)
-apply (rule APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"])
+apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *})
+apply (rule QUOTIENT_fset)
+apply (rule IDENTITY_QUOTIENT)
+apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *})
+apply (rule FUN_QUOTIENT)
 apply (rule QUOTIENT_fset)
 apply (rule IDENTITY_QUOTIENT)
-apply (rule REP_ABS_RSP(1)[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id"])
-prefer 2
 apply (simp only: FUN_REL.simps)
-prefer 2
-apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"])
+apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *})
 apply (rule QUOTIENT_fset)
 (* APPLY_RSP *)
-apply (tactic {* instantiate_tac @{thm APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op \<approx>" "ABS_fset" "REP_fset"]} @{context} 1 *})
+apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *})
 apply (rule QUOTIENT_fset)
 apply (rule QUOTIENT_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 (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *})
 apply (rule IDENTITY_QUOTIENT)
+apply (rule FUN_QUOTIENT)
+apply (rule QUOTIENT_fset)
+apply (rule QUOTIENT_fset)
 (* CONS respects *)
-prefer 2
 apply (simp add: FUN_REL.simps)
 apply (rule allI)
 apply (rule allI)
@@ -1134,19 +1147,21 @@
 apply (rule impI)
 apply (rule cons_preserves)
 apply (assumption)
-prefer 2
 apply (simp)
-prefer 2
-apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"])
+apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *})
 apply (rule QUOTIENT_fset)
 apply (assumption)
-prefer 8
-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 (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *})
+apply (rule FUN_QUOTIENT)
+apply (rule QUOTIENT_fset)
+apply (rule IDENTITY_QUOTIENT)
 apply (rule IDENTITY_QUOTIENT)
-prefer 3
-apply (rule REP_ABS_RSP(1)[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id"])
 prefer 2
+apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *})
+apply (rule FUN_QUOTIENT)
+apply (rule QUOTIENT_fset)
+apply (rule IDENTITY_QUOTIENT)
 sorry
 
 prove list_induct_t: trm