# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1254239178 -7200
# Node ID ec5fbe7ab427d5a5fc3f79213eead2e9b5259a61
# Parent  b2ab3ba388a06064551fc5c2484c69c081620eb6
First version of handling of the universal quantifier

diff -r b2ab3ba388a0 -r ec5fbe7ab427 QuotMain.thy
--- a/QuotMain.thy	Tue Sep 29 15:58:14 2009 +0200
+++ b/QuotMain.thy	Tue Sep 29 17:46:18 2009 +0200
@@ -829,6 +829,10 @@
                 @{const_name "card1"}]
 *}
 
+ML {* val qty = @{typ "'a fset"} *}
+ML {* val tt = Type ("fun", [Type ("fun", [qty, @{typ "prop"}]), @{typ "prop"}]) *}
+ML {* val fall = Const(@{const_name all}, tt) *}
+
 ML {*
 fun build_goal ctxt thm constructors rty qty mk_rep mk_abs =
   let
@@ -844,6 +848,9 @@
         if fastype_of t = rty then mk_rep_abs t else t
       end;
 
+    fun is_all (Const ("all", Type("fun", [Type("fun", [ty, _]), _]))) = ty = rty
+      | is_all _ = false;
+
     fun build_aux ctxt1 tm =
       let
         val (head, args) = Term.strip_comb tm;
@@ -867,9 +874,13 @@
               val rec_term = build_aux ctxt2 t';
             in Term.lambda_name (x, v) rec_term end
         | _ =>
-            if is_constructor head then
+            if is_all head then (* I assume that we never lift 'prop' since it is not of sort type *)
+              list_comb (fall, args')
+            else if is_constructor head then
               maybe_mk_rep_abs (list_comb (head, map maybe_mk_rep_abs args'))
-            else maybe_mk_rep_abs (list_comb (head, args')))
+            else
+              maybe_mk_rep_abs (list_comb (head, args'))
+        )
       end;
 
     val concl2 = Thm.prop_of thm;
@@ -1095,7 +1106,6 @@
       build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs
     )
 *}
-term all
 ML {*
   val cgoal = 
     Toplevel.program (fn () =>
@@ -1142,13 +1152,13 @@
 local_setup {* lift_theorem_fset @{binding "leqi4_lift"} @{thm list_eq.intros(4)} *}
 local_setup {* lift_theorem_fset @{binding "leqi5_lift"} @{thm list_eq.intros(5)} *}
 local_setup {* lift_theorem_fset @{binding "m2_lift"} @{thm m2} *}
-local_setup {* lift_theorem_fset @{binding "card_suc"} @{thm card1_suc} *}
+(*local_setup {* lift_theorem_fset @{binding "card_suc"} @{thm card1_suc} *}*)
 
 thm m1_lift
 thm leqi4_lift
 thm leqi5_lift
 thm m2_lift
-thm card_suc
+(*thm card_suc*)
 
 thm leqi4_lift
 ML {*
@@ -1167,6 +1177,7 @@
   )
 *}
 
+(*
 thm card_suc
 ML {*
   val (nam, typ) = (hd (tl (Term.add_vars (term_of (#prop (crep_thm @{thm card_suc}))) [])))
@@ -1183,7 +1194,7 @@
     )
   )
 *}
-
+*)
 
 
 
@@ -1196,8 +1207,12 @@
 ML {*
   val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs
 *}
+ML {* term_of @{cpat "all"} *}
 ML {*
-  val cgoal = cterm_of @{theory} goal
+  val cgoal = 
+    Toplevel.program (fn () =>
+      cterm_of @{theory} goal
+    );
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)
 *}
 ML {* @{term "\<exists>x. P x"} *}