# HG changeset patch # User wenzelm # Date 967503331 -7200 # Node ID 2c5b42311eb0eb7ac7b1a8fc2d0361bfca651fc9 # Parent e33422a2eb9c3901e043bcaf6946068043e77168 cong setup now part of Simplifier; diff -r e33422a2eb9c -r 2c5b42311eb0 src/FOL/FOL.thy --- a/src/FOL/FOL.thy Tue Aug 29 00:54:22 2000 +0200 +++ b/src/FOL/FOL.thy Tue Aug 29 00:55:31 2000 +0200 @@ -55,7 +55,6 @@ use "simpdata.ML" setup simpsetup -setup cong_attrib_setup setup "Simplifier.method_setup Splitter.split_modifiers" setup Splitter.setup setup Clasimp.setup diff -r e33422a2eb9c -r 2c5b42311eb0 src/FOL/simpdata.ML --- a/src/FOL/simpdata.ML Tue Aug 29 00:54:22 2000 +0200 +++ b/src/FOL/simpdata.ML Tue Aug 29 00:55:31 2000 +0200 @@ -6,7 +6,7 @@ Simplification data for FOL *) -(*** Addition of rules to simpsets and clasets simultaneously ***) (* FIXME move to Provers/clasimp.ML? *) +(*** Addition of rules to simpsets and clasets simultaneously ***) (* FIXME move to Provers/clasimp.ML? *) infix 4 addIffs delIffs; @@ -30,15 +30,15 @@ fun delIff ((cla, simp), th) = (case FOLogic.dest_Trueprop (#prop (rep_thm th)) of - (Const ("Not", _) $ A) => - cla delrules [zero_var_indexes (th RS notE)] - | (Const("op <->", _) $ _ $ _) => - cla delrules [zero_var_indexes (th RS iffD2), - cla_make_elim (zero_var_indexes (th RS iffD1))] - | _ => cla delrules [th], + (Const ("Not", _) $ A) => + cla delrules [zero_var_indexes (th RS notE)] + | (Const("op <->", _) $ _ $ _) => + cla delrules [zero_var_indexes (th RS iffD2), + cla_make_elim (zero_var_indexes (th RS iffD1))] + | _ => cla delrules [th], simp delsimps [th]) handle TERM _ => (warning("DelIffs: ignoring conditional theorem\n" ^ - string_of_thm th); (cla, simp)); + string_of_thm th); (cla, simp)); fun store_clasimp (cla, simp) = (claset_ref () := cla; simpset_ref () := simp) in @@ -139,6 +139,7 @@ rule_by_tactic (REPEAT_FIRST (resolve_tac [meta_eq_to_obj_eq, def_imp_iff])); +(*Congruence rules for = or <-> (instead of ==)*) fun mk_meta_cong rl = standard(mk_meta_eq (mk_meta_prems rl)) handle THM _ => @@ -188,29 +189,29 @@ (*existential miniscoping*) val int_ex_simps = map int_prove_fun - ["(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) <-> (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))"]; (*classical rules*) val cla_ex_simps = map prove_fun ["(EX x. P(x) --> Q) <-> (ALL x. P(x)) --> Q", - "(EX x. P --> Q(x)) <-> P --> (EX x. Q(x))"]; + "(EX x. P --> Q(x)) <-> P --> (EX x. Q(x))"]; val ex_simps = int_ex_simps @ cla_ex_simps; (*universal miniscoping*) val int_all_simps = map int_prove_fun - ["(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))"]; + ["(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))"]; (*classical rules*) val cla_all_simps = map prove_fun ["(ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q", - "(ALL x. P | Q(x)) <-> P | (ALL x. Q(x))"]; + "(ALL x. P | Q(x)) <-> P | (ALL x. Q(x))"]; val all_simps = int_all_simps @ cla_all_simps; @@ -338,28 +339,6 @@ open Induction; -(* Add congruence rules for = or <-> (instead of ==) *) - -(* ###FIXME: Move to simplifier, - taking mk_meta_cong as input, eliminating addeqcongs and deleqcongs *) -infix 4 addcongs delcongs; -fun ss addcongs congs = ss addeqcongs (map mk_meta_cong congs); -fun ss delcongs congs = ss deleqcongs (map mk_meta_cong congs); -fun Addcongs congs = (simpset_ref() := simpset() addcongs congs); -fun Delcongs congs = (simpset_ref() := simpset() delcongs congs); - -val cong_add_global = Simplifier.change_global_ss (op addcongs); -val cong_del_global = Simplifier.change_global_ss (op delcongs); -val cong_add_local = Simplifier.change_local_ss (op addcongs); -val cong_del_local = Simplifier.change_local_ss (op delcongs); - -val cong_attrib_setup = - [Attrib.add_attributes [("cong", - (Attrib.add_del_args cong_add_global cong_del_global, - Attrib.add_del_args cong_add_local cong_del_local), - "declare Simplifier congruence rules")]]; - - val meta_simps = [triv_forall_equality, (* prunes params *) True_implies_equals]; (* prune asms `True' *) @@ -372,27 +351,28 @@ val triv_rls = [TrueI,refl,reflexive_thm,iff_refl,notFalseI]; fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls@prems), - atac, etac FalseE]; + atac, etac FalseE]; (*No premature instantiation of variables during simplification*) fun safe_solver prems = FIRST'[match_tac (triv_rls@prems), - eq_assume_tac, ematch_tac [FalseE]]; + eq_assume_tac, ematch_tac [FalseE]]; (*No simprules, but basic infastructure for simplification*) -val FOL_basic_ss = empty_ss setsubgoaler asm_simp_tac - addsimprocs [defALL_regroup,defEX_regroup] - setSSolver (mk_solver "FOL safe" safe_solver) - setSolver (mk_solver "FOL unsafe" unsafe_solver) - setmksimps (mksimps mksimps_pairs); - +val FOL_basic_ss = + empty_ss setsubgoaler asm_simp_tac + addsimprocs [defALL_regroup, defEX_regroup] + setSSolver (mk_solver "FOL safe" safe_solver) + setSolver (mk_solver "FOL unsafe" unsafe_solver) + setmksimps (mksimps mksimps_pairs) + setmkcong mk_meta_cong; (*intuitionistic simprules only*) -val IFOL_ss = - FOL_basic_ss addsimps (meta_simps @ IFOL_simps @ - int_ex_simps @ int_all_simps) +val IFOL_ss = + FOL_basic_ss addsimps (meta_simps @ IFOL_simps @ + int_ex_simps @ int_all_simps) addcongs [imp_cong]; -val cla_simps = +val cla_simps = [de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_all, not_ex, cases_simp] @ map prove_fun diff -r e33422a2eb9c -r 2c5b42311eb0 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Tue Aug 29 00:54:22 2000 +0200 +++ b/src/HOL/HOL.thy Tue Aug 29 00:55:31 2000 +0200 @@ -217,8 +217,7 @@ use "blastdata.ML" setup Blast.setup use "simpdata.ML" setup Simplifier.setup - setup "Simplifier.method_setup Splitter.split_modifiers" - setup simpsetup setup cong_attrib_setup + setup "Simplifier.method_setup Splitter.split_modifiers" setup simpsetup setup Splitter.setup setup Clasimp.setup setup iff_attrib_setup diff -r e33422a2eb9c -r 2c5b42311eb0 src/HOL/simpdata.ML --- a/src/HOL/simpdata.ML Tue Aug 29 00:54:22 2000 +0200 +++ b/src/HOL/simpdata.ML Tue Aug 29 00:55:31 2000 +0200 @@ -8,46 +8,46 @@ section "Simplifier"; -(*** Addition of rules to simpsets and clasets simultaneously ***) (* FIXME move to Provers/clasimp.ML? *) +(*** Addition of rules to simpsets and clasets simultaneously ***) (* FIXME move to Provers/clasimp.ML? *) infix 4 addIffs delIffs; -(*Takes UNCONDITIONAL theorems of the form A<->B to - the Safe Intr rule B==>A and +(*Takes UNCONDITIONAL theorems of the form A<->B to + the Safe Intr rule B==>A and the Safe Destruct rule A==>B. Also ~A goes to the Safe Elim rule A ==> ?R Failing other cases, A is added as a Safe Intr rule*) local val iff_const = HOLogic.eq_const HOLogic.boolT; - fun addIff ((cla, simp), th) = + fun addIff ((cla, simp), th) = (case HOLogic.dest_Trueprop (#prop (rep_thm th)) of (Const("Not", _) $ A) => cla addSEs [zero_var_indexes (th RS notE)] | (con $ _ $ _) => if con = iff_const - then cla addSIs [zero_var_indexes (th RS iffD2)] + then cla addSIs [zero_var_indexes (th RS iffD2)] addSDs [zero_var_indexes (th RS iffD1)] else cla addSIs [th] | _ => cla addSIs [th], simp addsimps [th]) - handle TERM _ => error ("AddIffs: theorem must be unconditional\n" ^ + handle TERM _ => error ("AddIffs: theorem must be unconditional\n" ^ string_of_thm th); - fun delIff ((cla, simp), th) = + fun delIff ((cla, simp), th) = (case HOLogic.dest_Trueprop (#prop (rep_thm th)) of - (Const ("Not", _) $ A) => - cla delrules [zero_var_indexes (th RS notE)] - | (con $ _ $ _) => - if con = iff_const - then cla delrules - [zero_var_indexes (th RS iffD2), - cla_make_elim (zero_var_indexes (th RS iffD1))] - else cla delrules [th] - | _ => cla delrules [th], + (Const ("Not", _) $ A) => + cla delrules [zero_var_indexes (th RS notE)] + | (con $ _ $ _) => + if con = iff_const + then cla delrules + [zero_var_indexes (th RS iffD2), + cla_make_elim (zero_var_indexes (th RS iffD1))] + else cla delrules [th] + | _ => cla delrules [th], simp delsimps [th]) - handle TERM _ => (warning("DelIffs: ignoring conditional theorem\n" ^ - string_of_thm th); (cla, simp)); + handle TERM _ => (warning("DelIffs: ignoring conditional theorem\n" ^ + string_of_thm th); (cla, simp)); fun store_clasimp (cla, simp) = (claset_ref () := cla; simpset_ref () := simp) in @@ -89,6 +89,7 @@ fun mk_eq_True r = Some(r RS meta_eq_to_obj_eq RS Eq_TrueI); +(*Congruence rules for = (instead of ==)*) fun mk_meta_cong rl = standard(mk_meta_eq(replicate (nprems_of rl) meta_eq_to_obj_eq MRS rl)) handle THM _ => @@ -101,45 +102,23 @@ "(~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", + "(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 & 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 | 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", + "(!x. P) = P", "(? x. P) = P", "? x. x=t", "? x. t=x", (*two needed for the one-point-rule quantifier simplification procs*) - "(? x. x=t & P(x)) = P(t)", (*essential for termination!!*) + "(? x. x=t & P(x)) = P(t)", (*essential for termination!!*) "(! x. t=x --> P(x)) = P(t)" ]; (*covers a stray case*) -(* Add congruence rules for = (instead of ==) *) - -(* ###FIXME: Move to simplifier, - taking mk_meta_cong as input, eliminating addeqcongs and deleqcongs *) -infix 4 addcongs delcongs; -fun ss addcongs congs = ss addeqcongs (map mk_meta_cong congs); -fun ss delcongs congs = ss deleqcongs (map mk_meta_cong congs); -fun Addcongs congs = (simpset_ref() := simpset() addcongs congs); -fun Delcongs congs = (simpset_ref() := simpset() delcongs congs); - -val cong_add_global = Simplifier.change_global_ss (op addcongs); -val cong_del_global = Simplifier.change_global_ss (op delcongs); -val cong_add_local = Simplifier.change_local_ss (op addcongs); -val cong_del_local = Simplifier.change_local_ss (op delcongs); - -val cong_attrib_setup = - [Attrib.add_attributes [("cong", - (Attrib.add_del_args cong_add_global cong_del_global, - Attrib.add_del_args cong_add_local cong_del_local), - "declare Simplifier congruence rules")]]; - - val imp_cong = impI RSN (2, prove_goal (the_context ()) "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))" (fn _=> [(Blast_tac 1)]) RS mp RS mp); @@ -235,8 +214,8 @@ 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.*) +(*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))"; @@ -250,19 +229,19 @@ (* '&' congruence rule: not included by default! May slow rewrite proofs down by as much as 50% *) -let val th = prove_goal (the_context ()) +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 ()) +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 ()) +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; @@ -393,7 +372,7 @@ (*In general it seems wrong to add distributive laws by default: they might cause exponential blow-up. But imp_disjL has been in for a while - and cannot be removed without affecting existing proofs. Moreover, + and cannot be removed without affecting existing proofs. Moreover, rewriting by "(P|Q --> R) = ((P-->R)&(Q-->R))" might be justified on the grounds that it allows simplification of R in the two cases.*) @@ -433,14 +412,16 @@ eq_assume_tac, ematch_tac [FalseE]]; val safe_solver = mk_solver "HOL safe" safe_solver_tac; -val HOL_basic_ss = empty_ss setsubgoaler asm_simp_tac - setSSolver safe_solver - setSolver unsafe_solver - setmksimps (mksimps mksimps_pairs) - setmkeqTrue mk_eq_True; +val HOL_basic_ss = + empty_ss setsubgoaler asm_simp_tac + setSSolver safe_solver + setSolver unsafe_solver + setmksimps (mksimps mksimps_pairs) + setmkeqTrue mk_eq_True + setmkcong mk_meta_cong; -val HOL_ss = - HOL_basic_ss addsimps +val HOL_ss = + HOL_basic_ss addsimps ([triv_forall_equality, (* prunes params *) True_implies_equals, (* prune asms `True' *) eta_contract_eq, (* prunes eta-expansions *) @@ -486,7 +467,7 @@ during unification.*) fun expand_case_tac P i = res_inst_tac [("P",P)] expand_case i THEN - Simp_tac (i+1) THEN + Simp_tac (i+1) THEN Simp_tac i; (*This lemma restricts the effect of the rewrite rule u=v to the left-hand @@ -496,9 +477,8 @@ qed "restrict_to_left"; (* default simpset *) -val simpsetup = - [fn thy => (simpset_ref_of thy := HOL_ss addcongs [if_weak_cong]; - thy)]; +val simpsetup = + [fn thy => (simpset_ref_of thy := HOL_ss addcongs [if_weak_cong]; thy)]; (*** integration of simplifier with classical reasoner ***) @@ -523,7 +503,7 @@ (*** A general refutation procedure ***) - + (* Parameters: test: term -> bool diff -r e33422a2eb9c -r 2c5b42311eb0 src/Sequents/simpdata.ML --- a/src/Sequents/simpdata.ML Tue Aug 29 00:54:22 2000 +0200 +++ b/src/Sequents/simpdata.ML Tue Aug 29 00:55:31 2000 +0200 @@ -10,10 +10,10 @@ (*** Rewrite rules ***) -fun prove_fun s = - (writeln s; +fun prove_fun s = + (writeln s; prove_goal LK.thy s - (fn prems => [ (cut_facts_tac prems 1), + (fn prems => [ (cut_facts_tac prems 1), (fast_tac (pack() add_safes [subst]) 1) ])); val conj_simps = map prove_fun @@ -34,7 +34,7 @@ val imp_simps = map prove_fun ["|- (P --> False) <-> ~P", "|- (P --> True) <-> True", - "|- (False --> P) <-> True", "|- (True --> P) <-> P", + "|- (False --> P) <-> True", "|- (True --> P) <-> P", "|- (P --> P) <-> True", "|- (P --> ~P) <-> ~P"]; val iff_simps = map prove_fun @@ -44,40 +44,40 @@ val quant_simps = map prove_fun - ["|- (ALL x. P) <-> P", + ["|- (ALL x. P) <-> P", "|- (ALL x. x=t --> P(x)) <-> P(t)", "|- (ALL x. t=x --> P(x)) <-> P(t)", "|- (EX x. P) <-> P", - "|- (EX x. x=t & P(x)) <-> P(t)", + "|- (EX x. x=t & P(x)) <-> P(t)", "|- (EX x. t=x & P(x)) <-> P(t)"]; (*** Miniscoping: pushing quantifiers in We do NOT distribute of ALL over &, or dually that of EX over | - Baaz and Leitsch, On Skolemization and Proof Complexity (1994) + Baaz and Leitsch, On Skolemization and Proof Complexity (1994) show that this step can increase proof length! ***) (*existential miniscoping*) -val ex_simps = map prove_fun +val ex_simps = map prove_fun ["|- (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))"]; + "|- (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))"]; (*universal miniscoping*) val all_simps = map prove_fun ["|- (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))", - "|- (ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q", - "|- (ALL x. P | Q(x)) <-> P | (ALL x. Q(x))"]; + "|- (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))", + "|- (ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q", + "|- (ALL x. P | Q(x)) <-> P | (ALL x. Q(x))"]; (*These are NOT supplied by default!*) val distrib_simps = map prove_fun - ["|- P & (Q | R) <-> P&Q | P&R", + ["|- P & (Q | R) <-> P&Q | P&R", "|- (Q | R) & P <-> Q&P | R&P", "|- (P | Q --> R) <-> (P --> R) & (Q --> R)"]; @@ -91,29 +91,29 @@ case concl_of r of Const("Trueprop",_) $ Abs(_,_,a) $ Abs(_,_,c) => (case (forms_of_seq a, forms_of_seq c) of - ([], [p]) => - (case p of - Const("op -->",_)$_$_ => atomize(r RS mp_R) - | Const("op &",_)$_$_ => atomize(r RS conjunct1) @ - atomize(r RS conjunct2) - | Const("All",_)$_ => atomize(r RS spec) - | Const("True",_) => [] (*True is DELETED*) - | Const("False",_) => [] (*should False do something?*) - | _ => [r]) + ([], [p]) => + (case p of + Const("op -->",_)$_$_ => atomize(r RS mp_R) + | Const("op &",_)$_$_ => atomize(r RS conjunct1) @ + atomize(r RS conjunct2) + | Const("All",_)$_ => atomize(r RS spec) + | Const("True",_) => [] (*True is DELETED*) + | Const("False",_) => [] (*should False do something?*) + | _ => [r]) | _ => []) (*ignore theorem unless it has precisely one conclusion*) | _ => [r]; Goal "|- ~P ==> |- (P <-> False)"; by (etac (thinR RS cut) 1); -by (Fast_tac 1); +by (Fast_tac 1); qed "P_iff_F"; val iff_reflection_F = P_iff_F RS iff_reflection; Goal "|- P ==> |- (P <-> True)"; by (etac (thinR RS cut) 1); -by (Fast_tac 1); +by (Fast_tac 1); qed "P_iff_T"; val iff_reflection_T = P_iff_T RS iff_reflection; @@ -122,22 +122,23 @@ fun mk_meta_eq th = case concl_of th of Const("==",_)$_$_ => th | Const("Trueprop",_) $ Abs(_,_,a) $ Abs(_,_,c) => - (case (forms_of_seq a, forms_of_seq c) of - ([], [p]) => - (case p of - (Const("op =",_)$_$_) => th RS eq_reflection - | (Const("op <->",_)$_$_) => th RS iff_reflection - | (Const("Not",_)$_) => th RS iff_reflection_F - | _ => th RS iff_reflection_T) - | _ => error ("addsimps: unable to use theorem\n" ^ - string_of_thm th)); + (case (forms_of_seq a, forms_of_seq c) of + ([], [p]) => + (case p of + (Const("op =",_)$_$_) => th RS eq_reflection + | (Const("op <->",_)$_$_) => th RS iff_reflection + | (Const("Not",_)$_) => th RS iff_reflection_F + | _ => th RS iff_reflection_T) + | _ => error ("addsimps: unable to use theorem\n" ^ + string_of_thm th)); (*Replace premises x=y, X<->Y by X==Y*) -val mk_meta_prems = - rule_by_tactic +val mk_meta_prems = + rule_by_tactic (REPEAT_FIRST (resolve_tac [meta_eq_to_obj_eq, def_imp_iff])); +(*Congruence rules for = or <-> (instead of ==)*) fun mk_meta_cong rl = standard(mk_meta_eq (mk_meta_prems rl)) handle THM _ => @@ -147,7 +148,7 @@ (*** Named rewrite rules ***) fun prove nm thm = qed_goal nm LK.thy thm - (fn prems => [ (cut_facts_tac prems 1), + (fn prems => [ (cut_facts_tac prems 1), (fast_tac LK_pack 1) ]); prove "conj_commute" "|- P&Q <-> Q&P"; @@ -177,26 +178,26 @@ prove "not_iff" "|- ~(P <-> Q) <-> (P <-> ~Q)"; -val [p1,p2] = Goal +val [p1,p2] = Goal "[| |- P <-> P'; |- P' ==> |- Q <-> Q' |] ==> |- (P-->Q) <-> (P'-->Q')"; by (lemma_tac p1 1); by (Safe_tac 1); -by (REPEAT (rtac cut 1 - THEN - DEPTH_SOLVE_1 (resolve_tac [thinL, thinR, p2 COMP monotonic] 1) - THEN - Safe_tac 1)); +by (REPEAT (rtac cut 1 + THEN + DEPTH_SOLVE_1 (resolve_tac [thinL, thinR, p2 COMP monotonic] 1) + THEN + Safe_tac 1)); qed "imp_cong"; -val [p1,p2] = Goal +val [p1,p2] = Goal "[| |- P <-> P'; |- P' ==> |- Q <-> Q' |] ==> |- (P&Q) <-> (P'&Q')"; by (lemma_tac p1 1); by (Safe_tac 1); -by (REPEAT (rtac cut 1 - THEN - DEPTH_SOLVE_1 (resolve_tac [thinL, thinR, p2 COMP monotonic] 1) - THEN - Safe_tac 1)); +by (REPEAT (rtac cut 1 + THEN + DEPTH_SOLVE_1 (resolve_tac [thinL, thinR, p2 COMP monotonic] 1) + THEN + Safe_tac 1)); qed "conj_cong"; Goal "|- (x=y) <-> (y=x)"; @@ -229,32 +230,26 @@ (*** Standard simpsets ***) -(*Add congruence rules for = or <-> (instead of ==) *) -infix 4 addcongs delcongs; -fun ss addcongs congs = ss addeqcongs (map mk_meta_cong congs); -fun ss delcongs congs = ss deleqcongs (map mk_meta_cong congs); - -fun Addcongs congs = (simpset_ref() := simpset() addcongs congs); -fun Delcongs congs = (simpset_ref() := simpset() delcongs congs); - val triv_rls = [FalseL, TrueR, basic, refl, iff_refl, reflexive_thm]; fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls@prems), - assume_tac]; + assume_tac]; (*No premature instantiation of variables during simplification*) fun safe_solver prems = FIRST'[fn i => DETERM (match_tac (triv_rls@prems) i), - eq_assume_tac]; + eq_assume_tac]; (*No simprules, but basic infrastructure for simplification*) -val LK_basic_ss = empty_ss setsubgoaler asm_simp_tac - setSSolver (mk_solver "safe" safe_solver) - setSolver (mk_solver "unsafe" unsafe_solver) - setmksimps (map mk_meta_eq o atomize o gen_all); +val LK_basic_ss = + empty_ss setsubgoaler asm_simp_tac + setSSolver (mk_solver "safe" safe_solver) + setSolver (mk_solver "unsafe" unsafe_solver) + setmksimps (map mk_meta_eq o atomize o gen_all) + setmkcong mk_meta_cong; val LK_simps = [triv_forall_equality, (* prunes params *) - refl RS P_iff_T] @ - conj_simps @ disj_simps @ not_simps @ + refl RS P_iff_T] @ + conj_simps @ disj_simps @ not_simps @ imp_simps @ iff_simps @quant_simps @ all_simps @ ex_simps @ [de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2] @ map prove_fun @@ -262,8 +257,10 @@ "|- ~ ~ P <-> P", "|- (~P --> P) <-> P", "|- (~P <-> ~Q) <-> (P<->Q)"]; -val LK_ss = LK_basic_ss addsimps LK_simps addeqcongs [left_cong] - addcongs [imp_cong]; +val LK_ss = + LK_basic_ss addsimps LK_simps + addeqcongs [left_cong] + addcongs [imp_cong]; simpset_ref() := LK_ss;