src/HOL/Tools/Argo/argo_tactic.ML
author wenzelm
Sun Nov 26 21:08:32 2017 +0100 (17 months ago)
changeset 67091 1393c2340eec
parent 66301 8a6a89d6cf2b
child 67149 e61557884799
permissions -rw-r--r--
more symbols;
     1 (*  Title:      HOL/Tools/Argo/argo_tactic.ML
     2     Author:     Sascha Boehme
     3 
     4 HOL method and tactic for the Argo solver.
     5 *)
     6 
     7 signature ARGO_TACTIC =
     8 sig
     9   val trace: string Config.T
    10   val timeout: real Config.T
    11 
    12   (* extending the tactic *)
    13   type trans_context =
    14     Name.context * Argo_Expr.typ Typtab.table * (string * Argo_Expr.typ) Termtab.table
    15   type ('a, 'b) trans = 'a -> trans_context -> 'b * trans_context
    16   type ('a, 'b) trans' = 'a -> trans_context -> ('b * trans_context) option
    17   type extension = {
    18     trans_type: (typ, Argo_Expr.typ) trans -> (typ, Argo_Expr.typ) trans',
    19     trans_term: (term, Argo_Expr.expr) trans -> (term, Argo_Expr.expr) trans',
    20     term_of: (Argo_Expr.expr -> term) -> Argo_Expr.expr -> term option,
    21     replay_rewr: Proof.context -> Argo_Proof.rewrite -> conv,
    22     replay: (Argo_Expr.expr -> cterm) -> Proof.context -> Argo_Proof.rule -> thm list -> thm option}
    23   val add_extension: extension -> theory -> theory
    24 
    25   (* proof utilities *)
    26   val discharges: thm -> thm list -> thm list
    27   val flatten_conv: conv -> thm -> conv
    28 
    29   (* interface to the tactic as well as the underlying checker and prover *)
    30   datatype result = Satisfiable of term -> bool option | Unsatisfiable
    31   val check: term list -> Proof.context -> result * Proof.context
    32   val prove: thm list -> Proof.context -> thm option * Proof.context
    33   val argo_tac: Proof.context -> thm list -> int -> tactic
    34 end
    35 
    36 structure Argo_Tactic: ARGO_TACTIC =
    37 struct
    38 
    39 (* readable fresh names for terms *)
    40 
    41 fun fresh_name n = Name.variant (case Long_Name.base_name n of "" => "x" | n' => n')
    42 
    43 fun fresh_type_name (Type (n, _)) = fresh_name n
    44   | fresh_type_name (TFree (n, _)) = fresh_name n
    45   | fresh_type_name (TVar ((n, i), _)) = fresh_name (n ^ "." ^ string_of_int i)
    46 
    47 fun fresh_term_name (Const (n, _)) = fresh_name n
    48   | fresh_term_name (Free (n, _)) = fresh_name n
    49   | fresh_term_name (Var ((n, i), _)) = fresh_name (n ^ "." ^ string_of_int i)
    50   | fresh_term_name _ = fresh_name ""
    51 
    52 
    53 (* tracing *)
    54 
    55 datatype mode = None | Basic | Full
    56 
    57 fun string_of_mode None = "none"
    58   | string_of_mode Basic = "basic"
    59   | string_of_mode Full = "full"
    60 
    61 fun requires_mode None = []
    62   | requires_mode Basic = [Basic, Full]
    63   | requires_mode Full = [Full]
    64 
    65 val trace = Attrib.setup_config_string @{binding argo_trace} (K (string_of_mode None))
    66 
    67 fun allows_mode ctxt = exists (equal (Config.get ctxt trace) o string_of_mode) o requires_mode
    68 
    69 fun output mode ctxt msg = if allows_mode ctxt mode then Output.tracing ("Argo: " ^ msg) else ()
    70 val tracing = output Basic
    71 val full_tracing = output Full
    72 
    73 fun with_mode mode ctxt f = if allows_mode ctxt mode then f ctxt else ()
    74 val with_tracing = with_mode Basic
    75 val with_full_tracing = with_mode Full
    76 
    77 
    78 (* timeout *)
    79 
    80 val timeout = Attrib.setup_config_real @{binding argo_timeout} (K 10.0)
    81 
    82 fun time_of_timeout ctxt = Time.fromReal (Config.get ctxt timeout)
    83 
    84 fun with_timeout ctxt f x = Timeout.apply (time_of_timeout ctxt) f x
    85 
    86 
    87 (* extending the tactic *)
    88 
    89 type trans_context =
    90   Name.context * Argo_Expr.typ Typtab.table * (string * Argo_Expr.typ) Termtab.table
    91 
    92 type ('a, 'b) trans = 'a -> trans_context -> 'b * trans_context
    93 type ('a, 'b) trans' = 'a -> trans_context -> ('b * trans_context) option
    94 
    95 type extension = {
    96   trans_type: (typ, Argo_Expr.typ) trans -> (typ, Argo_Expr.typ) trans',
    97   trans_term: (term, Argo_Expr.expr) trans -> (term, Argo_Expr.expr) trans',
    98   term_of: (Argo_Expr.expr -> term) -> Argo_Expr.expr -> term option,
    99   replay_rewr: Proof.context -> Argo_Proof.rewrite -> conv,
   100   replay: (Argo_Expr.expr -> cterm) -> Proof.context -> Argo_Proof.rule -> thm list -> thm option}
   101 
   102 fun eq_extension ((serial1, _), (serial2, _)) = (serial1 = serial2)
   103 
   104 structure Extensions = Theory_Data
   105 (
   106   type T = (serial * extension) list
   107   val empty = []
   108   val extend = I
   109   val merge = merge eq_extension 
   110 )
   111 
   112 fun add_extension ext = Extensions.map (insert eq_extension (serial (), ext))
   113 fun get_extensions ctxt = Extensions.get (Proof_Context.theory_of ctxt)
   114 fun apply_first ctxt f = get_first (fn (_, e) => f e) (get_extensions ctxt)
   115 
   116 fun ext_trans sel ctxt f x tcx = apply_first ctxt (fn ext => sel ext f x tcx)
   117 
   118 val ext_trans_type = ext_trans (fn {trans_type, ...}: extension => trans_type)
   119 val ext_trans_term = ext_trans (fn {trans_term, ...}: extension => trans_term)
   120 
   121 fun ext_term_of ctxt f e = apply_first ctxt (fn {term_of, ...}: extension => term_of f e)
   122 
   123 fun ext_replay_rewr ctxt r = 
   124   get_extensions ctxt
   125   |> map (fn (_, {replay_rewr, ...}: extension) => replay_rewr ctxt r)
   126   |> Conv.first_conv
   127 
   128 fun ext_replay cprop_of ctxt rule prems =
   129   (case apply_first ctxt (fn {replay, ...}: extension => replay cprop_of ctxt rule prems) of
   130     SOME thm => thm
   131   | NONE => raise THM ("failed to replay " ^ quote (Argo_Proof.string_of_rule rule), 0, []))
   132 
   133 
   134 (* translating input terms *)
   135 
   136 fun add_new_type T (names, types, terms) =
   137   let
   138     val (n, names') = fresh_type_name T names
   139     val ty = Argo_Expr.Type n
   140   in (ty, (names', Typtab.update (T, ty) types, terms)) end
   141 
   142 fun add_type T (tcx as (_, types, _)) =
   143   (case Typtab.lookup types T of
   144     SOME ty => (ty, tcx)
   145   | NONE => add_new_type T tcx)
   146 
   147 fun trans_type _ @{typ HOL.bool} = pair Argo_Expr.Bool
   148   | trans_type ctxt (Type (@{type_name "fun"}, [T1, T2])) =
   149       trans_type ctxt T1 ##>> trans_type ctxt T2 #>> Argo_Expr.Func
   150   | trans_type ctxt T = (fn tcx =>
   151       (case ext_trans_type ctxt (trans_type ctxt) T tcx of
   152         SOME result => result
   153       | NONE => add_type T tcx))
   154 
   155 fun add_new_term ctxt t T tcx =
   156   let
   157     val (ty, (names, types, terms)) = trans_type ctxt T tcx
   158     val (n, names') = fresh_term_name t names
   159     val c = (n, ty)
   160   in (Argo_Expr.mk_con c, (names', types, Termtab.update (t, c) terms)) end
   161 
   162 fun add_term ctxt t (tcx as (_, _, terms)) =
   163   (case Termtab.lookup terms t of
   164     SOME c => (Argo_Expr.mk_con c, tcx)
   165   | NONE => add_new_term ctxt t (Term.fastype_of t) tcx)
   166 
   167 fun mk_eq @{typ HOL.bool} = Argo_Expr.mk_iff
   168   | mk_eq _ = Argo_Expr.mk_eq
   169 
   170 fun trans_term _ @{const HOL.True} = pair Argo_Expr.true_expr
   171   | trans_term _ @{const HOL.False} = pair Argo_Expr.false_expr
   172   | trans_term ctxt (@{const HOL.Not} $ t) = trans_term ctxt t #>> Argo_Expr.mk_not
   173   | trans_term ctxt (@{const HOL.conj} $ t1 $ t2) =
   174       trans_term ctxt t1 ##>> trans_term ctxt t2 #>> uncurry Argo_Expr.mk_and2
   175   | trans_term ctxt (@{const HOL.disj} $ t1 $ t2) =
   176       trans_term ctxt t1 ##>> trans_term ctxt t2 #>> uncurry Argo_Expr.mk_or2
   177   | trans_term ctxt (@{const HOL.implies} $ t1 $ t2) =
   178       trans_term ctxt t1 ##>> trans_term ctxt t2 #>> uncurry Argo_Expr.mk_imp
   179   | trans_term ctxt (Const (@{const_name HOL.If}, _) $ t1 $ t2 $ t3) =
   180       trans_term ctxt t1 ##>> trans_term ctxt t2 ##>> trans_term ctxt t3 #>>
   181       (fn ((u1, u2), u3) => Argo_Expr.mk_ite u1 u2 u3)
   182   | trans_term ctxt (Const (@{const_name HOL.eq}, T) $ t1 $ t2) =
   183       trans_term ctxt t1 ##>> trans_term ctxt t2 #>> uncurry (mk_eq (Term.domain_type T))
   184   | trans_term ctxt (t as (t1 $ t2)) = (fn tcx =>
   185       (case ext_trans_term ctxt (trans_term ctxt) t tcx of
   186         SOME result => result
   187       | NONE => tcx |> trans_term ctxt t1 ||>> trans_term ctxt t2 |>> uncurry Argo_Expr.mk_app))
   188   | trans_term ctxt t = (fn tcx =>
   189       (case ext_trans_term ctxt (trans_term ctxt) t tcx of
   190         SOME result => result
   191       | NONE => add_term ctxt t tcx))
   192 
   193 fun translate ctxt prop = trans_term ctxt (HOLogic.dest_Trueprop prop)
   194 
   195 
   196 (* invoking the solver *)
   197 
   198 type data = {
   199   names: Name.context,
   200   types: Argo_Expr.typ Typtab.table,
   201   terms: (string * Argo_Expr.typ) Termtab.table,
   202   argo: Argo_Solver.context}
   203 
   204 fun mk_data names types terms argo: data = {names=names, types=types, terms=terms, argo=argo}
   205 val empty_data = mk_data Name.context Typtab.empty Termtab.empty Argo_Solver.context
   206 
   207 structure Solver_Data = Proof_Data
   208 (
   209   type T = data option
   210   fun init _ = SOME empty_data
   211 )
   212 
   213 datatype ('m, 'p) solver_result = Model of 'm | Proof of 'p
   214 
   215 fun raw_solve es argo = Model (Argo_Solver.assert es argo)
   216   handle Argo_Proof.UNSAT proof => Proof proof
   217 
   218 fun value_of terms model t =
   219   (case Termtab.lookup terms t of
   220     SOME c => model c
   221   | _ => NONE)
   222 
   223 fun trace_props props ctxt =
   224   tracing ctxt (Pretty.string_of (Pretty.big_list "using these propositions:"
   225     (map (Syntax.pretty_term ctxt) props)))
   226 
   227 fun trace_result ctxt ({elapsed, ...}: Timing.timing) msg =
   228   tracing ctxt ("found a " ^ msg ^ " in " ^ string_of_int (Time.toMilliseconds elapsed) ^ " ms")
   229 
   230 fun solve props ctxt =
   231   (case Solver_Data.get ctxt of
   232     NONE => error "bad Argo solver context"
   233   | SOME {names, types, terms, argo} =>
   234       let
   235         val _ = with_tracing ctxt (trace_props props)
   236         val (es, (names', types', terms')) = fold_map (translate ctxt) props (names, types, terms)
   237         val _ = tracing ctxt "starting the prover"
   238       in
   239         (case Timing.timing (raw_solve es) argo of
   240           (time, Proof proof) =>
   241             let val _ = trace_result ctxt time "proof"
   242             in (Proof (terms', proof), Solver_Data.put NONE ctxt) end
   243         | (time, Model argo') =>
   244             let
   245               val _ = trace_result ctxt time "model"
   246               val model = value_of terms' (Argo_Solver.model_of argo')
   247             in (Model model, Solver_Data.put (SOME (mk_data names' types' terms' argo')) ctxt) end)
   248       end)
   249 
   250 
   251 (* reverse translation *)
   252 
   253 structure Contab = Table(type key = string * Argo_Expr.typ val ord = Argo_Expr.con_ord)
   254 
   255 fun mk_nary f ts = uncurry (fold_rev (curry f)) (split_last ts)
   256 
   257 fun mk_nary' d _ [] = d
   258   | mk_nary' _ f ts = mk_nary f ts
   259 
   260 fun mk_ite t1 t2 t3 =
   261   let
   262     val T = Term.fastype_of t2
   263     val ite = Const (@{const_name HOL.If}, [@{typ HOL.bool}, T, T] ---> T)
   264   in ite $ t1 $ t2 $ t3 end
   265 
   266 fun term_of _ (Argo_Expr.E (Argo_Expr.True, _)) = @{const HOL.True}
   267   | term_of _ (Argo_Expr.E (Argo_Expr.False, _)) = @{const HOL.False}
   268   | term_of cx (Argo_Expr.E (Argo_Expr.Not, [e])) = HOLogic.mk_not (term_of cx e)
   269   | term_of cx (Argo_Expr.E (Argo_Expr.And, es)) =
   270       mk_nary' @{const HOL.True} HOLogic.mk_conj (map (term_of cx) es)
   271   | term_of cx (Argo_Expr.E (Argo_Expr.Or, es)) =
   272       mk_nary' @{const HOL.False} HOLogic.mk_disj (map (term_of cx) es)
   273   | term_of cx (Argo_Expr.E (Argo_Expr.Imp, [e1, e2])) =
   274       HOLogic.mk_imp (term_of cx e1, term_of cx e2)
   275   | term_of cx (Argo_Expr.E (Argo_Expr.Iff, [e1, e2])) =
   276       HOLogic.mk_eq (term_of cx e1, term_of cx e2)
   277   | term_of cx (Argo_Expr.E (Argo_Expr.Ite, [e1, e2, e3])) =
   278       mk_ite (term_of cx e1) (term_of cx e2) (term_of cx e3)
   279   | term_of cx (Argo_Expr.E (Argo_Expr.Eq, [e1, e2])) =
   280       HOLogic.mk_eq (term_of cx e1, term_of cx e2)
   281   | term_of cx (Argo_Expr.E (Argo_Expr.App, [e1, e2])) =
   282       term_of cx e1 $ term_of cx e2
   283   | term_of (_, cons) (Argo_Expr.E (Argo_Expr.Con (c as (n, _)), _)) =
   284       (case Contab.lookup cons c of
   285         SOME t => t
   286       | NONE => error ("Unexpected expression named " ^ quote n))
   287   | term_of (cx as (ctxt, _)) e =
   288       (case ext_term_of ctxt (term_of cx) e of
   289         SOME t => t
   290       | NONE => raise Fail "bad expression")
   291 
   292 fun as_prop ct = Thm.apply @{cterm HOL.Trueprop} ct
   293 
   294 fun cterm_of ctxt cons e = Thm.cterm_of ctxt (term_of (ctxt, cons) e)
   295 fun cprop_of ctxt cons e = as_prop (cterm_of ctxt cons e)
   296 
   297 
   298 (* generic proof tools *)
   299 
   300 fun discharge thm rule = thm INCR_COMP rule
   301 fun discharge2 thm1 thm2 rule = discharge thm2 (discharge thm1 rule)
   302 fun discharges thm rules = [thm] RL rules
   303 
   304 fun under_assumption f ct =
   305   let val cprop = as_prop ct
   306   in Thm.implies_intr cprop (f (Thm.assume cprop)) end
   307 
   308 fun instantiate cv ct = Thm.instantiate ([], [(Term.dest_Var (Thm.term_of cv), ct)])
   309 
   310 
   311 (* proof replay for tautologies *)
   312 
   313 fun prove_taut ctxt ns t = Goal.prove ctxt ns [] (HOLogic.mk_Trueprop t)
   314   (fn {context, ...} => HEADGOAL (Classical.fast_tac context))
   315 
   316 fun with_frees ctxt n mk =
   317   let
   318     val ns = map (fn i => "P" ^ string_of_int i) (0 upto (n - 1))
   319     val ts = map (Free o rpair @{typ bool}) ns
   320     val t = mk_nary HOLogic.mk_disj (mk ts)
   321   in prove_taut ctxt ns t end
   322 
   323 fun taut_and1_term ts = mk_nary HOLogic.mk_conj ts :: map HOLogic.mk_not ts
   324 fun taut_and2_term i ts = [HOLogic.mk_not (mk_nary HOLogic.mk_conj ts), nth ts i]
   325 fun taut_or1_term i ts = [mk_nary HOLogic.mk_disj ts, HOLogic.mk_not (nth ts i)]
   326 fun taut_or2_term ts = HOLogic.mk_not (mk_nary HOLogic.mk_disj ts) :: ts
   327 
   328 val iff_1_taut = @{lemma "P = Q \<or> P \<or> Q" by fast}
   329 val iff_2_taut = @{lemma "P = Q \<or> (\<not>P) \<or> (\<not>Q)" by fast}
   330 val iff_3_taut = @{lemma "\<not>(P = Q) \<or> (\<not>P) \<or> Q" by fast}
   331 val iff_4_taut = @{lemma "\<not>(P = Q) \<or> P \<or> (\<not>Q)" by fast}
   332 val ite_then_taut = @{lemma "\<not>P \<or> (if P then t else u) = t" by auto}
   333 val ite_else_taut = @{lemma "P \<or> (if P then t else u) = u" by auto}
   334 
   335 fun taut_rule_of ctxt (Argo_Proof.Taut_And_1 n) = with_frees ctxt n taut_and1_term
   336   | taut_rule_of ctxt (Argo_Proof.Taut_And_2 (i, n)) = with_frees ctxt n (taut_and2_term i)
   337   | taut_rule_of ctxt (Argo_Proof.Taut_Or_1 (i, n)) = with_frees ctxt n (taut_or1_term i)
   338   | taut_rule_of ctxt (Argo_Proof.Taut_Or_2 n) = with_frees ctxt n taut_or2_term
   339   | taut_rule_of _ Argo_Proof.Taut_Iff_1 = iff_1_taut
   340   | taut_rule_of _ Argo_Proof.Taut_Iff_2 = iff_2_taut
   341   | taut_rule_of _ Argo_Proof.Taut_Iff_3 = iff_3_taut
   342   | taut_rule_of _ Argo_Proof.Taut_Iff_4 = iff_4_taut
   343   | taut_rule_of _ Argo_Proof.Taut_Ite_Then = ite_then_taut
   344   | taut_rule_of _ Argo_Proof.Taut_Ite_Else = ite_else_taut
   345 
   346 fun replay_taut ctxt k ct =
   347   let val rule = taut_rule_of ctxt k
   348   in Thm.instantiate (Thm.match (Thm.cprop_of rule, ct)) rule end
   349 
   350 
   351 (* proof replay for conjunct extraction *)
   352 
   353 fun replay_conjunct 0 1 thm = thm
   354   | replay_conjunct 0 _ thm = discharge thm @{thm conjunct1}
   355   | replay_conjunct 1 2 thm = discharge thm @{thm conjunct2}
   356   | replay_conjunct i n thm = replay_conjunct (i - 1) (n - 1) (discharge thm @{thm conjunct2})
   357 
   358 
   359 (* proof replay for rewrite steps *)
   360 
   361 fun mk_rewr thm = thm RS @{thm eq_reflection}
   362 
   363 fun not_nary_conv rule i ct =
   364   if i > 1 then (Conv.rewr_conv rule then_conv Conv.arg_conv (not_nary_conv rule (i - 1))) ct
   365   else Conv.all_conv ct
   366 
   367 val flatten_and_thm = @{lemma "(P1 \<and> P2) \<and> P3 \<equiv> P1 \<and> P2 \<and> P3" by simp}
   368 val flatten_or_thm = @{lemma "(P1 \<or> P2) \<or> P3 \<equiv> P1 \<or> P2 \<or> P3" by simp}
   369 
   370 fun flatten_conv cv rule ct = (
   371   Conv.try_conv (Conv.arg_conv cv) then_conv
   372   Conv.try_conv (Conv.rewr_conv rule then_conv cv)) ct
   373 
   374 fun flat_conj_conv ct =
   375   (case Thm.term_of ct of
   376     @{const HOL.conj} $ _ $ _ => flatten_conv flat_conj_conv flatten_and_thm ct
   377   | _ => Conv.all_conv ct)
   378 
   379 fun flat_disj_conv ct =
   380   (case Thm.term_of ct of
   381     @{const HOL.disj} $ _ $ _ => flatten_conv flat_disj_conv flatten_or_thm ct
   382   | _ => Conv.all_conv ct)
   383 
   384 fun explode rule1 rule2 thm =
   385   explode rule1 rule2 (thm RS rule1) @ explode rule1 rule2 (thm RS rule2) handle THM _ => [thm]
   386 val explode_conj = explode @{thm conjunct1} @{thm conjunct2}
   387 val explode_ndis = explode @{lemma "\<not>(P \<or> Q) \<Longrightarrow> \<not>P" by auto} @{lemma "\<not>(P \<or> Q) \<Longrightarrow> \<not>Q" by auto}
   388 
   389 fun pick_false i thms = nth thms i
   390 
   391 fun pick_dual rule (i1, i2) thms =
   392   rule OF [nth thms i1, nth thms i2] handle THM _ => rule OF [nth thms i2, nth thms i1]
   393 val pick_dual_conj = pick_dual @{lemma "\<not>P \<Longrightarrow> P \<Longrightarrow> False" by auto}
   394 val pick_dual_ndis = pick_dual @{lemma "\<not>P \<Longrightarrow> P \<Longrightarrow> \<not>True" by auto}
   395 
   396 fun join thm0 rule is thms =
   397   let
   398     val l = length thms
   399     val thms' = fold (fn i => cons (if 0 <= i andalso i < l then nth thms i else thm0)) is []
   400   in fold (fn thm => fn thm' => discharge2 thm thm' rule) (tl thms') (hd thms') end
   401 
   402 val join_conj = join @{lemma "True" by auto} @{lemma "P \<Longrightarrow> Q \<Longrightarrow> P \<and> Q" by auto}
   403 val join_ndis = join @{lemma "\<not>False" by auto} @{lemma "\<not>P \<Longrightarrow> \<not>Q \<Longrightarrow> \<not>(P \<or> Q)" by auto}
   404 
   405 val false_thm = @{lemma "False \<Longrightarrow> P" by auto}
   406 val ntrue_thm = @{lemma "\<not>True \<Longrightarrow> P" by auto}
   407 val iff_conj_thm = @{lemma "(P \<Longrightarrow> Q) \<Longrightarrow> (Q \<Longrightarrow> P) \<Longrightarrow> P = Q" by auto}
   408 val iff_ndis_thm = @{lemma "(\<not>P \<Longrightarrow> \<not>Q) \<Longrightarrow> (\<not>Q \<Longrightarrow> \<not>P) \<Longrightarrow> P = Q" by auto}
   409 
   410 fun iff_intro rule lf rf ct =
   411   let
   412     val lhs = under_assumption lf ct
   413     val rhs = rf (Thm.dest_arg (snd (Thm.dest_implies (Thm.cprop_of lhs))))
   414   in mk_rewr (discharge2 lhs rhs rule) end
   415 
   416 fun with_conj f g ct = iff_intro iff_conj_thm (f o explode_conj) g ct
   417 fun with_ndis f g ct = iff_intro iff_ndis_thm (f o explode_ndis) g (Thm.apply @{cterm HOL.Not} ct)
   418 
   419 fun swap_indices n iss = map (fn i => find_index (fn is => member (op =) is i) iss) (0 upto (n - 1))
   420 fun sort_nary w f g (n, iss) = w (f (map hd iss)) (under_assumption (f (swap_indices n iss) o g))
   421 val sort_conj = sort_nary with_conj join_conj explode_conj
   422 val sort_ndis = sort_nary with_ndis join_ndis explode_ndis 
   423 
   424 val not_true_thm = mk_rewr @{lemma "(\<not>True) = False" by auto}
   425 val not_false_thm = mk_rewr @{lemma "(\<not>False) = True" by auto}
   426 val not_not_thm = mk_rewr @{lemma "(\<not>\<not>P) = P" by auto}
   427 val not_and_thm = mk_rewr @{lemma "(\<not>(P \<and> Q)) = (\<not>P \<or> \<not>Q)" by auto}
   428 val not_or_thm = mk_rewr @{lemma "(\<not>(P \<or> Q)) = (\<not>P \<and> \<not>Q)" by auto}
   429 val not_iff_thms = map mk_rewr
   430   @{lemma "(\<not>((\<not>P) = Q)) = (P = Q)" "(\<not>(P = (\<not>Q))) = (P = Q)" "(\<not>(P = Q)) = ((\<not>P) = Q)" by auto}
   431 val iff_true_thms = map mk_rewr @{lemma "(True = P) = P" "(P = True) = P" by auto}
   432 val iff_false_thms = map mk_rewr @{lemma "(False = P) = (\<not>P)" "(P = False) = (\<not>P)" by auto}
   433 val iff_not_not_thm = mk_rewr @{lemma "((\<not>P) = (\<not>Q)) = (P = Q)" by auto}
   434 val iff_refl_thm = mk_rewr @{lemma "(P = P) = True" by auto}
   435 val iff_symm_thm = mk_rewr @{lemma "(P = Q) = (Q = P)" by auto}
   436 val iff_dual_thms = map mk_rewr @{lemma "(P = (\<not>P)) = False" "((\<not>P) = P) = False" by auto}
   437 val imp_thm = mk_rewr @{lemma "(P \<longrightarrow> Q) = (\<not>P \<or> Q)" by auto}
   438 val ite_prop_thm = mk_rewr @{lemma "(If P Q R) = ((\<not>P \<or> Q) \<and> (P \<or> R) \<and> (Q \<or> R))" by auto}
   439 val ite_true_thm = mk_rewr @{lemma "(If True t u) = t" by auto}
   440 val ite_false_thm = mk_rewr @{lemma "(If False t u) = u" by auto}
   441 val ite_eq_thm = mk_rewr @{lemma "(If P t t) = t" by auto}
   442 val eq_refl_thm = mk_rewr @{lemma "(t = t) = True" by auto}
   443 val eq_symm_thm = mk_rewr @{lemma "(t1 = t2) = (t2 = t1)" by auto}
   444 
   445 fun replay_rewr _ Argo_Proof.Rewr_Not_True = Conv.rewr_conv not_true_thm
   446   | replay_rewr _ Argo_Proof.Rewr_Not_False = Conv.rewr_conv not_false_thm
   447   | replay_rewr _ Argo_Proof.Rewr_Not_Not = Conv.rewr_conv not_not_thm
   448   | replay_rewr _ (Argo_Proof.Rewr_Not_And i) = not_nary_conv not_and_thm i
   449   | replay_rewr _ (Argo_Proof.Rewr_Not_Or i) = not_nary_conv not_or_thm i
   450   | replay_rewr _ Argo_Proof.Rewr_Not_Iff = Conv.rewrs_conv not_iff_thms
   451   | replay_rewr _ (Argo_Proof.Rewr_And_False i) = with_conj (pick_false i) (K false_thm)
   452   | replay_rewr _ (Argo_Proof.Rewr_And_Dual ip) = with_conj (pick_dual_conj ip) (K false_thm)
   453   | replay_rewr _ (Argo_Proof.Rewr_And_Sort is) = flat_conj_conv then_conv sort_conj is
   454   | replay_rewr _ (Argo_Proof.Rewr_Or_True i) = with_ndis (pick_false i) (K ntrue_thm)
   455   | replay_rewr _ (Argo_Proof.Rewr_Or_Dual ip) = with_ndis (pick_dual_ndis ip) (K ntrue_thm)
   456   | replay_rewr _ (Argo_Proof.Rewr_Or_Sort is) = flat_disj_conv then_conv sort_ndis is
   457   | replay_rewr _ Argo_Proof.Rewr_Iff_True = Conv.rewrs_conv iff_true_thms
   458   | replay_rewr _ Argo_Proof.Rewr_Iff_False = Conv.rewrs_conv iff_false_thms
   459   | replay_rewr _ Argo_Proof.Rewr_Iff_Not_Not = Conv.rewr_conv iff_not_not_thm
   460   | replay_rewr _ Argo_Proof.Rewr_Iff_Refl = Conv.rewr_conv iff_refl_thm
   461   | replay_rewr _ Argo_Proof.Rewr_Iff_Symm = Conv.rewr_conv iff_symm_thm
   462   | replay_rewr _ Argo_Proof.Rewr_Iff_Dual  = Conv.rewrs_conv iff_dual_thms
   463   | replay_rewr _ Argo_Proof.Rewr_Imp = Conv.rewr_conv imp_thm
   464   | replay_rewr _ Argo_Proof.Rewr_Ite_Prop = Conv.rewr_conv ite_prop_thm
   465   | replay_rewr _ Argo_Proof.Rewr_Ite_True = Conv.rewr_conv ite_true_thm
   466   | replay_rewr _ Argo_Proof.Rewr_Ite_False = Conv.rewr_conv ite_false_thm
   467   | replay_rewr _ Argo_Proof.Rewr_Ite_Eq = Conv.rewr_conv ite_eq_thm
   468   | replay_rewr _ Argo_Proof.Rewr_Eq_Refl = Conv.rewr_conv eq_refl_thm
   469   | replay_rewr _ Argo_Proof.Rewr_Eq_Symm = Conv.rewr_conv eq_symm_thm
   470   | replay_rewr ctxt r = ext_replay_rewr ctxt r
   471 
   472 fun binop_conv cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
   473 
   474 fun replay_conv _ Argo_Proof.Keep_Conv ct = Conv.all_conv ct
   475   | replay_conv ctxt (Argo_Proof.Then_Conv (c1, c2)) ct = 
   476       (replay_conv ctxt c1 then_conv replay_conv ctxt c2) ct
   477   | replay_conv ctxt (Argo_Proof.Args_Conv (Argo_Expr.App, [c1, c2])) ct =
   478       Conv.combination_conv (replay_conv ctxt c1) (replay_conv ctxt c2) ct
   479   | replay_conv ctxt (Argo_Proof.Args_Conv (_, cs)) ct = replay_args_conv ctxt cs ct
   480   | replay_conv ctxt (Argo_Proof.Rewr_Conv r) ct = replay_rewr ctxt r ct
   481 
   482 and replay_args_conv _ [] ct = Conv.all_conv ct
   483   | replay_args_conv ctxt [c] ct = Conv.arg_conv (replay_conv ctxt c) ct
   484   | replay_args_conv ctxt [c1, c2] ct = binop_conv (replay_conv ctxt c1) (replay_conv ctxt c2) ct
   485   | replay_args_conv ctxt (c :: cs) ct =
   486       (case Term.head_of (Thm.term_of ct) of
   487         Const (@{const_name HOL.If}, _) =>
   488           let val (cs', c') = split_last cs
   489           in Conv.combination_conv (replay_args_conv ctxt (c :: cs')) (replay_conv ctxt c') ct end
   490       | _ => binop_conv (replay_conv ctxt c) (replay_args_conv ctxt cs) ct)
   491 
   492 fun replay_rewrite ctxt c thm = Conv.fconv_rule (HOLogic.Trueprop_conv (replay_conv ctxt c)) thm
   493 
   494 
   495 (* proof replay for clauses *)
   496 
   497 val prep_clause_rule = @{lemma "P \<Longrightarrow> \<not>P \<Longrightarrow> False" by fast}
   498 val extract_lit_rule = @{lemma "(\<not>(P \<or> Q) \<Longrightarrow> False) \<Longrightarrow> \<not>P \<Longrightarrow> \<not>Q \<Longrightarrow> False" by fast}
   499 
   500 fun add_lit i thm lits =
   501   let val ct = Thm.cprem_of thm 1
   502   in (Thm.implies_elim thm (Thm.assume ct), (i, ct) :: lits) end
   503 
   504 fun extract_lits [] _ = error "Bad clause"
   505   | extract_lits [i] (thm, lits) = add_lit i thm lits
   506   | extract_lits (i :: is) (thm, lits) =
   507       extract_lits is (add_lit i (discharge thm extract_lit_rule) lits)
   508 
   509 fun lit_ord ((l1, _), (l2, _)) = int_ord (abs l1, abs l2)
   510 
   511 fun replay_with_lits [] thm lits = (thm, lits)
   512   | replay_with_lits is thm lits =
   513       extract_lits is (discharge thm prep_clause_rule, lits)
   514       ||> Ord_List.make lit_ord
   515 
   516 fun replay_clause is thm = replay_with_lits is thm []
   517 
   518 
   519 (* proof replay for unit resolution *)
   520 
   521 val unit_rule = @{lemma "(P \<Longrightarrow> False) \<Longrightarrow> (\<not>P \<Longrightarrow> False) \<Longrightarrow> False" by fast}
   522 val unit_rule_var = Thm.dest_arg (Thm.dest_arg1 (Thm.cprem_of unit_rule 1))
   523 val bogus_ct = @{cterm HOL.True}
   524 
   525 fun replay_unit_res lit (pthm, plits) (nthm, nlits) =
   526   let
   527     val plit = the (AList.lookup (op =) plits lit)
   528     val nlit = the (AList.lookup (op =) nlits (~lit))
   529     val prune = Ord_List.remove lit_ord (lit, bogus_ct)
   530   in
   531     unit_rule
   532     |> instantiate unit_rule_var (Thm.dest_arg plit)
   533     |> Thm.elim_implies (Thm.implies_intr plit pthm)
   534     |> Thm.elim_implies (Thm.implies_intr nlit nthm)
   535     |> rpair (Ord_List.union lit_ord (prune nlits) (prune plits))
   536   end
   537 
   538 
   539 (* proof replay for hypothesis *)
   540 
   541 val dneg_rule = @{lemma "\<not>\<not>P \<Longrightarrow> P" by auto}
   542 
   543 fun replay_hyp i ct =
   544   if i < 0 then (Thm.assume ct, [(~i, ct)])
   545   else
   546     let val cu = as_prop (Thm.apply @{cterm HOL.Not} (Thm.apply @{cterm HOL.Not} (Thm.dest_arg ct)))
   547     in (discharge (Thm.assume cu) dneg_rule, [(~i, cu)]) end
   548 
   549 
   550 (* proof replay for lemma *)
   551 
   552 fun replay_lemma is (thm, lits) = replay_with_lits is thm lits
   553 
   554 
   555 (* proof replay for reflexivity *)
   556 
   557 val refl_rule = @{thm refl}
   558 val refl_rule_var = Thm.dest_arg1 (Thm.dest_arg (Thm.cprop_of refl_rule))
   559 
   560 fun replay_refl ct = Thm.instantiate (Thm.match (refl_rule_var, ct)) refl_rule
   561 
   562 
   563 (* proof replay for symmetry *)
   564 
   565 val symm_rules = @{lemma "a = b ==> b = a" "\<not>(a = b) \<Longrightarrow> \<not>(b = a)" by simp_all}
   566 
   567 fun replay_symm thm = hd (discharges thm symm_rules)
   568 
   569 
   570 (* proof replay for transitivity *)
   571 
   572 val trans_rules = @{lemma
   573   "\<not>(a = b) \<Longrightarrow> b = c \<Longrightarrow> \<not>(a = c)"
   574   "a = b \<Longrightarrow> \<not>(b = c) \<Longrightarrow> \<not>(a = c)"
   575   "a = b \<Longrightarrow> b = c ==> a = c"
   576   by simp_all}
   577 
   578 fun replay_trans thm1 thm2 = hd (discharges thm2 (discharges thm1 trans_rules))
   579 
   580 
   581 (* proof replay for congruence *)
   582 
   583 fun replay_cong thm1 thm2 = discharge thm2 (discharge thm1 @{thm cong})
   584 
   585 
   586 (* proof replay for substitution *)
   587 
   588 val subst_rule1 = @{lemma "\<not>(p a) \<Longrightarrow> p = q \<Longrightarrow> a = b \<Longrightarrow> \<not>(q b)" by simp}
   589 val subst_rule2 = @{lemma "p a \<Longrightarrow> p = q \<Longrightarrow> a = b \<Longrightarrow> q b" by simp}
   590 
   591 fun replay_subst thm1 thm2 thm3 =
   592   subst_rule1 OF [thm1, thm2, thm3] handle THM _ => subst_rule2 OF [thm1, thm2, thm3]
   593 
   594 
   595 (* proof replay *)
   596 
   597 structure Thm_Cache = Table(type key = Argo_Proof.proof_id val ord = Argo_Proof.proof_id_ord)
   598 
   599 val unclausify_rule1 = @{lemma "(\<not>P \<Longrightarrow> False) \<Longrightarrow> P" by auto}
   600 val unclausify_rule2 = @{lemma "(P \<Longrightarrow> False) \<Longrightarrow> \<not>P" by auto}
   601 
   602 fun unclausify (thm, lits) ls =
   603   (case (Thm.prop_of thm, lits) of
   604     (@{const HOL.Trueprop} $ @{const HOL.False}, [(_, ct)]) =>
   605       let val thm = Thm.implies_intr ct thm
   606       in (discharge thm unclausify_rule1 handle THM _ => discharge thm unclausify_rule2, ls) end
   607   | _ => (thm, Ord_List.union lit_ord lits ls))
   608 
   609 fun with_thms f tps = fold_map unclausify tps [] |>> f
   610 
   611 fun bad_premises () = raise Fail "bad number of premises"
   612 fun with_thms1 f = with_thms (fn [thm] => f thm | _ => bad_premises ())
   613 fun with_thms2 f = with_thms (fn [thm1, thm2] => f thm1 thm2 | _ => bad_premises ())
   614 fun with_thms3 f = with_thms (fn [thm1, thm2, thm3] => f thm1 thm2 thm3 | _ => bad_premises ())
   615 
   616 fun replay_rule (ctxt, cons, facts) prems rule =
   617   (case rule of
   618     Argo_Proof.Axiom i => (nth facts i, [])
   619   | Argo_Proof.Taut (k, concl) => (replay_taut ctxt k (cprop_of ctxt cons concl), [])
   620   | Argo_Proof.Conjunct (i, n) => with_thms1 (replay_conjunct i n) prems
   621   | Argo_Proof.Rewrite c => with_thms1 (replay_rewrite ctxt c) prems
   622   | Argo_Proof.Clause is => replay_clause is (fst (hd prems))
   623   | Argo_Proof.Unit_Res i => replay_unit_res i (hd prems) (hd (tl prems))
   624   | Argo_Proof.Hyp (i, concl) => replay_hyp i (cprop_of ctxt cons concl)
   625   | Argo_Proof.Lemma is => replay_lemma is (hd prems)
   626   | Argo_Proof.Refl concl => (replay_refl (cterm_of ctxt cons concl), [])
   627   | Argo_Proof.Symm => with_thms1 replay_symm prems
   628   | Argo_Proof.Trans => with_thms2 replay_trans prems
   629   | Argo_Proof.Cong => with_thms2 replay_cong prems
   630   | Argo_Proof.Subst => with_thms3 replay_subst prems
   631   | _ => with_thms (ext_replay (cprop_of ctxt cons) ctxt rule) prems)
   632 
   633 fun with_cache f proof thm_cache =
   634   (case Thm_Cache.lookup thm_cache (Argo_Proof.id_of proof) of
   635     SOME thm => (thm, thm_cache)
   636   | NONE =>
   637       let val (thm, thm_cache') = f proof thm_cache
   638       in (thm, Thm_Cache.update (Argo_Proof.id_of proof, thm) thm_cache') end)
   639 
   640 fun trace_step ctxt proof_id rule proofs = with_full_tracing ctxt (fn ctxt' =>
   641   let
   642     val id = Argo_Proof.string_of_proof_id proof_id
   643     val ids = map (Argo_Proof.string_of_proof_id o Argo_Proof.id_of) proofs
   644     val rule_string = Argo_Proof.string_of_rule rule
   645   in full_tracing ctxt' ("  " ^ id ^ " <- " ^ space_implode " " ids ^ " . " ^ rule_string) end)
   646 
   647 fun replay_bottom_up (env as (ctxt, _, _)) proof thm_cache =
   648   let
   649     val (proof_id, rule, proofs) = Argo_Proof.dest proof
   650     val (prems, thm_cache) = fold_map (with_cache (replay_bottom_up env)) proofs thm_cache
   651     val _ = trace_step ctxt proof_id rule proofs
   652   in (replay_rule env prems rule, thm_cache) end
   653 
   654 fun replay_proof env proof = with_cache (replay_bottom_up env) proof Thm_Cache.empty
   655 
   656 fun replay ctxt terms facts proof =
   657   let
   658     val env = (ctxt, Termtab.fold (Contab.update o swap) terms Contab.empty, facts)
   659     val _ = tracing ctxt "replaying the proof"
   660     val ({elapsed=t, ...}, ((thm, _), _)) = Timing.timing (replay_proof env) proof
   661     val _ = tracing ctxt ("replayed the proof in " ^ string_of_int (Time.toMilliseconds t) ^ " ms")
   662   in thm end
   663 
   664 
   665 (* normalizing goals *)
   666 
   667 fun instantiate_elim_rule thm =
   668   let val ct = Drule.strip_imp_concl (Thm.cprop_of thm)
   669   in
   670     (case Thm.term_of ct of
   671       @{const HOL.Trueprop} $ Var (_, @{typ HOL.bool}) =>
   672         instantiate (Thm.dest_arg ct) @{cterm HOL.False} thm
   673     | Var _ => instantiate ct @{cprop HOL.False} thm
   674     | _ => thm)
   675   end
   676 
   677 fun atomize_conv ctxt ct =
   678   (case Thm.term_of ct of
   679     @{const HOL.Trueprop} $ _ => Conv.all_conv
   680   | @{const Pure.imp} $ _ $ _ =>
   681       Conv.binop_conv (atomize_conv ctxt) then_conv
   682       Conv.rewr_conv @{thm atomize_imp}
   683   | Const (@{const_name Pure.eq}, _) $ _ $ _ =>
   684       Conv.binop_conv (atomize_conv ctxt) then_conv
   685       Conv.rewr_conv @{thm atomize_eq}
   686   | Const (@{const_name Pure.all}, _) $ Abs _ =>
   687       Conv.binder_conv (atomize_conv o snd) ctxt then_conv
   688       Conv.rewr_conv @{thm atomize_all}
   689   | _ => Conv.all_conv) ct
   690 
   691 fun normalize ctxt thm =
   692   thm
   693   |> instantiate_elim_rule
   694   |> Conv.fconv_rule (Thm.beta_conversion true then_conv Thm.eta_conversion)
   695   |> Drule.forall_intr_vars
   696   |> Conv.fconv_rule (atomize_conv ctxt)
   697 
   698 
   699 (* prover, tactic and method *)
   700 
   701 datatype result = Satisfiable of term -> bool option | Unsatisfiable
   702 
   703 fun check props ctxt =
   704   (case solve props ctxt of
   705     (Proof _, ctxt') => (Unsatisfiable, ctxt')
   706   | (Model model, ctxt') => (Satisfiable model, ctxt'))
   707 
   708 fun prove thms ctxt =
   709   let val thms' = map (normalize ctxt) thms
   710   in
   711     (case solve (map Thm.prop_of thms') ctxt of
   712       (Model _, ctxt') => (NONE, ctxt')
   713     | (Proof (terms, proof), ctxt') => (SOME (replay ctxt' terms thms' proof), ctxt'))
   714   end
   715 
   716 fun argo_tac ctxt thms =
   717   CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1
   718     (Conv.try_conv (Conv.rewr_conv @{thm atomize_eq})))) ctxt)
   719   THEN' Tactic.resolve_tac ctxt [@{thm ccontr}]
   720   THEN' Subgoal.FOCUS (fn {context, prems, ...} =>
   721     (case with_timeout context (prove (thms @ prems)) context of
   722       (SOME thm, _) => Tactic.resolve_tac context [thm] 1
   723     | (NONE, _) => Tactical.no_tac)) ctxt
   724 
   725 val _ =
   726   Theory.setup (Method.setup @{binding argo}
   727     (Scan.optional Attrib.thms [] >>
   728       (fn thms => fn ctxt => METHOD (fn facts =>
   729         HEADGOAL (argo_tac ctxt (thms @ facts)))))
   730     "Applies the Argo prover")
   731 
   732 end