src/HOL/Tools/Metis/metis_reconstruct.ML
author blanchet
Wed, 01 Jun 2011 10:29:43 +0200
changeset 43969 a19826080596
parent 43947 6ec2a3c7b69e
child 43971 d73fc2e55308
permissions -rw-r--r--
tuned names
blanchet@40139
     1
(*  Title:      HOL/Tools/Metis/metis_reconstruct.ML
blanchet@39735
     2
    Author:     Kong W. Susanto, Cambridge University Computer Laboratory
blanchet@39735
     3
    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
blanchet@39735
     4
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@39735
     5
    Copyright   Cambridge University 2007
blanchet@39735
     6
blanchet@39735
     7
Proof reconstruction for Metis.
blanchet@39735
     8
*)
blanchet@39735
     9
blanchet@39735
    10
signature METIS_RECONSTRUCT =
blanchet@39735
    11
sig
blanchet@39737
    12
  type mode = Metis_Translate.mode
blanchet@39737
    13
blanchet@43521
    14
  exception METIS of string * string
blanchet@43521
    15
blanchet@40159
    16
  val trace : bool Config.T
blanchet@40159
    17
  val trace_msg : Proof.context -> (unit -> string) -> unit
blanchet@40913
    18
  val verbose : bool Config.T
blanchet@40913
    19
  val verbose_warning : Proof.context -> string -> unit
blanchet@43969
    20
  val hol_term_from_metis :
blanchet@43969
    21
    mode -> int Symtab.table -> Proof.context -> Metis_Term.term -> term
blanchet@39737
    22
  val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
blanchet@40068
    23
  val untyped_aconv : term -> term -> bool
blanchet@39737
    24
  val replay_one_inference :
blanchet@43935
    25
    Proof.context -> mode -> (string * term) list -> int Symtab.table
blanchet@39737
    26
    -> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list
blanchet@39737
    27
    -> (Metis_Thm.thm * thm) list
blanchet@40145
    28
  val discharge_skolem_premises :
blanchet@40145
    29
    Proof.context -> (thm * term) option list -> thm -> thm
blanchet@39735
    30
end;
blanchet@39735
    31
blanchet@39735
    32
structure Metis_Reconstruct : METIS_RECONSTRUCT =
blanchet@39735
    33
struct
blanchet@39735
    34
blanchet@43935
    35
open ATP_Problem
blanchet@43926
    36
open ATP_Translate
blanchet@43935
    37
open ATP_Reconstruct
blanchet@39737
    38
open Metis_Translate
blanchet@39737
    39
blanchet@43521
    40
exception METIS of string * string
blanchet@43521
    41
wenzelm@43487
    42
val trace = Attrib.setup_config_bool @{binding metis_trace} (K false)
wenzelm@43487
    43
val verbose = Attrib.setup_config_bool @{binding metis_verbose} (K true)
blanchet@40159
    44
blanchet@40159
    45
fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
blanchet@40913
    46
fun verbose_warning ctxt msg =
blanchet@43521
    47
  if Config.get ctxt verbose then warning ("Metis: " ^ msg) else ()
blanchet@39737
    48
blanchet@39738
    49
datatype term_or_type = SomeTerm of term | SomeType of typ
blanchet@39737
    50
blanchet@39737
    51
fun terms_of [] = []
blanchet@39738
    52
  | terms_of (SomeTerm t :: tts) = t :: terms_of tts
blanchet@39738
    53
  | terms_of (SomeType _ :: tts) = terms_of tts;
blanchet@39737
    54
blanchet@39737
    55
fun types_of [] = []
blanchet@39738
    56
  | types_of (SomeTerm (Var ((a,idx), _)) :: tts) =
blanchet@42962
    57
      if String.isPrefix metis_generated_var_prefix a then
blanchet@39737
    58
          (*Variable generated by Metis, which might have been a type variable.*)
blanchet@39737
    59
          TVar (("'" ^ a, idx), HOLogic.typeS) :: types_of tts
blanchet@39737
    60
      else types_of tts
blanchet@39738
    61
  | types_of (SomeTerm _ :: tts) = types_of tts
blanchet@39738
    62
  | types_of (SomeType T :: tts) = T :: types_of tts;
blanchet@39737
    63
blanchet@39737
    64
fun apply_list rator nargs rands =
blanchet@39737
    65
  let val trands = terms_of rands
blanchet@39738
    66
  in  if length trands = nargs then SomeTerm (list_comb(rator, trands))
blanchet@39737
    67
      else raise Fail
blanchet@39737
    68
        ("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global Pure.thy rator ^
wenzelm@41739
    69
          " expected " ^ string_of_int nargs ^
blanchet@39737
    70
          " received " ^ commas (map (Syntax.string_of_term_global Pure.thy) trands))
blanchet@39737
    71
  end;
blanchet@39737
    72
blanchet@39737
    73
fun infer_types ctxt =
wenzelm@43232
    74
  Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt);
blanchet@39737
    75
blanchet@43935
    76
(* We use 1 rather than 0 because variable references in clauses may otherwise
blanchet@43935
    77
   conflict with variable constraints in the goal...at least, type inference
blanchet@43935
    78
   often fails otherwise. See also "axiom_inf" below. *)
blanchet@39738
    79
fun mk_var (w, T) = Var ((w, 1), T)
blanchet@39737
    80
blanchet@39737
    81
(*include the default sort, if available*)
blanchet@39737
    82
fun mk_tfree ctxt w =
blanchet@39737
    83
  let val ww = "'" ^ w
blanchet@39737
    84
  in  TFree(ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1)))  end;
blanchet@39737
    85
blanchet@39737
    86
(*Remove the "apply" operator from an HO term*)
blanchet@43935
    87
fun strip_happ args (Metis_Term.Fn (".", [t, u])) = strip_happ (u :: args) t
blanchet@43935
    88
  | strip_happ args x = (x, args)
blanchet@39737
    89
blanchet@39737
    90
fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS)
blanchet@39737
    91
blanchet@39737
    92
fun hol_type_from_metis_term _ (Metis_Term.Var v) =
blanchet@39737
    93
     (case strip_prefix_and_unascii tvar_prefix v of
blanchet@39737
    94
          SOME w => make_tvar w
blanchet@39737
    95
        | NONE   => make_tvar v)
blanchet@39737
    96
  | hol_type_from_metis_term ctxt (Metis_Term.Fn(x, tys)) =
blanchet@39737
    97
     (case strip_prefix_and_unascii type_const_prefix x of
blanchet@41388
    98
          SOME tc => Type (invert_const tc,
blanchet@39738
    99
                           map (hol_type_from_metis_term ctxt) tys)
blanchet@39737
   100
        | NONE    =>
blanchet@39737
   101
      case strip_prefix_and_unascii tfree_prefix x of
blanchet@39737
   102
          SOME tf => mk_tfree ctxt tf
blanchet@39737
   103
        | NONE    => raise Fail ("hol_type_from_metis_term: " ^ x));
blanchet@39737
   104
blanchet@39737
   105
(*Maps metis terms to isabelle terms*)
blanchet@43212
   106
fun hol_term_from_metis_PT ctxt fol_tm =
wenzelm@43232
   107
  let val thy = Proof_Context.theory_of ctxt
blanchet@40159
   108
      val _ = trace_msg ctxt (fn () => "hol_term_from_metis_PT: " ^
blanchet@40159
   109
                                       Metis_Term.toString fol_tm)
blanchet@39737
   110
      fun tm_to_tt (Metis_Term.Var v) =
blanchet@39737
   111
             (case strip_prefix_and_unascii tvar_prefix v of
blanchet@39738
   112
                  SOME w => SomeType (make_tvar w)
blanchet@39737
   113
                | NONE =>
blanchet@39737
   114
              case strip_prefix_and_unascii schematic_var_prefix v of
blanchet@39738
   115
                  SOME w => SomeTerm (mk_var (w, HOLogic.typeT))
blanchet@43134
   116
                | NONE   => SomeTerm (mk_var (v, HOLogic.typeT)))
blanchet@39737
   117
                    (*Var from Metis with a name like _nnn; possibly a type variable*)
blanchet@39737
   118
        | tm_to_tt (Metis_Term.Fn ("{}", [arg])) = tm_to_tt arg   (*hBOOL*)
blanchet@43935
   119
        | tm_to_tt (t as Metis_Term.Fn (".", _)) =
blanchet@43935
   120
            let val (rator,rands) = strip_happ [] t in
blanchet@43935
   121
              case rator of
blanchet@43935
   122
                Metis_Term.Fn(fname,ts) => applic_to_tt (fname, ts @ rands)
blanchet@43935
   123
              | _ => case tm_to_tt rator of
blanchet@43935
   124
                         SomeTerm t => SomeTerm (list_comb(t, terms_of (map tm_to_tt rands)))
blanchet@43935
   125
                       | _ => raise Fail "tm_to_tt: HO application"
blanchet@39737
   126
            end
blanchet@39737
   127
        | tm_to_tt (Metis_Term.Fn (fname, args)) = applic_to_tt (fname,args)
