src/HOL/simpdata.ML
 author berghofe Fri Aug 31 16:29:18 2001 +0200 (2001-08-31) changeset 11534 0494d0347f18 parent 11451 8abfb4f7bd02 child 11624 8a45c7abef04 permissions -rw-r--r--
Proof of True_implies_equals is stored with "open" derivation to
facilitate simplification of proof terms.
 clasohm@1465 ` 1` ```(* Title: HOL/simpdata.ML ``` clasohm@923 ` 2` ``` ID: \$Id\$ ``` clasohm@1465 ` 3` ``` Author: Tobias Nipkow ``` clasohm@923 ` 4` ``` Copyright 1991 University of Cambridge ``` clasohm@923 ` 5` oheimb@5304 ` 6` ```Instantiation of the generic simplifier for HOL. ``` clasohm@923 ` 7` ```*) ``` clasohm@923 ` 8` paulson@1984 ` 9` ```section "Simplifier"; ``` paulson@1984 ` 10` wenzelm@7357 ` 11` ```val [prem] = goal (the_context ()) "x==y ==> x=y"; ``` paulson@7031 ` 12` ```by (rewtac prem); ``` paulson@7031 ` 13` ```by (rtac refl 1); ``` paulson@7031 ` 14` ```qed "meta_eq_to_obj_eq"; ``` nipkow@4640 ` 15` oheimb@9023 ` 16` ```Goal "(%s. f s) = f"; ``` oheimb@9023 ` 17` ```br refl 1; ``` oheimb@9023 ` 18` ```qed "eta_contract_eq"; ``` oheimb@9023 ` 19` clasohm@923 ` 20` ```local ``` clasohm@923 ` 21` wenzelm@7357 ` 22` ``` fun prover s = prove_goal (the_context ()) s (fn _ => [(Blast_tac 1)]); ``` clasohm@923 ` 23` nipkow@2134 ` 24` ```in ``` nipkow@2134 ` 25` oheimb@5552 ` 26` ```(*Make meta-equalities. The operator below is Trueprop*) ``` oheimb@5552 ` 27` nipkow@6128 ` 28` ```fun mk_meta_eq r = r RS eq_reflection; ``` wenzelm@9832 ` 29` ```fun safe_mk_meta_eq r = mk_meta_eq r handle Thm.THM _ => r; ``` nipkow@6128 ` 30` nipkow@6128 ` 31` ```val Eq_TrueI = mk_meta_eq(prover "P --> (P = True)" RS mp); ``` nipkow@6128 ` 32` ```val Eq_FalseI = mk_meta_eq(prover "~P --> (P = False)" RS mp); ``` oheimb@5304 ` 33` nipkow@6128 ` 34` ```fun mk_eq th = case concl_of th of ``` nipkow@6128 ` 35` ``` Const("==",_)\$_\$_ => th ``` nipkow@6128 ` 36` ``` | _\$(Const("op =",_)\$_\$_) => mk_meta_eq th ``` nipkow@6128 ` 37` ``` | _\$(Const("Not",_)\$_) => th RS Eq_FalseI ``` nipkow@6128 ` 38` ``` | _ => th RS Eq_TrueI; ``` nipkow@6128 ` 39` ```(* last 2 lines requires all formulae to be of the from Trueprop(.) *) ``` oheimb@5304 ` 40` nipkow@6128 ` 41` ```fun mk_eq_True r = Some(r RS meta_eq_to_obj_eq RS Eq_TrueI); ``` oheimb@5552 ` 42` wenzelm@9713 ` 43` ```(*Congruence rules for = (instead of ==)*) ``` nipkow@6128 ` 44` ```fun mk_meta_cong rl = ``` nipkow@6128 ` 45` ``` standard(mk_meta_eq(replicate (nprems_of rl) meta_eq_to_obj_eq MRS rl)) ``` nipkow@6128 ` 46` ``` handle THM _ => ``` nipkow@6128 ` 47` ``` error("Premises and conclusion of congruence rules must be =-equalities"); ``` nipkow@3896 ` 48` nipkow@5975 ` 49` ```val not_not = prover "(~ ~ P) = P"; ``` clasohm@923 ` 50` nipkow@5975 ` 51` ```val simp_thms = [not_not] @ map prover ``` paulson@2082 ` 52` ``` [ "(x=x) = True", ``` nipkow@5975 ` 53` ``` "(~True) = False", "(~False) = True", ``` paulson@2082 ` 54` ``` "(~P) ~= P", "P ~= (~P)", "(P ~= Q) = (P = (~Q))", ``` nipkow@4640 ` 55` ``` "(True=P) = P", "(P=True) = P", "(False=P) = (~P)", "(P=False) = (~P)", ``` wenzelm@9713 ` 56` ``` "(True --> P) = P", "(False --> P) = True", ``` paulson@2082 ` 57` ``` "(P --> True) = True", "(P --> P) = True", ``` paulson@2082 ` 58` ``` "(P --> False) = (~P)", "(P --> ~P) = (~P)", ``` wenzelm@9713 ` 59` ``` "(P & True) = P", "(True & P) = P", ``` nipkow@2800 ` 60` ``` "(P & False) = False", "(False & P) = False", ``` nipkow@2800 ` 61` ``` "(P & P) = P", "(P & (P & Q)) = (P & Q)", ``` paulson@3913 ` 62` ``` "(P & ~P) = False", "(~P & P) = False", ``` wenzelm@9713 ` 63` ``` "(P | True) = True", "(True | P) = True", ``` nipkow@2800 ` 64` ``` "(P | False) = P", "(False | P) = P", ``` nipkow@2800 ` 65` ``` "(P | P) = P", "(P | (P | Q)) = (P | Q)", ``` paulson@3913 ` 66` ``` "(P | ~P) = True", "(~P | P) = True", ``` paulson@2082 ` 67` ``` "((~P) = (~Q)) = (P=Q)", ``` wenzelm@9713 ` 68` ``` "(!x. P) = P", "(? x. P) = P", "? x. x=t", "? x. t=x", ``` nipkow@11232 ` 69` ```(* needed for the one-point-rule quantifier simplification procs*) ``` nipkow@11232 ` 70` ```(*essential for termination!!*) ``` nipkow@11232 ` 71` ``` "(? x. x=t & P(x)) = P(t)", ``` nipkow@11232 ` 72` ``` "(? x. t=x & P(x)) = P(t)", ``` nipkow@11232 ` 73` ``` "(! x. x=t --> P(x)) = P(t)", ``` nipkow@11232 ` 74` ``` "(! x. t=x --> P(x)) = P(t)" ]; ``` clasohm@923 ` 75` nipkow@9875 ` 76` ```val imp_cong = standard(impI RSN ``` wenzelm@7357 ` 77` ``` (2, prove_goal (the_context ()) "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))" ``` nipkow@9875 ` 78` ``` (fn _=> [(Blast_tac 1)]) RS mp RS mp)); ``` paulson@1922 ` 79` paulson@1948 ` 80` ```(*Miniscoping: pushing in existential quantifiers*) ``` wenzelm@7648 ` 81` ```val ex_simps = map prover ``` wenzelm@3842 ` 82` ``` ["(EX x. P x & Q) = ((EX x. P x) & Q)", ``` wenzelm@3842 ` 83` ``` "(EX x. P & Q x) = (P & (EX x. Q x))", ``` wenzelm@3842 ` 84` ``` "(EX x. P x | Q) = ((EX x. P x) | Q)", ``` wenzelm@3842 ` 85` ``` "(EX x. P | Q x) = (P | (EX x. Q x))", ``` wenzelm@3842 ` 86` ``` "(EX x. P x --> Q) = ((ALL x. P x) --> Q)", ``` wenzelm@3842 ` 87` ``` "(EX x. P --> Q x) = (P --> (EX x. Q x))"]; ``` paulson@1948 ` 88` paulson@1948 ` 89` ```(*Miniscoping: pushing in universal quantifiers*) ``` paulson@1948 ` 90` ```val all_simps = map prover ``` wenzelm@3842 ` 91` ``` ["(ALL x. P x & Q) = ((ALL x. P x) & Q)", ``` wenzelm@3842 ` 92` ``` "(ALL x. P & Q x) = (P & (ALL x. Q x))", ``` wenzelm@3842 ` 93` ``` "(ALL x. P x | Q) = ((ALL x. P x) | Q)", ``` wenzelm@3842 ` 94` ``` "(ALL x. P | Q x) = (P | (ALL x. Q x))", ``` wenzelm@3842 ` 95` ``` "(ALL x. P x --> Q) = ((EX x. P x) --> Q)", ``` wenzelm@3842 ` 96` ``` "(ALL x. P --> Q x) = (P --> (ALL x. Q x))"]; ``` paulson@1948 ` 97` clasohm@923 ` 98` clasohm@923 ` 99` ```end; ``` clasohm@923 ` 100` wenzelm@7648 ` 101` ```bind_thms ("ex_simps", ex_simps); ``` wenzelm@7648 ` 102` ```bind_thms ("all_simps", all_simps); ``` berghofe@7711 ` 103` ```bind_thm ("not_not", not_not); ``` nipkow@9875 ` 104` ```bind_thm ("imp_cong", imp_cong); ``` wenzelm@7648 ` 105` nipkow@3654 ` 106` ```(* Elimination of True from asumptions: *) ``` nipkow@3654 ` 107` berghofe@11534 ` 108` ```local fun rd s = read_cterm (sign_of (the_context())) (s, propT); ``` berghofe@11534 ` 109` ```in val True_implies_equals = standard' (equal_intr ``` berghofe@11534 ` 110` ``` (implies_intr_hyps (implies_elim (assume (rd "True ==> PROP P")) TrueI)) ``` berghofe@11534 ` 111` ``` (implies_intr_hyps (implies_intr (rd "True") (assume (rd "PROP P"))))); ``` berghofe@11534 ` 112` ```end; ``` nipkow@3654 ` 113` wenzelm@7357 ` 114` ```fun prove nm thm = qed_goal nm (the_context ()) thm (fn _ => [(Blast_tac 1)]); ``` clasohm@923 ` 115` paulson@9511 ` 116` ```prove "eq_commute" "(a=b) = (b=a)"; ``` paulson@7623 ` 117` ```prove "eq_left_commute" "(P=(Q=R)) = (Q=(P=R))"; ``` paulson@7623 ` 118` ```prove "eq_assoc" "((P=Q)=R) = (P=(Q=R))"; ``` paulson@7623 ` 119` ```val eq_ac = [eq_commute, eq_left_commute, eq_assoc]; ``` paulson@7623 ` 120` paulson@9511 ` 121` ```prove "neq_commute" "(a~=b) = (b~=a)"; ``` paulson@9511 ` 122` clasohm@923 ` 123` ```prove "conj_commute" "(P&Q) = (Q&P)"; ``` clasohm@923 ` 124` ```prove "conj_left_commute" "(P&(Q&R)) = (Q&(P&R))"; ``` clasohm@923 ` 125` ```val conj_comms = [conj_commute, conj_left_commute]; ``` nipkow@2134 ` 126` ```prove "conj_assoc" "((P&Q)&R) = (P&(Q&R))"; ``` clasohm@923 ` 127` paulson@1922 ` 128` ```prove "disj_commute" "(P|Q) = (Q|P)"; ``` paulson@1922 ` 129` ```prove "disj_left_commute" "(P|(Q|R)) = (Q|(P|R))"; ``` paulson@1922 ` 130` ```val disj_comms = [disj_commute, disj_left_commute]; ``` nipkow@2134 ` 131` ```prove "disj_assoc" "((P|Q)|R) = (P|(Q|R))"; ``` paulson@1922 ` 132` clasohm@923 ` 133` ```prove "conj_disj_distribL" "(P&(Q|R)) = (P&Q | P&R)"; ``` clasohm@923 ` 134` ```prove "conj_disj_distribR" "((P|Q)&R) = (P&R | Q&R)"; ``` nipkow@1485 ` 135` paulson@1892 ` 136` ```prove "disj_conj_distribL" "(P|(Q&R)) = ((P|Q) & (P|R))"; ``` paulson@1892 ` 137` ```prove "disj_conj_distribR" "((P&Q)|R) = ((P|R) & (Q|R))"; ``` paulson@1892 ` 138` nipkow@2134 ` 139` ```prove "imp_conjR" "(P --> (Q&R)) = ((P-->Q) & (P-->R))"; ``` nipkow@2134 ` 140` ```prove "imp_conjL" "((P&Q) -->R) = (P --> (Q --> R))"; ``` nipkow@2134 ` 141` ```prove "imp_disjL" "((P|Q) --> R) = ((P-->R)&(Q-->R))"; ``` paulson@1892 ` 142` paulson@3448 ` 143` ```(*These two are specialized, but imp_disj_not1 is useful in Auth/Yahalom.ML*) ``` paulson@8114 ` 144` ```prove "imp_disj_not1" "(P --> Q | R) = (~Q --> P --> R)"; ``` paulson@8114 ` 145` ```prove "imp_disj_not2" "(P --> Q | R) = (~R --> P --> Q)"; ``` paulson@3448 ` 146` paulson@3904 ` 147` ```prove "imp_disj1" "((P-->Q)|R) = (P--> Q|R)"; ``` paulson@3904 ` 148` ```prove "imp_disj2" "(Q|(P-->R)) = (P--> Q|R)"; ``` paulson@3904 ` 149` nipkow@1485 ` 150` ```prove "de_Morgan_disj" "(~(P | Q)) = (~P & ~Q)"; ``` nipkow@1485 ` 151` ```prove "de_Morgan_conj" "(~(P & Q)) = (~P | ~Q)"; ``` paulson@3446 ` 152` ```prove "not_imp" "(~(P --> Q)) = (P & ~Q)"; ``` paulson@1922 ` 153` ```prove "not_iff" "(P~=Q) = (P = (~Q))"; ``` oheimb@4743 ` 154` ```prove "disj_not1" "(~P | Q) = (P --> Q)"; ``` oheimb@4743 ` 155` ```prove "disj_not2" "(P | ~Q) = (Q --> P)"; (* changes orientation :-( *) ``` nipkow@5975 ` 156` ```prove "imp_conv_disj" "(P --> Q) = ((~P) | Q)"; ``` nipkow@5975 ` 157` nipkow@5975 ` 158` ```prove "iff_conv_conj_imp" "(P = Q) = ((P --> Q) & (Q --> P))"; ``` nipkow@5975 ` 159` nipkow@1485 ` 160` wenzelm@9713 ` 161` ```(*Avoids duplication of subgoals after split_if, when the true and false ``` wenzelm@9713 ` 162` ``` cases boil down to the same thing.*) ``` nipkow@2134 ` 163` ```prove "cases_simp" "((P --> Q) & (~P --> Q)) = Q"; ``` nipkow@2134 ` 164` wenzelm@3842 ` 165` ```prove "not_all" "(~ (! x. P(x))) = (? x.~P(x))"; ``` paulson@1922 ` 166` ```prove "imp_all" "((! x. P x) --> Q) = (? x. P x --> Q)"; ``` wenzelm@3842 ` 167` ```prove "not_ex" "(~ (? x. P(x))) = (! x.~P(x))"; ``` paulson@1922 ` 168` ```prove "imp_ex" "((? x. P x) --> Q) = (! x. P x --> Q)"; ``` oheimb@1660 ` 169` nipkow@1655 ` 170` ```prove "ex_disj_distrib" "(? x. P(x) | Q(x)) = ((? x. P(x)) | (? x. Q(x)))"; ``` nipkow@1655 ` 171` ```prove "all_conj_distrib" "(!x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))"; ``` nipkow@1655 ` 172` nipkow@2134 ` 173` ```(* '&' congruence rule: not included by default! ``` nipkow@2134 ` 174` ``` May slow rewrite proofs down by as much as 50% *) ``` nipkow@2134 ` 175` wenzelm@9713 ` 176` ```let val th = prove_goal (the_context ()) ``` nipkow@2134 ` 177` ``` "(P=P')--> (P'--> (Q=Q'))--> ((P&Q) = (P'&Q'))" ``` paulson@7031 ` 178` ``` (fn _=> [(Blast_tac 1)]) ``` nipkow@2134 ` 179` ```in bind_thm("conj_cong",standard (impI RSN (2, th RS mp RS mp))) end; ``` nipkow@2134 ` 180` wenzelm@9713 ` 181` ```let val th = prove_goal (the_context ()) ``` nipkow@2134 ` 182` ``` "(Q=Q')--> (Q'--> (P=P'))--> ((P&Q) = (P'&Q'))" ``` paulson@7031 ` 183` ``` (fn _=> [(Blast_tac 1)]) ``` nipkow@2134 ` 184` ```in bind_thm("rev_conj_cong",standard (impI RSN (2, th RS mp RS mp))) end; ``` nipkow@2134 ` 185` nipkow@2134 ` 186` ```(* '|' congruence rule: not included by default! *) ``` nipkow@2134 ` 187` wenzelm@9713 ` 188` ```let val th = prove_goal (the_context ()) ``` nipkow@2134 ` 189` ``` "(P=P')--> (~P'--> (Q=Q'))--> ((P|Q) = (P'|Q'))" ``` paulson@7031 ` 190` ``` (fn _=> [(Blast_tac 1)]) ``` nipkow@2134 ` 191` ```in bind_thm("disj_cong",standard (impI RSN (2, th RS mp RS mp))) end; ``` nipkow@2134 ` 192` nipkow@2134 ` 193` ```prove "eq_sym_conv" "(x=y) = (y=x)"; ``` nipkow@2134 ` 194` paulson@5278 ` 195` paulson@5278 ` 196` ```(** if-then-else rules **) ``` paulson@5278 ` 197` paulson@7031 ` 198` ```Goalw [if_def] "(if True then x else y) = x"; ``` paulson@7031 ` 199` ```by (Blast_tac 1); ``` paulson@7031 ` 200` ```qed "if_True"; ``` nipkow@2134 ` 201` paulson@7031 ` 202` ```Goalw [if_def] "(if False then x else y) = y"; ``` paulson@7031 ` 203` ```by (Blast_tac 1); ``` paulson@7031 ` 204` ```qed "if_False"; ``` nipkow@2134 ` 205` paulson@7127 ` 206` ```Goalw [if_def] "P ==> (if P then x else y) = x"; ``` paulson@7031 ` 207` ```by (Blast_tac 1); ``` paulson@7031 ` 208` ```qed "if_P"; ``` oheimb@5304 ` 209` paulson@7127 ` 210` ```Goalw [if_def] "~P ==> (if P then x else y) = y"; ``` paulson@7031 ` 211` ```by (Blast_tac 1); ``` paulson@7031 ` 212` ```qed "if_not_P"; ``` nipkow@2134 ` 213` paulson@7031 ` 214` ```Goal "P(if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))"; ``` paulson@7031 ` 215` ```by (res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1); ``` paulson@7031 ` 216` ```by (stac if_P 2); ``` paulson@7031 ` 217` ```by (stac if_not_P 1); ``` paulson@7031 ` 218` ```by (ALLGOALS (Blast_tac)); ``` paulson@7031 ` 219` ```qed "split_if"; ``` paulson@7031 ` 220` paulson@7031 ` 221` ```Goal "P(if Q then x else y) = (~((Q & ~P x) | (~Q & ~P y)))"; ``` paulson@7031 ` 222` ```by (stac split_if 1); ``` paulson@7031 ` 223` ```by (Blast_tac 1); ``` paulson@7031 ` 224` ```qed "split_if_asm"; ``` nipkow@2134 ` 225` wenzelm@9384 ` 226` ```bind_thms ("if_splits", [split_if, split_if_asm]); ``` wenzelm@9384 ` 227` oheimb@11003 ` 228` ```bind_thm ("if_def2", read_instantiate [("P","\\x. x")] split_if); ``` oheimb@11003 ` 229` paulson@7031 ` 230` ```Goal "(if c then x else x) = x"; ``` paulson@7031 ` 231` ```by (stac split_if 1); ``` paulson@7031 ` 232` ```by (Blast_tac 1); ``` paulson@7031 ` 233` ```qed "if_cancel"; ``` oheimb@5304 ` 234` paulson@7031 ` 235` ```Goal "(if x = y then y else x) = x"; ``` paulson@7031 ` 236` ```by (stac split_if 1); ``` paulson@7031 ` 237` ```by (Blast_tac 1); ``` paulson@7031 ` 238` ```qed "if_eq_cancel"; ``` oheimb@5304 ` 239` paulson@4769 ` 240` ```(*This form is useful for expanding IFs on the RIGHT of the ==> symbol*) ``` paulson@7127 ` 241` ```Goal "(if P then Q else R) = ((P-->Q) & (~P-->R))"; ``` paulson@7031 ` 242` ```by (rtac split_if 1); ``` paulson@7031 ` 243` ```qed "if_bool_eq_conj"; ``` paulson@4769 ` 244` paulson@4769 ` 245` ```(*And this form is useful for expanding IFs on the LEFT*) ``` paulson@7031 ` 246` ```Goal "(if P then Q else R) = ((P&Q) | (~P&R))"; ``` paulson@7031 ` 247` ```by (stac split_if 1); ``` paulson@7031 ` 248` ```by (Blast_tac 1); ``` paulson@7031 ` 249` ```qed "if_bool_eq_disj"; ``` nipkow@2134 ` 250` nipkow@11232 ` 251` ```local ``` nipkow@11232 ` 252` ```val uncurry = prove_goal (the_context()) "P --> Q --> R ==> P & Q --> R" ``` nipkow@11232 ` 253` ``` (fn prems => [cut_facts_tac prems 1, Blast_tac 1]); ``` nipkow@11232 ` 254` nipkow@11232 ` 255` ```val iff_allI = allI RS ``` nipkow@11232 ` 256` ``` prove_goal (the_context()) "!x. P x = Q x ==> (!x. P x) = (!x. Q x)" ``` nipkow@11232 ` 257` ``` (fn prems => [cut_facts_tac prems 1, Blast_tac 1]) ``` nipkow@11232 ` 258` ```in ``` paulson@4351 ` 259` paulson@4351 ` 260` ```(*** make simplification procedures for quantifier elimination ***) ``` paulson@4351 ` 261` wenzelm@9851 ` 262` ```structure Quantifier1 = Quantifier1Fun ``` wenzelm@9851 ` 263` ```(struct ``` paulson@4351 ` 264` ``` (*abstract syntax*) ``` paulson@4351 ` 265` ``` fun dest_eq((c as Const("op =",_)) \$ s \$ t) = Some(c,s,t) ``` paulson@4351 ` 266` ``` | dest_eq _ = None; ``` paulson@4351 ` 267` ``` fun dest_conj((c as Const("op &",_)) \$ s \$ t) = Some(c,s,t) ``` paulson@4351 ` 268` ``` | dest_conj _ = None; ``` nipkow@11232 ` 269` ``` fun dest_imp((c as Const("op -->",_)) \$ s \$ t) = Some(c,s,t) ``` nipkow@11232 ` 270` ``` | dest_imp _ = None; ``` paulson@4351 ` 271` ``` val conj = HOLogic.conj ``` paulson@4351 ` 272` ``` val imp = HOLogic.imp ``` paulson@4351 ` 273` ``` (*rules*) ``` paulson@4351 ` 274` ``` val iff_reflection = eq_reflection ``` paulson@4351 ` 275` ``` val iffI = iffI ``` paulson@4351 ` 276` ``` val conjI= conjI ``` paulson@4351 ` 277` ``` val conjE= conjE ``` paulson@4351 ` 278` ``` val impI = impI ``` paulson@4351 ` 279` ``` val mp = mp ``` nipkow@11232 ` 280` ``` val uncurry = uncurry ``` paulson@4351 ` 281` ``` val exI = exI ``` paulson@4351 ` 282` ``` val exE = exE ``` nipkow@11232 ` 283` ``` val iff_allI = iff_allI ``` paulson@4351 ` 284` ```end); ``` paulson@4351 ` 285` nipkow@11232 ` 286` ```end; ``` nipkow@11232 ` 287` nipkow@4320 ` 288` ```local ``` nipkow@11220 ` 289` ```val ex_pattern = Thm.read_cterm (Theory.sign_of (the_context ())) ``` nipkow@11220 ` 290` ``` ("EX x. P(x) & Q(x)",HOLogic.boolT) ``` nipkow@11220 ` 291` ```val all_pattern = Thm.read_cterm (Theory.sign_of (the_context ())) ``` nipkow@11232 ` 292` ``` ("ALL x. P(x) --> Q(x)",HOLogic.boolT) ``` nipkow@4320 ` 293` ```in ``` nipkow@11220 ` 294` ```val defEX_regroup = mk_simproc "defined EX" [ex_pattern] ``` nipkow@11220 ` 295` ``` Quantifier1.rearrange_ex ``` nipkow@11220 ` 296` ```val defALL_regroup = mk_simproc "defined ALL" [all_pattern] ``` nipkow@11220 ` 297` ``` Quantifier1.rearrange_all ``` nipkow@4320 ` 298` ```end; ``` paulson@3913 ` 299` paulson@4351 ` 300` paulson@4351 ` 301` ```(*** Case splitting ***) ``` paulson@3913 ` 302` oheimb@5304 ` 303` ```structure SplitterData = ``` oheimb@5304 ` 304` ``` struct ``` oheimb@5304 ` 305` ``` structure Simplifier = Simplifier ``` oheimb@5552 ` 306` ``` val mk_eq = mk_eq ``` oheimb@5304 ` 307` ``` val meta_eq_to_iff = meta_eq_to_obj_eq ``` oheimb@5304 ` 308` ``` val iffD = iffD2 ``` oheimb@5304 ` 309` ``` val disjE = disjE ``` oheimb@5304 ` 310` ``` val conjE = conjE ``` oheimb@5304 ` 311` ``` val exE = exE ``` paulson@10231 ` 312` ``` val contrapos = contrapos_nn ``` paulson@10231 ` 313` ``` val contrapos2 = contrapos_pp ``` oheimb@5304 ` 314` ``` val notnotD = notnotD ``` oheimb@5304 ` 315` ``` end; ``` nipkow@4681 ` 316` oheimb@5304 ` 317` ```structure Splitter = SplitterFun(SplitterData); ``` oheimb@2263 ` 318` oheimb@5304 ` 319` ```val split_tac = Splitter.split_tac; ``` oheimb@5304 ` 320` ```val split_inside_tac = Splitter.split_inside_tac; ``` oheimb@5304 ` 321` ```val split_asm_tac = Splitter.split_asm_tac; ``` oheimb@5307 ` 322` ```val op addsplits = Splitter.addsplits; ``` oheimb@5307 ` 323` ```val op delsplits = Splitter.delsplits; ``` oheimb@5304 ` 324` ```val Addsplits = Splitter.Addsplits; ``` oheimb@5304 ` 325` ```val Delsplits = Splitter.Delsplits; ``` oheimb@4718 ` 326` nipkow@2134 ` 327` ```(*In general it seems wrong to add distributive laws by default: they ``` nipkow@2134 ` 328` ``` might cause exponential blow-up. But imp_disjL has been in for a while ``` wenzelm@9713 ` 329` ``` and cannot be removed without affecting existing proofs. Moreover, ``` nipkow@2134 ` 330` ``` rewriting by "(P|Q --> R) = ((P-->R)&(Q-->R))" might be justified on the ``` nipkow@2134 ` 331` ``` grounds that it allows simplification of R in the two cases.*) ``` nipkow@2134 ` 332` nipkow@2134 ` 333` ```val mksimps_pairs = ``` nipkow@2134 ` 334` ``` [("op -->", [mp]), ("op &", [conjunct1,conjunct2]), ``` nipkow@2134 ` 335` ``` ("All", [spec]), ("True", []), ("False", []), ``` paulson@4769 ` 336` ``` ("If", [if_bool_eq_conj RS iffD1])]; ``` nipkow@1758 ` 337` oheimb@5552 ` 338` ```(* ###FIXME: move to Provers/simplifier.ML ``` oheimb@5304 ` 339` ```val mk_atomize: (string * thm list) list -> thm -> thm list ``` oheimb@5304 ` 340` ```*) ``` oheimb@5552 ` 341` ```(* ###FIXME: move to Provers/simplifier.ML *) ``` oheimb@5304 ` 342` ```fun mk_atomize pairs = ``` oheimb@5304 ` 343` ``` let fun atoms th = ``` oheimb@5304 ` 344` ``` (case concl_of th of ``` oheimb@5304 ` 345` ``` Const("Trueprop",_) \$ p => ``` oheimb@5304 ` 346` ``` (case head_of p of ``` oheimb@5304 ` 347` ``` Const(a,_) => ``` oheimb@5304 ` 348` ``` (case assoc(pairs,a) of ``` oheimb@5304 ` 349` ``` Some(rls) => flat (map atoms ([th] RL rls)) ``` oheimb@5304 ` 350` ``` | None => [th]) ``` oheimb@5304 ` 351` ``` | _ => [th]) ``` oheimb@5304 ` 352` ``` | _ => [th]) ``` oheimb@5304 ` 353` ``` in atoms end; ``` oheimb@5304 ` 354` oheimb@11162 ` 355` ```fun mksimps pairs = (map mk_eq o mk_atomize pairs o forall_elim_vars_safe); ``` oheimb@5304 ` 356` nipkow@7570 ` 357` ```fun unsafe_solver_tac prems = ``` nipkow@7570 ` 358` ``` FIRST'[resolve_tac(reflexive_thm::TrueI::refl::prems), atac, etac FalseE]; ``` nipkow@7570 ` 359` ```val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac; ``` nipkow@7570 ` 360` oheimb@2636 ` 361` ```(*No premature instantiation of variables during simplification*) ``` nipkow@7570 ` 362` ```fun safe_solver_tac prems = ``` nipkow@7570 ` 363` ``` FIRST'[match_tac(reflexive_thm::TrueI::refl::prems), ``` nipkow@7570 ` 364` ``` eq_assume_tac, ematch_tac [FalseE]]; ``` nipkow@7570 ` 365` ```val safe_solver = mk_solver "HOL safe" safe_solver_tac; ``` oheimb@2443 ` 366` wenzelm@9713 ` 367` ```val HOL_basic_ss = ``` wenzelm@9713 ` 368` ``` empty_ss setsubgoaler asm_simp_tac ``` wenzelm@9713 ` 369` ``` setSSolver safe_solver ``` wenzelm@9713 ` 370` ``` setSolver unsafe_solver ``` wenzelm@9713 ` 371` ``` setmksimps (mksimps mksimps_pairs) ``` wenzelm@9713 ` 372` ``` setmkeqTrue mk_eq_True ``` wenzelm@9713 ` 373` ``` setmkcong mk_meta_cong; ``` oheimb@2443 ` 374` wenzelm@9713 ` 375` ```val HOL_ss = ``` wenzelm@9713 ` 376` ``` HOL_basic_ss addsimps ``` paulson@3446 ` 377` ``` ([triv_forall_equality, (* prunes params *) ``` nipkow@3654 ` 378` ``` True_implies_equals, (* prune asms `True' *) ``` oheimb@9023 ` 379` ``` eta_contract_eq, (* prunes eta-expansions *) ``` oheimb@4718 ` 380` ``` if_True, if_False, if_cancel, if_eq_cancel, ``` oheimb@5304 ` 381` ``` imp_disjL, conj_assoc, disj_assoc, ``` paulson@3904 ` 382` ``` de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_imp, ``` paulson@11451 ` 383` ``` disj_not1, not_all, not_ex, cases_simp, ``` wenzelm@11434 ` 384` ``` thm "the_eq_trivial", the_sym_eq_trivial, thm "plus_ac0.zero", thm "plus_ac0_zero_right"] ``` paulson@3446 ` 385` ``` @ ex_simps @ all_simps @ simp_thms) ``` nipkow@4032 ` 386` ``` addsimprocs [defALL_regroup,defEX_regroup] ``` wenzelm@4744 ` 387` ``` addcongs [imp_cong] ``` nipkow@4830 ` 388` ``` addsplits [split_if]; ``` paulson@2082 ` 389` wenzelm@11034 ` 390` ```fun hol_simplify rews = Simplifier.full_simplify (HOL_basic_ss addsimps rews); ``` wenzelm@11034 ` 391` ```fun hol_rewrite_cterm rews = ``` wenzelm@11034 ` 392` ``` #2 o Thm.dest_comb o #prop o Thm.crep_thm o Simplifier.full_rewrite (HOL_basic_ss addsimps rews); ``` wenzelm@11034 ` 393` wenzelm@11034 ` 394` paulson@6293 ` 395` ```(*Simplifies x assuming c and y assuming ~c*) ``` paulson@6293 ` 396` ```val prems = Goalw [if_def] ``` paulson@6293 ` 397` ``` "[| b=c; c ==> x=u; ~c ==> y=v |] ==> \ ``` paulson@6293 ` 398` ```\ (if b then x else y) = (if c then u else v)"; ``` paulson@6293 ` 399` ```by (asm_simp_tac (HOL_ss addsimps prems) 1); ``` paulson@6293 ` 400` ```qed "if_cong"; ``` paulson@6293 ` 401` paulson@7127 ` 402` ```(*Prevents simplification of x and y: faster and allows the execution ``` paulson@7127 ` 403` ``` of functional programs. NOW THE DEFAULT.*) ``` paulson@7031 ` 404` ```Goal "b=c ==> (if b then x else y) = (if c then x else y)"; ``` paulson@7031 ` 405` ```by (etac arg_cong 1); ``` paulson@7031 ` 406` ```qed "if_weak_cong"; ``` paulson@6293 ` 407` paulson@6293 ` 408` ```(*Prevents simplification of t: much faster*) ``` paulson@7031 ` 409` ```Goal "a = b ==> (let x=a in t(x)) = (let x=b in t(x))"; ``` paulson@7031 ` 410` ```by (etac arg_cong 1); ``` paulson@7031 ` 411` ```qed "let_weak_cong"; ``` paulson@6293 ` 412` paulson@7031 ` 413` ```Goal "f(if c then x else y) = (if c then f x else f y)"; ``` paulson@7031 ` 414` ```by (simp_tac (HOL_ss setloop (split_tac [split_if])) 1); ``` paulson@7031 ` 415` ```qed "if_distrib"; ``` nipkow@1655 ` 416` paulson@4327 ` 417` ```(*For expand_case_tac*) ``` paulson@7584 ` 418` ```val prems = Goal "[| P ==> Q(True); ~P ==> Q(False) |] ==> Q(P)"; ``` paulson@2948 ` 419` ```by (case_tac "P" 1); ``` paulson@2948 ` 420` ```by (ALLGOALS (asm_simp_tac (HOL_ss addsimps prems))); ``` paulson@7584 ` 421` ```qed "expand_case"; ``` paulson@2948 ` 422` paulson@4327 ` 423` ```(*Used in Auth proofs. Typically P contains Vars that become instantiated ``` paulson@4327 ` 424` ``` during unification.*) ``` paulson@2948 ` 425` ```fun expand_case_tac P i = ``` paulson@2948 ` 426` ``` res_inst_tac [("P",P)] expand_case i THEN ``` wenzelm@9713 ` 427` ``` Simp_tac (i+1) THEN ``` paulson@2948 ` 428` ``` Simp_tac i; ``` paulson@2948 ` 429` paulson@7584 ` 430` ```(*This lemma restricts the effect of the rewrite rule u=v to the left-hand ``` paulson@7584 ` 431` ``` side of an equality. Used in {Integ,Real}/simproc.ML*) ``` paulson@7584 ` 432` ```Goal "x=y ==> (x=z) = (y=z)"; ``` paulson@7584 ` 433` ```by (asm_simp_tac HOL_ss 1); ``` paulson@7584 ` 434` ```qed "restrict_to_left"; ``` paulson@2948 ` 435` wenzelm@7357 ` 436` ```(* default simpset *) ``` wenzelm@9713 ` 437` ```val simpsetup = ``` wenzelm@9713 ` 438` ``` [fn thy => (simpset_ref_of thy := HOL_ss addcongs [if_weak_cong]; thy)]; ``` berghofe@3615 ` 439` oheimb@4652 ` 440` wenzelm@5219 ` 441` ```(*** integration of simplifier with classical reasoner ***) ``` oheimb@2636 ` 442` wenzelm@5219 ` 443` ```structure Clasimp = ClasimpFun ``` wenzelm@8473 ` 444` ``` (structure Simplifier = Simplifier and Splitter = Splitter ``` wenzelm@9851 ` 445` ``` and Classical = Classical and Blast = Blast ``` oheimb@11344 ` 446` ``` val iffD1 = iffD1 val iffD2 = iffD2 val notE = notE ``` wenzelm@9851 ` 447` ``` val cla_make_elim = cla_make_elim); ``` oheimb@4652 ` 448` ```open Clasimp; ``` oheimb@2636 ` 449` oheimb@2636 ` 450` ```val HOL_css = (HOL_cs, HOL_ss); ``` nipkow@5975 ` 451` nipkow@5975 ` 452` wenzelm@8641 ` 453` nipkow@5975 ` 454` ```(*** A general refutation procedure ***) ``` wenzelm@9713 ` 455` nipkow@5975 ` 456` ```(* Parameters: ``` nipkow@5975 ` 457` nipkow@5975 ` 458` ``` test: term -> bool ``` nipkow@5975 ` 459` ``` tests if a term is at all relevant to the refutation proof; ``` nipkow@5975 ` 460` ``` if not, then it can be discarded. Can improve performance, ``` nipkow@5975 ` 461` ``` esp. if disjunctions can be discarded (no case distinction needed!). ``` nipkow@5975 ` 462` nipkow@5975 ` 463` ``` prep_tac: int -> tactic ``` nipkow@5975 ` 464` ``` A preparation tactic to be applied to the goal once all relevant premises ``` nipkow@5975 ` 465` ``` have been moved to the conclusion. ``` nipkow@5975 ` 466` nipkow@5975 ` 467` ``` ref_tac: int -> tactic ``` nipkow@5975 ` 468` ``` the actual refutation tactic. Should be able to deal with goals ``` nipkow@5975 ` 469` ``` [| A1; ...; An |] ==> False ``` wenzelm@9876 ` 470` ``` where the Ai are atomic, i.e. no top-level &, | or EX ``` nipkow@5975 ` 471` ```*) ``` nipkow@5975 ` 472` nipkow@5975 ` 473` ```fun refute_tac test prep_tac ref_tac = ``` nipkow@5975 ` 474` ``` let val nnf_simps = ``` nipkow@5975 ` 475` ``` [imp_conv_disj,iff_conv_conj_imp,de_Morgan_disj,de_Morgan_conj, ``` nipkow@5975 ` 476` ``` not_all,not_ex,not_not]; ``` nipkow@5975 ` 477` ``` val nnf_simpset = ``` nipkow@5975 ` 478` ``` empty_ss setmkeqTrue mk_eq_True ``` nipkow@5975 ` 479` ``` setmksimps (mksimps mksimps_pairs) ``` nipkow@5975 ` 480` ``` addsimps nnf_simps; ``` nipkow@5975 ` 481` ``` val prem_nnf_tac = full_simp_tac nnf_simpset; ``` nipkow@5975 ` 482` nipkow@5975 ` 483` ``` val refute_prems_tac = ``` nipkow@5975 ` 484` ``` REPEAT(eresolve_tac [conjE, exE] 1 ORELSE ``` nipkow@5975 ` 485` ``` filter_prems_tac test 1 ORELSE ``` paulson@6301 ` 486` ``` etac disjE 1) THEN ``` nipkow@11200 ` 487` ``` ((etac notE 1 THEN eq_assume_tac 1) ORELSE ``` nipkow@11200 ` 488` ``` ref_tac 1); ``` nipkow@5975 ` 489` ``` in EVERY'[TRY o filter_prems_tac test, ``` nipkow@6128 ` 490` ``` DETERM o REPEAT o etac rev_mp, prep_tac, rtac ccontr, prem_nnf_tac, ``` nipkow@5975 ` 491` ``` SELECT_GOAL (DEPTH_SOLVE refute_prems_tac)] ``` nipkow@5975 ` 492` ``` end; ```