# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1255100745 -7200
# Node ID fdaf1466daf0ccf9d3990470d33a6ec1723e2af0
# Parent  4efc9e6661a416ebc9609ad990169001837a25ef
Further experiments with proving induction manually

diff -r 4efc9e6661a4 -r fdaf1466daf0 QuotMain.thy
--- a/QuotMain.thy	Fri Oct 09 15:03:43 2009 +0200
+++ b/QuotMain.thy	Fri Oct 09 17:05:45 2009 +0200
@@ -1102,25 +1102,28 @@
 term "f ===> g"
 
 definition
-  "rfall p m = (\<forall>x. (p x \<longrightarrow> m x))"
+  "res_forall p m = (\<forall>x. (x \<in> p \<longrightarrow> m x))"
+
+definition
+  "res_exists p m = (\<exists>x. (x \<in> p \<and> m x))"
 
-term "ABS_fset"
-term "I"
+(* The definition is total??? *)
+definition
+  "x IN p ==> (res_abstract p m x = m x)"
 
-term "(REP_fset ---> I) ---> I"
-lemma "rfall (Respects ((op \<approx>) ===> (op =)))
+lemma "(res_forall (Respects ((op \<approx>) ===> (op =)))
          (((REP_fset ---> id) ---> id)
              (((ABS_fset ---> id) ---> id)
                (\<lambda>P.
                   (ABS_fset ---> id) ((REP_fset ---> id) P)
                     (REP_fset (ABS_fset [])) \<and>
-                  rfall (Respects (op \<approx>))
+                  res_forall (Respects (op \<approx>))
                     ((ABS_fset ---> id)
                        ((REP_fset ---> id)
                           (\<lambda>t.
                              ((ABS_fset ---> id)
                                ((REP_fset ---> id) P)
-                               (REP_fset (ABS_fset t))) -->
+                               (REP_fset (ABS_fset t))) \<longrightarrow>
                              (!h.
                                (ABS_fset ---> id)
                                  ((REP_fset ---> id) P)
@@ -1128,20 +1131,34 @@
                                     (ABS_fset
                                        (h #
                                             REP_fset
-                                              (ABS_fset t)))))))) -->
-                  rfall (Respects (op \<approx>))
+                                              (ABS_fset t)))))))) \<longrightarrow>
+                  res_forall (Respects (op \<approx>))
                     ((ABS_fset ---> id)
                        ((REP_fset ---> id)
                           (\<lambda>l.
                              (ABS_fset ---> id)
                                ((REP_fset ---> id) P)
-                               (REP_fset (ABS_fset l))))))))"
-
-apply (unfold rfall_def)
+                               (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))))"
+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 (unfold id_def)
 apply (simp add: FUN_MAP_I)
+apply (simp add:IN_RESPECTS)
 apply (simp add: QUOT_TYPE_I_fset.thm10)
-.
+apply (simp add:list_eq_refl)
+
+
+
+apply (simp add: QUOT_TYPE_I_fset.R_trans2)
+
+apply (rule ext)
+apply (simp add:QUOT_TYPE_I_fset.REP_ABS_rsp)
+apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *} )
+apply (simp add:cons_preserves)
+
+
 
 (*prove aaa: {* (Thm.term_of cgoal2) *}
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )