Am 17.06.2016 4:04 nachm. schrieb "Mark Adams" <m...@proof-technologies.com
>:
>
> I think the problem now is that the syntactic form of the HOL term you
supply to 'new_inductive_definition' does not fit what is allowed by the
command, because you are not allowed to have compound implications (see the
HOL Light reference manual entry for 'new_inductive_definition'). So I
think you should get what you intend by transforming it to something
logically equivalent, i.e. change "A ==> B ==> C" to "A /\ B ==> C". The
error messages could be much better here.
>
> Mark.
>
Thank you. That was exactly the problem I had.
Heiko
>
> On 17/06/2016 10:51, Heiko Becker wrote:
>>
>> Hello,
>>
>>
>> On 06/16/2016 01:45 PM, Mark Adams wrote:
>>>
>>> Hi Heiko,
>>>
>>> That's strange, your corrected version goes through fine on my
computer. Do you still get the same problem if you restart HOL Light and
enter the corrected script? What version of HOL Light are you using?
>>>
>>> Mark.
>>>
>>>
>>
>>
>> It turns out, that I accidentally loaded both commands. The sstep
definition and the next one. And the failure came from the next one. But I
am unable to fix it currently:
>>
>> let bstep_RULES, bstep_INDUCT, bstep_CASES = new_inductive_definition
>> `(!(x:num) (e:exp) (s1:cmd) (s2:cmd) (env:num->real) (v:real).
>> exp_eval e env = v ==>
>> bstep s1 (upd_env x v env) s2 ==>
>> bstep (Ass x e s1) env s2) /\
>> (!(c:bexp) (s1:cmd) (s2:cmd) (t:cmd) (env:num->real).
>> bval c env = T ==>
>> bstep s1 env s2 ==>
>> bstep (Ite c s1 t) env s2) /\
>> (!(c:bexp) (s:cmd) (t1:cmd) (t2:cmd) (env:num->real).
>> bval c env = F ==>
>> bstep t1 env t2 ==>
>> bstep (Ite c s t1) env t2)`;;
>> Exception: Failure "dest_var: not a variable".
>>
>> I have tried removing some parts of the definition to see if I have an
undefined variable lying around but could not arrive at some obvious
failure.
>>
>> Best regards,
>>
>> Heiko
>>
>>>
>>> On 16/06/2016 10:01, Heiko Becker wrote:
>>>>
>>>>
>>>>
>>>> -------- Forwarded Message --------
>>>> Subject:
>>>> Re: [Hol-info] HOL-Light Beginner Questions
>>>> Date:
>>>> Thu, 16 Jun 2016 10:59:44 +0200
>>>> From:
>>>> Heiko Becker <heikobecke...@gmail.com>
>>>> To:
>>>> Ramana Kumar <ramana.ku...@cl.cam.ac.uk>
>>>> CC:
>>>> hol-info <hol-info@lists.sourceforge.net>
>>>>
>>>>
>>>>
>>>> On 06/16/2016 01:57 AM, Ramana Kumar wrote:
>>>>>
>>>>> I expect it could be because the Boolean constants are spelled "T"
and "F" rather than "true" and "false" in the logic, so the latter are
being treated as free variables.
>>>>>
>>>>
>>>>
>>>> Thank you for your explanation. I am getting closer to getting my
definition working.
>>>> I have changed it as follows:
>>>>
>>>> let sstep_RULES,sstep_INDUCT,sstep_CASES = new_inductive_definition
>>>> `(!x e s env v. exp_eval e env = v ==> sstep (Ass x e s) env s
(upd_env x v env)) /\
>>>> (!c s t env. bval c env = T ==> sstep (Ite c s t) env s env) /\
>>>> (!c s t env. bval c env = F ==> sstep (Ite c s t) env t env)`;;
>>>>
>>>> But now HOL-Light complains about some construct not being a variable:
>>>> Exception: Failure "dest_var: not a variable".
>>>>
>>>> Can you maybe help me again?
>>>>
>>>> Best regards,
>>>>
>>>> Heiko
>>>>
>>>>> On 16 June 2016 at 01:09, Heiko Becker <heikobecke...@gmail.com>
wrote:
>>>>>>
>>>>>>
>>>>>> My formalization:
>>>>>>
>>>>>> let exp_INDUCT, exp_REC= define_type
>>>>>> "exp = Var num
>>>>>> | Const real
>>>>>> | Plus exp exp
>>>>>> | Sub exp exp
>>>>>> | Mult exp exp
>>>>>> | Div exp exp";;
>>>>>>
>>>>>> let exp_eval_SIMPS = define
>>>>>> `(exp_eval (Var x) E = E x) /\
>>>>>> (exp_eval (Const r) E = r) /\
>>>>>> (exp_eval (Plus e1 e2) E = (exp_eval e1) E + (exp_eval e2) E) /\
>>>>>> (exp_eval (Sub e1 e2) E = (exp_eval e1) E - (exp_eval e2) E) /\
>>>>>> (exp_eval (Mult e1 e2) E = (exp_eval e1) E * (exp_eval e2) E) /\
>>>>>> (exp_eval (Div e1 e2) E = (exp_eval e1) E / (exp_eval e2) E)`;;
>>>>>>
>>>>>> let bexp_INDUCT, bexp_REC = define_type
>>>>>> "bexp = leq exp exp
>>>>>> | less exp exp";;
>>>>>>
>>>>>> let bval_SIMPS = define
>>>>>> `(bval (leq e1 e2) (E:num->real) = (exp_eval e1 E) <= (exp_eval
e2 E)) /\
>>>>>> (bval (less e1 e2) E = (exp_eval e1 E) < (exp_eval e2 E))`;;
>>>>>>
>>>>>> let cmd_INDUCT, cmd_REC = define_type
>>>>>> "cmd = Ass num exp cmd
>>>>>> | Ite bexp cmd cmd
>>>>>> | Nop";;
>>>>>>
>>>>>> let upd_env_simps1 = define
>>>>>> `upd_env (x:num) (v:real) (E:num->real) =(\y. if y = x then v
else E
>>>>>> y)`;;
>>>>>>
>>>>>> let sstep_RULES,sstep_INDUCT,sstep_CASES = new_inductive_definition
>>>>>> `(!x e s E v. exp_eval e E = v ==> sstep (Ass x e s) E s (upd_env
x v
>>>>>> E)) /\
>>>>>> (! c s t E. bval c E = true ==> sstep (Ite c s t) E s E) /\
>>>>>> (! c s t E. bval c E = false ==> sstep (Ite c s t) E t E)`;;
>>>>>>
>>>>>>
>>>>>> When loading the sstep definitions I get the following failure:
>>>>>> Exception: Failure "new_definition: term not closed".
>>>>>>
>>>>
>>>> Forwarding my message. Send from wrong mail account intially.
>>>>
>>>>
>>>>
------------------------------------------------------------------------------
>>>> What NetFlow Analyzer can do for you? Monitors network bandwidth and
traffic
>>>> patterns at an interface-level. Reveals which users, apps, and
protocols are
>>>> consuming the most bandwidth. Provides multi-vendor support for
NetFlow,
>>>> J-Flow, sFlow and other flows. Make informed decisions using capacity
planning
>>>> reports.
http://pubads.g.doubleclick.net/gampad/clk?id=1444514421&iu=/41014381
>>>>
>>>> _______________________________________________
>>>> hol-info mailing list
>>>> hol-info@lists.sourceforge.net
>>>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>
>>
>>
>>
------------------------------------------------------------------------------
>> What NetFlow Analyzer can do for you? Monitors network bandwidth and
traffic
>> patterns at an interface-level. Reveals which users, apps, and protocols
are
>> consuming the most bandwidth. Provides multi-vendor support for NetFlow,
>> J-Flow, sFlow and other flows. Make informed decisions using capacity
planning
>> reports. http://sdm.link/zohomanageengine
>>
>> _______________________________________________
>> hol-info mailing list
>> hol-info@lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
Attend Shape: An AT&T Tech Expo July 15-16. Meet us at AT&T Park in San
Francisco, CA to explore cutting-edge tech and listen to tech luminaries
present their vision of the future. This family event has something for
everyone, including kids. Get more information and register today.
http://sdm.link/attshape
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
