# HG changeset patch # User boehmes # Date 1475175284 -7200 # Node ID 3daf02070be5f54e28bcfd9fba7e4f29c575b173 # Parent f77dca1abf1b6845fe96607abe39660287a3fd64 new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic diff -r f77dca1abf1b -r 3daf02070be5 src/HOL/Argo.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Argo.thy Thu Sep 29 20:54:44 2016 +0200 @@ -0,0 +1,27 @@ +(* Title: HOL/Argo.thy + Author: Sascha Boehme +*) + +theory Argo +imports HOL +begin + +ML_file "~~/src/Tools/Argo/argo_expr.ML" +ML_file "~~/src/Tools/Argo/argo_term.ML" +ML_file "~~/src/Tools/Argo/argo_lit.ML" +ML_file "~~/src/Tools/Argo/argo_proof.ML" +ML_file "~~/src/Tools/Argo/argo_rewr.ML" +ML_file "~~/src/Tools/Argo/argo_cls.ML" +ML_file "~~/src/Tools/Argo/argo_common.ML" +ML_file "~~/src/Tools/Argo/argo_cc.ML" +ML_file "~~/src/Tools/Argo/argo_simplex.ML" +ML_file "~~/src/Tools/Argo/argo_thy.ML" +ML_file "~~/src/Tools/Argo/argo_heap.ML" +ML_file "~~/src/Tools/Argo/argo_cdcl.ML" +ML_file "~~/src/Tools/Argo/argo_core.ML" +ML_file "~~/src/Tools/Argo/argo_clausify.ML" +ML_file "~~/src/Tools/Argo/argo_solver.ML" + +ML_file "Tools/Argo/argo_tactic.ML" + +end diff -r f77dca1abf1b -r 3daf02070be5 src/HOL/ROOT --- a/src/HOL/ROOT Thu Sep 29 18:52:34 2016 +0200 +++ b/src/HOL/ROOT Thu Sep 29 20:54:44 2016 +0200 @@ -626,6 +626,7 @@ Sudoku Code_Timing Perm_Fragments + Argo_Examples theories [skip_proofs = false] Meson_Test document_files "root.bib" "root.tex" diff -r f77dca1abf1b -r 3daf02070be5 src/HOL/Real.thy --- a/src/HOL/Real.thy Thu Sep 29 18:52:34 2016 +0200 +++ b/src/HOL/Real.thy Thu Sep 29 20:54:44 2016 +0200 @@ -10,7 +10,7 @@ section \Development of the Reals using Cauchy Sequences\ theory Real -imports Rat +imports Rat Argo begin text \ @@ -1807,4 +1807,9 @@ for x y :: real by auto + +subsection \Setup for Argo\ + +ML_file "Tools/Argo/argo_real.ML" + end diff -r f77dca1abf1b -r 3daf02070be5 src/HOL/Tools/Argo/argo_real.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Argo/argo_real.ML Thu Sep 29 20:54:44 2016 +0200 @@ -0,0 +1,297 @@ +(* Title: HOL/Tools/argo_real.ML + Author: Sascha Boehme + +Extension of the Argo tactic for the reals. +*) + +structure Argo_Real: sig end = +struct + +(* translating input terms *) + +fun trans_type _ @{typ Real.real} tcx = SOME (Argo_Expr.Real, tcx) + | trans_type _ _ _ = NONE + +fun trans_term f (@{const Groups.uminus_class.uminus (real)} $ t) tcx = + tcx |> f t |>> Argo_Expr.mk_neg |> SOME + | trans_term f (@{const Groups.plus_class.plus (real)} $ t1 $ t2) tcx = + tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_add2 |> SOME + | trans_term f (@{const Groups.minus_class.minus (real)} $ t1 $ t2) tcx = + tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_sub |> SOME + | trans_term f (@{const Groups.times_class.times (real)} $ t1 $ t2) tcx = + tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_mul |> SOME + | trans_term f (@{const Rings.divide_class.divide (real)} $ t1 $ t2) tcx = + tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_div |> SOME + | trans_term f (@{const Orderings.ord_class.min (real)} $ t1 $ t2) tcx = + tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_min |> SOME + | trans_term f (@{const Orderings.ord_class.max (real)} $ t1 $ t2) tcx = + tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_max |> SOME + | trans_term f (@{const Groups.abs_class.abs (real)} $ t) tcx = + tcx |> f t |>> Argo_Expr.mk_abs |> SOME + | trans_term f (@{const Orderings.ord_class.less (real)} $ t1 $ t2) tcx = + tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_lt |> SOME + | trans_term f (@{const Orderings.ord_class.less_eq (real)} $ t1 $ t2) tcx = + tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_le |> SOME + | trans_term _ t tcx = + (case try HOLogic.dest_number t of + SOME (@{typ Real.real}, n) => SOME (Argo_Expr.mk_num (Rat.of_int n), tcx) + | _ => NONE) + + +(* reverse translation *) + +fun mk_plus t1 t2 = @{const Groups.plus_class.plus (real)} $ t1 $ t2 +fun mk_sum ts = uncurry (fold_rev mk_plus) (split_last ts) +fun mk_times t1 t2 = @{const Groups.times_class.times (real)} $ t1 $ t2 +fun mk_divide t1 t2 = @{const Rings.divide_class.divide (real)} $ t1 $ t2 +fun mk_le t1 t2 = @{const Orderings.ord_class.less_eq (real)} $ t1 $ t2 +fun mk_lt t1 t2 = @{const Orderings.ord_class.less (real)} $ t1 $ t2 + +fun mk_real_num i = HOLogic.mk_number @{typ Real.real} i + +fun mk_number n = + let val (p, q) = Rat.dest n + in if q = 1 then mk_real_num p else mk_divide (mk_real_num p) (mk_real_num q) end + +fun term_of _ (Argo_Expr.E (Argo_Expr.Num n, _)) = SOME (mk_number n) + | term_of f (Argo_Expr.E (Argo_Expr.Neg, [e])) = + SOME (@{const Groups.uminus_class.uminus (real)} $ f e) + | term_of f (Argo_Expr.E (Argo_Expr.Add, es)) = SOME (mk_sum (map f es)) + | term_of f (Argo_Expr.E (Argo_Expr.Sub, [e1, e2])) = + SOME (@{const Groups.minus_class.minus (real)} $ f e1 $ f e2) + | term_of f (Argo_Expr.E (Argo_Expr.Mul, [e1, e2])) = SOME (mk_times (f e1) (f e2)) + | term_of f (Argo_Expr.E (Argo_Expr.Div, [e1, e2])) = SOME (mk_divide (f e1) (f e2)) + | term_of f (Argo_Expr.E (Argo_Expr.Min, [e1, e2])) = + SOME (@{const Orderings.ord_class.min (real)} $ f e1 $ f e2) + | term_of f (Argo_Expr.E (Argo_Expr.Max, [e1, e2])) = + SOME (@{const Orderings.ord_class.max (real)} $ f e1 $ f e2) + | term_of f (Argo_Expr.E (Argo_Expr.Abs, [e])) = SOME (@{const Groups.abs_class.abs (real)} $ f e) + | term_of f (Argo_Expr.E (Argo_Expr.Le, [e1, e2])) = SOME (mk_le (f e1) (f e2)) + | term_of f (Argo_Expr.E (Argo_Expr.Lt, [e1, e2])) = SOME (mk_lt (f e1) (f e2)) + | term_of _ _ = NONE + + +(* proof replay for rewrite steps *) + +fun mk_rewr thm = thm RS @{thm eq_reflection} + +fun by_simp ctxt t = + let fun prove {context, ...} = HEADGOAL (Simplifier.simp_tac context) + in Goal.prove ctxt [] [] (HOLogic.mk_Trueprop t) prove end + +fun prove_num_pred ctxt n = + by_simp ctxt (uncurry mk_lt (apply2 mk_number (if @0 < n then (@0, n) else (n, @0)))) + +fun simp_conv ctxt t = Conv.rewr_conv (mk_rewr (by_simp ctxt t)) + +fun nums_conv mk f ctxt n m = + simp_conv ctxt (HOLogic.mk_eq (mk (mk_number n) (mk_number m), mk_number (f (n, m)))) + +val add_nums_conv = nums_conv mk_plus (op +) +val mul_nums_conv = nums_conv mk_times (op *) +val div_nums_conv = nums_conv mk_divide (op /) + +fun cmp_nums_conv ctxt b ct = + let val t = if b then @{const HOL.True} else @{const HOL.False} + in simp_conv ctxt (HOLogic.mk_eq (Thm.term_of ct, t)) ct end + +local + +fun is_add2 (@{const Groups.plus_class.plus (real)} $ _ $ _) = true + | is_add2 _ = false + +fun is_add3 (@{const Groups.plus_class.plus (real)} $ _ $ t) = is_add2 t + | is_add3 _ = false + +val flatten_thm = mk_rewr @{lemma "(a::real) + b + c = a + (b + c)" by simp} + +fun flatten_conv ct = + if is_add2 (Thm.term_of ct) then Argo_Tactic.flatten_conv flatten_conv flatten_thm ct + else Conv.all_conv ct + +val swap_conv = Conv.rewrs_conv (map mk_rewr @{lemma + "(a::real) + (b + c) = b + (a + c)" + "(a::real) + b = b + a" + by simp_all}) + +val assoc_conv = Conv.rewr_conv (mk_rewr @{lemma "(a::real) + (b + c) = (a + b) + c" by simp}) + +val norm_monom_thm = mk_rewr @{lemma "1 * (a::real) = a" by simp} +fun norm_monom_conv n = if n = @1 then Conv.rewr_conv norm_monom_thm else Conv.all_conv + +val add2_thms = map mk_rewr @{lemma + "n * (a::real) + m * a = (n + m) * a" + "n * (a::real) + a = (n + 1) * a" + "(a::real) + m * a = (1 + m) * a" + "(a::real) + a = (1 + 1) * a" + by algebra+} + +val add3_thms = map mk_rewr @{lemma + "n * (a::real) + (m * a + b) = (n + m) * a + b" + "n * (a::real) + (a + b) = (n + 1) * a + b" + "(a::real) + (m * a + b) = (1 + m) * a + b" + "(a::real) + (a + b) = (1 + 1) * a + b" + by algebra+} + +fun choose_conv cv2 cv3 ct = if is_add3 (Thm.term_of ct) then cv3 ct else cv2 ct + +fun join_num_conv ctxt n m = + let val conv = add_nums_conv ctxt n m + in choose_conv conv (assoc_conv then_conv Conv.arg1_conv conv) end + +fun join_monom_conv ctxt n m = + let + val conv = Conv.arg1_conv (add_nums_conv ctxt n m) then_conv norm_monom_conv (n + m) + fun seq_conv thms cv = Conv.rewrs_conv thms then_conv cv + in choose_conv (seq_conv add2_thms conv) (seq_conv add3_thms (Conv.arg1_conv conv)) end + +fun join_conv NONE = join_num_conv + | join_conv (SOME _) = join_monom_conv + +fun bubble_down_conv _ _ [] ct = Conv.no_conv ct + | bubble_down_conv _ _ [_] ct = Conv.all_conv ct + | bubble_down_conv ctxt i ((m1 as (n1, i1)) :: (m2 as (n2, i2)) :: ms) ct = + if i1 = i then + if i2 = i then + (join_conv i ctxt n1 n2 then_conv bubble_down_conv ctxt i ((n1 + n2, i) :: ms)) ct + else (swap_conv then_conv Conv.arg_conv (bubble_down_conv ctxt i (m1 :: ms))) ct + else Conv.arg_conv (bubble_down_conv ctxt i (m2 :: ms)) ct + +fun drop_var i ms = filter_out (fn (_, i') => i' = i) ms + +fun permute_conv _ [] [] ct = Conv.all_conv ct + | permute_conv ctxt (ms as ((_, i) :: _)) [] ct = + (bubble_down_conv ctxt i ms then_conv permute_conv ctxt (drop_var i ms) []) ct + | permute_conv ctxt ms1 ms2 ct = + let val (ms2', (_, i)) = split_last ms2 + in (bubble_down_conv ctxt i ms1 then_conv permute_conv ctxt (drop_var i ms1) ms2') ct end + +val no_monom_conv = Conv.rewr_conv (mk_rewr @{lemma "0 * (a::real) = 0" by simp}) + +val norm_sum_conv = Conv.rewrs_conv (map mk_rewr @{lemma + "0 * (a::real) + b = b" + "(a::real) + 0 * b = a" + "0 + (a::real) = a" + "(a::real) + 0 = a" + by simp_all}) + +fun drop0_conv ct = + if is_add2 (Thm.term_of ct) then + ((norm_sum_conv then_conv drop0_conv) else_conv Conv.arg_conv drop0_conv) ct + else Conv.try_conv no_monom_conv ct + +fun full_add_conv ctxt ms1 ms2 = + if eq_list (op =) (ms1, ms2) then flatten_conv + else flatten_conv then_conv permute_conv ctxt ms1 ms2 then_conv drop0_conv + +in + +fun add_conv ctxt (ms1, ms2 as [(n, NONE)]) = + if n = @0 then full_add_conv ctxt ms1 [] else full_add_conv ctxt ms1 ms2 + | add_conv ctxt (ms1, ms2) = full_add_conv ctxt ms1 ms2 + +end + +val mul_sum_thm = mk_rewr @{lemma "(x::real) * (y + z) = x * y + x * z" by (rule ring_distribs)} +fun mul_sum_conv ct = + Conv.try_conv (Conv.rewr_conv mul_sum_thm then_conv Conv.binop_conv mul_sum_conv) ct + +fun var_of_add_cmp (_ $ _ $ (_ $ _ $ (_ $ _ $ Var v))) = v + | var_of_add_cmp t = raise TERM ("var_of_add_cmp", [t]) + +fun add_cmp_conv ctxt n thm = + let val v = var_of_add_cmp (Thm.prop_of thm) + in Conv.rewr_conv (Thm.instantiate ([], [(v, Thm.cterm_of ctxt (mk_number n))]) thm) end + +fun mul_cmp_conv ctxt n pos_thm neg_thm = + let val thm = if @0 < n then pos_thm else neg_thm + in Conv.rewr_conv (prove_num_pred ctxt n RS thm) end + +val neg_thm = mk_rewr @{lemma "-(x::real) = -1 * x" by simp} +val sub_thm = mk_rewr @{lemma "(x::real) - y = x + -1 * y" by simp} +val mul_zero_thm = mk_rewr @{lemma "0 * (x::real) = 0" by (rule mult_zero_left)} +val mul_one_thm = mk_rewr @{lemma "1 * (x::real) = x" by (rule mult_1)} +val mul_comm_thm = mk_rewr @{lemma "(x::real) * y = y * x" by simp} +val mul_assoc_thm = mk_rewr @{lemma "(x::real) * (y * z) = (x * y) * z" by simp} +val div_zero_thm = mk_rewr @{lemma "0 / (x::real) = 0" by simp} +val div_one_thm = mk_rewr @{lemma "(x::real) / 1 = x" by simp} +val div_mul_thm = mk_rewr @{lemma "(x::real) / y = x * (1 / y)" by simp} +val div_inv_thm = mk_rewr @{lemma "(x::real) / y = (1 / y) * x" by simp} +val div_left_thm = mk_rewr @{lemma "((x::real) * y) / z = x * (y / z)" by simp} +val div_right_thm = mk_rewr @{lemma "(x::real) / (y * z) = (1 / y) * (x / z)" by simp} +val min_thm = mk_rewr @{lemma "min (x::real) y = (if x <= y then x else y)" by (rule min_def)} +val max_thm = mk_rewr @{lemma "max (x::real) y = (if x <= y then y else x)" by (rule max_def)} +val abs_thm = mk_rewr @{lemma "abs (x::real) = (if 0 <= x then x else -x)" by simp} +val eq_le_thm = mk_rewr @{lemma "((x::real) = y) = ((x <= y) & (y <= x))" by (rule order_eq_iff)} +val add_le_thm = mk_rewr @{lemma "((x::real) <= y) = (x + n <= y + n)" by simp} +val add_lt_thm = mk_rewr @{lemma "((x::real) < y) = (x + n < y + n)" by simp} +val sub_le_thm = mk_rewr @{lemma "((x::real) <= y) = (x - y <= 0)" by simp} +val sub_lt_thm = mk_rewr @{lemma "((x::real) < y) = (x - y < 0)" by simp} +val pos_mul_le_thm = mk_rewr @{lemma "0 < n ==> ((x::real) <= y) = (n * x <= n * y)" by simp} +val neg_mul_le_thm = mk_rewr @{lemma "n < 0 ==> ((x::real) <= y) = (n * y <= n * x)" by simp} +val pos_mul_lt_thm = mk_rewr @{lemma "0 < n ==> ((x::real) < y) = (n * x < n * y)" by simp} +val neg_mul_lt_thm = mk_rewr @{lemma "n < 0 ==> ((x::real) < y) = (n * y < n * x)" by simp} +val not_le_thm = mk_rewr @{lemma "(~((x::real) <= y)) = (y < x)" by auto} +val not_lt_thm = mk_rewr @{lemma "(~((x::real) < y)) = (y <= x)" by auto} + +fun replay_rewr _ Argo_Proof.Rewr_Neg = Conv.rewr_conv neg_thm + | replay_rewr ctxt (Argo_Proof.Rewr_Add ps) = add_conv ctxt ps + | replay_rewr _ Argo_Proof.Rewr_Sub = Conv.rewr_conv sub_thm + | replay_rewr _ Argo_Proof.Rewr_Mul_Zero = Conv.rewr_conv mul_zero_thm + | replay_rewr _ Argo_Proof.Rewr_Mul_One = Conv.rewr_conv mul_one_thm + | replay_rewr ctxt (Argo_Proof.Rewr_Mul_Nums (n, m)) = mul_nums_conv ctxt n m + | replay_rewr _ Argo_Proof.Rewr_Mul_Comm = Conv.rewr_conv mul_comm_thm + | replay_rewr _ Argo_Proof.Rewr_Mul_Assoc = Conv.rewr_conv mul_assoc_thm + | replay_rewr _ Argo_Proof.Rewr_Mul_Sum = mul_sum_conv + | replay_rewr ctxt (Argo_Proof.Rewr_Div_Nums (n, m)) = div_nums_conv ctxt n m + | replay_rewr _ Argo_Proof.Rewr_Div_Zero = Conv.rewr_conv div_zero_thm + | replay_rewr _ Argo_Proof.Rewr_Div_One = Conv.rewr_conv div_one_thm + | replay_rewr _ Argo_Proof.Rewr_Div_Mul = Conv.rewr_conv div_mul_thm + | replay_rewr _ Argo_Proof.Rewr_Div_Inv = Conv.rewr_conv div_inv_thm + | replay_rewr _ Argo_Proof.Rewr_Div_Left = Conv.rewr_conv div_left_thm + | replay_rewr _ Argo_Proof.Rewr_Div_Right = Conv.rewr_conv div_right_thm + | replay_rewr _ Argo_Proof.Rewr_Min = Conv.rewr_conv min_thm + | replay_rewr _ Argo_Proof.Rewr_Max = Conv.rewr_conv max_thm + | replay_rewr _ Argo_Proof.Rewr_Abs = Conv.rewr_conv abs_thm + | replay_rewr _ Argo_Proof.Rewr_Eq_Le = Conv.rewr_conv eq_le_thm + | replay_rewr ctxt (Argo_Proof.Rewr_Ineq_Nums (_, b)) = cmp_nums_conv ctxt b + | replay_rewr ctxt (Argo_Proof.Rewr_Ineq_Add (Argo_Proof.Le, n)) = + add_cmp_conv ctxt n add_le_thm + | replay_rewr ctxt (Argo_Proof.Rewr_Ineq_Add (Argo_Proof.Lt, n)) = + add_cmp_conv ctxt n add_lt_thm + | replay_rewr _ (Argo_Proof.Rewr_Ineq_Sub Argo_Proof.Le) = Conv.rewr_conv sub_le_thm + | replay_rewr _ (Argo_Proof.Rewr_Ineq_Sub Argo_Proof.Lt) = Conv.rewr_conv sub_lt_thm + | replay_rewr ctxt (Argo_Proof.Rewr_Ineq_Mul (Argo_Proof.Le, n)) = + mul_cmp_conv ctxt n pos_mul_le_thm neg_mul_le_thm + | replay_rewr ctxt (Argo_Proof.Rewr_Ineq_Mul (Argo_Proof.Lt, n)) = + mul_cmp_conv ctxt n pos_mul_lt_thm neg_mul_lt_thm + | replay_rewr _ (Argo_Proof.Rewr_Not_Ineq Argo_Proof.Le) = Conv.rewr_conv not_le_thm + | replay_rewr _ (Argo_Proof.Rewr_Not_Ineq Argo_Proof.Lt) = Conv.rewr_conv not_lt_thm + | replay_rewr _ _ = Conv.no_conv + + +(* proof replay *) + +val combine_thms = @{lemma + "(a::real) c < d ==> a + c c <= d ==> a + c c < d ==> a + c c <= d ==> a + c <= b + d" + by auto} + +fun combine thm1 thm2 = hd (Argo_Tactic.discharges thm2 (Argo_Tactic.discharges thm1 combine_thms)) + +fun replay _ _ Argo_Proof.Linear_Comb prems = SOME (uncurry (fold_rev combine) (split_last prems)) + | replay _ _ _ _ = NONE + + +(* real extension of the Argo solver *) + +val _ = Theory.setup (Argo_Tactic.add_extension { + trans_type = trans_type, + trans_term = trans_term, + term_of = term_of, + replay_rewr = replay_rewr, + replay = replay}) + +end diff -r f77dca1abf1b -r 3daf02070be5 src/HOL/Tools/Argo/argo_tactic.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Argo/argo_tactic.ML Thu Sep 29 20:54:44 2016 +0200 @@ -0,0 +1,730 @@ +(* Title: HOL/Tools/argo_tactic.ML + Author: Sascha Boehme + +HOL method and tactic for the Argo solver. +*) + +signature ARGO_TACTIC = +sig + val trace: string Config.T + val timeout: real Config.T + + (* extending the tactic *) + type trans_context = + Name.context * Argo_Expr.typ Typtab.table * (string * Argo_Expr.typ) Termtab.table + type ('a, 'b) trans = 'a -> trans_context -> 'b * trans_context + type ('a, 'b) trans' = 'a -> trans_context -> ('b * trans_context) option + type extension = { + trans_type: (typ, Argo_Expr.typ) trans -> (typ, Argo_Expr.typ) trans', + trans_term: (term, Argo_Expr.expr) trans -> (term, Argo_Expr.expr) trans', + term_of: (Argo_Expr.expr -> term) -> Argo_Expr.expr -> term option, + replay_rewr: Proof.context -> Argo_Proof.rewrite -> conv, + replay: (Argo_Expr.expr -> cterm) -> Proof.context -> Argo_Proof.rule -> thm list -> thm option} + val add_extension: extension -> theory -> theory + + (* proof utilities *) + val discharges: thm -> thm list -> thm list + val flatten_conv: conv -> thm -> conv + + (* interface to the tactic as well as the underlying checker and prover *) + datatype result = Satisfiable of term -> bool option | Unsatisfiable + val check: term list -> Proof.context -> result * Proof.context + val prove: thm list -> Proof.context -> thm option * Proof.context + val argo_tac: Proof.context -> thm list -> int -> tactic +end + +structure Argo_Tactic: ARGO_TACTIC = +struct + +(* readable fresh names for terms *) + +fun fresh_name n = Name.variant (case Long_Name.base_name n of "" => "x" | n' => n') + +fun fresh_type_name (Type (n, _)) = fresh_name n + | fresh_type_name (TFree (n, _)) = fresh_name n + | fresh_type_name (TVar ((n, i), _)) = fresh_name (n ^ "." ^ string_of_int i) + +fun fresh_term_name (Const (n, _)) = fresh_name n + | fresh_term_name (Free (n, _)) = fresh_name n + | fresh_term_name (Var ((n, i), _)) = fresh_name (n ^ "." ^ string_of_int i) + | fresh_term_name _ = fresh_name "" + + +(* tracing *) + +datatype mode = None | Basic | Full + +fun string_of_mode None = "none" + | string_of_mode Basic = "basic" + | string_of_mode Full = "full" + +fun requires_mode None = [] + | requires_mode Basic = [Basic, Full] + | requires_mode Full = [Full] + +val trace = Attrib.setup_config_string @{binding argo_trace} (K (string_of_mode None)) + +fun allows_mode ctxt = exists (equal (Config.get ctxt trace) o string_of_mode) o requires_mode + +fun output mode ctxt msg = if allows_mode ctxt mode then Output.tracing ("Argo: " ^ msg) else () +val tracing = output Basic +val full_tracing = output Full + +fun with_mode mode ctxt f = if allows_mode ctxt mode then f ctxt else () +val with_tracing = with_mode Basic +val with_full_tracing = with_mode Full + + +(* timeout *) + +val timeout = Attrib.setup_config_real @{binding argo_timeout} (K 10.0) + +fun time_of_timeout ctxt = Time.fromReal (Config.get ctxt timeout) + +fun with_timeout ctxt f x = Timeout.apply (time_of_timeout ctxt) f x + + +(* extending the tactic *) + +type trans_context = + Name.context * Argo_Expr.typ Typtab.table * (string * Argo_Expr.typ) Termtab.table + +type ('a, 'b) trans = 'a -> trans_context -> 'b * trans_context +type ('a, 'b) trans' = 'a -> trans_context -> ('b * trans_context) option + +type extension = { + trans_type: (typ, Argo_Expr.typ) trans -> (typ, Argo_Expr.typ) trans', + trans_term: (term, Argo_Expr.expr) trans -> (term, Argo_Expr.expr) trans', + term_of: (Argo_Expr.expr -> term) -> Argo_Expr.expr -> term option, + replay_rewr: Proof.context -> Argo_Proof.rewrite -> conv, + replay: (Argo_Expr.expr -> cterm) -> Proof.context -> Argo_Proof.rule -> thm list -> thm option} + +fun eq_extension ((serial1, _), (serial2, _)) = (serial1 = serial2) + +structure Extensions = Theory_Data +( + type T = (serial * extension) list + val empty = [] + val extend = I + val merge = merge eq_extension +) + +fun add_extension ext = Extensions.map (insert eq_extension (serial (), ext)) +fun get_extensions ctxt = Extensions.get (Proof_Context.theory_of ctxt) +fun apply_first ctxt f = get_first (fn (_, e) => f e) (get_extensions ctxt) + +fun ext_trans sel ctxt f x tcx = apply_first ctxt (fn ext => sel ext f x tcx) + +val ext_trans_type = ext_trans (fn {trans_type, ...}: extension => trans_type) +val ext_trans_term = ext_trans (fn {trans_term, ...}: extension => trans_term) + +fun ext_term_of ctxt f e = apply_first ctxt (fn {term_of, ...}: extension => term_of f e) + +fun ext_replay_rewr ctxt r = + get_extensions ctxt + |> map (fn (_, {replay_rewr, ...}: extension) => replay_rewr ctxt r) + |> Conv.first_conv + +fun ext_replay cprop_of ctxt rule prems = + (case apply_first ctxt (fn {replay, ...}: extension => replay cprop_of ctxt rule prems) of + SOME thm => thm + | NONE => raise THM ("failed to replay " ^ quote (Argo_Proof.string_of_rule rule), 0, [])) + + +(* translating input terms *) + +fun add_new_type T (names, types, terms) = + let + val (n, names') = fresh_type_name T names + val ty = Argo_Expr.Type n + in (ty, (names', Typtab.update (T, ty) types, terms)) end + +fun add_type T (tcx as (_, types, _)) = + (case Typtab.lookup types T of + SOME ty => (ty, tcx) + | NONE => add_new_type T tcx) + +fun trans_type _ @{typ HOL.bool} = pair Argo_Expr.Bool + | trans_type ctxt (Type (@{type_name "fun"}, [T1, T2])) = + trans_type ctxt T1 ##>> trans_type ctxt T2 #>> Argo_Expr.Func + | trans_type ctxt T = (fn tcx => + (case ext_trans_type ctxt (trans_type ctxt) T tcx of + SOME result => result + | NONE => add_type T tcx)) + +fun add_new_term ctxt t T tcx = + let + val (ty, (names, types, terms)) = trans_type ctxt T tcx + val (n, names') = fresh_term_name t names + val c = (n, ty) + in (Argo_Expr.mk_con c, (names', types, Termtab.update (t, c) terms)) end + +fun add_term ctxt t (tcx as (_, _, terms)) = + (case Termtab.lookup terms t of + SOME c => (Argo_Expr.mk_con c, tcx) + | NONE => add_new_term ctxt t (Term.fastype_of t) tcx) + +fun mk_eq @{typ HOL.bool} = Argo_Expr.mk_iff + | mk_eq _ = Argo_Expr.mk_eq + +fun trans_term _ @{const HOL.True} = pair Argo_Expr.true_expr + | trans_term _ @{const HOL.False} = pair Argo_Expr.false_expr + | trans_term ctxt (@{const HOL.Not} $ t) = trans_term ctxt t #>> Argo_Expr.mk_not + | trans_term ctxt (@{const HOL.conj} $ t1 $ t2) = + trans_term ctxt t1 ##>> trans_term ctxt t2 #>> uncurry Argo_Expr.mk_and2 + | trans_term ctxt (@{const HOL.disj} $ t1 $ t2) = + trans_term ctxt t1 ##>> trans_term ctxt t2 #>> uncurry Argo_Expr.mk_or2 + | trans_term ctxt (@{const HOL.implies} $ t1 $ t2) = + trans_term ctxt t1 ##>> trans_term ctxt t2 #>> uncurry Argo_Expr.mk_imp + | trans_term ctxt (Const (@{const_name HOL.If}, _) $ t1 $ t2 $ t3) = + trans_term ctxt t1 ##>> trans_term ctxt t2 ##>> trans_term ctxt t3 #>> + (fn ((u1, u2), u3) => Argo_Expr.mk_ite u1 u2 u3) + | trans_term ctxt (Const (@{const_name HOL.eq}, T) $ t1 $ t2) = + trans_term ctxt t1 ##>> trans_term ctxt t2 #>> uncurry (mk_eq (Term.domain_type T)) + | trans_term ctxt (t as (t1 $ t2)) = (fn tcx => + (case ext_trans_term ctxt (trans_term ctxt) t tcx of + SOME result => result + | NONE => tcx |> trans_term ctxt t1 ||>> trans_term ctxt t2 |>> uncurry Argo_Expr.mk_app)) + | trans_term ctxt t = (fn tcx => + (case ext_trans_term ctxt (trans_term ctxt) t tcx of + SOME result => result + | NONE => add_term ctxt t tcx)) + +fun translate ctxt prop = trans_term ctxt (HOLogic.dest_Trueprop prop) + + +(* invoking the solver *) + +type data = { + names: Name.context, + types: Argo_Expr.typ Typtab.table, + terms: (string * Argo_Expr.typ) Termtab.table, + argo: Argo_Solver.context} + +fun mk_data names types terms argo: data = {names=names, types=types, terms=terms, argo=argo} +val empty_data = mk_data Name.context Typtab.empty Termtab.empty Argo_Solver.context + +structure Solver_Data = Proof_Data +( + type T = data option + fun init _ = SOME empty_data +) + +datatype ('m, 'p) solver_result = Model of 'm | Proof of 'p + +fun raw_solve es argo = Model (Argo_Solver.assert es argo) + handle Argo_Proof.UNSAT proof => Proof proof + +fun value_of terms model t = + (case Termtab.lookup terms t of + SOME c => model c + | _ => NONE) + +fun trace_props props ctxt = + tracing ctxt (Pretty.string_of (Pretty.big_list "using these propositions:" + (map (Syntax.pretty_term ctxt) props))) + +fun trace_result ctxt ({elapsed, ...}: Timing.timing) msg = + tracing ctxt ("found a " ^ msg ^ " in " ^ string_of_int (Time.toMilliseconds elapsed) ^ " ms") + +fun solve props ctxt = + (case Solver_Data.get ctxt of + NONE => error "bad Argo solver context" + | SOME {names, types, terms, argo} => + let + val _ = with_tracing ctxt (trace_props props) + val (es, (names', types', terms')) = fold_map (translate ctxt) props (names, types, terms) + val _ = tracing ctxt "starting the prover" + in + (case Timing.timing (raw_solve es) argo of + (time, Proof proof) => + let val _ = trace_result ctxt time "proof" + in (Proof (terms', proof), Solver_Data.put NONE ctxt) end + | (time, Model argo') => + let + val _ = trace_result ctxt time "model" + val model = value_of terms' (Argo_Solver.model_of argo') + in (Model model, Solver_Data.put (SOME (mk_data names' types' terms' argo')) ctxt) end) + end) + + +(* reverse translation *) + +structure Contab = Table(type key = string * Argo_Expr.typ val ord = Argo_Expr.con_ord) + +fun mk_nary f ts = uncurry (fold_rev (curry f)) (split_last ts) + +fun mk_nary' d _ [] = d + | mk_nary' _ f ts = mk_nary f ts + +fun mk_ite t1 t2 t3 = + let + val T = Term.fastype_of t2 + val ite = Const (@{const_name HOL.If}, [@{typ HOL.bool}, T, T] ---> T) + in ite $ t1 $ t2 $ t3 end + +fun term_of _ (Argo_Expr.E (Argo_Expr.True, _)) = @{const HOL.True} + | term_of _ (Argo_Expr.E (Argo_Expr.False, _)) = @{const HOL.False} + | term_of cx (Argo_Expr.E (Argo_Expr.Not, [e])) = HOLogic.mk_not (term_of cx e) + | term_of cx (Argo_Expr.E (Argo_Expr.And, es)) = + mk_nary' @{const HOL.True} HOLogic.mk_conj (map (term_of cx) es) + | term_of cx (Argo_Expr.E (Argo_Expr.Or, es)) = + mk_nary' @{const HOL.False} HOLogic.mk_disj (map (term_of cx) es) + | term_of cx (Argo_Expr.E (Argo_Expr.Imp, [e1, e2])) = + HOLogic.mk_imp (term_of cx e1, term_of cx e2) + | term_of cx (Argo_Expr.E (Argo_Expr.Iff, [e1, e2])) = + HOLogic.mk_eq (term_of cx e1, term_of cx e2) + | term_of cx (Argo_Expr.E (Argo_Expr.Ite, [e1, e2, e3])) = + mk_ite (term_of cx e1) (term_of cx e2) (term_of cx e3) + | term_of cx (Argo_Expr.E (Argo_Expr.Eq, [e1, e2])) = + HOLogic.mk_eq (term_of cx e1, term_of cx e2) + | term_of cx (Argo_Expr.E (Argo_Expr.App, [e1, e2])) = + term_of cx e1 $ term_of cx e2 + | term_of (_, cons) (Argo_Expr.E (Argo_Expr.Con (c as (n, _)), _)) = + (case Contab.lookup cons c of + SOME t => t + | NONE => error ("Unexpected expression named " ^ quote n)) + | term_of (cx as (ctxt, _)) e = + (case ext_term_of ctxt (term_of cx) e of + SOME t => t + | NONE => raise Fail "bad expression") + +fun as_prop ct = Thm.apply @{cterm HOL.Trueprop} ct + +fun cterm_of ctxt cons e = Thm.cterm_of ctxt (term_of (ctxt, cons) e) +fun cprop_of ctxt cons e = as_prop (cterm_of ctxt cons e) + + +(* generic proof tools *) + +fun discharge thm rule = thm INCR_COMP rule +fun discharge2 thm1 thm2 rule = discharge thm2 (discharge thm1 rule) +fun discharges thm rules = [thm] RL rules + +fun under_assumption f ct = + let val cprop = as_prop ct + in Thm.implies_intr cprop (f (Thm.assume cprop)) end + +fun instantiate cv ct = Thm.instantiate ([], [(Term.dest_Var (Thm.term_of cv), ct)]) + + +(* proof replay for tautologies *) + +fun prove_taut ctxt ns t = Goal.prove ctxt ns [] (HOLogic.mk_Trueprop t) + (fn {context, ...} => HEADGOAL (Classical.fast_tac context)) + +fun with_frees ctxt n mk = + let + val ns = map (fn i => "P" ^ string_of_int i) (0 upto (n - 1)) + val ts = map (Free o rpair @{typ bool}) ns + val t = mk_nary HOLogic.mk_disj (mk ts) + in prove_taut ctxt ns t end + +fun taut_and1_term ts = mk_nary HOLogic.mk_conj ts :: map HOLogic.mk_not ts +fun taut_and2_term i ts = [HOLogic.mk_not (mk_nary HOLogic.mk_conj ts), nth ts i] +fun taut_or1_term i ts = [mk_nary HOLogic.mk_disj ts, HOLogic.mk_not (nth ts i)] +fun taut_or2_term ts = HOLogic.mk_not (mk_nary HOLogic.mk_disj ts) :: ts + +val iff_1_taut = @{lemma "P = Q | P | Q" by fast} +val iff_2_taut = @{lemma "P = Q | (~P) | (~Q)" by fast} +val iff_3_taut = @{lemma "~(P = Q) | (~P) | Q" by fast} +val iff_4_taut = @{lemma "~(P = Q) | P | (~Q)" by fast} +val ite_then_taut = @{lemma "~P | (if P then t else u) = t" by auto} +val ite_else_taut = @{lemma "P | (if P then t else u) = u" by auto} + +fun taut_rule_of ctxt (Argo_Proof.Taut_And_1 n) = with_frees ctxt n taut_and1_term + | taut_rule_of ctxt (Argo_Proof.Taut_And_2 (i, n)) = with_frees ctxt n (taut_and2_term i) + | taut_rule_of ctxt (Argo_Proof.Taut_Or_1 (i, n)) = with_frees ctxt n (taut_or1_term i) + | taut_rule_of ctxt (Argo_Proof.Taut_Or_2 n) = with_frees ctxt n taut_or2_term + | taut_rule_of _ Argo_Proof.Taut_Iff_1 = iff_1_taut + | taut_rule_of _ Argo_Proof.Taut_Iff_2 = iff_2_taut + | taut_rule_of _ Argo_Proof.Taut_Iff_3 = iff_3_taut + | taut_rule_of _ Argo_Proof.Taut_Iff_4 = iff_4_taut + | taut_rule_of _ Argo_Proof.Taut_Ite_Then = ite_then_taut + | taut_rule_of _ Argo_Proof.Taut_Ite_Else = ite_else_taut + +fun replay_taut ctxt k ct = + let val rule = taut_rule_of ctxt k + in Thm.instantiate (Thm.match (Thm.cprop_of rule, ct)) rule end + + +(* proof replay for conjunct extraction *) + +fun replay_conjunct 0 1 thm = thm + | replay_conjunct 0 _ thm = discharge thm @{thm conjunct1} + | replay_conjunct 1 2 thm = discharge thm @{thm conjunct2} + | replay_conjunct i n thm = replay_conjunct (i - 1) (n - 1) (discharge thm @{thm conjunct2}) + + +(* proof replay for rewrite steps *) + +fun mk_rewr thm = thm RS @{thm eq_reflection} + +fun not_nary_conv rule i ct = + if i > 1 then (Conv.rewr_conv rule then_conv Conv.arg_conv (not_nary_conv rule (i - 1))) ct + else Conv.all_conv ct + +val flatten_and_thm = @{lemma "(P1 & P2) & P3 == P1 & P2 & P3" by simp} +val flatten_or_thm = @{lemma "(P1 | P2) | P3 == P1 | P2 | P3" by simp} + +fun flatten_conv cv rule ct = ( + Conv.try_conv (Conv.arg_conv cv) then_conv + Conv.try_conv (Conv.rewr_conv rule then_conv cv)) ct + +fun flat_conj_conv ct = + (case Thm.term_of ct of + @{const HOL.conj} $ _ $ _ => flatten_conv flat_conj_conv flatten_and_thm ct + | _ => Conv.all_conv ct) + +fun flat_disj_conv ct = + (case Thm.term_of ct of + @{const HOL.disj} $ _ $ _ => flatten_conv flat_disj_conv flatten_or_thm ct + | _ => Conv.all_conv ct) + +fun explode rule1 rule2 thm = + explode rule1 rule2 (thm RS rule1) @ explode rule1 rule2 (thm RS rule2) handle THM _ => [thm] +val explode_conj = explode @{thm conjunct1} @{thm conjunct2} +val explode_ndis = explode @{lemma "~(P | Q) ==> ~P" by auto} @{lemma "~(P | Q) ==> ~Q" by auto} + +fun pick_false i thms = nth thms i + +fun pick_dual rule (i1, i2) thms = + rule OF [nth thms i1, nth thms i2] handle THM _ => rule OF [nth thms i2, nth thms i1] +val pick_dual_conj = pick_dual @{lemma "~P ==> P ==> False" by auto} +val pick_dual_ndis = pick_dual @{lemma "~P ==> P ==> ~True" by auto} + +fun join thm0 rule is thms = + let + val l = length thms + val thms' = fold (fn i => cons (if 0 <= i andalso i < l then nth thms i else thm0)) is [] + in fold (fn thm => fn thm' => discharge2 thm thm' rule) (tl thms') (hd thms') end + +val join_conj = join @{lemma "True" by auto} @{lemma "P ==> Q ==> P & Q" by auto} +val join_ndis = join @{lemma "~False" by auto} @{lemma "~P ==> ~Q ==> ~(P | Q)" by auto} + +val false_thm = @{lemma "False ==> P" by auto} +val ntrue_thm = @{lemma "~True ==> P" by auto} +val iff_conj_thm = @{lemma "(P ==> Q) ==> (Q ==> P) ==> P = Q" by auto} +val iff_ndis_thm = @{lemma "(~P ==> ~Q) ==> (~Q ==> ~P) ==> P = Q" by auto} + +fun iff_intro rule lf rf ct = + let + val lhs = under_assumption lf ct + val rhs = rf (Thm.dest_arg (snd (Thm.dest_implies (Thm.cprop_of lhs)))) + in mk_rewr (discharge2 lhs rhs rule) end + +fun with_conj f g ct = iff_intro iff_conj_thm (f o explode_conj) g ct +fun with_ndis f g ct = iff_intro iff_ndis_thm (f o explode_ndis) g (Thm.apply @{cterm HOL.Not} ct) + +fun swap_indices n iss = map (fn i => find_index (fn is => member (op =) is i) iss) (0 upto (n - 1)) +fun sort_nary w f g (n, iss) = w (f (map hd iss)) (under_assumption (f (swap_indices n iss) o g)) +val sort_conj = sort_nary with_conj join_conj explode_conj +val sort_ndis = sort_nary with_ndis join_ndis explode_ndis + +val not_true_thm = mk_rewr @{lemma "(~True) = False" by auto} +val not_false_thm = mk_rewr @{lemma "(~False) = True" by auto} +val not_not_thm = mk_rewr @{lemma "(~~P) = P" by auto} +val not_and_thm = mk_rewr @{lemma "(~(P & Q)) = (~P | ~Q)" by auto} +val not_or_thm = mk_rewr @{lemma "(~(P | Q)) = (~P & ~Q)" by auto} +val not_iff_thms = map mk_rewr + @{lemma "(~((~P) = Q)) = (P = Q)" "(~(P = (~Q))) = (P = Q)" "(~(P = Q)) = ((~P) = Q)" by auto} +val iff_true_thms = map mk_rewr @{lemma "(True = P) = P" "(P = True) = P" by auto} +val iff_false_thms = map mk_rewr @{lemma "(False = P) = (~P)" "(P = False) = (~P)" by auto} +val iff_not_not_thm = mk_rewr @{lemma "((~P) = (~Q)) = (P = Q)" by auto} +val iff_refl_thm = mk_rewr @{lemma "(P = P) = True" by auto} +val iff_symm_thm = mk_rewr @{lemma "(P = Q) = (Q = P)" by auto} +val iff_dual_thms = map mk_rewr @{lemma "(P = (~P)) = False" "((~P) = P) = False" by auto} +val imp_thm = mk_rewr @{lemma "(P --> Q) = (~P | Q)" by auto} +val ite_prop_thm = mk_rewr @{lemma "(If P Q R) = ((~P | Q) & (P | R) & (Q | R))" by auto} +val ite_true_thm = mk_rewr @{lemma "(If True t u) = t" by auto} +val ite_false_thm = mk_rewr @{lemma "(If False t u) = u" by auto} +val ite_eq_thm = mk_rewr @{lemma "(If P t t) = t" by auto} +val eq_refl_thm = mk_rewr @{lemma "(t = t) = True" by auto} +val eq_symm_thm = mk_rewr @{lemma "(t1 = t2) = (t2 = t1)" by auto} + +fun replay_rewr _ Argo_Proof.Rewr_Not_True = Conv.rewr_conv not_true_thm + | replay_rewr _ Argo_Proof.Rewr_Not_False = Conv.rewr_conv not_false_thm + | replay_rewr _ Argo_Proof.Rewr_Not_Not = Conv.rewr_conv not_not_thm + | replay_rewr _ (Argo_Proof.Rewr_Not_And i) = not_nary_conv not_and_thm i + | replay_rewr _ (Argo_Proof.Rewr_Not_Or i) = not_nary_conv not_or_thm i + | replay_rewr _ Argo_Proof.Rewr_Not_Iff = Conv.rewrs_conv not_iff_thms + | replay_rewr _ (Argo_Proof.Rewr_And_False i) = with_conj (pick_false i) (K false_thm) + | replay_rewr _ (Argo_Proof.Rewr_And_Dual ip) = with_conj (pick_dual_conj ip) (K false_thm) + | replay_rewr _ (Argo_Proof.Rewr_And_Sort is) = flat_conj_conv then_conv sort_conj is + | replay_rewr _ (Argo_Proof.Rewr_Or_True i) = with_ndis (pick_false i) (K ntrue_thm) + | replay_rewr _ (Argo_Proof.Rewr_Or_Dual ip) = with_ndis (pick_dual_ndis ip) (K ntrue_thm) + | replay_rewr _ (Argo_Proof.Rewr_Or_Sort is) = flat_disj_conv then_conv sort_ndis is + | replay_rewr _ Argo_Proof.Rewr_Iff_True = Conv.rewrs_conv iff_true_thms + | replay_rewr _ Argo_Proof.Rewr_Iff_False = Conv.rewrs_conv iff_false_thms + | replay_rewr _ Argo_Proof.Rewr_Iff_Not_Not = Conv.rewr_conv iff_not_not_thm + | replay_rewr _ Argo_Proof.Rewr_Iff_Refl = Conv.rewr_conv iff_refl_thm + | replay_rewr _ Argo_Proof.Rewr_Iff_Symm = Conv.rewr_conv iff_symm_thm + | replay_rewr _ Argo_Proof.Rewr_Iff_Dual = Conv.rewrs_conv iff_dual_thms + | replay_rewr _ Argo_Proof.Rewr_Imp = Conv.rewr_conv imp_thm + | replay_rewr _ Argo_Proof.Rewr_Ite_Prop = Conv.rewr_conv ite_prop_thm + | replay_rewr _ Argo_Proof.Rewr_Ite_True = Conv.rewr_conv ite_true_thm + | replay_rewr _ Argo_Proof.Rewr_Ite_False = Conv.rewr_conv ite_false_thm + | replay_rewr _ Argo_Proof.Rewr_Ite_Eq = Conv.rewr_conv ite_eq_thm + | replay_rewr _ Argo_Proof.Rewr_Eq_Refl = Conv.rewr_conv eq_refl_thm + | replay_rewr _ Argo_Proof.Rewr_Eq_Symm = Conv.rewr_conv eq_symm_thm + | replay_rewr ctxt r = ext_replay_rewr ctxt r + +fun binop_conv cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2 + +fun replay_conv _ Argo_Proof.Keep_Conv ct = Conv.all_conv ct + | replay_conv ctxt (Argo_Proof.Then_Conv (c1, c2)) ct = + (replay_conv ctxt c1 then_conv replay_conv ctxt c2) ct + | replay_conv ctxt (Argo_Proof.Args_Conv cs) ct = replay_args_conv ctxt cs ct + | replay_conv ctxt (Argo_Proof.Rewr_Conv r) ct = replay_rewr ctxt r ct + +and replay_args_conv _ [] ct = Conv.all_conv ct + | replay_args_conv ctxt [c] ct = Conv.arg_conv (replay_conv ctxt c) ct + | replay_args_conv ctxt [c1, c2] ct = binop_conv (replay_conv ctxt c1) (replay_conv ctxt c2) ct + | replay_args_conv ctxt (c :: cs) ct = + (case Term.head_of (Thm.term_of ct) of + Const (@{const_name HOL.If}, _) => + let val (cs', c') = split_last cs + in Conv.combination_conv (replay_args_conv ctxt (c :: cs')) (replay_conv ctxt c') ct end + | _ => binop_conv (replay_conv ctxt c) (replay_args_conv ctxt cs) ct) + +fun replay_rewrite ctxt c thm = Conv.fconv_rule (HOLogic.Trueprop_conv (replay_conv ctxt c)) thm + + +(* proof replay for clauses *) + +val prep_clause_rule = @{lemma "P ==> ~P ==> False" by fast} +val extract_lit_rule = @{lemma "(~(P | Q) ==> False) ==> ~P ==> ~Q ==> False" by fast} + +fun add_lit i thm lits = + let val ct = Thm.cprem_of thm 1 + in (Thm.implies_elim thm (Thm.assume ct), (i, ct) :: lits) end + +fun extract_lits [] _ = error "Bad clause" + | extract_lits [i] (thm, lits) = add_lit i thm lits + | extract_lits (i :: is) (thm, lits) = + extract_lits is (add_lit i (discharge thm extract_lit_rule) lits) + +fun lit_ord ((l1, _), (l2, _)) = int_ord (abs l1, abs l2) + +fun replay_with_lits [] thm lits = (thm, lits) + | replay_with_lits is thm lits = + extract_lits is (discharge thm prep_clause_rule, lits) + ||> Ord_List.make lit_ord + +fun replay_clause is thm = replay_with_lits is thm [] + + +(* proof replay for unit resolution *) + +val unit_rule = @{lemma "(P ==> False) ==> (~P ==> False) ==> False" by fast} +val unit_rule_var = Thm.dest_arg (Thm.dest_arg1 (Thm.cprem_of unit_rule 1)) +val bogus_ct = @{cterm HOL.True} + +fun replay_unit_res lit (pthm, plits) (nthm, nlits) = + let + val plit = the (AList.lookup (op =) plits lit) + val nlit = the (AList.lookup (op =) nlits (~lit)) + val prune = Ord_List.remove lit_ord (lit, bogus_ct) + in + unit_rule + |> instantiate unit_rule_var (Thm.dest_arg plit) + |> Thm.elim_implies (Thm.implies_intr plit pthm) + |> Thm.elim_implies (Thm.implies_intr nlit nthm) + |> rpair (Ord_List.union lit_ord (prune nlits) (prune plits)) + end + + +(* proof replay for hypothesis *) + +val dneg_rule = @{lemma "~~P ==> P" by auto} + +fun replay_hyp i ct = + if i < 0 then (Thm.assume ct, [(~i, ct)]) + else + let val cu = as_prop (Thm.apply @{cterm HOL.Not} (Thm.apply @{cterm HOL.Not} (Thm.dest_arg ct))) + in (discharge (Thm.assume cu) dneg_rule, [(~i, cu)]) end + + +(* proof replay for lemma *) + +fun replay_lemma is (thm, lits) = replay_with_lits is thm lits + + +(* proof replay for reflexivity *) + +val refl_rule = @{thm refl} +val refl_rule_var = Thm.dest_arg1 (Thm.dest_arg (Thm.cprop_of refl_rule)) + +fun replay_refl ct = Thm.instantiate (Thm.match (refl_rule_var, ct)) refl_rule + + +(* proof replay for symmetry *) + +val symm_rules = @{lemma "a = b ==> b = a" "~(a = b) ==> ~(b = a)" by simp_all} + +fun replay_symm thm = hd (discharges thm symm_rules) + + +(* proof replay for transitivity *) + +val trans_rules = @{lemma + "~(a = b) ==> b = c ==> ~(a = c)" + "a = b ==> ~(b = c) ==> ~(a = c)" + "a = b ==> b = c ==> a = c" + by simp_all} + +fun replay_trans thm1 thm2 = hd (discharges thm2 (discharges thm1 trans_rules)) + + +(* proof replay for congruence *) + +fun replay_cong thm1 thm2 = discharge thm2 (discharge thm1 @{thm cong}) + + +(* proof replay for substitution *) + +val subst_rule1 = @{lemma "~(p a) ==> p = q ==> a = b ==> ~(q b)" by simp} +val subst_rule2 = @{lemma "p a ==> p = q ==> a = b ==> q b" by simp} + +fun replay_subst thm1 thm2 thm3 = + subst_rule1 OF [thm1, thm2, thm3] handle THM _ => subst_rule2 OF [thm1, thm2, thm3] + + +(* proof replay *) + +structure Thm_Cache = Table(type key = Argo_Proof.proof_id val ord = Argo_Proof.proof_id_ord) + +val unclausify_rule1 = @{lemma "(~P ==> False) ==> P" by auto} +val unclausify_rule2 = @{lemma "(P ==> False) ==> ~P" by auto} + +fun unclausify (thm, lits) ls = + (case (Thm.prop_of thm, lits) of + (@{const HOL.Trueprop} $ @{const HOL.False}, [(_, ct)]) => + let val thm = Thm.implies_intr ct thm + in (discharge thm unclausify_rule1 handle THM _ => discharge thm unclausify_rule2, ls) end + | _ => (thm, Ord_List.union lit_ord lits ls)) + +fun with_thms f tps = fold_map unclausify tps [] |>> f + +fun bad_premises () = raise Fail "bad number of premises" +fun with_thms1 f = with_thms (fn [thm] => f thm | _ => bad_premises ()) +fun with_thms2 f = with_thms (fn [thm1, thm2] => f thm1 thm2 | _ => bad_premises ()) +fun with_thms3 f = with_thms (fn [thm1, thm2, thm3] => f thm1 thm2 thm3 | _ => bad_premises ()) + +fun replay_rule (ctxt, cons, facts) prems rule = + (case rule of + Argo_Proof.Axiom i => (nth facts i, []) + | Argo_Proof.Taut (k, concl) => (replay_taut ctxt k (cprop_of ctxt cons concl), []) + | Argo_Proof.Conjunct (i, n) => with_thms1 (replay_conjunct i n) prems + | Argo_Proof.Rewrite c => with_thms1 (replay_rewrite ctxt c) prems + | Argo_Proof.Clause is => replay_clause is (fst (hd prems)) + | Argo_Proof.Unit_Res i => replay_unit_res i (hd prems) (hd (tl prems)) + | Argo_Proof.Hyp (i, concl) => replay_hyp i (cprop_of ctxt cons concl) + | Argo_Proof.Lemma is => replay_lemma is (hd prems) + | Argo_Proof.Refl concl => (replay_refl (cterm_of ctxt cons concl), []) + | Argo_Proof.Symm => with_thms1 replay_symm prems + | Argo_Proof.Trans => with_thms2 replay_trans prems + | Argo_Proof.Cong => with_thms2 replay_cong prems + | Argo_Proof.Subst => with_thms3 replay_subst prems + | _ => with_thms (ext_replay (cprop_of ctxt cons) ctxt rule) prems) + +fun with_cache f proof thm_cache = + (case Thm_Cache.lookup thm_cache (Argo_Proof.id_of proof) of + SOME thm => (thm, thm_cache) + | NONE => + let val (thm, thm_cache') = f proof thm_cache + in (thm, Thm_Cache.update (Argo_Proof.id_of proof, thm) thm_cache') end) + +fun trace_step ctxt proof_id rule proofs = with_full_tracing ctxt (fn ctxt' => + let + val id = Argo_Proof.string_of_proof_id proof_id + val ids = map (Argo_Proof.string_of_proof_id o Argo_Proof.id_of) proofs + val rule_string = Argo_Proof.string_of_rule rule + in full_tracing ctxt' (" " ^ id ^ " <- " ^ space_implode " " ids ^ " . " ^ rule_string) end) + +fun replay_bottom_up (env as (ctxt, _, _)) proof thm_cache = + let + val (proof_id, rule, proofs) = Argo_Proof.dest proof + val (prems, thm_cache) = fold_map (with_cache (replay_bottom_up env)) proofs thm_cache + val _ = trace_step ctxt proof_id rule proofs + in (replay_rule env prems rule, thm_cache) end + +fun replay_proof env proof = with_cache (replay_bottom_up env) proof Thm_Cache.empty + +fun replay ctxt terms facts proof = + let + val env = (ctxt, Termtab.fold (Contab.update o swap) terms Contab.empty, facts) + val _ = tracing ctxt "replaying the proof" + val ({elapsed=t, ...}, ((thm, _), _)) = Timing.timing (replay_proof env) proof + val _ = tracing ctxt ("replayed the proof in " ^ string_of_int (Time.toMilliseconds t) ^ " ms") + in thm end + + +(* normalizing goals *) + +fun instantiate_elim_rule thm = + let val ct = Drule.strip_imp_concl (Thm.cprop_of thm) + in + (case Thm.term_of ct of + @{const HOL.Trueprop} $ Var (_, @{typ HOL.bool}) => + instantiate (Thm.dest_arg ct) @{cterm HOL.False} thm + | Var _ => instantiate ct @{cprop HOL.False} thm + | _ => thm) + end + +fun atomize_conv ctxt ct = + (case Thm.term_of ct of + @{const HOL.Trueprop} $ _ => Conv.all_conv + | @{const Pure.imp} $ _ $ _ => + Conv.binop_conv (atomize_conv ctxt) then_conv + Conv.rewr_conv @{thm atomize_imp} + | Const (@{const_name Pure.eq}, _) $ _ $ _ => + Conv.binop_conv (atomize_conv ctxt) then_conv + Conv.rewr_conv @{thm atomize_eq} + | Const (@{const_name Pure.all}, _) $ Abs _ => + Conv.binder_conv (atomize_conv o snd) ctxt then_conv + Conv.rewr_conv @{thm atomize_all} + | _ => Conv.all_conv) ct + +fun normalize ctxt thm = + thm + |> instantiate_elim_rule + |> Conv.fconv_rule (Thm.beta_conversion true then_conv Thm.eta_conversion) + |> Drule.forall_intr_vars + |> Conv.fconv_rule (atomize_conv ctxt) + + +(* prover, tactic and method *) + +datatype result = Satisfiable of term -> bool option | Unsatisfiable + +fun check props ctxt = + (case solve props ctxt of + (Proof _, ctxt') => (Unsatisfiable, ctxt') + | (Model model, ctxt') => (Satisfiable model, ctxt')) + +fun prove thms ctxt = + let val thms' = map (normalize ctxt) thms + in + (case solve (map Thm.prop_of thms') ctxt of + (Model _, ctxt') => (NONE, ctxt') + | (Proof (terms, proof), ctxt') => (SOME (replay ctxt' terms thms' proof), ctxt')) + end + +fun argo_tac ctxt thms = + CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 + (Conv.try_conv (Conv.rewr_conv @{thm atomize_eq})))) ctxt) + THEN' Tactic.resolve_tac ctxt [@{thm ccontr}] + THEN' Subgoal.FOCUS (fn {context, prems, ...} => + (case with_timeout context (prove (thms @ prems)) context of + (SOME thm, _) => Tactic.resolve_tac context [thm] 1 + | (NONE, _) => Tactical.no_tac)) ctxt + +val _ = + Theory.setup (Method.setup @{binding argo} + (Scan.optional Attrib.thms [] >> + (fn thms => fn ctxt => METHOD (fn facts => + HEADGOAL (argo_tac ctxt (thms @ facts))))) + "Applies the Argo prover") + +end diff -r f77dca1abf1b -r 3daf02070be5 src/HOL/ex/Argo_Examples.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/Argo_Examples.thy Thu Sep 29 20:54:44 2016 +0200 @@ -0,0 +1,1328 @@ +(* Title: HOL/ex/Argo_Examples.thy + Author: Sascha Boehme +*) + +section \Argo\ + +theory Argo_Examples +imports Complex_Main +begin + +text \ + This theory is intended to showcase and test different features of the \argo\ proof method. + + The \argo\ proof method can be applied to propositional problems, problems involving equality + reasoning and problems of linear real arithmetic. + + The \argo\ proof method provides two options. To specify an upper limit of the proof methods + run time in seconds, use the option \argo_timeout\. To specify the amount of output, use the + option \argo_trace\ with value \none\ for no tracing output, value \basic\ for viewing the + underlying propositions and some timings, and value \full\ for additionally inspecting the + proof replay steps. +\ + +declare[[argo_trace = full]] + +subsection \Propositional logic\ + +notepad +begin + have "True" by argo +next + have "~False" by argo +next + fix P :: bool + assume "False" + then have "P" by argo +next + fix P :: bool + assume "~True" + then have "P" by argo +next + fix P :: bool + assume "P" + then have "P" by argo +next + fix P :: bool + assume "~~P" + then have "P" by argo +next + fix P Q R :: bool + assume "P & Q & R" + then have "R & P & Q" by argo +next + fix P Q R :: bool + assume "P & (Q & True & R) & (Q & P) & True" + then have "R & P & Q" by argo +next + fix P Q1 Q2 Q3 Q4 Q5 :: bool + assume "Q1 & (Q2 & P & Q3) & (Q4 & ~P & Q5)" + then have "~True" by argo +next + fix P Q1 Q2 Q3 :: bool + assume "(Q1 & False) & Q2 & Q3" + then have "P::bool" by argo +next + fix P Q R :: bool + assume "P | Q | R" + then have "R | P | Q" by argo +next + fix P Q R :: bool + assume "P | (Q | False | R) | (Q | P) | False" + then have "R | P | Q" by argo +next + fix P Q1 Q2 Q3 Q4 :: bool + have "(Q1 & P & Q2) --> False | (Q3 | (Q4 | P) | False)" by argo +next + fix Q1 Q2 Q3 Q4 :: bool + have "Q1 | (Q2 | True | Q3) | Q4" by argo +next + fix P Q R :: bool + assume "(P & Q) | (P & ~Q) | (P & R) | (P & ~R)" + then have "P" by argo +next + fix P :: bool + assume "P = True" + then have "P" by argo +next + fix P :: bool + assume "False = P" + then have "~P" by argo +next + fix P Q :: bool + assume "P = (~P)" + then have "Q" by argo +next + fix P :: bool + have "(~P) = (~P)" by argo +next + fix P Q :: bool + assume "P" and "~Q" + then have "P = (~Q)" by argo +next + fix P Q :: bool + assume "((P::bool) = Q) | (Q = P)" + then have "(P --> Q) & (Q --> P)" by argo +next + fix P Q :: bool + assume "(P::bool) = Q" + then have "Q = P" by argo +next + fix P Q R :: bool + assume "if P then Q else R" + then have "Q | R" by argo +next + fix P Q :: bool + assume "P | Q" + and "P | ~Q" + and "~P | Q" + and "~P | ~Q" + then have "False" by argo +next + fix P Q R :: bool + assume "P | Q | R" + and "P | Q | ~R" + and "P | ~Q | R" + and "P | ~Q | ~R" + and "~P | Q | R" + and "~P | Q | ~R" + and "~P | ~Q | R" + and "~P | ~Q | ~R" + then have "False" by argo +next + fix a b c d e f g h i j k l m n p q :: bool + assume "(a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)" + then have "(a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)" by argo +next + fix P :: bool + have "P=P=P=P=P=P=P=P=P=P" by argo +next + fix a b c d e f p q x :: bool + assume "a | b | c | d" + and "e | f | (a & d)" + and "~(a | (c & ~c)) | b" + and "~(b & (x | ~x)) | c" + and "~(d | False) | c" + and "~(c | (~p & (p | (q & ~q))))" + then have "False" by argo +end + + +subsection \Equality, congruence and predicates\ + +notepad +begin + fix t :: "'a" + have "t = t" by argo +next + fix t u :: "'a" + assume "t = u" + then have "u = t" by argo +next + fix s t u :: "'a" + assume "s = t" and "t = u" + then have "s = u" by argo +next + fix s t u v :: "'a" + assume "s = t" and "t = u" and "u = v" and "u = s" + then have "s = v" by argo +next + fix s t u v w :: "'a" + assume "s = t" and "t = u" and "s = v" and "v = w" + then have "w = u" by argo +next + fix s t u a b c :: "'a" + assume "s = t" and "t = u" and "a = b" and "b = c" + then have "s = a --> c = u" by argo +next + fix a b c d :: "'a" + assume "(a = b & b = c) | (a = d & d = c)" + then have "a = c" by argo +next + fix a b1 b2 b3 b4 c d :: "'a" + assume "(a = b1 & ((b1 = b2 & b2 = b3) | (b1 = b4 & b4 = b3)) & b3 = c) | (a = d & d = c)" + then have "a = c" by argo +next + fix a b :: "'a" + have "(if True then a else b) = a" by argo +next + fix a b :: "'a" + have "(if False then a else b) = b" by argo +next + fix a b :: "'a" + have "(if \True then a else b) = b" by argo +next + fix a b :: "'a" + have "(if \False then a else b) = a" by argo +next + fix P :: "bool" + fix a :: "'a" + have "(if P then a else a) = a" by argo +next + fix P :: "bool" + fix a b c :: "'a" + assume "P" and "a = c" + then have "(if P then a else b) = c" by argo +next + fix P :: "bool" + fix a b c :: "'a" + assume "~P" and "b = c" + then have "(if P then a else b) = c" by argo +next + fix P Q :: "bool" + fix a b c d :: "'a" + assume "P" and "Q" and "a = d" + then have "(if P then (if Q then a else b) else c) = d" by argo +next + fix a b c :: "'a" + assume "a \ b" and "b = c" + then have "a \ c" by argo +next + fix a b c :: "'a" + assume "a \ b" and "a = c" + then have "c \ b" by argo +next + fix a b c d :: "'a" + assume "a = b" and "c = d" and "b \ d" + then have "a \ c" by argo +next + fix a b c d :: "'a" + assume "a = b" and "c = d" and "d \ b" + then have "a \ c" by argo +next + fix a b c d :: "'a" + assume "a = b" and "c = d" and "b \ d" + then have "c \ a" by argo +next + fix a b c d :: "'a" + assume "a = b" and "c = d" and "d \ b" + then have "c \ a" by argo +next + fix a b c d e f :: "'a" + assume "a \ b" and "b = c" and "b = d" and "d = e" and "a = f" + then have "f \ e" by argo +next + fix a b :: "'a" and f :: "'a \ 'a" + assume "a = b" + then have "f a = f b" by argo +next + fix a b c :: "'a" and f :: "'a \ 'a" + assume "f a = f b" and "b = c" + then have "f a = f c" by argo +next + fix a :: "'a" and f :: "'a \ 'a" + assume "f a = a" + then have "f (f a) = a" by argo +next + fix a b :: "'a" and f g :: "'a \ 'a" + assume "a = b" + then have "g (f a) = g (f b)" by argo +next + fix a b :: "'a" and f g :: "'a \ 'a" + assume "f a = b" and "g b = a" + then have "f (g (f a)) = b" by argo +next + fix a b :: "'a" and g :: "'a \ 'a \ 'a" + assume "a = b" + then have "g a b = g b a" by argo +next + fix a b :: "'a" and f :: "'a \ 'a" and g :: "'a \ 'a \ 'a" + assume "f a = b" + then have "g (f a) b = g b (f a)" by argo +next + fix a b c d e g h :: "'a" and f :: "'a \ 'a \ 'a" + assume "c = d" and "e = c" and "e = b" and "b = h" and "f g h = d" and "f g d = a" + then have "a = b" by argo +next + fix a b :: "'a" and P :: "'a \ bool" + assume "P a" and "a = b" + then have "P b" by argo +next + fix a b :: "'a" and P :: "'a \ bool" + assume "~ P a" and "a = b" + then have "~ P b" by argo +next + fix a b c d :: "'a" and P :: "'a \ 'a \ bool" + assume "P a b" and "a = c" and "b = d" + then have "P c d" by argo +next + fix a b c d :: "'a" and P :: "'a \ 'a \ bool" + assume "~ P a b" and "a = c" and "b = d" + then have "~ P c d" by argo +end + + +subsection \Linear real arithmetic\ + +subsubsection \Negation and subtraction\ + +notepad +begin + fix a b :: real + have + "-a = -1 * a" + "-(-a) = a" + "a - b = a + -1 * b" + "a - (-b) = a + b" + by argo+ +end + + +subsubsection \Multiplication\ + +notepad +begin + fix a b c d :: real + have + "(2::real) * 3 = 6" + "0 * a = 0" + "a * 0 = 0" + "1 * a = a" + "a * 1 = a" + "2 * a = a * 2" + "2 * a * 3 = 6 * a" + "2 * a * 3 * 5 = 30 * a" + "a * 0 * b = 0" + "a * (0 * b) = 0" + "a * (b * c) = (a * b) * c" + "a * (b * (c * d)) = ((a * b) * c) * d" + "a * (b + c + d) = a * b + a * c + a * d" + by argo+ +end + + +subsubsection \Division\ + +notepad +begin + fix a b c :: real + have + "(6::real) / 2 = 3" + "a / 0 = a / 0" + "a / 0 <= a / 0" + "~(a / 0 < a / 0)" + "0 / a = 0" + "a / 1 = a" + "a / 3 = 1/3 * a" + "6 * a / 2 = 3 * a" + "a / ((5 * b) / 2) = 2/5 * a / b" + "a / (5 * (b / 2)) = 2/5 * a / b" + "(a / 5) * (b / 2) = 1/10 * a * b" + "a / (3 * b) = 1/3 * a / b" + "(a + b) / 5 = 1/5 * a + 1/5 * b" + "a / (5 * 1/5) = a" + by argo+ +end + + +subsubsection \Addition\ + +notepad +begin + fix a b c d :: real + have + "a + b = b + a" + "a + b + c = c + b + a" + "a + b + c + d = d + c + b + a" + "a + (b + (c + d)) = ((a + b) + c) + d" + "(5::real) + -3 = 2" + "(3::real) + 5 + -1 = 7" + "2 + a = a + 2" + "a + b + a = b + 2 * a" + "-1 + a + -1 + 2 + b + 5/3 + b + 1/3 + 5 * b + 2/3 = 8/3 + a + 7 * b" + "1 + b + b + 5 * b + 3 * a + 7 + a + 2 = 10 + 4 * a + 7 * b" + by argo+ +end + + +subsubsection \Minimum and maximum\ + +notepad +begin + fix a b :: real + have + "min (3::real) 5 = 3" + "min (5::real) 3 = 3" + "min (3::real) (-5) = -5" + "min (-5::real) 3 = -5" + "min a a = a" + "a \ b \ min a b = a" + "a > b \ min a b = b" + "min a b \ a" + "min a b \ b" + "min a b = min b a" + by argo+ +next + fix a b :: real + have + "max (3::real) 5 = 5" + "max (5::real) 3 = 5" + "max (3::real) (-5) = 3" + "max (-5::real) 3 = 3" + "max a a = a" + "a \ b \ max a b = b" + "a > b \ max a b = a" + "a \ max a b" + "b \ max a b" + "max a b = max b a" + by argo+ +next + fix a b :: real + have + "min a b \ max a b" + "min a b + max a b = a + b" + "a < b \ min a b < max a b" + by argo+ +end + + +subsubsection \Absolute value\ + +notepad +begin + fix a :: real + have + "abs (3::real) = 3" + "abs (-3::real) = 3" + "0 \ abs a" + "a \ abs a" + "a \ 0 \ abs a = a" + "a < 0 \ abs a = -a" + "abs (abs a) = abs a" + by argo+ +end + + +subsubsection \Equality\ + +notepad +begin + fix a b c d :: real + have + "(3::real) = 3" + "~((3::real) = 4)" + "~((4::real) = 3)" + "3 * a = 5 --> a = 5/3" + "-3 * a = 5 --> -5/3 = a" + "5 = 3 * a --> 5/3 = a " + "5 = -3 * a --> a = -5/3" + "2 + 3 * a = 4 --> a = 2/3" + "4 = 2 + 3 * a --> 2/3 = a" + "2 + 3 * a + 5 * b + c = 4 --> 3 * a + 5 * b + c = 2" + "4 = 2 + 3 * a + 5 * b + c --> 2 = 3 * a + 5 * b + c" + "-2 * a + b + -3 * c = 7 --> -7 = 2 * a + -1 * b + 3 * c" + "7 = -2 * a + b + -3 * c --> 2 * a + -1 * b + 3 * c = -7" + "-2 * a + b + -3 * c + 4 * d = 7 --> -7 = 2 * a + -1 * b + 3 * c + -4 * d" + "7 = -2 * a + b + -3 * c + 4 * d --> 2 * a + -1 * b + 3 * c + -4 * d = -7" + "a + 3 * b = 5 * c + b --> a + 2 * b + -5 * c = 0" + by argo+ +end + + +subsubsection \Less-equal\ + +notepad +begin + fix a b c d :: real + have + "(3::real) <= 3" + "(3::real) <= 4" + "~((4::real) <= 3)" + "3 * a <= 5 --> a <= 5/3" + "-3 * a <= 5 --> -5/3 <= a" + "5 <= 3 * a --> 5/3 <= a " + "5 <= -3 * a --> a <= -5/3" + "2 + 3 * a <= 4 --> a <= 2/3" + "4 <= 2 + 3 * a --> 2/3 <= a" + "2 + 3 * a + 5 * b + c <= 4 --> 3 * a + 5 * b + c <= 2" + "4 <= 2 + 3 * a + 5 * b + c --> 2 <= 3 * a + 5 * b + c" + "-2 * a + b + -3 * c <= 7 --> -7 <= 2 * a + -1 * b + 3 * c" + "7 <= -2 * a + b + -3 * c --> 2 * a + -1 * b + 3 * c <= -7" + "-2 * a + b + -3 * c + 4 * d <= 7 --> -7 <= 2 * a + -1 * b + 3 * c + -4 * d" + "7 <= -2 * a + b + -3 * c + 4 * d --> 2 * a + -1 * b + 3 * c + -4 * d <= -7" + "a + 3 * b <= 5 * c + b --> a + 2 * b + -5 * c <= 0" + by argo+ +end + +subsubsection \Less\ + +notepad +begin + fix a b c d :: real + have + "(3::real) < 4" + "~((3::real) < 3)" + "~((4::real) < 3)" + "3 * a < 5 --> a < 5/3" + "-3 * a < 5 --> -5/3 < a" + "5 < 3 * a --> 5/3 < a " + "5 < -3 * a --> a < -5/3" + "2 + 3 * a < 4 --> a < 2/3" + "4 < 2 + 3 * a --> 2/3 < a" + "2 + 3 * a + 5 * b + c < 4 --> 3 * a + 5 * b + c < 2" + "4 < 2 + 3 * a + 5 * b + c --> 2 < 3 * a + 5 * b + c" + "-2 * a + b + -3 * c < 7 --> -7 < 2 * a + -1 * b + 3 * c" + "7 < -2 * a + b + -3 * c --> 2 * a + -1 * b + 3 * c < -7" + "-2 * a + b + -3 * c + 4 * d < 7 --> -7 < 2 * a + -1 * b + 3 * c + -4 * d" + "7 < -2 * a + b + -3 * c + 4 * d --> 2 * a + -1 * b + 3 * c + -4 * d < -7" + "a + 3 * b < 5 * c + b --> a + 2 * b + -5 * c < 0" + by argo+ +end + + +subsubsection \Other examples\ + +notepad +begin + have + "(0::real) < 1" + "(47::real) + 11 < 8 * 15" + by argo+ +next + fix a :: real + assume "a < 3" + then have "a < 5" "a <= 5" "~(5 < a)" "~(5 <= a)" by argo+ +next + fix a :: real + assume "a <= 3" + then have "a < 5" "a <= 5" "~(5 < a)" "~(5 <= a)" by argo+ +next + fix a :: real + assume "~(3 < a)" + then have "a < 5" "a <= 5" "~(5 < a)" "~(5 <= a)" by argo+ +next + fix a :: real + assume "~(3 <= a)" + then have "a < 5" "a <= 5" "~(5 < a)" "~(5 <= a)" by argo+ +next + fix a :: real + have "a < 3 | a = 3 | a > 3" by argo +next + fix a b :: real + assume "0 < a" and "a < b" + then have "0 < b" by argo +next + fix a b :: real + assume "0 < a" and "a \ b" + then have "0 \ b" by argo +next + fix a b :: real + assume "0 \ a" and "a < b" + then have "0 \ b" by argo +next + fix a b :: real + assume "0 \ a" and "a \ b" + then have "0 \ b" by argo +next + fix a b c :: real + assume "2 \ a" and "3 \ b" and "c \ 5" + then have "-2 * a + -3 * b + 5 * c < 13" by argo +next + fix a b c :: real + assume "2 \ a" and "3 \ b" and "c \ 5" + then have "-2 * a + -3 * b + 5 * c \ 12" by argo +next + fix a b :: real + assume "a = 2" and "b = 3" + then have "a + b > 5 \ a < b" by argo +next + fix a b c :: real + assume "5 0" + then have "b > 0" by argo +next + fix a b c :: real + assume "a + b < 7" and "5 0" + then have "0 b" + then have "b < a" by argo +next + fix a b :: real + have "(a - b) - a = (a - a) - b" by argo +next + fix n m n' m' :: real + have " + (n < m & m < n') | (n < m & m = n') | (n < n' & n' < m) | + (n = n' & n' < m) | (n = m & m < n') | + (n' < m & m < n) | (n' < m & m = n) | + (n' < n & n < m) | (n' = n & n < m) | (n' = m & m < n) | + (m < n & n < n') | (m < n & n' = n) | (m < n' & n' < n) | + (m = n & n < n') | (m = n' & n' < n) | + (n' = m & m = n)" + by argo +end + + +subsection \Larger examples\ + +declare[[argo_trace = basic, argo_timeout = 60]] + + +text \Translated from TPTP problem library: PUZ015-2.006.dimacs\ + +lemma assumes 1: "~x0" + and 2: "~x30" + and 3: "~x29" + and 4: "~x59" + and 5: "x1 | x31 | x0" + and 6: "x2 | x32 | x1" + and 7: "x3 | x33 | x2" + and 8: "x4 | x34 | x3" + and 9: "x35 | x4" + and 10: "x5 | x36 | x30" + and 11: "x6 | x37 | x5 | x31" + and 12: "x7 | x38 | x6 | x32" + and 13: "x8 | x39 | x7 | x33" + and 14: "x9 | x40 | x8 | x34" + and 15: "x41 | x9 | x35" + and 16: "x10 | x42 | x36" + and 17: "x11 | x43 | x10 | x37" + and 18: "x12 | x44 | x11 | x38" + and 19: "x13 | x45 | x12 | x39" + and 20: "x14 | x46 | x13 | x40" + and 21: "x47 | x14 | x41" + and 22: "x15 | x48 | x42" + and 23: "x16 | x49 | x15 | x43" + and 24: "x17 | x50 | x16 | x44" + and 25: "x18 | x51 | x17 | x45" + and 26: "x19 | x52 | x18 | x46" + and 27: "x53 | x19 | x47" + and 28: "x20 | x54 | x48" + and 29: "x21 | x55 | x20 | x49" + and 30: "x22 | x56 | x21 | x50" + and 31: "x23 | x57 | x22 | x51" + and 32: "x24 | x58 | x23 | x52" + and 33: "x59 | x24 | x53" + and 34: "x25 | x54" + and 35: "x26 | x25 | x55" + and 36: "x27 | x26 | x56" + and 37: "x28 | x27 | x57" + and 38: "x29 | x28 | x58" + and 39: "~x1 | ~x31" + and 40: "~x1 | ~x0" + and 41: "~x31 | ~x0" + and 42: "~x2 | ~x32" + and 43: "~x2 | ~x1" + and 44: "~x32 | ~x1" + and 45: "~x3 | ~x33" + and 46: "~x3 | ~x2" + and 47: "~x33 | ~x2" + and 48: "~x4 | ~x34" + and 49: "~x4 | ~x3" + and 50: "~x34 | ~x3" + and 51: "~x35 | ~x4" + and 52: "~x5 | ~x36" + and 53: "~x5 | ~x30" + and 54: "~x36 | ~x30" + and 55: "~x6 | ~x37" + and 56: "~x6 | ~x5" + and 57: "~x6 | ~x31" + and 58: "~x37 | ~x5" + and 59: "~x37 | ~x31" + and 60: "~x5 | ~x31" + and 61: "~x7 | ~x38" + and 62: "~x7 | ~x6" + and 63: "~x7 | ~x32" + and 64: "~x38 | ~x6" + and 65: "~x38 | ~x32" + and 66: "~x6 | ~x32" + and 67: "~x8 | ~x39" + and 68: "~x8 | ~x7" + and 69: "~x8 | ~x33" + and 70: "~x39 | ~x7" + and 71: "~x39 | ~x33" + and 72: "~x7 | ~x33" + and 73: "~x9 | ~x40" + and 74: "~x9 | ~x8" + and 75: "~x9 | ~x34" + and 76: "~x40 | ~x8" + and 77: "~x40 | ~x34" + and 78: "~x8 | ~x34" + and 79: "~x41 | ~x9" + and 80: "~x41 | ~x35" + and 81: "~x9 | ~x35" + and 82: "~x10 | ~x42" + and 83: "~x10 | ~x36" + and 84: "~x42 | ~x36" + and 85: "~x11 | ~x43" + and 86: "~x11 | ~x10" + and 87: "~x11 | ~x37" + and 88: "~x43 | ~x10" + and 89: "~x43 | ~x37" + and 90: "~x10 | ~x37" + and 91: "~x12 | ~x44" + and 92: "~x12 | ~x11" + and 93: "~x12 | ~x38" + and 94: "~x44 | ~x11" + and 95: "~x44 | ~x38" + and 96: "~x11 | ~x38" + and 97: "~x13 | ~x45" + and 98: "~x13 | ~x12" + and 99: "~x13 | ~x39" + and 100: "~x45 | ~x12" + and 101: "~x45 | ~x39" + and 102: "~x12 | ~x39" + and 103: "~x14 | ~x46" + and 104: "~x14 | ~x13" + and 105: "~x14 | ~x40" + and 106: "~x46 | ~x13" + and 107: "~x46 | ~x40" + and 108: "~x13 | ~x40" + and 109: "~x47 | ~x14" + and 110: "~x47 | ~x41" + and 111: "~x14 | ~x41" + and 112: "~x15 | ~x48" + and 113: "~x15 | ~x42" + and 114: "~x48 | ~x42" + and 115: "~x16 | ~x49" + and 116: "~x16 | ~x15" + and 117: "~x16 | ~x43" + and 118: "~x49 | ~x15" + and 119: "~x49 | ~x43" + and 120: "~x15 | ~x43" + and 121: "~x17 | ~x50" + and 122: "~x17 | ~x16" + and 123: "~x17 | ~x44" + and 124: "~x50 | ~x16" + and 125: "~x50 | ~x44" + and 126: "~x16 | ~x44" + and 127: "~x18 | ~x51" + and 128: "~x18 | ~x17" + and 129: "~x18 | ~x45" + and 130: "~x51 | ~x17" + and 131: "~x51 | ~x45" + and 132: "~x17 | ~x45" + and 133: "~x19 | ~x52" + and 134: "~x19 | ~x18" + and 135: "~x19 | ~x46" + and 136: "~x52 | ~x18" + and 137: "~x52 | ~x46" + and 138: "~x18 | ~x46" + and 139: "~x53 | ~x19" + and 140: "~x53 | ~x47" + and 141: "~x19 | ~x47" + and 142: "~x20 | ~x54" + and 143: "~x20 | ~x48" + and 144: "~x54 | ~x48" + and 145: "~x21 | ~x55" + and 146: "~x21 | ~x20" + and 147: "~x21 | ~x49" + and 148: "~x55 | ~x20" + and 149: "~x55 | ~x49" + and 150: "~x20 | ~x49" + and 151: "~x22 | ~x56" + and 152: "~x22 | ~x21" + and 153: "~x22 | ~x50" + and 154: "~x56 | ~x21" + and 155: "~x56 | ~x50" + and 156: "~x21 | ~x50" + and 157: "~x23 | ~x57" + and 158: "~x23 | ~x22" + and 159: "~x23 | ~x51" + and 160: "~x57 | ~x22" + and 161: "~x57 | ~x51" + and 162: "~x22 | ~x51" + and 163: "~x24 | ~x58" + and 164: "~x24 | ~x23" + and 165: "~x24 | ~x52" + and 166: "~x58 | ~x23" + and 167: "~x58 | ~x52" + and 168: "~x23 | ~x52" + and 169: "~x59 | ~x24" + and 170: "~x59 | ~x53" + and 171: "~x24 | ~x53" + and 172: "~x25 | ~x54" + and 173: "~x26 | ~x25" + and 174: "~x26 | ~x55" + and 175: "~x25 | ~x55" + and 176: "~x27 | ~x26" + and 177: "~x27 | ~x56" + and 178: "~x26 | ~x56" + and 179: "~x28 | ~x27" + and 180: "~x28 | ~x57" + and 181: "~x27 | ~x57" + and 182: "~x29 | ~x28" + and 183: "~x29 | ~x58" + and 184: "~x28 | ~x58" + shows "False" + using assms + by argo + + +text \Translated from TPTP problem library: MSC007-1.008.dimacs\ + +lemma assumes 1: "x0 | x1 | x2 | x3 | x4 | x5 | x6" + and 2: "x7 | x8 | x9 | x10 | x11 | x12 | x13" + and 3: "x14 | x15 | x16 | x17 | x18 | x19 | x20" + and 4: "x21 | x22 | x23 | x24 | x25 | x26 | x27" + and 5: "x28 | x29 | x30 | x31 | x32 | x33 | x34" + and 6: "x35 | x36 | x37 | x38 | x39 | x40 | x41" + and 7: "x42 | x43 | x44 | x45 | x46 | x47 | x48" + and 8: "x49 | x50 | x51 | x52 | x53 | x54 | x55" + and 9: "~x0 | ~x7" + and 10: "~x0 | ~x14" + and 11: "~x0 | ~x21" + and 12: "~x0 | ~x28" + and 13: "~x0 | ~x35" + and 14: "~x0 | ~x42" + and 15: "~x0 | ~x49" + and 16: "~x7 | ~x14" + and 17: "~x7 | ~x21" + and 18: "~x7 | ~x28" + and 19: "~x7 | ~x35" + and 20: "~x7 | ~x42" + and 21: "~x7 | ~x49" + and 22: "~x14 | ~x21" + and 23: "~x14 | ~x28" + and 24: "~x14 | ~x35" + and 25: "~x14 | ~x42" + and 26: "~x14 | ~x49" + and 27: "~x21 | ~x28" + and 28: "~x21 | ~x35" + and 29: "~x21 | ~x42" + and 30: "~x21 | ~x49" + and 31: "~x28 | ~x35" + and 32: "~x28 | ~x42" + and 33: "~x28 | ~x49" + and 34: "~x35 | ~x42" + and 35: "~x35 | ~x49" + and 36: "~x42 | ~x49" + and 37: "~x1 | ~x8" + and 38: "~x1 | ~x15" + and 39: "~x1 | ~x22" + and 40: "~x1 | ~x29" + and 41: "~x1 | ~x36" + and 42: "~x1 | ~x43" + and 43: "~x1 | ~x50" + and 44: "~x8 | ~x15" + and 45: "~x8 | ~x22" + and 46: "~x8 | ~x29" + and 47: "~x8 | ~x36" + and 48: "~x8 | ~x43" + and 49: "~x8 | ~x50" + and 50: "~x15 | ~x22" + and 51: "~x15 | ~x29" + and 52: "~x15 | ~x36" + and 53: "~x15 | ~x43" + and 54: "~x15 | ~x50" + and 55: "~x22 | ~x29" + and 56: "~x22 | ~x36" + and 57: "~x22 | ~x43" + and 58: "~x22 | ~x50" + and 59: "~x29 | ~x36" + and 60: "~x29 | ~x43" + and 61: "~x29 | ~x50" + and 62: "~x36 | ~x43" + and 63: "~x36 | ~x50" + and 64: "~x43 | ~x50" + and 65: "~x2 | ~x9" + and 66: "~x2 | ~x16" + and 67: "~x2 | ~x23" + and 68: "~x2 | ~x30" + and 69: "~x2 | ~x37" + and 70: "~x2 | ~x44" + and 71: "~x2 | ~x51" + and 72: "~x9 | ~x16" + and 73: "~x9 | ~x23" + and 74: "~x9 | ~x30" + and 75: "~x9 | ~x37" + and 76: "~x9 | ~x44" + and 77: "~x9 | ~x51" + and 78: "~x16 | ~x23" + and 79: "~x16 | ~x30" + and 80: "~x16 | ~x37" + and 81: "~x16 | ~x44" + and 82: "~x16 | ~x51" + and 83: "~x23 | ~x30" + and 84: "~x23 | ~x37" + and 85: "~x23 | ~x44" + and 86: "~x23 | ~x51" + and 87: "~x30 | ~x37" + and 88: "~x30 | ~x44" + and 89: "~x30 | ~x51" + and 90: "~x37 | ~x44" + and 91: "~x37 | ~x51" + and 92: "~x44 | ~x51" + and 93: "~x3 | ~x10" + and 94: "~x3 | ~x17" + and 95: "~x3 | ~x24" + and 96: "~x3 | ~x31" + and 97: "~x3 | ~x38" + and 98: "~x3 | ~x45" + and 99: "~x3 | ~x52" + and 100: "~x10 | ~x17" + and 101: "~x10 | ~x24" + and 102: "~x10 | ~x31" + and 103: "~x10 | ~x38" + and 104: "~x10 | ~x45" + and 105: "~x10 | ~x52" + and 106: "~x17 | ~x24" + and 107: "~x17 | ~x31" + and 108: "~x17 | ~x38" + and 109: "~x17 | ~x45" + and 110: "~x17 | ~x52" + and 111: "~x24 | ~x31" + and 112: "~x24 | ~x38" + and 113: "~x24 | ~x45" + and 114: "~x24 | ~x52" + and 115: "~x31 | ~x38" + and 116: "~x31 | ~x45" + and 117: "~x31 | ~x52" + and 118: "~x38 | ~x45" + and 119: "~x38 | ~x52" + and 120: "~x45 | ~x52" + and 121: "~x4 | ~x11" + and 122: "~x4 | ~x18" + and 123: "~x4 | ~x25" + and 124: "~x4 | ~x32" + and 125: "~x4 | ~x39" + and 126: "~x4 | ~x46" + and 127: "~x4 | ~x53" + and 128: "~x11 | ~x18" + and 129: "~x11 | ~x25" + and 130: "~x11 | ~x32" + and 131: "~x11 | ~x39" + and 132: "~x11 | ~x46" + and 133: "~x11 | ~x53" + and 134: "~x18 | ~x25" + and 135: "~x18 | ~x32" + and 136: "~x18 | ~x39" + and 137: "~x18 | ~x46" + and 138: "~x18 | ~x53" + and 139: "~x25 | ~x32" + and 140: "~x25 | ~x39" + and 141: "~x25 | ~x46" + and 142: "~x25 | ~x53" + and 143: "~x32 | ~x39" + and 144: "~x32 | ~x46" + and 145: "~x32 | ~x53" + and 146: "~x39 | ~x46" + and 147: "~x39 | ~x53" + and 148: "~x46 | ~x53" + and 149: "~x5 | ~x12" + and 150: "~x5 | ~x19" + and 151: "~x5 | ~x26" + and 152: "~x5 | ~x33" + and 153: "~x5 | ~x40" + and 154: "~x5 | ~x47" + and 155: "~x5 | ~x54" + and 156: "~x12 | ~x19" + and 157: "~x12 | ~x26" + and 158: "~x12 | ~x33" + and 159: "~x12 | ~x40" + and 160: "~x12 | ~x47" + and 161: "~x12 | ~x54" + and 162: "~x19 | ~x26" + and 163: "~x19 | ~x33" + and 164: "~x19 | ~x40" + and 165: "~x19 | ~x47" + and 166: "~x19 | ~x54" + and 167: "~x26 | ~x33" + and 168: "~x26 | ~x40" + and 169: "~x26 | ~x47" + and 170: "~x26 | ~x54" + and 171: "~x33 | ~x40" + and 172: "~x33 | ~x47" + and 173: "~x33 | ~x54" + and 174: "~x40 | ~x47" + and 175: "~x40 | ~x54" + and 176: "~x47 | ~x54" + and 177: "~x6 | ~x13" + and 178: "~x6 | ~x20" + and 179: "~x6 | ~x27" + and 180: "~x6 | ~x34" + and 181: "~x6 | ~x41" + and 182: "~x6 | ~x48" + and 183: "~x6 | ~x55" + and 184: "~x13 | ~x20" + and 185: "~x13 | ~x27" + and 186: "~x13 | ~x34" + and 187: "~x13 | ~x41" + and 188: "~x13 | ~x48" + and 189: "~x13 | ~x55" + and 190: "~x20 | ~x27" + and 191: "~x20 | ~x34" + and 192: "~x20 | ~x41" + and 193: "~x20 | ~x48" + and 194: "~x20 | ~x55" + and 195: "~x27 | ~x34" + and 196: "~x27 | ~x41" + and 197: "~x27 | ~x48" + and 198: "~x27 | ~x55" + and 199: "~x34 | ~x41" + and 200: "~x34 | ~x48" + and 201: "~x34 | ~x55" + and 202: "~x41 | ~x48" + and 203: "~x41 | ~x55" + and 204: "~x48 | ~x55" + shows "False" + using assms + by argo + + +lemma "0 \ (yc::real) \ + 0 \ yd \ 0 \ yb \ 0 \ ya \ + 0 \ yf \ + 0 \ xh \ 0 \ ye \ 0 \ yg \ + 0 \ yw \ 0 \ xs \ 0 \ yu \ + 0 \ aea \ 0 \ aee \ 0 \ aed \ + 0 \ zy \ 0 \ xz \ 0 \ zw \ + 0 \ zb \ + 0 \ za \ 0 \ yy \ 0 \ yz \ + 0 \ zp \ 0 \ zo \ 0 \ yq \ + 0 \ adp \ 0 \ aeb \ 0 \ aec \ + 0 \ acm \ 0 \ aco \ 0 \ acn \ + 0 \ abl \ + 0 \ zr \ 0 \ zq \ 0 \ abh \ + 0 \ abq \ 0 \ zd \ 0 \ abo \ + 0 \ acd \ + 0 \ acc \ 0 \ xi \ 0 \ acb \ + 0 \ acp \ 0 \ acr \ 0 \ acq \ + 0 \ xw \ + 0 \ xr \ 0 \ xv \ 0 \ xu \ + 0 \ zc \ 0 \ acg \ 0 \ ach \ + 0 \ zt \ 0 \ zs \ 0 \ xy \ + 0 \ ady \ 0 \ adw \ 0 \ zg \ + 0 \ abd \ + 0 \ abc \ 0 \ yr \ 0 \ abb \ + 0 \ adi \ + 0 \ x \ 0 \ adh \ 0 \ xa \ + 0 \ aak \ 0 \ aai \ 0 \ aad \ + 0 \ aba \ 0 \ zh \ 0 \ aay \ + 0 \ abg \ 0 \ ys \ 0 \ abe \ + 0 \ abs1 \ + 0 \ yt \ 0 \ abr \ 0 \ zu \ + 0 \ abv \ + 0 \ zn \ 0 \ abw \ 0 \ zm \ + 0 \ adl \ 0 \ adn \ + 0 \ acf \ 0 \ aca \ + 0 \ ads \ 0 \ aaq \ + 0 \ ada \ + 0 \ aaf \ 0 \ aac \ 0 \ aag \ + 0 \ aal \ + 0 \ acu \ 0 \ acs \ 0 \ act \ + 0 \ aas \ 0 \ xb \ 0 \ aat \ + 0 \ zk \ 0 \ zj \ 0 \ zi \ + 0 \ ack \ + 0 \ acj \ 0 \ xc \ 0 \ aci \ + 0 \ aav \ 0 \ aah \ 0 \ xd \ + 0 \ abt \ + 0 \ xo \ 0 \ abu \ 0 \ xn \ + 0 \ adc \ + 0 \ abz \ 0 \ adc \ 0 \ abz \ + 0 \ xt \ + 0 \ zz \ 0 \ aab \ 0 \ aaa \ + 0 \ adq \ + 0 \ xl \ 0 \ adr \ 0 \ adb \ + 0 \ zf \ 0 \ yh \ 0 \ yi \ + 0 \ aao \ 0 \ aam \ 0 \ xe \ + 0 \ abk \ + 0 \ aby \ 0 \ abj \ 0 \ abx \ + 0 \ yp \ + 0 \ yl \ 0 \ yj \ 0 \