The tactic
ACCEPT_TAC
(blastLib.BBLAST_PROVE
``?r:word8. 100w ≤₊ r + 251w ∧ r + 251w <₊ 200w``)
will prove your goal. If you’re doing this sort of thing a lot then you should
consider wrapping this process up into a custom tactic.
- Anthony
On 27 Jun 2014, at 18:49, Jiaqi Tan <tanji...@cmu.edu> wrote:
> Hi,
>
> Is it possible, using just the built-in HOL4 libraries/theorems, to
> automatically generate witnesses for an existentially quantified theorem over
> a finite set?
>
> Specifically, I have theorems of the form:
> {r − 5w} ⊆ {a | 100w ≤₊ a ∧ a <₊ 200w}
>
> Where the variable r is of type word8, and the set specification is also over
> word8.
>
> I tried simplifying using the following simplification sets:
>
> SIMP_TAC (std_ss ++ ARITH_ss ++ wordsLib.WORD_ss ++
> pred_setSimps.PRED_SET_ss) []
>
> And this yields the subgoal:
> val it = [([],``∃r. 100w ≤₊ r + 251w ∧ r + 251w <₊ 200w``)]: goal list
>
> Is it possible, using just the available theorems in the base HOL4
> installation, to automatically discharge such existential goals of membership
> in fixed size word sets?
>
> Thank you!
>
> Regards,
> Jiaqi Tan
>
>
>
> ------------------------------------------------------------------------------
> Open source business process management suite built on Java and Eclipse
> Turn processes into business applications with Bonita BPM Community Edition
> Quickly connect people, data, and systems into organized workflows
> Winner of BOSSIE, CODIE, OW2 and Gartner awards
> http://p.sf.net/sfu/Bonitasoft_______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
Open source business process management suite built on Java and Eclipse
Turn processes into business applications with Bonita BPM Community Edition
Quickly connect people, data, and systems into organized workflows
Winner of BOSSIE, CODIE, OW2 and Gartner awards
http://p.sf.net/sfu/Bonitasoft
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
