src/HOL/Tools/Argo/argo_real.ML
author boehmes
Thu Sep 29 20:54:44 2016 +0200 (2016-09-29)
changeset 63960 3daf02070be5
child 63992 3aa9837d05c7
permissions -rw-r--r--
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes@63960
     1
(*  Title:      HOL/Tools/argo_real.ML
boehmes@63960
     2
    Author:     Sascha Boehme
boehmes@63960
     3
boehmes@63960
     4
Extension of the Argo tactic for the reals.
boehmes@63960
     5
*)
boehmes@63960
     6
boehmes@63960
     7
structure Argo_Real: sig end =
boehmes@63960
     8
struct
boehmes@63960
     9
boehmes@63960
    10
(* translating input terms *)
boehmes@63960
    11
boehmes@63960
    12
fun trans_type _ @{typ Real.real} tcx = SOME (Argo_Expr.Real, tcx)
boehmes@63960
    13
  | trans_type _ _ _ = NONE
boehmes@63960
    14
boehmes@63960
    15
fun trans_term f (@{const Groups.uminus_class.uminus (real)} $ t) tcx =
boehmes@63960
    16
      tcx |> f t |>> Argo_Expr.mk_neg |> SOME
boehmes@63960
    17
  | trans_term f (@{const Groups.plus_class.plus (real)} $ t1 $ t2) tcx =
boehmes@63960
    18
      tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_add2 |> SOME
boehmes@63960
    19
  | trans_term f (@{const Groups.minus_class.minus (real)} $ t1 $ t2) tcx =
boehmes@63960
    20
      tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_sub |> SOME
boehmes@63960
    21
  | trans_term f (@{const Groups.times_class.times (real)} $ t1 $ t2) tcx =
boehmes@63960
    22
      tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_mul |> SOME
boehmes@63960
    23
  | trans_term f (@{const Rings.divide_class.divide (real)} $ t1 $ t2) tcx =
boehmes@63960
    24
      tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_div |> SOME
boehmes@63960
    25
  | trans_term f (@{const Orderings.ord_class.min (real)} $ t1 $ t2) tcx =
boehmes@63960
    26
      tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_min |> SOME
boehmes@63960
    27
  | trans_term f (@{const Orderings.ord_class.max (real)} $ t1 $ t2) tcx =
boehmes@63960
    28
      tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_max |> SOME
boehmes@63960
    29
  | trans_term f (@{const Groups.abs_class.abs (real)} $ t) tcx =
boehmes@63960
    30
      tcx |> f t |>> Argo_Expr.mk_abs |> SOME
boehmes@63960
    31
  | trans_term f (@{const Orderings.ord_class.less (real)} $ t1 $ t2) tcx =
boehmes@63960
    32
      tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_lt |> SOME
boehmes@63960
    33
  | trans_term f (@{const Orderings.ord_class.less_eq (real)} $ t1 $ t2) tcx =
boehmes@63960
    34
      tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_le |> SOME
boehmes@63960
    35
  | trans_term _ t tcx =
boehmes@63960
    36
      (case try HOLogic.dest_number t of
boehmes@63960
    37
        SOME (@{typ Real.real}, n) => SOME (Argo_Expr.mk_num (Rat.of_int n), tcx)
boehmes@63960
    38
      | _ => NONE)
boehmes@63960
    39
boehmes@63960
    40
boehmes@63960
    41
(* reverse translation *)
boehmes@63960
    42
boehmes@63960
    43
fun mk_plus t1 t2 = @{const Groups.plus_class.plus (real)} $ t1 $ t2
boehmes@63960
    44
fun mk_sum ts = uncurry (fold_rev mk_plus) (split_last ts)
boehmes@63960
    45
fun mk_times t1 t2 = @{const Groups.times_class.times (real)} $ t1 $ t2
boehmes@63960
    46
fun mk_divide t1 t2 = @{const Rings.divide_class.divide (real)} $ t1 $ t2
boehmes@63960
    47
