Note that this approach will fail if the term to be rewritten is under a
variable binding.
MP_REWRITE_TAC REAL_DIV_REFL ([], ``!x. x <> 0 ==> P (x/x)``)
gives back an unprovable x <> 0 as a new subgoal, and also fails to simplify the
bound x/x in the “original” branch. (Put `x*x + 1` in `x` if
Thank you Vincent for the tactic you provided. It saves time and lines of
code, indeed.
On Thu, Nov 22, 2012 at 3:31 PM, Vincent Aravantinos <
vincent.aravanti...@gmail.com> wrote:
> Hi list,
>
> I often face the following small but annoying problem:
>
> * Situation:
>- I have a theorem (sa
Hi Vincent,
I had exactly the same problem when I was doing long proofs in HOL Light
for the Flyspeck project. Later, I learned SSReflect extension in Coq
where the described rewriting issue was solved by "rewrite" tactic. Some
time ago, I implemented my version of a subset of SSReflect languag
Hi Vincent,
Peter Homeier has given a thorough treatment of just this problem some
time ago. It can be found in the structure "dep_rewrite". It seems you have
to load it before opening it. There is documentation in
src/1/dep_rewrite.sml
in the distribution.
Cheers,
Konrad.
On Thu, Nov 22, 20
Hi list,
I often face the following small but annoying problem:
* Situation:
- I have a theorem (say, "Th") of the form "P ==> t = u"
ex: REAL_DIV_REFL
(|- !x. ~(x = &0) ==> x / x = &1 in HOL-Light, |- !x. x <> 0 ==> (x
/ x = 1) in HOL4)
- the conclusion of my goal is a (big) te
