src/HOL/Tools/Metis/metis_reconstruct.ML
author wenzelm
Wed, 29 May 2013 18:25:11 +0200
changeset 52223 5bb6ae8acb87
parent 52178 6228806b2605
child 52225 568b2cd65d50
permissions -rw-r--r--
tuned signature -- more explicit flags for low-level Thm.bicompose;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
39958
88c9aa5666de tuned comments
blanchet
parents: 39953
diff changeset
     1
(*  Title:      HOL/Tools/Metis/metis_reconstruct.ML
39495
bb4fb9ffe2d1 added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff changeset
     2
    Author:     Kong W. Susanto, Cambridge University Computer Laboratory
bb4fb9ffe2d1 added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff changeset
     3
    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
bb4fb9ffe2d1 added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff changeset
     4
    Author:     Jasmin Blanchette, TU Muenchen
bb4fb9ffe2d1 added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff changeset
     5
    Copyright   Cambridge University 2007
bb4fb9ffe2d1 added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff changeset
     6
bb4fb9ffe2d1 added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff changeset
     7
Proof reconstruction for Metis.
bb4fb9ffe2d1 added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff changeset
     8
*)
bb4fb9ffe2d1 added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff changeset
     9
bb4fb9ffe2d1 added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff changeset
    10
signature METIS_RECONSTRUCT =
bb4fb9ffe2d1 added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff changeset
    11
sig
46320
0b8b73b49848 renamed two files to make room for a new file
blanchet
parents: 45569
diff changeset
    12
  type type_enc = ATP_Problem_Generate.type_enc
44492
a330c0608da8 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents: 44241
diff changeset
    13
50875
bfb626265782 less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents: 48132
diff changeset
    14
  exception METIS_RECONSTRUCT of string * string
42650
552eae49f97d reintroduce this idea of running "metisFT" after a failed "metis" -- I took it out in e85ce10cef1a because I couldn't think of a reasonable use case, but now that ATPs use sound encodings and include dangerous facts (e.g. True_or_False) it makes more sense than ever to run "metisFT" after "metis"
blanchet
parents: 42616
diff changeset
    15
52031
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51998
diff changeset
    16
  val hol_clause_of_metis :
45508
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 44492
diff changeset
    17
    Proof.context -> type_enc -> int Symtab.table
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 44492
diff changeset
    18
    -> (string * term) list * (string * term) list -> Metis_Thm.thm -> term
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
    19
  val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
    20
  val replay_one_inference :
45508
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 44492
diff changeset
    21
    Proof.context -> type_enc
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 44492
diff changeset
    22
    -> (string * term) list * (string * term) list -> int Symtab.table
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
    23
    -> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
    24
    -> (Metis_Thm.thm * thm) list
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
    25
  val discharge_skolem_premises :
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
    26
    Proof.context -> (thm * term) option list -> thm -> thm
39495
bb4fb9ffe2d1 added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff changeset
    27
end;
bb4fb9ffe2d1 added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff changeset
    28
bb4fb9ffe2d1 added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff changeset
    29
structure Metis_Reconstruct : METIS_RECONSTRUCT =
bb4fb9ffe2d1 added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff changeset
    30
struct
bb4fb9ffe2d1 added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff changeset
    31
43094
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
    32
open ATP_Problem
46320
0b8b73b49848 renamed two files to make room for a new file
blanchet
parents: 45569
diff changeset
    33
open ATP_Problem_Generate
0b8b73b49848 renamed two files to make room for a new file
blanchet
parents: 45569
diff changeset
    34
open ATP_Proof_Reconstruct
0b8b73b49848 renamed two files to make room for a new file
blanchet
parents: 45569
diff changeset
    35
open Metis_Generate
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
    36
50875
bfb626265782 less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents: 48132
diff changeset
    37
exception METIS_RECONSTRUCT of string * string
42650
552eae49f97d reintroduce this idea of running "metisFT" after a failed "metis" -- I took it out in e85ce10cef1a because I couldn't think of a reasonable use case, but now that ATPs use sound encodings and include dangerous facts (e.g. True_or_False) it makes more sense than ever to run "metisFT" after "metis"
blanchet
parents: 42616
diff changeset
    38
52031
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51998
diff changeset
    39
fun atp_name_of_metis type_enc s =
44492
a330c0608da8 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents: 44241
diff changeset
    40
  case find_first (fn (_, (f, _)) => f type_enc = s) metis_name_table of
43104
81d1b15aa0ae use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents: 43103
diff changeset
    41
    SOME ((s, _), (_, swap)) => (s, swap)
81d1b15aa0ae use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents: 43103
diff changeset
    42
  | _ => (s, false)
52031
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51998
diff changeset
    43
fun atp_term_of_metis type_enc (Metis_Term.Fn (s, tms)) =
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51998
diff changeset
    44
    let val (s, swap) = atp_name_of_metis type_enc (Metis_Name.toString s) in
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51998
diff changeset
    45
      ATerm ((s, []), tms |> map (atp_term_of_metis type_enc) |> swap ? rev)
43104
81d1b15aa0ae use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents: 43103
diff changeset
    46
    end
52031
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51998
diff changeset
    47
  | atp_term_of_metis _ (Metis_Term.Var s) =
48132
9aa0fad4e864 added type arguments to "ATerm" constructor -- but don't use them yet
blanchet
parents: 46708
diff changeset
    48
    ATerm ((Metis_Name.toString s, []), [])
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
    49
52031
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51998
diff changeset
    50
fun hol_term_of_metis ctxt type_enc sym_tab =
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51998
diff changeset
    51
  atp_term_of_metis type_enc #> term_of_atp ctxt false sym_tab NONE
43094
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
    52
52031
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51998
diff changeset
    53
fun atp_literal_of_metis type_enc (pos, atom) =
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51998
diff changeset
    54
  atom |> Metis_Term.Fn |> atp_term_of_metis type_enc
44492
a330c0608da8 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents: 44241
diff changeset
    55
       |> AAtom |> not pos ? mk_anot
52031
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51998
diff changeset
    56
fun atp_clause_of_metis _ [] = AAtom (ATerm ((tptp_false, []), []))
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51998
diff changeset
    57
  | atp_clause_of_metis type_enc lits =
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51998
diff changeset
    58
    lits |> map (atp_literal_of_metis type_enc) |> mk_aconns AOr
43136
cf5cda219058 handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents: 43135
diff changeset
    59
45508
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 44492
diff changeset
    60
fun polish_hol_terms ctxt (lifted, old_skolems) =
45569
eb30a5490543 wrap lambdas earlier, to get more control over beta/eta
blanchet
parents: 45511
diff changeset
    61
  map (reveal_lam_lifted lifted #> reveal_old_skolem_terms old_skolems)
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43209
diff changeset
    62
  #> Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
43184
b16693484c5d reveal Skolems in new Metis
blanchet
parents: 43177
diff changeset
    63
52031
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51998
diff changeset
    64
fun hol_clause_of_metis ctxt type_enc sym_tab concealed =
43159
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43136
diff changeset
    65
  Metis_Thm.clause
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43136
diff changeset
    66
  #> Metis_LiteralSet.toList
52031
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51998
diff changeset
    67
  #> atp_clause_of_metis type_enc
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51998
diff changeset
    68
  #> prop_of_atp ctxt false sym_tab
45508
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 44492
diff changeset
    69
  #> singleton (polish_hol_terms ctxt concealed)
43136
cf5cda219058 handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents: 43135
diff changeset
    70
52031
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51998
diff changeset
    71
fun hol_terms_of_metis ctxt type_enc concealed sym_tab fol_tms =
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51998
diff changeset
    72
  let val ts = map (hol_term_of_metis ctxt type_enc sym_tab) fol_tms
39978
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
    73
      val _ = trace_msg ctxt (fn () => "  calling type inference:")
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
    74
      val _ = app (fn t => trace_msg ctxt
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
    75
                                     (fn () => Syntax.string_of_term ctxt t)) ts
45508
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 44492
diff changeset
    76
      val ts' = ts |> polish_hol_terms ctxt concealed
39978
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
    77
      val _ = app (fn t => trace_msg ctxt
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
    78
                    (fn () => "  final term: " ^ Syntax.string_of_term ctxt t ^
43128
a19826080596 tuned names
blanchet
parents: 43106
diff changeset
    79
                              " of type " ^ Syntax.string_of_typ ctxt (type_of t)))
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
    80
                  ts'
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
    81
  in  ts'  end;
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
    82
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
    83
(* ------------------------------------------------------------------------- *)
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
    84
(* FOL step Inference Rules                                                  *)
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
    85
(* ------------------------------------------------------------------------- *)
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
    86
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
    87
(*for debugging only*)
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
    88
(*
39978
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
    89
fun print_thpair ctxt (fth,th) =
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
    90
  (trace_msg ctxt (fn () => "=============================================");
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
    91
   trace_msg ctxt (fn () => "Metis: " ^ Metis_Thm.toString fth);
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
    92
   trace_msg ctxt (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th));
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
    93
*)
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
    94
43094
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
    95
fun lookth th_pairs fth =
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
    96
  the (AList.lookup (uncurry Metis_Thm.equal) th_pairs fth)
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
    97
  handle Option.Option =>
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
    98
         raise Fail ("Failed to find Metis theorem " ^ Metis_Thm.toString fth)
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
    99
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   100
fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx));
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   101
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   102
(* INFERENCE RULE: AXIOM *)
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   103
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43209
diff changeset
   104
(* This causes variables to have an index of 1 by default. See also
52031
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51998
diff changeset
   105
   "term_of_atp" in "ATP_Proof_Reconstruct". *)
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43209
diff changeset
   106
val axiom_inference = Thm.incr_indexes 1 oo lookth
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   107
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   108
(* INFERENCE RULE: ASSUME *)
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   109
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   110
val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)}
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   111
43187
95bd1ef1331a make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents: 43186
diff changeset
   112
