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