src/HOL/simpdata.ML
changeset 4769 bb60149fe21b
parent 4744 4469d498cd48
child 4794 9db0916ecdae
equal deleted inserted replaced
4768:c342d63173e9 4769:bb60149fe21b
    55 qed_goal "meta_eq_to_obj_eq" HOL.thy "x==y ==> x=y"
    55 qed_goal "meta_eq_to_obj_eq" HOL.thy "x==y ==> x=y"
    56   (fn [prem] => [rewtac prem, rtac refl 1]);
    56   (fn [prem] => [rewtac prem, rtac refl 1]);
    57 
    57 
    58 local
    58 local
    59 
    59 
    60   fun prover s = prove_goal HOL.thy s (K [blast_tac HOL_cs 1]);
    60   fun prover s = prove_goal HOL.thy s (K [Blast_tac 1]);
    61 
    61 
    62   val P_imp_P_iff_True = prover "P --> (P = True)" RS mp;
    62   val P_imp_P_iff_True = prover "P --> (P = True)" RS mp;
    63   val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection;
    63   val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection;
    64 
    64 
    65   val not_P_imp_P_iff_F = prover "~P --> (P = False)" RS mp;
    65   val not_P_imp_P_iff_F = prover "~P --> (P = False)" RS mp;
   131 
   131 
   132 fun mksimps pairs = map mk_meta_eq_simp o atomize pairs o gen_all;
   132 fun mksimps pairs = map mk_meta_eq_simp o atomize pairs o gen_all;
   133 
   133 
   134 val imp_cong = impI RSN
   134 val imp_cong = impI RSN
   135     (2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
   135     (2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
   136         (fn _=> [blast_tac HOL_cs 1]) RS mp RS mp);
   136         (fn _=> [Blast_tac 1]) RS mp RS mp);
   137 
   137 
   138 (*Miniscoping: pushing in existential quantifiers*)
   138 (*Miniscoping: pushing in existential quantifiers*)
   139 val ex_simps = map prover 
   139 val ex_simps = map prover 
   140                 ["(EX x. P x & Q)   = ((EX x. P x) & Q)",
   140                 ["(EX x. P x & Q)   = ((EX x. P x) & Q)",
   141                  "(EX x. P & Q x)   = (P & (EX x. Q x))",
   141                  "(EX x. P & Q x)   = (P & (EX x. Q x))",
   173  "(True ==> PROP P) == PROP P"
   173  "(True ==> PROP P) == PROP P"
   174 (K [rtac equal_intr_rule 1, atac 2,
   174 (K [rtac equal_intr_rule 1, atac 2,
   175           METAHYPS (fn prems => resolve_tac prems 1) 1,
   175           METAHYPS (fn prems => resolve_tac prems 1) 1,
   176           rtac TrueI 1]);
   176           rtac TrueI 1]);
   177 
   177 
   178 fun prove nm thm  = qed_goal nm HOL.thy thm (K [blast_tac HOL_cs 1]);
   178 fun prove nm thm  = qed_goal nm HOL.thy thm (K [Blast_tac 1]);
   179 
   179 
   180 prove "conj_commute" "(P&Q) = (Q&P)";
   180 prove "conj_commute" "(P&Q) = (Q&P)";
   181 prove "conj_left_commute" "(P&(Q&R)) = (Q&(P&R))";
   181 prove "conj_left_commute" "(P&(Q&R)) = (Q&(P&R))";
   182 val conj_comms = [conj_commute, conj_left_commute];
   182 val conj_comms = [conj_commute, conj_left_commute];
   183 prove "conj_assoc" "((P&Q)&R) = (P&(Q&R))";
   183 prove "conj_assoc" "((P&Q)&R) = (P&(Q&R))";
   226 (* '&' congruence rule: not included by default!
   226 (* '&' congruence rule: not included by default!
   227    May slow rewrite proofs down by as much as 50% *)
   227    May slow rewrite proofs down by as much as 50% *)
   228 
   228 
   229 let val th = prove_goal HOL.thy 
   229 let val th = prove_goal HOL.thy 
   230                 "(P=P')--> (P'--> (Q=Q'))--> ((P&Q) = (P'&Q'))"
   230                 "(P=P')--> (P'--> (Q=Q'))--> ((P&Q) = (P'&Q'))"
   231                 (fn _=> [blast_tac HOL_cs 1])
   231                 (fn _=> [Blast_tac 1])
   232 in  bind_thm("conj_cong",standard (impI RSN (2, th RS mp RS mp)))  end;
   232 in  bind_thm("conj_cong",standard (impI RSN (2, th RS mp RS mp)))  end;
   233 
   233 
   234 let val th = prove_goal HOL.thy 
   234 let val th = prove_goal HOL.thy 
   235                 "(Q=Q')--> (Q'--> (P=P'))--> ((P&Q) = (P'&Q'))"
   235                 "(Q=Q')--> (Q'--> (P=P'))--> ((P&Q) = (P'&Q'))"
   236                 (fn _=> [blast_tac HOL_cs 1])
   236                 (fn _=> [Blast_tac 1])
   237 in  bind_thm("rev_conj_cong",standard (impI RSN (2, th RS mp RS mp)))  end;
   237 in  bind_thm("rev_conj_cong",standard (impI RSN (2, th RS mp RS mp)))  end;
   238 
   238 
   239 (* '|' congruence rule: not included by default! *)
   239 (* '|' congruence rule: not included by default! *)
   240 
   240 
   241 let val th = prove_goal HOL.thy 
   241 let val th = prove_goal HOL.thy 
   242                 "(P=P')--> (~P'--> (Q=Q'))--> ((P|Q) = (P'|Q'))"
   242                 "(P=P')--> (~P'--> (Q=Q'))--> ((P|Q) = (P'|Q'))"
   243                 (fn _=> [blast_tac HOL_cs 1])
   243                 (fn _=> [Blast_tac 1])
   244 in  bind_thm("disj_cong",standard (impI RSN (2, th RS mp RS mp)))  end;
   244 in  bind_thm("disj_cong",standard (impI RSN (2, th RS mp RS mp)))  end;
   245 
   245 
   246 prove "eq_sym_conv" "(x=y) = (y=x)";
   246 prove "eq_sym_conv" "(x=y) = (y=x)";
   247 
   247 
   248 qed_goalw "o_apply" HOL.thy [o_def] "(f o g) x = f (g x)"
   248 qed_goalw "o_apply" HOL.thy [o_def] "(f o g) x = f (g x)"
   266 qed_goal "expand_if" HOL.thy
   266 qed_goal "expand_if" HOL.thy
   267     "P(if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))" (K [
   267     "P(if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))" (K [
   268 	res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1,
   268 	res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1,
   269          stac if_P 2,
   269          stac if_P 2,
   270          stac if_not_P 1,
   270          stac if_not_P 1,
   271          ALLGOALS (blast_tac HOL_cs)]);
   271          ALLGOALS (Blast_tac)]);
   272 
   272 
   273 qed_goal "split_if_asm" HOL.thy
   273 qed_goal "split_if_asm" HOL.thy
   274     "P(if Q then x else y) = (~((Q & ~P x) | (~Q & ~P y)))" (K [
   274     "P(if Q then x else y) = (~((Q & ~P x) | (~Q & ~P y)))"
   275 	stac expand_if 1,
   275     (K [stac expand_if 1,
   276         blast_tac HOL_cs 1]);
   276 	Blast_tac 1]);
   277 
   277 
   278 qed_goal "if_bool_eq" HOL.thy
   278 (*This form is useful for expanding IFs on the RIGHT of the ==> symbol*)
   279                    "(if P then Q else R) = ((P-->Q) & (~P-->R))"
   279 qed_goal "if_bool_eq_conj" HOL.thy
   280                    (K [rtac expand_if 1]);
   280     "(if P then Q else R) = ((P-->Q) & (~P-->R))"
       
   281     (K [rtac expand_if 1]);
       
   282 
       
   283 (*And this form is useful for expanding IFs on the LEFT*)
       
   284 qed_goal "if_bool_eq_disj" HOL.thy
       
   285     "(if P then Q else R) = ((P&Q) | (~P&R))"
       
   286     (K [stac expand_if 1,
       
   287 	Blast_tac 1]);
   281 
   288 
   282 
   289 
   283 (*** make simplification procedures for quantifier elimination ***)
   290 (*** make simplification procedures for quantifier elimination ***)
   284 
   291 
   285 structure Quantifier1 = Quantifier1Fun(
   292 structure Quantifier1 = Quantifier1Fun(
   352 
   359 
   353 fun Addsplits splits = (simpset_ref() := simpset() addsplits splits);
   360 fun Addsplits splits = (simpset_ref() := simpset() addsplits splits);
   354 fun Delsplits splits = (simpset_ref() := simpset() delsplits splits);
   361 fun Delsplits splits = (simpset_ref() := simpset() delsplits splits);
   355 
   362 
   356 qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"
   363 qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"
   357   (K [split_tac [expand_if] 1, blast_tac HOL_cs 1]);
   364   (K [split_tac [expand_if] 1, Blast_tac 1]);
   358 
   365 
   359 qed_goal "if_eq_cancel" HOL.thy "(if x = y then y else x) = x"
   366 qed_goal "if_eq_cancel" HOL.thy "(if x = y then y else x) = x"
   360   (K [split_tac [expand_if] 1, blast_tac HOL_cs 1]);
   367   (K [split_tac [expand_if] 1, Blast_tac 1]);
   361 
   368 
   362 (** 'if' congruence rules: neither included by default! *)
   369 (** 'if' congruence rules: neither included by default! *)
   363 
   370 
   364 (*Simplifies x assuming c and y assuming ~c*)
   371 (*Simplifies x assuming c and y assuming ~c*)
   365 qed_goal "if_cong" HOL.thy
   372 qed_goal "if_cong" HOL.thy
   386   grounds that it allows simplification of R in the two cases.*)
   393   grounds that it allows simplification of R in the two cases.*)
   387 
   394 
   388 val mksimps_pairs =
   395 val mksimps_pairs =
   389   [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
   396   [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
   390    ("All", [spec]), ("True", []), ("False", []),
   397    ("All", [spec]), ("True", []), ("False", []),
   391    ("If", [if_bool_eq RS iffD1])];
   398    ("If", [if_bool_eq_conj RS iffD1])];
   392 
   399 
   393 fun unsafe_solver prems = FIRST'[resolve_tac (reflexive_thm::TrueI::refl::prems),
   400 fun unsafe_solver prems = FIRST'[resolve_tac (reflexive_thm::TrueI::refl::prems),
   394 				 atac, etac FalseE];
   401 				 atac, etac FalseE];
   395 (*No premature instantiation of variables during simplification*)
   402 (*No premature instantiation of variables during simplification*)
   396 fun   safe_solver prems = FIRST'[match_tac (reflexive_thm::TrueI::prems),
   403 fun   safe_solver prems = FIRST'[match_tac (reflexive_thm::TrueI::prems),