fun inst_excluded_middle thy i_atom =
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   113
  let val th = EXCLUDED_MIDDLE
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   114
      val [vx] = Term.add_vars (prop_of th) []
43187
95bd1ef1331a make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents: 43186
diff changeset
   115
      val substs = [(cterm_of thy (Var vx), cterm_of thy i_atom)]
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   116
  in  cterm_instantiate substs th  end;
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   117
45508
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 44492
diff changeset
   118
fun assume_inference ctxt type_enc concealed sym_tab atom =
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   119
  inst_excluded_middle
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42354
diff changeset
   120
      (Proof_Context.theory_of ctxt)
52031
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51998
diff changeset
   121
      (singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab)
43187
95bd1ef1331a make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents: 43186
diff changeset
   122
                 (Metis_Term.Fn atom))
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   123
39498
e8aef7ea9cbb make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents: 39497
diff changeset
   124
(* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   125
   to reconstruct them admits new possibilities of errors, e.g. concerning
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   126
   sorts. Instead we try to arrange that new TVars are distinct and that types
39498
e8aef7ea9cbb make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents: 39497
diff changeset
   127
   can be inferred from terms. *)
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   128
45508
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 44492
diff changeset
   129
fun inst_inference ctxt type_enc concealed sym_tab th_pairs fsubst th =
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42354
diff changeset
   130
  let val thy = Proof_Context.theory_of ctxt
43094
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
   131
      val i_th = lookth th_pairs th
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   132
      val i_th_vars = Term.add_vars (prop_of i_th) []
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   133
      fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars)
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   134
      fun subst_translation (x,y) =
39498
e8aef7ea9cbb make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents: 39497
diff changeset
   135
        let val v = find_var x
45508
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 44492
diff changeset
   136
            (* We call "polish_hol_terms" below. *)
52031
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51998
diff changeset
   137
            val t = hol_term_of_metis ctxt type_enc sym_tab y
39498
e8aef7ea9cbb make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents: 39497
diff changeset
   138
        in  SOME (cterm_of thy (Var v), t)  end
e8aef7ea9cbb make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents: 39497
diff changeset
   139
        handle Option.Option =>
39978
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
   140
               (trace_msg ctxt (fn () => "\"find_var\" failed for " ^ x ^
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
   141
                                         " in " ^ Display.string_of_thm ctxt i_th);
39498
e8aef7ea9cbb make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents: 39497
diff changeset
   142
                NONE)
e8aef7ea9cbb make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents: 39497
diff changeset
   143
             | TYPE _ =>
52031
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51998
diff changeset
   144
               (trace_msg ctxt (fn () => "\"hol_term_of_metis\" failed for " ^ x ^
39978
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
   145
                                         " in " ^ Display.string_of_thm ctxt i_th);
39498
e8aef7ea9cbb make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents: 39497
diff changeset
   146
                NONE)
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   147
      fun remove_typeinst (a, t) =
43268
c0eaa8b9bff5 removed yet another hack in "make_metis" script -- respect opacity of "Metis_Name.name"
blanchet
parents: 43262
diff changeset
   148
        let val a = Metis_Name.toString a in
45511
9b0f8ca4388e continued implementation of lambda-lifting in Metis
blanchet
parents: 45508
diff changeset
   149
          case unprefix_and_unascii schematic_var_prefix a of
43268
c0eaa8b9bff5 removed yet another hack in "make_metis" script -- respect opacity of "Metis_Name.name"
blanchet
parents: 43262
diff changeset
   150
            SOME b => SOME (b, t)
c0eaa8b9bff5 removed yet another hack in "make_metis" script -- respect opacity of "Metis_Name.name"
blanchet
parents: 43262
diff changeset
   151
          | NONE =>
45511
9b0f8ca4388e continued implementation of lambda-lifting in Metis
blanchet
parents: 45508
diff changeset
   152
            case unprefix_and_unascii tvar_prefix a of
43268
c0eaa8b9bff5 removed yet another hack in "make_metis" script -- respect opacity of "Metis_Name.name"
blanchet
parents: 43262
diff changeset
   153
              SOME _ => NONE (* type instantiations are forbidden *)
c0eaa8b9bff5 removed yet another hack in "make_metis" script -- respect opacity of "Metis_Name.name"
blanchet
parents: 43262
diff changeset
   154
            | NONE => SOME (a, t) (* internal Metis var? *)
c0eaa8b9bff5 removed yet another hack in "make_metis" script -- respect opacity of "Metis_Name.name"
blanchet
parents: 43262
diff changeset
   155
        end
39978
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
   156
      val _ = trace_msg ctxt (fn () => "  isa th: " ^ Display.string_of_thm ctxt i_th)
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   157
      val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst)
43184
b16693484c5d reveal Skolems in new Metis
blanchet
parents: 43177
diff changeset
   158
      val (vars, tms) =
b16693484c5d reveal Skolems in new Metis
blanchet
parents: 43177
diff changeset
   159
        ListPair.unzip (map_filter subst_translation substs)
45508
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 44492
diff changeset
   160
        ||> polish_hol_terms ctxt concealed
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   161
      val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   162
      val substs' = ListPair.zip (vars, map ctm_of tms)
39978
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
   163
      val _ = trace_msg ctxt (fn () =>
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   164
        cat_lines ("subst_translations:" ::
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   165
          (substs' |> map (fn (x, y) =>
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   166
            Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   167
            Syntax.string_of_term ctxt (term_of y)))));
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   168
  in cterm_instantiate substs' i_th end
50875
bfb626265782 less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents: 48132
diff changeset
   169
  handle THM (msg, _, _) => raise METIS_RECONSTRUCT ("inst_inference", msg)
bfb626265782 less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents: 48132
diff changeset
   170
       | ERROR msg => raise METIS_RECONSTRUCT ("inst_inference", msg)
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   171
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   172
(* INFERENCE RULE: RESOLVE *)
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   173
43330
c6bbeca3ee06 clarified special incr_type_indexes;
wenzelm
parents: 43301
diff changeset
   174
(*Increment the indexes of only the type variables*)
c6bbeca3ee06 clarified special incr_type_indexes;
wenzelm
parents: 43301
diff changeset
   175
fun incr_type_indexes inc th =
c6bbeca3ee06 clarified special incr_type_indexes;
wenzelm
parents: 43301
diff changeset
   176
  let val tvs = Term.add_tvars (Thm.full_prop_of th) []
c6bbeca3ee06 clarified special incr_type_indexes;
wenzelm
parents: 43301
diff changeset
   177
      and thy = Thm.theory_of_thm th
c6bbeca3ee06 clarified special incr_type_indexes;
wenzelm
parents: 43301
diff changeset
   178
      fun inc_tvar ((a,i),s) = pairself (ctyp_of thy) (TVar ((a,i),s), TVar ((a,i+inc),s))
c6bbeca3ee06 clarified special incr_type_indexes;
wenzelm
parents: 43301
diff changeset
   179
  in Thm.instantiate (map inc_tvar tvs, []) th end;
c6bbeca3ee06 clarified special incr_type_indexes;
wenzelm
parents: 43301
diff changeset
   180
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   181
(* Like RSN, but we rename apart only the type variables. Vars here typically
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   182
   have an index of 1, and the use of RSN would increase this typically to 3.
43300
854f667df3d6 removed more dead code
blanchet
parents: 43298
diff changeset
   183
   Instantiations of those Vars could then fail. *)
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   184
fun resolve_inc_tyvars thy tha i thb =
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   185
  let
43330
c6bbeca3ee06 clarified special incr_type_indexes;
wenzelm
parents: 43301
diff changeset
   186
    val tha = incr_type_indexes (1 + Thm.maxidx_of thb) tha
43359
blanchet
parents: 43333
diff changeset
   187
    fun aux (tha, thb) =
52223
5bb6ae8acb87 tuned signature -- more explicit flags for low-level Thm.bicompose;
wenzelm
parents: 52178
diff changeset
   188
      case Thm.bicompose {flatten = true, match = false, incremented = false}
5bb6ae8acb87 tuned signature -- more explicit flags for low-level Thm.bicompose;
wenzelm
parents: 52178
diff changeset
   189
            (false, tha, nprems_of tha) i thb
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   190
           |> Seq.list_of |> distinct Thm.eq_thm of
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   191
        [th] => th
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   192
      | _ => raise THM ("resolve_inc_tyvars: unique result expected", i,
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   193
                        [tha, thb])
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   194
  in
43359
blanchet
parents: 43333
diff changeset
   195
    aux (tha, thb)
52223
5bb6ae8acb87 tuned signature -- more explicit flags for low-level Thm.bicompose;
wenzelm
parents: 52178
diff changeset
   196
    handle TERM z =>  (* FIXME obsolete!? *)
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   197
           (* The unifier, which is invoked from "Thm.bicompose", will sometimes
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   198
              refuse to unify "?a::?'a" with "?a::?'b" or "?a::nat" and throw a
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   199
              "TERM" exception (with "add_ffpair" as first argument). We then
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   200
              perform unification of the types of variables by hand and try
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   201
              again. We could do this the first time around but this error
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   202
              occurs seldom and we don't want to break existing proofs in subtle
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   203
              ways or slow them down needlessly. *)
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   204
           case [] |> fold (Term.add_vars o prop_of) [tha, thb]
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   205
                   |> AList.group (op =)
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   206
                   |> maps (fn ((s, _), T :: Ts) =>
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   207
                               map (fn T' => (Free (s, T), Free (s, T'))) Ts)
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   208
                   |> rpair (Envir.empty ~1)
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   209
                   |-> fold (Pattern.unify thy)
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   210
                   |> Envir.type_env |> Vartab.dest
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   211
                   |> map (fn (x, (S, T)) =>
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   212
                              pairself (ctyp_of thy) (TVar (x, S), T)) of
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   213
             [] => raise TERM z
43359
blanchet
parents: 43333
diff changeset
   214
           | ps => (tha, thb) |> pairself (Drule.instantiate_normalize (ps, []))
