# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1255357889 -7200
# Node ID cb74afa437d72fe108dac741b84a0e674d2f481b
# Parent  1a0b771051c7ede2d42a4d834cc87547744b251a
Bounded quantifier

diff -r 1a0b771051c7 -r cb74afa437d7 QuotMain.thy
--- a/QuotMain.thy	Mon Oct 12 15:47:27 2009 +0200
+++ b/QuotMain.thy	Mon Oct 12 16:31:29 2009 +0200
@@ -1138,36 +1138,20 @@
     );
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)
 *}
-ML {* @{term "\<exists>x. P x"} *}
-
-term "f ---> g"
-term "f ===> g"
-
-definition
-  "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))"
-
-(* The definition is total??? *)
-definition
-  "x IN p ==> (res_abstract p m x = m x)"
+  "x IN p ==> (Babs p m x = m x)"
 
 print_theorems
-thm res_abstract_def
+thm Babs_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 =)))
+lemma "(Ball (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>
-                  res_forall (Respects (op \<approx>))
+                  Ball (Respects (op \<approx>))
                     ((ABS_fset ---> id)
                        ((REP_fset ---> id)
                           (\<lambda>t.
@@ -1182,7 +1166,7 @@
                                        (h #
                                             REP_fset
                                               (ABS_fset t)))))))) \<longrightarrow>
-                  res_forall (Respects (op \<approx>))
+                  Ball (Respects (op \<approx>))
                     ((ABS_fset ---> id)
                        ((REP_fset ---> id)
                           (\<lambda>l.
@@ -1190,13 +1174,13 @@
                                ((REP_fset ---> id) P)
                                (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)))"
+   = Ball (Respects ((op \<approx>) ===> (op =)))
+     (\<lambda>P. ((P []) \<and> (Ball (Respects (op \<approx>)) (\<lambda>t. P t \<longrightarrow> (\<forall>h. (P (h # t)))))) \<longrightarrow>
+     (Ball (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 (unfold Ball_def)
 apply (simp only: IN_RESPECTS)
 apply (simp only:list_eq_refl)
 apply (unfold id_def)