10751
|
1 |
(* Title : HOL/Real/Hyperreal/fuf.ML
|
|
2 |
ID : $Id$
|
|
3 |
Author : Jacques D. Fleuriot
|
|
4 |
Copyright : 1998 University of Cambridge
|
|
5 |
1999 University of Edinburgh
|
|
6 |
|
|
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.
|
|
10 |
*)
|
|
11 |
|
14299
|
12 |
val FreeUltrafilterNat_empty = thm "FreeUltrafilterNat_empty";
|
|
13 |
val FreeUltrafilterNat_subset = thm "FreeUltrafilterNat_subset";
|
|
14 |
val FreeUltrafilterNat_Compl_mem = thm "FreeUltrafilterNat_Compl_mem";
|
|
15 |
val FreeUltrafilterNat_Int = thm "FreeUltrafilterNat_Int";
|
|
16 |
|
10751
|
17 |
local
|
|
18 |
|
|
19 |
exception FUFempty;
|
|
20 |
|
|
21 |
fun get_fuf_hyps [] zs = zs
|
|
22 |
| get_fuf_hyps (x::xs) zs =
|
|
23 |
case (concl_of x) of
|
|
24 |
(_ $ (Const ("Not",_) $ (Const ("op :",_) $ _ $
|
17298
|
25 |
Const ("StarType.FreeUltrafilterNat",_)))) => get_fuf_hyps xs
|
10751
|
26 |
((x RS FreeUltrafilterNat_Compl_mem)::zs)
|
|
27 |
|(_ $ (Const ("op :",_) $ _ $
|
17298
|
28 |
Const ("StarType.FreeUltrafilterNat",_))) => get_fuf_hyps xs (x::zs)
|
10751
|
29 |
| _ => get_fuf_hyps xs zs;
|
|
30 |
|
|
31 |
fun inter_prems [] = raise FUFempty
|
|
32 |
| inter_prems [x] = x
|
|
33 |
| inter_prems (x::y::ys) =
|
|
34 |
inter_prems (([x,y] MRS FreeUltrafilterNat_Int) :: ys);
|
|
35 |
|
|
36 |
in
|
|
37 |
|
|
38 |
(*---------------------------------------------------------------
|
|
39 |
solves goals of the form
|
|
40 |
[| A1: FUF; A2: FUF; ...; An: FUF |] ==> B : FUF
|
|
41 |
where A1 Int A2 Int ... Int An <= B
|
|
42 |
---------------------------------------------------------------*)
|
|
43 |
|
|
44 |
fun fuf_tac css i = METAHYPS(fn prems =>
|
|
45 |
(rtac ((inter_prems (get_fuf_hyps prems [])) RS
|
|
46 |
FreeUltrafilterNat_subset) 1) THEN
|
|
47 |
auto_tac css) i;
|
|
48 |
|
|
49 |
fun Fuf_tac i = fuf_tac (clasimpset ()) i;
|
|
50 |
|
|
51 |
|
|
52 |
(*---------------------------------------------------------------
|
|
53 |
solves goals of the form
|
|
54 |
[| A1: FUF; A2: FUF; ...; An: FUF |] ==> P
|
|
55 |
where A1 Int A2 Int ... Int An <= {} since {} ~: FUF
|
|
56 |
(i.e. uses fact that FUF is a proper filter)
|
|
57 |
---------------------------------------------------------------*)
|
|
58 |
|
|
59 |
fun fuf_empty_tac css i = METAHYPS (fn prems =>
|
|
60 |
rtac ((inter_prems (get_fuf_hyps prems [])) RS
|
|
61 |
(FreeUltrafilterNat_subset RS (FreeUltrafilterNat_empty RS notE))) 1
|
|
62 |
THEN auto_tac css) i;
|
|
63 |
|
|
64 |
fun Fuf_empty_tac i = fuf_empty_tac (clasimpset ()) i;
|
|
65 |
|
|
66 |
|
|
67 |
(*---------------------------------------------------------------
|
|
68 |
In fact could make this the only tactic: just need to
|
|
69 |
use contraposition and then look for empty set.
|
|
70 |
---------------------------------------------------------------*)
|
|
71 |
|
|
72 |
fun ultra_tac css i = rtac ccontr i THEN fuf_empty_tac css i;
|
|
73 |
fun Ultra_tac i = ultra_tac (clasimpset ()) i;
|
|
74 |
|
|
75 |
end;
|