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