Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more)

There hasn’t been any change in FIRST_ASSUM and FIRST_X_ASSUM. As always, FIRST_ASSUM leaves the assumption in place, and FIRST_X_ASSUM pulls it out. Michael From: Konrad Slind Date: Tuesday, 17 January 2017 at 15:22 To: "Norrish, Michael (Data61, Canberra City)"

Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more)

Oh, and the other thing that now bites (I think) is the FIRST_ASSUM --> FIRST_X_ASSUM replacement, which, if not done, can derail proofs. Konrad. On Mon, Jan 16, 2017 at 5:47 PM, wrote: > There were really two changes. If it was just a rename, then a >

Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more)

There were really two changes. If it was just a rename, then a find-and-replace (pat_assum -> pat_x_assum) would solve all the problems. However, there was another change to do with the handling of free variables in the pattern. As per the release notes, that change might require the use of

Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more)

If you are using the working copy of HOL from the git repository, you should check the release notes in HOLDIR/doc. We document major incompatibilities there. Note also that the last official release was K10. There is a tag for K11 in the repository, and some release notes for it, but it

Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more)

I have to say that the PAT_ASSUM --> PAT_X_ASSUM change has caused me a lot of pain. I can see the argument for the renaming, but it has broken a lot of proofs. Konrad. On Mon, Jan 16, 2017 at 1:06 PM, Thomas Tuerk wrote: > Hi Chun, > > PAT_ASSUM was renamed to

Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more)

Hi Chun, PAT_ASSUM was renamed to PAT_X_ASSUM in June. See commit fa81d70b67a61d6eddc6a517f968594c21be384d https://github.com/HOL-Theorem-Prover/HOL/commit/fa81d70b67a61d6eddc6a517f968594c21be384d for details and explanation. The reason was to unify naming. The X actually indicates that the

Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more)

Hi again, Actually I found a solution: val ALL_DISTINCT_CONS = store_thm("ALL_DISTINCT_CONS", ``!l. ALL_DISTINCT (h::l) ==> ALL_DISTINCT l``, RW_TAC std_ss [ALL_DISTINCT_FILTER,FILTER,MEM] THEN Q.PAT_X_ASSUM `!y. P` (MP_TAC o Q.SPEC `x`) THEN RW_TAC std_ss [FILTER_NEQ_NIL] THEN

[Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more)

Hi, HOL Reference said that, PAT_ASSUM "Finds the first assumption that matches the term argument, applies the theorem tactic to it, and removes this assumption.” But I found it actually doesn’t remove the assumption in latest Kananaskis 11. To see this, try the following goal (open listTheory