fun mk_le t1 t2 = @{const Orderings.ord_class.less_eq (real)} $ t1 $ t2
boehmes@63960
    48
fun mk_lt t1 t2 = @{const Orderings.ord_class.less (real)} $ t1 $ t2
boehmes@63960
    49
boehmes@63960
    50
fun mk_real_num i = HOLogic.mk_number @{typ Real.real} i
boehmes@63960
    51
boehmes@63960
    52
fun mk_number n =
boehmes@63960
    53
  let val (p, q) = Rat.dest n
boehmes@63960
    54
  in if q = 1 then mk_real_num p else mk_divide (mk_real_num p) (mk_real_num q) end
boehmes@63960
    55
boehmes@63960
    56
fun term_of _ (Argo_Expr.E (Argo_Expr.Num n, _)) = SOME (mk_number n)
boehmes@63960
    57
  | term_of f (Argo_Expr.E (Argo_Expr.Neg, [e])) =
boehmes@63960
    58
      SOME (@{const Groups.uminus_class.uminus (real)} $ f e)
boehmes@63960
    59
  | term_of f (Argo_Expr.E (Argo_Expr.Add, es)) = SOME (mk_sum (map f es))
boehmes@63960
    60
  | term_of f (Argo_Expr.E (Argo_Expr.Sub, [e1, e2])) =
boehmes@63960
    61
      SOME (@{const Groups.minus_class.minus (real)} $ f e1 $ f e2)
boehmes@63960
    62
  | term_of f (Argo_Expr.E (Argo_Expr.Mul, [e1, e2])) = SOME (mk_times (f e1) (f e2))
boehmes@63960
    63
  | term_of f (Argo_Expr.E (Argo_Expr.Div, [e1, e2])) = SOME (mk_divide (f e1) (f e2))
boehmes@63960
    64
  | term_of f (Argo_Expr.E (Argo_Expr.Min, [e1, e2])) =
boehmes@63960
    65
      SOME (@{const Orderings.ord_class.min (real)} $ f e1 $ f e2)
boehmes@63960
    66
  | term_of f (Argo_Expr.E (Argo_Expr.Max, [e1, e2])) =
boehmes@63960
    67
      SOME (@{const Orderings.ord_class.max (real)} $ f e1 $ f e2)
boehmes@63960
    68
  | term_of f (Argo_Expr.E (Argo_Expr.Abs, [e])) = SOME (@{const Groups.abs_class.abs (real)} $ f e)
boehmes@63960
    69
  | term_of f (Argo_Expr.E (Argo_Expr.Le, [e1, e2])) = SOME (mk_le (f e1) (f e2))
boehmes@63960
    70
  | term_of f (Argo_Expr.E (Argo_Expr.Lt, [e1, e2])) = SOME (mk_lt (f e1) (f e2))
boehmes@63960
    71
  | term_of _ _ = NONE
boehmes@63960
    72
boehmes@63960
    73
boehmes@63960
    74
(* proof replay for rewrite steps *)
boehmes@63960
    75
boehmes@63960
    76
fun mk_rewr thm = thm RS @{thm eq_reflection}
boehmes@63960
    77
boehmes@63960
    78
fun by_simp ctxt t = 
boehmes@63960
    79
  let fun prove {context, ...} = HEADGOAL (Simplifier.simp_tac context)
boehmes@63960
    80
  in Goal.prove ctxt [] [] (HOLogic.mk_Trueprop t) prove end
boehmes@63960
    81
boehmes@63960
    82
fun prove_num_pred ctxt n =
boehmes@63960
    83
  by_simp ctxt (uncurry mk_lt (apply2 mk_number (if @0 < n then (@0, n) else (n, @0))))
boehmes@63960
    84
boehmes@63960
    85
fun simp_conv ctxt t = Conv.rewr_conv (mk_rewr (by_simp ctxt t))
boehmes@63960
    86
boehmes@63960
    87
fun nums_conv mk f ctxt n m =
boehmes@63960
    88
  simp_conv ctxt (HOLogic.mk_eq (mk (mk_number n) (mk_number m), mk_number (f (n, m))))
