summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Thu, 13 Aug 1998 17:28:52 +0200 | |

changeset 5309 | 01c2b317da88 |

parent 5308 | 3ca4da83012c |

child 5310 | 3e14d6d66dab |

stac now handles definitions as well as equalities

src/FOL/IFOL.ML | file | annotate | diff | comparison | revisions | |

src/HOL/HOL.ML | file | annotate | diff | comparison | revisions |

--- a/src/FOL/IFOL.ML Thu Aug 13 17:28:19 1998 +0200 +++ b/src/FOL/IFOL.ML Thu Aug 13 17:28:52 1998 +0200 @@ -236,11 +236,29 @@ (** ~ b=a ==> ~ a=b **) val [not_sym] = compose(sym,2,contrapos); + +(* Two theorms for rewriting only one instance of a definition: + the first for definitions of formulae and the second for terms *) + +val prems = goal IFOL.thy "(A == B) ==> A <-> B"; +by (rewrite_goals_tac prems); +by (rtac iff_refl 1); +qed "def_imp_iff"; + +val prems = goal IFOL.thy "(A == B) ==> A = B"; +by (rewrite_goals_tac prems); +by (rtac refl 1); +qed "def_imp_eq"; + (*Substitution: rule and tactic*) bind_thm ("ssubst", sym RS subst); -(*Fails unless the substitution has an effect*) -fun stac th = CHANGED_GOAL (rtac (th RS ssubst)); +(*Apply an equality or definition ONCE. + Fails unless the substitution has an effect*) +fun stac th = + let val th' = th RS def_imp_eq handle _ => th + in CHANGED_GOAL (rtac (th' RS ssubst)) + end; (*A special case of ex1E that would otherwise need quantifier expansion*) qed_goal "ex1_equalsE" IFOL.thy @@ -382,20 +400,6 @@ by (REPEAT (eresolve_tac (prems RL [disjI1, disjI2]) 1)); qed "disj_imp_disj"; -(* The following two theorms are useful when rewriting only one instance *) -(* of a definition *) -(* first one for definitions of formulae and the second for terms *) - -val prems = goal IFOL.thy "(A == B) ==> A <-> B"; -by (rewrite_goals_tac prems); -by (rtac iff_refl 1); -qed "def_imp_iff"; - -val prems = goal IFOL.thy "(A == B) ==> A = B"; -by (rewrite_goals_tac prems); -by (rtac refl 1); -qed "def_imp_eq"; - (** strip ALL and --> from proved goal while preserving ALL-bound var names **)

--- a/src/HOL/HOL.ML Thu Aug 13 17:28:19 1998 +0200 +++ b/src/HOL/HOL.ML Thu Aug 13 17:28:52 1998 +0200 @@ -23,6 +23,11 @@ (fn prems => [rtac subst 1, resolve_tac prems 1, resolve_tac prems 1]); +val prems = goal thy "(A == B) ==> A = B"; +by (rewrite_goals_tac prems); +by (rtac refl 1); +qed "def_imp_eq"; + (*Useful with eresolve_tac for proving equalties from known equalities. a = b | | @@ -353,8 +358,12 @@ (** Standard abbreviations **) -(*Fails unless the substitution has an effect*) -fun stac th = CHANGED_GOAL (rtac (th RS ssubst)); +(*Apply an equality or definition ONCE. + Fails unless the substitution has an effect*) +fun stac th = + let val th' = th RS def_imp_eq handle _ => th + in CHANGED_GOAL (rtac (th' RS ssubst)) + end; fun strip_tac i = REPEAT(resolve_tac [impI,allI] i);