src/Provers/hypsubst.ML
changeset 9628 53a62fd8b2dc
parent 9592 abbd48606a0a
child 9705 8eecca293907
equal deleted inserted replaced
9627:31d4a77c89d6 9628:53a62fd8b2dc
     1 (*  Title:      Provers/hypsubst.ML
     1 (*  Title:      Provers/hypsubst.ML
     2     ID:         $Id$
     2     ID:         $Id$
     3     Authors:    Martin D Coen, Tobias Nipkow and Lawrence C Paulson
     3     Authors:    Martin D Coen, Tobias Nipkow and Lawrence C Paulson
     4     Copyright   1995  University of Cambridge
     4     Copyright   1995  University of Cambridge
     5 
     5 
     6 Tactic to substitute using (at least) the assumption x=t in the rest of the
     6 Basic equational reasoning: (hyp_)subst method and symmetric attribute.
     7 subgoal, and to delete (at least) that assumption.
     7 
     8 Original version due to Martin Coen.
     8 Tactic to substitute using (at least) the assumption x=t in the rest
       
     9 of the subgoal, and to delete (at least) that assumption.  Original
       
    10 version due to Martin Coen.
     9 
    11 
    10 This version uses the simplifier, and requires it to be already present.
    12 This version uses the simplifier, and requires it to be already present.
    11 
    13 
    12 Test data:
    14 Test data:
    13 
    15 
   250 fun stac th =
   252 fun stac th =
   251   let val th' = th RS Data.rev_eq_reflection handle THM _ => th
   253   let val th' = th RS Data.rev_eq_reflection handle THM _ => th
   252   in CHANGED_GOAL (rtac (th' RS ssubst)) end;
   254   in CHANGED_GOAL (rtac (th' RS ssubst)) end;
   253 
   255 
   254 
   256 
   255 (* proof method setup *)
   257 (* proof methods *)
   256 
   258 
   257 val subst_meth = Method.goal_args' Attrib.local_thm stac;
   259 val subst_meth = Method.goal_args' Attrib.local_thm stac;
   258 val hyp_subst_meth = Method.goal_args (Scan.succeed ()) (K hyp_subst_tac);
   260 val hyp_subst_meth = Method.goal_args (Scan.succeed ()) (K hyp_subst_tac);
   259 
   261 
       
   262 
       
   263 (* attributes *)
       
   264 
       
   265 fun symmetric_rule thm =
       
   266   thm RS Drule.symmetric_thm handle THM _ =>
       
   267   thm RS Data.sym handle THM _ => error "Failed to apply symmetry of == or =";
       
   268 
       
   269 fun gen_symmetric x = Drule.rule_attribute (K symmetric_rule);
       
   270 
       
   271 
       
   272 (* theory setup *)
       
   273 
   260 val hypsubst_setup =
   274 val hypsubst_setup =
   261  [Method.add_methods
   275  [Method.add_methods
   262   [("hyp_subst", hyp_subst_meth, "substitution using an assumption (improper)"),
   276   [("hypsubst", hyp_subst_meth, "substitution using an assumption (improper)"),
   263    ("subst", subst_meth, "substitution")]];
   277    ("subst", subst_meth, "substitution")],
       
   278   Attrib.add_attributes
       
   279   [("symmetric", (gen_symmetric, gen_symmetric), "apply symmetry of == or =")]];
   264 
   280 
   265 end;
   281 end;