Commit 10c11261 authored by Heiko Becker's avatar Heiko Becker

Type in doc fixing and add lemma existential_rewriting to HOL dev, without proof

parent c42a6ab3
......@@ -39,7 +39,7 @@ Inductive exp (V:Type): Type :=
Definition perturb (r:R) (e:R) :=
Rmult r (Rplus 1 e).
(**
Abbreviation for the type of an environment
Abbreviation for the environment types
**)
Definition env_ty := nat -> R.
Definition analysisResult :Type := exp Q -> intv * error.
......
......@@ -36,6 +36,11 @@ let exp_IND, exp_REC = define_type
**)
let perturb = define
`(perturb:real->real->real) (r:real) (e:real) = r * ((&1) + e)`;;
(**
Abbreviations for the environment types
**)
new_type_abbrev("env_ty",`:num->real`);;
new_type_abbrev("analysisResult",`:(real)exp->intv#err`);;
(**
Define expression evaluation relation parametric by an "error" delta.
This value will be used later to express float computations using a perturbation
......@@ -213,6 +218,12 @@ let eval_0_det =
EXISTS_TAC `env:num->real` THEN ASM_SIMP_TAC[];
ASM_REWRITE_TAC[]]]]]]);;
g `! (b:binop) (e1:(real)exp) (e2:(real)exp) (eps:real) (cenv:env_ty) (v:real).
eval_exp eps cenv (Binop b e1 e2) v <=>
? v1 v2.
eval_exp eps cenv e1 v1 /\
eval_exp eps cenv e2 v2 /\
eval_exp eps (updEnv 2 v2 (updEnv 1 v1 cenv)) (Binop b (Var 1) (Var 2)) v`;;
(*
Using the parametric expressions, define boolean expressions for conditionals
*)
......
......@@ -4,6 +4,8 @@
*)
new_type_abbrev ("interval", `:real#real`);;
new_type_abbrev ("err", `:real`);;
new_type_abbrev ("intv", `:real#real`);;
new_type_abbrev ("error", `:real`);;
new_type_abbrev ("ann", `:intverval#err`);;
let mkInterval = define `mkInterval (a:real) (b:real) = (a,b)`;;
......
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