src/HOL/Hyperreal/fuf.ML

separation of HOL-Hyperreal from HOL-Real

(*  Title       : HOL/Real/Hyperreal/fuf.ML
    ID          : $Id$
    Author      : Jacques D. Fleuriot
    Copyright   : 1998  University of Cambridge
                  1999  University of Edinburgh

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
        (_ $ (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 inter_prems [] = raise FUFempty
|   inter_prems [x] = x
|   inter_prems (x::y::ys) =
      inter_prems (([x,y] MRS FreeUltrafilterNat_Int) :: ys);

in

(*---------------------------------------------------------------
   solves goals of the form
    [| A1: FUF; A2: FUF; ...; An: FUF |] ==> B : FUF
   where A1 Int A2 Int ... Int An <= B
 ---------------------------------------------------------------*)

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 i = fuf_tac (clasimpset ()) 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)
 ---------------------------------------------------------------*)

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 i = fuf_empty_tac (clasimpset ()) i;


(*---------------------------------------------------------------
  All in one -- not really needed.
 ---------------------------------------------------------------*)

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;


(*---------------------------------------------------------------
   In fact could make this the only tactic: just need to
   use contraposition and then look for empty set.
 ---------------------------------------------------------------*)

fun ultra_tac css i = rtac ccontr i THEN fuf_empty_tac css i;
fun Ultra_tac i = ultra_tac (clasimpset ()) i;

end;