blanchet
parents: 43333
diff changeset
   215
                              |> aux
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   216
  end
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   217
40221
d10b68c6e6d4 do not let Metis be confused by higher-order reasoning leading to literals of the form "~ ~ p", which are really the same as "p"
blanchet
parents: 40158
diff changeset
   218
fun s_not (@{const Not} $ t) = t
d10b68c6e6d4 do not let Metis be confused by higher-order reasoning leading to literals of the form "~ ~ p", which are really the same as "p"
blanchet
parents: 40158
diff changeset
   219
  | s_not t = HOLogic.mk_not t
43195
6dc58b3b73b5 improved correctness of handling of higher-order occurrences of "Not" in new Metis (and probably in old Metis)
blanchet
parents: 43187
diff changeset
   220
fun simp_not_not (@{const Trueprop} $ t) = @{const Trueprop} $ simp_not_not t
6dc58b3b73b5 improved correctness of handling of higher-order occurrences of "Not" in new Metis (and probably in old Metis)
blanchet
parents: 43187
diff changeset
   221
  | simp_not_not (@{const Not} $ t) = s_not (simp_not_not t)
40221
d10b68c6e6d4 do not let Metis be confused by higher-order reasoning leading to literals of the form "~ ~ p", which are really the same as "p"
blanchet
parents: 40158
diff changeset
   222
  | simp_not_not t = t
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   223
43195
6dc58b3b73b5 improved correctness of handling of higher-order occurrences of "Not" in new Metis (and probably in old Metis)
blanchet
parents: 43187
diff changeset
   224
val normalize_literal = simp_not_not o Envir.eta_contract
6dc58b3b73b5 improved correctness of handling of higher-order occurrences of "Not" in new Metis (and probably in old Metis)
blanchet
parents: 43187
diff changeset
   225
43187
95bd1ef1331a make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents: 43186
diff changeset
   226
(* Find the relative location of an untyped term within a list of terms as a
95bd1ef1331a make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents: 43186
diff changeset
   227
   1-based index. Returns 0 in case of failure. *)
40221
d10b68c6e6d4 do not let Metis be confused by higher-order reasoning leading to literals of the form "~ ~ p", which are really the same as "p"
blanchet
parents: 40158
diff changeset
   228
fun index_of_literal lit haystack =
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   229
  let
43195
6dc58b3b73b5 improved correctness of handling of higher-order occurrences of "Not" in new Metis (and probably in old Metis)
blanchet
parents: 43187
diff changeset
   230
    fun match_lit normalize =
43134
0c82e00ba63e make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents: 43130
diff changeset
   231
      HOLogic.dest_Trueprop #> normalize
43301
8d7fc4a5b502 removed needless function that duplicated standard functionality, with a little unnecessary twist
blanchet
parents: 43300
diff changeset
   232
      #> curry Term.aconv_untyped (lit |> normalize)
43195
6dc58b3b73b5 improved correctness of handling of higher-order occurrences of "Not" in new Metis (and probably in old Metis)
blanchet
parents: 43187
diff changeset
   233
  in
6dc58b3b73b5 improved correctness of handling of higher-order occurrences of "Not" in new Metis (and probably in old Metis)
blanchet
parents: 43187
diff changeset
   234
    (case find_index (match_lit I) haystack of
6dc58b3b73b5 improved correctness of handling of higher-order occurrences of "Not" in new Metis (and probably in old Metis)
blanchet
parents: 43187
diff changeset
   235
       ~1 => find_index (match_lit (simp_not_not o Envir.eta_contract)) haystack
6dc58b3b73b5 improved correctness of handling of higher-order occurrences of "Not" in new Metis (and probably in old Metis)
blanchet
parents: 43187
diff changeset
   236
     | j => j) + 1
6dc58b3b73b5 improved correctness of handling of higher-order occurrences of "Not" in new Metis (and probably in old Metis)
blanchet
parents: 43187
diff changeset
   237
  end
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   238
39893
25a339e1ff9b move functions closer to where they're used
blanchet
parents: 39887
diff changeset
   239
(* Permute a rule's premises to move the i-th premise to the last position. *)
25a339e1ff9b move functions closer to where they're used
blanchet
parents: 39887
diff changeset
   240
fun make_last i th =
25a339e1ff9b move functions closer to where they're used
blanchet
parents: 39887
diff changeset
   241
  let val n = nprems_of th
25a339e1ff9b move functions closer to where they're used
blanchet
parents: 39887
diff changeset
   242
  in  if 1 <= i andalso i <= n
25a339e1ff9b move functions closer to where they're used
blanchet
parents: 39887
diff changeset
   243
      then Thm.permute_prems (i-1) 1 th
25a339e1ff9b move functions closer to where they're used
blanchet
parents: 39887
diff changeset
   244
      else raise THM("select_literal", i, [th])
25a339e1ff9b move functions closer to where they're used
blanchet
parents: 39887
diff changeset
   245
  end;
25a339e1ff9b move functions closer to where they're used
blanchet
parents: 39887
diff changeset
   246
42348
187354e22c7d improve on 0b05cc14c2cb: make sure that a literal variable "?foo" isn't accidentally renamed "?Q", which might be enough to confuse the new Skolemizer (cf. "Clausify.thy" example)
blanchet
parents: 42344
diff changeset
   247
(* Maps a rule that ends "... ==> P ==> False" to "... ==> ~ P" while avoiding
42349
721e85fd2db3 make 48170228f562 work also with "HO_Reas" examples
blanchet
parents: 42348
diff changeset
   248
   to create double negations. The "select" wrapper is a trick to ensure that
721e85fd2db3 make 48170228f562 work also with "HO_Reas" examples
blanchet
parents: 42348
diff changeset
   249
   "P ==> ~ False ==> False" is rewritten to "P ==> False", not to "~ P". We
721e85fd2db3 make 48170228f562 work also with "HO_Reas" examples
blanchet
parents: 42348
diff changeset
   250
   don't use this trick in general because it makes the proof object uglier than
721e85fd2db3 make 48170228f562 work also with "HO_Reas" examples
blanchet
parents: 42348
diff changeset
   251
   necessary. FIXME. *)
721e85fd2db3 make 48170228f562 work also with "HO_Reas" examples
blanchet
parents: 42348
diff changeset
   252
fun negate_head th =
721e85fd2db3 make 48170228f562 work also with "HO_Reas" examples
blanchet
parents: 42348
diff changeset
   253
  if exists (fn t => t aconv @{prop "~ False"}) (prems_of th) then
721e85fd2db3 make 48170228f562 work also with "HO_Reas" examples
blanchet
parents: 42348
diff changeset
   254
    (th RS @{thm select_FalseI})
721e85fd2db3 make 48170228f562 work also with "HO_Reas" examples
blanchet
parents: 42348
diff changeset
   255
    |> fold (rewrite_rule o single)
721e85fd2db3 make 48170228f562 work also with "HO_Reas" examples
blanchet
parents: 42348
diff changeset
   256
            @{thms not_atomize_select atomize_not_select}
721e85fd2db3 make 48170228f562 work also with "HO_Reas" examples
blanchet
parents: 42348
diff changeset
   257
  else
721e85fd2db3 make 48170228f562 work also with "HO_Reas" examples
blanchet
parents: 42348
diff changeset
   258
    th |> fold (rewrite_rule o single) @{thms not_atomize atomize_not}
39893
25a339e1ff9b move functions closer to where they're used
blanchet
parents: 39887
diff changeset
   259
25a339e1ff9b move functions closer to where they're used
blanchet
parents: 39887
diff changeset
   260
(* Maps the clause  [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *)
42348
187354e22c7d improve on 0b05cc14c2cb: make sure that a literal variable "?foo" isn't accidentally renamed "?Q", which might be enough to confuse the new Skolemizer (cf. "Clausify.thy" example)
blanchet
parents: 42344
diff changeset
   261
val select_literal = negate_head oo make_last
39893
25a339e1ff9b move functions closer to where they're used
blanchet
parents: 39887
diff changeset
   262
45508
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 44492
diff changeset
   263
fun resolve_inference ctxt type_enc concealed sym_tab th_pairs atom th1 th2 =
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   264
  let
43094
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
   265
    val (i_th1, i_th2) = pairself (lookth th_pairs) (th1, th2)
43187
95bd1ef1331a make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents: 43186
diff changeset
   266
    val _ = trace_msg ctxt (fn () =>
95bd1ef1331a make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents: 43186
diff changeset
   267
        "  isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1 ^ "\n\
95bd1ef1331a make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents: 43186
diff changeset
   268
        \  isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   269
  in
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   270
    (* Trivial cases where one operand is type info *)
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   271
    if Thm.eq_thm (TrueI, i_th1) then
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   272
      i_th2
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   273
    else if Thm.eq_thm (TrueI, i_th2) then
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   274
      i_th1
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   275
    else
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   276
      let
43187
95bd1ef1331a make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents: 43186
diff changeset
   277
        val thy = Proof_Context.theory_of ctxt
95bd1ef1331a make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents: 43186
diff changeset
   278
        val i_atom =
52031
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51998
diff changeset
   279
          singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab)
43187
95bd1ef1331a make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents: 43186
diff changeset
   280
                    (Metis_Term.Fn atom)
95bd1ef1331a make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents: 43186
diff changeset
   281
        val _ = trace_msg ctxt (fn () =>
95bd1ef1331a make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents: 43186
diff changeset
   282
                    "  atom: " ^ Syntax.string_of_term ctxt i_atom)
95bd1ef1331a make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents: 43186
diff changeset
   283
      in
95bd1ef1331a make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents: 43186
diff changeset
   284
        case index_of_literal (s_not i_atom) (prems_of i_th1) of
95bd1ef1331a make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents: 43186
diff changeset
   285
          0 =>
95bd1ef1331a make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents: 43186
diff changeset
   286
          (trace_msg ctxt (fn () => "Failed to find literal in \"th1\"");
95bd1ef1331a make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents: 43186
diff changeset
   287
           i_th1)
95bd1ef1331a make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents: 43186
diff changeset
   288
        | j1 =>
95bd1ef1331a make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents: 43186
diff changeset
   289
          (trace_msg ctxt (fn () => "  index th1: " ^ string_of_int j1);
95bd1ef1331a make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents: 43186
diff changeset
   290
           case index_of_literal i_atom (prems_of i_th2) of
95bd1ef1331a make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents: 43186
diff changeset
   291
             0 =>
95bd1ef1331a make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents: 43186
diff changeset
   292
             (trace_msg ctxt (fn () => "Failed to find literal in \"th2\"");
95bd1ef1331a make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents: 43186
diff changeset
   293
              i_th2)
95bd1ef1331a make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents: 43186
diff changeset
   294
           | j2 =>
95bd1ef1331a make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents: 43186
diff changeset
   295
             (trace_msg ctxt (fn () => "  index th2: " ^ string_of_int j2);
95bd1ef1331a make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents: 43186
diff changeset
   296
              resolve_inc_tyvars thy (select_literal j1 i_th1) j2 i_th2
50875
bfb626265782 less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents: 48132
diff changeset
   297
              handle TERM (s, _) =>
bfb626265782 less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents: 48132
diff changeset
   298
                     raise METIS_RECONSTRUCT ("resolve_inference", s)))
43187
95bd1ef1331a make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents: 43186
diff changeset
   299
      end
95bd1ef1331a make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents: 43186
diff changeset
   300
  end
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   301
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   302
(* INFERENCE RULE: REFL *)
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   303
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   304
val REFL_THM = Thm.incr_indexes 2 @{lemma "t ~= t ==> False" by simp}
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   305
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   306
val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   307
val refl_idx = 1 + Thm.maxidx_of REFL_THM;
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   308
45508
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 44492
diff changeset
   309
fun refl_inference ctxt type_enc concealed sym_tab t =
43094
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
   310
  let
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
   311
    val thy = Proof_Context.theory_of ctxt
44492
a330c0608da8 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents: 44241
diff changeset
   312
    val i_t =
52031
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51998
diff changeset
   313
      singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab) t
43094
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
   314
    val _ = trace_msg ctxt (fn () => "  term: " ^ Syntax.string_of_term ctxt i_t)
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
   315
    val c_t = cterm_incr_types thy refl_idx i_t
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
   316
  in cterm_instantiate [(refl_x, c_t)] REFL_THM end
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   317
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   318
(* INFERENCE RULE: EQUALITY *)
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   319
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   320
val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp}
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   321
val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp}
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   322
45508
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 44492
diff changeset
   323
