setup for refined facts handling;
authorwenzelm
Tue Sep 21 17:26:42 1999 +0200 (1999-09-21 ago)
changeset 755808b2d5c94b8a
parent 7557 1b977741f530
child 7559 1d2c099e98f7
setup for refined facts handling;
Method.bang_sectioned_args / Args.bang_facts;
eliminated asm_simp;
tuned improper methods;
src/Provers/simplifier.ML
     1.1 --- a/src/Provers/simplifier.ML	Tue Sep 21 17:24:50 1999 +0200
     1.2 +++ b/src/Provers/simplifier.ML	Tue Sep 21 17:26:42 1999 +0200
     1.3 @@ -417,7 +417,6 @@
     1.4  (* add / del *)
     1.5  
     1.6  val simpN = "simp";
     1.7 -val asm_simpN = "asm_simp";
     1.8  val addN = "add";
     1.9  val delN = "del";
    1.10  val onlyN = "only";
    1.11 @@ -468,29 +467,21 @@
    1.12    Args.$$$ onlyN >> K (map_local_simpset clear_ss, simp_add_local),
    1.13    Args.$$$ otherN >> K (I, I)];
    1.14  
    1.15 -val simp_args = Method.only_sectioned_args simp_modifiers';
    1.16 -
    1.17 -fun simp_meth thin cut tac ctxt = Method.METHOD (fn facts =>
    1.18 -  FIRSTGOAL
    1.19 -    ((if thin then REPEAT_DETERM o etac Drule.thin_rl else K all_tac)
    1.20 -      THEN' (if cut then Method.insert_tac facts else K all_tac)
    1.21 -      THEN' tac (get_local_simpset ctxt)));
    1.22 -
    1.23 -val simp_method = simp_args ooo simp_meth;
    1.24 +fun simp_method tac =
    1.25 +  (fn prems => fn ctxt => Method.METHOD (fn facts =>
    1.26 +    FIRSTGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_simpset ctxt))))
    1.27 +  |> Method.bang_sectioned_args simp_modifiers';
    1.28  
    1.29  
    1.30  (* setup_methods *)
    1.31  
    1.32  val setup_methods = Method.add_methods
    1.33 - [(simpN,               simp_method true true (CHANGED oo asm_full_simp_tac),
    1.34 -    "full simplification (including facts, excluding assumptions)"),
    1.35 -  (asm_simpN,           simp_method false true (CHANGED oo asm_full_simp_tac),
    1.36 -    "full simplification (including facts and assumptions)"),
    1.37 -  ("simp_tac",          simp_method false false simp_tac, "simp_tac (improper!)"),
    1.38 -  ("asm_simp_tac",      simp_method false false asm_simp_tac, "asm_simp_tac (improper!)"),
    1.39 -  ("full_simp_tac",     simp_method false false full_simp_tac, "full_simp_tac (improper!)"),
    1.40 -  ("asm_full_simp_tac", simp_method false false asm_full_simp_tac, "asm_full_simp_tac (improper!)"),
    1.41 -  ("asm_lr_simp_tac",   simp_method false false asm_lr_simp_tac, "asm_lr_simp_tac (improper!)")];
    1.42 + [(simpN,               simp_method (CHANGED oo asm_full_simp_tac), "full simplification"),
    1.43 +  ("simp_tac",          simp_method simp_tac, "simp_tac (improper!)"),
    1.44 +  ("asm_simp_tac",      simp_method asm_simp_tac, "asm_simp_tac (improper!)"),
    1.45 +  ("full_simp_tac",     simp_method full_simp_tac, "full_simp_tac (improper!)"),
    1.46 +  ("asm_full_simp_tac", simp_method asm_full_simp_tac, "asm_full_simp_tac (improper!)"),
    1.47 +  ("asm_lr_simp_tac",   simp_method asm_lr_simp_tac, "asm_lr_simp_tac (improper!)")];
    1.48  
    1.49  
    1.50