Commit 67e1af47 authored by Heiko Becker's avatar Heiko Becker

Merge master with translation branch to obtain code extraction for Coq and HOL4

parents 4b62ec07 196c64b5
......@@ -28,8 +28,10 @@ hol4/*/*.ui
hol4/*/*.uo
hol4/*/.*
hol4/heap
hol4/output/heap
hol4/output/certificate_*
hol4/*/heap
hol4/output/*.sml
hol4/binary/cake_checker
hol4/binary/checker.S
daisy
rawdata/*
.ensime*
......
This diff is collapsed.
Require Import CertificateChecker.
Extraction Language Ocaml.
Extraction "CertificateChecker.ml" CertificateCheckerCmd.
\ No newline at end of file
#############################################################################
## v # The Coq Proof Assistant ##
## <O___,, # INRIA - CNRS - LIX - LRI - PPS ##
## \VV/ # ##
## // # Makefile automagically generated by coq_makefile V8.6 ##
#############################################################################
# WARNING
#
# This Makefile has been automagically generated
# Edit at your own risks !
#
# END OF WARNING
#
# This Makefile was generated by the command line :
# coq_makefile -f _CoqProject -o Makefile
#
.DEFAULT_GOAL := all
# This Makefile may take arguments passed as environment variables:
# COQBIN to specify the directory where Coq binaries resides;
# TIMECMD set a command to log .v compilation time;
# TIMED if non empty, use the default time command as TIMECMD;
# ZDEBUG/COQDEBUG to specify debug flags for ocamlc&ocamlopt/coqc;
# DSTROOT to specify a prefix to install path.
# VERBOSE to disable the short display of compilation rules.
VERBOSE?=
SHOW := $(if $(VERBOSE),@true "",@echo "")
HIDE := $(if $(VERBOSE),,@)
# Here is a hack to make $(eval $(shell works:
define donewline
endef
includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr -d '\r' | tr '\n' '@'; })))
$(call includecmdwithout@,$(COQBIN)coqtop -config)
TIMED?=
TIMECMD?=
STDTIME?=/usr/bin/time -f "$* (user: %U mem: %M ko)"
TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
vo_to_obj = $(addsuffix .o,\
$(filter-out Warning: Error:,\
$(shell $(COQBIN)coqtop -q -noinit -batch -quiet -print-mod-uid $(1))))
##########################
# #
# Libraries definitions. #
# #
##########################
COQLIBS?=\
-R "../" Daisy
COQCHKLIBS?=\
-R "../" Daisy
COQDOCLIBS?=\
-R "../" Daisy
##########################
# #
# Variables definitions. #
# #
##########################
OPT?=
COQDEP?="$(COQBIN)coqdep" -c
COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)
COQCHKFLAGS?=-silent -o
COQDOCFLAGS?=-interpolate -utf8
COQC?=$(TIMER) "$(COQBIN)coqc"
GALLINA?="$(COQBIN)gallina"
COQDOC?="$(COQBIN)coqdoc"
COQCHK?="$(COQBIN)coqchk"
COQMKTOP?="$(COQBIN)coqmktop"
##################
# #
# Install Paths. #
# #
##################
ifdef USERINSTALL
XDG_DATA_HOME?="$(HOME)/.local/share"
COQLIBINSTALL=$(XDG_DATA_HOME)/coq
COQDOCINSTALL=$(XDG_DATA_HOME)/doc/coq
else
COQLIBINSTALL="${COQLIB}user-contrib"
COQDOCINSTALL="${DOCDIR}user-contrib"
COQTOPINSTALL="${COQLIB}toploop"
endif
######################
# #
# Files dispatching. #
# #
######################
VFILES:=Checker_extraction.v
ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),)
-include $(addsuffix .d,$(VFILES))
else
ifeq ($(MAKECMDGOALS),)
-include $(addsuffix .d,$(VFILES))
endif
endif
.SECONDARY: $(addsuffix .d,$(VFILES))
VO=vo
VOFILES:=$(VFILES:.v=.$(VO))
VOFILES0=$(patsubst ..//%,%,$(filter ..//%,$(VOFILES)))
GLOBFILES:=$(VFILES:.v=.glob)
GFILES:=$(VFILES:.v=.g)
HTMLFILES:=$(VFILES:.v=.html)
GHTMLFILES:=$(VFILES:.v=.g.html)
OBJFILES=$(call vo_to_obj,$(VOFILES))
ALLNATIVEFILES=$(OBJFILES:.o=.cmi) $(OBJFILES:.o=.cmo) $(OBJFILES:.o=.cmx) $(OBJFILES:.o=.cmxs)
NATIVEFILES=$(foreach f, $(ALLNATIVEFILES), $(wildcard $f))
NATIVEFILES0=$(patsubst ..//%,%,$(filter ..//%,$(NATIVEFILES)))
ifeq '$(HASNATDYNLINK)' 'true'
HASNATDYNLINK_OR_EMPTY := yes
else
HASNATDYNLINK_OR_EMPTY :=
endif
#######################################
# #
# Definition of the toplevel targets. #
# #
#######################################
all: $(VOFILES)
quick: $(VOFILES:.vo=.vio)
vio2vo:
$(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio)
checkproofs:
$(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio)
gallina: $(GFILES)
html: $(GLOBFILES) $(VFILES)
- mkdir -p html
$(COQDOC) -toc $(COQDOCFLAGS) -html $(COQDOCLIBS) -d html $(VFILES)
gallinahtml: $(GLOBFILES) $(VFILES)
- mkdir -p html
$(COQDOC) -toc $(COQDOCFLAGS) -html -g $(COQDOCLIBS) -d html $(VFILES)
all.ps: $(VFILES)
$(COQDOC) -toc $(COQDOCFLAGS) -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
all-gal.ps: $(VFILES)
$(COQDOC) -toc $(COQDOCFLAGS) -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
all.pdf: $(VFILES)
$(COQDOC) -toc $(COQDOCFLAGS) -pdf $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
all-gal.pdf: $(VFILES)
$(COQDOC) -toc $(COQDOCFLAGS) -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
validate: $(VOFILES)
$(COQCHK) $(COQCHKFLAGS) $(COQCHKLIBS) $(notdir $(^:.vo=))
beautify: $(VFILES:=.beautified)
for file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done
@echo 'Do not do "make clean" until you are sure that everything went well!'
@echo 'If there were a problem, execute "for file in $$(find . -name \*.v.old -print); do mv $${file} $${file%.old}; done" in your shell/'
.PHONY: all archclean beautify byte clean cleanall gallina gallinahtml html install install-doc install-natdynlink install-toploop opt printenv quick uninstall userinstall validate vio2vo
####################
# #
# Special targets. #
# #
####################
byte:
$(MAKE) all "OPT:=-byte"
opt:
$(MAKE) all "OPT:=-opt"
userinstall:
+$(MAKE) USERINSTALL=true install
install:
cd "../" && for i in $(NATIVEFILES0) $(GLOBFILES0) $(VFILES0) $(VOFILES0); do \
install -d "`dirname "$(DSTROOT)"$(COQLIBINSTALL)/Daisy/$$i`"; \
install -m 0644 $$i "$(DSTROOT)"$(COQLIBINSTALL)/Daisy/$$i; \
done
install-doc:
install -d "$(DSTROOT)"$(COQDOCINSTALL)/Daisy/html
for i in html/*; do \
install -m 0644 $$i "$(DSTROOT)"$(COQDOCINSTALL)/Daisy/$$i;\
done
uninstall_me.sh: Makefile
echo '#!/bin/sh' > $@
printf 'cd "$${DSTROOT}"$(COQLIBINSTALL)/Daisy && rm -f $(NATIVEFILES0) $(GLOBFILES0) $(VFILES0) $(VOFILES0) && find . -type d -and -empty -delete\ncd "$${DSTROOT}"$(COQLIBINSTALL) && find "Daisy" -maxdepth 0 -and -empty -exec rmdir -p \{\} \;\n' >> "$@"
printf 'cd "$${DSTROOT}"$(COQDOCINSTALL)/Daisy \\\n' >> "$@"
printf '&& rm -f $(shell find "html" -maxdepth 1 -and -type f -print)\n' >> "$@"
printf 'cd "$${DSTROOT}"$(COQDOCINSTALL) && find Daisy/html -maxdepth 0 -and -empty -exec rmdir -p \{\} \;\n' >> "$@"
chmod +x $@
uninstall: uninstall_me.sh
sh $<
.merlin:
@echo 'FLG -rectypes' > .merlin
@echo "B $(COQLIB)kernel" >> .merlin
@echo "B $(COQLIB)lib" >> .merlin
@echo "B $(COQLIB)library" >> .merlin
@echo "B $(COQLIB)parsing" >> .merlin
@echo "B $(COQLIB)pretyping" >> .merlin
@echo "B $(COQLIB)interp" >> .merlin
@echo "B $(COQLIB)printing" >> .merlin
@echo "B $(COQLIB)intf" >> .merlin
@echo "B $(COQLIB)proofs" >> .merlin
@echo "B $(COQLIB)tactics" >> .merlin
@echo "B $(COQLIB)tools" >> .merlin
@echo "B $(COQLIB)ltacprof" >> .merlin
@echo "B $(COQLIB)toplevel" >> .merlin
@echo "B $(COQLIB)stm" >> .merlin
@echo "B $(COQLIB)grammar" >> .merlin
@echo "B $(COQLIB)config" >> .merlin
@echo "B $(COQLIB)ltac" >> .merlin
@echo "B $(COQLIB)engine" >> .merlin
clean::
rm -f $(OBJFILES) $(OBJFILES:.o=.native) $(NATIVEFILES)
find . -name .coq-native -type d -empty -delete
rm -f $(VOFILES) $(VOFILES:.vo=.vio) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)
rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) all-mli.tex
- rm -rf html mlihtml uninstall_me.sh
cleanall:: clean
rm -f $(patsubst %.v,.%.aux,$(VFILES))
archclean::
rm -f *.cmx *.o
printenv:
@"$(COQBIN)coqtop" -config
@echo 'OCAMLFIND = $(OCAMLFIND)'
@echo 'PP = $(PP)'
@echo 'COQFLAGS = $(COQFLAGS)'
@echo 'COQLIBINSTALL = $(COQLIBINSTALL)'
@echo 'COQDOCINSTALL = $(COQDOCINSTALL)'
Makefile: _CoqProject
mv -f $@ $@.bak
"$(COQBIN)coq_makefile" -f $< -o $@
###################
# #
# Implicit rules. #
# #
###################
$(VOFILES): %.vo: %.v
$(SHOW)COQC $<
$(HIDE)$(COQC) $(COQDEBUG) $(COQFLAGS) $<
$(GLOBFILES): %.glob: %.v
$(COQC) $(COQDEBUG) $(COQFLAGS) $<
$(VFILES:.v=.vio): %.vio: %.v
$(COQC) -quick $(COQDEBUG) $(COQFLAGS) $<
$(GFILES): %.g: %.v
$(GALLINA) $<
$(VFILES:.v=.tex): %.tex: %.v
$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@
$(HTMLFILES): %.html: %.v %.glob
$(COQDOC) $(COQDOCFLAGS) -html $< -o $@
$(VFILES:.v=.g.tex): %.g.tex: %.v
$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@
$(GHTMLFILES): %.g.html: %.v %.glob
$(COQDOC) $(COQDOCFLAGS) -html -g $< -o $@
$(addsuffix .d,$(VFILES)): %.v.d: %.v
$(SHOW)'COQDEP $<'
$(HIDE)$(COQDEP) $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
$(addsuffix .beautified,$(VFILES)): %.v.beautified:
$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*.v
# WARNING
#
# This Makefile has been automagically generated
# Edit at your own risks !
#
# END OF WARNING
-R ../ Daisy
Checker_extraction.v
......@@ -36,4 +36,6 @@ val emptyEnv_def = Define `
val updEnv_def = Define `
updEnv (x:num) (v:real) (E:env) (y:num) :real option = if y = x then SOME v else E y`;
val - = export_theory();
val noDivzero_def = Define `noDivzero (a:real) (b:real) = (a < &0 \/ &0 < b)`;
val _ = export_theory();
......@@ -67,8 +67,6 @@ val validErrorboundCmd_def = Define `
| Ret e =>
validErrorbound e env dVars`;
val noDivzero_def = Define `noDivzero (a:real) (b:real) = (a < &0 \/ &0 < b)`;
val err_always_positive = store_thm ("err_always_positive",
``!(e:real exp) (absenv:analysisResult) (iv:interval) (err:real) dVars.
(validErrorbound (e:real exp) (absenv:analysisResult) dVars) /\
......
INCLUDES = $(HOLDIR)/examples/machine-code/hoare-triple Infra
INCLUDES = $(HOLDIR)/examples/machine-code/hoare-triple Infra cakeml/translator cakeml/basis cakeml/characteristic
OPTIONS = QUIT_ON_FAILURE
ifdef POLY
......@@ -19,6 +19,8 @@ BARE_THYS = BasicProvers Defn HolKernel Parse Tactic monadsyntax \
quantHeuristicsLib relationTheory res_quanTheory rich_listTheory \
sortingTheory sptreeTheory stringTheory sumTheory wordsTheory \
simpLib realTheory realLib RealArith \
cakeml/translator/ml_translatorLib \
cakeml/basis/ioProgLib
DEPS = $(patsubst %,%.uo,$(BARE_THYS1)) $(PARENTHEAP)
......
......@@ -227,18 +227,27 @@ fs iv_ss \\ rpt strip_tac \\ once_rewrite_tac [GSYM REAL_INV_1OVER]
by (match_mp_tac REAL_INV_LE_ANTIMONO \\ fs []) \\
REAL_ASM_ARITH_TAC));
val iv_inv_preserves_valid = store_thm ("iv_neg_preserves_valid",
val iv_inv_preserves_valid = store_thm ("iv_inv_preserves_valid",
``!iv.
(IVhi iv < 0 \/ 0 < IVlo iv) /\
valid iv ==> valid (invertInterval iv)``,
fs [valid_def, invertInterval_def, IVlo_def, IVhi_def]
\\ rpt strip_tac
>- (cheat)
>- (fs [GSYM REAL_INV_1OVER]
\\ `- (inv (FST iv)) <= - (inv (SND iv))` suffices_by fs []
\\ `0 < - SND iv` by REAL_ASM_ARITH_TAC
\\ `- (inv (FST iv)) = inv (- (FST iv))` by (match_mp_tac REAL_NEG_INV \\ REAL_ASM_ARITH_TAC)
\\ `- (inv (SND iv)) = inv (- (SND iv))` by (match_mp_tac REAL_NEG_INV \\ REAL_ASM_ARITH_TAC)
\\ rpt (qpat_x_assum `- (inv _) = _` (fn thm => rewrite_tac [thm]))
\\ match_mp_tac REAL_INV_LE_ANTIMONO_IMPR
\\ rpt CONJ_TAC \\ fs []
\\ match_mp_tac REAL_LET_TRANS
\\ asm_exists_tac \\ fs [])
>- (fs[GSYM REAL_INV_1OVER]
\\ match_mp_tac REAL_INV_LE_ANTIMONO_IMPR
\\ rpt CONJ_TAC \\ fs[]
\\ rpt CONJ_TAC \\ fs []
\\ match_mp_tac REAL_LTE_TRANS
\\ asm_exists_tac \\ fs[]));
\\ asm_exists_tac \\ fs []));
val interval_addition_valid = store_thm ("interval_addition_valid",
``!iv1 iv2. validIntervalAdd iv1 iv2 (addInterval iv1 iv2)``,
......@@ -254,6 +263,17 @@ fs iv_ss \\ rpt strip_tac
match_mp_tac REAL_LE_TRANS \\
HINT_EXISTS_TAC \\ strip_tac \\ fs [REAL_LE_MAX]));
val iv_add_preserves_valid = store_thm ("iv_add_preserves_valid",
``!iv1 iv2.
valid iv1 /\ valid iv2 ==>
valid (addInterval iv1 iv2)``,
fs [valid_def, addInterval_def, IVlo_def, IVhi_def, absIntvUpd_def, min4_def, max4_def]
\\ rpt strip_tac
\\ match_mp_tac REAL_LE_TRANS
\\ qexists_tac `FST iv1 + FST iv2` \\ fs [REAL_MIN_LE1]
\\ match_mp_tac REAL_LE_TRANS
\\ qexists_tac `FST iv1 + FST iv2` \\ fs [REAL_LE_MAX1]);
val interval_subtraction_valid = store_thm ("interval_subtraction_valid",
``!iv1 iv2.
validIntervalSub iv1 iv2 (subtractInterval iv1 iv2)``,
......@@ -263,6 +283,17 @@ rpt gen_tac \\ strip_tac \\
match_mp_tac (REWRITE_RULE (iv_ss @ [FST,SND]) (SPECL [``iv1:interval``,``(-r,-q):interval``] interval_addition_valid)) \\
fs []);
val iv_sub_preserves_valid = store_thm ("iv_sub_preserves_valid",
``!iv1 iv2.
valid iv1 /\ valid iv2 ==>
valid (subtractInterval iv1 iv2)``,
once_rewrite_tac [subtractInterval_def]
\\ rpt strip_tac
\\ match_mp_tac iv_add_preserves_valid
\\ conj_tac \\ fs []
\\ match_mp_tac iv_neg_preserves_valid \\ fs []);
val interval_multiplication_valid = store_thm ("interval_multiplication_valid",
``!iv1 iv2 a b.
contained a iv1 /\ contained b iv2 ==> contained (a * b) (multInterval iv1 iv2)``,
......@@ -402,6 +433,19 @@ fs iv_ss \\ rpt strip_tac
rewrite_tac [SIMP_RULE bool_ss [max4_def] (CONV_RULE let_CONV thm)])
max4_correct)))));
val iv_mult_preserves_valid = store_thm ("iv_mult_preserves_valid",
``!iv1 iv2.
valid iv1 /\ valid iv2 ==>
valid (multInterval iv1 iv2)``,
fs [valid_def, multInterval_def, IVlo_def, IVhi_def, absIntvUpd_def, min4_def, max4_def]
\\ rpt strip_tac
\\ match_mp_tac REAL_LE_TRANS
\\ qexists_tac `FST iv1 * FST iv2`
\\ fs [REAL_MIN_LE1]
\\ match_mp_tac REAL_LE_TRANS
\\ qexists_tac `FST iv1 * FST iv2`
\\ fs [REAL_LE_MAX1]);
val interval_division_valid = store_thm ( "interval_division_valid",
``!(iv1:interval) (iv2:interval) (a:real) (b:real).
(IVhi iv2 < 0 \/ 0 < IVlo iv2) /\
......@@ -420,6 +464,17 @@ match_mp_tac
(iv_ss @ [FST, SND, real_div, REAL_MUL_LID]) (SPECL [``(q,r):interval``, ``b:real``] interval_inversion_valid)) \\
fs[]);
val iv_div_preserves_valid = store_thm ("iv_div_preserves_valid",
``!iv1 iv2.
valid iv1 /\ valid iv2 /\ (IVhi iv2 < 0 \/ 0 < IVlo iv2) ==>
valid (divideInterval iv1 iv2)``,
once_rewrite_tac [divideInterval_def]
\\ rpt strip_tac
\\ match_mp_tac iv_mult_preserves_valid
\\ fs []
\\ match_mp_tac iv_inv_preserves_valid
\\ fs []);
(** Properties of the maxAbs function **)
val contained_leq_maxAbs = store_thm ("contained_leq_maxAbs",
``!a iv. contained a iv ==> abs a <= maxAbs iv``,
......
......@@ -385,44 +385,102 @@ val validIntervalboundsCmd_sound = store_thm ("validIntervalboundsCmd_sound",
\\ fs [domain_union]
\\ CCONTR_TAC \\ metis_tac []));
val validIntervalbounds_noDivzero_real = store_thm("validIntervalbounds_noDivzero_real",
``!(f1 f2:real exp) (absenv:analysisResult) (P:precond) (dVars:num_set).
validIntervalbounds (Binop Div f1 f2) absenv P dVars ==>
noDivzero (SND (FST (absenv f2))) (FST (FST (absenv f2)))``,
rpt strip_tac
\\ Cases_on `absenv f2` \\ Cases_on `absenv f1` \\ Cases_on `absenv (Binop Div f1 f2)`
\\ fs [Once validIntervalbounds_def, noDivzero_def, IVhi_def, IVlo_def]);
val validIntervalbounds_validates_iv = store_thm ("validIntervalbounds_validates_iv",
``!(f:real exp) (absenv:analysisResult) (P:precond) (dVars:num_set).
(!v. v IN domain dVars ==>
valid (FST (absenv (Var v)))) /\
validIntervalbounds f absenv P dVars ==>
valid (FST (absenv f))``,
cheat
(* Induct
\\ rpt strip_tac \\ fs [Once validIntervalbounds_def]
Induct
\\ rpt strip_tac
>- (first_x_assum (fn thm => qspecl_then [`n`] ASSUME_TAC thm)
\\ Cases_on `absenv (Var n)` \\ fs[])
>- (Cases_on `absenv (Param n)` \\ fs[valid_def, isSupersetInterval_def]
\\ match_mp_tac REAL_LE_TRANS
\\ asm_exists_tac
\\ CONJ_TAC \\ TRY (simp[])
\\ match_mp_tac REAL_LE_TRANS
\\ asm_exists_tac
\\ CONJ_TAC \\ simp[])
>- (Cases_on `absenv (Const v)` \\ fs[isSupersetInterval_def, valid_def]
\\ Cases_on `absenv (Var n)`
\\ fs[domain_lookup, valid_def, isSupersetInterval_def, validIntervalbounds_def]
\\ REAL_ASM_ARITH_TAC)
>- (rpt strip_tac
\\ Cases_on `absenv (Const v)` \\ fs[isSupersetInterval_def, valid_def, validIntervalbounds_def]
\\ match_mp_tac REAL_LE_TRANS
\\ asm_exists_tac \\ CONJ_TAC \\ fs[IVlo_def, IVhi_def])
>- (Cases_on `absenv (Unop u f)` \\ fs[]
\\ qpat_x_assum `validIntervalbounds _ _ _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE[validIntervalbounds_def] thm))
>- (qpat_x_assum `validIntervalbounds _ _ _ _`
(fn thm => ASSUME_TAC (ONCE_REWRITE_RULE[validIntervalbounds_def] thm))
\\ Cases_on `absenv (Unop u f)` \\ fs[]
\\ `valid (FST (absenv f))`
by (first_x_assum match_mp_tac \\
qexists_tac `P` \\ qexists_tac `dVars`
\\ fs[])
\\ Cases_on `absenv f` \\ fs[]
\\ Cases_on `u` \\ fs[isSupersetInterval_def]
>- (`valid (negateInterval q')` by (match_mp_tac iv_neg_preserves_valid \\ fs[])
\\ fs[valid_def]
\\ Cases_on `u`
>- (`valid (negateInterval q')`
by (match_mp_tac iv_neg_preserves_valid \\ fs[])
\\ fs[valid_def, isSupersetInterval_def]
\\ match_mp_tac REAL_LE_TRANS
\\ asm_exists_tac \\ fs[]
\\ match_mp_tac REAL_LE_TRANS
\\ asm_exists_tac \\ fs[])
>- (cheat) (* FIXME: ONLY TWO CASES! *)
>- (cheat))
>- (cheat) *)
);
>- (`valid (invertInterval q')`
by (match_mp_tac iv_inv_preserves_valid \\ fs[])
\\ fs[valid_def, isSupersetInterval_def]
>- (match_mp_tac REAL_LE_TRANS
\\ asm_exists_tac \\ fs[]
\\ match_mp_tac REAL_LE_TRANS
\\ asm_exists_tac \\ fs[])
>- (match_mp_tac REAL_LE_TRANS
\\ asm_exists_tac \\ fs[]
\\ match_mp_tac REAL_LE_TRANS
\\ asm_exists_tac \\ fs[])))
>- (rename1 `Binop b f1 f2`
\\ qpat_x_assum `validIntervalbounds _ _ _ _`
(fn thm => ASSUME_TAC (ONCE_REWRITE_RULE[validIntervalbounds_def] thm))
\\ Cases_on `absenv (Binop b f1 f2)` \\ rename1 `absenv (Binop b f1 f2) = (iv,err)`
\\ fs[]
\\ `valid (FST (absenv f1))`
by (first_x_assum match_mp_tac
\\ qexists_tac `P` \\ qexists_tac `dVars`
\\ fs[])
\\ `valid (FST (absenv f2))`
by (first_x_assum match_mp_tac
\\ qexists_tac `P` \\ qexists_tac `dVars`
\\ fs[])
\\ Cases_on `absenv f1` \\ Cases_on `absenv f2`
\\ rename1 `absenv f1 = (iv_f1, err_f1)`
\\ rename1 `absenv f2 = (iv_f2, err_f2)`
\\ fs[]
\\ Cases_on `b`
>- (`valid (addInterval iv_f1 iv_f2)`
by (match_mp_tac iv_add_preserves_valid \\ fs[])
\\ fs[valid_def, isSupersetInterval_def]
\\ match_mp_tac REAL_LE_TRANS
\\ asm_exists_tac \\ fs []
\\ match_mp_tac REAL_LE_TRANS
\\ asm_exists_tac \\ fs [])
>- (`valid (subtractInterval iv_f1 iv_f2)`
by (match_mp_tac iv_sub_preserves_valid \\ fs[])
\\ fs[valid_def, isSupersetInterval_def]
\\ match_mp_tac REAL_LE_TRANS
\\ asm_exists_tac \\ fs []
\\ match_mp_tac REAL_LE_TRANS
\\ asm_exists_tac \\ fs [])
>- (`valid (multInterval iv_f1 iv_f2)`
by (match_mp_tac iv_mult_preserves_valid \\ fs[])
\\ fs[valid_def, isSupersetInterval_def]
\\ match_mp_tac REAL_LE_TRANS
\\ asm_exists_tac \\ fs []
\\ match_mp_tac REAL_LE_TRANS
\\ asm_exists_tac \\ fs [])
>- (`valid (divideInterval iv_f1 iv_f2)`
by (match_mp_tac iv_div_preserves_valid \\ fs[])
\\ fs[valid_def, isSupersetInterval_def]
\\ match_mp_tac REAL_LE_TRANS
\\ asm_exists_tac \\ fs []
\\ match_mp_tac REAL_LE_TRANS
\\ asm_exists_tac \\ fs [])));
val _ = export_theory();
INCLUDES = .. ../cakeml/characteristic/examples/compilation/compile
OPTIONS = QUIT_ON_FAILURE
ifdef POLY
HOLHEAP = heap
EXTRA_CLEANS = $(HOLHEAP) $(HOLHEAP).o
all: $(HOLHEAP) cake_checker
ifndef CC
CC=gcc