1 (* Title : HOL/Real/Hyperreal/fuf.ml |
1 (* Title : HOL/Real/Hyperreal/fuf.ML |
2 ID : $Id$ |
2 ID : $Id$ |
3 Author : Jacques D. Fleuriot |
3 Author : Jacques D. Fleuriot |
4 Copyright : 1998 University of Cambridge |
4 Copyright : 1998 University of Cambridge |
5 1999 University of Edinburgh |
5 1999 University of Edinburgh |
6 Description : Simple tactics to help proofs involving our |
6 |
7 free ultrafilter (FreeUltrafilterNat). We rely |
7 Simple tactics to help proofs involving our free ultrafilter |
8 on the fact that filters satisfy the finite |
8 (FreeUltrafilterNat). We rely on the fact that filters satisfy the |
9 intersection property. |
9 finite intersection property. |
10 *) |
10 *) |
|
11 |
|
12 local |
11 |
13 |
12 exception FUFempty; |
14 exception FUFempty; |
13 |
15 |
14 fun get_fuf_hyps [] zs = zs |
16 fun get_fuf_hyps [] zs = zs |
15 | get_fuf_hyps (x::xs) zs = |
17 | get_fuf_hyps (x::xs) zs = |
16 case (concl_of x) of |
18 case (concl_of x) of |
17 (_ $ (Const ("Not",_) $ (Const ("op :",_) $ _ $ |
19 (_ $ (Const ("Not",_) $ (Const ("op :",_) $ _ $ |
18 Const ("HyperDef.FreeUltrafilterNat",_)))) => get_fuf_hyps xs |
20 Const ("HyperDef.FreeUltrafilterNat",_)))) => get_fuf_hyps xs |
19 ((x RS FreeUltrafilterNat_Compl_mem)::zs) |
21 ((x RS FreeUltrafilterNat_Compl_mem)::zs) |
20 |(_ $ (Const ("op :",_) $ _ $ |
22 |(_ $ (Const ("op :",_) $ _ $ |
21 Const ("HyperDef.FreeUltrafilterNat",_))) => get_fuf_hyps xs (x::zs) |
23 Const ("HyperDef.FreeUltrafilterNat",_))) => get_fuf_hyps xs (x::zs) |
22 | _ => get_fuf_hyps xs zs; |
24 | _ => get_fuf_hyps xs zs; |
23 |
25 |
24 fun Intprems [] = raise FUFempty |
26 fun inter_prems [] = raise FUFempty |
25 | Intprems [x] = x |
27 | inter_prems [x] = x |
26 | Intprems (x::y::ys) = |
28 | inter_prems (x::y::ys) = |
27 Intprems (([x,y] MRS FreeUltrafilterNat_Int) :: ys); |
29 inter_prems (([x,y] MRS FreeUltrafilterNat_Int) :: ys); |
28 |
30 |
29 (*--------------------------------------------------------------- |
31 in |
30 solves goals of the form |
32 |
31 [| A1: FUF; A2: FUF; ...; An: FUF |] ==> B : FUF |
33 (*--------------------------------------------------------------- |
32 where A1 Int A2 Int ... Int An <= B |
34 solves goals of the form |
|
35 [| A1: FUF; A2: FUF; ...; An: FUF |] ==> B : FUF |
|
36 where A1 Int A2 Int ... Int An <= B |
33 ---------------------------------------------------------------*) |
37 ---------------------------------------------------------------*) |
34 |
38 |
35 val Fuf_tac = METAHYPS(fn prems => |
39 fun fuf_tac css i = METAHYPS(fn prems => |
36 (rtac ((Intprems (get_fuf_hyps prems [])) RS |
40 (rtac ((inter_prems (get_fuf_hyps prems [])) RS |
37 FreeUltrafilterNat_subset) 1) THEN |
41 FreeUltrafilterNat_subset) 1) THEN |
38 Auto_tac); |
42 auto_tac css) i; |
39 |
43 |
40 fun fuf_tac (fclaset,fsimpset) i = METAHYPS(fn prems => |
44 fun Fuf_tac i = fuf_tac (clasimpset ()) i; |
41 (rtac ((Intprems (get_fuf_hyps prems [])) RS |
|
42 FreeUltrafilterNat_subset) 1) THEN |
|
43 auto_tac (fclaset,fsimpset)) i; |
|
44 |
45 |
45 (*--------------------------------------------------------------- |
46 |
46 solves goals of the form |
47 (*--------------------------------------------------------------- |
|
48 solves goals of the form |
47 [| A1: FUF; A2: FUF; ...; An: FUF |] ==> P |
49 [| A1: FUF; A2: FUF; ...; An: FUF |] ==> P |
48 where A1 Int A2 Int ... Int An <= {} since {} ~: FUF |
50 where A1 Int A2 Int ... Int An <= {} since {} ~: FUF |
49 (i.e. uses fact that FUF is a proper filter) |
51 (i.e. uses fact that FUF is a proper filter) |
50 ---------------------------------------------------------------*) |
52 ---------------------------------------------------------------*) |
51 |
53 |
52 val Fuf_empty_tac = METAHYPS(fn prems => |
54 fun fuf_empty_tac css i = METAHYPS (fn prems => |
53 (rtac ((Intprems (get_fuf_hyps prems [])) RS |
55 rtac ((inter_prems (get_fuf_hyps prems [])) RS |
54 (FreeUltrafilterNat_subset RS |
56 (FreeUltrafilterNat_subset RS (FreeUltrafilterNat_empty RS notE))) 1 |
55 (FreeUltrafilterNat_empty RS notE))) 1) |
57 THEN auto_tac css) i; |
56 THEN Auto_tac); |
|
57 |
58 |
58 fun fuf_empty_tac (fclaset,fsimpset) i = METAHYPS(fn prems => |
59 fun Fuf_empty_tac i = fuf_empty_tac (clasimpset ()) i; |
59 (rtac ((Intprems (get_fuf_hyps prems [])) RS |
|
60 (FreeUltrafilterNat_subset RS |
|
61 (FreeUltrafilterNat_empty RS notE))) 1) |
|
62 THEN auto_tac (fclaset,fsimpset)) i; |
|
63 |
60 |
64 (*--------------------------------------------------------------- |
61 |
|
62 (*--------------------------------------------------------------- |
65 All in one -- not really needed. |
63 All in one -- not really needed. |
66 ---------------------------------------------------------------*) |
64 ---------------------------------------------------------------*) |
67 |
65 |
68 fun Fuf_auto_tac i = SOLVE (Fuf_empty_tac i) ORELSE TRY(Fuf_tac i); |
66 fun fuf_auto_tac css i = SOLVE (fuf_empty_tac css i) ORELSE TRY (fuf_tac css i); |
|
67 fun Fuf_auto_tac i = fuf_auto_tac (clasimpset ()) i; |
69 |
68 |
70 fun fuf_auto_tac (fclaset,fsimpset) i = |
|
71 SOLVE (fuf_empty_tac (fclaset,fsimpset) i) |
|
72 ORELSE TRY(fuf_tac (fclaset,fsimpset) i); |
|
73 |
69 |
74 (*--------------------------------------------------------------- |
70 (*--------------------------------------------------------------- |
75 In fact could make this the only tactic: just need to |
71 In fact could make this the only tactic: just need to |
76 use contraposition and then look for empty set. |
72 use contraposition and then look for empty set. |
77 ---------------------------------------------------------------*) |
73 ---------------------------------------------------------------*) |
78 |
74 |
79 fun Ultra_tac i = rtac ccontr i THEN Fuf_empty_tac i; |
75 fun ultra_tac css i = rtac ccontr i THEN fuf_empty_tac css i; |
80 fun ultra_tac (fclaset,fsimpset) i = rtac ccontr i THEN |
76 fun Ultra_tac i = ultra_tac (clasimpset ()) i; |
81 fuf_empty_tac (fclaset,fsimpset) i; |
|
82 |
77 |
|
78 end; |