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
