author | lcp |
Wed, 14 Dec 1994 16:48:36 +0100 | |
changeset 784 | b5adfdad0663 |
parent 756 | e0e5c1581e4c |
child 942 | d9edeb96b51c |
permissions | -rw-r--r-- |
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 |
||
784 | 53 |
bind_thm("conj_commute", int_prove_fun "P&Q <-> Q&P"); |
54 |
bind_thm("disj_commute", int_prove_fun "P|Q <-> Q|P"); |
|
55 |
||
282 | 56 |
(** Conversion into rewrite rules **) |
0 | 57 |
|
53 | 58 |
fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th; |
59 |
||
282 | 60 |
(*Make atomic rewrite rules*) |
429
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset
|
61 |
fun atomize r = |
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset
|
62 |
case concl_of r of |
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset
|
63 |
Const("Trueprop",_) $ p => |
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset
|
64 |
(case p of |
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset
|
65 |
Const("op -->",_)$_$_ => atomize(r RS mp) |
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset
|
66 |
| Const("op &",_)$_$_ => atomize(r RS conjunct1) @ |
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset
|
67 |
atomize(r RS conjunct2) |
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset
|
68 |
| Const("All",_)$_ => atomize(r RS spec) |
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset
|
69 |
| Const("True",_) => [] (*True is DELETED*) |
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset
|
70 |
| Const("False",_) => [] (*should False do something?*) |
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset
|
71 |
| _ => [r]) |
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset
|
72 |
| _ => [r]; |
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset
|
73 |
|
282 | 74 |
|
75 |
val P_iff_F = int_prove_fun "~P ==> (P <-> False)"; |
|
76 |
val iff_reflection_F = P_iff_F RS iff_reflection; |
|
77 |
||
78 |
val P_iff_T = int_prove_fun "P ==> (P <-> True)"; |
|
79 |
val iff_reflection_T = P_iff_T RS iff_reflection; |
|
80 |
||
81 |
(*Make meta-equalities. The operator below is Trueprop*) |
|
82 |
fun mk_meta_eq th = case concl_of th of |
|
394
432bb9995893
Modified mk_meta_eq to leave meta-equlities on unchanged.
nipkow
parents:
371
diff
changeset
|
83 |
Const("==",_)$_$_ => th |
432bb9995893
Modified mk_meta_eq to leave meta-equlities on unchanged.
nipkow
parents:
371
diff
changeset
|
84 |
| _ $ (Const("op =",_)$_$_) => th RS eq_reflection |
282 | 85 |
| _ $ (Const("op <->",_)$_$_) => th RS iff_reflection |
86 |
| _ $ (Const("Not",_)$_) => th RS iff_reflection_F |
|
87 |
| _ => th RS iff_reflection_T; |
|
0 | 88 |
|
89 |
structure Induction = InductionFun(struct val spec=IFOL.spec end); |
|
90 |
||
91 |
open Simplifier Induction; |
|
92 |
||
3 | 93 |
infix addcongs; |
94 |
fun ss addcongs congs = |
|
282 | 95 |
ss addeqcongs (congs RL [eq_reflection,iff_reflection]); |
96 |
||
97 |
val IFOL_rews = |
|
98 |
[refl RS P_iff_T] @ conj_rews @ disj_rews @ not_rews @ |
|
99 |
imp_rews @ iff_rews @ quant_rews; |
|
3 | 100 |
|
282 | 101 |
val notFalseI = int_prove_fun "~False"; |
102 |
val triv_rls = [TrueI,refl,iff_refl,notFalseI]; |
|
103 |
||
104 |
val IFOL_ss = |
|
105 |
empty_ss |
|
106 |
setmksimps (map mk_meta_eq o atomize o gen_all) |
|
371
3a853818f1d2
FOL/simpdata: added etac FalseE in setsolver call. Toby: "now that the
lcp
parents:
282
diff
changeset
|
107 |
setsolver (fn prems => resolve_tac (triv_rls@prems) |
3a853818f1d2
FOL/simpdata: added etac FalseE in setsolver call. Toby: "now that the
lcp
parents:
282
diff
changeset
|
108 |
ORELSE' assume_tac |
3a853818f1d2
FOL/simpdata: added etac FalseE in setsolver call. Toby: "now that the
lcp
parents:
282
diff
changeset
|
109 |
ORELSE' etac FalseE) |
282 | 110 |
setsubgoaler asm_simp_tac |
111 |
addsimps IFOL_rews |
|
112 |
addcongs [imp_cong]; |
|
0 | 113 |
|
114 |
(*Classical version...*) |
|
115 |
fun prove_fun s = |
|
282 | 116 |
(writeln s; |
117 |
prove_goal FOL.thy s |
|
118 |
(fn prems => [ (cut_facts_tac prems 1), |
|
119 |
(Cla.fast_tac FOL_cs 1) ])); |
|
745 | 120 |
|
0 | 121 |
val cla_rews = map prove_fun |
282 | 122 |
["~(P&Q) <-> ~P | ~Q", |
123 |
"P | ~P", "~P | P", |
|
0 | 124 |
"~ ~ P <-> P", "(~P --> P) <-> P"]; |
125 |
||
126 |
val FOL_ss = IFOL_ss addsimps cla_rews; |
|
127 |
||
128 |
(*** case splitting ***) |
|
129 |
||
756 | 130 |
qed_goal "meta_iffD" FOL.thy "[| P==Q; Q |] ==> P" |
131 |
(fn [prem1,prem2] => [rewtac prem1, rtac prem2 1]); |
|
282 | 132 |
|
133 |
fun split_tac splits = |
|
134 |
mk_case_split_tac meta_iffD (map mk_meta_eq splits); |