Commit 110af488 authored by Heiko Becker's avatar Heiko Becker
Browse files

Merge branch 'translation' to obtain new definition of insert

parents 1d6e6eb6 62cc26e2
[submodule "hol4/cakeml"]
branch = daisy
path = hol4/cakeml
url = https://github.com/CakeML/cakeml.git
......@@ -36,9 +36,4 @@ 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`;
(**
Abbreviation for insertion into "num_set" type
**)
val Insert_def = Define `Insert x V = insert x () V`;
val - = export_theory();
......@@ -58,7 +58,7 @@ val freeVars_def = Define `
val definedVars_def = Define `
definedVars (f:'a cmd) :num_set =
case f of
|Let x e g => Insert x (definedVars g)
|Let (x:num) e g => insert x () (definedVars g)
|Ret e => LN`;
val _ = export_theory ();
......@@ -11,12 +11,12 @@ val (approxEnv_rules, approxEnv_ind, approxEnv_cases) = Hol_reln `
approxEnv E1 A fVars dVars E2 /\
(abs (v1 - v2) <= abs v1 * machineEpsilon) /\
(lookup x (union fVars dVars) = NONE) ==>
approxEnv (updEnv x v1 E1) A (Insert x fVars) dVars (updEnv x v2 E2)) /\
approxEnv (updEnv x v1 E1) A (insert x () fVars) dVars (updEnv x v2 E2)) /\
(!(E1:env) (E2:env) (A:analysisResult) (fVars:num_set) (dVars:num_set) v1 v2 x.
approxEnv E1 A fVars dVars E2 /\
(abs (v1 - v2) <= SND (A (Var x))) /\
(lookup x (union fVars dVars) = NONE) ==>
approxEnv (updEnv x v1 E1) A fVars (Insert x dVars) (updEnv x v2 E2))`;
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);
......
......@@ -10,6 +10,8 @@ open ExpressionAbbrevsTheory EnvironmentsTheory
val _ = new_theory "ErrorBounds";
val _ = Parse.hide "delta"; (* so that it can be used as a variable *)
val const_abs_err_bounded = store_thm ("const_abs_err_bounded",
``!(n:real) (nR:real) (nF:real) (E1 E2:env).
eval_exp 0 E1 (Const n) nR /\
......
......@@ -14,6 +14,8 @@ open IntervalValidationTheory EnvironmentsTheory CommandsTheory ssaPrgsTheory
val _ = new_theory "ErrorValidation";
val _ = Parse.hide "delta"; (* so that it can be used as a variable *)
val validErrorbound_def = Define `
validErrorbound e (absenv:analysisResult) (dVars:num_set)=
let (intv, err) = absenv e in
......@@ -51,7 +53,7 @@ val validErrorboundCmd_def = Define `
validErrorboundCmd (f:real cmd) (env:analysisResult) (dVars:num_set)=
case f of
| Let x e g =>
if validErrorboundCmd g env (Insert x dVars)
if validErrorboundCmd g env (insert x () dVars)
then
(validErrorbound e env dVars/\
(env e = env (Var x)))
......@@ -136,10 +138,11 @@ val validErrorboundCorrectVariable_ind = prove (
\\ rw_asm_star `A (Var v) = _`
\\ rw_asm_star `A (Var v) = _`
\\ first_x_assum match_mp_tac
\\ qexistsl_tac [`P`, `Insert v fVars`, `dVars`, `updEnv v nR E1`]
\\ fs [updEnv_def]
\\ conj_tac
>- (fs [usedVars_def, SUBSET_DEF, Insert_def, domain_insert])
\\ qexistsl_tac [`P`, `insert v () fVars`, `dVars`, `updEnv v nR E1`]
\\ fs [updEnv_def, domain_insert]
\\ rpt conj_tac
>- (fs [usedVars_def, SUBSET_DEF, domain_insert])
>- (rpt strip_tac \\ first_x_assum match_mp_tac \\ fs [])
>- (match_mp_tac Var_load \\ fs [updEnv_def]))
>- (first_x_assum match_mp_tac
\\ qexistsl_tac [`v`, `nlo`, `nhi`, `P`]
......@@ -164,7 +167,7 @@ val validErrorboundCorrectVariable_ind = prove (
\\ fs [domain_lookup])
>- (fs []
\\ first_x_assum match_mp_tac
\\ fs [domain_insert, Insert_def]))))
\\ fs [domain_insert]))))
>- (fs [updEnv_def]
\\ Cases_on `v = x` \\ rveq
>- (fs [validErrorbound_def, lookup_union]
......@@ -174,17 +177,17 @@ val validErrorboundCorrectVariable_ind = prove (
\\ rpt conj_tac
>- (match_mp_tac Var_load \\ fs [])
>- (match_mp_tac Var_load \\ fs [])
>- (fs [validIntervalbounds_def, Insert_def, lookup_insert])
>- (fs [validErrorbound_def, Insert_def, lookup_insert])
>- (fs [validIntervalbounds_def, lookup_insert])
>- (fs [validErrorbound_def, lookup_insert])
>- (rpt strip_tac
\\ specialize `!v. v IN domain (Insert _ _) ==> _` `v'`
\\ specialize `!v. v = _ \/ v IN domain _ ==> _` `v'`
\\ Cases_on `v' = x`
>- (rveq \\ fs [lookup_union]
\\ Cases_on `lookup v' fVars`
\\ fs [domain_lookup])
>- (fs []
\\ first_x_assum match_mp_tac
\\ fs [domain_insert, Insert_def]))
\\ fs [domain_insert]))
>- (rpt strip_tac
\\ rpt (first_x_assum (qspec_then `v'` ASSUME_TAC))
\\ specialize `v' IN domin fVars ==> _` `v' IN domain fVars`
......@@ -2263,7 +2266,7 @@ val validErrorboundCmd_sound = store_thm ("validErrorboundCmd_sound",
\\ first_x_assum match_mp_tac
\\ qpat_x_assum `validErrorboundCmd _ _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [validErrorboundCmd_def] thm))
\\ qpat_x_assum `validIntervalboundsCmd _ _ _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [validIntervalboundsCmd_def] thm))
\\ qexistsl_tac [`absenv`, `updEnv n vr E1`, `updEnv n vf E2`, `outVars`, `fVars`, `Insert n dVars`, `elo`, `ehi`, `P`]
\\ qexistsl_tac [`absenv`, `updEnv n vr E1`, `updEnv n vf E2`, `outVars`, `fVars`, `insert n () dVars`, `elo`, `ehi`, `P`]
\\ fs [Once getRetExp_def]
\\ rpt conj_tac
>- (match_mp_tac approxUpdBound
......@@ -2282,44 +2285,41 @@ val validErrorboundCmd_sound = store_thm ("validErrorboundCmd_sound",
\\ metis_tac [])
>- (Cases_on `lookup n (union fVars dVars)` \\ fs [domain_lookup]))
>- (match_mp_tac ssa_equal_set
\\ qexists_tac `Insert n (union fVars dVars)` \\ fs [Insert_def, domain_union]
\\ qexists_tac `insert n () (union fVars dVars)` \\ fs [ domain_union]
\\ once_rewrite_tac [UNION_COMM]
\\ fs [INSERT_UNION_EQ])
>- (fs [SUBSET_DEF] \\ rpt strip_tac
\\ first_x_assum match_mp_tac
\\ once_rewrite_tac [freeVars_def]
\\ fs [domain_union]
\\ conj_tac
>- (Cases_on `x = n` \\ rveq \\ fs []
\\ `domain (freeVars f) SUBSET (domain (Insert n (union fVars dVars)))`
by (match_mp_tac ssa_subset_freeVars
\\ qexists_tac `outVars` \\ fs [])
\\ fs [SUBSET_DEF]
\\ specialize `!x. x IN _ ==> _` `n`
\\ specialize `n IN _ ==> _` `n IN _`
\\ fs [Insert_def, domain_insert, domain_union])
>- (fs [domain_insert, Insert_def]))
>- (rpt strip_tac
\\ fs [updEnv_def]
\\ Cases_on `v = n` \\ rveq
>- (fs []
\\ rw_sym_asm `absenv e = _`
\\ match_mp_tac validIntervalbounds_sound
\\ qexistsl_tac [`P`, `fVars`, `dVars`, `E1`]
\\ fs [SUBSET_DEF]
\\ rpt strip_tac
\\ first_x_assum match_mp_tac
\\ once_rewrite_tac [freeVars_def]
\\ fs [domain_union]
\\ metis_tac [])
>- (fs [Insert_def, domain_insert]))
\\ fs [domain_union])
>- (Cases_on `x = n` \\ rveq \\ fs []
>- (rpt strip_tac \\ rveq \\ fs []
>- (qexists_tac `vr` \\ fs [updEnv_def]
\\ rw_sym_asm `absenv e = _`
\\ match_mp_tac validIntervalbounds_sound
\\ qexistsl_tac [`P`, `fVars`, `dVars`, `E1`] \\ fs[SUBSET_DEF]
\\ rpt strip_tac \\ first_x_assum match_mp_tac
\\ fs [Once freeVars_def, domain_union]
\\ metis_tac [])
>- (fs [updEnv_def]
\\ Cases_on `v = n` \\ fs[]
\\ rveq \\ fs [domain_union]))
>- (rpt strip_tac \\ fs []
>- (rveq
\\ qexists_tac `vr` \\ fs [updEnv_def]
\\ rw_sym_asm `absenv e = _`
\\ match_mp_tac validIntervalbounds_sound
\\ qexistsl_tac [`P`, `fVars`, `dVars`, `E1`] \\ fs[SUBSET_DEF]
\\ rpt strip_tac \\ first_x_assum match_mp_tac
\\ fs [Once freeVars_def, domain_union]
\\ metis_tac [])
>- (fs [updEnv_def]
\\ Cases_on `v = n` \\ fs[]
\\ rveq \\ fs [domain_union])))
>- (rpt strip_tac
\\ fs [updEnv_def]
\\ specialize `!v. v IN domain fVars ==> _` `v`
\\ specialize `v IN domain fVars ==> _` `v IN domain fVars`
\\ Cases_on `v = n` \\ fs []
\\ rveq
\\ `n IN domain (union fVars dVars)` by (fs [domain_union])))
\\ Cases_on `n = v` \\ rveq \\ fs []
\\ fs [domain_union]))
>- (inversion `bstep _ _ 0 _` bstep_cases \\ rveq
\\ inversion `bstep _ _ machineEpsilon _` bstep_cases \\ rveq
\\ rename1 `eval_exp 0 _ e vR`
......
INCLUDES = $(HOLDIR)/examples/machine-code/hoare-triple Infra
INCLUDES = $(HOLDIR)/examples/machine-code/hoare-triple Infra cakeml/translator
OPTIONS = QUIT_ON_FAILURE
ifdef POLY
......@@ -18,7 +18,8 @@ BARE_THYS = BasicProvers Defn HolKernel Parse Tactic monadsyntax \
optionTheory pairLib pairTheory pred_setTheory \
quantHeuristicsLib relationTheory res_quanTheory rich_listTheory \
sortingTheory sptreeTheory stringTheory sumTheory wordsTheory \
simpLib realTheory realLib RealArith Infra/preamble
simpLib realTheory realLib RealArith \
cakeml/translator/ml_translatorLib
DEPS = $(patsubst %,%.uo,$(BARE_THYS1)) $(PARENTHEAP)
......
......@@ -183,6 +183,12 @@ val interval_negation_valid = store_thm ("interval_negation_valid",
contained a iv ==> contained (- a) (negateInterval iv)``,
fs iv_ss);
val iv_neg_preserves_valid = store_thm ("iv_neg_preserves_valid",
``!iv.
valid iv ==> valid (negateInterval iv)``,
fs [valid_def, negateInterval_def, IVlo_def, IVhi_def]);
val interval_inversion_valid = store_thm ("interval_inversion_valid",
``!iv a.
(IVhi iv < 0 \/ 0 < IVlo iv) /\ contained a iv ==>
......@@ -221,6 +227,19 @@ 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",
``!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]
\\ match_mp_tac REAL_INV_LE_ANTIMONO_IMPR
\\ rpt CONJ_TAC \\ fs[]
\\ match_mp_tac REAL_LTE_TRANS
\\ asm_exists_tac \\ fs[]));
val interval_addition_valid = store_thm ("interval_addition_valid",
``!iv1 iv2. validIntervalAdd iv1 iv2 (addInterval iv1 iv2)``,
fs iv_ss \\ rpt strip_tac
......
......@@ -9,9 +9,12 @@ open preamble
open simpLib realTheory realLib RealArith pred_setTheory sptreeTheory
open AbbrevsTheory ExpressionsTheory RealSimpsTheory DaisyTactics
open ExpressionAbbrevsTheory IntervalArithTheory CommandsTheory ssaPrgsTheory
open sptreeLib sptreeTheory
val _ = new_theory "IntervalValidation";
val _ = Parse.hide "delta"; (* so that it can be used as a variable *)
val validIntervalbounds_def = Define `
validIntervalbounds e (absenv:analysisResult) (P:precond) (validVars:num_set) =
let (intv, _) = absenv e in
......@@ -66,7 +69,7 @@ val validIntervalboundsCmd_def = Define `
| Let x e g =>
if (validIntervalbounds e absenv P validVars /\
(FST (absenv e) = FST (absenv (Var x))))
then validIntervalboundsCmd g absenv P (Insert x validVars)
then validIntervalboundsCmd g absenv P (insert x () validVars)
else F
| Ret e =>
(validIntervalbounds e absenv P validVars)`;
......@@ -335,30 +338,33 @@ val validIntervalboundsCmd_sound = store_thm ("validIntervalboundsCmd_sound",
\\ inversion `bstep _ _ _ _` bstep_cases
\\ fs []
\\ first_x_assum match_mp_tac
\\ qexistsl_tac [`absenv`, `updEnv n v E`, `fVars`, `Insert n dVars`, `outVars`, `err`, `P`]
\\ qexistsl_tac [`absenv`, `updEnv n v E`, `fVars`, `insert n () dVars`, `outVars`, `err`, `P`]
\\ fs [updEnv_def]
\\ rpt conj_tac
>- (match_mp_tac ssa_equal_set
\\ qexists_tac `(Insert n (union fVars dVars))`
\\ fs [domain_union, Insert_def, domain_insert]
\\ qexists_tac `(insert n () (union fVars dVars))`
\\ fs [domain_union, domain_insert]
\\ once_rewrite_tac [UNION_COMM]
\\ fs [INSERT_UNION_EQ, UNION_COMM])
>- (rpt strip_tac
\\ Cases_on `v' = n`
\\ Cases_on `v' = n` \\ fs[]
>- (rveq
\\ qexists_tac `v` \\ fs []
\\ rw_sym_asm `FST (absenv e) = _`
\\ match_mp_tac validIntervalbounds_sound
\\ qexistsl_tac [`P`, `fVars`, `dVars`, `E`] \\ fs [SUBSET_DEF]
\\ rpt strip_tac
\\ first_x_assum match_mp_tac \\ fs [Once freeVars_def, domain_union]
\\ metis_tac [])
>- (rw[]
\\ first_x_assum match_mp_tac
\\ fs [Insert_def, domain_insert]))
>- (rveq
\\ rw_sym_asm `FST (absenv e) = _`
\\ match_mp_tac validIntervalbounds_sound
\\ qexistsl_tac [`P`, `fVars`, `dVars`, `E`] \\ fs [SUBSET_DEF]
\\ rpt strip_tac
\\ first_x_assum match_mp_tac \\ fs [Once freeVars_def, domain_union]
\\ metis_tac []))
>- (rpt strip_tac
\\ Cases_on `v' = n` \\ fs[domain_union])
>- (fs [Insert_def, domain_insert, SUBSET_DEF]
>- (fs [ domain_insert, SUBSET_DEF]
\\ rpt strip_tac
\\ first_x_assum match_mp_tac
\\ once_rewrite_tac [freeVars_def, domain_union]
......@@ -379,4 +385,44 @@ val validIntervalboundsCmd_sound = store_thm ("validIntervalboundsCmd_sound",
\\ fs [domain_union]
\\ CCONTR_TAC \\ metis_tac []));
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]
>- (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]
\\ 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))
\\ `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]
\\ 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) *)
);
val _ = export_theory();
Subproject commit df1790a2ee43b9d3c00d7b036784285b8f491c0f
open preamble
open simpLib realTheory realLib RealArith
open ml_translatorTheory ml_translatorLib std_preludeTheory;
val _ = new_theory "realProg";
val _ = translation_extends "std_prelude";
(* real_of_int *)
val real_of_int_def = Define `
real_of_int (i:int) = if i < 0 then - & (Num (-i)) else & (Num i):real`;
val real_of_int_num = store_thm("real_of_int_num[simp]",
``real_of_int (& n) = &n``,
rewrite_tac[real_of_int_def]
\\ Cases_on `&n`
\\ fs []);
val real_of_int_add = store_thm("real_of_int_add[simp]",
``real_of_int (m + n) = real_of_int m + real_of_int n``,
Cases_on `m` \\ Cases_on `n` \\ fs [real_of_int_def] \\ rw []
\\ fs [integerTheory.INT_ADD_CALCULATE]
\\ rw [] \\ fs [] \\ fs [GSYM NOT_LESS,realTheory.add_ints]);
val real_of_int_neg = store_thm("real_of_int_neg[simp]",
``real_of_int (-m) = -real_of_int m``,
Cases_on `m` \\ fs [real_of_int_def]);
val real_of_int_sub = store_thm("real_of_int_sub[simp]",
``real_of_int (m - n) = real_of_int m - real_of_int n``,
fs [integerTheory.int_sub,realTheory.real_sub]);
val real_of_int_mul = store_thm("real_of_int_mul[simp]",
``real_of_int (m * n) = real_of_int m * real_of_int n``,
Cases_on `m` \\ Cases_on `n` \\ fs [real_of_int_def] \\ rw []
\\ fs [integerTheory.INT_MUL_CALCULATE]);
(* -- *)
val REAL_TYPE_def = Define `
REAL_TYPE (r:real) =
\v. ?(n:int) (d:num). (r = (real_of_int n) / (real_of_num d)) /\
PAIR_TYPE INT NUM (n,d) v /\ d <> 0`;
val _ = add_type_inv ``REAL_TYPE`` ``:(int # num)``;
val pair_of_num_def = Define `
pair_of_num n = ((& (n:num)):int, 1:num)`;
val pair_of_num_v_thm = translate pair_of_num_def;
val Eval_REAL_NUM = Q.prove(
`!v. (NUM --> PAIR_TYPE INT NUM) pair_of_num v ==>
(NUM --> REAL_TYPE) ($&) v`,
SIMP_TAC (srw_ss()) [Arrow_def,AppReturns_def,REAL_TYPE_def,PULL_EXISTS,
FORALL_PROD] \\ rw [] \\ res_tac
\\ pop_assum (strip_assume_tac o SPEC_ALL)
\\ fs [] \\ asm_exists_tac \\ fs []
\\ qexists_tac `& x` \\ qexists_tac `1`
\\ fs [pair_of_num_def] \\ fs [real_of_int_def])
|> (fn th => MATCH_MP th pair_of_num_v_thm)
|> add_user_proved_v_thm;
val pair_le_def = Define `
pair_le (n1,d1) (n2,d2) = (n1 * & d2 <= n2 * & d1)`;
val pair_le_v_thm = translate pair_le_def;
val Eval_REAL_LE = Q.prove(
`!v. (PAIR_TYPE INT NUM --> PAIR_TYPE INT NUM --> BOOL) pair_le v ==>
(REAL_TYPE --> REAL_TYPE --> BOOL) ($<=) v`,
SIMP_TAC (srw_ss()) [Arrow_def,AppReturns_def,REAL_TYPE_def,PULL_EXISTS,
pair_le_def,FORALL_PROD] \\ rw [] \\ res_tac
\\ pop_assum (strip_assume_tac o SPEC_ALL)
\\ fs [] \\ asm_exists_tac \\ fs []
\\ rw [] \\ first_x_assum drule
\\ qmatch_goalsub_rename_tac `(empty_state with refs := refs2)`
\\ disch_then (qspec_then `refs2` mp_tac)
\\ strip_tac \\ rpt (asm_exists_tac \\ fs [])
\\ pop_assum mp_tac
\\ ntac 2 (qpat_x_assum `~_` mp_tac)
\\ rpt (pop_assum kall_tac)
\\ fs [BOOL_def] \\ rw [] \\ rveq
\\ EQ_TAC \\ rw []
\\ fs [realTheory.le_rat]
\\ Cases_on `n` \\ fs [real_of_int_def]
\\ Cases_on `n'` \\ fs [real_of_int_def]
\\ rfs [realTheory.REAL_MUL_LNEG,integerTheory.INT_MUL_CALCULATE]
\\ qpat_x_assum `(_ <= _:int)` mp_tac
\\ fs [integerTheory.INT_NOT_LE])
|> (fn th => MATCH_MP th pair_le_v_thm)
|> add_user_proved_v_thm;
val pair_lt_def = Define `
pair_lt (n1,d1) (n2,d2) = (n1 * & d2 < n2 * & d1)`;
val pair_lt_v_thm = translate pair_lt_def;
val Eval_REAL_LT = Q.prove(
`!v. (PAIR_TYPE INT NUM --> PAIR_TYPE INT NUM --> BOOL) pair_lt v ==>
(REAL_TYPE --> REAL_TYPE --> BOOL) ($<) v`,
SIMP_TAC (srw_ss()) [Arrow_def,AppReturns_def,REAL_TYPE_def,PULL_EXISTS,
pair_lt_def,FORALL_PROD] \\ rw [] \\ res_tac
\\ pop_assum (strip_assume_tac o SPEC_ALL)
\\ fs [] \\ asm_exists_tac \\ fs []
\\ rw [] \\ first_x_assum drule
\\ qmatch_goalsub_rename_tac `(empty_state with refs := refs2)`
\\ disch_then (qspec_then `refs2` mp_tac)
\\ strip_tac \\ rpt (asm_exists_tac \\ fs [])
\\ pop_assum mp_tac
\\ ntac 2 (qpat_x_assum `~_` mp_tac)
\\ rpt (pop_assum kall_tac)
\\ fs [BOOL_def] \\ rw [] \\ rveq
\\ EQ_TAC \\ rw []
\\ fs [realTheory.lt_rat]
\\ Cases_on `n` \\ fs [real_of_int_def]
\\ Cases_on `n'` \\ fs [real_of_int_def]
\\ rfs [realTheory.REAL_MUL_LNEG,integerTheory.INT_MUL_CALCULATE]
\\ qpat_x_assum `(_ <= _:int)` mp_tac
\\ fs [integerTheory.INT_NOT_LE])
|> (fn th => MATCH_MP th pair_lt_v_thm)
|> add_user_proved_v_thm;
val pair_add_def = Define `
pair_add (n1:int, d1:num) (n2, d2) = ((n1 * &d2) + (n2 * &d1),d1 * d2)`;
val pair_add_v_thm = translate pair_add_def;
val Eval_REAL_ADD = Q.prove(
`!v. (PAIR_TYPE INT NUM --> PAIR_TYPE INT NUM --> PAIR_TYPE INT NUM) pair_add v ==>
(REAL_TYPE --> REAL_TYPE --> REAL_TYPE) ($+) v`,
SIMP_TAC (srw_ss()) [Arrow_def,AppReturns_def,REAL_TYPE_def,PULL_EXISTS,
pair_add_def,FORALL_PROD] \\ rw [] \\ res_tac
\\ pop_assum (strip_assume_tac o SPEC_ALL)
\\ fs [] \\ asm_exists_tac \\ fs []
\\ rw [] \\ first_x_assum drule
\\ qmatch_goalsub_rename_tac `(empty_state with refs := refs2)`
\\ disch_then (qspec_then `refs2` mp_tac)
\\ strip_tac \\ rpt (asm_exists_tac \\ fs [])
\\ pop_assum mp_tac
\\ ntac 2 (qpat_x_assum `~_` mp_tac)
\\ rpt (pop_assum kall_tac)
\\ fs [PAIR_TYPE_def]
\\ rw [] \\ rveq \\ fs []
\\ qexists_tac `n * &d' + n' * &d`
\\ qexists_tac `d * d'`
\\ fs[real_of_int_add]
\\ fs [REAL_ADD_RAT]
\\ qspecl_then [`&d`, `real_of_int n'`] (fn thm => fs[Once thm]) REAL_MUL_COMM)
|> (fn th => MATCH_MP th pair_add_v_thm)
|> add_user_proved_v_thm;
val pair_sub_def = Define `
pair_sub (n1:int, d1:num) (n2, d2) = ((n1 * &d2) - (n2 * &d1),d1 * d2)`;
val pair_sub_v_thm = translate pair_sub_def;
val Eval_REAL_SUB = Q.prove(
`!v. (PAIR_TYPE INT NUM --> PAIR_TYPE INT NUM --> PAIR_TYPE INT NUM) pair_sub v ==>
(REAL_TYPE --> REAL_TYPE --> REAL_TYPE) ($-) v`,
SIMP_TAC (srw_ss()) [Arrow_def,AppReturns_def,REAL_TYPE_def,PULL_EXISTS,
pair_sub_def,FORALL_PROD] \\ rw [] \\ res_tac
\\ pop_assum (strip_assume_tac o SPEC_ALL)
\\ fs [] \\ asm_exists_tac \\ fs []
\\ rw [] \\ first_x_assum drule
\\ qmatch_goalsub_rename_tac `(empty_state with refs := refs2)`
\\ disch_then (qspec_then `refs2` mp_tac)
\\ strip_tac \\ rpt (asm_exists_tac \\ fs [])
\\ pop_assum mp_tac
\\ ntac 2 (qpat_x_assum `~_` mp_tac)
\\ rpt (pop_assum kall_tac)
\\ fs [PAIR_TYPE_def]
\\ rw [] \\ rveq \\ fs []
\\ qexists_tac `n * &d' - n' * &d`
\\ qexists_tac `d * d'`
\\ fs[real_of_int_sub]
\\ fs [real_sub, real_div, REAL_NEG_LMUL]
\\ fs [GSYM real_div]
\\ fs [REAL_ADD_RAT]
\\ qspecl_then [`&d`, `- real_of_int n'`] (fn thm => fs[Once thm]) REAL_MUL_COMM)
|> (fn th => MATCH_MP th pair_sub_v_thm)
|> add_user_proved_v_thm;
val real_neg_lem = prove(
``!(x:real). - x = 0 - x``,
fs[]);
val pair_neg_v_thm = translate real_neg_lem;
val pair_mul_def = Define `
pair_mul (n1,d1) (n2,d2) = (n1 * n2:int, d1 * d2:num)`;
val pair_mul_v_thm = translate pair_mul_def;
val Eval_REAL_MUL = Q.prove(
`!v. (PAIR_TYPE INT NUM --> PAIR_TYPE INT NUM --> PAIR_TYPE INT NUM) pair_mul v ==>
(REAL_TYPE --> REAL_TYPE --> REAL_TYPE) ($*) v`,
SIMP_TAC (srw_ss()) [Arrow_def,AppReturns_def,REAL_TYPE_def,PULL_EXISTS,
pair_mul_def,FORALL_PROD] \\ rw [] \\ res_tac
\\ pop_assum (strip_assume_tac o SPEC_ALL)
\\ fs [] \\ asm_exists_tac \\ fs []
\\ rw [] \\ first_x_assum drule
\\ qmatch_goalsub_rename_tac `(empty_state with refs := refs2)`
\\ disch_then (qspec_then `refs2` mp_tac)
\\ strip_tac \\ rpt (asm_exists_tac \\ fs [])
\\ pop_assum mp_tac
\\ ntac 2 (qpat_x_assum `~_` mp_tac)
\\ rpt (pop_assum kall_tac)
\\ fs [PAIR_TYPE_def]
\\ rw [] \\ rveq \\ fs []
\\ qexists_tac `n * n'` \\ fs []
\\ qexists_tac `d * d'` \\ fs []
\\ fs [real_of_int_mul]
\\ match_mp_tac REAL_EQ_RMUL_IMP
\\ qexists_tac `&(d * d')`
\\ `&(d * d') 0:real` by fs []
\\ drule REAL_DIV_RMUL
\\ simp_tac std_ss [] \\ fs [] \\ rw []
\\ qabbrev_tac `n1 = real_of_int n`
\\ qabbrev_tac `n2 = real_of_int n'`
\\ once_rewrite_tac [EQ_SYM_EQ]
\\ `n1 / &d * (n2 / &d') * &(</