fun equality_inference ctxt type_enc concealed sym_tab (pos, atom) fp fr =
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42354
diff changeset
   324
  let val thy = Proof_Context.theory_of ctxt
43187
95bd1ef1331a make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents: 43186
diff changeset
   325
      val m_tm = Metis_Term.Fn atom
95bd1ef1331a make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents: 43186
diff changeset
   326
      val [i_atom, i_tm] =
52031
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51998
diff changeset
   327
        hol_terms_of_metis ctxt type_enc concealed sym_tab [m_tm, fr]
51951
fab4ab92e812 more standard Isabelle/ML operations -- avoid inaccurate Bool.fromString;
wenzelm
parents: 51929
diff changeset
   328
      val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Markup.print_bool pos)
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   329
      fun replace_item_list lx 0 (_::ls) = lx::ls
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   330
        | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
43205
23b81469499f more preparations towards hijacking Metis
blanchet
parents: 43195
diff changeset
   331
      fun path_finder_fail tm ps t =
50875
bfb626265782 less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents: 48132
diff changeset
   332
        raise METIS_RECONSTRUCT ("equality_inference (path_finder)",
bfb626265782 less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents: 48132
diff changeset
   333
                  "path = " ^ space_implode " " (map string_of_int ps) ^
bfb626265782 less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents: 48132
diff changeset
   334
                  " isa-term: " ^ Syntax.string_of_term ctxt tm ^
bfb626265782 less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents: 48132
diff changeset
   335
                  (case t of
bfb626265782 less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents: 48132
diff changeset
   336
                     SOME t => " fol-term: " ^ Metis_Term.toString t
bfb626265782 less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents: 48132
diff changeset
   337
                   | NONE => ""))
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43209
diff changeset
   338
      fun path_finder tm [] _ = (tm, Bound 0)
050a03afe024 Metis code cleanup
blanchet
parents: 43209
diff changeset
   339
        | path_finder tm (p :: ps) (t as Metis_Term.Fn (s, ts)) =
43177
5017d436a572 properly unmangle names in path finder
blanchet
parents: 43174
diff changeset
   340
          let
43268
c0eaa8b9bff5 removed yet another hack in "make_metis" script -- respect opacity of "Metis_Name.name"
blanchet
parents: 43262
diff changeset
   341
            val s = s |> Metis_Name.toString
