# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1255348711 -7200
# Node ID 0370493040f30708a67b9bdaa2b27c1de22d52b6
# Parent  fdaf1466daf0ccf9d3990470d33a6ec1723e2af0
Further with the manual proof

diff -r fdaf1466daf0 -r 0370493040f3 QuotMain.thy
--- a/QuotMain.thy	Fri Oct 09 17:05:45 2009 +0200
+++ b/QuotMain.thy	Mon Oct 12 13:58:31 2009 +0200
@@ -1111,6 +1111,14 @@
 definition
   "x IN p ==> (res_abstract p m x = m x)"
 
+print_theorems
+thm res_abstract_def
+
+(*TODO*)
+term "\<forall>x. x \<in> S \<longrightarrow> P x"
+term "\<forall>x \<in> S. P x"
+
+
 lemma "(res_forall (Respects ((op \<approx>) ===> (op =)))
          (((REP_fset ---> id) ---> id)
              (((ABS_fset ---> id) ---> id)
@@ -1138,16 +1146,26 @@
                           (\<lambda>l.
                              (ABS_fset ---> id)
                                ((REP_fset ---> id) P)
-                               (REP_fset (ABS_fset l)))))))))"
-term "  (\<forall>P. (((P []) \<and> (\<forall>t. (P t \<longrightarrow> (\<forall>h. P (h # t))))) \<longrightarrow> (\<forall>l. (P l))))"
+                               (REP_fset (ABS_fset l)))))))))
+
+   = res_forall (Respects ((op \<approx>) ===> (op =)))
+     (\<lambda>P. ((P []) \<and> (res_forall (Respects (op \<approx>)) (\<lambda>t. P t \<longrightarrow> (\<forall>h. (P (h # t)))))) \<longrightarrow>
+     (res_forall (Respects (op \<approx>)) (\<lambda>l. P l)))"
+term "(\<forall>P. (((P []) \<and> (\<forall>t. (P t \<longrightarrow> (\<forall>h. P (h # t))))) \<longrightarrow> (\<forall>l. (P l))))"
 thm LAMBDA_PRS1[symmetric]
 (*apply (simp only:LAMBDA_PRS1[symmetric] FUN_QUOTIENT IDENTITY_QUOTIENT QUOT_TYPE_I_fset.QUOTIENT)*)
 apply (unfold res_forall_def)
+apply (simp only: IN_RESPECTS)
+apply (simp only:list_eq_refl)
 apply (unfold id_def)
-apply (simp add: FUN_MAP_I)
+(*apply (simp only: FUN_MAP_I)*)
+apply (simp)
+apply (simp only: QUOT_TYPE_I_fset.thm10)
+apply (tactic {* foo_tac' @{context} 1 *})
+
+..
 apply (simp add:IN_RESPECTS)
-apply (simp add: QUOT_TYPE_I_fset.thm10)
-apply (simp add:list_eq_refl)
+