blanchet@39737
   128
      and applic_to_tt ("=",ts) =
blanchet@39738
   129
            SomeTerm (list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
blanchet@39737
   130
        | applic_to_tt (a,ts) =
blanchet@39737
   131
            case strip_prefix_and_unascii const_prefix a of
blanchet@39737
   132
                SOME b =>
blanchet@40067
   133
                  let
blanchet@43441
   134
                    val c = b |> invert_const |> unproxify_const
blanchet@40067
   135
                    val ntypes = num_type_args thy c
blanchet@40067
   136
                    val nterms = length ts - ntypes
blanchet@40067
   137
                    val tts = map tm_to_tt ts
blanchet@40067
   138
                    val tys = types_of (List.take(tts,ntypes))
blanchet@40120
   139
                    val t =
blanchet@40120
   140
                      if String.isPrefix new_skolem_const_prefix c then
blanchet@43212
   141
                        Var ((new_skolem_var_name_from_const c, 1),
blanchet@40120
   142
                             Type_Infer.paramify_vars (tl tys ---> hd tys))
blanchet@40120
   143
                      else
blanchet@40120
   144
                        Const (c, dummyT)
blanchet@39737
   145
                  in if length tys = ntypes then
blanchet@40067
   146
                         apply_list t nterms (List.drop(tts,ntypes))
blanchet@39737
   147
                     else
wenzelm@41739
   148
                       raise Fail ("Constant " ^ c ^ " expects " ^ string_of_int ntypes ^
wenzelm@41739
   149
                                   " but gets " ^ string_of_int (length tys) ^
blanchet@39737
   150
                                   " type arguments\n" ^
blanchet@39737
   151
                                   cat_lines (map (Syntax.string_of_typ ctxt) tys) ^
blanchet@39737
   152
                                   " the terms are \n" ^
blanchet@39737
   153
                                   cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
blanchet@39737
   154
                     end
blanchet@39737
   155
              | NONE => (*Not a constant. Is it a type constructor?*)
blanchet@39737
   156
            case strip_prefix_and_unascii type_const_prefix a of
blanchet@39737
   157
                SOME b =>
blanchet@41388
   158
                SomeType (Type (invert_const b, types_of (map tm_to_tt ts)))
blanchet@39737
   159
              | NONE => (*Maybe a TFree. Should then check that ts=[].*)
blanchet@39737
   160
            case strip_prefix_and_unascii tfree_prefix a of
blanchet@39738
   161
                SOME b => SomeType (mk_tfree ctxt b)
blanchet@39737
   162
              | NONE => (*a fixed variable? They are Skolem functions.*)
blanchet@39737
   163
            case strip_prefix_and_unascii fixed_var_prefix a of
blanchet@39737
   164
                SOME b =>
blanchet@39738
   165
                  let val opr = Free (b, HOLogic.typeT)
blanchet@39737
   166
                  in  apply_list opr (length ts) (map tm_to_tt ts)  end
blanchet@39737
   167
              | NONE => raise Fail ("unexpected metis function: " ^ a)
blanchet@39737
   168
  in
blanchet@39737
   169
    case tm_to_tt fol_tm of
blanchet@39738
   170
      SomeTerm t => t
blanchet@39738
   171
    | SomeType T => raise TYPE ("fol_tm_to_tt: Term expected", [T], [])
blanchet@39737
   172
  end
blanchet@39737
   173
blanchet@39737
   174
(*Maps fully-typed metis terms to isabelle terms*)
blanchet@43212
   175
fun hol_term_from_metis_FT ctxt fol_tm =
blanchet@40159
   176
  let val _ = trace_msg ctxt (fn () => "hol_term_from_metis_FT: " ^
blanchet@40159
   177
                                       Metis_Term.toString fol_tm)
blanchet@43208
   178
      fun do_const c =
blanchet@43441
   179
        let val c = c |> invert_const |> unproxify_const in
blanchet@43208
   180
          if String.isPrefix new_skolem_const_prefix c then
blanchet@43208
   181
            Var ((new_skolem_var_name_from_const c, 1), dummyT)
blanchet@43208
   182
          else
blanchet@43208
   183
            Const (c, dummyT)
blanchet@43208
   184
        end
blanchet@43945
   185
      fun cvt (Metis_Term.Fn (":", [Metis_Term.Var v, _])) =
blanchet@39737
   186
             (case strip_prefix_and_unascii schematic_var_prefix v of
blanchet@39737
   187
                  SOME w =>  mk_var(w, dummyT)
blanchet@39737
   188
                | NONE   => mk_var(v, dummyT))
blanchet@43945
   189
        | cvt (Metis_Term.Fn (":", [Metis_Term.Fn ("=",[]), _])) =
blanchet@39737
   190
            Const (@{const_name HOL.eq}, HOLogic.typeT)
blanchet@43945
   191
        | cvt (Metis_Term.Fn (":", [Metis_Term.Fn (x,[]), ty])) =
blanchet@39737
   192
           (case strip_prefix_and_unascii const_prefix x of
blanchet@43208
   193
                SOME c => do_const c
blanchet@39737
   194
              | NONE => (*Not a constant. Is it a fixed variable??*)
blanchet@39737
   195
            case strip_prefix_and_unascii fixed_var_prefix x of
blanchet@39737
   196
                SOME v => Free (v, hol_type_from_metis_term ctxt ty)
blanchet@39737
   197
              | NONE => raise Fail ("hol_term_from_metis_FT bad constant: " ^ x))
blanchet@43945
   198
        | cvt (Metis_Term.Fn (":", [Metis_Term.Fn (".", [tm1,tm2]), _])) =
blanchet@39737
   199
            cvt tm1 $ cvt tm2
blanchet@39737
   200
        | cvt (Metis_Term.Fn (".",[tm1,tm2])) = (*untyped application*)
blanchet@39737
   201
            cvt tm1 $ cvt tm2
blanchet@39737
   202
        | cvt (Metis_Term.Fn ("{}", [arg])) = cvt arg   (*hBOOL*)
blanchet@39737
   203
        | cvt (Metis_Term.Fn ("=", [tm1,tm2])) =
blanchet@39737
   204
            list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), map cvt [tm1,tm2])
blanchet@39737
   205
        | cvt (t as Metis_Term.Fn (x, [])) =
blanchet@39737
   206
           (case strip_prefix_and_unascii const_prefix x of
blanchet@43208
   207
                SOME c => do_const c
blanchet@39737
   208
              | NONE => (*Not a constant. Is it a fixed variable??*)
blanchet@39737
   209
            case strip_prefix_and_unascii fixed_var_prefix x of
blanchet@39737
   210
                SOME v => Free (v, dummyT)
blanchet@40159
   211
              | NONE => (trace_msg ctxt (fn () =>
blanchet@40159
   212
                                      "hol_term_from_metis_FT bad const: " ^ x);
blanchet@43212
   213
                         hol_term_from_metis_PT ctxt t))
blanchet@40159
   214
        | cvt t = (trace_msg ctxt (fn () =>
blanchet@40159
   215
                   "hol_term_from_metis_FT bad term: " ^ Metis_Term.toString t);
blanchet@43212
   216
                   hol_term_from_metis_PT ctxt t)
blanchet@39737
   217
  in fol_tm |> cvt end
blanchet@39737
   218
blanchet@43935
   219
