0
|
1 |
(* Title: FOL/simpdata
|
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
282
|
4 |
Copyright 1994 University of Cambridge
|
0
|
5 |
|
|
6 |
Simplification data for FOL
|
|
7 |
*)
|
|
8 |
|
|
9 |
(*** Rewrite rules ***)
|
|
10 |
|
|
11 |
fun int_prove_fun s =
|
282
|
12 |
(writeln s;
|
|
13 |
prove_goal IFOL.thy s
|
|
14 |
(fn prems => [ (cut_facts_tac prems 1),
|
|
15 |
(Int.fast_tac 1) ]));
|
0
|
16 |
|
|
17 |
val conj_rews = map int_prove_fun
|
282
|
18 |
["P & True <-> P", "True & P <-> P",
|
0
|
19 |
"P & False <-> False", "False & P <-> False",
|
|
20 |
"P & P <-> P",
|
282
|
21 |
"P & ~P <-> False", "~P & P <-> False",
|
0
|
22 |
"(P & Q) & R <-> P & (Q & R)"];
|
|
23 |
|
|
24 |
val disj_rews = map int_prove_fun
|
|
25 |
["P | True <-> True", "True | P <-> True",
|
|
26 |
"P | False <-> P", "False | P <-> P",
|
|
27 |
"P | P <-> P",
|
|
28 |
"(P | Q) | R <-> P | (Q | R)"];
|
|
29 |
|
|
30 |
val not_rews = map int_prove_fun
|
282
|
31 |
["~(P|Q) <-> ~P & ~Q",
|
|
32 |
"~ False <-> True", "~ True <-> False"];
|
0
|
33 |
|
|
34 |
val imp_rews = map int_prove_fun
|
|
35 |
["(P --> False) <-> ~P", "(P --> True) <-> True",
|
|
36 |
"(False --> P) <-> True", "(True --> P) <-> P",
|
|
37 |
"(P --> P) <-> True", "(P --> ~P) <-> ~P"];
|
|
38 |
|
|
39 |
val iff_rews = map int_prove_fun
|
|
40 |
["(True <-> P) <-> P", "(P <-> True) <-> P",
|
|
41 |
"(P <-> P) <-> True",
|
|
42 |
"(False <-> P) <-> ~P", "(P <-> False) <-> ~P"];
|
|
43 |
|
|
44 |
val quant_rews = map int_prove_fun
|
|
45 |
["(ALL x.P) <-> P", "(EX x.P) <-> P"];
|
|
46 |
|
|
47 |
(*These are NOT supplied by default!*)
|
|
48 |
val distrib_rews = map int_prove_fun
|
282
|
49 |
["P & (Q | R) <-> P&Q | P&R",
|
|
50 |
"(Q | R) & P <-> Q&P | R&P",
|
0
|
51 |
"(P | Q --> R) <-> (P --> R) & (Q --> R)"];
|
|
52 |
|
282
|
53 |
(** Conversion into rewrite rules **)
|
0
|
54 |
|
53
|
55 |
fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
|
|
56 |
|
282
|
57 |
(*Make atomic rewrite rules*)
|
|
58 |
fun atomize th = case concl_of th of
|
|
59 |
_ $ (Const("op &",_) $ _ $ _) => atomize(th RS conjunct1) @
|
|
60 |
atomize(th RS conjunct2)
|
|
61 |
| _ $ (Const("op -->",_) $ _ $ _) => atomize(th RS mp)
|
|
62 |
| _ $ (Const("All",_) $ _) => atomize(th RS spec)
|
|
63 |
| _ $ (Const("True",_)) => []
|
|
64 |
| _ $ (Const("False",_)) => []
|
|
65 |
| _ => [th];
|
|
66 |
|
|
67 |
val P_iff_F = int_prove_fun "~P ==> (P <-> False)";
|
|
68 |
val iff_reflection_F = P_iff_F RS iff_reflection;
|
|
69 |
|
|
70 |
val P_iff_T = int_prove_fun "P ==> (P <-> True)";
|
|
71 |
val iff_reflection_T = P_iff_T RS iff_reflection;
|
|
72 |
|
|
73 |
(*Make meta-equalities. The operator below is Trueprop*)
|
|
74 |
fun mk_meta_eq th = case concl_of th of
|
|
75 |
_ $ (Const("op =",_)$_$_) => th RS eq_reflection
|
|
76 |
| _ $ (Const("op <->",_)$_$_) => th RS iff_reflection
|
|
77 |
| _ $ (Const("Not",_)$_) => th RS iff_reflection_F
|
|
78 |
| _ => th RS iff_reflection_T;
|
0
|
79 |
|
|
80 |
structure Induction = InductionFun(struct val spec=IFOL.spec end);
|
|
81 |
|
|
82 |
open Simplifier Induction;
|
|
83 |
|
3
|
84 |
infix addcongs;
|
|
85 |
fun ss addcongs congs =
|
282
|
86 |
ss addeqcongs (congs RL [eq_reflection,iff_reflection]);
|
|
87 |
|
|
88 |
val IFOL_rews =
|
|
89 |
[refl RS P_iff_T] @ conj_rews @ disj_rews @ not_rews @
|
|
90 |
imp_rews @ iff_rews @ quant_rews;
|
3
|
91 |
|
282
|
92 |
val notFalseI = int_prove_fun "~False";
|
|
93 |
val triv_rls = [TrueI,refl,iff_refl,notFalseI];
|
|
94 |
|
|
95 |
val IFOL_ss =
|
|
96 |
empty_ss
|
|
97 |
setmksimps (map mk_meta_eq o atomize o gen_all)
|
|
98 |
setsolver (fn prems => resolve_tac (triv_rls@prems) ORELSE' assume_tac)
|
|
99 |
setsubgoaler asm_simp_tac
|
|
100 |
addsimps IFOL_rews
|
|
101 |
addcongs [imp_cong];
|
0
|
102 |
|
|
103 |
(*Classical version...*)
|
|
104 |
fun prove_fun s =
|
282
|
105 |
(writeln s;
|
|
106 |
prove_goal FOL.thy s
|
|
107 |
(fn prems => [ (cut_facts_tac prems 1),
|
|
108 |
(Cla.fast_tac FOL_cs 1) ]));
|
0
|
109 |
val cla_rews = map prove_fun
|
282
|
110 |
["~(P&Q) <-> ~P | ~Q",
|
|
111 |
"P | ~P", "~P | P",
|
0
|
112 |
"~ ~ P <-> P", "(~P --> P) <-> P"];
|
|
113 |
|
|
114 |
val FOL_ss = IFOL_ss addsimps cla_rews;
|
|
115 |
|
|
116 |
(*** case splitting ***)
|
|
117 |
|
282
|
118 |
val meta_iffD =
|
|
119 |
prove_goal FOL.thy "[| P==Q; Q |] ==> P"
|
|
120 |
(fn [prem1,prem2] => [rewtac prem1, rtac prem2 1])
|
|
121 |
|
|
122 |
fun split_tac splits =
|
|
123 |
mk_case_split_tac meta_iffD (map mk_meta_eq splits);
|