Commit da20be68 authored by Magnus Myreen's avatar Magnus Myreen

Prove `EqualityType REAL_TYPE`

parent 774e566d
......@@ -335,4 +335,44 @@ val pair_div_v_thm =
|> DISCH_ALL |> REWRITE_RULE [pair_div_side_def] |> UNDISCH_ALL
|> add_user_proved_v_thm;
val EqualityType_REAL_TYPE = store_thm("EqualityType_REAL_TYPE",
``EqualityType REAL_TYPE``,
rw [EqualityType_def]
\\ fs [REAL_TYPE_def,PAIR_TYPE_def,INT_def,NUM_def] \\ EVAL_TAC
\\ rveq \\ fs []
\\ EQ_TAC \\ strip_tac \\ fs []
\\ fs [GSYM real_of_int_def]
\\ Cases_on `d = d'` \\ rveq
THEN1
(fs [realTheory.real_div,realTheory.REAL_INV_EQ_0] \\ fs []
\\ Cases_on `n` \\ Cases_on `n'` \\ fs [real_of_int_def])
\\ fs []
\\ `(real_of_int n / &d) * (&d * &d') = (real_of_int n' / &d') * (&d * &d')`
by fs [realTheory.REAL_EQ_RMUL]
\\ `real_of_int n / &d * &d = real_of_int n` by
(match_mp_tac realTheory.REAL_DIV_RMUL \\ fs [])
\\ `real_of_int n' / &d' * &d' = real_of_int n'` by
(match_mp_tac realTheory.REAL_DIV_RMUL \\ fs [])
\\ `real_of_int n * & d' = real_of_int n' * & d` by
metis_tac [realTheory.REAL_MUL_ASSOC,realTheory.REAL_MUL_COMM]
\\ pop_assum mp_tac
\\ ntac 3 (pop_assum kall_tac) \\ fs []
\\ Cases_on `n` \\ Cases_on `n'` \\ fs [real_of_int_def]
\\ rveq \\ fs []
\\ CCONTR_TAC \\ fs []
\\ rfs [realTheory.REAL_DIV_RMUL]
\\ fs [realTheory.real_div,realTheory.REAL_INV_EQ_0]
\\ rename1 `d1 * n1 = d2 * n2:num`
\\ `divides d2 (d1 * n1) /\
divides n2 (d1 * n1) /\
divides d1 (d2 * n2) /\
divides n1 (d2 * n2)` by
(fs [dividesTheory.divides_def] \\ metis_tac [MULT_COMM])
\\ `gcd d1 n2 = 1 /\ gcd d2 n1 = 1` by metis_tac [GCD_SYM]
\\ fs []
\\ imp_res_tac L_EUCLIDES
\\ imp_res_tac dividesTheory.DIVIDES_ANTISYM
\\ rveq \\ rfs [arithmeticTheory.EQ_MULT_RCANCEL])
|> store_eq_thm;
val _ = export_theory();
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