src/Provers/hypsubst.ML
 changeset 9628 53a62fd8b2dc parent 9592 abbd48606a0a child 9705 8eecca293907
equal 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;`