diff -r 50219e796e05 -r de944fcd6a05 QuotMain.thy
--- a/QuotMain.thy	Sat Oct 17 12:44:58 2009 +0200
+++ b/QuotMain.thy	Sat Oct 17 14:16:57 2009 +0200
@@ -1236,12 +1236,72 @@
 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_tac APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"])
+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>)"])
+(* 3: ho_respects *)
+prefer 4
+(* ABS_REP_RSP *)
+apply (rule REP_ABS_RSP(1)[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id"])
+prefer 2
+(* LAMBDA_RSP *)
+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 *)
+apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
+(* REFL_TAC *)
+apply (simp)
+(* APPLY_RSP *)
+apply (rule APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"])
+prefer 3
+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 4
-apply (rule list_eq_refl )
+apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"])
+prefer 2
+(* FIRST_ASSUM MATCH_ACCEPT_TAC *)
+apply (assumption)
+prefer 5
+(* MK_COMB_TAC *)
+apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
+(* REFL_TAC *)
+apply (simp)
+(* 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"])
+prefer 3
+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 4
+apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"])
+prefer 2
+(* APPLY_RSP *)
+thm APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op \<approx>" "ABS_fset" "REP_fset" ]
 
+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"] )
+prefer 3
+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"])
+(* 3: CONS respects *)
+prefer 3
+apply (simp only: FUN_REL.simps)
+apply (rule allI)
+apply (rule allI)
+apply (rule impI)
+apply (rule allI)
+apply (rule allI)
+apply (rule impI)
+apply (simp)
+thm cons_preserves
+apply (rule cons_preserves)
+apply (assumption)
+prefer 3
+apply (simp)
 sorry
 
 thm list.recs(2)