45511
9b0f8ca4388e continued implementation of lambda-lifting in Metis
blanchet
parents: 45508
diff changeset
   342
                      |> perhaps (try (unprefix_and_unascii const_prefix
46392
676a4b4b6e73 implemented partial application aliases (for SPASS mainly)
blanchet
parents: 46320
diff changeset
   343
                                       #> the #> unmangled_const_name #> hd))
43177
5017d436a572 properly unmangle names in path finder
blanchet
parents: 43174
diff changeset
   344
          in
5017d436a572 properly unmangle names in path finder
blanchet
parents: 43174
diff changeset
   345
            if s = metis_predicator orelse s = predicator_name orelse
44492
a330c0608da8 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents: 44241
diff changeset
   346
               s = metis_systematic_type_tag orelse s = metis_ad_hoc_type_tag
a330c0608da8 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents: 44241
diff changeset
   347
               orelse s = type_tag_name then
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43209
diff changeset
   348
              path_finder tm ps (nth ts p)
43177
5017d436a572 properly unmangle names in path finder
blanchet
parents: 43174
diff changeset
   349
            else if s = metis_app_op orelse s = app_op_name then
43130
d73fc2e55308 implemented missing hAPP and ti cases of new path finder
blanchet
parents: 43128
diff changeset
   350
              let
d73fc2e55308 implemented missing hAPP and ti cases of new path finder
blanchet
parents: 43128
diff changeset
   351
                val (tm1, tm2) = dest_comb tm
d73fc2e55308 implemented missing hAPP and ti cases of new path finder
blanchet
parents: 43128
diff changeset
   352
                val p' = p - (length ts - 2)
d73fc2e55308 implemented missing hAPP and ti cases of new path finder
blanchet
parents: 43128
diff changeset
   353
              in
d73fc2e55308 implemented missing hAPP and ti cases of new path finder
blanchet
parents: 43128
diff changeset
   354
                if p' = 0 then
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43209
diff changeset
   355
                  path_finder tm1 ps (nth ts p) ||> (fn y => y $ tm2)
43130
d73fc2e55308 implemented missing hAPP and ti cases of new path finder
blanchet
parents: 43128
diff changeset
   356
                else
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43209
diff changeset
   357
                  path_finder tm2 ps (nth ts p) ||> (fn y => tm1 $ y)
43130
d73fc2e55308 implemented missing hAPP and ti cases of new path finder
blanchet
parents: 43128
diff changeset
   358
              end
d73fc2e55308 implemented missing hAPP and ti cases of new path finder
blanchet
parents: 43128
diff changeset
   359
            else
d73fc2e55308 implemented missing hAPP and ti cases of new path finder
blanchet
parents: 43128
diff changeset
   360
              let
d73fc2e55308 implemented missing hAPP and ti cases of new path finder
blanchet
parents: 43128
diff changeset
   361
                val (tm1, args) = strip_comb tm
d73fc2e55308 implemented missing hAPP and ti cases of new path finder
blanchet
parents: 43128
diff changeset
   362
                val adjustment = length ts - length args
d73fc2e55308 implemented missing hAPP and ti cases of new path finder
blanchet
parents: 43128
diff changeset
   363
                val p' = if adjustment > p then p else p - adjustment
43205
23b81469499f more preparations towards hijacking Metis
blanchet
parents: 43195
diff changeset
   364
                val tm_p =
23b81469499f more preparations towards hijacking Metis
blanchet
parents: 43195
diff changeset
   365
                  nth args p'
43278
1fbdcebb364b more robust exception pattern General.Subscript;
wenzelm
parents: 43268
diff changeset
   366
                  handle General.Subscript => path_finder_fail tm (p :: ps) (SOME t)
43130
d73fc2e55308 implemented missing hAPP and ti cases of new path finder
blanchet
parents: 43128
diff changeset
   367
                val _ = trace_msg ctxt (fn () =>
d73fc2e55308 implemented missing hAPP and ti cases of new path finder
blanchet
parents: 43128
diff changeset
   368
                    "path_finder: " ^ string_of_int p ^ "  " ^
d73fc2e55308 implemented missing hAPP and ti cases of new path finder
blanchet
parents: 43128
diff changeset
   369
                    Syntax.string_of_term ctxt tm_p)
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43209
diff changeset
   370
                val (r, t) = path_finder tm_p ps (nth ts p)
43130
d73fc2e55308 implemented missing hAPP and ti cases of new path finder
blanchet
parents: 43128
diff changeset
   371
              in (r, list_comb (tm1, replace_item_list t p' args)) end
d73fc2e55308 implemented missing hAPP and ti cases of new path finder
blanchet
parents: 43128
diff changeset
   372
          end
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43209
diff changeset
   373
        | path_finder tm ps t = path_finder_fail tm ps (SOME t)
050a03afe024 Metis code cleanup
blanchet
parents: 43209
diff changeset
   374
      val (tm_subst, body) = path_finder i_atom fp m_tm
39498
e8aef7ea9cbb make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents: 39497
diff changeset
   375
      val tm_abs = Abs ("x", type_of tm_subst, body)
39978
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
   376
      val _ = trace_msg ctxt (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
   377
      val _ = trace_msg ctxt (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
   378
      val _ = trace_msg ctxt (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   379
      val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst)  (*ill typed but gives right max*)
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   380
      val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
39978
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
   381
      val _ = trace_msg ctxt (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   382
      val eq_terms = map (pairself (cterm_of thy))
44121
44adaa6db327 old term operations are legacy;
wenzelm
parents: 43359
diff changeset
   383
        (ListPair.zip (Misc_Legacy.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   384
  in  cterm_instantiate eq_terms subst'  end;
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   385
43094
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
   386
val factor = Seq.hd o distinct_subgoals_tac
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   387
45508
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 44492
diff changeset
   388
fun one_step ctxt type_enc concealed sym_tab th_pairs p =
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   389
  case p of
43186
blanchet
parents: 43184
diff changeset
   390
    (fol_th, Metis_Proof.Axiom _) => axiom_inference th_pairs fol_th |> factor
43187
95bd1ef1331a make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents: 43186
diff changeset
   391
  | (_, Metis_Proof.Assume f_atom) =>
45508
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 44492
diff changeset
   392
    assume_inference ctxt type_enc concealed sym_tab f_atom
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   393
  | (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) =>
45508
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 44492
diff changeset
   394
    inst_inference ctxt type_enc concealed sym_tab th_pairs f_subst f_th1
43186
blanchet
parents: 43184
diff changeset
   395
    |> factor
43187
95bd1ef1331a make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents: 43186
diff changeset
   396
  | (_, Metis_Proof.Resolve(f_atom, f_th1, f_th2)) =>
45508
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 44492
diff changeset
   397
    resolve_inference ctxt type_enc concealed sym_tab th_pairs f_atom f_th1
44492
a330c0608da8 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents: 44241
diff changeset
   398
                      f_th2
43094
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
   399
    |> factor
43186
blanchet
parents: 43184
diff changeset
   400
  | (_, Metis_Proof.Refl f_tm) =>
45508
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 44492
diff changeset
   401
    refl_inference ctxt type_enc concealed sym_tab f_tm
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   402
  | (_, Metis_Proof.Equality (f_lit, f_p, f_r)) =>
45508
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 44492
diff changeset
   403
    equality_inference ctxt type_enc concealed sym_tab f_lit f_p f_r
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   404
39893
25a339e1ff9b move functions closer to where they're used
blanchet
parents: 39887
diff changeset
   405
fun flexflex_first_order th =
25a339e1ff9b move functions closer to where they're used
blanchet
parents: 39887
diff changeset
   406
  case Thm.tpairs_of th of
25a339e1ff9b move functions closer to where they're used
blanchet
parents: 39887
diff changeset
   407
      [] => th
25a339e1ff9b move functions closer to where they're used
blanchet
parents: 39887
diff changeset
   408
    | pairs =>
25a339e1ff9b move functions closer to where they're used
blanchet
parents: 39887
diff changeset
   409
        let val thy = theory_of_thm th
52178
6228806b2605 instantiate types as well (see also Thm.first_order_match);
wenzelm
parents: 52031
diff changeset
   410
            val cert = cterm_of thy
6228806b2605 instantiate types as well (see also Thm.first_order_match);
wenzelm
parents: 52031
diff changeset
   411
            val certT = ctyp_of thy
6228806b2605 instantiate types as well (see also Thm.first_order_match);
wenzelm
parents: 52031
diff changeset
   412
            val (tyenv, tenv) =
39893
25a339e1ff9b move functions closer to where they're used
blanchet
parents: 39887
diff changeset
   413
              fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
52178
6228806b2605 instantiate types as well (see also Thm.first_order_match);
wenzelm
parents: 52031
diff changeset
   414
            fun mkT (v, (S, T)) = (certT (TVar (v, S)), certT T)
6228806b2605 instantiate types as well (see also Thm.first_order_match);
wenzelm
parents: 52031
diff changeset
   415
            fun mk (v, (T, t)) =
6228806b2605 instantiate types as well (see also Thm.first_order_match);
wenzelm
parents: 52031
diff changeset
   416
              let val T' = Envir.subst_type tyenv T
6228806b2605 instantiate types as well (see also Thm.first_order_match);
wenzelm
parents: 52031
diff changeset
   417
              in (cert (Var (v, T')), cert t) end
6228806b2605 instantiate types as well (see also Thm.first_order_match);
wenzelm
parents: 52031
diff changeset
   418
            val instsT = Vartab.fold (cons o mkT) tyenv []
6228806b2605 instantiate types as well (see also Thm.first_order_match);
wenzelm
parents: 52031
diff changeset
   419
            val insts = Vartab.fold (cons o mk) tenv []
6228806b2605 instantiate types as well (see also Thm.first_order_match);
wenzelm
parents: 52031
diff changeset
   420
            val th' = Thm.instantiate (instsT, insts) th
39893
25a339e1ff9b move functions closer to where they're used
blanchet
parents: 39887
diff changeset
   421
        in  th'  end
25a339e1ff9b move functions closer to where they're used
blanchet
parents: 39887
diff changeset
   422
        handle THM _ => th;
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   423
43268
c0eaa8b9bff5 removed yet another hack in "make_metis" script -- respect opacity of "Metis_Name.name"
blanchet
parents: 43262
diff changeset
   424
fun is_metis_literal_genuine (_, (s, _)) =
c0eaa8b9bff5 removed yet another hack in "make_metis" script -- respect opacity of "Metis_Name.name"
blanchet
parents: 43262
diff changeset
   425
  not (String.isPrefix class_prefix (Metis_Name.toString s))
39895
a91a84b1dfdd reintroduced code that keeps track of whether the Isabelle and Metis proofs are in sync -- generalized to work with the new skolemizer
blanchet
parents: 39893
diff changeset
   426
fun is_isabelle_literal_genuine t =
39953
aa54f347e5e2 hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents: 39946
diff changeset
   427
  case t of _ $ (Const (@{const_name Meson.skolem}, _) $ _) => false | _ => true
39895
a91a84b1dfdd reintroduced code that keeps track of whether the Isabelle and Metis proofs are in sync -- generalized to work with the new skolemizer
blanchet
parents: 39893
diff changeset
   428
a91a84b1dfdd reintroduced code that keeps track of whether the Isabelle and Metis proofs are in sync -- generalized to work with the new skolemizer
blanchet
parents: 39893
diff changeset
   429
fun count p xs = fold (fn x => if p x then Integer.add 1 else I) xs 0
a91a84b1dfdd reintroduced code that keeps track of whether the Isabelle and Metis proofs are in sync -- generalized to work with the new skolemizer
blanchet
parents: 39893
diff changeset
   430
42333
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42271
diff changeset
   431
(* Seldomly needed hack. A Metis clause is represented as a set, so duplicate
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42271
diff changeset
   432
   disjuncts are impossible. In the Isabelle proof, in spite of efforts to
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42271
diff changeset
   433
   eliminate them, duplicates sometimes appear with slightly different (but
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42271
diff changeset
   434
   unifiable) types. *)
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42271
diff changeset
   435
fun resynchronize ctxt fol_th th =
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42271
diff changeset
   436
  let
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42271
diff changeset
   437
    val num_metis_lits =
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42271
diff changeset
   438
      count is_metis_literal_genuine
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42271
diff changeset
   439
            (Metis_LiteralSet.toList (Metis_Thm.clause fol_th))
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42271
diff changeset
   440
    val num_isabelle_lits = count is_isabelle_literal_genuine (prems_of th)
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42271
diff changeset
   441
  in
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42271
diff changeset
   442
    if num_metis_lits >= num_isabelle_lits then
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42271
diff changeset
   443
      th
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42271
diff changeset
   444
    else
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42271
diff changeset
   445
      let
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42271
diff changeset
   446
        val (prems0, concl) = th |> prop_of |> Logic.strip_horn
43195
6dc58b3b73b5 improved correctness of handling of higher-order occurrences of "Not" in new Metis (and probably in old Metis)
blanchet
parents: 43187
diff changeset
   447
        val prems = prems0 |> map normalize_literal
43301
8d7fc4a5b502 removed needless function that duplicated standard functionality, with a little unnecessary twist
blanchet
parents: 43300
diff changeset
   448
                           |> distinct Term.aconv_untyped
42333
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42271
diff changeset
   449
        val goal = Logic.list_implies (prems, concl)
46708
b138dee7bed3 prefer cut_tac, where it is clear that the special variants cut_rules_tac or cut_facts_tac are not required;
wenzelm
parents: 46392
diff changeset
   450
        val tac = cut_tac th 1
43195
6dc58b3b73b5 improved correctness of handling of higher-order occurrences of "Not" in new Metis (and probably in old Metis)
blanchet
parents: 43187
diff changeset
   451
                  THEN rewrite_goals_tac @{thms not_not [THEN eq_reflection]}
6dc58b3b73b5 improved correctness of handling of higher-order occurrences of "Not" in new Metis (and probably in old Metis)
blanchet
parents: 43187
diff changeset
   452
                  THEN ALLGOALS assume_tac
42333
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42271
diff changeset
   453
      in
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42271
diff changeset
   454
        if length prems = length prems0 then
50875
bfb626265782 less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents: 48132
diff changeset
   455
          raise METIS_RECONSTRUCT ("resynchronize", "Out of sync")
42333
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42271
diff changeset
   456
        else
43195
6dc58b3b73b5 improved correctness of handling of higher-order occurrences of "Not" in new Metis (and probably in old Metis)
blanchet
parents: 43187
diff changeset
   457
          Goal.prove ctxt [] [] goal (K tac)
42333
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42271
diff changeset
   458
          |> resynchronize ctxt fol_th
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42271
diff changeset
   459
      end
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42271
diff changeset
   460
  end
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42271
diff changeset
   461
45508
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 44492
diff changeset
   462
fun replay_one_inference ctxt type_enc concealed sym_tab (fol_th, inf)
44492
a330c0608da8 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents: 44241
diff changeset
   463
                         th_pairs =
43094
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
   464
  if not (null th_pairs) andalso
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
   465
     prop_of (snd (hd th_pairs)) aconv @{prop False} then
40868
177cd660abb7 give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one -- this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents: 40724
diff changeset
   466
    (* Isabelle sometimes identifies literals (premises) that are distinct in
177cd660abb7 give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one -- this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents: 40724
diff changeset
   467
       Metis (e.g., because of type variables). We give the Isabelle proof the
177cd660abb7 give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one -- this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents: 40724
diff changeset
   468
       benefice of the doubt. *)
43094
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
   469
    th_pairs
40868
177cd660abb7 give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one -- this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents: 40724
diff changeset
   470
  else
177cd660abb7 give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one -- this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents: 40724
diff changeset
   471
    let
177cd660abb7 give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one -- this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents: 40724
diff changeset
   472
      val _ = trace_msg ctxt
177cd660abb7 give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one -- this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents: 40724
diff changeset
   473
                  (fn () => "=============================================")
177cd660abb7 give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one -- this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents: 40724
diff changeset
   474
      val _ = trace_msg ctxt
177cd660abb7 give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one -- this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents: 40724
diff changeset
   475
                  (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)
177cd660abb7 give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one -- this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents: 40724
diff changeset
   476
      val _ = trace_msg ctxt
177cd660abb7 give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one -- this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents: 40724
diff changeset
   477
                  (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)
45508
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 44492
diff changeset
   478
      val th = one_step ctxt type_enc concealed sym_tab th_pairs (fol_th, inf)
40868
177cd660abb7 give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one -- this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents: 40724
diff changeset
   479
               |> flexflex_first_order
42333
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42271
diff changeset
   480
               |> resynchronize ctxt fol_th
40868
177cd660abb7 give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one -- this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents: 40724
diff changeset
   481
      val _ = trace_msg ctxt
177cd660abb7 give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one -- this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents: 40724
diff changeset
   482
                  (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
177cd660abb7 give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one -- this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents: 40724
diff changeset
   483
      val _ = trace_msg ctxt
177cd660abb7 give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one -- this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents: 40724
diff changeset
   484
                  (fn () => "=============================================")
43094
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
   485
    in (fol_th, th) :: th_pairs end
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   486
42342
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42341
diff changeset
   487
(* It is normally sufficient to apply "assume_tac" to unify the conclusion with
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42341
diff changeset
   488
   one of the premises. Unfortunately, this sometimes yields "Variable
51701
1e29891759c4 tuned exceptions -- avoid composing error messages in low-level situations;
wenzelm
parents: 50875
diff changeset
   489
   has two distinct types" errors. To avoid this, we instantiate the
42342
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42341
diff changeset
   490
   variables before applying "assume_tac". Typical constraints are of the form
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42341
diff changeset
   491
     ?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,
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42341
diff changeset
   492
   where the nonvariables are goal parameters. *)
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42341
diff changeset
   493
fun unify_first_prem_with_concl thy i th =
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42341
diff changeset
   494
  let
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42341
diff changeset
   495
    val goal = Logic.get_goal (prop_of th) i |> Envir.beta_eta_contract
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42341
diff changeset
   496
    val prem = goal |> Logic.strip_assums_hyp |> hd
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42341
diff changeset
   497
    val concl = goal |> Logic.strip_assums_concl
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42341
diff changeset
   498
    fun pair_untyped_aconv (t1, t2) (u1, u2) =
43301
8d7fc4a5b502 removed needless function that duplicated standard functionality, with a little unnecessary twist
blanchet
parents: 43300
diff changeset
   499
      Term.aconv_untyped (t1, u1) andalso Term.aconv_untyped (t2, u2)
42342
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42341
diff changeset
   500
    fun add_terms tp inst =
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42341
diff changeset
   501
      if exists (pair_untyped_aconv tp) inst then inst
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42341
diff changeset
   502
      else tp :: map (apsnd (subst_atomic [tp])) inst
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42341
diff changeset
   503
    fun is_flex t =
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42341
diff changeset
   504
      case strip_comb t of
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42341
diff changeset
   505
        (Var _, args) => forall is_Bound args
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42341
diff changeset
   506
      | _ => false
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42341
diff changeset
   507
    fun unify_flex flex rigid =
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42341
diff changeset
   508
      case strip_comb flex of
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42341
diff changeset
   509
        (Var (z as (_, T)), args) =>
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42341
diff changeset
   510
        add_terms (Var z,
44241
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 44121
diff changeset
   511
          fold_rev absdummy (take (length args) (binder_types T)) rigid)
42342
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42341
diff changeset
   512
      | _ => I
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42341
diff changeset
   513
    fun unify_potential_flex comb atom =
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42341
diff changeset
   514
      if is_flex comb then unify_flex comb atom
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42341
diff changeset
   515
      else if is_Var atom then add_terms (atom, comb)
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42341
diff changeset
   516
      else I
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42341
diff changeset
   517
    fun unify_terms (t, u) =
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42341
diff changeset
   518
      case (t, u) of
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42341
diff changeset
   519
        (t1 $ t2, u1 $ u2) =>
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42341
diff changeset
   520
        if is_flex t then unify_flex t u
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42341
diff changeset
   521
        else if is_flex u then unify_flex u t
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42341
diff changeset
   522
        else fold unify_terms [(t1, u1), (t2, u2)]
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42341
diff changeset
   523
      | (_ $ _, _) => unify_potential_flex t u
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42341
diff changeset
   524
      | (_, _ $ _) => unify_potential_flex u t
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42341
diff changeset
   525
      | (Var _, _) => add_terms (t, u)
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42341
diff changeset
   526
      | (_, Var _) => add_terms (u, t)
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42341
diff changeset
   527
      | _ => I
42344
4a58173ffb99 "unify_first_prem_with_concl" (cf. 9ceb585c097a) sometimes throws an exception, but it is very rarely needed -- catch the exception for now
blanchet
parents: 42342
diff changeset
   528
    val t_inst =
4a58173ffb99 "unify_first_prem_with_concl" (cf. 9ceb585c097a) sometimes throws an exception, but it is very rarely needed -- catch the exception for now
blanchet
parents: 42342
diff changeset
   529
      [] |> try (unify_terms (prem, concl) #> map (pairself (cterm_of thy)))
4a58173ffb99 "unify_first_prem_with_concl" (cf. 9ceb585c097a) sometimes throws an exception, but it is very rarely needed -- catch the exception for now
blanchet
parents: 42342
diff changeset
   530
         |> the_default [] (* FIXME *)
42342
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42341
diff changeset
   531
  in th |> cterm_instantiate t_inst end
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   532
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   533
val copy_prem = @{lemma "P ==> (P ==> P ==> Q) ==> Q" by fast}
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   534
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   535
fun copy_prems_tac [] ns i =
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   536
    if forall (curry (op =) 1) ns then all_tac else copy_prems_tac (rev ns) [] i
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   537
  | copy_prems_tac (1 :: ms) ns i =
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   538
    rotate_tac 1 i THEN copy_prems_tac ms (1 :: ns) i
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   539
  | copy_prems_tac (m :: ms) ns i =
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   540
    etac copy_prem i THEN copy_prems_tac ms (m div 2 :: (m + 1) div 2 :: ns) i
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   541
42271
7d08265f181d further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents: 42270
diff changeset
   542
(* Metis generates variables of the form _nnn. *)
7d08265f181d further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents: 42270
diff changeset
   543
val is_metis_fresh_variable = String.isPrefix "_"
7d08265f181d further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents: 42270
diff changeset
   544
40258
2c0d8fe36c21 make handling of parameters more robust, by querying the goal
blanchet
parents: 40221
diff changeset
   545
fun instantiate_forall_tac thy t i st =
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   546
  let
40258
2c0d8fe36c21 make handling of parameters more robust, by querying the goal
blanchet
parents: 40221
diff changeset
   547
    val params = Logic.strip_params (Logic.get_goal (prop_of st) i) |> rev
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   548
    fun repair (t as (Var ((s, _), _))) =
40258
2c0d8fe36c21 make handling of parameters more robust, by querying the goal
blanchet
parents: 40221
diff changeset
   549
        (case find_index (fn (s', _) => s' = s) params of
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   550
           ~1 => t
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   551
         | j => Bound j)
40261
7a02144874f3 more work on new Skolemizer without Hilbert_Choice
blanchet
parents: 40259
diff changeset
   552
      | repair (t $ u) =
7a02144874f3 more work on new Skolemizer without Hilbert_Choice
blanchet
parents: 40259
diff changeset
   553
        (case (repair t, repair u) of
7a02144874f3 more work on new Skolemizer without Hilbert_Choice
blanchet
parents: 40259
diff changeset
   554
           (t as Bound j, u as Bound k) =>
7a02144874f3 more work on new Skolemizer without Hilbert_Choice
blanchet
parents: 40259
diff changeset
   555
           (* This is a rather subtle trick to repair the discrepancy between
7a02144874f3 more work on new Skolemizer without Hilbert_Choice
blanchet
parents: 40259
diff changeset
   556
              the fully skolemized term that MESON gives us (where existentials
7a02144874f3 more work on new Skolemizer without Hilbert_Choice
blanchet
parents: 40259
diff changeset
   557
              were pulled out) and the reality. *)
7a02144874f3 more work on new Skolemizer without Hilbert_Choice
blanchet
parents: 40259
diff changeset
   558
           if k > j then t else t $ u
7a02144874f3 more work on new Skolemizer without Hilbert_Choice
blanchet
parents: 40259
diff changeset
   559
         | (t, u) => t $ u)
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   560
      | repair t = t
44241
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 44121
diff changeset
   561
    val t' = t |> repair |> fold (absdummy o snd) params
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   562
    fun do_instantiate th =
42270
5f2960582e45 make new Skolemizer more robust
blanchet
parents: 42107
diff changeset
   563
      case Term.add_vars (prop_of th) []
42271
7d08265f181d further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents: 42270
diff changeset
   564
           |> filter_out ((Meson_Clausify.is_zapped_var_name orf
7d08265f181d further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents: 42270
diff changeset
   565
                           is_metis_fresh_variable) o fst o fst) of
42270
5f2960582e45 make new Skolemizer more robust
blanchet
parents: 42107
diff changeset
   566
        [] => th
42271
7d08265f181d further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents: 42270
diff changeset
   567
      | [var as (_, T)] =>
7d08265f181d further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents: 42270
diff changeset
   568
        let
7d08265f181d further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents: 42270
diff changeset
   569
          val var_binder_Ts = T |> binder_types |> take (length params) |> rev
7d08265f181d further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents: 42270
diff changeset
   570
          val var_body_T = T |> funpow (length params) range_type
7d08265f181d further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents: 42270
diff changeset
   571
          val tyenv =
7d08265f181d further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents: 42270
diff changeset
   572
            Vartab.empty |> Type.raw_unifys (fastype_of t :: map snd params,
7d08265f181d further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents: 42270
diff changeset
   573
                                             var_body_T :: var_binder_Ts)
7d08265f181d further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents: 42270
diff changeset
   574
          val env =
7d08265f181d further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents: 42270
diff changeset
   575
            Envir.Envir {maxidx = Vartab.fold (Integer.max o snd o fst) tyenv 0,
7d08265f181d further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents: 42270
diff changeset
   576
                         tenv = Vartab.empty, tyenv = tyenv}
7d08265f181d further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents: 42270
diff changeset
   577
          val ty_inst =
7d08265f181d further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents: 42270
diff changeset
   578
            Vartab.fold (fn (x, (S, T)) =>
7d08265f181d further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents: 42270
diff changeset
   579
                            cons (pairself (ctyp_of thy) (TVar (x, S), T)))
7d08265f181d further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents: 42270
diff changeset
   580
                        tyenv []
7d08265f181d further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents: 42270
diff changeset
   581
          val t_inst =
7d08265f181d further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents: 42270
diff changeset
   582
            [pairself (cterm_of thy o Envir.norm_term env) (Var var, t')]
43333
2bdec7f430d3 renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
wenzelm
parents: 43330
diff changeset
   583
        in th |> Drule.instantiate_normalize (ty_inst, t_inst) end
42271
7d08265f181d further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents: 42270
diff changeset
   584
      | _ => raise Fail "expected a single non-zapped, non-Metis Var"
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   585
  in
42271
7d08265f181d further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents: 42270
diff changeset
   586
    (DETERM (etac @{thm allE} i THEN rotate_tac ~1 i)
40258
2c0d8fe36c21 make handling of parameters more robust, by querying the goal
blanchet
parents: 40221
diff changeset
   587
     THEN PRIMITIVE do_instantiate) st
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   588
  end
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   589
41135
8c5d44c7e8af tuning: unused var
blanchet
parents: 40868
diff changeset
   590
fun fix_exists_tac t =
43162
9a8acc5adfa3 added Metis examples to test the new type encodings
blanchet
parents: 43159
diff changeset
   591
  etac @{thm exE} THEN' rename_tac [t |> dest_Var |> fst |> fst]
40261
7a02144874f3 more work on new Skolemizer without Hilbert_Choice
blanchet
parents: 40259
diff changeset
   592
7a02144874f3 more work on new Skolemizer without Hilbert_Choice
blanchet
parents: 40259
diff changeset
   593
fun release_quantifier_tac thy (skolem, t) =
41135
8c5d44c7e8af tuning: unused var
blanchet
parents: 40868
diff changeset
   594
  (if skolem then fix_exists_tac else instantiate_forall_tac thy) t
40261
7a02144874f3 more work on new Skolemizer without Hilbert_Choice
blanchet
parents: 40259
diff changeset
   595
40258
2c0d8fe36c21 make handling of parameters more robust, by querying the goal
blanchet
parents: 40221
diff changeset
   596
fun release_clusters_tac _ _ _ [] = K all_tac
2c0d8fe36c21 make handling of parameters more robust, by querying the goal
blanchet
parents: 40221
diff changeset
   597
  | release_clusters_tac thy ax_counts substs
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   598
                         ((ax_no, cluster_no) :: clusters) =
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   599
    let
40261
7a02144874f3 more work on new Skolemizer without Hilbert_Choice
blanchet
parents: 40259
diff changeset
   600
      val cluster_of_var =
7a02144874f3 more work on new Skolemizer without Hilbert_Choice
blanchet
parents: 40259
diff changeset
   601
        Meson_Clausify.cluster_of_zapped_var_name o fst o fst o dest_Var
7a02144874f3 more work on new Skolemizer without Hilbert_Choice
blanchet
parents: 40259
diff changeset
   602
      fun in_right_cluster ((_, (cluster_no', _)), _) = cluster_no' = cluster_no
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   603
      val cluster_substs =
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   604
        substs
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   605
        |> map_filter (fn (ax_no', (_, (_, tsubst))) =>
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   606
                          if ax_no' = ax_no then
40261
7a02144874f3 more work on new Skolemizer without Hilbert_Choice
blanchet
parents: 40259
diff changeset
   607
                            tsubst |> map (apfst cluster_of_var)
7a02144874f3 more work on new Skolemizer without Hilbert_Choice
blanchet
parents: 40259
diff changeset
   608
                                   |> filter (in_right_cluster o fst)
7a02144874f3 more work on new Skolemizer without Hilbert_Choice
blanchet
parents: 40259
diff changeset
   609
                                   |> map (apfst snd)
7a02144874f3 more work on new Skolemizer without Hilbert_Choice
blanchet
parents: 40259
diff changeset
   610
                                   |> SOME
7a02144874f3 more work on new Skolemizer without Hilbert_Choice
blanchet
parents: 40259
diff changeset
   611
                          else
7a02144874f3 more work on new Skolemizer without Hilbert_Choice
blanchet
parents: 40259
diff changeset
   612
                            NONE)
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   613
      fun do_cluster_subst cluster_subst =
40261
7a02144874f3 more work on new Skolemizer without Hilbert_Choice
blanchet
parents: 40259
diff changeset
   614
        map (release_quantifier_tac thy) cluster_subst @ [rotate_tac 1]
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   615
      val first_prem = find_index (fn (ax_no', _) => ax_no' = ax_no) substs
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   616
    in
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   617
      rotate_tac first_prem
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   618
      THEN' (EVERY' (maps do_cluster_subst cluster_substs))
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   619
      THEN' rotate_tac (~ first_prem - length cluster_substs)
40258
2c0d8fe36c21 make handling of parameters more robust, by querying the goal
blanchet
parents: 40221
diff changeset
   620
      THEN' release_clusters_tac thy ax_counts substs clusters
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   621
    end
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   622
40264
b91e2e16d994 fixed order of quantifier instantiation in new Skolemizer
blanchet
parents: 40261
diff changeset
   623
fun cluster_key ((ax_no, (cluster_no, index_no)), skolem) =
b91e2e16d994 fixed order of quantifier instantiation in new Skolemizer
blanchet
parents: 40261
diff changeset
   624
  (ax_no, (cluster_no, (skolem, index_no)))
b91e2e16d994 fixed order of quantifier instantiation in new Skolemizer
blanchet
parents: 40261
diff changeset
   625
fun cluster_ord p =
b91e2e16d994 fixed order of quantifier instantiation in new Skolemizer
blanchet
parents: 40261
diff changeset
   626
  prod_ord int_ord (prod_ord int_ord (prod_ord bool_ord int_ord))
b91e2e16d994 fixed order of quantifier instantiation in new Skolemizer
blanchet
parents: 40261
diff changeset
   627
           (pairself cluster_key p)
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   628
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   629
val tysubst_ord =
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   630
  list_ord (prod_ord Term_Ord.fast_indexname_ord
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   631
                     (prod_ord Term_Ord.sort_ord Term_Ord.typ_ord))
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   632
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   633
structure Int_Tysubst_Table =
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   634
  Table(type key = int * (indexname * (sort * typ)) list
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   635
        val ord = prod_ord int_ord tysubst_ord)
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   636
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   637
structure Int_Pair_Graph =
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   638
  Graph(type key = int * int val ord = prod_ord int_ord int_ord)
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   639
42271
7d08265f181d further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents: 42270
diff changeset
   640
fun shuffle_key (((axiom_no, (_, index_no)), _), _) = (axiom_no, index_no)
40258
2c0d8fe36c21 make handling of parameters more robust, by querying the goal
blanchet
parents: 40221
diff changeset
   641
fun shuffle_ord p = prod_ord int_ord int_ord (pairself shuffle_key p)
2c0d8fe36c21 make handling of parameters more robust, by querying the goal
blanchet
parents: 40221
diff changeset
   642
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   643
(* Attempts to derive the theorem "False" from a theorem of the form
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   644
   "P1 ==> ... ==> Pn ==> False", where the "Pi"s are to be discharged using the
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   645
   specified axioms. The axioms have leading "All" and "Ex" quantifiers, which
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   646
   must be eliminated first. *)
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   647
fun discharge_skolem_premises ctxt axioms prems_imp_false =
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   648
  if prop_of prems_imp_false aconv @{prop False} then
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   649
    prems_imp_false
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   650
  else
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   651
    let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42354
diff changeset
   652
      val thy = Proof_Context.theory_of ctxt
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   653
      fun match_term p =
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   654
        let
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   655
          val (tyenv, tenv) =
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   656
            Pattern.first_order_match thy p (Vartab.empty, Vartab.empty)
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   657
          val tsubst =
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   658
            tenv |> Vartab.dest
42099
447fa058ab22 avoid evil "export_without_context", which breaks if there are local "fixes"
blanchet
parents: 42098
diff changeset
   659
                 |> filter (Meson_Clausify.is_zapped_var_name o fst o fst)
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   660
                 |> sort (cluster_ord
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   661
                          o pairself (Meson_Clausify.cluster_of_zapped_var_name
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   662
                                      o fst o fst))
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   663
                 |> map (Meson.term_pair_of
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   664
                         #> pairself (Envir.subst_term_types tyenv))
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   665
          val tysubst = tyenv |> Vartab.dest
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   666
        in (tysubst, tsubst) end
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51951
diff changeset
   667
      fun subst_info_of_prem subgoal_no prem =
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   668
        case prem of
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   669
          _ $ (Const (@{const_name Meson.skolem}, _) $ (_ $ t $ num)) =>
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   670
          let val ax_no = HOLogic.dest_nat num in
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   671
            (ax_no, (subgoal_no,
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   672
                     match_term (nth axioms ax_no |> the |> snd, t)))
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   673
          end
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   674
        | _ => raise TERM ("discharge_skolem_premises: Malformed premise",
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   675
                           [prem])
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   676
      fun cluster_of_var_name skolem s =
42098
f978caf60bbe more robust handling of variables in new Skolemizer
blanchet
parents: 41491
diff changeset
   677
        case try Meson_Clausify.cluster_of_zapped_var_name s of
f978caf60bbe more robust handling of variables in new Skolemizer
blanchet
parents: 41491
diff changeset
   678
          NONE => NONE
f978caf60bbe more robust handling of variables in new Skolemizer
blanchet
parents: 41491
diff changeset
   679
        | SOME ((ax_no, (cluster_no, _)), skolem') =>
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   680
          if skolem' = skolem andalso cluster_no > 0 then
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   681
            SOME (ax_no, cluster_no)
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   682
          else
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   683
            NONE
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   684
      fun clusters_in_term skolem t =
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   685
        Term.add_var_names t [] |> map_filter (cluster_of_var_name skolem o fst)
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51951
diff changeset
   686
      fun deps_of_term_subst (var, t) =
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   687
        case clusters_in_term false var of
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   688
          [] => NONE
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   689
        | [(ax_no, cluster_no)] =>
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   690
          SOME ((ax_no, cluster_no),
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   691
                clusters_in_term true t
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   692
                |> cluster_no > 1 ? cons (ax_no, cluster_no - 1))
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   693
        | _ => raise TERM ("discharge_skolem_premises: Expected Var", [var])
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   694
      val prems = Logic.strip_imp_prems (prop_of prems_imp_false)
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51951
diff changeset
   695
      val substs = prems |> map2 subst_info_of_prem (1 upto length prems)
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   696
                         |> sort (int_ord o pairself fst)
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51951
diff changeset
   697
      val depss = maps (map_filter deps_of_term_subst o snd o snd o snd) substs
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   698
      val clusters = maps (op ::) depss
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   699
      val ordered_clusters =
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   700
        Int_Pair_Graph.empty
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   701
        |> fold Int_Pair_Graph.default_node (map (rpair ()) clusters)
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   702
        |> fold Int_Pair_Graph.add_deps_acyclic depss
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   703
        |> Int_Pair_Graph.topological_order
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   704
        handle Int_Pair_Graph.CYCLES _ =>
40158
a88d6073b190 clearer error messages
blanchet
parents: 39978
diff changeset
   705
               error "Cannot replay Metis proof in Isabelle without \
a88d6073b190 clearer error messages
blanchet
parents: 39978
diff changeset
   706
                     \\"Hilbert_Choice\"."
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   707
      val ax_counts =
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   708
        Int_Tysubst_Table.empty
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   709
        |> fold (fn (ax_no, (_, (tysubst, _))) =>
43262
547a02d889f5 removed experimental code submitted by mistake
blanchet
parents: 43259
diff changeset
   710
                    Int_Tysubst_Table.map_default ((ax_no, tysubst), 0)
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   711
                                                  (Integer.add 1)) substs
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   712
        |> Int_Tysubst_Table.dest
42339
0e5d1e5e1177 use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents: 42337
diff changeset
   713
      val needed_axiom_props =
0e5d1e5e1177 use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents: 42337
diff changeset
   714
        0 upto length axioms - 1 ~~ axioms
0e5d1e5e1177 use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents: 42337
diff changeset
   715
        |> map_filter (fn (_, NONE) => NONE
0e5d1e5e1177 use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents: 42337
diff changeset
   716
                        | (ax_no, SOME (_, t)) =>
0e5d1e5e1177 use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents: 42337
diff changeset
   717
                          if exists (fn ((ax_no', _), n) =>
0e5d1e5e1177 use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents: 42337
diff changeset
   718
                                        ax_no' = ax_no andalso n > 0)
0e5d1e5e1177 use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents: 42337
diff changeset
   719
                                    ax_counts then
0e5d1e5e1177 use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents: 42337
diff changeset
   720
                            SOME t
0e5d1e5e1177 use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents: 42337
diff changeset
   721
                          else
0e5d1e5e1177 use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents: 42337
diff changeset
   722
                            NONE)
0e5d1e5e1177 use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents: 42337
diff changeset
   723
      val outer_param_names =
0e5d1e5e1177 use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents: 42337
diff changeset
   724
        [] |> fold Term.add_var_names needed_axiom_props
0e5d1e5e1177 use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents: 42337
diff changeset
   725
           |> filter (Meson_Clausify.is_zapped_var_name o fst)
0e5d1e5e1177 use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents: 42337
diff changeset
   726
           |> map (`(Meson_Clausify.cluster_of_zapped_var_name o fst))
0e5d1e5e1177 use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents: 42337
diff changeset
   727
           |> filter (fn (((_, (cluster_no, _)), skolem), _) =>
0e5d1e5e1177 use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents: 42337
diff changeset
   728
                         cluster_no = 0 andalso skolem)
0e5d1e5e1177 use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents: 42337
diff changeset
   729
           |> sort shuffle_ord |> map (fst o snd)
42270
5f2960582e45 make new Skolemizer more robust
blanchet
parents: 42107
diff changeset
   730
(* for debugging only:
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51951
diff changeset
   731
      fun string_of_subst_info (ax_no, (subgoal_no, (tysubst, tsubst))) =
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   732
        "ax: " ^ string_of_int ax_no ^ "; asm: " ^ string_of_int subgoal_no ^
51929
5e8a0b8bb070 avoid PolyML.makestring, even in dead code;
wenzelm
parents: 51701
diff changeset
   733
        "; tysubst: " ^ @{make_string} tysubst ^ "; tsubst: {" ^
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   734
        commas (map ((fn (s, t) => s ^ " |-> " ^ t)
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   735
                     o pairself (Syntax.string_of_term ctxt)) tsubst) ^ "}"
51929
5e8a0b8bb070 avoid PolyML.makestring, even in dead code;
wenzelm
parents: 51701
diff changeset
   736
      val _ = tracing ("ORDERED CLUSTERS: " ^ @{make_string} ordered_clusters)
5e8a0b8bb070 avoid PolyML.makestring, even in dead code;
wenzelm
parents: 51701
diff changeset
   737
      val _ = tracing ("AXIOM COUNTS: " ^ @{make_string} ax_counts)
5e8a0b8bb070 avoid PolyML.makestring, even in dead code;
wenzelm
parents: 51701
diff changeset
   738
      val _ = tracing ("OUTER PARAMS: " ^ @{make_string} outer_param_names)
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   739
      val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51951
diff changeset
   740
                       cat_lines (map string_of_subst_info substs))
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   741
*)
42271
7d08265f181d further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents: 42270
diff changeset
   742
      fun cut_and_ex_tac axiom =
46708
b138dee7bed3 prefer cut_tac, where it is clear that the special variants cut_rules_tac or cut_facts_tac are not required;
wenzelm
parents: 46392
diff changeset
   743
        cut_tac axiom 1
42271
7d08265f181d further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents: 42270
diff changeset
   744
        THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1)
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51951
diff changeset
   745
      fun rotation_of_subgoal i =
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   746
        find_index (fn (_, (subgoal_no, _)) => subgoal_no = i) substs
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   747
    in
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   748
      Goal.prove ctxt [] [] @{prop False}
42271
7d08265f181d further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents: 42270
diff changeset
   749
          (K (DETERM (EVERY (map (cut_and_ex_tac o fst o the o nth axioms o fst
7d08265f181d further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents: 42270
diff changeset
   750
                                  o fst) ax_counts)
7d08265f181d further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents: 42270
diff changeset
   751
                      THEN rename_tac outer_param_names 1
7d08265f181d further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents: 42270
diff changeset
   752
                      THEN copy_prems_tac (map snd ax_counts) [] 1)
40258
2c0d8fe36c21 make handling of parameters more robust, by querying the goal
blanchet
parents: 40221
diff changeset
   753
              THEN release_clusters_tac thy ax_counts substs ordered_clusters 1
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   754
              THEN match_tac [prems_imp_false] 1
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   755
              THEN ALLGOALS (fn i =>
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   756
                       rtac @{thm Meson.skolem_COMBK_I} i
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51951
diff changeset
   757
                       THEN rotate_tac (rotation_of_subgoal i) i
42342
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42341
diff changeset
   758
                       THEN PRIMITIVE (unify_first_prem_with_concl thy i)
42271
7d08265f181d further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents: 42270
diff changeset
   759
                       THEN assume_tac i
42270
5f2960582e45 make new Skolemizer more robust
blanchet
parents: 42107
diff changeset
   760
                       THEN flexflex_tac)))
40158
a88d6073b190 clearer error messages
blanchet
parents: 39978
diff changeset
   761
      handle ERROR _ =>
a88d6073b190 clearer error messages
blanchet
parents: 39978
diff changeset
   762
             error ("Cannot replay Metis proof in Isabelle:\n\
a88d6073b190 clearer error messages
blanchet
parents: 39978
diff changeset
   763
                    \Error when discharging Skolem assumptions.")
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   764
    end
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   765
39495
bb4fb9ffe2d1 added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff changeset
   766
end;