fun atp_name_from_metis s =
blanchet@43945
   220
  case find_first (fn (_, (s', _)) => s' = s) metis_name_table of
blanchet@43945
   221
    SOME ((s, _), (_, swap)) => (s, swap)
blanchet@43945
   222
  | _ => (s, false)
blanchet@43935
   223
fun atp_term_from_metis (Metis_Term.Fn (s, tms)) =
blanchet@43945
   224
    let val (s, swap) = atp_name_from_metis s in
blanchet@43945
   225
      ATerm (s, tms |> map atp_term_from_metis |> swap ? rev)
blanchet@43945
   226
    end
blanchet@43935
   227
  | atp_term_from_metis (Metis_Term.Var s) = ATerm (s, [])
blanchet@39737
   228
blanchet@43944
   229
fun hol_term_from_metis_MX sym_tab ctxt =
blanchet@43935
   230
  let val thy = Proof_Context.theory_of ctxt in
blanchet@43944
   231
    atp_term_from_metis #> term_from_atp thy false sym_tab []
blanchet@43944
   232
    (* FIXME ### tfrees instead of []? *) NONE
blanchet@43935
   233
  end
blanchet@43935
   234
blanchet@43935
   235
fun hol_term_from_metis FO _ = hol_term_from_metis_PT
blanchet@43935
   236
  | hol_term_from_metis HO _ = hol_term_from_metis_PT
blanchet@43935
   237
  | hol_term_from_metis FT _ = hol_term_from_metis_FT
blanchet@43944
   238
  | hol_term_from_metis MX sym_tab = hol_term_from_metis_MX sym_tab
blanchet@43935
   239
blanchet@43935
   240
fun hol_terms_from_metis ctxt mode old_skolems sym_tab fol_tms =
blanchet@43935
   241
  let val ts = map (hol_term_from_metis mode sym_tab ctxt) fol_tms
blanchet@40159
   242
      val _ = trace_msg ctxt (fn () => "  calling type inference:")
blanchet@40159
   243
      val _ = app (fn t => trace_msg ctxt
blanchet@40159
   244
                                     (fn () => Syntax.string_of_term ctxt t)) ts
blanchet@40067
   245
      val ts' = ts |> map (reveal_old_skolem_terms old_skolems)
blanchet@40067
   246
                   |> infer_types ctxt
blanchet@40159
   247
      val _ = app (fn t => trace_msg ctxt
blanchet@39737
   248
                    (fn () => "  final term: " ^ Syntax.string_of_term ctxt t ^
blanchet@43969
   249
                              " of type " ^ Syntax.string_of_typ ctxt (type_of t)))
blanchet@39737
   250
                  ts'
blanchet@39737
   251
  in  ts'  end;
blanchet@39737
   252
blanchet@39737
   253
(* ------------------------------------------------------------------------- *)
blanchet@39737
   254
(* FOL step Inference Rules                                                  *)
blanchet@39737
   255
(* ------------------------------------------------------------------------- *)
blanchet@39737
   256
blanchet@39737
   257
(*for debugging only*)
blanchet@39737
   258
(*
blanchet@40159
   259
fun print_thpair ctxt (fth,th) =
blanchet@40159
   260
  (trace_msg ctxt (fn () => "=============================================");
blanchet@40159
   261
   trace_msg ctxt (fn () => "Metis: " ^ Metis_Thm.toString fth);
blanchet@40159
   262
   trace_msg ctxt (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th));
blanchet@39737
   263
*)
blanchet@39737
   264
blanchet@43935
   265
fun lookth th_pairs fth =
blanchet@43935
   266
  the (AList.lookup (uncurry Metis_Thm.equal) th_pairs fth)
blanchet@39737
   267
  handle Option.Option =>
blanchet@39737
   268
         raise Fail ("Failed to find Metis theorem " ^ Metis_Thm.toString fth)
blanchet@39737
   269
blanchet@39737
   270
fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx));
blanchet@39737
   271
blanchet@39737
   272
(* INFERENCE RULE: AXIOM *)
blanchet@39737
   273
blanchet@43935
   274
(* This causes variables to have an index of 1 by default. See also "mk_var"
blanchet@43935
   275
   above. *)
blanchet@43935
   276
fun axiom_inf th_pairs th = Thm.incr_indexes 1 (lookth th_pairs th)
blanchet@39737
   277
blanchet@39737
   278
(* INFERENCE RULE: ASSUME *)
blanchet@39737
   279
blanchet@39737
   280
val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)}
blanchet@39737
   281
blanchet@39737
   282
fun inst_excluded_middle thy i_atm =
blanchet@39737
   283
  let val th = EXCLUDED_MIDDLE
blanchet@39737
   284
      val [vx] = Term.add_vars (prop_of th) []
blanchet@39737
   285
      val substs = [(cterm_of thy (Var vx), cterm_of thy i_atm)]
blanchet@39737
   286
  in  cterm_instantiate substs th  end;
blanchet@39737
   287
blanchet@43935
   288
fun assume_inf ctxt mode old_skolems sym_tab atm =
blanchet@39737
   289
  inst_excluded_middle
wenzelm@43232
   290
      (Proof_Context.theory_of ctxt)
blanchet@43935
   291
      (singleton (hol_terms_from_metis ctxt mode old_skolems sym_tab)
blanchet@40502
   292
                 (Metis_Term.Fn atm))
blanchet@39737
   293
blanchet@39738
   294
(* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying
blanchet@39737
   295
   to reconstruct them admits new possibilities of errors, e.g. concerning
blanchet@39737
   296
   sorts. Instead we try to arrange that new TVars are distinct and that types
blanchet@39738
   297
   can be inferred from terms. *)
blanchet@39737
   298
blanchet@43935
   299
fun inst_inf ctxt mode old_skolems sym_tab th_pairs fsubst th =
wenzelm@43232
   300
  let val thy = Proof_Context.theory_of ctxt
blanchet@43935
   301
      val i_th = lookth th_pairs th
blanchet@39737
   302
      val i_th_vars = Term.add_vars (prop_of i_th) []
blanchet@39737
   303
      fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars)
blanchet@39737
   304
      fun subst_translation (x,y) =
blanchet@39738
   305
        let val v = find_var x
blanchet@40067
   306
            (* We call "reveal_old_skolem_terms" and "infer_types" below. *)
blanchet@43935
   307
            val t = hol_term_from_metis mode sym_tab ctxt y
blanchet@39738
   308
        in  SOME (cterm_of thy (Var v), t)  end
blanchet@39738
   309
        handle Option.Option =>
blanchet@40159
   310
               (trace_msg ctxt (fn () => "\"find_var\" failed for " ^ x ^
blanchet@40159
   311
                                         " in " ^ Display.string_of_thm ctxt i_th);
blanchet@39738
   312
                NONE)
blanchet@39738
   313
             | TYPE _ =>
blanchet@40159
   314
               (trace_msg ctxt (fn () => "\"hol_term_from_metis\" failed for " ^ x ^
blanchet@40159
   315
                                         " in " ^ Display.string_of_thm ctxt i_th);
blanchet@39738
   316
                NONE)
blanchet@39737
   317
      fun remove_typeinst (a, t) =
blanchet@39737
   318
            case strip_prefix_and_unascii schematic_var_prefix a of
blanchet@39737
   319
                SOME b => SOME (b, t)
blanchet@39737
   320
              | NONE => case strip_prefix_and_unascii tvar_prefix a of
blanchet@39737
   321
                SOME _ => NONE          (*type instantiations are forbidden!*)
blanchet@39737
   322
              | NONE => SOME (a,t)    (*internal Metis var?*)
blanchet@40159
   323
      val _ = trace_msg ctxt (fn () => "  isa th: " ^ Display.string_of_thm ctxt i_th)
blanchet@39737
   324
      val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst)
blanchet@39737
   325
      val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs)
blanchet@40067
   326
      val tms = rawtms |> map (reveal_old_skolem_terms old_skolems)
blanchet@40067
   327
                       |> infer_types ctxt
blanchet@39737
   328
      val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
blanchet@39737
   329
      val substs' = ListPair.zip (vars, map ctm_of tms)
blanchet@40159
   330
      val _ = trace_msg ctxt (fn () =>
blanchet@39737
   331
        cat_lines ("subst_translations:" ::
blanchet@39737
   332
          (substs' |> map (fn (x, y) =>
blanchet@39737
   333
            Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
blanchet@39737
   334
            Syntax.string_of_term ctxt (term_of y)))));
blanchet@39737
   335
  in cterm_instantiate substs' i_th end
blanchet@43521
   336
  handle THM (msg, _, _) => raise METIS ("inst_inf", msg)
blanchet@43521
   337
       | ERROR msg => raise METIS ("inst_inf", msg)
blanchet@39737
   338
blanchet@39737
   339
(* INFERENCE RULE: RESOLVE *)
blanchet@39737
   340
blanchet@39737
   341
(* Like RSN, but we rename apart only the type variables. Vars here typically
blanchet@39737
   342
   have an index of 1, and the use of RSN would increase this typically to 3.
blanchet@39737
   343
   Instantiations of those Vars could then fail. See comment on "mk_var". *)
blanchet@39737
   344
fun resolve_inc_tyvars thy tha i thb =
blanchet@39737
   345
  let
blanchet@39737
   346
    val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
blanchet@39737
   347
    fun aux tha thb =
blanchet@39737
   348
      case Thm.bicompose false (false, tha, nprems_of tha) i thb
blanchet@39737
   349
           |> Seq.list_of |> distinct Thm.eq_thm of
blanchet@39737
   350
        [th] => th
blanchet@39737
   351
      | _ => raise THM ("resolve_inc_tyvars: unique result expected", i,
blanchet@39737
   352
                        [tha, thb])
blanchet@39737
   353
  in
blanchet@39737
   354
    aux tha thb
blanchet@39737
   355
    handle TERM z =>
blanchet@39737
   356
           (* The unifier, which is invoked from "Thm.bicompose", will sometimes
blanchet@39737
   357
              refuse to unify "?a::?'a" with "?a::?'b" or "?a::nat" and throw a
blanchet@39737
   358
              "TERM" exception (with "add_ffpair" as first argument). We then
blanchet@39737
   359
              perform unification of the types of variables by hand and try
blanchet@39737
   360
              again. We could do this the first time around but this error
blanchet@39737
   361
              occurs seldom and we don't want to break existing proofs in subtle
blanchet@39737
   362
              ways or slow them down needlessly. *)
blanchet@39737
   363
           case [] |> fold (Term.add_vars o prop_of) [tha, thb]
blanchet@39737
   364
                   |> AList.group (op =)
