author | huffman |
Thu, 15 Sep 2005 23:46:22 +0200 | |
changeset 17429 | e8d6ed3aacfe |
parent 17298 | ad73fb6144cf |
child 20245 | 54db3583354f |
permissions | -rw-r--r-- |
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 :",_) $ _ $ |
|
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17298
diff
changeset
|
25 |
Const ("StarDef.FreeUltrafilterNat",_)))) => get_fuf_hyps xs |
10751 | 26 |
((x RS FreeUltrafilterNat_Compl_mem)::zs) |
27 |
|(_ $ (Const ("op :",_) $ _ $ |
|
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17298
diff
changeset
|
28 |
Const ("StarDef.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; |