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