Sorry, I re-checked my Isabelle environment and found that the PolyML in
Isabelle is actually built by GCC (mingw versions), so my statement about
"PolyML cannot be built in ..." was completely wrong. The rest ideas should
still hold.
On 17 January 2017 at 13:36, Chun Tian (binghe) <binghe.l...@gmail.com>
wrote:
> 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)
>
>
--
---
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
