# HG changeset patch
# User boehmes
# Date 1501565183 -7200
# Node ID 8a6a89d6cf2b65632ecdfd5d73d3b48eaeacf499
# Parent  829f1f62b08700197a301125b2400d47e7b7684c
more explicit Argo proof traces; more correct proof replay for term applications

diff -r 829f1f62b087 -r 8a6a89d6cf2b src/HOL/Tools/Argo/argo_tactic.ML
--- 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
diff -r 829f1f62b087 -r 8a6a89d6cf2b src/HOL/ex/Argo_Examples.thy
--- 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"
diff -r 829f1f62b087 -r 8a6a89d6cf2b src/Tools/Argo/argo_expr.ML
--- 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)
diff -r 829f1f62b087 -r 8a6a89d6cf2b src/Tools/Argo/argo_proof.ML
--- 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
diff -r 829f1f62b087 -r 8a6a89d6cf2b src/Tools/Argo/argo_rewr.ML
--- 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