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