Commit 2ea56862 authored by Heiko Becker's avatar Heiko Becker
Browse files

Remove currently not used translationscript from master branch

parent 110af488
open preamble
open simpLib realTheory realLib RealArith
open ml_translatorTheory ml_translatorLib realProgTheory;
open AbbrevsTheory ExpressionsTheory RealSimpsTheory
open ExpressionAbbrevsTheory ErrorBoundsTheory IntervalArithTheory
open IntervalValidationTheory EnvironmentsTheory CommandsTheory ssaPrgsTheory
open CertificateCheckerTheory
val _ = new_theory "trans";
val _ = translation_extends "realProg";
(* for recursive translation *)
fun def_of_const tm = let
val res = dest_thy_const tm handle HOL_ERR _ =>
failwith ("Unable to translate: " ^ term_to_string tm)
val name = (#Name res)
fun def_from_thy thy name =
DB.fetch thy (name ^ "_pmatch") handle HOL_ERR _ =>
DB.fetch thy (name ^ "_def") handle HOL_ERR _ =>
DB.fetch thy (name ^ "_DEF") handle HOL_ERR _ =>
DB.fetch thy name
val def = def_from_thy "termination" name handle HOL_ERR _ =>
def_from_thy (#Thy res) name handle HOL_ERR _ =>
failwith ("Unable to find definition of " ^ name)
val def = def |> CONV_RULE (DEPTH_CONV BETA_CONV)
in def end
val _ = (find_def_for_const := def_of_const);
(* / for recursive translation *)
val divideInterval_v_thm = translate divideInterval_def;
val supersetInterval_v_thm = translate isSupersetInterval_def;
val validIvbounds_v_thm = translate validIntervalbounds_def;
val invertinterval_side_def = fetch "-" "invertinterval_side_def";
val divideinterval_side_def = fetch "-" "divideinterval_side_def";
val validintervalbounds_side_def = fetch "-" "validintervalbounds_side_def";
val ivbounds_side_valid = prove (
``!f absenv P V.
(∀v. v V valid (FST (absenv (Var v)))) ==>
validintervalbounds_side f absenv P V``,
recInduct validIntervalbounds_ind
\\ rw[]
\\ once_rewrite_tac [validintervalbounds_side_def]
\\ Cases_on `e`
>- (fs[] )
>- (fs[])
>- (fs[])
>- (fs[]
\\ rpt (qpat_x_assum `T` kall_tac)
\\ once_rewrite_tac [METIS_PROVE [] ``(b \/ c) <=> (~b ==> c)``]
\\ rpt strip_tac
\\ qpat_x_assum `(~ A) ==> B`
(fn thm =>
ASSUME_TAC (ONCE_REWRITE_RULE [GSYM (METIS_PROVE [] ``(b \/ c) <=> (~b ==> c)``)] thm))
\\ rveq
\\ `valid (FST(absenv e'))`
by (match_mp_tac validIntervalbounds_validates_iv
\\ qexists_tac `P` \\ qexists_tac `validVars'`
\\ fs[])
\\ once_rewrite_tac [invertinterval_side_def]
\\ cheat)
>- (fs[]
\\ rpt (qpat_x_assum `T` kall_tac)
\\ once_rewrite_tac [METIS_PROVE [] ``(b \/ c) <=> (~b ==> c)``]
\\ rpt strip_tac
\\ qpat_x_assum `(~ A) ==> B`
(fn thm =>
ASSUME_TAC (ONCE_REWRITE_RULE [GSYM (METIS_PROVE [] ``(b \/ c) <=> (~b ==> c)``)] thm))
\\ rveq
\\ `valid (FST(absenv e'))`
by (match_mp_tac validIntervalbounds_validates_iv
\\ qexists_tac `P` \\ qexists_tac `validVars'`
\\ fs[])
\\ `valid (FST(absenv e0))`
by (match_mp_tac validIntervalbounds_validates_iv
\\ qexists_tac `P` \\ qexists_tac `validVars'`
\\ fs[])
\\ rewrite_tac [divideinterval_side_def, invertinterval_side_def]
\\ cheat));
val certificate_if_thm = prove (``!f absenv P. CertificateChecker f absenv P <=> if (validIntervalbounds f absenv P EMPTY) then validErrorbound f absenv else F``, rw[CertificateChecker_def]);
val res = translate certificate_if_thm;
val certificatechecker_side_def = fetch "-" "certificatechecker_side_def";
val validerrorbound_side_def = fetch "-" "validerrorbound_side_def";
val precond_is_true = prove (``
!f absenv P.
certificatechecker_side f absenv P``,
cheat
(*
rw [certificatechecker_side_def]
recInduct
\\ rw []
\\ once_rewrite_tac [validIvbounds_thm]
\\ rw[]
>- (once_rewrite_tac [invertinterval_side_def])
>- ()
>- ()
>- ()
*));
val certificatecmd_if_thm = prove (``!f absenv P. CertificateCheckerCmd f absenv P <=> if (validIntervalboundsCmd f absenv P EMPTY) then validErrorboundCmd f absenv else F``, rw[CertificateCheckerCmd_def]);
val res = translate certificatecmd_if_thm;
val _ = export_theory();
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