Commit f313722d authored by Magnus Myreen's avatar Magnus Myreen

Make add, sub, mul on real use GCD to compact rat repr

parent 9af160f8
open preamble
open simpLib realTheory realLib RealArith
open ml_translatorTheory ml_translatorLib std_preludeTheory;
open gcdTheory
val _ = new_theory "realProg";
......@@ -122,16 +123,74 @@ val Eval_REAL_LT = Q.prove(
|> (fn th => MATCH_MP th pair_lt_v_thm)
|> add_user_proved_v_thm;
val gcd_mod_def = Define `
gcd_mod a b = if a = 0:num then b else gcd_mod (b MOD a) a`
val gcd_mod_thm = prove(
``!a b. gcd_mod a b = gcd a b``,
recInduct (fetch "-" "gcd_mod_ind") \\ rw []
\\ once_rewrite_tac [gcd_mod_def,GCD_EFFICIENTLY] \\ rw []);
val res = translate gcd_mod_def
val gcd_mod_side = prove(
``!a b. gcd_mod_side a b = T``,
recInduct (fetch "-" "gcd_mod_ind") \\ rw []
\\ once_rewrite_tac [fetch "-" "gcd_mod_side_def"]
\\ fs [ADD1] \\ rw [] \\ fs [])
|> update_precondition;
val div_gcd_def = Define `
div_gcd a b =
let d = gcd_mod (num_of_int a) b in
if d = 0 \/ d = 1 then (a,b) else (a / &d, b DIV d)`;
val res = translate div_gcd_def;
val gcd_LESS_EQ = prove(
``!m n. n <> 0 ==> gcd m n <= n``,
recInduct gcd_ind \\ rw []
\\ once_rewrite_tac [gcd_def]
\\ rw [] \\ fs []);
val PAIR_TYPE_IMP_REAL_TYPE = prove(
``r = real_of_int m / & n /\ n <> 0 ==>
PAIR_TYPE INT NUM (div_gcd m n) v ==> REAL_TYPE r v``,
fs [REAL_TYPE_def,div_gcd_def] \\ rw []
\\ fs [] \\ once_rewrite_tac [CONJ_COMM] \\ fs [CONJ_ASSOC]
\\ asm_exists_tac \\ fs [gcd_mod_thm]
\\ pop_assum kall_tac
\\ `gcd (num_of_int m) n <> 0` by fs []
\\ `0 < gcd (num_of_int m) n` by simp []
\\ Cases_on `m` \\ simp [ZERO_DIV]
\\ fs [DIV_EQ_X,NOT_LESS,gcd_LESS_EQ]
\\ rename1 `gcd m n <> 1`
THEN1
(qspecl_then [`m`,`n`] mp_tac FACTOR_OUT_GCD \\ fs []
\\ strip_tac \\ qabbrev_tac `kk = gcd m n`
\\ pop_assum kall_tac \\ rveq \\ fs [MULT_DIV]
\\ rewrite_tac [GSYM REAL_OF_NUM_MUL]
\\ match_mp_tac REAL_DIV_LMUL_CANCEL \\ fs [])
\\ qspecl_then [`m`,`n`] mp_tac FACTOR_OUT_GCD \\ fs []
\\ strip_tac \\ qabbrev_tac `kk = gcd m n`
\\ pop_assum kall_tac \\ rveq \\ fs [MULT_DIV]
\\ rewrite_tac [GSYM REAL_OF_NUM_MUL,GSYM integerTheory.INT_MUL]
\\ rewrite_tac [integerTheory.INT_NEG_RMUL,realTheory.REAL_NEG_RMUL]
\\ simp [integerTheory.INT_DIV_LMUL,REAL_DIV_LMUL_CANCEL]);
val pair_add_def = Define `
pair_add (n1:int, d1:num) (n2, d2) = ((n1 * &d2) + (n2 * &d1),d1 * d2)`;
pair_add (n1:int, d1:num) (n2, d2) =
div_gcd ((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,
SIMP_TAC (srw_ss()) [Arrow_def,AppReturns_def,Once REAL_TYPE_def,PULL_EXISTS,
pair_add_def,FORALL_PROD] \\ rw [] \\ res_tac
\\ SIMP_TAC (srw_ss()) [Arrow_def,AppReturns_def,Once 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
......@@ -140,27 +199,26 @@ val Eval_REAL_ADD = Q.prove(
\\ 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]
\\ rpt (pop_assum kall_tac) \\ rw [] \\ pop_assum mp_tac
\\ match_mp_tac PAIR_TYPE_IMP_REAL_TYPE
\\ fs [REAL_ADD_RAT]
\\ qspecl_then [`&d`, `real_of_int n'`] (fn thm => fs[Once thm]) REAL_MUL_COMM)
\\ fs [AC REAL_MUL_COMM REAL_MUL_ASSOC])
|> (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)`;
pair_sub (n1:int, d1:num) (n2, d2) =
div_gcd ((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,
SIMP_TAC (srw_ss()) [Arrow_def,AppReturns_def,Once REAL_TYPE_def,PULL_EXISTS,
pair_sub_def,FORALL_PROD] \\ rw [] \\ res_tac
\\ SIMP_TAC (srw_ss()) [Arrow_def,AppReturns_def,Once 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
......@@ -169,16 +227,13 @@ val Eval_REAL_SUB = Q.prove(
\\ 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'`
\\ rpt (pop_assum kall_tac) \\ rw [] \\ pop_assum mp_tac
\\ match_mp_tac PAIR_TYPE_IMP_REAL_TYPE
\\ 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)
\\ fs [AC REAL_MUL_COMM REAL_MUL_ASSOC])
|> (fn th => MATCH_MP th pair_sub_v_thm)
|> add_user_proved_v_thm;
......@@ -189,15 +244,17 @@ val real_neg_lem = prove(
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)`;
pair_mul (n1,d1) (n2,d2) = div_gcd (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,
SIMP_TAC (srw_ss()) [Arrow_def,AppReturns_def,Once REAL_TYPE_def,PULL_EXISTS,
pair_mul_def,FORALL_PROD] \\ rw [] \\ res_tac
\\ SIMP_TAC (srw_ss()) [Arrow_def,AppReturns_def,Once 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
......@@ -206,11 +263,8 @@ val Eval_REAL_MUL = Q.prove(
\\ 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 []
\\ rpt (pop_assum kall_tac) \\ rw [] \\ pop_assum mp_tac
\\ match_mp_tac PAIR_TYPE_IMP_REAL_TYPE
\\ fs [real_of_int_mul]
\\ match_mp_tac REAL_EQ_RMUL_IMP
\\ qexists_tac `&(d * d')`
......
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