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
<mailto: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 <mailto: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
