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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