boehmes@63960
    89
boehmes@63960
    90
val add_nums_conv = nums_conv mk_plus (op +)
boehmes@63960
    91
val mul_nums_conv = nums_conv mk_times (op *)
boehmes@63960
    92
val div_nums_conv = nums_conv mk_divide (op /)
boehmes@63960
    93
boehmes@63960
    94
fun cmp_nums_conv ctxt b ct =
boehmes@63960
    95
  let val t = if b then @{const HOL.True} else @{const HOL.False}
boehmes@63960
    96
  in simp_conv ctxt (HOLogic.mk_eq (Thm.term_of ct, t)) ct end
boehmes@63960
    97
boehmes@63960
    98
local
boehmes@63960
    99
boehmes@63960
   100
fun is_add2 (@{const Groups.plus_class.plus (real)} $ _ $ _) = true
boehmes@63960
   101
  | is_add2 _ = false
boehmes@63960
   102
boehmes@63960
   103
fun is_add3 (@{const Groups.plus_class.plus (real)} $ _ $ t) = is_add2 t
boehmes@63960
   104
  | is_add3 _ = false
boehmes@63960
   105
boehmes@63960
   106
val flatten_thm = mk_rewr @{lemma "(a::real) + b + c = a + (b + c)" by simp}
boehmes@63960
   107
  
boehmes@63960
   108
fun flatten_conv ct =
boehmes@63960
   109
  if is_add2 (Thm.term_of ct) then Argo_Tactic.flatten_conv flatten_conv flatten_thm ct
boehmes@63960
   110
  else Conv.all_conv ct
boehmes@63960
   111
boehmes@63960
   112
val swap_conv = Conv.rewrs_conv (map mk_rewr @{lemma 
boehmes@63960
   113
  "(a::real) + (b + c) = b + (a + c)"
boehmes@63960
   114
  "(a::real) + b = b + a"
boehmes@63960
   115
  by simp_all})
boehmes@63960
   116
boehmes@63960
   117
val assoc_conv = Conv.rewr_conv (mk_rewr @{lemma "(a::real) + (b + c) = (a + b) + c" by simp})
boehmes@63960
   118
boehmes@63960
   119
val norm_monom_thm = mk_rewr @{lemma "1 * (a::real) = a" by simp}
boehmes@63960
   120
fun norm_monom_conv n = if n = @1 then Conv.rewr_conv norm_monom_thm else Conv.all_conv
boehmes@63960
   121
boehmes@63960
   122
val add2_thms = map mk_rewr @{lemma
boehmes@63960
   123
  "n * (a::real) + m * a = (n + m) * a"
boehmes@63960
   124
  "n * (a::real) + a = (n + 1) * a"
boehmes@63960
   125
  "(a::real) + m * a = (1 + m) * a"
boehmes@63960
   126
  "(a::real) + a = (1 + 1) * a"
boehmes@63960
   127
  by algebra+}
boehmes@63960
   128
boehmes@63960
   129
val add3_thms = map mk_rewr @{lemma
boehmes@63960
   130
  "n * (a::real) + (m * a + b) = (n + m) * a + b"
boehmes@63960
   131
  "n * (a::real) + (a + b) = (n + 1) * a + b"
boehmes@63960
   132
  "(a::real) + (m * a + b) = (1 + m) * a + b"
boehmes@63960
   133
  "(a::real) + (a + b) = (1 + 1) * a + b"
boehmes@63960
   134
  by algebra+}
boehmes@63960
   135
boehmes@63960
   136
fun choose_conv cv2 cv3 ct = if is_add3 (Thm.term_of ct) then cv3 ct else cv2 ct
boehmes@63960
   137
boehmes@63960
   138
fun join_num_conv ctxt n m =
boehmes@63960
   139
  let val conv = add_nums_conv ctxt n m
boehmes@63960
   140
  in choose_conv conv (assoc_conv then_conv Conv.arg1_conv conv) end
boehmes@63960
   141
boehmes@63960
   142
fun join_monom_conv ctxt n m =
boehmes@63960
   143
  let
boehmes@63960
   144
    val conv = Conv.arg1_conv (add_nums_conv ctxt n m) then_conv norm_monom_conv (n + m)
boehmes@63960
   145
    fun seq_conv thms cv = Conv.rewrs_conv thms then_conv cv
boehmes@63960
   146
  in choose_conv (seq_conv add2_thms conv) (seq_conv add3_thms (Conv.arg1_conv conv)) end
boehmes@63960
   147
boehmes@63960
   148
fun join_conv NONE = join_num_conv
boehmes@63960
   149
  | join_conv (SOME _) = join_monom_conv
boehmes@63960
   150
boehmes@63960
   151
fun bubble_down_conv _ _ [] ct = Conv.no_conv ct
boehmes@63960
   152
  | bubble_down_conv _ _ [_] ct = Conv.all_conv ct
boehmes@63960
   153
  | bubble_down_conv ctxt i ((m1 as (n1, i1)) :: (m2 as (n2, i2)) :: ms) ct =
boehmes@63960
   154
      if i1 = i then
boehmes@63960
   155
        if i2 = i then
boehmes@63960
   156
          (join_conv i ctxt n1 n2 then_conv bubble_down_conv ctxt i ((n1 + n2, i) :: ms)) ct
boehmes@63960
   157
        else (swap_conv then_conv Conv.arg_conv (bubble_down_conv ctxt i (m1 :: ms))) ct
boehmes@63960
   158
      else Conv.arg_conv (bubble_down_conv ctxt i (m2 :: ms)) ct
boehmes@63960
   159
boehmes@63960
   160
