Commit f01a492d authored by Heiko Becker's avatar Heiko Becker
Browse files

Add intermediate proof state and type abbrev for environments

parent e892d8de
......@@ -7,7 +7,7 @@ needs "Infra/tactics.hl";;
Expressions will use binary operators.
Define them first
*)
let binop_INDUCT, binop_REC = define_type
let binop_IND, binop_REC = define_type
"binop = Plus | Sub | Mult | Div ";;
(*
Define an evaluation function for binary operators.
......@@ -22,7 +22,7 @@ let eval_binop = new_recursive_definition binop_REC
Define expressions parametric over some value type V.
Will ease reasoning about different instantiations later.
*)
let exp_INDUCT, exp_REC= define_type
let exp_IND, exp_REC= define_type
"exp = Var num
| Const V
| Binop binop exp exp";;
......@@ -35,6 +35,7 @@ let m_eps = define `m_eps:real = (&1)`;;
Define a perturbation function to ease writing of basic definitions
*)
let perturb = define `(perturb:real->real->real) = \r e. r * ((&1) + e)`;;
new_type_abbrev ("env_ty",`:num->real`);;
(*
Define expression evaluation relation parametric by an "error" delta.
This value will be used later to express float computations using a perturbation
......@@ -55,7 +56,7 @@ let eval_exp_RULES, eval_exp_IND, eval_exp_CASES = new_inductive_definition
Define real evaluation as a predicate on the epsilon of the evaluation relation
*)
let is_real_value = define
`is_real_value (e:(real)exp) (env:num->real) (v:real) = eval_exp (&0) env e v`;;
`is_real_value (e:(real)exp) (env:env_ty) (v:real) = eval_exp (&0) env e v`;;
let abs_leq_0_impl_zero =
prove (
......@@ -68,6 +69,14 @@ let abs_leq_0_impl_zero =
THEN ASM_REWRITE_TAC [SPECL [`abs d`; `&0:real`] REAL_LE_ANTISYM]
THEN MP_TAC (ASSUME `abs d = &0`)
THEN ASM_REWRITE_TAC [REAL_ABS_ZERO]);;
g `!e v1 v2 env.
eval_exp (&0) env e v1 /\ eval_exp (&0) env e v2 ==> v1 = v2`;;
e (MATCH_MP_TAC exp_IND THEN REPEAT STRIP_TAC);;
(* Now the problem with the "inversions" *)
e (SUBGOAL_TAC "v1_env_a" `eval_exp eps env (Var a) (env a)` [ALL_TAC]);;
e (ASM_REWRITE_TAC [eval_exp_CASES]);;
b();;
(*
Using the parametric expressions, define boolean expressions for conditionals
*)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment