1 (* Title : HOL/Real/Hyperreal/fuf.ML
3 Author : Jacques D. Fleuriot
4 Copyright : 1998 University of Cambridge
5 1999 University of Edinburgh
7 Simple tactics to help proofs involving our free ultrafilter
8 (FreeUltrafilterNat). We rely on the fact that filters satisfy the
9 finite intersection property.
16 fun get_fuf_hyps [] zs = zs
17 | get_fuf_hyps (x::xs) zs =
19 (_ $ (Const ("Not",_) $ (Const ("op :",_) $ _ $
20 Const ("HyperDef.FreeUltrafilterNat",_)))) => get_fuf_hyps xs
21 ((x RS FreeUltrafilterNat_Compl_mem)::zs)
22 |(_ $ (Const ("op :",_) $ _ $
23 Const ("HyperDef.FreeUltrafilterNat",_))) => get_fuf_hyps xs (x::zs)
24 | _ => get_fuf_hyps xs zs;
26 fun inter_prems [] = raise FUFempty
28 | inter_prems (x::y::ys) =
29 inter_prems (([x,y] MRS FreeUltrafilterNat_Int) :: ys);
33 (*---------------------------------------------------------------
34 solves goals of the form
35 [| A1: FUF; A2: FUF; ...; An: FUF |] ==> B : FUF
36 where A1 Int A2 Int ... Int An <= B
37 ---------------------------------------------------------------*)
39 fun fuf_tac css i = METAHYPS(fn prems =>
40 (rtac ((inter_prems (get_fuf_hyps prems [])) RS
41 FreeUltrafilterNat_subset) 1) THEN
44 fun Fuf_tac i = fuf_tac (clasimpset ()) i;
47 (*---------------------------------------------------------------
48 solves goals of the form
49 [| A1: FUF; A2: FUF; ...; An: FUF |] ==> P
50 where A1 Int A2 Int ... Int An <= {} since {} ~: FUF
51 (i.e. uses fact that FUF is a proper filter)
52 ---------------------------------------------------------------*)
54 fun fuf_empty_tac css i = METAHYPS (fn prems =>
55 rtac ((inter_prems (get_fuf_hyps prems [])) RS
56 (FreeUltrafilterNat_subset RS (FreeUltrafilterNat_empty RS notE))) 1
59 fun Fuf_empty_tac i = fuf_empty_tac (clasimpset ()) i;
62 (*---------------------------------------------------------------
63 In fact could make this the only tactic: just need to
64 use contraposition and then look for empty set.
65 ---------------------------------------------------------------*)
67 fun ultra_tac css i = rtac ccontr i THEN fuf_empty_tac css i;
68 fun Ultra_tac i = ultra_tac (clasimpset ()) i;