author | nipkow |
Wed, 19 Apr 2000 11:56:31 +0200 | |
changeset 8745 | 13b32661dde4 |
parent 7570 | a9391550eea1 |
child 9259 | 103acc345f75 |
permissions | -rw-r--r-- |
7098
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
1 |
(* Title: Sequents/simpdata.ML |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
4 |
Copyright 1999 University of Cambridge |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
5 |
|
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
6 |
Instantiation of the generic simplifier for LK |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
7 |
|
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
8 |
Borrows from the DC simplifier of Soren Heilmann. |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
9 |
*) |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
10 |
|
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
11 |
(*** Rewrite rules ***) |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
12 |
|
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
13 |
fun prove_fun s = |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
14 |
(writeln s; |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
15 |
prove_goal LK.thy s |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
16 |
(fn prems => [ (cut_facts_tac prems 1), |
7123 | 17 |
(fast_tac (pack() add_safes [subst]) 1) ])); |
7098
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
18 |
|
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
19 |
val conj_simps = map prove_fun |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
20 |
["|- P & True <-> P", "|- True & P <-> P", |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
21 |
"|- P & False <-> False", "|- False & P <-> False", |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
22 |
"|- P & P <-> P", " |- P & P & Q <-> P & Q", |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
23 |
"|- P & ~P <-> False", "|- ~P & P <-> False", |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
24 |
"|- (P & Q) & R <-> P & (Q & R)"]; |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
25 |
|
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
26 |
val disj_simps = map prove_fun |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
27 |
["|- P | True <-> True", "|- True | P <-> True", |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
28 |
"|- P | False <-> P", "|- False | P <-> P", |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
29 |
"|- P | P <-> P", "|- P | P | Q <-> P | Q", |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
30 |
"|- (P | Q) | R <-> P | (Q | R)"]; |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
31 |
|
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
32 |
val not_simps = map prove_fun |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
33 |
["|- ~ False <-> True", "|- ~ True <-> False"]; |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
34 |
|
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
35 |
val imp_simps = map prove_fun |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
36 |
["|- (P --> False) <-> ~P", "|- (P --> True) <-> True", |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
37 |
"|- (False --> P) <-> True", "|- (True --> P) <-> P", |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
38 |
"|- (P --> P) <-> True", "|- (P --> ~P) <-> ~P"]; |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
39 |
|
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
40 |
val iff_simps = map prove_fun |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
41 |
["|- (True <-> P) <-> P", "|- (P <-> True) <-> P", |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
42 |
"|- (P <-> P) <-> True", |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
43 |
"|- (False <-> P) <-> ~P", "|- (P <-> False) <-> ~P"]; |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
44 |
|
7123 | 45 |
|
46 |
val quant_simps = map prove_fun |
|
47 |
["|- (ALL x. P) <-> P", |
|
48 |
"|- (ALL x. x=t --> P(x)) <-> P(t)", |
|
49 |
"|- (ALL x. t=x --> P(x)) <-> P(t)", |
|
50 |
"|- (EX x. P) <-> P", |
|
51 |
"|- (EX x. x=t & P(x)) <-> P(t)", |
|
52 |
"|- (EX x. t=x & P(x)) <-> P(t)"]; |
|
53 |
||
54 |
(*** Miniscoping: pushing quantifiers in |
|
55 |
We do NOT distribute of ALL over &, or dually that of EX over | |
|
56 |
Baaz and Leitsch, On Skolemization and Proof Complexity (1994) |
|
57 |
show that this step can increase proof length! |
|
58 |
***) |
|
59 |
||
60 |
(*existential miniscoping*) |
|
61 |
val ex_simps = map prove_fun |
|
62 |
["|- (EX x. P(x) & Q) <-> (EX x. P(x)) & Q", |
|
63 |
"|- (EX x. P & Q(x)) <-> P & (EX x. Q(x))", |
|
64 |
"|- (EX x. P(x) | Q) <-> (EX x. P(x)) | Q", |
|
65 |
"|- (EX x. P | Q(x)) <-> P | (EX x. Q(x))", |
|
66 |
"|- (EX x. P(x) --> Q) <-> (ALL x. P(x)) --> Q", |
|
67 |
"|- (EX x. P --> Q(x)) <-> P --> (EX x. Q(x))"]; |
|
68 |
||
69 |
(*universal miniscoping*) |
|
70 |
val all_simps = map prove_fun |
|
71 |
["|- (ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q", |
|
72 |
"|- (ALL x. P & Q(x)) <-> P & (ALL x. Q(x))", |
|
73 |
"|- (ALL x. P(x) --> Q) <-> (EX x. P(x)) --> Q", |
|
74 |
"|- (ALL x. P --> Q(x)) <-> P --> (ALL x. Q(x))", |
|
75 |
"|- (ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q", |
|
76 |
"|- (ALL x. P | Q(x)) <-> P | (ALL x. Q(x))"]; |
|
77 |
||
7098
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
78 |
(*These are NOT supplied by default!*) |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
79 |
val distrib_simps = map prove_fun |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
80 |
["|- P & (Q | R) <-> P&Q | P&R", |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
81 |
"|- (Q | R) & P <-> Q&P | R&P", |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
82 |
"|- (P | Q --> R) <-> (P --> R) & (Q --> R)"]; |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
83 |
|
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
84 |
(** Conversion into rewrite rules **) |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
85 |
|
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
86 |
fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th; |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
87 |
|
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
88 |
|
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
89 |
(*Make atomic rewrite rules*) |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
90 |
fun atomize r = |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
91 |
case concl_of r of |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
92 |
Const("Trueprop",_) $ Abs(_,_,a) $ Abs(_,_,c) => |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
93 |
(case (forms_of_seq a, forms_of_seq c) of |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
94 |
([], [p]) => |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
95 |
(case p of |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
96 |
Const("op -->",_)$_$_ => atomize(r RS mp_R) |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
97 |
| Const("op &",_)$_$_ => atomize(r RS conjunct1) @ |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
98 |
atomize(r RS conjunct2) |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
99 |
| Const("All",_)$_ => atomize(r RS spec) |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
100 |
| Const("True",_) => [] (*True is DELETED*) |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
101 |
| Const("False",_) => [] (*should False do something?*) |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
102 |
| _ => [r]) |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
103 |
| _ => []) (*ignore theorem unless it has precisely one conclusion*) |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
104 |
| _ => [r]; |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
105 |
|
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
106 |
|
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
107 |
qed_goal "P_iff_F" LK.thy "|- ~P ==> |- (P <-> False)" |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
108 |
(fn prems => [lemma_tac (hd prems) 1, fast_tac LK_pack 1]); |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
109 |
val iff_reflection_F = P_iff_F RS iff_reflection; |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
110 |
|
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
111 |
qed_goal "P_iff_T" LK.thy "|- P ==> |- (P <-> True)" |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
112 |
(fn prems => [lemma_tac (hd prems) 1, fast_tac LK_pack 1]); |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
113 |
val iff_reflection_T = P_iff_T RS iff_reflection; |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
114 |
|
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
115 |
(*Make meta-equalities.*) |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
116 |
fun mk_meta_eq th = case concl_of th of |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
117 |
Const("==",_)$_$_ => th |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
118 |
| Const("Trueprop",_) $ Abs(_,_,a) $ Abs(_,_,c) => |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
119 |
(case (forms_of_seq a, forms_of_seq c) of |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
120 |
([], [p]) => |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
121 |
(case p of |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
122 |
(Const("op =",_)$_$_) => th RS eq_reflection |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
123 |
| (Const("op <->",_)$_$_) => th RS iff_reflection |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
124 |
| (Const("Not",_)$_) => th RS iff_reflection_F |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
125 |
| _ => th RS iff_reflection_T) |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
126 |
| _ => error ("addsimps: unable to use theorem\n" ^ |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
127 |
string_of_thm th)); |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
128 |
|
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
129 |
|
7123 | 130 |
(*Replace premises x=y, X<->Y by X==Y*) |
131 |
val mk_meta_prems = |
|
132 |
rule_by_tactic |
|
133 |
(REPEAT_FIRST (resolve_tac [meta_eq_to_obj_eq, def_imp_iff])); |
|
134 |
||
135 |
fun mk_meta_cong rl = |
|
136 |
standard(mk_meta_eq (mk_meta_prems rl)) |
|
137 |
handle THM _ => |
|
138 |
error("Premises and conclusion of congruence rules must use =-equality or <->"); |
|
139 |
||
140 |
||
141 |
(*** Named rewrite rules ***) |
|
7098
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
142 |
|
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
143 |
fun prove nm thm = qed_goal nm LK.thy thm |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
144 |
(fn prems => [ (cut_facts_tac prems 1), |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
145 |
(fast_tac LK_pack 1) ]); |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
146 |
|
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
147 |
prove "conj_commute" "|- P&Q <-> Q&P"; |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
148 |
prove "conj_left_commute" "|- P&(Q&R) <-> Q&(P&R)"; |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
149 |
val conj_comms = [conj_commute, conj_left_commute]; |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
150 |
|
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
151 |
prove "disj_commute" "|- P|Q <-> Q|P"; |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
152 |
prove "disj_left_commute" "|- P|(Q|R) <-> Q|(P|R)"; |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
153 |
val disj_comms = [disj_commute, disj_left_commute]; |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
154 |
|
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
155 |
prove "conj_disj_distribL" "|- P&(Q|R) <-> (P&Q | P&R)"; |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
156 |
prove "conj_disj_distribR" "|- (P|Q)&R <-> (P&R | Q&R)"; |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
157 |
|
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
158 |
prove "disj_conj_distribL" "|- P|(Q&R) <-> (P|Q) & (P|R)"; |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
159 |
prove "disj_conj_distribR" "|- (P&Q)|R <-> (P|R) & (Q|R)"; |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
160 |
|
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
161 |
prove "imp_conj_distrib" "|- (P --> (Q&R)) <-> (P-->Q) & (P-->R)"; |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
162 |
prove "imp_conj" "|- ((P&Q)-->R) <-> (P --> (Q --> R))"; |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
163 |
prove "imp_disj" "|- (P|Q --> R) <-> (P-->R) & (Q-->R)"; |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
164 |
|
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
165 |
prove "imp_disj1" "|- (P-->Q) | R <-> (P-->Q | R)"; |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
166 |
prove "imp_disj2" "|- Q | (P-->R) <-> (P-->Q | R)"; |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
167 |
|
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
168 |
prove "de_Morgan_disj" "|- (~(P | Q)) <-> (~P & ~Q)"; |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
169 |
prove "de_Morgan_conj" "|- (~(P & Q)) <-> (~P | ~Q)"; |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
170 |
|
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
171 |
prove "not_iff" "|- ~(P <-> Q) <-> (P <-> ~Q)"; |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
172 |
|
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
173 |
|
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
174 |
val [p1,p2] = Goal |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
175 |
"[| |- P <-> P'; |- P' ==> |- Q <-> Q' |] ==> |- (P-->Q) <-> (P'-->Q')"; |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
176 |
by (lemma_tac p1 1); |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
177 |
by (Safe_tac 1); |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
178 |
by (REPEAT (rtac cut 1 |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
179 |
THEN |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
180 |
DEPTH_SOLVE_1 (resolve_tac [thinL, thinR, p2 COMP monotonic] 1) |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
181 |
THEN |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
182 |
Safe_tac 1)); |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
183 |
qed "imp_cong"; |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
184 |
|
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
185 |
val [p1,p2] = Goal |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
186 |
"[| |- P <-> P'; |- P' ==> |- Q <-> Q' |] ==> |- (P&Q) <-> (P'&Q')"; |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
187 |
by (lemma_tac p1 1); |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
188 |
by (Safe_tac 1); |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
189 |
by (REPEAT (rtac cut 1 |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
190 |
THEN |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
191 |
DEPTH_SOLVE_1 (resolve_tac [thinL, thinR, p2 COMP monotonic] 1) |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
192 |
THEN |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
193 |
Safe_tac 1)); |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
194 |
qed "conj_cong"; |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
195 |
|
7123 | 196 |
Goal "|- (x=y) <-> (y=x)"; |
197 |
by (fast_tac (pack() add_safes [subst]) 1); |
|
198 |
qed "eq_sym_conv"; |
|
199 |
||
200 |
||
201 |
(** if-then-else rules **) |
|
202 |
||
203 |
Goalw [If_def] "|- (if True then x else y) = x"; |
|
204 |
by (Fast_tac 1); |
|
205 |
qed "if_True"; |
|
206 |
||
207 |
Goalw [If_def] "|- (if False then x else y) = y"; |
|
208 |
by (Fast_tac 1); |
|
209 |
qed "if_False"; |
|
210 |
||
211 |
Goalw [If_def] "|- P ==> |- (if P then x else y) = x"; |
|
212 |
by (etac (thinR RS cut) 1); |
|
213 |
by (Fast_tac 1); |
|
214 |
qed "if_P"; |
|
215 |
||
216 |
Goalw [If_def] "|- ~P ==> |- (if P then x else y) = y"; |
|
217 |
by (etac (thinR RS cut) 1); |
|
218 |
by (Fast_tac 1); |
|
219 |
qed "if_not_P"; |
|
220 |
||
7098
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
221 |
|
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
222 |
open Simplifier; |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
223 |
|
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
224 |
(*** Standard simpsets ***) |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
225 |
|
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
226 |
(*Add congruence rules for = or <-> (instead of ==) *) |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
227 |
infix 4 addcongs delcongs; |
7123 | 228 |
fun ss addcongs congs = ss addeqcongs (map mk_meta_cong congs); |
229 |
fun ss delcongs congs = ss deleqcongs (map mk_meta_cong congs); |
|
7098
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
230 |
|
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
231 |
fun Addcongs congs = (simpset_ref() := simpset() addcongs congs); |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
232 |
fun Delcongs congs = (simpset_ref() := simpset() delcongs congs); |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
233 |
|
7123 | 234 |
val triv_rls = [FalseL, TrueR, basic, refl, iff_refl, reflexive_thm]; |
7098
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
235 |
|
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
236 |
fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls@prems), |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
237 |
assume_tac]; |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
238 |
(*No premature instantiation of variables during simplification*) |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
239 |
fun safe_solver prems = FIRST'[fn i => DETERM (match_tac (triv_rls@prems) i), |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
240 |
eq_assume_tac]; |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
241 |
|
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
242 |
(*No simprules, but basic infrastructure for simplification*) |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
243 |
val LK_basic_ss = empty_ss setsubgoaler asm_simp_tac |
7570 | 244 |
setSSolver (mk_solver "safe" safe_solver) |
245 |
setSolver (mk_solver "unsafe" unsafe_solver) |
|
7098
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
246 |
setmksimps (map mk_meta_eq o atomize o gen_all); |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
247 |
|
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
248 |
val LK_simps = |
7123 | 249 |
[triv_forall_equality, (* prunes params *) |
250 |
refl RS P_iff_T] @ |
|
251 |
conj_simps @ disj_simps @ not_simps @ |
|
252 |
imp_simps @ iff_simps @quant_simps @ all_simps @ ex_simps @ |
|
7098
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
253 |
[de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2] @ |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
254 |
map prove_fun |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
255 |
["|- P | ~P", "|- ~P | P", |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
256 |
"|- ~ ~ P <-> P", "|- (~P --> P) <-> P", |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
257 |
"|- (~P <-> ~Q) <-> (P<->Q)"]; |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
258 |
|
7123 | 259 |
val LK_ss = LK_basic_ss addsimps LK_simps addeqcongs [left_cong] |
260 |
addcongs [imp_cong]; |
|
7098
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
261 |
|
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
262 |
simpset_ref() := LK_ss; |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
263 |
|
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
264 |
|
7123 | 265 |
(* To create substition rules *) |
7098
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
266 |
|
7123 | 267 |
qed_goal "eq_imp_subst" LK.thy "|- a=b ==> $H, A(a), $G |- $E, A(b), $F" |
7098
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
268 |
(fn prems => |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
269 |
[cut_facts_tac prems 1, |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
270 |
asm_simp_tac LK_basic_ss 1]); |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
271 |
|
7123 | 272 |
Goal "|- P(if Q then x else y) <-> ((Q --> P(x)) & (~Q --> P(y)))"; |
273 |
by (res_inst_tac [ ("P","Q") ] cut 1); |
|
274 |
by (simp_tac (simpset() addsimps [if_P]) 2); |
|
275 |
by (res_inst_tac [ ("P","~Q") ] cut 1); |
|
276 |
by (simp_tac (simpset() addsimps [if_not_P]) 2); |
|
277 |
by (Fast_tac 1); |
|
278 |
qed "split_if"; |
|
7098
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
279 |
|
7123 | 280 |
Goal "|- (if P then x else x) = x"; |
281 |
by (lemma_tac split_if 1); |
|
282 |
by (Fast_tac 1); |
|
283 |
qed "if_cancel"; |
|
284 |
||
285 |
Goal "|- (if x=y then y else x) = x"; |
|
286 |
by (lemma_tac split_if 1); |
|
287 |
by (Safe_tac 1); |
|
288 |
by (rtac symL 1); |
|
289 |
by (rtac basic 1); |
|
290 |
qed "if_eq_cancel"; |
|
291 |
||
292 |
(*Putting in automatic case splits seems to require a lot of work.*) |