diff -r fc7e3f01bc40 -r 3bd113b8f7a6 src/HOL/simpdata.ML --- a/src/HOL/simpdata.ML Sat Nov 24 16:53:31 2001 +0100 +++ b/src/HOL/simpdata.ML Sat Nov 24 16:54:10 2001 +0100 @@ -6,206 +6,73 @@ Instantiation of the generic simplifier for HOL. *) -section "Simplifier"; - -val [prem] = goal (the_context ()) "x==y ==> x=y"; -by (rewtac prem); -by (rtac refl 1); -qed "meta_eq_to_obj_eq"; - -Goal "(%s. f s) = f"; -br refl 1; -qed "eta_contract_eq"; - - -fun prover s = prove_goal (the_context ()) s (fn _ => [(Blast_tac 1)]); - -bind_thm ("not_not", prover "(~ ~ P) = P"); - -bind_thms ("simp_thms", [not_not] @ map prover - ["(x=x) = True", - "(~True) = False", "(~False) = True", - "(~P) ~= P", "P ~= (~P)", "(P ~= Q) = (P = (~Q))", - "(True=P) = P", "(P=True) = P", "(False=P) = (~P)", "(P=False) = (~P)", - "(True --> P) = P", "(False --> P) = True", - "(P --> True) = True", "(P --> P) = True", - "(P --> False) = (~P)", "(P --> ~P) = (~P)", - "(P & True) = P", "(True & P) = P", - "(P & False) = False", "(False & P) = False", - "(P & P) = P", "(P & (P & Q)) = (P & Q)", - "(P & ~P) = False", "(~P & P) = False", - "(P | True) = True", "(True | P) = True", - "(P | False) = P", "(False | P) = P", - "(P | P) = P", "(P | (P | Q)) = (P | Q)", - "(P | ~P) = True", "(~P | P) = True", - "((~P) = (~Q)) = (P=Q)", - "(!x. P) = P", "(? x. P) = P", "? x. x=t", "? x. t=x", -(* needed for the one-point-rule quantifier simplification procs*) -(*essential for termination!!*) - "(? x. x=t & P(x)) = P(t)", - "(? x. t=x & P(x)) = P(t)", - "(! x. x=t --> P(x)) = P(t)", - "(! x. t=x --> P(x)) = P(t)"]); - -bind_thm ("imp_cong", standard (impI RSN - (2, prove_goal (the_context ()) "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))" - (fn _=> [(Blast_tac 1)]) RS mp RS mp))); - -(*Miniscoping: pushing in existential quantifiers*) -bind_thms ("ex_simps", map prover - ["(EX x. P x & Q) = ((EX x. P x) & Q)", - "(EX x. P & Q x) = (P & (EX x. Q x))", - "(EX x. P x | Q) = ((EX x. P x) | Q)", - "(EX x. P | Q x) = (P | (EX x. Q x))", - "(EX x. P x --> Q) = ((ALL x. P x) --> Q)", - "(EX x. P --> Q x) = (P --> (EX x. Q x))"]); - -(*Miniscoping: pushing in universal quantifiers*) -bind_thms ("all_simps", map prover - ["(ALL x. P x & Q) = ((ALL x. P x) & Q)", - "(ALL x. P & Q x) = (P & (ALL x. Q x))", - "(ALL x. P x | Q) = ((ALL x. P x) | Q)", - "(ALL x. P | Q x) = (P | (ALL x. Q x))", - "(ALL x. P x --> Q) = ((EX x. P x) --> Q)", - "(ALL x. P --> Q x) = (P --> (ALL x. Q x))"]); - - -fun prove nm thm = qed_goal nm (the_context ()) thm (fn _ => [(Blast_tac 1)]); - -prove "eq_commute" "(a=b) = (b=a)"; -prove "eq_left_commute" "(P=(Q=R)) = (Q=(P=R))"; -prove "eq_assoc" "((P=Q)=R) = (P=(Q=R))"; -bind_thms ("eq_ac", [eq_commute, eq_left_commute, eq_assoc]); - -prove "neq_commute" "(a~=b) = (b~=a)"; - -prove "conj_commute" "(P&Q) = (Q&P)"; -prove "conj_left_commute" "(P&(Q&R)) = (Q&(P&R))"; -bind_thms ("conj_comms", [conj_commute, conj_left_commute]); -prove "conj_assoc" "((P&Q)&R) = (P&(Q&R))"; - -prove "disj_commute" "(P|Q) = (Q|P)"; -prove "disj_left_commute" "(P|(Q|R)) = (Q|(P|R))"; -bind_thms ("disj_comms", [disj_commute, disj_left_commute]); -prove "disj_assoc" "((P|Q)|R) = (P|(Q|R))"; - -prove "conj_disj_distribL" "(P&(Q|R)) = (P&Q | P&R)"; -prove "conj_disj_distribR" "((P|Q)&R) = (P&R | Q&R)"; - -prove "disj_conj_distribL" "(P|(Q&R)) = ((P|Q) & (P|R))"; -prove "disj_conj_distribR" "((P&Q)|R) = ((P|R) & (Q|R))"; - -prove "imp_conjR" "(P --> (Q&R)) = ((P-->Q) & (P-->R))"; -prove "imp_conjL" "((P&Q) -->R) = (P --> (Q --> R))"; -prove "imp_disjL" "((P|Q) --> R) = ((P-->R)&(Q-->R))"; - -(*These two are specialized, but imp_disj_not1 is useful in Auth/Yahalom.ML*) -prove "imp_disj_not1" "(P --> Q | R) = (~Q --> P --> R)"; -prove "imp_disj_not2" "(P --> Q | R) = (~R --> P --> Q)"; - -prove "imp_disj1" "((P-->Q)|R) = (P--> Q|R)"; -prove "imp_disj2" "(Q|(P-->R)) = (P--> Q|R)"; +(* legacy ML bindings *) -prove "de_Morgan_disj" "(~(P | Q)) = (~P & ~Q)"; -prove "de_Morgan_conj" "(~(P & Q)) = (~P | ~Q)"; -prove "not_imp" "(~(P --> Q)) = (P & ~Q)"; -prove "not_iff" "(P~=Q) = (P = (~Q))"; -prove "disj_not1" "(~P | Q) = (P --> Q)"; -prove "disj_not2" "(P | ~Q) = (Q --> P)"; (* changes orientation :-( *) -prove "imp_conv_disj" "(P --> Q) = ((~P) | Q)"; - -prove "iff_conv_conj_imp" "(P = Q) = ((P --> Q) & (Q --> P))"; - - -(*Avoids duplication of subgoals after split_if, when the true and false - cases boil down to the same thing.*) -prove "cases_simp" "((P --> Q) & (~P --> Q)) = Q"; - -prove "not_all" "(~ (! x. P(x))) = (? x.~P(x))"; -prove "imp_all" "((! x. P x) --> Q) = (? x. P x --> Q)"; -prove "not_ex" "(~ (? x. P(x))) = (! x.~P(x))"; -prove "imp_ex" "((? x. P x) --> Q) = (! x. P x --> Q)"; - -prove "ex_disj_distrib" "(? x. P(x) | Q(x)) = ((? x. P(x)) | (? x. Q(x)))"; -prove "all_conj_distrib" "(!x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))"; - -(* '&' congruence rule: not included by default! - May slow rewrite proofs down by as much as 50% *) - -let val th = prove_goal (the_context ()) - "(P=P')--> (P'--> (Q=Q'))--> ((P&Q) = (P'&Q'))" - (fn _=> [(Blast_tac 1)]) -in bind_thm("conj_cong",standard (impI RSN (2, th RS mp RS mp))) end; - -let val th = prove_goal (the_context ()) - "(Q=Q')--> (Q'--> (P=P'))--> ((P&Q) = (P'&Q'))" - (fn _=> [(Blast_tac 1)]) -in bind_thm("rev_conj_cong",standard (impI RSN (2, th RS mp RS mp))) end; - -(* '|' congruence rule: not included by default! *) - -let val th = prove_goal (the_context ()) - "(P=P')--> (~P'--> (Q=Q'))--> ((P|Q) = (P'|Q'))" - (fn _=> [(Blast_tac 1)]) -in bind_thm("disj_cong",standard (impI RSN (2, th RS mp RS mp))) end; - -prove "eq_sym_conv" "(x=y) = (y=x)"; - - -(** if-then-else rules **) +val Eq_FalseI = thm "Eq_FalseI"; +val Eq_TrueI = thm "Eq_TrueI"; +val all_conj_distrib = thm "all_conj_distrib"; +val all_simps = thms "all_simps"; +val cases_simp = thm "cases_simp"; +val conj_assoc = thm "conj_assoc"; +val conj_comms = thms "conj_comms"; +val conj_commute = thm "conj_commute"; +val conj_cong = thm "conj_cong"; +val conj_disj_distribL = thm "conj_disj_distribL"; +val conj_disj_distribR = thm "conj_disj_distribR"; +val conj_left_commute = thm "conj_left_commute"; +val de_Morgan_conj = thm "de_Morgan_conj"; +val de_Morgan_disj = thm "de_Morgan_disj"; +val disj_assoc = thm "disj_assoc"; +val disj_comms = thms "disj_comms"; +val disj_commute = thm "disj_commute"; +val disj_cong = thm "disj_cong"; +val disj_conj_distribL = thm "disj_conj_distribL"; +val disj_conj_distribR = thm "disj_conj_distribR"; +val disj_left_commute = thm "disj_left_commute"; +val disj_not1 = thm "disj_not1"; +val disj_not2 = thm "disj_not2"; +val eq_ac = thms "eq_ac"; +val eq_assoc = thm "eq_assoc"; +val eq_commute = thm "eq_commute"; +val eq_left_commute = thm "eq_left_commute"; +val eq_sym_conv = thm "eq_sym_conv"; +val eta_contract_eq = thm "eta_contract_eq"; +val ex_disj_distrib = thm "ex_disj_distrib"; +val ex_simps = thms "ex_simps"; +val if_False = thm "if_False"; +val if_P = thm "if_P"; +val if_True = thm "if_True"; +val if_bool_eq_conj = thm "if_bool_eq_conj"; +val if_bool_eq_disj = thm "if_bool_eq_disj"; +val if_cancel = thm "if_cancel"; +val if_def2 = thm "if_def2"; +val if_eq_cancel = thm "if_eq_cancel"; +val if_not_P = thm "if_not_P"; +val if_splits = thms "if_splits"; +val iff_conv_conj_imp = thm "iff_conv_conj_imp"; +val imp_all = thm "imp_all"; +val imp_cong = thm "imp_cong"; +val imp_conjL = thm "imp_conjL"; +val imp_conjR = thm "imp_conjR"; +val imp_conv_disj = thm "imp_conv_disj"; +val imp_disj1 = thm "imp_disj1"; +val imp_disj2 = thm "imp_disj2"; +val imp_disjL = thm "imp_disjL"; +val imp_disj_not1 = thm "imp_disj_not1"; +val imp_disj_not2 = thm "imp_disj_not2"; +val imp_ex = thm "imp_ex"; +val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq"; +val neq_commute = thm "neq_commute"; +val not_all = thm "not_all"; +val not_ex = thm "not_ex"; +val not_iff = thm "not_iff"; +val not_imp = thm "not_imp"; +val not_not = thm "not_not"; +val rev_conj_cong = thm "rev_conj_cong"; +val simp_thms = thms "simp_thms"; +val split_if = thm "split_if"; +val split_if_asm = thm "split_if_asm"; -Goalw [if_def] "(if True then x else y) = x"; -by (Blast_tac 1); -qed "if_True"; - -Goalw [if_def] "(if False then x else y) = y"; -by (Blast_tac 1); -qed "if_False"; - -Goalw [if_def] "P ==> (if P then x else y) = x"; -by (Blast_tac 1); -qed "if_P"; - -Goalw [if_def] "~P ==> (if P then x else y) = y"; -by (Blast_tac 1); -qed "if_not_P"; - -Goal "P(if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))"; -by (res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1); -by (stac if_P 2); -by (stac if_not_P 1); -by (ALLGOALS (Blast_tac)); -qed "split_if"; - -Goal "P(if Q then x else y) = (~((Q & ~P x) | (~Q & ~P y)))"; -by (stac split_if 1); -by (Blast_tac 1); -qed "split_if_asm"; - -bind_thms ("if_splits", [split_if, split_if_asm]); - -bind_thm ("if_def2", read_instantiate [("P","\\x. x")] split_if); - -Goal "(if c then x else x) = x"; -by (stac split_if 1); -by (Blast_tac 1); -qed "if_cancel"; - -Goal "(if x = y then y else x) = x"; -by (stac split_if 1); -by (Blast_tac 1); -qed "if_eq_cancel"; - -(*This form is useful for expanding IFs on the RIGHT of the ==> symbol*) -Goal "(if P then Q else R) = ((P-->Q) & (~P-->R))"; -by (rtac split_if 1); -qed "if_bool_eq_conj"; - -(*And this form is useful for expanding IFs on the LEFT*) -Goal "(if P then Q else R) = ((P&Q) | (~P&R))"; -by (stac split_if 1); -by (Blast_tac 1); -qed "if_bool_eq_disj"; local val uncurry = prove_goal (the_context()) "P --> Q --> R ==> P & Q --> R" @@ -264,9 +131,6 @@ fun mk_meta_eq r = r RS eq_reflection; fun safe_mk_meta_eq r = mk_meta_eq r handle Thm.THM _ => r; -bind_thm ("Eq_TrueI", mk_meta_eq (prover "P --> (P = True)" RS mp)); -bind_thm ("Eq_FalseI", mk_meta_eq(prover "~P --> (P = False)" RS mp)); - fun mk_eq th = case concl_of th of Const("==",_)$_$_ => th | _$(Const("op =",_)$_$_) => mk_meta_eq th