Commit 723edf12 authored by Heiko Becker's avatar Heiko Becker
Browse files

Finish porting HOL4 to new semantics

parent e41fc655
......@@ -6,7 +6,7 @@
**)
open preamble
open simpLib realTheory realLib RealArith
open AbbrevsTheory ExpressionsTheory RealSimpsTheory
open AbbrevsTheory ExpressionsTheory RealSimpsTheory DaisyTactics
open ExpressionAbbrevsTheory ErrorBoundsTheory IntervalArithTheory
open IntervalValidationTheory ErrorValidationTheory
......@@ -15,11 +15,15 @@ val _ = new_theory "CertificateChecker";
(** Certificate checking function **)
val CertificateChecker_def = Define
`CertificateChecker (e:real exp) (absenv:analysisResult) (P:precond) =
((validIntervalbounds e absenv P EMPTY) /\ (validErrorbound e absenv))`;
if (validIntervalbounds e absenv P LN)
then (validErrorbound e absenv LN)
else F`;
val CertificateCheckerCmd_def = Define
`CertificateCheckerCmd (f:real cmd) (absenv:analysisResult) (P:precond) =
((validIntervalboundsCmd f absenv P EMPTY) /\ (validErrorboundCmd f absenv))`;
if (validIntervalboundsCmd f absenv P LN)
then (validErrorboundCmd f absenv LN)
else F`;
(**
Soundness proof for the certificate checker.
......@@ -27,44 +31,56 @@ val CertificateCheckerCmd_def = Define
the real valued execution respects the precondition.
**)
val Certificate_checking_is_sound = store_thm ("Certificate_checking_is_sound",
``!(e:real exp) (absenv:analysisResult) P (VarEnv1 VarEnv2 ParamEnv:env)
(vR:real) (vF:real).
approxEnv VarEnv1 absenv VarEnv2 /\
eval_exp 0 VarEnv1 ParamEnv P e vR /\
eval_exp machineEpsilon VarEnv2 ParamEnv P e vF /\
``!(e:real exp) (absenv:analysisResult) (P:precond) (E1 E2:env)
(vR:real) (vF:real) fVars.
approxEnv E1 absenv fVars LN E2 /\
(!v.
v IN (domain fVars) ==>
?vR.
(E1 v = SOME vR) /\
FST (P v) <= vR /\ vR <= SND (P v)) /\
(domain (usedVars e)) SUBSET (domain fVars) /\
eval_exp 0 E1 e vR /\
eval_exp machineEpsilon E2 e vF /\
CertificateChecker e absenv P ==>
abs (vR - vF) <= (SND (absenv e))``,
(**
The proofs is a simple composition of the soundness proofs for the range
validator and the error bound validator.
**)
simp [CertificateChecker_def] \\
rpt strip_tac \\
Cases_on `absenv e` \\
rename1 `absenv e = (iv, err)` \\
Cases_on `iv` \\
rename1 `absenv e = ((elo, ehi), err)` \\
match_mp_tac validErrorbound_sound \\
qexistsl_tac [`e`, `VarEnv1`, `VarEnv2`, `ParamEnv`, `absenv`, `P`, `elo`, `ehi`, `EMPTY`] \\
fs[]);
simp [CertificateChecker_def]
\\ rpt strip_tac
\\ Cases_on `absenv e`
\\ rename1 `absenv e = (iv, err)`
\\ Cases_on `iv`
\\ rename1 `absenv e = ((elo, ehi), err)`
\\ match_mp_tac validErrorbound_sound
\\ qexistsl_tac [`e`, `E1`, `E2`, `absenv`, `P`, `elo`, `ehi`, `fVars`, `LN`]
\\ fs[]);
val CertificateCmd_checking_is_sound = store_thm ("CertificateCmd_checking_is_sound",
``!(f:real cmd) (absenv:analysisResult) (P:precond)
(VarEnv1 VarEnv2 ParamEnv:env) (outVars:num set) (envR envF:env).
approxEnv VarEnv1 absenv VarEnv2 /\
ssaPrg f EMPTY outVars /\
bstep f VarEnv1 ParamEnv P 0 Nop envR /\
bstep f VarEnv2 ParamEnv P machineEpsilon Nop envF /\
(E1 E2:env) (outVars:num_set) (vR vF:real) fVars.
approxEnv E1 absenv fVars LN E2 /\
(!v.
v IN (domain fVars) ==>
?vR.
(E1 v = SOME vR) /\
FST (P v) <= vR /\ vR <= SND (P v)) /\
domain (freeVars f) SUBSET (domain fVars) /\
ssa f fVars outVars /\
bstep f E1 0 vR /\
bstep f E2 machineEpsilon vF /\
CertificateCheckerCmd f absenv P ==>
abs (envR 0 - envF 0) <= (SND (absenv (Var 0)))``,
simp [CertificateCheckerCmd_def] \\
rpt strip_tac \\
match_mp_tac validErrorboundCmd_sound \\
Cases_on `absenv (Var 0)` \\
rename1 `absenv (Var 0) = (iv, err)` \\
Cases_on `iv` \\
rename1 `absenv (Var 0) = ((elo, ehi), err)` \\
qexistsl_tac [`f`, `absenv`, `VarEnv1`, `VarEnv2`, `ParamEnv`, `EMPTY`, `outVars`, `elo`, `ehi`, `P`] \\
fs[]);
abs (vR - vF) <= (SND (absenv (getRetExp f)))``,
simp [CertificateCheckerCmd_def]
\\ rpt strip_tac
\\ match_mp_tac validErrorboundCmd_sound
\\ Cases_on `absenv (getRetExp f)`
\\ rename1 `absenv (getRetExp f) = (iv, err)`
\\ Cases_on `iv`
\\ rename1 `absenv (getRetExp f) = ((elo, ehi), err)`
\\ qexistsl_tac [`f`, `absenv`, `E1`, `E2`, `outVars`, `fVars`, `LN`, `elo`, `ehi`, `P`]
\\ fs[]);
val _ = export_theory();
......@@ -18,4 +18,9 @@ val (approxEnv_rules, approxEnv_ind, approxEnv_cases) = Hol_reln `
(lookup x (union fVars dVars) = NONE) ==>
approxEnv (updEnv x v1 E1) A fVars (Insert x dVars) (updEnv x v2 E2))`;
val [approxRefl, approxUpdFree, approxUpdBound] = CONJ_LIST 3 approxEnv_rules;
save_thm ("approxRefl", approxRefl);
save_thm ("approxUpdFree", approxUpdFree);
save_thm ("approxUpdBound", approxUpdBound);
val _ = export_theory ();;
This diff is collapsed.
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