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.
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
------------------------------------------------------------------------------
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