blanchet@39737
   365
                   |> maps (fn ((s, _), T :: Ts) =>
blanchet@39737
   366
                               map (fn T' => (Free (s, T), Free (s, T'))) Ts)
blanchet@39737
   367
                   |> rpair (Envir.empty ~1)
blanchet@39737
   368
                   |-> fold (Pattern.unify thy)
blanchet@39737
   369
                   |> Envir.type_env |> Vartab.dest
blanchet@39737
   370
                   |> map (fn (x, (S, T)) =>
blanchet@39737
   371
                              pairself (ctyp_of thy) (TVar (x, S), T)) of
blanchet@39737
   372
             [] => raise TERM z
blanchet@39737
   373
           | ps => aux (instantiate (ps, []) tha) (instantiate (ps, []) thb)
blanchet@39737
   374
  end
blanchet@39737
   375
blanchet@40462
   376
fun s_not (@{const Not} $ t) = t
blanchet@40462
   377
  | s_not t = HOLogic.mk_not t
blanchet@40462
   378
fun simp_not_not (@{const Not} $ t) = s_not (simp_not_not t)
blanchet@40462
   379
  | simp_not_not t = t
blanchet@39737
   380
blanchet@39737
   381
(* Match untyped terms. *)
blanchet@39737
   382
fun untyped_aconv (Const (a, _)) (Const(b, _)) = (a = b)
blanchet@39737
   383
  | untyped_aconv (Free (a, _)) (Free (b, _)) = (a = b)
blanchet@39737
   384
  | untyped_aconv (Var ((a, _), _)) (Var ((b, _), _)) =
blanchet@39737
   385
    (a = b) (* The index is ignored, for some reason. *)
blanchet@39737
   386
  | untyped_aconv (Bound i) (Bound j) = (i = j)
blanchet@39737
   387
  | untyped_aconv (Abs (_, _, t)) (Abs (_, _, u)) = untyped_aconv t u
blanchet@39737
   388
  | untyped_aconv (t1 $ t2) (u1 $ u2) =
blanchet@39737
   389
    untyped_aconv t1 u1 andalso untyped_aconv t2 u2
blanchet@39737
   390
  | untyped_aconv _ _ = false
blanchet@39737
   391
blanchet@39737
   392
(* Finding the relative location of an untyped term within a list of terms *)
blanchet@40462
   393
fun index_of_literal lit haystack =
blanchet@39737
   394
  let
blanchet@40462
   395
    val normalize = simp_not_not o Envir.eta_contract
blanchet@40462
   396
    val match_lit =
blanchet@40462
   397
      HOLogic.dest_Trueprop #> normalize #> untyped_aconv (lit |> normalize)
blanchet@40462
   398
  in case find_index match_lit haystack of ~1 => raise Empty | n => n + 1 end
blanchet@39737
   399
blanchet@40074
   400
(* Permute a rule's premises to move the i-th premise to the last position. *)
blanchet@40074
   401
fun make_last i th =
blanchet@40074
   402
  let val n = nprems_of th
blanchet@40074
   403
  in  if 1 <= i andalso i <= n
blanchet@40074
   404
      then Thm.permute_prems (i-1) 1 th
blanchet@40074
   405
      else raise THM("select_literal", i, [th])
blanchet@40074
   406
  end;
blanchet@40074
   407
blanchet@43219
   408
(* Maps a rule that ends "... ==> P ==> False" to "... ==> ~ P" while avoiding
blanchet@43220
   409
   to create double negations. The "select" wrapper is a trick to ensure that
blanchet@43220
   410
   "P ==> ~ False ==> False" is rewritten to "P ==> False", not to "~ P". We
blanchet@43220
   411
   don't use this trick in general because it makes the proof object uglier than
blanchet@43220
   412
   necessary. FIXME. *)
blanchet@43220
   413
fun negate_head th =
blanchet@43220
   414
  if exists (fn t => t aconv @{prop "~ False"}) (prems_of th) then
blanchet@43220
   415
    (th RS @{thm select_FalseI})
blanchet@43220
   416
    |> fold (rewrite_rule o single)
blanchet@43220
   417
            @{thms not_atomize_select atomize_not_select}
blanchet@43220
   418
  else
blanchet@43220
   419
    th |> fold (rewrite_rule o single) @{thms not_atomize atomize_not}
blanchet@40074
   420
blanchet@40074
   421
(* Maps the clause  [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *)
blanchet@43219
   422
val select_literal = negate_head oo make_last
blanchet@40074
   423
blanchet@43935
   424
fun resolve_inf ctxt mode old_skolems sym_tab th_pairs atm th1 th2 =
blanchet@39737
   425
  let
wenzelm@43232
   426
    val thy = Proof_Context.theory_of ctxt
blanchet@43935
   427
    val (i_th1, i_th2) = pairself (lookth th_pairs) (th1, th2)
blanchet@40159
   428
    val _ = trace_msg ctxt (fn () => "  isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
blanchet@40159
   429
    val _ = trace_msg ctxt (fn () => "  isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
blanchet@39737
   430
  in
blanchet@39737
   431
    (* Trivial cases where one operand is type info *)
blanchet@39737
   432
    if Thm.eq_thm (TrueI, i_th1) then
blanchet@39737
   433
      i_th2
blanchet@39737
   434
    else if Thm.eq_thm (TrueI, i_th2) then
blanchet@39737
   435
      i_th1
blanchet@39737
   436
    else
blanchet@39737
   437
      let
blanchet@40462
   438
        val i_atm =
blanchet@43935
   439
          singleton (hol_terms_from_metis ctxt mode old_skolems sym_tab)
blanchet@40462
   440
                    (Metis_Term.Fn atm)
blanchet@40159
   441
        val _ = trace_msg ctxt (fn () => "  atom: " ^ Syntax.string_of_term ctxt i_atm)
blanchet@39737
   442
        val prems_th1 = prems_of i_th1
blanchet@39737
   443
        val prems_th2 = prems_of i_th2
blanchet@40462
   444
        val index_th1 =
blanchet@40462
   445
          index_of_literal (s_not i_atm) prems_th1
blanchet@40462
   446
          handle Empty => raise Fail "Failed to find literal in th1"
wenzelm@41739
   447
        val _ = trace_msg ctxt (fn () => "  index_th1: " ^ string_of_int index_th1)
blanchet@40462
   448
        val index_th2 =
blanchet@40462
   449
          index_of_literal i_atm prems_th2
blanchet@40462
   450
          handle Empty => raise Fail "Failed to find literal in th2"
wenzelm@41739
   451
        val _ = trace_msg ctxt (fn () => "  index_th2: " ^ string_of_int index_th2)
blanchet@39737
   452
    in
blanchet@43219
   453
      resolve_inc_tyvars thy (select_literal index_th1 i_th1) index_th2 i_th2
blanchet@43521
   454
      handle TERM (s, _) => raise METIS ("resolve_inf", s)
blanchet@39737
   455
    end
blanchet@39737
   456
  end;
blanchet@39737
   457
blanchet@39737
   458
(* INFERENCE RULE: REFL *)
blanchet@39737
   459
blanchet@39737
   460
val REFL_THM = Thm.incr_indexes 2 @{lemma "t ~= t ==> False" by simp}
blanchet@39737
   461
blanchet@39737
   462
val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
blanchet@39737
   463
val refl_idx = 1 + Thm.maxidx_of REFL_THM;
blanchet@39737
   464
blanchet@43935
   465
fun refl_inf ctxt mode old_skolems sym_tab t =
blanchet@43935
   466
  let
blanchet@43935
   467
    val thy = Proof_Context.theory_of ctxt
blanchet@43935
   468
    val i_t = singleton (hol_terms_from_metis ctxt mode old_skolems sym_tab) t
blanchet@43935
   469
    val _ = trace_msg ctxt (fn () => "  term: " ^ Syntax.string_of_term ctxt i_t)
blanchet@43935
   470
    val c_t = cterm_incr_types thy refl_idx i_t
blanchet@43935
   471
  in cterm_instantiate [(refl_x, c_t)] REFL_THM end
blanchet@39737
   472
blanchet@39737
   473
(* INFERENCE RULE: EQUALITY *)
blanchet@39737
   474
blanchet@39737
   475
val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp}
blanchet@39737
   476
val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp}
blanchet@39737
   477
blanchet@39737
   478
val metis_eq = Metis_Term.Fn ("=", []);
blanchet@39737
   479
blanchet@43934
   480
(* Equality has no type arguments *)
blanchet@43934
   481
fun get_ty_arg_size _ (Const (@{const_name HOL.eq}, _)) = 0
blanchet@43934
   482
  | get_ty_arg_size thy (Const (s, _)) =
blanchet@43934
   483
    (num_type_args thy s handle TYPE _ => 0)
blanchet@43934
   484
  | get_ty_arg_size _ _ = 0
blanchet@39737
   485
blanchet@43935
   486
fun equality_inf ctxt mode old_skolems sym_tab (pos, atm) fp fr =
wenzelm@43232
   487
  let val thy = Proof_Context.theory_of ctxt
blanchet@39737
   488
      val m_tm = Metis_Term.Fn atm
blanchet@43935
   489
      val [i_atm, i_tm] =
blanchet@43935
   490
        hol_terms_from_metis ctxt mode old_skolems sym_tab [m_tm, fr]
blanchet@40159
   491
      val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Bool.toString pos)
blanchet@39737
   492
      fun replace_item_list lx 0 (_::ls) = lx::ls
blanchet@39737
   493
        | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
blanchet@43945
   494
      fun path_finder_fail mode tm ps t =
blanchet@43945
   495
        raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^
blanchet@43945
   496
                    "equality_inf, path_finder_" ^ string_of_mode mode ^
blanchet@43945
   497
                    ": path = " ^ space_implode " " (map string_of_int ps) ^
blanchet@43945
   498
                    " isa-term: " ^ Syntax.string_of_term ctxt tm ^
blanchet@43945
   499
                    (case t of
blanchet@43945
   500
                       SOME t => " fol-term: " ^ Metis_Term.toString t
blanchet@43945
   501
                     | NONE => ""))
