# HG changeset patch
# User wenzelm
# Date 972401668 -7200
# Node ID ef2df4ca9da1a66444eb9a884337f7417793b8b7
# Parent  ec30a7d15f76c2d8e611ef1c98d914f6f1357196
tuned;

diff -r ec30a7d15f76 -r ef2df4ca9da1 src/HOL/Real/Hyperreal/fuf.ML
--- a/src/HOL/Real/Hyperreal/fuf.ML	Tue Oct 24 10:48:51 2000 +0200
+++ b/src/HOL/Real/Hyperreal/fuf.ML	Tue Oct 24 17:34:28 2000 +0200
@@ -1,82 +1,78 @@
-(*  Title       : HOL/Real/Hyperreal/fuf.ml
+(*  Title       : HOL/Real/Hyperreal/fuf.ML
     ID          : $Id$
     Author      : Jacques D. Fleuriot
     Copyright   : 1998  University of Cambridge
                   1999  University of Edinburgh
-    Description : Simple tactics to help proofs involving our 
-                  free ultrafilter (FreeUltrafilterNat). We rely
-                  on the fact that filters satisfy the  finite 
-                  intersection property.
+
+Simple tactics to help proofs involving our free ultrafilter
+(FreeUltrafilterNat). We rely on the fact that filters satisfy the
+finite intersection property.
 *)
 
+local
+
 exception FUFempty;
 
 fun get_fuf_hyps [] zs = zs
-|   get_fuf_hyps (x::xs) zs = 
-        case (concl_of x) of 
+|   get_fuf_hyps (x::xs) zs =
+        case (concl_of x) of
         (_ $ (Const ("Not",_) $ (Const ("op :",_) $ _ $
-             Const ("HyperDef.FreeUltrafilterNat",_)))) =>  get_fuf_hyps xs 
+             Const ("HyperDef.FreeUltrafilterNat",_)))) =>  get_fuf_hyps xs
                                               ((x RS FreeUltrafilterNat_Compl_mem)::zs)
        |(_ $ (Const ("op :",_) $ _ $
              Const ("HyperDef.FreeUltrafilterNat",_)))  =>  get_fuf_hyps xs (x::zs)
        | _ => get_fuf_hyps xs zs;
 
-fun Intprems [] = raise FUFempty
-|   Intprems [x] = x
-|   Intprems (x::y::ys) = 
-      Intprems (([x,y] MRS FreeUltrafilterNat_Int) :: ys);
+fun inter_prems [] = raise FUFempty
+|   inter_prems [x] = x
+|   inter_prems (x::y::ys) =
+      inter_prems (([x,y] MRS FreeUltrafilterNat_Int) :: ys);
 
-(*---------------------------------------------------------------  
-   solves goals of the form 
-    [| A1: FUF; A2: FUF; ...; An: FUF |] ==> B : FUF   
-   where A1 Int A2 Int ... Int An <= B 
+in
+
+(*---------------------------------------------------------------
+   solves goals of the form
+    [| A1: FUF; A2: FUF; ...; An: FUF |] ==> B : FUF
+   where A1 Int A2 Int ... Int An <= B
  ---------------------------------------------------------------*)
 
-val Fuf_tac = METAHYPS(fn prems =>
-                    (rtac ((Intprems (get_fuf_hyps prems [])) RS
-                           FreeUltrafilterNat_subset) 1) THEN 
-                    Auto_tac);
+fun fuf_tac css i = METAHYPS(fn prems =>
+                    (rtac ((inter_prems (get_fuf_hyps prems [])) RS
+                           FreeUltrafilterNat_subset) 1) THEN
+                    auto_tac css) i;
 
-fun fuf_tac (fclaset,fsimpset) i = METAHYPS(fn prems =>
-                    (rtac ((Intprems (get_fuf_hyps prems [])) RS
-                           FreeUltrafilterNat_subset) 1) THEN 
-                    auto_tac (fclaset,fsimpset)) i;
+fun Fuf_tac i = fuf_tac (clasimpset ()) i;
+
 
-(*---------------------------------------------------------------  
-   solves goals of the form 
+(*---------------------------------------------------------------
+   solves goals of the form
     [| A1: FUF; A2: FUF; ...; An: FUF |] ==> P
    where A1 Int A2 Int ... Int An <= {} since {} ~: FUF
    (i.e. uses fact that FUF is a proper filter)
  ---------------------------------------------------------------*)
 
-val Fuf_empty_tac = METAHYPS(fn prems => 
-                    (rtac ((Intprems (get_fuf_hyps prems [])) RS
-                           (FreeUltrafilterNat_subset RS 
-                           (FreeUltrafilterNat_empty RS notE))) 1) 
-                     THEN Auto_tac);
+fun fuf_empty_tac css i = METAHYPS (fn prems =>
+  rtac ((inter_prems (get_fuf_hyps prems [])) RS
+    (FreeUltrafilterNat_subset RS (FreeUltrafilterNat_empty RS notE))) 1
+                     THEN auto_tac css) i;
 
-fun fuf_empty_tac (fclaset,fsimpset) i = METAHYPS(fn prems => 
-                    (rtac ((Intprems (get_fuf_hyps prems [])) RS
-                           (FreeUltrafilterNat_subset RS 
-                          (FreeUltrafilterNat_empty RS notE))) 1) 
-                     THEN auto_tac (fclaset,fsimpset)) i;
+fun Fuf_empty_tac i = fuf_empty_tac (clasimpset ()) i;
 
-(*---------------------------------------------------------------  
+
+(*---------------------------------------------------------------
   All in one -- not really needed.
  ---------------------------------------------------------------*)
 
-fun Fuf_auto_tac i = SOLVE (Fuf_empty_tac i) ORELSE TRY(Fuf_tac i);
+fun fuf_auto_tac css i = SOLVE (fuf_empty_tac css i) ORELSE TRY (fuf_tac css i);
+fun Fuf_auto_tac i = fuf_auto_tac (clasimpset ()) i;
 
-fun fuf_auto_tac (fclaset,fsimpset) i = 
-     SOLVE (fuf_empty_tac (fclaset,fsimpset) i) 
-     ORELSE TRY(fuf_tac (fclaset,fsimpset) i);
 
-(*---------------------------------------------------------------  
+(*---------------------------------------------------------------
    In fact could make this the only tactic: just need to
    use contraposition and then look for empty set.
  ---------------------------------------------------------------*)
 
-fun Ultra_tac i = rtac ccontr i THEN Fuf_empty_tac i;
-fun ultra_tac (fclaset,fsimpset) i = rtac ccontr i THEN 
-              fuf_empty_tac (fclaset,fsimpset) i;
+fun ultra_tac css i = rtac ccontr i THEN fuf_empty_tac css i;
+fun Ultra_tac i = ultra_tac (clasimpset ()) i;
 
+end;