Hello Heiko,
It worked for me:
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)`;;
val sstep_RULES : thm =
|- (!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)
val sstep_INDUCT : thm =
|- !sstep'. (!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)
==> (!a0 a1 a2 a3. sstep a0 a1 a2 a3 ==> sstep' a0 a1 a2 a3)
val sstep_CASES : thm =
|- !a0 a1 a2 a3.
sstep a0 a1 a2 a3 <=>
(?x e v.
a0 = Ass x e a2 /\ a3 = upd_env x v a1 /\ exp_eval e a1 =
v) \/
(?c t. a0 = Ite c a2 t /\ a3 = a1 /\ (bval c a1 <=> T)) \/
(?c s. a0 = Ite c s a2 /\ a3 = a1 /\ (bval c a1 <=> F))
#
Regards,
Petros
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
https://lists.sourceforge.net/lists/listinfo/hol-info
--
Dr Petros Papapanagiotou
CISA, School of Informatics
The University of Edinburgh
Email: p...@ed.ac.uk
---
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
------------------------------------------------------------------------------
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
