52 val DelIffs = seq delIff |
52 val DelIffs = seq delIff |
53 end; |
53 end; |
54 |
54 |
55 local |
55 local |
56 |
56 |
57 fun prover s = prove_goal HOL.thy s (fn _ => [blast_tac HOL_cs 1]); |
57 fun prover s = prove_goal HOL.thy s (K [blast_tac HOL_cs 1]); |
58 |
58 |
59 val P_imp_P_iff_True = prover "P --> (P = True)" RS mp; |
59 val P_imp_P_iff_True = prover "P --> (P = True)" RS mp; |
60 val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection; |
60 val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection; |
61 |
61 |
62 val not_P_imp_P_iff_F = prover "~P --> (P = False)" RS mp; |
62 val not_P_imp_P_iff_F = prover "~P --> (P = False)" RS mp; |
164 |
164 |
165 (* Elimination of True from asumptions: *) |
165 (* Elimination of True from asumptions: *) |
166 |
166 |
167 val True_implies_equals = prove_goal HOL.thy |
167 val True_implies_equals = prove_goal HOL.thy |
168 "(True ==> PROP P) == PROP P" |
168 "(True ==> PROP P) == PROP P" |
169 (fn _ => [rtac equal_intr_rule 1, atac 2, |
169 (K [rtac equal_intr_rule 1, atac 2, |
170 METAHYPS (fn prems => resolve_tac prems 1) 1, |
170 METAHYPS (fn prems => resolve_tac prems 1) 1, |
171 rtac TrueI 1]); |
171 rtac TrueI 1]); |
172 |
172 |
173 fun prove nm thm = qed_goal nm HOL.thy thm (fn _ => [blast_tac HOL_cs 1]); |
173 fun prove nm thm = qed_goal nm HOL.thy thm (K [blast_tac HOL_cs 1]); |
174 |
174 |
175 prove "conj_commute" "(P&Q) = (Q&P)"; |
175 prove "conj_commute" "(P&Q) = (Q&P)"; |
176 prove "conj_left_commute" "(P&(Q&R)) = (Q&(P&R))"; |
176 prove "conj_left_commute" "(P&(Q&R)) = (Q&(P&R))"; |
177 val conj_comms = [conj_commute, conj_left_commute]; |
177 val conj_comms = [conj_commute, conj_left_commute]; |
178 prove "conj_assoc" "((P&Q)&R) = (P&(Q&R))"; |
178 prove "conj_assoc" "((P&Q)&R) = (P&(Q&R))"; |
237 in bind_thm("disj_cong",standard (impI RSN (2, th RS mp RS mp))) end; |
237 in bind_thm("disj_cong",standard (impI RSN (2, th RS mp RS mp))) end; |
238 |
238 |
239 prove "eq_sym_conv" "(x=y) = (y=x)"; |
239 prove "eq_sym_conv" "(x=y) = (y=x)"; |
240 |
240 |
241 qed_goalw "o_apply" HOL.thy [o_def] "(f o g) x = f (g x)" |
241 qed_goalw "o_apply" HOL.thy [o_def] "(f o g) x = f (g x)" |
242 (fn _ => [rtac refl 1]); |
242 (K [rtac refl 1]); |
243 |
243 |
244 qed_goal "meta_eq_to_obj_eq" HOL.thy "x==y ==> x=y" |
244 qed_goal "meta_eq_to_obj_eq" HOL.thy "x==y ==> x=y" |
245 (fn [prem] => [rewtac prem, rtac refl 1]); |
245 (fn [prem] => [rewtac prem, rtac refl 1]); |
246 |
246 |
247 qed_goalw "if_True" HOL.thy [if_def] "(if True then x else y) = x" |
247 qed_goalw "if_True" HOL.thy [if_def] "(if True then x else y) = x" |
248 (fn _=>[blast_tac (HOL_cs addIs [select_equality]) 1]); |
248 (K [Blast_tac 1]); |
249 |
249 |
250 qed_goalw "if_False" HOL.thy [if_def] "(if False then x else y) = y" |
250 qed_goalw "if_False" HOL.thy [if_def] "(if False then x else y) = y" |
251 (fn _=>[blast_tac (HOL_cs addIs [select_equality]) 1]); |
251 (K [Blast_tac 1]); |
252 |
252 |
253 qed_goal "if_P" HOL.thy "P ==> (if P then x else y) = x" |
253 qed_goal "if_P" HOL.thy "P ==> (if P then x else y) = x" |
254 (fn [prem] => [ stac (prem RS eqTrueI) 1, rtac if_True 1 ]); |
254 (fn [prem] => [ stac (prem RS eqTrueI) 1, rtac if_True 1 ]); |
255 (* |
255 (* |
256 qed_goal "if_not_P" HOL.thy "~P ==> (if P then x else y) = y" |
256 qed_goal "if_not_P" HOL.thy "~P ==> (if P then x else y) = y" |
257 (fn [prem] => [ stac (prem RS not_P_imp_P_iff_F) 1, rtac if_False 1 ]); |
257 (fn [prem] => [ stac (prem RS not_P_imp_P_iff_F) 1, rtac if_False 1 ]); |
258 *) |
258 *) |
259 qed_goalw "if_not_P" HOL.thy [if_def] "!!P. ~P ==> (if P then x else y) = y" |
259 qed_goalw "if_not_P" HOL.thy [if_def] "!!P. ~P ==> (if P then x else y) = y" |
260 (fn _ => [blast_tac (HOL_cs addIs [select_equality]) 1]); |
260 (K [Blast_tac 1]); |
261 |
261 |
262 qed_goal "expand_if" HOL.thy |
262 qed_goal "expand_if" HOL.thy |
263 "P(if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))" (K [ |
263 "P(if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))" (K [ |
264 res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1, |
264 res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1, |
265 stac if_P 2, |
265 stac if_P 2, |
271 stac expand_if 1, |
271 stac expand_if 1, |
272 blast_tac HOL_cs 1]); |
272 blast_tac HOL_cs 1]); |
273 |
273 |
274 qed_goal "if_bool_eq" HOL.thy |
274 qed_goal "if_bool_eq" HOL.thy |
275 "(if P then Q else R) = ((P-->Q) & (~P-->R))" |
275 "(if P then Q else R) = ((P-->Q) & (~P-->R))" |
276 (fn _ => [rtac expand_if 1]); |
276 (K [rtac expand_if 1]); |
277 |
277 |
278 |
278 |
279 (*** make simplification procedures for quantifier elimination ***) |
279 (*** make simplification procedures for quantifier elimination ***) |
280 |
280 |
281 structure Quantifier1 = Quantifier1Fun( |
281 structure Quantifier1 = Quantifier1Fun( |
335 infix 4 addsplits; |
335 infix 4 addsplits; |
336 fun ss addsplits splits = ss addloop (split_tac splits); |
336 fun ss addsplits splits = ss addloop (split_tac splits); |
337 |
337 |
338 |
338 |
339 qed_goal "if_cancel" HOL.thy "(if c then x else x) = x" |
339 qed_goal "if_cancel" HOL.thy "(if c then x else x) = x" |
340 (fn _ => [split_tac [expand_if] 1, blast_tac HOL_cs 1]); |
340 (K [split_tac [expand_if] 1, blast_tac HOL_cs 1]); |
341 |
341 |
342 (** 'if' congruence rules: neither included by default! *) |
342 (** 'if' congruence rules: neither included by default! *) |
343 |
343 |
344 (*Simplifies x assuming c and y assuming ~c*) |
344 (*Simplifies x assuming c and y assuming ~c*) |
345 qed_goal "if_cong" HOL.thy |
345 qed_goal "if_cong" HOL.thy |
393 addsimprocs [defALL_regroup,defEX_regroup] |
393 addsimprocs [defALL_regroup,defEX_regroup] |
394 addcongs [imp_cong]; |
394 addcongs [imp_cong]; |
395 |
395 |
396 qed_goal "if_distrib" HOL.thy |
396 qed_goal "if_distrib" HOL.thy |
397 "f(if c then x else y) = (if c then f x else f y)" |
397 "f(if c then x else y) = (if c then f x else f y)" |
398 (fn _ => [simp_tac (HOL_ss setloop (split_tac [expand_if])) 1]); |
398 (K [simp_tac (HOL_ss setloop (split_tac [expand_if])) 1]); |
399 |
399 |
400 qed_goalw "o_assoc" HOL.thy [o_def] "f o (g o h) = f o g o h" |
400 qed_goalw "o_assoc" HOL.thy [o_def] "f o (g o h) = f o g o h" |
401 (fn _ => [rtac ext 1, rtac refl 1]); |
401 (K [rtac ext 1, rtac refl 1]); |
402 |
402 |
403 |
403 |
404 (*For expand_case_tac*) |
404 (*For expand_case_tac*) |
405 val prems = goal HOL.thy "[| P ==> Q(True); ~P ==> Q(False) |] ==> Q(P)"; |
405 val prems = goal HOL.thy "[| P ==> Q(True); ~P ==> Q(False) |] ==> Q(P)"; |
406 by (case_tac "P" 1); |
406 by (case_tac "P" 1); |