fun drop_var i ms = filter_out (fn (_, i') => i' = i) ms
boehmes@63960
   161
boehmes@63960
   162
fun permute_conv _ [] [] ct = Conv.all_conv ct
boehmes@63960
   163
  | permute_conv ctxt (ms as ((_, i) :: _)) [] ct =
boehmes@63960
   164
      (bubble_down_conv ctxt i ms then_conv permute_conv ctxt (drop_var i ms) []) ct
boehmes@63960
   165
  | permute_conv ctxt ms1 ms2 ct =
boehmes@63960
   166
      let val (ms2', (_, i)) = split_last ms2
boehmes@63960
   167
      in (bubble_down_conv ctxt i ms1 then_conv permute_conv ctxt (drop_var i ms1) ms2') ct end
boehmes@63960
   168
boehmes@63960
   169
val no_monom_conv = Conv.rewr_conv (mk_rewr @{lemma "0 * (a::real) = 0" by simp})
boehmes@63960
   170
boehmes@63960
   171
val norm_sum_conv = Conv.rewrs_conv (map mk_rewr @{lemma
boehmes@63960
   172
  "0 * (a::real) + b = b"
boehmes@63960
   173
  "(a::real) + 0 * b = a"
boehmes@63960
   174
  "0 + (a::real) = a"
boehmes@63960
   175
  "(a::real) + 0 = a"
boehmes@63960
   176
  by simp_all})
boehmes@63960
   177
boehmes@63960
   178
fun drop0_conv ct =
boehmes@63960
   179
  if is_add2 (Thm.term_of ct) then
boehmes@63960
   180
    ((norm_sum_conv then_conv drop0_conv) else_conv Conv.arg_conv drop0_conv) ct
boehmes@63960
   181
  else Conv.try_conv no_monom_conv ct
boehmes@63960
   182
boehmes@63960
   183
fun full_add_conv ctxt ms1 ms2 =
boehmes@63960
   184
  if eq_list (op =) (ms1, ms2) then flatten_conv
boehmes@63960
   185
  else flatten_conv then_conv permute_conv ctxt ms1 ms2 then_conv drop0_conv
boehmes@63960
   186
boehmes@63960
   187
in
boehmes@63960
   188
boehmes@63960
   189
fun add_conv ctxt (ms1, ms2 as [(n, NONE)]) =
boehmes@63960
   190
      if n = @0 then full_add_conv ctxt ms1 [] else full_add_conv ctxt ms1 ms2
boehmes@63960
   191
  | add_conv ctxt (ms1, ms2) = full_add_conv ctxt ms1 ms2
boehmes@63960
   192
boehmes@63960
   193
end
boehmes@63960
   194
boehmes@63960
   195
val mul_sum_thm = mk_rewr @{lemma "(x::real) * (y + z) = x * y + x * z" by (rule ring_distribs)}
boehmes@63960
   196
fun mul_sum_conv ct =
boehmes@63960
   197
  Conv.try_conv (Conv.rewr_conv mul_sum_thm then_conv Conv.binop_conv mul_sum_conv) ct
boehmes@63960
   198
boehmes@63960
   199
fun var_of_add_cmp (_ $ _ $ (_ $ _ $ (_ $ _ $ Var v))) = v
boehmes@63960
   200
  | var_of_add_cmp t = raise TERM ("var_of_add_cmp", [t])
boehmes@63960
   201
boehmes@63960
   202
fun add_cmp_conv ctxt n thm =
boehmes@63960
   203
  let val v = var_of_add_cmp (Thm.prop_of thm)
boehmes@63960
   204
  in Conv.rewr_conv (Thm.instantiate ([], [(v, Thm.cterm_of ctxt (mk_number n))]) thm) end
boehmes@63960
   205
boehmes@63960
   206
fun mul_cmp_conv ctxt n pos_thm neg_thm =
boehmes@63960
   207
  let val thm = if @0 < n then pos_thm else neg_thm
boehmes@63960
   208
  in Conv.rewr_conv (prove_num_pred ctxt n RS thm) end
boehmes@63960
   209
boehmes@63960
   210
val neg_thm = mk_rewr @{lemma "-(x::real) = -1 * x" by simp}
boehmes@63960
   211
val sub_thm = mk_rewr @{lemma "(x::real) - y = x + -1 * y" by simp}
boehmes@63960
   212
val mul_zero_thm = mk_rewr @{lemma "0 * (x::real) = 0" by (rule mult_zero_left)}
boehmes@63960
   213
val mul_one_thm = mk_rewr @{lemma "1 * (x::real) = x" by (rule mult_1)}
boehmes@63960
   214
val mul_comm_thm = mk_rewr @{lemma "(x::real) * y = y * x" by simp}
boehmes@63960
   215
val mul_assoc_thm = mk_rewr @{lemma "(x::real) * (y * z) = (x * y) * z" by simp}
boehmes@63960
   216
val div_zero_thm = mk_rewr @{lemma "0 / (x::real) = 0" by simp}
boehmes@63960
   217
val div_one_thm = mk_rewr @{lemma "(x::real) / 1 = x" by simp}
boehmes@63960
   218
val div_mul_thm = mk_rewr @{lemma "(x::real) / y = x * (1 / y)" by simp}
boehmes@63960
   219
val div_inv_thm = mk_rewr @{lemma "(x::real) / y = (1 / y) * x" by simp}
boehmes@63960
   220
val div_left_thm = mk_rewr @{lemma "((x::real) * y) / z = x * (y / z)" by simp}
boehmes@63960
   221
val div_right_thm = mk_rewr @{lemma "(x::real) / (y * z) = (1 / y) * (x / z)" by simp}
boehmes@63960
   222
val min_thm = mk_rewr @{lemma "min (x::real) y = (if x <= y then x else y)" by (rule min_def)}
boehmes@63960
   223
val max_thm = mk_rewr @{lemma "max (x::real) y = (if x <= y then y else x)" by (rule max_def)}
boehmes@63960
   224
val abs_thm = mk_rewr @{lemma "abs (x::real) = (if 0 <= x then x else -x)" by simp}
boehmes@63960
   225
val eq_le_thm = mk_rewr @{lemma "((x::real) = y) = ((x <= y) & (y <= x))" by (rule order_eq_iff)}
boehmes@63960
   226
val add_le_thm = mk_rewr @{lemma "((x::real) <= y) = (x + n <= y + n)" by simp}
boehmes@63960
   227
val add_lt_thm = mk_rewr @{lemma "((x::real) < y) = (x + n < y + n)" by simp}
boehmes@63960
   228
val sub_le_thm = mk_rewr @{lemma "((x::real) <= y) = (x - y <= 0)" by simp}
boehmes@63960
   229
val sub_lt_thm = mk_rewr @{lemma "((x::real) < y) = (x - y < 0)" by simp}
boehmes@63960
   230
val pos_mul_le_thm = mk_rewr @{lemma "0 < n ==> ((x::real) <= y) = (n * x <= n * y)" by simp}
boehmes@63960
   231
val neg_mul_le_thm = mk_rewr @{lemma "n < 0 ==> ((x::real) <= y) = (n * y <= n * x)" by simp}
boehmes@63960
   232
val pos_mul_lt_thm = mk_rewr @{lemma "0 < n ==> ((x::real) < y) = (n * x < n * y)" by simp}
boehmes@63960
   233
val neg_mul_lt_thm = mk_rewr @{lemma "n < 0 ==> ((x::real) < y) = (n * y < n * x)" by simp}
boehmes@63960
   234
val not_le_thm = mk_rewr @{lemma "(~((x::real) <= y)) = (y < x)" by auto}
boehmes@63960
   235
val not_lt_thm = mk_rewr @{lemma "(~((x::real) < y)) = (y <= x)" by auto}
boehmes@63960
   236
boehmes@63960
   237
fun replay_rewr _ Argo_Proof.Rewr_Neg = Conv.rewr_conv neg_thm
boehmes@63960
   238
  | replay_rewr ctxt (Argo_Proof.Rewr_Add ps) = add_conv ctxt ps
boehmes@63960
   239
  | replay_rewr _ Argo_Proof.Rewr_Sub = Conv.rewr_conv sub_thm
boehmes@63960
   240
  | replay_rewr _ Argo_Proof.Rewr_Mul_Zero = Conv.rewr_conv mul_zero_thm
boehmes@63960
   241
  | replay_rewr _ Argo_Proof.Rewr_Mul_One = Conv.rewr_conv mul_one_thm
boehmes@63960
   242
  | replay_rewr ctxt (Argo_Proof.Rewr_Mul_Nums (n, m)) = mul_nums_conv ctxt n m
boehmes@63960
   243
  | replay_rewr _ Argo_Proof.Rewr_Mul_Comm = Conv.rewr_conv mul_comm_thm
boehmes@63960
   244
  | replay_rewr _ Argo_Proof.Rewr_Mul_Assoc = Conv.rewr_conv mul_assoc_thm
boehmes@63960
   245
  | replay_rewr _ Argo_Proof.Rewr_Mul_Sum = mul_sum_conv
boehmes@63960
   246
  | replay_rewr ctxt (Argo_Proof.Rewr_Div_Nums (n, m)) = div_nums_conv ctxt n m
boehmes@63960
   247
  | replay_rewr _ Argo_Proof.Rewr_Div_Zero = Conv.rewr_conv div_zero_thm
boehmes@63960
   248
  | replay_rewr _ Argo_Proof.Rewr_Div_One = Conv.rewr_conv div_one_thm
boehmes@63960
   249
  | replay_rewr _ Argo_Proof.Rewr_Div_Mul = Conv.rewr_conv div_mul_thm
boehmes@63960
   250
  | replay_rewr _ Argo_Proof.Rewr_Div_Inv = Conv.rewr_conv div_inv_thm
boehmes@63960
   251
  | replay_rewr _ Argo_Proof.Rewr_Div_Left = Conv.rewr_conv div_left_thm
boehmes@63960
   252
  | replay_rewr _ Argo_Proof.Rewr_Div_Right = Conv.rewr_conv div_right_thm
boehmes@63960
   253
  | replay_rewr _ Argo_Proof.Rewr_Min = Conv.rewr_conv min_thm
boehmes@63960
   254
  | replay_rewr _ Argo_Proof.Rewr_Max = Conv.rewr_conv max_thm
boehmes@63960
   255
  | replay_rewr _ Argo_Proof.Rewr_Abs = Conv.rewr_conv abs_thm
boehmes@63960
   256
  | replay_rewr _ Argo_Proof.Rewr_Eq_Le = Conv.rewr_conv eq_le_thm
boehmes@63960
   257
  | replay_rewr ctxt (Argo_Proof.Rewr_Ineq_Nums (_, b)) = cmp_nums_conv ctxt b
boehmes@63960
   258
  | replay_rewr ctxt (Argo_Proof.Rewr_Ineq_Add (Argo_Proof.Le, n)) =
boehmes@63960
   259
      add_cmp_conv ctxt n add_le_thm
boehmes@63960
   260
  | replay_rewr ctxt (Argo_Proof.Rewr_Ineq_Add (Argo_Proof.Lt, n)) =
boehmes@63960
   261
      add_cmp_conv ctxt n add_lt_thm
boehmes@63960
   262
  | replay_rewr _ (Argo_Proof.Rewr_Ineq_Sub Argo_Proof.Le) = Conv.rewr_conv sub_le_thm
boehmes@63960
   263
  | replay_rewr _ (Argo_Proof.Rewr_Ineq_Sub Argo_Proof.Lt) = Conv.rewr_conv sub_lt_thm
boehmes@63960
   264
  | replay_rewr ctxt (Argo_Proof.Rewr_Ineq_Mul (Argo_Proof.Le, n)) =
boehmes@63960
   265
      mul_cmp_conv ctxt n pos_mul_le_thm neg_mul_le_thm
boehmes@63960
   266
  | replay_rewr ctxt (Argo_Proof.Rewr_Ineq_Mul (Argo_Proof.Lt, n)) =
boehmes@63960
   267
      mul_cmp_conv ctxt n pos_mul_lt_thm neg_mul_lt_thm
boehmes@63960
   268
  | replay_rewr _ (Argo_Proof.Rewr_Not_Ineq Argo_Proof.Le) = Conv.rewr_conv not_le_thm
boehmes@63960
   269
  | replay_rewr _ (Argo_Proof.Rewr_Not_Ineq Argo_Proof.Lt) = Conv.rewr_conv not_lt_thm
boehmes@63960
   270
  | replay_rewr _ _ = Conv.no_conv
boehmes@63960
   271
boehmes@63960
   272
boehmes@63960
   273
(* proof replay *)
boehmes@63960
   274
boehmes@63960
   275
val combine_thms = @{lemma
boehmes@63960
   276
  "(a::real) < b ==> c < d ==> a + c < b + d"
boehmes@63960
   277
  "(a::real) < b ==> c <= d ==> a + c < b + d"
boehmes@63960
   278
  "(a::real) <= b ==> c < d ==> a + c < b + d"
boehmes@63960
   279
  "(a::real) <= b ==> c <= d ==> a + c <= b + d"
boehmes@63960
   280
  by auto}
boehmes@63960
   281
boehmes@63960
   282
fun combine thm1 thm2 = hd (Argo_Tactic.discharges thm2 (Argo_Tactic.discharges thm1 combine_thms))
boehmes@63960
   283
boehmes@63960
   284
fun replay _ _ Argo_Proof.Linear_Comb prems = SOME (uncurry (fold_rev combine) (split_last prems))
boehmes@63960
   285
  | replay _ _ _ _ = NONE
boehmes@63960
   286
boehmes@63960
   287
boehmes@63960
   288
(* real extension of the Argo solver *)
boehmes@63960
   289
boehmes@63960
   290
val _ = Theory.setup (Argo_Tactic.add_extension {
boehmes@63960
   291
  trans_type = trans_type,
boehmes@63960
   292
  trans_term = trans_term,
boehmes@63960
   293
  term_of = term_of,
boehmes@63960
   294
  replay_rewr = replay_rewr,
boehmes@63960
   295
  replay = replay})
boehmes@63960
   296
boehmes@63960
   297
end