--- a/src/HOL/Tools/Argo/argo_tactic.ML Mon Jul 31 15:38:21 2017 +0100
+++ b/src/HOL/Tools/Argo/argo_tactic.ML Tue Aug 01 07:26:23 2017 +0200
@@ -474,7 +474,9 @@
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.Args_Conv (Argo_Expr.App, [c1, c2])) ct =
+ Conv.combination_conv (replay_conv ctxt c1) (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
--- a/src/HOL/ex/Argo_Examples.thy Mon Jul 31 15:38:21 2017 +0100
+++ b/src/HOL/ex/Argo_Examples.thy Tue Aug 01 07:26:23 2017 +0200
@@ -530,6 +530,9 @@
notepad
begin
+ fix a b :: real
+ have "f (a + b) = f (b + a)" by argo
+next
have
"(0::real) < 1"
"(47::real) + 11 < 8 * 15"
--- a/src/Tools/Argo/argo_expr.ML Mon Jul 31 15:38:21 2017 +0100
+++ b/src/Tools/Argo/argo_expr.ML Tue Aug 01 07:26:23 2017 +0200
@@ -58,6 +58,9 @@
(* testers *)
val is_nary: kind -> bool
+
+ (* string representations *)
+ val string_of_kind: kind -> string
end
structure Argo_Expr: ARGO_EXPR =
@@ -137,10 +140,12 @@
(* constructors *)
-val kind_of_string = the o Symtab.lookup (Symtab.make [
+val string_kinds = [
("true", True),("false", False), ("not", Not), ("and", And), ("or", Or), ("imp", Imp),
("iff", Iff), ("ite", Ite), ("eq", Eq), ("app", App), ("le", Le), ("lt", Lt), ("neg", Neg),
- ("add", Add), ("sub", Sub), ("mul", Mul), ("div", Div), ("min", Min), ("max", Max), ("abs", Abs)])
+ ("add", Add), ("sub", Sub), ("mul", Mul), ("div", Div), ("min", Min), ("max", Max), ("abs", Abs)]
+
+val kind_of_string = the o Symtab.lookup (Symtab.make string_kinds)
val true_expr = E (True, [])
val false_expr = E (False, [])
@@ -247,6 +252,15 @@
fun is_nary k = member (op =) [And, Or, Add] k
+
+(* string representations *)
+
+val kind_strings = map swap string_kinds
+
+fun string_of_kind (Con (n, _)) = n
+ | string_of_kind (Num n) = Rat.string_of_rat n
+ | string_of_kind k = the (AList.lookup (op =) kind_strings k)
+
end
structure Argo_Exprtab = Table(type key = Argo_Expr.expr val ord = Argo_Expr.expr_ord)
--- a/src/Tools/Argo/argo_proof.ML Mon Jul 31 15:38:21 2017 +0100
+++ b/src/Tools/Argo/argo_proof.ML Tue Aug 01 07:26:23 2017 +0200
@@ -42,7 +42,8 @@
Rewr_Ineq_Sub of inequality | Rewr_Ineq_Mul of inequality * Rat.rat |
Rewr_Not_Ineq of inequality
datatype conv =
- Keep_Conv | Then_Conv of conv * conv | Args_Conv of conv list | Rewr_Conv of rewrite
+ Keep_Conv | Then_Conv of conv * conv | Args_Conv of Argo_Expr.kind * conv list |
+ Rewr_Conv of rewrite
datatype rule =
Axiom of int | Taut of tautology * Argo_Expr.expr | Conjunct of int * int | Rewrite of conv |
Hyp of int * Argo_Expr.expr | Clause of int list | Lemma of int list | Unit_Res of int |
@@ -56,7 +57,7 @@
(* conversion constructors *)
val keep_conv: conv
val mk_then_conv: conv -> conv -> conv
- val mk_args_conv: conv list -> conv
+ val mk_args_conv: Argo_Expr.kind -> conv list -> conv
val mk_rewr_conv: rewrite -> conv
(* context *)
@@ -130,7 +131,8 @@
Rewr_Not_Ineq of inequality
datatype conv =
- Keep_Conv | Then_Conv of conv * conv | Args_Conv of conv list | Rewr_Conv of rewrite
+ Keep_Conv | Then_Conv of conv * conv | Args_Conv of Argo_Expr.kind * conv list |
+ Rewr_Conv of rewrite
datatype rule =
Axiom of int | Taut of tautology * Argo_Expr.expr | Conjunct of int * int | Rewrite of conv |
@@ -186,9 +188,9 @@
| mk_then_conv c Keep_Conv = c
| mk_then_conv c1 c2 = Then_Conv (c1, c2)
-fun mk_args_conv cs =
+fun mk_args_conv k cs =
if forall (fn Keep_Conv => true | _ => false) cs then Keep_Conv
- else Args_Conv cs
+ else Args_Conv (k, cs)
fun mk_rewr_conv r = Rewr_Conv r
@@ -386,7 +388,8 @@
fun string_of_conv Keep_Conv = "_"
| string_of_conv (c as Then_Conv _) =
space_implode " then " (map (enclose "(" ")" o string_of_conv) (flatten_then_conv c))
- | string_of_conv (Args_Conv cs) = "args " ^ brackets string_of_conv cs
+ | string_of_conv (Args_Conv (k, cs)) =
+ "args " ^ Argo_Expr.string_of_kind k ^ " " ^ brackets string_of_conv cs
| string_of_conv (Rewr_Conv r) = string_of_rewr r
fun string_of_rule (Axiom i) = "axiom " ^ string_of_int i
--- a/src/Tools/Argo/argo_rewr.ML Mon Jul 31 15:38:21 2017 +0100
+++ b/src/Tools/Argo/argo_rewr.ML Tue Aug 01 07:26:23 2017 +0200
@@ -55,7 +55,7 @@
fun on_args f (Argo_Expr.E (k, es)) =
let val (es, cs) = split_list (f es)
- in (Argo_Expr.E (k, es), Argo_Proof.mk_args_conv cs) end
+ in (Argo_Expr.E (k, es), Argo_Proof.mk_args_conv k cs) end
fun args cv e = on_args (map cv) e