clasohm@1463
|
1 |
(* Title: FOLP/simpdata.ML
|
clasohm@0
|
2 |
ID: $Id$
|
clasohm@1459
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
clasohm@0
|
4 |
Copyright 1991 University of Cambridge
|
clasohm@0
|
5 |
|
clasohm@1463
|
6 |
Simplification data for FOLP
|
clasohm@0
|
7 |
*)
|
clasohm@0
|
8 |
|
clasohm@0
|
9 |
(*** Rewrite rules ***)
|
clasohm@0
|
10 |
|
clasohm@0
|
11 |
fun int_prove_fun_raw s =
|
clasohm@0
|
12 |
(writeln s; prove_goal IFOLP.thy s
|
paulson@2603
|
13 |
(fn prems => [ (cut_facts_tac prems 1), (IntPr.fast_tac 1) ]));
|
clasohm@0
|
14 |
|
clasohm@0
|
15 |
fun int_prove_fun s = int_prove_fun_raw ("?p : "^s);
|
clasohm@0
|
16 |
|
clasohm@0
|
17 |
val conj_rews = map int_prove_fun
|
clasohm@1459
|
18 |
["P & True <-> P", "True & P <-> P",
|
clasohm@0
|
19 |
"P & False <-> False", "False & P <-> False",
|
clasohm@0
|
20 |
"P & P <-> P",
|
clasohm@1459
|
21 |
"P & ~P <-> False", "~P & P <-> False",
|
clasohm@0
|
22 |
"(P & Q) & R <-> P & (Q & R)"];
|
clasohm@0
|
23 |
|
clasohm@0
|
24 |
val disj_rews = map int_prove_fun
|
clasohm@1459
|
25 |
["P | True <-> True", "True | P <-> True",
|
clasohm@1459
|
26 |
"P | False <-> P", "False | P <-> P",
|
clasohm@0
|
27 |
"P | P <-> P",
|
clasohm@0
|
28 |
"(P | Q) | R <-> P | (Q | R)"];
|
clasohm@0
|
29 |
|
clasohm@0
|
30 |
val not_rews = map int_prove_fun
|
clasohm@1459
|
31 |
["~ False <-> True", "~ True <-> False"];
|
clasohm@0
|
32 |
|
clasohm@0
|
33 |
val imp_rews = map int_prove_fun
|
clasohm@1459
|
34 |
["(P --> False) <-> ~P", "(P --> True) <-> True",
|
clasohm@1459
|
35 |
"(False --> P) <-> True", "(True --> P) <-> P",
|
clasohm@1459
|
36 |
"(P --> P) <-> True", "(P --> ~P) <-> ~P"];
|
clasohm@0
|
37 |
|
clasohm@0
|
38 |
val iff_rews = map int_prove_fun
|
clasohm@1459
|
39 |
["(True <-> P) <-> P", "(P <-> True) <-> P",
|
clasohm@0
|
40 |
"(P <-> P) <-> True",
|
clasohm@1459
|
41 |
"(False <-> P) <-> ~P", "(P <-> False) <-> ~P"];
|
clasohm@0
|
42 |
|
clasohm@0
|
43 |
val quant_rews = map int_prove_fun
|
wenzelm@3836
|
44 |
["(ALL x. P) <-> P", "(EX x. P) <-> P"];
|
clasohm@0
|
45 |
|
clasohm@0
|
46 |
(*These are NOT supplied by default!*)
|
clasohm@0
|
47 |
val distrib_rews = map int_prove_fun
|
clasohm@0
|
48 |
["~(P|Q) <-> ~P & ~Q",
|
clasohm@0
|
49 |
"P & (Q | R) <-> P&Q | P&R", "(Q | R) & P <-> Q&P | R&P",
|
clasohm@0
|
50 |
"(P | Q --> R) <-> (P --> R) & (Q --> R)",
|
wenzelm@3836
|
51 |
"~(EX x. NORM(P(x))) <-> (ALL x. ~NORM(P(x)))",
|
wenzelm@3836
|
52 |
"((EX x. NORM(P(x))) --> Q) <-> (ALL x. NORM(P(x)) --> Q)",
|
wenzelm@3836
|
53 |
"(EX x. NORM(P(x))) & NORM(Q) <-> (EX x. NORM(P(x)) & NORM(Q))",
|
wenzelm@3836
|
54 |
"NORM(Q) & (EX x. NORM(P(x))) <-> (EX x. NORM(Q) & NORM(P(x)))"];
|
clasohm@0
|
55 |
|
clasohm@0
|
56 |
val P_Imp_P_iff_T = int_prove_fun_raw "p:P ==> ?p:(P <-> True)";
|
clasohm@0
|
57 |
|
clasohm@0
|
58 |
fun make_iff_T th = th RS P_Imp_P_iff_T;
|
clasohm@0
|
59 |
|
clasohm@0
|
60 |
val refl_iff_T = make_iff_T refl;
|
clasohm@0
|
61 |
|
clasohm@0
|
62 |
val norm_thms = [(norm_eq RS sym, norm_eq),
|
clasohm@1459
|
63 |
(NORM_iff RS iff_sym, NORM_iff)];
|
clasohm@0
|
64 |
|
clasohm@0
|
65 |
|
clasohm@0
|
66 |
(* Conversion into rewrite rules *)
|
clasohm@0
|
67 |
|
clasohm@0
|
68 |
val not_P_imp_P_iff_F = int_prove_fun_raw "p:~P ==> ?p:(P <-> False)";
|
clasohm@0
|
69 |
|
clasohm@0
|
70 |
fun mk_eq th = case concl_of th of
|
clasohm@0
|
71 |
_ $ (Const("op <->",_)$_$_) $ _ => th
|
clasohm@0
|
72 |
| _ $ (Const("op =",_)$_$_) $ _ => th
|
clasohm@0
|
73 |
| _ $ (Const("Not",_)$_) $ _ => th RS not_P_imp_P_iff_F
|
clasohm@0
|
74 |
| _ => make_iff_T th;
|
clasohm@0
|
75 |
|
oheimb@5304
|
76 |
|
oheimb@5304
|
77 |
val mksimps_pairs =
|
oheimb@5304
|
78 |
[("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
|
oheimb@5304
|
79 |
("All", [spec]), ("True", []), ("False", [])];
|
clasohm@0
|
80 |
|
oheimb@5304
|
81 |
fun mk_atomize pairs =
|
oheimb@5304
|
82 |
let fun atoms th =
|
oheimb@5304
|
83 |
(case concl_of th of
|
oheimb@5304
|
84 |
Const("Trueprop",_) $ p =>
|
oheimb@5304
|
85 |
(case head_of p of
|
oheimb@5304
|
86 |
Const(a,_) =>
|
oheimb@5304
|
87 |
(case assoc(pairs,a) of
|
oheimb@5304
|
88 |
Some(rls) => flat (map atoms ([th] RL rls))
|
oheimb@5304
|
89 |
| None => [th])
|
oheimb@5304
|
90 |
| _ => [th])
|
oheimb@5304
|
91 |
| _ => [th])
|
oheimb@5304
|
92 |
in atoms end;
|
oheimb@5304
|
93 |
|
oheimb@5304
|
94 |
fun mk_rew_rules th = map mk_eq (mk_atomize mksimps_pairs th);
|
clasohm@0
|
95 |
|
clasohm@0
|
96 |
(*destruct function for analysing equations*)
|
clasohm@0
|
97 |
fun dest_red(_ $ (red $ lhs $ rhs) $ _) = (red,lhs,rhs)
|
clasohm@0
|
98 |
| dest_red t = raise TERM("FOL/dest_red", [t]);
|
clasohm@0
|
99 |
|
clasohm@0
|
100 |
structure FOLP_SimpData : SIMP_DATA =
|
clasohm@0
|
101 |
struct
|
clasohm@1459
|
102 |
val refl_thms = [refl, iff_refl]
|
clasohm@1459
|
103 |
val trans_thms = [trans, iff_trans]
|
clasohm@1459
|
104 |
val red1 = iffD1
|
clasohm@1459
|
105 |
val red2 = iffD2
|
clasohm@1459
|
106 |
val mk_rew_rules = mk_rew_rules
|
clasohm@1459
|
107 |
val case_splits = [] (*NO IF'S!*)
|
clasohm@1459
|
108 |
val norm_thms = norm_thms
|
clasohm@1459
|
109 |
val subst_thms = [subst];
|
clasohm@1459
|
110 |
val dest_red = dest_red
|
clasohm@0
|
111 |
end;
|
clasohm@0
|
112 |
|
clasohm@0
|
113 |
structure FOLP_Simp = SimpFun(FOLP_SimpData);
|
clasohm@0
|
114 |
|
clasohm@0
|
115 |
(*not a component of SIMP_DATA, but an argument of SIMP_TAC *)
|
clasohm@0
|
116 |
val FOLP_congs =
|
clasohm@0
|
117 |
[all_cong,ex_cong,eq_cong,
|
clasohm@0
|
118 |
conj_cong,disj_cong,imp_cong,iff_cong,not_cong] @ pred_congs;
|
clasohm@0
|
119 |
|
clasohm@0
|
120 |
val IFOLP_rews =
|
clasohm@0
|
121 |
[refl_iff_T] @ conj_rews @ disj_rews @ not_rews @
|
clasohm@0
|
122 |
imp_rews @ iff_rews @ quant_rews;
|
clasohm@0
|
123 |
|
lcp@1009
|
124 |
open FOLP_Simp;
|
clasohm@0
|
125 |
|
clasohm@0
|
126 |
val auto_ss = empty_ss setauto ares_tac [TrueI];
|
clasohm@0
|
127 |
|
clasohm@0
|
128 |
val IFOLP_ss = auto_ss addcongs FOLP_congs addrews IFOLP_rews;
|
clasohm@0
|
129 |
|
clasohm@0
|
130 |
(*Classical version...*)
|
clasohm@0
|
131 |
fun prove_fun s =
|
clasohm@0
|
132 |
(writeln s; prove_goal FOLP.thy s
|
clasohm@0
|
133 |
(fn prems => [ (cut_facts_tac prems 1), (Cla.fast_tac FOLP_cs 1) ]));
|
clasohm@0
|
134 |
|
clasohm@0
|
135 |
val cla_rews = map prove_fun
|
clasohm@1459
|
136 |
["?p:P | ~P", "?p:~P | P",
|
clasohm@1459
|
137 |
"?p:~ ~ P <-> P", "?p:(~P --> P) <-> P"];
|
clasohm@0
|
138 |
|
clasohm@0
|
139 |
val FOLP_rews = IFOLP_rews@cla_rews;
|
clasohm@0
|
140 |
|
clasohm@0
|
141 |
val FOLP_ss = auto_ss addcongs FOLP_congs addrews FOLP_rews;
|
clasohm@0
|
142 |
|
clasohm@0
|
143 |
|