4 Copyright 1991 University of Cambridge |
4 Copyright 1991 University of Cambridge |
5 |
5 |
6 Instantiation of the generic simplifier for HOL. |
6 Instantiation of the generic simplifier for HOL. |
7 *) |
7 *) |
8 |
8 |
9 section "Simplifier"; |
9 (* legacy ML bindings *) |
10 |
10 |
11 val [prem] = goal (the_context ()) "x==y ==> x=y"; |
11 val Eq_FalseI = thm "Eq_FalseI"; |
12 by (rewtac prem); |
12 val Eq_TrueI = thm "Eq_TrueI"; |
13 by (rtac refl 1); |
13 val all_conj_distrib = thm "all_conj_distrib"; |
14 qed "meta_eq_to_obj_eq"; |
14 val all_simps = thms "all_simps"; |
15 |
15 val cases_simp = thm "cases_simp"; |
16 Goal "(%s. f s) = f"; |
16 val conj_assoc = thm "conj_assoc"; |
17 br refl 1; |
17 val conj_comms = thms "conj_comms"; |
18 qed "eta_contract_eq"; |
18 val conj_commute = thm "conj_commute"; |
19 |
19 val conj_cong = thm "conj_cong"; |
20 |
20 val conj_disj_distribL = thm "conj_disj_distribL"; |
21 fun prover s = prove_goal (the_context ()) s (fn _ => [(Blast_tac 1)]); |
21 val conj_disj_distribR = thm "conj_disj_distribR"; |
22 |
22 val conj_left_commute = thm "conj_left_commute"; |
23 bind_thm ("not_not", prover "(~ ~ P) = P"); |
23 val de_Morgan_conj = thm "de_Morgan_conj"; |
24 |
24 val de_Morgan_disj = thm "de_Morgan_disj"; |
25 bind_thms ("simp_thms", [not_not] @ map prover |
25 val disj_assoc = thm "disj_assoc"; |
26 ["(x=x) = True", |
26 val disj_comms = thms "disj_comms"; |
27 "(~True) = False", "(~False) = True", |
27 val disj_commute = thm "disj_commute"; |
28 "(~P) ~= P", "P ~= (~P)", "(P ~= Q) = (P = (~Q))", |
28 val disj_cong = thm "disj_cong"; |
29 "(True=P) = P", "(P=True) = P", "(False=P) = (~P)", "(P=False) = (~P)", |
29 val disj_conj_distribL = thm "disj_conj_distribL"; |
30 "(True --> P) = P", "(False --> P) = True", |
30 val disj_conj_distribR = thm "disj_conj_distribR"; |
31 "(P --> True) = True", "(P --> P) = True", |
31 val disj_left_commute = thm "disj_left_commute"; |
32 "(P --> False) = (~P)", "(P --> ~P) = (~P)", |
32 val disj_not1 = thm "disj_not1"; |
33 "(P & True) = P", "(True & P) = P", |
33 val disj_not2 = thm "disj_not2"; |
34 "(P & False) = False", "(False & P) = False", |
34 val eq_ac = thms "eq_ac"; |
35 "(P & P) = P", "(P & (P & Q)) = (P & Q)", |
35 val eq_assoc = thm "eq_assoc"; |
36 "(P & ~P) = False", "(~P & P) = False", |
36 val eq_commute = thm "eq_commute"; |
37 "(P | True) = True", "(True | P) = True", |
37 val eq_left_commute = thm "eq_left_commute"; |
38 "(P | False) = P", "(False | P) = P", |
38 val eq_sym_conv = thm "eq_sym_conv"; |
39 "(P | P) = P", "(P | (P | Q)) = (P | Q)", |
39 val eta_contract_eq = thm "eta_contract_eq"; |
40 "(P | ~P) = True", "(~P | P) = True", |
40 val ex_disj_distrib = thm "ex_disj_distrib"; |
41 "((~P) = (~Q)) = (P=Q)", |
41 val ex_simps = thms "ex_simps"; |
42 "(!x. P) = P", "(? x. P) = P", "? x. x=t", "? x. t=x", |
42 val if_False = thm "if_False"; |
43 (* needed for the one-point-rule quantifier simplification procs*) |
43 val if_P = thm "if_P"; |
44 (*essential for termination!!*) |
44 val if_True = thm "if_True"; |
45 "(? x. x=t & P(x)) = P(t)", |
45 val if_bool_eq_conj = thm "if_bool_eq_conj"; |
46 "(? x. t=x & P(x)) = P(t)", |
46 val if_bool_eq_disj = thm "if_bool_eq_disj"; |
47 "(! x. x=t --> P(x)) = P(t)", |
47 val if_cancel = thm "if_cancel"; |
48 "(! x. t=x --> P(x)) = P(t)"]); |
48 val if_def2 = thm "if_def2"; |
49 |
49 val if_eq_cancel = thm "if_eq_cancel"; |
50 bind_thm ("imp_cong", standard (impI RSN |
50 val if_not_P = thm "if_not_P"; |
51 (2, prove_goal (the_context ()) "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))" |
51 val if_splits = thms "if_splits"; |
52 (fn _=> [(Blast_tac 1)]) RS mp RS mp))); |
52 val iff_conv_conj_imp = thm "iff_conv_conj_imp"; |
53 |
53 val imp_all = thm "imp_all"; |
54 (*Miniscoping: pushing in existential quantifiers*) |
54 val imp_cong = thm "imp_cong"; |
55 bind_thms ("ex_simps", map prover |
55 val imp_conjL = thm "imp_conjL"; |
56 ["(EX x. P x & Q) = ((EX x. P x) & Q)", |
56 val imp_conjR = thm "imp_conjR"; |
57 "(EX x. P & Q x) = (P & (EX x. Q x))", |
57 val imp_conv_disj = thm "imp_conv_disj"; |
58 "(EX x. P x | Q) = ((EX x. P x) | Q)", |
58 val imp_disj1 = thm "imp_disj1"; |
59 "(EX x. P | Q x) = (P | (EX x. Q x))", |
59 val imp_disj2 = thm "imp_disj2"; |
60 "(EX x. P x --> Q) = ((ALL x. P x) --> Q)", |
60 val imp_disjL = thm "imp_disjL"; |
61 "(EX x. P --> Q x) = (P --> (EX x. Q x))"]); |
61 val imp_disj_not1 = thm "imp_disj_not1"; |
62 |
62 val imp_disj_not2 = thm "imp_disj_not2"; |
63 (*Miniscoping: pushing in universal quantifiers*) |
63 val imp_ex = thm "imp_ex"; |
64 bind_thms ("all_simps", map prover |
64 val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq"; |
65 ["(ALL x. P x & Q) = ((ALL x. P x) & Q)", |
65 val neq_commute = thm "neq_commute"; |
66 "(ALL x. P & Q x) = (P & (ALL x. Q x))", |
66 val not_all = thm "not_all"; |
67 "(ALL x. P x | Q) = ((ALL x. P x) | Q)", |
67 val not_ex = thm "not_ex"; |
68 "(ALL x. P | Q x) = (P | (ALL x. Q x))", |
68 val not_iff = thm "not_iff"; |
69 "(ALL x. P x --> Q) = ((EX x. P x) --> Q)", |
69 val not_imp = thm "not_imp"; |
70 "(ALL x. P --> Q x) = (P --> (ALL x. Q x))"]); |
70 val not_not = thm "not_not"; |
71 |
71 val rev_conj_cong = thm "rev_conj_cong"; |
72 |
72 val simp_thms = thms "simp_thms"; |
73 fun prove nm thm = qed_goal nm (the_context ()) thm (fn _ => [(Blast_tac 1)]); |
73 val split_if = thm "split_if"; |
74 |
74 val split_if_asm = thm "split_if_asm"; |
75 prove "eq_commute" "(a=b) = (b=a)"; |
75 |
76 prove "eq_left_commute" "(P=(Q=R)) = (Q=(P=R))"; |
|
77 prove "eq_assoc" "((P=Q)=R) = (P=(Q=R))"; |
|
78 bind_thms ("eq_ac", [eq_commute, eq_left_commute, eq_assoc]); |
|
79 |
|
80 prove "neq_commute" "(a~=b) = (b~=a)"; |
|
81 |
|
82 prove "conj_commute" "(P&Q) = (Q&P)"; |
|
83 prove "conj_left_commute" "(P&(Q&R)) = (Q&(P&R))"; |
|
84 bind_thms ("conj_comms", [conj_commute, conj_left_commute]); |
|
85 prove "conj_assoc" "((P&Q)&R) = (P&(Q&R))"; |
|
86 |
|
87 prove "disj_commute" "(P|Q) = (Q|P)"; |
|
88 prove "disj_left_commute" "(P|(Q|R)) = (Q|(P|R))"; |
|
89 bind_thms ("disj_comms", [disj_commute, disj_left_commute]); |
|
90 prove "disj_assoc" "((P|Q)|R) = (P|(Q|R))"; |
|
91 |
|
92 prove "conj_disj_distribL" "(P&(Q|R)) = (P&Q | P&R)"; |
|
93 prove "conj_disj_distribR" "((P|Q)&R) = (P&R | Q&R)"; |
|
94 |
|
95 prove "disj_conj_distribL" "(P|(Q&R)) = ((P|Q) & (P|R))"; |
|
96 prove "disj_conj_distribR" "((P&Q)|R) = ((P|R) & (Q|R))"; |
|
97 |
|
98 prove "imp_conjR" "(P --> (Q&R)) = ((P-->Q) & (P-->R))"; |
|
99 prove "imp_conjL" "((P&Q) -->R) = (P --> (Q --> R))"; |
|
100 prove "imp_disjL" "((P|Q) --> R) = ((P-->R)&(Q-->R))"; |
|
101 |
|
102 (*These two are specialized, but imp_disj_not1 is useful in Auth/Yahalom.ML*) |
|
103 prove "imp_disj_not1" "(P --> Q | R) = (~Q --> P --> R)"; |
|
104 prove "imp_disj_not2" "(P --> Q | R) = (~R --> P --> Q)"; |
|
105 |
|
106 prove "imp_disj1" "((P-->Q)|R) = (P--> Q|R)"; |
|
107 prove "imp_disj2" "(Q|(P-->R)) = (P--> Q|R)"; |
|
108 |
|
109 prove "de_Morgan_disj" "(~(P | Q)) = (~P & ~Q)"; |
|
110 prove "de_Morgan_conj" "(~(P & Q)) = (~P | ~Q)"; |
|
111 prove "not_imp" "(~(P --> Q)) = (P & ~Q)"; |
|
112 prove "not_iff" "(P~=Q) = (P = (~Q))"; |
|
113 prove "disj_not1" "(~P | Q) = (P --> Q)"; |
|
114 prove "disj_not2" "(P | ~Q) = (Q --> P)"; (* changes orientation :-( *) |
|
115 prove "imp_conv_disj" "(P --> Q) = ((~P) | Q)"; |
|
116 |
|
117 prove "iff_conv_conj_imp" "(P = Q) = ((P --> Q) & (Q --> P))"; |
|
118 |
|
119 |
|
120 (*Avoids duplication of subgoals after split_if, when the true and false |
|
121 cases boil down to the same thing.*) |
|
122 prove "cases_simp" "((P --> Q) & (~P --> Q)) = Q"; |
|
123 |
|
124 prove "not_all" "(~ (! x. P(x))) = (? x.~P(x))"; |
|
125 prove "imp_all" "((! x. P x) --> Q) = (? x. P x --> Q)"; |
|
126 prove "not_ex" "(~ (? x. P(x))) = (! x.~P(x))"; |
|
127 prove "imp_ex" "((? x. P x) --> Q) = (! x. P x --> Q)"; |
|
128 |
|
129 prove "ex_disj_distrib" "(? x. P(x) | Q(x)) = ((? x. P(x)) | (? x. Q(x)))"; |
|
130 prove "all_conj_distrib" "(!x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))"; |
|
131 |
|
132 (* '&' congruence rule: not included by default! |
|
133 May slow rewrite proofs down by as much as 50% *) |
|
134 |
|
135 let val th = prove_goal (the_context ()) |
|
136 "(P=P')--> (P'--> (Q=Q'))--> ((P&Q) = (P'&Q'))" |
|
137 (fn _=> [(Blast_tac 1)]) |
|
138 in bind_thm("conj_cong",standard (impI RSN (2, th RS mp RS mp))) end; |
|
139 |
|
140 let val th = prove_goal (the_context ()) |
|
141 "(Q=Q')--> (Q'--> (P=P'))--> ((P&Q) = (P'&Q'))" |
|
142 (fn _=> [(Blast_tac 1)]) |
|
143 in bind_thm("rev_conj_cong",standard (impI RSN (2, th RS mp RS mp))) end; |
|
144 |
|
145 (* '|' congruence rule: not included by default! *) |
|
146 |
|
147 let val th = prove_goal (the_context ()) |
|
148 "(P=P')--> (~P'--> (Q=Q'))--> ((P|Q) = (P'|Q'))" |
|
149 (fn _=> [(Blast_tac 1)]) |
|
150 in bind_thm("disj_cong",standard (impI RSN (2, th RS mp RS mp))) end; |
|
151 |
|
152 prove "eq_sym_conv" "(x=y) = (y=x)"; |
|
153 |
|
154 |
|
155 (** if-then-else rules **) |
|
156 |
|
157 Goalw [if_def] "(if True then x else y) = x"; |
|
158 by (Blast_tac 1); |
|
159 qed "if_True"; |
|
160 |
|
161 Goalw [if_def] "(if False then x else y) = y"; |
|
162 by (Blast_tac 1); |
|
163 qed "if_False"; |
|
164 |
|
165 Goalw [if_def] "P ==> (if P then x else y) = x"; |
|
166 by (Blast_tac 1); |
|
167 qed "if_P"; |
|
168 |
|
169 Goalw [if_def] "~P ==> (if P then x else y) = y"; |
|
170 by (Blast_tac 1); |
|
171 qed "if_not_P"; |
|
172 |
|
173 Goal "P(if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))"; |
|
174 by (res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1); |
|
175 by (stac if_P 2); |
|
176 by (stac if_not_P 1); |
|
177 by (ALLGOALS (Blast_tac)); |
|
178 qed "split_if"; |
|
179 |
|
180 Goal "P(if Q then x else y) = (~((Q & ~P x) | (~Q & ~P y)))"; |
|
181 by (stac split_if 1); |
|
182 by (Blast_tac 1); |
|
183 qed "split_if_asm"; |
|
184 |
|
185 bind_thms ("if_splits", [split_if, split_if_asm]); |
|
186 |
|
187 bind_thm ("if_def2", read_instantiate [("P","\\<lambda>x. x")] split_if); |
|
188 |
|
189 Goal "(if c then x else x) = x"; |
|
190 by (stac split_if 1); |
|
191 by (Blast_tac 1); |
|
192 qed "if_cancel"; |
|
193 |
|
194 Goal "(if x = y then y else x) = x"; |
|
195 by (stac split_if 1); |
|
196 by (Blast_tac 1); |
|
197 qed "if_eq_cancel"; |
|
198 |
|
199 (*This form is useful for expanding IFs on the RIGHT of the ==> symbol*) |
|
200 Goal "(if P then Q else R) = ((P-->Q) & (~P-->R))"; |
|
201 by (rtac split_if 1); |
|
202 qed "if_bool_eq_conj"; |
|
203 |
|
204 (*And this form is useful for expanding IFs on the LEFT*) |
|
205 Goal "(if P then Q else R) = ((P&Q) | (~P&R))"; |
|
206 by (stac split_if 1); |
|
207 by (Blast_tac 1); |
|
208 qed "if_bool_eq_disj"; |
|
209 |
76 |
210 local |
77 local |
211 val uncurry = prove_goal (the_context()) "P --> Q --> R ==> P & Q --> R" |
78 val uncurry = prove_goal (the_context()) "P --> Q --> R ==> P & Q --> R" |
212 (fn prems => [cut_facts_tac prems 1, Blast_tac 1]); |
79 (fn prems => [cut_facts_tac prems 1, Blast_tac 1]); |
213 |
80 |