Commit 774e566d authored by Magnus Myreen's avatar Magnus Myreen

Add `gcd n d = 1` into REAL_TYPE inv

parent f313722d
......@@ -42,7 +42,8 @@ val real_of_int_mul = store_thm("real_of_int_mul[simp]",
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`;
gcd (num_of_int n) d = 1 /\ d <> 0 /\
PAIR_TYPE INT NUM (n,d) v`;
val _ = add_type_inv ``REAL_TYPE`` ``:(int # num)``;
......@@ -157,7 +158,8 @@ 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]
\\ rewrite_tac [CONJ_ASSOC]
\\ once_rewrite_tac [CONJ_COMM]
\\ asm_exists_tac \\ fs [gcd_mod_thm]
\\ pop_assum kall_tac
\\ `gcd (num_of_int m) n <> 0` by fs []
......@@ -309,13 +311,15 @@ val Eval_REAL_INV = Q.prove(
(qexists_tac `&d`
\\ qexists_tac `n'` \\ fs []
\\ rewrite_tac [realTheory.REAL_INV_1OVER]
\\ fs [realTheory.div_ratr])
\\ fs [realTheory.div_ratr]
\\ once_rewrite_tac [GCD_SYM] \\ fs [])
THEN1
(qexists_tac `-&d`
\\ qexists_tac `n'` \\ fs []
\\ rewrite_tac [realTheory.REAL_INV_1OVER]
\\ fs [realTheory.div_ratr]
\\ fs [realTheory.neg_rat]))
\\ fs [realTheory.neg_rat]
\\ once_rewrite_tac [GCD_SYM] \\ fs []))
|> UNDISCH
|> (fn th => MATCH_MP th pair_inv_v_thm)
|> add_user_proved_v_thm;
......
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