Commit 80f0d0c4 authored by Magnus Myreen's avatar Magnus Myreen
Browse files

Move out REAL_TYPE from transScript.sml

parent 139aea84
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') * &(d * d') =
((n1 / &d) * &d) * ((n2 / &d') * &d')` by
(fs [AC REAL_MUL_ASSOC REAL_MUL_SYM]
\\ fs [REAL_MUL_ASSOC]
\\ fs [AC REAL_MUL_ASSOC REAL_MUL_SYM])
\\ pop_assum (fn th => rewrite_tac [th])
\\ `&d <> 0:real /\ &d' <> 0:real` by fs []
\\ fs [REAL_DIV_RMUL])
|> (fn th => MATCH_MP th pair_mul_v_thm)
|> add_user_proved_v_thm;
val pair_inv_def = Define `
pair_inv (n1,d1) =
(if n1 < 0 then - & d1 else & d1,num_of_int n1)`;
val pair_inv_v_thm = translate pair_inv_def;
val Eval_REAL_INV = Q.prove(
`PRECONDITION (r <> 0) ==>
!v. (PAIR_TYPE INT NUM --> PAIR_TYPE INT NUM) pair_inv v ==>
(Eq REAL_TYPE r --> REAL_TYPE) inv v`,
SIMP_TAC (srw_ss()) [Arrow_def,AppReturns_def,REAL_TYPE_def,PULL_EXISTS,
pair_mul_def,FORALL_PROD,Eq_def,PRECONDITION_def] \\ rw [] \\ res_tac
\\ pop_assum (strip_assume_tac o SPEC_ALL)
\\ fs [] \\ asm_exists_tac \\ fs []
\\ rw [] \\ first_x_assum drule
\\ disch_then (qspec_then `refs` mp_tac)
\\ strip_tac \\ rpt (asm_exists_tac \\ fs [])
\\ fs [realTheory.REAL_EQ_LDIV_EQ] \\ rveq
\\ fs [pair_inv_def,real_of_int_def]
\\ Cases_on `n` \\ fs []
THEN1
(qexists_tac `&d`
\\ qexists_tac `n'` \\ fs []
\\ rewrite_tac [realTheory.REAL_INV_1OVER]
\\ fs [realTheory.div_ratr])
THEN1
(qexists_tac `-&d`
\\ qexists_tac `n'` \\ fs []
\\ rewrite_tac [realTheory.REAL_INV_1OVER]
\\ fs [realTheory.div_ratr]
\\ fs [realTheory.neg_rat]))
|> UNDISCH
|> (fn th => MATCH_MP th pair_inv_v_thm)
|> add_user_proved_v_thm;
val _ = (next_ml_names := ["pair_div"])
val pair_div_v_thm = translate realTheory.real_div;
val pair_div_side_def = pair_div_v_thm
|> hyp |> hd |> rand |> repeat rator |> DB.match [] |> hd |> snd |> fst;
val pair_div_v_thm =
pair_div_v_thm
|> DISCH_ALL |> REWRITE_RULE [pair_div_side_def] |> UNDISCH_ALL
|> add_user_proved_v_thm;
val _ = export_theory();
open preamble
open simpLib realTheory realLib RealArith
open ml_translatorTheory ml_translatorLib std_preludeTheory;
open ml_translatorTheory ml_translatorLib realProgTheory;
open abbrevsTheory expressionsTheory RealSimpsTheory
open ExpressionAbbrevsTheory ErrorBoundsTheory IntervalArithTheory
......@@ -8,19 +8,12 @@ open IntervalValidationTheory EnvironmentsTheory CommandsTheory ssaPrgsTheory
val _ = new_theory "trans";
val _ = translation_extends "std_prelude";
val _ = translation_extends "realProg";
(*
TODO:
- consider putting all CakeML related files in a subdir called cakeml
(but keep using preamble from CakeML)
- split the REAL_TYPE setup into a file called realProgTheory
(following CakeML naming convention by which prog generating files
end with Prog suffix)
- for fast EVAL and good ML code, use sptrees to represent sets of
natural numbers (sptreeTheory in HOL) use type `:num_set` which is
an abbreviation for `:unit spt`
......@@ -50,282 +43,8 @@ val _ = (find_def_for_const := def_of_const);
val _ = translate IntervalValidationTheory.freeVars_def
(* 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_add (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_add 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 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') * &(d * d') =
((n1 / &d) * &d) * ((n2 / &d') * &d')` by
(fs [AC REAL_MUL_ASSOC REAL_MUL_SYM]
\\ fs [REAL_MUL_ASSOC]
\\ fs [AC REAL_MUL_ASSOC REAL_MUL_SYM])
\\ pop_assum (fn th => rewrite_tac [th])
\\ `&d <> 0:real /\ &d' <> 0:real` by fs []
\\ fs [REAL_DIV_RMUL])
|> (fn th => MATCH_MP th pair_mul_v_thm)
|> add_user_proved_v_thm;
val pair_inv_def = Define `
pair_inv (n1,d1) =
(if n1 < 0 then - & d1 else & d1,num_of_int n1)`;
val pair_inv_v_thm = translate pair_inv_def;
val Eval_REAL_INV = Q.prove(
`PRECONDITION (r <> 0) ==>
!v. (PAIR_TYPE INT NUM --> PAIR_TYPE INT NUM) pair_inv v ==>
(Eq REAL_TYPE r --> REAL_TYPE) inv v`,
SIMP_TAC (srw_ss()) [Arrow_def,AppReturns_def,REAL_TYPE_def,PULL_EXISTS,
pair_mul_def,FORALL_PROD,Eq_def,PRECONDITION_def] \\ rw [] \\ res_tac
\\ pop_assum (strip_assume_tac o SPEC_ALL)
\\ fs [] \\ asm_exists_tac \\ fs []
\\ rw [] \\ first_x_assum drule
\\ disch_then (qspec_then `refs` mp_tac)
\\ strip_tac \\ rpt (asm_exists_tac \\ fs [])
\\ fs [realTheory.REAL_EQ_LDIV_EQ] \\ rveq
\\ fs [pair_inv_def,real_of_int_def]
\\ Cases_on `n` \\ fs []
THEN1
(qexists_tac `&d`
\\ qexists_tac `n'` \\ fs []
\\ rewrite_tac [realTheory.REAL_INV_1OVER]
\\ fs [realTheory.div_ratr])
THEN1
(qexists_tac `-&d`
\\ qexists_tac `n'` \\ fs []
\\ rewrite_tac [realTheory.REAL_INV_1OVER]
\\ fs [realTheory.div_ratr]
\\ fs [realTheory.neg_rat]))
|> UNDISCH
|> (fn th => MATCH_MP th pair_inv_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 _ = (next_ml_names := ["pair_div"])
val pair_div_v_thm = translate realTheory.real_div;
val pair_div_side_def = pair_div_v_thm
|> hyp |> hd |> rand |> repeat rator |> DB.match [] |> hd |> snd |> fst;
val pair_div_v_thm =
pair_div_v_thm
|> DISCH_ALL |> REWRITE_RULE [pair_div_side_def] |> UNDISCH_ALL
|> add_user_proved_v_thm;
val divideInterval_v_thm = translate divideInterval_def;
(show_assums:=true);
val supersetInterval_v_thm = translate isSupersetInterval_def;
val validIvbounds_v_thm = translate validIntervalbounds_def;
......
Markdown is supported
0%