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