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.
On 16 June 2016 at 01:09, Heiko Becker <heikobecke...@gmail.com> wrote:
> Hello everyone,
>
> I am currently learning HOL-Light and therefore working through the
> tutorial from the official page.[1]
> To get a feeling for the inductive definitions, I started a
> formalization similar to the semantics on page 109.
> My problem is that when I try to define some small step semantics I get
> a failure saying that I have some unbound free variables, but I cannot
> resolve this failure.
>
> 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".
>
>
> Can someone maybe help me figuring out where this failure comes from?
>
> Thanks in advance.
>
> Best regards,
>
> Heiko
>
> -----------------------
> [1]: https://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial.pdf
>
>
> ------------------------------------------------------------------------------
> 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
