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