(*  Title       : HOL/Real/Hyperreal/fuf.ml
    ID          : $Id: fuf.ML,v 1.1 1999/08/16 16:41:08 paulson Exp $
    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.
*)

exception FUFempty;

fun get_fuf_hyps [] zs = zs
|   get_fuf_hyps (x::xs) zs = 
        case (concl_of x) of 
        (_ $ (Const ("Not",_) $ (Const ("op :",_) $ _ $
             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);

(*---------------------------------------------------------------  
   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 (fclaset,fsimpset) i = METAHYPS(fn prems =>
                    (rtac ((Intprems (get_fuf_hyps prems [])) RS
                           FreeUltrafilterNat_subset) 1) THEN 
                    auto_tac (fclaset,fsimpset)) i;

(*---------------------------------------------------------------  
   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 (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;

(*---------------------------------------------------------------  
  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 (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;