blanchet@39738
   502
      fun path_finder_FO tm [] = (tm, Bound 0)
blanchet@39737
   503
        | path_finder_FO tm (p::ps) =
blanchet@39737
   504
            let val (tm1,args) = strip_comb tm
blanchet@39737
   505
                val adjustment = get_ty_arg_size thy tm1
blanchet@43935
   506
                val p' = if adjustment > p then p else p - adjustment
wenzelm@43235
   507
                val tm_p = nth args p'
blanchet@39737
   508
                  handle Subscript =>
blanchet@43521
   509
                         raise METIS ("equality_inf",
blanchet@43521
   510
                                      string_of_int p ^ " adj " ^
blanchet@43521
   511
                                      string_of_int adjustment ^ " term " ^
blanchet@43521
   512
                                      Syntax.string_of_term ctxt tm)
wenzelm@41739
   513
                val _ = trace_msg ctxt (fn () => "path_finder: " ^ string_of_int p ^
blanchet@39737
   514
                                      "  " ^ Syntax.string_of_term ctxt tm_p)
blanchet@39737
   515
                val (r,t) = path_finder_FO tm_p ps
blanchet@39737
   516
            in
blanchet@39737
   517
                (r, list_comb (tm1, replace_item_list t p' args))
blanchet@39737
   518
            end
blanchet@39738
   519
      fun path_finder_HO tm [] = (tm, Bound 0)
blanchet@39737
   520
        | path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps)
blanchet@39737
   521
        | path_finder_HO (t$u) (_::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps)
blanchet@43945
   522
        | path_finder_HO tm ps = path_finder_fail HO tm ps NONE
blanchet@39738
   523
      fun path_finder_FT tm [] _ = (tm, Bound 0)
blanchet@43945
   524
        | path_finder_FT tm (0::ps) (Metis_Term.Fn (":", [t1, _])) =
blanchet@39737
   525
            path_finder_FT tm ps t1
blanchet@39737
   526
        | path_finder_FT (t$u) (0::ps) (Metis_Term.Fn (".", [t1, _])) =
blanchet@39737
   527
            (fn(x,y) => (x, y$u)) (path_finder_FT t ps t1)
blanchet@39737
   528
        | path_finder_FT (t$u) (1::ps) (Metis_Term.Fn (".", [_, t2])) =
blanchet@39737
   529
            (fn(x,y) => (x, t$y)) (path_finder_FT u ps t2)
blanchet@43945
   530
        | path_finder_FT tm ps t = path_finder_fail FT tm ps (SOME t)
blanchet@43944
   531
      fun path_finder_MX tm [] _ = (tm, Bound 0)
blanchet@43944
   532
        | path_finder_MX tm (p :: ps) (t as Metis_Term.Fn (s, ts)) =
blanchet@43945
   533
          (* FIXME ### what if these are mangled? *) 
blanchet@43945
   534
          if s = metis_type_tag then
blanchet@43947
   535
            if p = 0 then path_finder_MX tm ps (hd ts)
blanchet@43945
   536
            else path_finder_fail MX tm (p :: ps) (SOME t)
blanchet@43945
   537
          else if s = metis_app_op then
blanchet@43938
   538
            let
blanchet@43938
   539
              val (tm1, tm2) = dest_comb tm in
blanchet@43944
   540
              if p = 0 then path_finder_MX tm1 ps (hd ts) ||> (fn y => y $ tm2)
blanchet@43944
   541
              else path_finder_MX tm2 ps (nth ts 1) ||> (fn y => tm1 $ y)
blanchet@43938
   542
            end
blanchet@43938
   543
          else
blanchet@43938
   544
            let
blanchet@43938
   545
              val (tm1, args) = strip_comb tm
blanchet@43938
   546
              val adjustment = length ts - length args
blanchet@43938
   547
              val p' = if adjustment > p then p else p - adjustment
blanchet@43938
   548
              val tm_p = nth args p'
blanchet@43938
   549
                handle Subscript =>
blanchet@43945
   550
                       path_finder_fail MX tm (p :: ps) (SOME t)
blanchet@43938
   551
              val _ = trace_msg ctxt (fn () =>
blanchet@43938
   552
                  "path_finder: " ^ string_of_int p ^ "  " ^
blanchet@43938
   553
                  Syntax.string_of_term ctxt tm_p)
blanchet@43944
   554
              val (r, t) = path_finder_MX tm_p ps (nth ts p)
blanchet@43938
   555
            in (r, list_comb (tm1, replace_item_list t p' args)) end
blanchet@43945
   556
        | path_finder_MX tm ps t = path_finder_fail MX tm ps (SOME t)
blanchet@39737
   557
      fun path_finder FO tm ps _ = path_finder_FO tm ps
blanchet@39737
   558
        | path_finder HO (tm as Const(@{const_name HOL.eq},_) $ _ $ _) (p::ps) _ =
blanchet@39737
   559
             (*equality: not curried, as other predicates are*)
blanchet@39737
   560
             if p=0 then path_finder_HO tm (0::1::ps)  (*select first operand*)
blanchet@39737
   561
             else path_finder_HO tm (p::ps)        (*1 selects second operand*)
blanchet@39737
   562
        | path_finder HO tm (_ :: ps) (Metis_Term.Fn ("{}", [_])) =
blanchet@39737
   563
             path_finder_HO tm ps      (*if not equality, ignore head to skip hBOOL*)
blanchet@39737
   564
        | path_finder FT (tm as Const(@{const_name HOL.eq}, _) $ _ $ _) (p::ps)
blanchet@39737
   565
                            (Metis_Term.Fn ("=", [t1,t2])) =
blanchet@39737
   566
             (*equality: not curried, as other predicates are*)
blanchet@39737
   567
             if p=0 then path_finder_FT tm (0::1::ps)
blanchet@43935
   568
                          (Metis_Term.Fn (metis_app_op, [Metis_Term.Fn (metis_app_op, [metis_eq,t1]), t2]))
blanchet@39737
   569
                          (*select first operand*)
blanchet@39737
   570
             else path_finder_FT tm (p::ps)
blanchet@43935
   571
                   (Metis_Term.Fn (metis_app_op, [metis_eq, t2]))
blanchet@39737
   572
                   (*1 selects second operand*)
blanchet@39737
   573
        | path_finder FT tm (_ :: ps) (Metis_Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1
blanchet@39737
   574
             (*if not equality, ignore head to skip the hBOOL predicate*)
blanchet@39737
   575
        | path_finder FT tm ps t = path_finder_FT tm ps t  (*really an error case!*)
blanchet@43944
   576
        | path_finder MX tm ps t = path_finder_MX tm ps t
blanchet@39737
   577
      fun path_finder_lit ((nt as Const (@{const_name Not}, _)) $ tm_a) idx =
blanchet@39737
   578
            let val (tm, tm_rslt) = path_finder mode tm_a idx m_tm
blanchet@39737
   579
            in (tm, nt $ tm_rslt) end
blanchet@39737
   580
        | path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm
blanchet@39737
   581
      val (tm_subst, body) = path_finder_lit i_atm fp
blanchet@39738
   582
      val tm_abs = Abs ("x", type_of tm_subst, body)
blanchet@40159
   583
      val _ = trace_msg ctxt (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
blanchet@40159
   584
      val _ = trace_msg ctxt (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
blanchet@40159
   585
      val _ = trace_msg ctxt (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
blanchet@39737
   586
      val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst)  (*ill typed but gives right max*)
blanchet@39737
   587
      val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
blanchet@40159
   588
      val _ = trace_msg ctxt (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
blanchet@39737
   589
      val eq_terms = map (pairself (cterm_of thy))
blanchet@39737
   590
        (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
blanchet@39737
   591
  in  cterm_instantiate eq_terms subst'  end;
blanchet@39737
   592
blanchet@43935
   593
val factor = Seq.hd o distinct_subgoals_tac
blanchet@39737
   594
blanchet@43935
   595
fun one_step ctxt mode old_skolems sym_tab th_pairs p =
blanchet@39737
   596
  case p of
blanchet@43935
   597
    (fol_th, Metis_Proof.Axiom _) => axiom_inf th_pairs fol_th |> factor
blanchet@43935
   598
  | (_, Metis_Proof.Assume f_atm) =>
blanchet@43935
   599
    assume_inf ctxt mode old_skolems sym_tab f_atm
blanchet@39737
   600
  | (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) =>
blanchet@43935
   601
    inst_inf ctxt mode old_skolems sym_tab th_pairs f_subst f_th1 |> factor
blanchet@39737
   602
  | (_, Metis_Proof.Resolve(f_atm, f_th1, f_th2)) =>
blanchet@43935
   603
    resolve_inf ctxt mode old_skolems sym_tab th_pairs f_atm f_th1 f_th2
blanchet@43935
   604
    |> factor
blanchet@43935
   605
  | (_, Metis_Proof.Refl f_tm) => refl_inf ctxt mode old_skolems sym_tab f_tm
blanchet@39737
   606
  | (_, Metis_Proof.Equality (f_lit, f_p, f_r)) =>
blanchet@43935
   607
    equality_inf ctxt mode old_skolems sym_tab f_lit f_p f_r
blanchet@39737
   608
blanchet@40074
   609
fun flexflex_first_order th =
blanchet@40074
   610
  case Thm.tpairs_of th of
blanchet@40074
   611
      [] => th
blanchet@40074
   612
    | pairs =>
blanchet@40074
   613
        let val thy = theory_of_thm th
blanchet@40074
   614
            val (_, tenv) =
blanchet@40074
   615
              fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
blanchet@40074
   616
            val t_pairs = map Meson.term_pair_of (Vartab.dest tenv)
blanchet@40074
   617
            val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th
blanchet@40074
   618
        in  th'  end
blanchet@40074
   619
        handle THM _ => th;
blanchet@39737
   620
blanchet@40076
   621
fun is_metis_literal_genuine (_, (s, _)) = not (String.isPrefix class_prefix s)
blanchet@40076
   622
fun is_isabelle_literal_genuine t =
blanchet@40134
   623
  case t of _ $ (Const (@{const_name Meson.skolem}, _) $ _) => false | _ => true
blanchet@40076
   624
blanchet@40076
   625
fun count p xs = fold (fn x => if p x then Integer.add 1 else I) xs 0
blanchet@40076
   626
blanchet@43204
   627
(* Seldomly needed hack. A Metis clause is represented as a set, so duplicate
blanchet@43204
   628
   disjuncts are impossible. In the Isabelle proof, in spite of efforts to
blanchet@43204
   629
   eliminate them, duplicates sometimes appear with slightly different (but
blanchet@43204
   630
   unifiable) types. *)
blanchet@43204
   631
fun resynchronize ctxt fol_th th =
blanchet@43204
   632
  let
blanchet@43204
   633
    val num_metis_lits =
blanchet@43204
   634
      count is_metis_literal_genuine
blanchet@43204
   635
            (Metis_LiteralSet.toList (Metis_Thm.clause fol_th))
blanchet@43204
   636
    val num_isabelle_lits = count is_isabelle_literal_genuine (prems_of th)
blanchet@43204
   637
  in
blanchet@43204
   638
    if num_metis_lits >= num_isabelle_lits then
blanchet@43204
   639
      th
blanchet@43204
   640
    else
blanchet@43204
   641
      let
blanchet@43204
   642
        val (prems0, concl) = th |> prop_of |> Logic.strip_horn
blanchet@43204
   643
        val prems = prems0 |> distinct (uncurry untyped_aconv)
blanchet@43204
   644
        val goal = Logic.list_implies (prems, concl)
blanchet@43204
   645
      in
blanchet@43204
   646
        if length prems = length prems0 then
blanchet@43521
   647
          raise METIS ("resynchronize", "Out of sync")
blanchet@43204
   648
        else
blanchet@43204
   649
          Goal.prove ctxt [] [] goal (K (cut_rules_tac [th] 1
blanchet@43204
   650
                                         THEN ALLGOALS assume_tac))
blanchet@43204
   651
          |> resynchronize ctxt fol_th
blanchet@43204
   652
      end
blanchet@43204
   653
  end
blanchet@43204
   654
blanchet@43935
   655
fun replay_one_inference ctxt mode old_skolems sym_tab (fol_th, inf) th_pairs =
blanchet@43935
   656
  if not (null th_pairs) andalso
blanchet@43935
   657
     prop_of (snd (hd th_pairs)) aconv @{prop False} then
blanchet@41110
   658
    (* Isabelle sometimes identifies literals (premises) that are distinct in
blanchet@41110
   659
       Metis (e.g., because of type variables). We give the Isabelle proof the
blanchet@41110
   660
       benefice of the doubt. *)
blanchet@43935
   661
    th_pairs
blanchet@41110
   662
  else
blanchet@41110
   663
    let
blanchet@41110
   664
      val _ = trace_msg ctxt
blanchet@41110
   665
                  (fn () => "=============================================")
blanchet@41110
   666
      val _ = trace_msg ctxt
blanchet@41110
   667
                  (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)
blanchet@41110
   668
      val _ = trace_msg ctxt
blanchet@41110
   669
                  (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)
blanchet@43935
   670
      val th = one_step ctxt mode old_skolems sym_tab th_pairs (fol_th, inf)
blanchet@41110
   671
               |> flexflex_first_order
blanchet@43204
   672
               |> resynchronize ctxt fol_th
blanchet@41110
   673
      val _ = trace_msg ctxt
blanchet@41110
   674
                  (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
blanchet@41110
   675
      val _ = trace_msg ctxt
blanchet@41110
   676
                  (fn () => "=============================================")
blanchet@43935
   677
    in (fol_th, th) :: th_pairs end
blanchet@39737
   678
blanchet@43213
   679
(* It is normally sufficient to apply "assume_tac" to unify the conclusion with
blanchet@43213
   680
   one of the premises. Unfortunately, this sometimes yields "Variable
blanchet@43213
   681
   ?SK_a_b_c_x has two distinct types" errors. To avoid this, we instantiate the
blanchet@43213
   682
   variables before applying "assume_tac". Typical constraints are of the form
blanchet@43213
   683
     ?SK_a_b_c_x SK_d_e_f_y ... SK_a_b_c_x ... SK_g_h_i_z =?= SK_a_b_c_x,
blanchet@43213
   684
   where the nonvariables are goal parameters. *)
blanchet@43213
   685
fun unify_first_prem_with_concl thy i th =
blanchet@43213
   686
  let
blanchet@43213
   687
    val goal = Logic.get_goal (prop_of th) i |> Envir.beta_eta_contract
blanchet@43213
   688
    val prem = goal |> Logic.strip_assums_hyp |> hd
blanchet@43213
   689
    val concl = goal |> Logic.strip_assums_concl
blanchet@43213
   690
    fun pair_untyped_aconv (t1, t2) (u1, u2) =
blanchet@43213
   691
      untyped_aconv t1 u1 andalso untyped_aconv t2 u2
blanchet@43213
   692
    fun add_terms tp inst =
blanchet@43213
   693
      if exists (pair_untyped_aconv tp) inst then inst
blanchet@43213
   694
      else tp :: map (apsnd (subst_atomic [tp])) inst
blanchet@43213
   695
    fun is_flex t =
blanchet@43213
   696
      case strip_comb t of
blanchet@43213
   697
        (Var _, args) => forall is_Bound args
blanchet@43213
   698
      | _ => false
blanchet@43213
   699
    fun unify_flex flex rigid =
blanchet@43213
   700
      case strip_comb flex of
blanchet@43213
   701
        (Var (z as (_, T)), args) =>
blanchet@43213
   702
        add_terms (Var z,
blanchet@43213
   703
          fold_rev (curry absdummy) (take (length args) (binder_types T)) rigid)
blanchet@43213
   704
      | _ => I
blanchet@43213
   705
    fun unify_potential_flex comb atom =
blanchet@43213
   706
      if is_flex comb then unify_flex comb atom
blanchet@43213
   707
      else if is_Var atom then add_terms (atom, comb)
blanchet@43213
   708
      else I
blanchet@43213
   709
    fun unify_terms (t, u) =
blanchet@43213
   710
      case (t, u) of
blanchet@43213
   711
        (t1 $ t2, u1 $ u2) =>
blanchet@43213
   712
        if is_flex t then unify_flex t u
blanchet@43213
   713
        else if is_flex u then unify_flex u t
blanchet@43213
   714
        else fold unify_terms [(t1, u1), (t2, u2)]
blanchet@43213
   715
      | (_ $ _, _) => unify_potential_flex t u
blanchet@43213
   716
      | (_, _ $ _) => unify_potential_flex u t
blanchet@43213
   717
      | (Var _, _) => add_terms (t, u)
blanchet@43213
   718
      | (_, Var _) => add_terms (u, t)
blanchet@43213
   719
      | _ => I
blanchet@43215
   720
    val t_inst =
blanchet@43215
   721
      [] |> try (unify_terms (prem, concl) #> map (pairself (cterm_of thy)))
blanchet@43215
   722
         |> the_default [] (* FIXME *)
blanchet@43213
   723
  in th |> cterm_instantiate t_inst end
blanchet@40145
   724
blanchet@40145
   725
val copy_prem = @{lemma "P ==> (P ==> P ==> Q) ==> Q" by fast}
blanchet@40145
   726
blanchet@40145
   727
fun copy_prems_tac [] ns i =
blanchet@40145
   728
    if forall (curry (op =) 1) ns then all_tac else copy_prems_tac (rev ns) [] i
blanchet@40145
   729
  | copy_prems_tac (1 :: ms) ns i =
blanchet@40145
   730
    rotate_tac 1 i THEN copy_prems_tac ms (1 :: ns) i
blanchet@40145
   731
  | copy_prems_tac (m :: ms) ns i =
blanchet@40145
   732
    etac copy_prem i THEN copy_prems_tac ms (m div 2 :: (m + 1) div 2 :: ns) i
blanchet@40145
   733
blanchet@43135
   734
(* Metis generates variables of the form _nnn. *)
blanchet@43135
   735
val is_metis_fresh_variable = String.isPrefix "_"
blanchet@43135
   736
blanchet@40501
   737
fun instantiate_forall_tac thy t i st =
blanchet@40145
   738
  let
blanchet@40501
   739
    val params = Logic.strip_params (Logic.get_goal (prop_of st) i) |> rev
blanchet@40145
   740
    fun repair (t as (Var ((s, _), _))) =
blanchet@40501
   741
        (case find_index (fn (s', _) => s' = s) params of
blanchet@40145
   742
           ~1 => t
blanchet@40145
   743
         | j => Bound j)
blanchet@40504
   744
      | repair (t $ u) =
blanchet@40504
   745
        (case (repair t, repair u) of
blanchet@40504
   746
           (t as Bound j, u as Bound k) =>
blanchet@40504
   747
           (* This is a rather subtle trick to repair the discrepancy between
blanchet@40504
   748
              the fully skolemized term that MESON gives us (where existentials
blanchet@40504
   749
              were pulled out) and the reality. *)
blanchet@40504
   750
           if k > j then t else t $ u
blanchet@40504
   751
         | (t, u) => t $ u)
blanchet@40145
   752
      | repair t = t
blanchet@40145
   753
    val t' = t |> repair |> fold (curry absdummy) (map snd params)
blanchet@40145
   754
    fun do_instantiate th =
blanchet@43134
   755
      case Term.add_vars (prop_of th) []
blanchet@43135
   756
           |> filter_out ((Meson_Clausify.is_zapped_var_name orf
blanchet@43135
   757
                           is_metis_fresh_variable) o fst o fst) of
blanchet@43134
   758
        [] => th
blanchet@43135
   759
      | [var as (_, T)] =>
blanchet@43135
   760
        let
blanchet@43135
   761
          val var_binder_Ts = T |> binder_types |> take (length params) |> rev
blanchet@43135
   762
          val var_body_T = T |> funpow (length params) range_type
blanchet@43135
   763
          val tyenv =
blanchet@43135
   764
            Vartab.empty |> Type.raw_unifys (fastype_of t :: map snd params,
blanchet@43135
   765
                                             var_body_T :: var_binder_Ts)
blanchet@43135
   766
          val env =
blanchet@43135
   767
            Envir.Envir {maxidx = Vartab.fold (Integer.max o snd o fst) tyenv 0,
blanchet@43135
   768
                         tenv = Vartab.empty, tyenv = tyenv}
blanchet@43135
   769
          val ty_inst =
blanchet@43135
   770
            Vartab.fold (fn (x, (S, T)) =>
blanchet@43135
   771
                            cons (pairself (ctyp_of thy) (TVar (x, S), T)))
blanchet@43135
   772
                        tyenv []
blanchet@43135
   773
          val t_inst =
blanchet@43135
   774
            [pairself (cterm_of thy o Envir.norm_term env) (Var var, t')]
blanchet@43213
   775
        in th |> instantiate (ty_inst, t_inst) end
blanchet@43135
   776
      | _ => raise Fail "expected a single non-zapped, non-Metis Var"
blanchet@40145
   777
  in
blanchet@43135
   778
    (DETERM (etac @{thm allE} i THEN rotate_tac ~1 i)
blanchet@40501
   779
     THEN PRIMITIVE do_instantiate) st
blanchet@40145
   780
  end
blanchet@40145
   781
blanchet@41383
   782
fun fix_exists_tac t =
blanchet@40504
   783
  etac @{thm exE}
blanchet@40504
   784
  THEN' rename_tac [t |> dest_Var |> fst |> fst]
blanchet@40504
   785
blanchet@40504
   786
fun release_quantifier_tac thy (skolem, t) =
blanchet@41383
   787
  (if skolem then fix_exists_tac else instantiate_forall_tac thy) t
blanchet@40504
   788
blanchet@40501
   789
fun release_clusters_tac _ _ _ [] = K all_tac
blanchet@40501
   790
  | release_clusters_tac thy ax_counts substs
blanchet@40145
   791
                         ((ax_no, cluster_no) :: clusters) =
blanchet@40145
   792
    let
blanchet@40504
   793
      val cluster_of_var =
blanchet@40504
   794
        Meson_Clausify.cluster_of_zapped_var_name o fst o fst o dest_Var
blanchet@40504
   795
      fun in_right_cluster ((_, (cluster_no', _)), _) = cluster_no' = cluster_no
blanchet@40145
   796
      val cluster_substs =
blanchet@40145
   797
        substs
blanchet@40145
   798
        |> map_filter (fn (ax_no', (_, (_, tsubst))) =>
blanchet@40145
   799
                          if ax_no' = ax_no then
blanchet@40504
   800
                            tsubst |> map (apfst cluster_of_var)
blanchet@40504
   801
                                   |> filter (in_right_cluster o fst)
blanchet@40504
   802
                                   |> map (apfst snd)
blanchet@40504
   803
                                   |> SOME
blanchet@40504
   804
                          else
blanchet@40504
   805
                            NONE)
blanchet@40145
   806
      fun do_cluster_subst cluster_subst =
blanchet@40504
   807
        map (release_quantifier_tac thy) cluster_subst @ [rotate_tac 1]
blanchet@40145
   808
      val first_prem = find_index (fn (ax_no', _) => ax_no' = ax_no) substs
blanchet@40145
   809
    in
blanchet@40145
   810
      rotate_tac first_prem
blanchet@40145
   811
      THEN' (EVERY' (maps do_cluster_subst cluster_substs))
blanchet@40145
   812
      THEN' rotate_tac (~ first_prem - length cluster_substs)
blanchet@40501
   813
      THEN' release_clusters_tac thy ax_counts substs clusters
blanchet@40145
   814
    end
blanchet@40145
   815
blanchet@40507
   816
fun cluster_key ((ax_no, (cluster_no, index_no)), skolem) =
blanchet@40507
   817
  (ax_no, (cluster_no, (skolem, index_no)))
blanchet@40507
   818
fun cluster_ord p =
blanchet@40507
   819
  prod_ord int_ord (prod_ord int_ord (prod_ord bool_ord int_ord))
blanchet@40507
   820
           (pairself cluster_key p)
blanchet@40145
   821
blanchet@40145
   822
val tysubst_ord =
blanchet@40145
   823
  list_ord (prod_ord Term_Ord.fast_indexname_ord
blanchet@40145
   824
                     (prod_ord Term_Ord.sort_ord Term_Ord.typ_ord))
blanchet@40145
   825
blanchet@40145
   826
structure Int_Tysubst_Table =
blanchet@40145
   827
  Table(type key = int * (indexname * (sort * typ)) list
blanchet@40145
   828
        val ord = prod_ord int_ord tysubst_ord)
blanchet@40145
   829
blanchet@40145
   830
structure Int_Pair_Graph =
blanchet@40145
   831
  Graph(type key = int * int val ord = prod_ord int_ord int_ord)
blanchet@40145
   832
blanchet@43135
   833
fun shuffle_key (((axiom_no, (_, index_no)), _), _) = (axiom_no, index_no)
blanchet@40501
   834
fun shuffle_ord p = prod_ord int_ord int_ord (pairself shuffle_key p)
blanchet@40501
   835
blanchet@40145
   836
(* Attempts to derive the theorem "False" from a theorem of the form
blanchet@40145
   837
   "P1 ==> ... ==> Pn ==> False", where the "Pi"s are to be discharged using the
blanchet@40145
   838
   specified axioms. The axioms have leading "All" and "Ex" quantifiers, which
blanchet@40145
   839
   must be eliminated first. *)
blanchet@40145
   840
fun discharge_skolem_premises ctxt axioms prems_imp_false =
blanchet@40145
   841
  if prop_of prems_imp_false aconv @{prop False} then
blanchet@40145
   842
    prems_imp_false
blanchet@40145
   843
  else
blanchet@40145
   844
    let
wenzelm@43232
   845
      val thy = Proof_Context.theory_of ctxt
blanchet@40145
   846
      fun match_term p =
blanchet@40145
   847
        let
blanchet@40145
   848
          val (tyenv, tenv) =
blanchet@40145
   849
            Pattern.first_order_match thy p (Vartab.empty, Vartab.empty)
blanchet@40145
   850
          val tsubst =
blanchet@40145
   851
            tenv |> Vartab.dest
blanchet@42963
   852
                 |> filter (Meson_Clausify.is_zapped_var_name o fst o fst)
blanchet@40145
   853
                 |> sort (cluster_ord
blanchet@40145
   854
                          o pairself (Meson_Clausify.cluster_of_zapped_var_name
blanchet@40145
   855
                                      o fst o fst))
blanchet@40145
   856
                 |> map (Meson.term_pair_of
blanchet@40145
   857
                         #> pairself (Envir.subst_term_types tyenv))
blanchet@40145
   858
          val tysubst = tyenv |> Vartab.dest
blanchet@40145
   859
        in (tysubst, tsubst) end
blanchet@40145
   860
      fun subst_info_for_prem subgoal_no prem =
blanchet@40145
   861
        case prem of
blanchet@40145
   862
          _ $ (Const (@{const_name Meson.skolem}, _) $ (_ $ t $ num)) =>
blanchet@40145
   863
          let val ax_no = HOLogic.dest_nat num in
blanchet@40145
   864
            (ax_no, (subgoal_no,
blanchet@40145
   865
                     match_term (nth axioms ax_no |> the |> snd, t)))
blanchet@40145
   866
          end
blanchet@40145
   867
        | _ => raise TERM ("discharge_skolem_premises: Malformed premise",
blanchet@40145
   868
                           [prem])
blanchet@40145
   869
      fun cluster_of_var_name skolem s =
blanchet@42962
   870
        case try Meson_Clausify.cluster_of_zapped_var_name s of
blanchet@42962
   871
          NONE => NONE
blanchet@42962
   872
        | SOME ((ax_no, (cluster_no, _)), skolem') =>
blanchet@40145
   873
          if skolem' = skolem andalso cluster_no > 0 then
blanchet@40145
   874
            SOME (ax_no, cluster_no)
blanchet@40145
   875
          else
blanchet@40145
   876
            NONE
blanchet@40145
   877
      fun clusters_in_term skolem t =
blanchet@40145
   878
        Term.add_var_names t [] |> map_filter (cluster_of_var_name skolem o fst)
blanchet@40145
   879
      fun deps_for_term_subst (var, t) =
blanchet@40145
   880
        case clusters_in_term false var of
blanchet@40145
   881
          [] => NONE
blanchet@40145
   882
        | [(ax_no, cluster_no)] =>
blanchet@40145
   883
          SOME ((ax_no, cluster_no),
blanchet@40145
   884
                clusters_in_term true t
blanchet@40145
   885
                |> cluster_no > 1 ? cons (ax_no, cluster_no - 1))
blanchet@40145
   886
        | _ => raise TERM ("discharge_skolem_premises: Expected Var", [var])
blanchet@40145
   887
      val prems = Logic.strip_imp_prems (prop_of prems_imp_false)
blanchet@40145
   888
      val substs = prems |> map2 subst_info_for_prem (1 upto length prems)
blanchet@40145
   889
                         |> sort (int_ord o pairself fst)
blanchet@40145
   890
      val depss = maps (map_filter deps_for_term_subst o snd o snd o snd) substs
blanchet@40145
   891
      val clusters = maps (op ::) depss
blanchet@40145
   892
      val ordered_clusters =
blanchet@40145
   893
        Int_Pair_Graph.empty
blanchet@40145
   894
        |> fold Int_Pair_Graph.default_node (map (rpair ()) clusters)
blanchet@40145
   895
        |> fold Int_Pair_Graph.add_deps_acyclic depss
blanchet@40145
   896
        |> Int_Pair_Graph.topological_order
blanchet@40145
   897
        handle Int_Pair_Graph.CYCLES _ =>
blanchet@40399
   898
               error "Cannot replay Metis proof in Isabelle without \
blanchet@40399
   899
                     \\"Hilbert_Choice\"."
blanchet@40145
   900
      val ax_counts =
blanchet@40145
   901
        Int_Tysubst_Table.empty
blanchet@40145
   902
        |> fold (fn (ax_no, (_, (tysubst, _))) =>
blanchet@40145
   903
                    Int_Tysubst_Table.map_default ((ax_no, tysubst), 0)
blanchet@40145
   904
                                                  (Integer.add 1)) substs
blanchet@40145
   905
        |> Int_Tysubst_Table.dest
blanchet@43210
   906
      val needed_axiom_props =
blanchet@43210
   907
        0 upto length axioms - 1 ~~ axioms
blanchet@43210
   908
        |> map_filter (fn (_, NONE) => NONE
blanchet@43210
   909
                        | (ax_no, SOME (_, t)) =>
blanchet@43210
   910
                          if exists (fn ((ax_no', _), n) =>
blanchet@43210
   911
                                        ax_no' = ax_no andalso n > 0)
blanchet@43210
   912
                                    ax_counts then
blanchet@43210
   913
                            SOME t
blanchet@43210
   914
                          else
blanchet@43210
   915
                            NONE)
blanchet@43210
   916
      val outer_param_names =
blanchet@43210
   917
        [] |> fold Term.add_var_names needed_axiom_props
blanchet@43210
   918
           |> filter (Meson_Clausify.is_zapped_var_name o fst)
blanchet@43210
   919
           |> map (`(Meson_Clausify.cluster_of_zapped_var_name o fst))
blanchet@43210
   920
           |> filter (fn (((_, (cluster_no, _)), skolem), _) =>
blanchet@43210
   921
                         cluster_no = 0 andalso skolem)
blanchet@43210
   922
           |> sort shuffle_ord |> map (fst o snd)
blanchet@43134
   923
(* for debugging only:
blanchet@40145
   924
      fun string_for_subst_info (ax_no, (subgoal_no, (tysubst, tsubst))) =
blanchet@40145
   925
        "ax: " ^ string_of_int ax_no ^ "; asm: " ^ string_of_int subgoal_no ^
blanchet@40145
   926
        "; tysubst: " ^ PolyML.makestring tysubst ^ "; tsubst: {" ^
blanchet@40145
   927
        commas (map ((fn (s, t) => s ^ " |-> " ^ t)
blanchet@40145
   928
                     o pairself (Syntax.string_of_term ctxt)) tsubst) ^ "}"
blanchet@40507
   929
      val _ = tracing ("ORDERED CLUSTERS: " ^ PolyML.makestring ordered_clusters)
blanchet@40507
   930
      val _ = tracing ("AXIOM COUNTS: " ^ PolyML.makestring ax_counts)
blanchet@43210
   931
      val _ = tracing ("OUTER PARAMS: " ^ PolyML.makestring outer_param_names)
blanchet@40145
   932
      val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^
blanchet@40145
   933
                       cat_lines (map string_for_subst_info substs))
blanchet@40145
   934
*)
blanchet@43135
   935
      fun cut_and_ex_tac axiom =
blanchet@43135
   936
        cut_rules_tac [axiom] 1
blanchet@43135
   937
        THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1)
blanchet@40145
   938
      fun rotation_for_subgoal i =
blanchet@40145
   939
        find_index (fn (_, (subgoal_no, _)) => subgoal_no = i) substs
blanchet@40145
   940
    in
blanchet@40145
   941
      Goal.prove ctxt [] [] @{prop False}
blanchet@43135
   942
          (K (DETERM (EVERY (map (cut_and_ex_tac o fst o the o nth axioms o fst
blanchet@43135
   943
                                  o fst) ax_counts)
blanchet@43135
   944
                      THEN rename_tac outer_param_names 1
blanchet@43135
   945
                      THEN copy_prems_tac (map snd ax_counts) [] 1)
blanchet@40501
   946
              THEN release_clusters_tac thy ax_counts substs ordered_clusters 1
blanchet@40145
   947
              THEN match_tac [prems_imp_false] 1
blanchet@40145
   948
              THEN ALLGOALS (fn i =>
blanchet@40145
   949
                       rtac @{thm Meson.skolem_COMBK_I} i
blanchet@40145
   950
                       THEN rotate_tac (rotation_for_subgoal i) i
blanchet@43213
   951
                       THEN PRIMITIVE (unify_first_prem_with_concl thy i)
blanchet@43135
   952
                       THEN assume_tac i
blanchet@43134
   953
                       THEN flexflex_tac)))
blanchet@40399
   954
      handle ERROR _ =>
blanchet@40399
   955
             error ("Cannot replay Metis proof in Isabelle:\n\
blanchet@40399
   956
                    \Error when discharging Skolem assumptions.")
blanchet@40145
   957
    end
blanchet@40145
   958
blanchet@39735
   959
end;