No, it’s actually my pleasure to make a little contribution.
For the Windows build issue, I think the correct path is to try to build
HOL using the PolyML (32bit and 64bit) and Cygwin environment shipped with
Isabelle2016-1 (installed on Windows 10). This version of PolyML is built
by Visual Studio 2010, it has normal executions, DLLs and other files, the
structure looks exactly like those we manually build on Linux and Mac.
PolyML cannot be built in Mingw32 or Cygwin32 using GCC compilers, thus
trying to build HOL in pure Cygwin environment results into failure. So we
can expect the final HOL build should be able to run standalone in Windows
CMD shell, if this plan works. MosML shouldn’t be considered at all.
I ever tried to make some initial fixes. The most obvious issue is that,
HOL’s ML code used functions from the “Posix” structure, but this structure
is not available on Windows. Some of these unavailable functions can be
found in OS structure, which is available on all platforms. Others may need
to be manually implemented on Windows using functions from OS or Windows
structures. Also, when detecting the location of executions, HOL’s ML code
doesn’t consider “.exe” as part of file name at all. These are all minor
issues is irrelevant to the theorem proving related code. However, I’m not
an experienced ML programmer (I’m actually a Common Lisp programmer), can’t
do complex ML coding at current moment …
On 17 January 2017 at 00:23, <michael.norr...@data61.csiro.au> wrote:
> 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 hasn’t been
> released due to issues with the Windows build. The change to PAT_ASSUM is
> documented in doc/next-release.md, which will eventually be renamed to
> the K12 release notes in all likelihood.
>
> The working repo did not have corrected .doc files for those functions
> though, so thank you very much for writing those!
>
> Michael
>
> On 17/1/17, 05:47, "Chun Tian (binghe)" <binghe.l...@gmail.com> wrote:
>
> 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 first):
>
> > g `!l. ALL_DISTINCT (h::l) ==> ALL_DISTINCT l`;
> val it =
> Proof manager status: 1 proof.
> 1. Incomplete goalstack:
> Initial goal:
> ∀l. ALL_DISTINCT (h::l) ⇒ ALL_DISTINCT l
> :
> proofs
>
> First I rewrite it:
>
> > e (RW_TAC std_ss [ALL_DISTINCT_FILTER,FILTER,MEM]);
> OK..
> 1 subgoal:
> val it =
> FILTER ($= x) l = [x]
> ------------------------------------
> 0. ∀x.
> (x = h) ∨ MEM x l ⇒
> ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])
> 1. MEM x l
> :
> proof
>
> Then I want to pick the assumption 0 and specialize the quantifier
> with `x`:
>
> > e (PAT_ASSUM ``!y. P`` (MP_TAC o Q.SPEC `x`));
> <<HOL message: inventing new type variable names: 'a>>
> OK..
> 1 subgoal:
> val it =
> ((x = h) ∨ MEM x l ⇒
> ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])) ⇒
> (FILTER ($= x) l = [x])
> ------------------------------------
> 0. ∀x.
> (x = h) ∨ MEM x l ⇒
> ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])
> 1. MEM x l
> :
> proof
> >
>
> Now you can see, the assumption 0 is still here. It’s not removed as
> the manual said.
>
> In Kananaskis 10, the behavior is exactly the same as described in the
> manual:
>
> - g `!l. ALL_DISTINCT (h::l) ==> ALL_DISTINCT l`;
> <<HOL message: inventing new type variable names: 'a>>
> > val it =
> Proof manager status: 1 proof.
> 1. Incomplete goalstack:
> Initial goal:
> ∀l. ALL_DISTINCT (h::l) ⇒ ALL_DISTINCT l
> : proofs
>
> - e (RW_TAC std_ss [ALL_DISTINCT_FILTER,FILTER,MEM]);
> OK..
> 1 subgoal:
> > val it =
> FILTER ($= x) l = [x]
> ------------------------------------
> 0. ∀x.
> (x = h) ∨ MEM x l ⇒
> ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) =
> [x])
> 1. MEM x l
> : proof
>
> - e (PAT_ASSUM ``!y. P`` (MP_TAC o Q.SPEC `x`));
> <<HOL message: inventing new type variable names: 'a>>
> OK..
> 1 subgoal:
> > val it =
> ((x = h) ∨ MEM x l ⇒
> ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])) ⇒
> (FILTER ($= x) l = [x])
> ------------------------------------
> MEM x l
> : proof
>
> See, the used assumption has been removed.
>
>
> Now let’s insist that, the behavior in latest Kananaskis 11 is more
> reasonable (thus we should update the manual), because later we may be able
> to use the assumption again for another different purpose. Now to finish
> the proof, in Kananaskis 10 a single rewrite almost finish the job using
> theorem FILTER_NEQ_NIL:
>
> - FILTER_NEQ_NIL;
> > val it =
> |- ∀P l. FILTER P l ≠ [] ⇔ ∃x. MEM x l ∧ P x
> : thm
> - e (RW_TAC std_ss [FILTER_NEQ_NIL]);
> OK..
> 1 subgoal:
> > val it =
>
> MEM h l
> ------------------------------------
> MEM h l
> : proof
>
> Now the goal is the same as the only assumption left:
>
> - e (FIRST_ASSUM ACCEPT_TAC);
> OK..
>
> Goal proved.
> [.] |- MEM h l
>
> Goal proved.
> [.]
> |- ((x = h) ∨ MEM x l ⇒
> ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])) ⇒
> (FILTER ($= x) l = [x])
>
> Goal proved.
> [..] |- FILTER ($= x) l = [x]
>
> But in Kananaskis 11 the same tactical cannot prove the theorem any
> more:
>
> > FILTER_NEQ_NIL;
> val it =
> |- ∀P l. FILTER P l ≠ [] ⇔ ∃x. MEM x l ∧ P x:
> thm
>
> > e (RW_TAC std_ss [FILTER_NEQ_NIL]);
> OK..
> 1 subgoal:
> val it =
>
> FILTER ($= x) l = [x]
> ------------------------------------
> 0. ∀x.
> (x = h) ∨ MEM x l ⇒
> ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])
> 1. MEM x l
> :
> proof
>
> In fact we’re going back to previous status before PAT_ASSUM was
> used! In short words, the following theorem definition doesn’t work any
> more: (it works in Kananaskis 10)
>
>
> (* BROKEN !!! *)
> 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
> PAT_ASSUM ``!y. P`` (MP_TAC o Q.SPEC `x`) THEN
> RW_TAC std_ss [FILTER_NEQ_NIL] THEN
> FIRST_ASSUM ACCEPT_TAC);
>
>
> Could anyone please explain these strange behaviors and point out a
> correct way to prove this theorem? (it’s actually part of the HOL-ACL2
> bridge, defined in “examples/acl2/ml/fmap_encodeScript.sml”)
>
> Best regards,
>
> Chun Tian
>
>
>
>
> ------------------------------------------------------------
> ------------------
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, SlashDot.org! http://sdm.link/slashdot
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
--
---
Chun Tian (binghe)
University of Bologna (Italy)
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, SlashDot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
