Commit 05bda039 authored by Magnus Myreen's avatar Magnus Myreen
Browse files

Simplify two proofs (as in hangout)

parent 61d70ff1
...@@ -49,18 +49,12 @@ val err_up = store_thm ("err_up", ...@@ -49,18 +49,12 @@ val err_up = store_thm ("err_up",
a - b <= c /\ a - b <= c /\
0 < a - b ==> 0 < a - b ==>
b <= a + c``, b <= a + c``,
rpt (strip_tac) \\
`b < a` by REAL_ASM_ARITH_TAC \\
`a <= b + c` by REAL_ASM_ARITH_TAC \\
`b + c <= a + c` by REAL_ASM_ARITH_TAC \\
REAL_ASM_ARITH_TAC); REAL_ASM_ARITH_TAC);
val REAL_LE_ADD_FLIP = store_thm ("REAL_LE_ADD_FLIP", val REAL_LE_ADD_FLIP = store_thm ("REAL_LE_ADD_FLIP",
``!a b (c:real). ``!a b (c:real).
a - b <= c ==> a - b <= c ==>
a - c <= b``, a - c <= b``,
rpt (strip_tac) \\
`a - b - c <= 0` by REAL_ASM_ARITH_TAC \\
REAL_ASM_ARITH_TAC); REAL_ASM_ARITH_TAC);
val _ = export_theory(); 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