src/HOL/Tools/Metis/metis_reconstruct.ML
author wenzelm
Wed, 08 Jun 2011 22:13:49 +0200
changeset 43297 e77baf329f48
parent 43294 0271fda2a83a
parent 43278 1fbdcebb364b
child 43298 82d4874757df
permissions -rw-r--r--
merged
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
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
    12
  exception METIS of string * string
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
    13
43159
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43136
diff changeset
    14
  val hol_clause_from_metis :
43184
b16693484c5d reveal Skolems in new Metis
blanchet
parents: 43177
diff changeset
    15
    Proof.context -> int Symtab.table -> (string * term) list -> Metis_Thm.thm
b16693484c5d reveal Skolems in new Metis
blanchet
parents: 43177
diff changeset
    16
    -> term
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
    17
  val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
43134
0c82e00ba63e make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents: 43130
diff changeset
    18
  val untyped_aconv : term * term -> bool
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
    19
  val replay_one_inference :
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43209
diff changeset
    20
    Proof.context -> (string * term) list -> int Symtab.table
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
    21
    -> 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
    22
    -> (Metis_Thm.thm * thm) list
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
    23
  val discharge_skolem_premises :
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
    24
    Proof.context -> (thm * term) option list -> thm -> thm
39495
bb4fb9ffe2d1 added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff changeset
    25
end;
bb4fb9ffe2d1 added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff changeset
    26
bb4fb9ffe2d1 added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff changeset
    27
structure Metis_Reconstruct : METIS_RECONSTRUCT =
bb4fb9ffe2d1 added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff changeset
    28
struct
bb4fb9ffe2d1 added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff changeset
    29
43094
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
    30
open ATP_Problem
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 42650
diff changeset
    31
open ATP_Translate
43094
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
    32
open ATP_Reconstruct
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
    33
open Metis_Translate
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
    34
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
    35
exception METIS of string * string
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
    36
39498
e8aef7ea9cbb make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents: 39497
diff changeset
    37
datatype term_or_type = SomeTerm of term | SomeType of typ
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
    38
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
    39
fun terms_of [] = []
39498
e8aef7ea9cbb make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents: 39497
diff changeset
    40
  | terms_of (SomeTerm t :: tts) = t :: terms_of tts
e8aef7ea9cbb make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents: 39497
diff changeset
    41
  | terms_of (SomeType _ :: tts) = terms_of tts;
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
    42
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
    43
fun types_of [] = []
43135
8c32a0160b0d more uniform handling of tfree sort inference in ATP reconstruction code, based on what Metis always has done
blanchet
parents: 43134
diff changeset
    44
  | types_of (SomeTerm (Var ((a, idx), _)) :: tts) =
8c32a0160b0d more uniform handling of tfree sort inference in ATP reconstruction code, based on what Metis always has done
blanchet
parents: 43134
diff changeset
    45
    types_of tts
8c32a0160b0d more uniform handling of tfree sort inference in ATP reconstruction code, based on what Metis always has done
blanchet
parents: 43134
diff changeset
    46
    |> (if String.isPrefix metis_generated_var_prefix a then
8c32a0160b0d more uniform handling of tfree sort inference in ATP reconstruction code, based on what Metis always has done
blanchet
parents: 43134
diff changeset
    47
          (* Variable generated by Metis, which might have been a type
8c32a0160b0d more uniform handling of tfree sort inference in ATP reconstruction code, based on what Metis always has done
blanchet
parents: 43134
diff changeset
    48
             variable. *)
8c32a0160b0d more uniform handling of tfree sort inference in ATP reconstruction code, based on what Metis always has done
blanchet
parents: 43134
diff changeset
    49
          cons (TVar (("'" ^ a, idx), HOLogic.typeS))
8c32a0160b0d more uniform handling of tfree sort inference in ATP reconstruction code, based on what Metis always has done
blanchet
parents: 43134
diff changeset
    50
        else
8c32a0160b0d more uniform handling of tfree sort inference in ATP reconstruction code, based on what Metis always has done
blanchet
parents: 43134
diff changeset
    51
          I)
39498
e8aef7ea9cbb make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents: 39497
diff changeset
    52
  | types_of (SomeTerm _ :: tts) = types_of tts
43135
8c32a0160b0d more uniform handling of tfree sort inference in ATP reconstruction code, based on what Metis always has done
blanchet
parents: 43134
diff changeset
    53
  | types_of (SomeType T :: tts) = T :: types_of tts
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
    54
43094
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
    55
fun atp_name_from_metis s =
43104
81d1b15aa0ae use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents: 43103
diff changeset
    56
  case find_first (fn (_, (s', _)) => s' = s) metis_name_table of
81d1b15aa0ae use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents: 43103
diff changeset
    57
    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
    58
  | _ => (s, false)
43094
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
    59
fun atp_term_from_metis (Metis_Term.Fn (s, tms)) =
43268
c0eaa8b9bff5 removed yet another hack in "make_metis" script -- respect opacity of "Metis_Name.name"
blanchet
parents: 43262
diff changeset
    60
    let val (s, swap) = atp_name_from_metis (Metis_Name.toString s) in
43104
81d1b15aa0ae use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents: 43103
diff changeset
    61
      ATerm (s, tms |> map atp_term_from_metis |> swap ? rev)
81d1b15aa0ae use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents: 43103
diff changeset
    62
    end
43268
c0eaa8b9bff5 removed yet another hack in "make_metis" script -- respect opacity of "Metis_Name.name"
blanchet
parents: 43262
diff changeset
    63
  | atp_term_from_metis (Metis_Term.Var s) = ATerm (Metis_Name.toString s, [])
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
    64
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43209
diff changeset
    65
fun hol_term_from_metis ctxt sym_tab =
050a03afe024 Metis code cleanup
blanchet
parents: 43209
diff changeset
    66
  atp_term_from_metis #> term_from_atp ctxt false sym_tab NONE
43094
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
    67
43136
cf5cda219058 handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents: 43135
diff changeset
    68
fun atp_literal_from_metis (pos, atom) =
cf5cda219058 handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents: 43135
diff changeset
    69
  atom |> Metis_Term.Fn |> atp_term_from_metis |> AAtom |> not pos ? mk_anot
cf5cda219058 handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents: 43135
diff changeset
    70
fun atp_clause_from_metis [] = AAtom (ATerm (tptp_false, []))
cf5cda219058 handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents: 43135
diff changeset
    71
  | atp_clause_from_metis lits =
cf5cda219058 handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents: 43135
diff changeset
    72
    lits |> map atp_literal_from_metis |> mk_aconns AOr
cf5cda219058 handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents: 43135
diff changeset
    73
43184
b16693484c5d reveal Skolems in new Metis
blanchet
parents: 43177
diff changeset
    74
fun reveal_old_skolems_and_infer_types ctxt old_skolems =
b16693484c5d reveal Skolems in new Metis
blanchet
parents: 43177
diff changeset
    75
  map (reveal_old_skolem_terms old_skolems)
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43209
diff changeset
    76
  #> Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
43184
b16693484c5d reveal Skolems in new Metis
blanchet
parents: 43177
diff changeset
    77
b16693484c5d reveal Skolems in new Metis
blanchet
parents: 43177
diff changeset
    78
fun hol_clause_from_metis ctxt sym_tab old_skolems =
43159
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43136
diff changeset
    79
  Metis_Thm.clause
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43136
diff changeset
    80
  #> Metis_LiteralSet.toList
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43136
diff changeset
    81
  #> atp_clause_from_metis
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43136
diff changeset
    82
  #> prop_from_atp ctxt false sym_tab
43184
b16693484c5d reveal Skolems in new Metis
blanchet
parents: 43177
diff changeset
    83
  #> singleton (reveal_old_skolems_and_infer_types ctxt old_skolems)
43136
cf5cda219058 handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents: 43135
diff changeset
    84
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43209
diff changeset
    85
fun hol_terms_from_metis ctxt old_skolems sym_tab fol_tms =
050a03afe024 Metis code cleanup
blanchet
parents: 43209
diff changeset
    86
  let val ts = map (hol_term_from_metis ctxt sym_tab) fol_tms
39978
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
    87
      val _ = trace_msg ctxt (fn () => "  calling type inference:")
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
    88
      val _ = app (fn t => trace_msg ctxt
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
    89
                                     (fn () => Syntax.string_of_term ctxt t)) ts
43184
b16693484c5d reveal Skolems in new Metis
blanchet
parents: 43177
diff changeset
    90
      val ts' =
b16693484c5d reveal Skolems in new Metis
blanchet
parents: 43177
diff changeset
    91
        ts |> reveal_old_skolems_and_infer_types ctxt old_skolems
39978
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
    92
      val _ = app (fn t => trace_msg ctxt
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
    93
                    (fn () => "  final term: " ^ Syntax.string_of_term ctxt t ^
43128
a19826080596 tuned names
blanchet
parents: 43106
diff changeset
    94
                              " 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
    95
                  ts'
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
    96
  in  ts'  end;
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
    97
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
    98
(* ------------------------------------------------------------------------- *)
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
    99
(* FOL step Inference Rules                                                  *)
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   100
(* ------------------------------------------------------------------------- *)
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
(*for debugging only*)
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   103
(*
39978
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
   104
fun print_thpair ctxt (fth,th) =
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
   105
  (trace_msg ctxt (fn () => "=============================================");
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
   106
   trace_msg ctxt (fn () => "Metis: " ^ Metis_Thm.toString fth);
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
   107
   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
   108
*)
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   109
43094
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
   110
fun lookth th_pairs fth =
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
   111
  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
   112
  handle Option.Option =>
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   113
         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
   114
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   115
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
   116
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   117
(* INFERENCE RULE: AXIOM *)
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   118
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43209
diff changeset
   119
(* This causes variables to have an index of 1 by default. See also
050a03afe024 Metis code cleanup
blanchet
parents: 43209
diff changeset
   120
   "term_from_atp" in "ATP_Reconstruct". *)
050a03afe024 Metis code cleanup
blanchet
parents: 43209
diff changeset
   121
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
   122
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   123
(* INFERENCE RULE: ASSUME *)
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   124
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   125
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
   126
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
   127
fun inst_excluded_middle thy i_atom =
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   128
  let val th = EXCLUDED_MIDDLE
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   129
      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
   130
      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
   131
  in  cterm_instantiate substs th  end;
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   132
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43209
diff changeset
   133
fun assume_inference ctxt old_skolems sym_tab atom =
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   134
  inst_excluded_middle
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42354
diff changeset
   135
      (Proof_Context.theory_of ctxt)
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43209
diff changeset
   136
      (singleton (hol_terms_from_metis ctxt old_skolems 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
   137
                 (Metis_Term.Fn atom))
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   138
39498
e8aef7ea9cbb make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents: 39497
diff changeset
   139
(* 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
   140
   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
   141
   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
   142
   can be inferred from terms. *)
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   143
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43209
diff changeset
   144
fun inst_inference ctxt old_skolems sym_tab th_pairs fsubst th =
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42354
diff changeset
   145
  let val thy = Proof_Context.theory_of ctxt
43094
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
   146
      val i_th = lookth th_pairs th
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   147
      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
   148
      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
   149
      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
   150
        let val v = find_var x
43184
b16693484c5d reveal Skolems in new Metis
blanchet
parents: 43177
diff changeset
   151
            (* We call "reveal_old_skolems_and_infer_types" below. *)
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43209
diff changeset
   152
            val t = hol_term_from_metis ctxt sym_tab y
39498
e8aef7ea9cbb make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents: 39497
diff changeset
   153
        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
   154
        handle Option.Option =>
39978
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
   155
               (trace_msg ctxt (fn () => "\"find_var\" failed for " ^ x ^
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
   156
                                         " 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
   157
                NONE)
e8aef7ea9cbb make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents: 39497
diff changeset
   158
             | TYPE _ =>
39978
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
   159
               (trace_msg ctxt (fn () => "\"hol_term_from_metis\" failed for " ^ x ^
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
   160
                                         " 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
   161
                NONE)
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   162
      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
   163
        let val a = Metis_Name.toString a in
c0eaa8b9bff5 removed yet another hack in "make_metis" script -- respect opacity of "Metis_Name.name"
blanchet
parents: 43262
diff changeset
   164
          case strip_prefix_and_unascii schematic_var_prefix a of
c0eaa8b9bff5 removed yet another hack in "make_metis" script -- respect opacity of "Metis_Name.name"
blanchet
parents: 43262
diff changeset
   165
            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
   166
          | NONE =>
c0eaa8b9bff5 removed yet another hack in "make_metis" script -- respect opacity of "Metis_Name.name"
blanchet
parents: 43262
diff changeset
   167
            case strip_prefix_and_unascii tvar_prefix a of
c0eaa8b9bff5 removed yet another hack in "make_metis" script -- respect opacity of "Metis_Name.name"
blanchet
parents: 43262
diff changeset
   168
              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
   169
            | 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
   170
        end
39978
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
   171
      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
   172
      val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst)
43184
b16693484c5d reveal Skolems in new Metis
blanchet
parents: 43177
diff changeset
   173
      val (vars, tms) =
b16693484c5d reveal Skolems in new Metis
blanchet
parents: 43177
diff changeset
   174
        ListPair.unzip (map_filter subst_translation substs)
b16693484c5d reveal Skolems in new Metis
blanchet
parents: 43177
diff changeset
   175
        ||> reveal_old_skolems_and_infer_types ctxt old_skolems
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   176
      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
   177
      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
   178
      val _ = trace_msg ctxt (fn () =>
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   179
        cat_lines ("subst_translations:" ::
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   180
          (substs' |> map (fn (x, y) =>
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   181
            Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   182
            Syntax.string_of_term ctxt (term_of y)))));
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   183
  in cterm_instantiate substs' i_th end
43186
blanchet
parents: 43184
diff changeset
   184
  handle THM (msg, _, _) => raise METIS ("inst_inference", msg)
blanchet
parents: 43184
diff changeset
   185
       | ERROR msg => raise METIS ("inst_inference", msg)
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   186
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   187
(* INFERENCE RULE: RESOLVE *)
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   188
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   189
(* 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
   190
   have an index of 1, and the use of RSN would increase this typically to 3.
43135
8c32a0160b0d more uniform handling of tfree sort inference in ATP reconstruction code, based on what Metis always has done
blanchet
parents: 43134
diff changeset
   191
   Instantiations of those Vars could then fail. See comment on "make_var". *)
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   192
fun resolve_inc_tyvars thy tha i thb =
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   193
  let
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   194
    val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   195
    fun aux tha thb =
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   196
      case Thm.bicompose false (false, tha, nprems_of tha) i thb
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   197
           |> Seq.list_of |> distinct Thm.eq_thm of
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   198
        [th] => th
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   199
      | _ => raise THM ("resolve_inc_tyvars: unique result expected", i,
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   200
                        [tha, thb])
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   201
  in
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   202
    aux tha thb
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   203
    handle TERM z =>
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   204
           (* 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
   205
              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
   206
              "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
   207
              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
   208
              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
   209
              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
   210
              ways or slow them down needlessly. *)
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   211
           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
   212
                   |> AList.group (op =)
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   213
                   |> maps (fn ((s, _), T :: Ts) =>
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   214
                               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
   215
                   |> rpair (Envir.empty ~1)
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   216
                   |-> fold (Pattern.unify thy)
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   217
                   |> Envir.type_env |> Vartab.dest
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   218
                   |> map (fn (x, (S, T)) =>
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   219
                              pairself (ctyp_of thy) (TVar (x, S), T)) of
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   220
             [] => raise TERM z
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   221
           | ps => aux (instantiate (ps, []) tha) (instantiate (ps, []) thb)
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   222
  end
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   223
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
   224
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
   225
  | 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
   226
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
   227
  | 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
   228
  | simp_not_not t = t
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   229
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   230
(* Match untyped terms. *)
43134
0c82e00ba63e make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents: 43130
diff changeset
   231
fun untyped_aconv (Const (a, _), Const(b, _)) = (a = b)
0c82e00ba63e make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents: 43130
diff changeset
   232
  | untyped_aconv (Free (a, _), Free (b, _)) = (a = b)
43294
0271fda2a83a restore comment about subtle issue
blanchet
parents: 43268
diff changeset
   233
  | untyped_aconv (Var ((a, _), _), Var ((b, _), _)) =
0271fda2a83a restore comment about subtle issue
blanchet
parents: 43268
diff changeset
   234
    (a = b) (* ignore variable numbers *)
43134
0c82e00ba63e make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents: 43130
diff changeset
   235
  | untyped_aconv (Bound i, Bound j) = (i = j)
0c82e00ba63e make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents: 43130
diff changeset
   236
  | untyped_aconv (Abs (_, _, t), Abs (_, _, u)) = untyped_aconv (t, u)
0c82e00ba63e make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents: 43130
diff changeset
   237
  | untyped_aconv (t1 $ t2, u1 $ u2) =
0c82e00ba63e make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents: 43130
diff changeset
   238
    untyped_aconv (t1, u1) andalso untyped_aconv (t2, u2)
0c82e00ba63e make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents: 43130
diff changeset
   239
  | untyped_aconv _ = false
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   240
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
   241
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
   242
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
   243
(* 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
   244
   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
   245
fun index_of_literal lit haystack =
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   246
  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
   247
    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
   248
      HOLogic.dest_Trueprop #> normalize
0c82e00ba63e make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents: 43130
diff changeset
   249
      #> curry untyped_aconv (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
   250
  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
   251
    (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
   252
       ~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
   253
     | 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
   254
  end
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   255
39893
25a339e1ff9b move functions closer to where they're used
blanchet
parents: 39887
diff changeset
   256
(* 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
   257
fun make_last i th =
25a339e1ff9b move functions closer to where they're used
blanchet
parents: 39887
diff changeset
   258
  let val n = nprems_of th
25a339e1ff9b move functions closer to where they're used
blanchet
parents: 39887
diff changeset
   259
  in  if 1 <= i andalso i <= n
25a339e1ff9b move functions closer to where they're used
blanchet
parents: 39887
diff changeset
   260
      then Thm.permute_prems (i-1) 1 th
25a339e1ff9b move functions closer to where they're used
blanchet
parents: 39887
diff changeset
   261
      else raise THM("select_literal", i, [th])
25a339e1ff9b move functions closer to where they're used
blanchet
parents: 39887
diff changeset
   262
  end;
25a339e1ff9b move functions closer to where they're used
blanchet
parents: 39887
diff changeset
   263
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
   264
(* 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
   265
   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
   266
   "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
   267
   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
   268
   necessary. FIXME. *)
721e85fd2db3 make 48170228f562 work also with "HO_Reas" examples
blanchet
parents: 42348
diff changeset
   269
fun negate_head th =
721e85fd2db3 make 48170228f562 work also with "HO_Reas" examples
blanchet
parents: 42348
diff changeset
   270
  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
   271
    (th RS @{thm select_FalseI})
721e85fd2db3 make 48170228f562 work also with "HO_Reas" examples
blanchet
parents: 42348
diff changeset
   272
    |> fold (rewrite_rule o single)
721e85fd2db3 make 48170228f562 work also with "HO_Reas" examples
blanchet
parents: 42348
diff changeset
   273
            @{thms not_atomize_select atomize_not_select}
721e85fd2db3 make 48170228f562 work also with "HO_Reas" examples
blanchet
parents: 42348
diff changeset
   274
  else
721e85fd2db3 make 48170228f562 work also with "HO_Reas" examples
blanchet
parents: 42348
diff changeset
   275
    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
   276
25a339e1ff9b move functions closer to where they're used
blanchet
parents: 39887
diff changeset
   277
(* 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
   278
val select_literal = negate_head oo make_last
39893
25a339e1ff9b move functions closer to where they're used
blanchet
parents: 39887
diff changeset
   279
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43209
diff changeset
   280
fun resolve_inference ctxt old_skolems sym_tab th_pairs atom th1 th2 =
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   281
  let
43094
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
   282
    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
   283
    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
   284
        "  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
   285
        \  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
   286
  in
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   287
    (* Trivial cases where one operand is type info *)
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   288
    if Thm.eq_thm (TrueI, i_th1) then
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   289
      i_th2
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   290
    else if Thm.eq_thm (TrueI, i_th2) then
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   291
      i_th1
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   292
    else
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   293
      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
   294
        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
   295
        val i_atom =
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43209
diff changeset
   296
          singleton (hol_terms_from_metis ctxt old_skolems 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
   297
                    (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
   298
        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
   299
                    "  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
   300
      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
   301
        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
   302
          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
   303
          (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
   304
           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
   305
        | 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
   306
          (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
   307
           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
   308
             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
   309
             (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
   310
              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
   311
           | 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
   312
             (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
   313
              resolve_inc_tyvars thy (select_literal j1 i_th1) j2 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
   314
              handle TERM (s, _) => raise METIS ("resolve_inference", s)))
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
   315
      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
   316
  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: REFL *)
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 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
   321
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   322
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
   323
val refl_idx = 1 + Thm.maxidx_of REFL_THM;
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   324
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43209
diff changeset
   325
fun refl_inference ctxt old_skolems sym_tab t =
43094
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
   326
  let
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
   327
    val thy = Proof_Context.theory_of ctxt
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43209
diff changeset
   328
    val i_t = singleton (hol_terms_from_metis ctxt old_skolems sym_tab) t
43094
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
   329
    val _ = trace_msg ctxt (fn () => "  term: " ^ Syntax.string_of_term ctxt i_t)
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
   330
    val c_t = cterm_incr_types thy refl_idx i_t
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
   331
  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
   332
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   333
(* INFERENCE RULE: EQUALITY *)
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   334
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   335
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
   336
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
   337
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43209
diff changeset
   338
fun equality_inference ctxt old_skolems sym_tab (pos, atom) fp fr =
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42354
diff changeset
   339
  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
   340
      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
   341
      val [i_atom, i_tm] =
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43209
diff changeset
   342
        hol_terms_from_metis ctxt old_skolems sym_tab [m_tm, fr]
39978
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
   343
      val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Bool.toString pos)
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   344
      fun replace_item_list lx 0 (_::ls) = lx::ls
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   345
        | 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
   346
      fun path_finder_fail tm ps t =
43209
007117fed183 fall back in case path finder fails -- these errors are sometimes salvageable
blanchet
parents: 43205
diff changeset
   347
        raise METIS ("equality_inference (path_finder)",
007117fed183 fall back in case path finder fails -- these errors are sometimes salvageable
blanchet
parents: 43205
diff changeset
   348
                     "path = " ^ space_implode " " (map string_of_int ps) ^
007117fed183 fall back in case path finder fails -- these errors are sometimes salvageable
blanchet
parents: 43205
diff changeset
   349
                     " isa-term: " ^ Syntax.string_of_term ctxt tm ^
007117fed183 fall back in case path finder fails -- these errors are sometimes salvageable
blanchet
parents: 43205
diff changeset
   350
                     (case t of
007117fed183 fall back in case path finder fails -- these errors are sometimes salvageable
blanchet
parents: 43205
diff changeset
   351
                        SOME t => " fol-term: " ^ Metis_Term.toString t
007117fed183 fall back in case path finder fails -- these errors are sometimes salvageable
blanchet
parents: 43205
diff changeset
   352
                      | NONE => ""))
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43209
diff changeset
   353
      fun path_finder tm [] _ = (tm, Bound 0)
050a03afe024 Metis code cleanup
blanchet
parents: 43209
diff changeset
   354
        | 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
   355
          let
43268
c0eaa8b9bff5 removed yet another hack in "make_metis" script -- respect opacity of "Metis_Name.name"
blanchet
parents: 43262
diff changeset
   356
            val s = s |> Metis_Name.toString
c0eaa8b9bff5 removed yet another hack in "make_metis" script -- respect opacity of "Metis_Name.name"
blanchet
parents: 43262
diff changeset
   357
                      |> perhaps (try (strip_prefix_and_unascii const_prefix
43177
5017d436a572 properly unmangle names in path finder
blanchet
parents: 43174
diff changeset
   358
                                       #> the #> unmangled_const_name))
5017d436a572 properly unmangle names in path finder
blanchet
parents: 43174
diff changeset
   359
          in
5017d436a572 properly unmangle names in path finder
blanchet
parents: 43174
diff changeset
   360
            if s = metis_predicator orelse s = predicator_name orelse
5017d436a572 properly unmangle names in path finder
blanchet
parents: 43174
diff changeset
   361
               s = metis_type_tag orelse s = type_tag_name then
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43209
diff changeset
   362
              path_finder tm ps (nth ts p)
43177
5017d436a572 properly unmangle names in path finder
blanchet
parents: 43174
diff changeset
   363
            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
   364
              let
d73fc2e55308 implemented missing hAPP and ti cases of new path finder
blanchet
parents: 43128
diff changeset
   365
                val (tm1, tm2) = dest_comb tm
d73fc2e55308 implemented missing hAPP and ti cases of new path finder
blanchet
parents: 43128
diff changeset
   366
                val p' = p - (length ts - 2)
d73fc2e55308 implemented missing hAPP and ti cases of new path finder
blanchet
parents: 43128
diff changeset
   367
              in
d73fc2e55308 implemented missing hAPP and ti cases of new path finder
blanchet
parents: 43128
diff changeset
   368
                if p' = 0 then
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43209
diff changeset
   369
                  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
   370
                else
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43209
diff changeset
   371
                  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
   372
              end
d73fc2e55308 implemented missing hAPP and ti cases of new path finder
blanchet
parents: 43128
diff changeset
   373
            else
d73fc2e55308 implemented missing hAPP and ti cases of new path finder
blanchet
parents: 43128
diff changeset
   374
              let
d73fc2e55308 implemented missing hAPP and ti cases of new path finder
blanchet
parents: 43128
diff changeset
   375
                val (tm1, args) = strip_comb tm
d73fc2e55308 implemented missing hAPP and ti cases of new path finder
blanchet
parents: 43128
diff changeset
   376
                val adjustment = length ts - length args
d73fc2e55308 implemented missing hAPP and ti cases of new path finder
blanchet
parents: 43128
diff changeset
   377
                val p' = if adjustment > p then p else p - adjustment
43205
23b81469499f more preparations towards hijacking Metis
blanchet
parents: 43195
diff changeset
   378
                val tm_p =
23b81469499f more preparations towards hijacking Metis
blanchet
parents: 43195
diff changeset
   379
                  nth args p'
43278
1fbdcebb364b more robust exception pattern General.Subscript;
wenzelm
parents: 43268
diff changeset
   380
                  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
   381
                val _ = trace_msg ctxt (fn () =>
d73fc2e55308 implemented missing hAPP and ti cases of new path finder
blanchet
parents: 43128
diff changeset
   382
                    "path_finder: " ^ string_of_int p ^ "  " ^
d73fc2e55308 implemented missing hAPP and ti cases of new path finder
blanchet
parents: 43128
diff changeset
   383
                    Syntax.string_of_term ctxt tm_p)
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43209
diff changeset
   384
                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
   385
              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
   386
          end
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43209
diff changeset
   387
        | path_finder tm ps t = path_finder_fail tm ps (SOME t)
050a03afe024 Metis code cleanup
blanchet
parents: 43209
diff changeset
   388
      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
   389
      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
   390
      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
   391
      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
   392
      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
   393
      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
   394
      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
   395
      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
   396
      val eq_terms = map (pairself (cterm_of thy))
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   397
        (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   398
  in  cterm_instantiate eq_terms subst'  end;
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   399
43094
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
   400
val factor = Seq.hd o distinct_subgoals_tac
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   401
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43209
diff changeset
   402
fun one_step ctxt old_skolems sym_tab th_pairs p =
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   403
  case p of
43186
blanchet
parents: 43184
diff changeset
   404
    (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
   405
  | (_, Metis_Proof.Assume f_atom) =>
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43209
diff changeset
   406
    assume_inference ctxt old_skolems sym_tab f_atom
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   407
  | (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) =>
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43209
diff changeset
   408
    inst_inference ctxt old_skolems sym_tab th_pairs f_subst f_th1
43186
blanchet
parents: 43184
diff changeset
   409
    |> 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
   410
  | (_, Metis_Proof.Resolve(f_atom, f_th1, f_th2)) =>
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43209
diff changeset
   411
    resolve_inference ctxt old_skolems sym_tab th_pairs f_atom f_th1 f_th2
43094
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
   412
    |> factor
43186
blanchet
parents: 43184
diff changeset
   413
  | (_, Metis_Proof.Refl f_tm) =>
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43209
diff changeset
   414
    refl_inference ctxt old_skolems sym_tab f_tm
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   415
  | (_, Metis_Proof.Equality (f_lit, f_p, f_r)) =>
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43209
diff changeset
   416
    equality_inference ctxt old_skolems sym_tab f_lit f_p f_r
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   417
39893
25a339e1ff9b move functions closer to where they're used
blanchet
parents: 39887
diff changeset
   418
fun flexflex_first_order th =
25a339e1ff9b move functions closer to where they're used
blanchet
parents: 39887
diff changeset
   419
  case Thm.tpairs_of th of
25a339e1ff9b move functions closer to where they're used
blanchet
parents: 39887
diff changeset
   420
      [] => th
25a339e1ff9b move functions closer to where they're used
blanchet
parents: 39887
diff changeset
   421
    | pairs =>
25a339e1ff9b move functions closer to where they're used
blanchet
parents: 39887
diff changeset
   422
        let val thy = theory_of_thm th
25a339e1ff9b move functions closer to where they're used
blanchet
parents: 39887
diff changeset
   423
            val (_, tenv) =
25a339e1ff9b move functions closer to where they're used
blanchet
parents: 39887
diff changeset
   424
              fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
25a339e1ff9b move functions closer to where they're used
blanchet
parents: 39887
diff changeset
   425
            val t_pairs = map Meson.term_pair_of (Vartab.dest tenv)
25a339e1ff9b move functions closer to where they're used
blanchet
parents: 39887
diff changeset
   426
            val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th
25a339e1ff9b move functions closer to where they're used
blanchet
parents: 39887
diff changeset
   427
        in  th'  end
25a339e1ff9b move functions closer to where they're used
blanchet
parents: 39887
diff changeset
   428
        handle THM _ => th;
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   429
43268
c0eaa8b9bff5 removed yet another hack in "make_metis" script -- respect opacity of "Metis_Name.name"
blanchet
parents: 43262
diff changeset
   430
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
   431
  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
   432
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
   433
  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
   434
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
   435
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
   436
42333
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42271
diff changeset
   437
(* 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
   438
   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
   439
   eliminate them, duplicates sometimes appear with slightly different (but
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42271
diff changeset
   440
   unifiable) types. *)
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42271
diff changeset
   441
fun resynchronize ctxt fol_th th =
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42271
diff changeset
   442
  let
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42271
diff changeset
   443
    val num_metis_lits =
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42271
diff changeset
   444
      count is_metis_literal_genuine
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42271
diff changeset
   445
            (Metis_LiteralSet.toList (Metis_Thm.clause fol_th))
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42271
diff changeset
   446
    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
   447
  in
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42271
diff changeset
   448
    if num_metis_lits >= num_isabelle_lits then
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42271
diff changeset
   449
      th
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42271
diff changeset
   450
    else
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42271
diff changeset
   451
      let
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42271
diff changeset
   452
        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
   453
        val prems = prems0 |> map normalize_literal
6dc58b3b73b5 improved correctness of handling of higher-order occurrences of "Not" in new Metis (and probably in old Metis)
blanchet
parents: 43187
diff changeset
   454
                           |> distinct untyped_aconv
42333
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42271
diff changeset
   455
        val goal = Logic.list_implies (prems, concl)
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
   456
        val tac = cut_rules_tac [th] 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
   457
                  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
   458
                  THEN ALLGOALS assume_tac
42333
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42271
diff changeset
   459
      in
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42271
diff changeset
   460
        if length prems = length prems0 then
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
   461
          raise METIS ("resynchronize", "Out of sync")
42333
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42271
diff changeset
   462
        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
   463
          Goal.prove ctxt [] [] goal (K tac)
42333
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42271
diff changeset
   464
          |> resynchronize ctxt fol_th
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42271
diff changeset
   465
      end
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42271
diff changeset
   466
  end
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42271
diff changeset
   467
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43209
diff changeset
   468
fun replay_one_inference ctxt old_skolems sym_tab (fol_th, inf) th_pairs =
43094
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
   469
  if not (null th_pairs) andalso
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
   470
     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
   471
    (* 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
   472
       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
   473
       benefice of the doubt. *)
43094
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
   474
    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
   475
  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
   476
    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
   477
      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
   478
                  (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
   479
      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
   480
                  (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
   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 () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43209
diff changeset
   483
      val th = one_step ctxt old_skolems 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
   484
               |> flexflex_first_order
42333
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42271
diff changeset
   485
               |> 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
   486
      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
   487
                  (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
   488
      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
   489
                  (fn () => "=============================================")
43094
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
   490
    in (fol_th, th) :: th_pairs end
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39495
diff changeset
   491
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
   492
(* 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
   493
   one of the premises. Unfortunately, this sometimes yields "Variable
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
   ?SK_a_b_c_x has two distinct types" errors. To avoid this, we instantiate the
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
   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
   496
     ?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
   497
   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
   498
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
   499
  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
   500
    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
   501
    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
   502
    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
   503
    fun pair_untyped_aconv (t1, t2) (u1, u2) =
43134
0c82e00ba63e make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents: 43130
diff changeset
   504
      untyped_aconv (t1, u1) andalso untyped_aconv (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
   505
    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
   506
      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
   507
      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
   508
    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
   509
      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
   510
        (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
   511
      | _ => 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
   512
    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
   513
      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
   514
        (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
   515
        add_terms (Var z,
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
          fold_rev (curry absdummy) (take (length args) (binder_types T)) 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
   517
      | _ => 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
   518
    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
   519
      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
   520
      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
   521
      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
   522
    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
   523
      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
   524
        (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
   525
        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
   526
        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
   527
        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
   528
      | (_ $ _, _) => 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
   529
      | (_, _ $ _) => 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
   530
      | (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
   531
      | (_, 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
   532
      | _ => 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
   533
    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
   534
      [] |> 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
   535
         |> 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
   536
  in th |> cterm_instantiate t_inst end
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   537
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   538
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
   539
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   540
fun copy_prems_tac [] ns i =
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   541
    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
   542
  | copy_prems_tac (1 :: ms) ns i =
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   543
    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
   544
  | copy_prems_tac (m :: ms) ns i =
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   545
    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
   546
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
   547
(* 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
   548
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
   549
40258
2c0d8fe36c21 make handling of parameters more robust, by querying the goal
blanchet
parents: 40221
diff changeset
   550
fun instantiate_forall_tac thy t i st =
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   551
  let
40258
2c0d8fe36c21 make handling of parameters more robust, by querying the goal
blanchet
parents: 40221
diff changeset
   552
    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
   553
    fun repair (t as (Var ((s, _), _))) =
40258
2c0d8fe36c21 make handling of parameters more robust, by querying the goal
blanchet
parents: 40221
diff changeset
   554
        (case find_index (fn (s', _) => s' = s) params of
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   555
           ~1 => t
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   556
         | j => Bound j)
40261
7a02144874f3 more work on new Skolemizer without Hilbert_Choice
blanchet
parents: 40259
diff changeset
   557
      | repair (t $ u) =
7a02144874f3 more work on new Skolemizer without Hilbert_Choice
blanchet
parents: 40259
diff changeset
   558
        (case (repair t, repair u) of
7a02144874f3 more work on new Skolemizer without Hilbert_Choice
blanchet
parents: 40259
diff changeset
   559
           (t as Bound j, u as Bound k) =>
7a02144874f3 more work on new Skolemizer without Hilbert_Choice
blanchet
parents: 40259
diff changeset
   560
           (* 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
   561
              the fully skolemized term that MESON gives us (where existentials
7a02144874f3 more work on new Skolemizer without Hilbert_Choice
blanchet
parents: 40259
diff changeset
   562
              were pulled out) and the reality. *)
7a02144874f3 more work on new Skolemizer without Hilbert_Choice
blanchet
parents: 40259
diff changeset
   563
           if k > j then t else t $ u
7a02144874f3 more work on new Skolemizer without Hilbert_Choice
blanchet
parents: 40259
diff changeset
   564
         | (t, u) => t $ u)
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   565
      | repair t = t
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   566
    val t' = t |> repair |> fold (curry absdummy) (map snd params)
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   567
    fun do_instantiate th =
42270
5f2960582e45 make new Skolemizer more robust
blanchet
parents: 42107
diff changeset
   568
      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
   569
           |> 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
   570
                           is_metis_fresh_variable) o fst o fst) of
42270
5f2960582e45 make new Skolemizer more robust
blanchet
parents: 42107
diff changeset
   571
        [] => 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
   572
      | [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
   573
        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
   574
          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
   575
          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
   576
          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
   577
            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
   578
                                             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
   579
          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
   580
            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
   581
                         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
   582
          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
   583
            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
   584
                            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
   585
                        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
   586
          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
   587
            [pairself (cterm_of thy o Envir.norm_term env) (Var var, t')]
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
   588
        in th |> instantiate (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
   589
      | _ => 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
   590
  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
   591
    (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
   592
     THEN PRIMITIVE do_instantiate) st
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   593
  end
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   594
41135
8c5d44c7e8af tuning: unused var
blanchet
parents: 40868
diff changeset
   595
fun fix_exists_tac t =
43162
9a8acc5adfa3 added Metis examples to test the new type encodings
blanchet
parents: 43159
diff changeset
   596
  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
   597
7a02144874f3 more work on new Skolemizer without Hilbert_Choice
blanchet
parents: 40259
diff changeset
   598
fun release_quantifier_tac thy (skolem, t) =
41135
8c5d44c7e8af tuning: unused var
blanchet
parents: 40868
diff changeset
   599
  (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
   600
40258
2c0d8fe36c21 make handling of parameters more robust, by querying the goal
blanchet
parents: 40221
diff changeset
   601
fun release_clusters_tac _ _ _ [] = K all_tac
2c0d8fe36c21 make handling of parameters more robust, by querying the goal
blanchet
parents: 40221
diff changeset
   602
  | release_clusters_tac thy ax_counts substs
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   603
                         ((ax_no, cluster_no) :: clusters) =
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   604
    let
40261
7a02144874f3 more work on new Skolemizer without Hilbert_Choice
blanchet
parents: 40259
diff changeset
   605
      val cluster_of_var =
7a02144874f3 more work on new Skolemizer without Hilbert_Choice
blanchet
parents: 40259
diff changeset
   606
        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
   607
      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
   608
      val cluster_substs =
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   609
        substs
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   610
        |> map_filter (fn (ax_no', (_, (_, tsubst))) =>
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   611
                          if ax_no' = ax_no then
40261
7a02144874f3 more work on new Skolemizer without Hilbert_Choice
blanchet
parents: 40259
diff changeset
   612
                            tsubst |> map (apfst cluster_of_var)
7a02144874f3 more work on new Skolemizer without Hilbert_Choice
blanchet
parents: 40259
diff changeset
   613
                                   |> filter (in_right_cluster o fst)
7a02144874f3 more work on new Skolemizer without Hilbert_Choice
blanchet
parents: 40259
diff changeset
   614
                                   |> map (apfst snd)
7a02144874f3 more work on new Skolemizer without Hilbert_Choice
blanchet
parents: 40259
diff changeset
   615
                                   |> SOME
7a02144874f3 more work on new Skolemizer without Hilbert_Choice
blanchet
parents: 40259
diff changeset
   616
                          else
7a02144874f3 more work on new Skolemizer without Hilbert_Choice
blanchet
parents: 40259
diff changeset
   617
                            NONE)
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   618
      fun do_cluster_subst cluster_subst =
40261
7a02144874f3 more work on new Skolemizer without Hilbert_Choice
blanchet
parents: 40259
diff changeset
   619
        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
   620
      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
   621
    in
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   622
      rotate_tac first_prem
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   623
      THEN' (EVERY' (maps do_cluster_subst cluster_substs))
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   624
      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
   625
      THEN' release_clusters_tac thy ax_counts substs clusters
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   626
    end
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   627
40264
b91e2e16d994 fixed order of quantifier instantiation in new Skolemizer
blanchet
parents: 40261
diff changeset
   628
fun cluster_key ((ax_no, (cluster_no, index_no)), skolem) =
b91e2e16d994 fixed order of quantifier instantiation in new Skolemizer
blanchet
parents: 40261
diff changeset
   629
  (ax_no, (cluster_no, (skolem, index_no)))
b91e2e16d994 fixed order of quantifier instantiation in new Skolemizer
blanchet
parents: 40261
diff changeset
   630
fun cluster_ord p =
b91e2e16d994 fixed order of quantifier instantiation in new Skolemizer
blanchet
parents: 40261
diff changeset
   631
  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
   632
           (pairself cluster_key p)
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   633
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   634
val tysubst_ord =
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   635
  list_ord (prod_ord Term_Ord.fast_indexname_ord
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   636
                     (prod_ord Term_Ord.sort_ord Term_Ord.typ_ord))
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   637
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   638
structure Int_Tysubst_Table =
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   639
  Table(type key = int * (indexname * (sort * typ)) list
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   640
        val ord = prod_ord int_ord tysubst_ord)
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   641
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   642
structure Int_Pair_Graph =
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   643
  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
   644
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
   645
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
   646
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
   647
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   648
(* 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
   649
   "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
   650
   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
   651
   must be eliminated first. *)
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   652
fun discharge_skolem_premises ctxt axioms prems_imp_false =
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   653
  if prop_of prems_imp_false aconv @{prop False} then
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   654
    prems_imp_false
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   655
  else
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   656
    let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42354
diff changeset
   657
      val thy = Proof_Context.theory_of ctxt
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   658
      fun match_term p =
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   659
        let
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   660
          val (tyenv, tenv) =
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   661
            Pattern.first_order_match thy p (Vartab.empty, Vartab.empty)
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   662
          val tsubst =
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   663
            tenv |> Vartab.dest
42099
447fa058ab22 avoid evil "export_without_context", which breaks if there are local "fixes"
blanchet
parents: 42098
diff changeset
   664
                 |> 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
   665
                 |> sort (cluster_ord
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   666
                          o pairself (Meson_Clausify.cluster_of_zapped_var_name
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   667
                                      o fst o fst))
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   668
                 |> map (Meson.term_pair_of
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   669
                         #> pairself (Envir.subst_term_types tyenv))
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   670
          val tysubst = tyenv |> Vartab.dest
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   671
        in (tysubst, tsubst) end
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   672
      fun subst_info_for_prem subgoal_no prem =
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   673
        case prem of
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   674
          _ $ (Const (@{const_name Meson.skolem}, _) $ (_ $ t $ num)) =>
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   675
          let val ax_no = HOLogic.dest_nat num in
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   676
            (ax_no, (subgoal_no,
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   677
                     match_term (nth axioms ax_no |> the |> snd, t)))
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   678
          end
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   679
        | _ => raise TERM ("discharge_skolem_premises: Malformed premise",
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   680
                           [prem])
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   681
      fun cluster_of_var_name skolem s =
42098
f978caf60bbe more robust handling of variables in new Skolemizer
blanchet
parents: 41491
diff changeset
   682
        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
   683
          NONE => NONE
f978caf60bbe more robust handling of variables in new Skolemizer
blanchet
parents: 41491
diff changeset
   684
        | SOME ((ax_no, (cluster_no, _)), skolem') =>
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   685
          if skolem' = skolem andalso cluster_no > 0 then
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   686
            SOME (ax_no, cluster_no)
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   687
          else
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
      fun clusters_in_term skolem t =
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   690
        Term.add_var_names t [] |> map_filter (cluster_of_var_name skolem o fst)
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   691
      fun deps_for_term_subst (var, t) =
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   692
        case clusters_in_term false var of
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   693
          [] => NONE
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   694
        | [(ax_no, cluster_no)] =>
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   695
          SOME ((ax_no, cluster_no),
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   696
                clusters_in_term true t
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   697
                |> cluster_no > 1 ? cons (ax_no, cluster_no - 1))
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   698
        | _ => raise TERM ("discharge_skolem_premises: Expected Var", [var])
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   699
      val prems = Logic.strip_imp_prems (prop_of prems_imp_false)
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   700
      val substs = prems |> map2 subst_info_for_prem (1 upto length prems)
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   701
                         |> sort (int_ord o pairself fst)
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   702
      val depss = maps (map_filter deps_for_term_subst o snd o snd o snd) substs
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   703
      val clusters = maps (op ::) depss
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   704
      val ordered_clusters =
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   705
        Int_Pair_Graph.empty
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   706
        |> fold Int_Pair_Graph.default_node (map (rpair ()) clusters)
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   707
        |> fold Int_Pair_Graph.add_deps_acyclic depss
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   708
        |> Int_Pair_Graph.topological_order
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   709
        handle Int_Pair_Graph.CYCLES _ =>
40158
a88d6073b190 clearer error messages
blanchet
parents: 39978
diff changeset
   710
               error "Cannot replay Metis proof in Isabelle without \
a88d6073b190 clearer error messages
blanchet
parents: 39978
diff changeset
   711
                     \\"Hilbert_Choice\"."
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   712
      val ax_counts =
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   713
        Int_Tysubst_Table.empty
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   714
        |> fold (fn (ax_no, (_, (tysubst, _))) =>
43262
547a02d889f5 removed experimental code submitted by mistake
blanchet
parents: 43259
diff changeset
   715
                    Int_Tysubst_Table.map_default ((ax_no, tysubst), 0)
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   716
                                                  (Integer.add 1)) substs
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   717
        |> 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
   718
      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
   719
        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
   720
        |> 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
   721
                        | (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
   722
                          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
   723
                                        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
   724
                                    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
   725
                            SOME t
0e5d1e5e1177 use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents: 42337
diff changeset
   726
                          else
0e5d1e5e1177 use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents: 42337
diff changeset
   727
                            NONE)
0e5d1e5e1177 use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents: 42337
diff changeset
   728
      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
   729
        [] |> 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
   730
           |> 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
   731
           |> 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
   732
           |> 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
   733
                         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
   734
           |> sort shuffle_ord |> map (fst o snd)
42270
5f2960582e45 make new Skolemizer more robust
blanchet
parents: 42107
diff changeset
   735
(* for debugging only:
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   736
      fun string_for_subst_info (ax_no, (subgoal_no, (tysubst, tsubst))) =
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   737
        "ax: " ^ string_of_int ax_no ^ "; asm: " ^ string_of_int subgoal_no ^
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   738
        "; tysubst: " ^ PolyML.makestring tysubst ^ "; tsubst: {" ^
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   739
        commas (map ((fn (s, t) => s ^ " |-> " ^ t)
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   740
                     o pairself (Syntax.string_of_term ctxt)) tsubst) ^ "}"
40264
b91e2e16d994 fixed order of quantifier instantiation in new Skolemizer
blanchet
parents: 40261
diff changeset
   741
      val _ = tracing ("ORDERED CLUSTERS: " ^ PolyML.makestring ordered_clusters)
b91e2e16d994 fixed order of quantifier instantiation in new Skolemizer
blanchet
parents: 40261
diff changeset
   742
      val _ = tracing ("AXIOM COUNTS: " ^ PolyML.makestring ax_counts)
42339
0e5d1e5e1177 use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents: 42337
diff changeset
   743
      val _ = tracing ("OUTER PARAMS: " ^ PolyML.makestring outer_param_names)
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   744
      val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   745
                       cat_lines (map string_for_subst_info substs))
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   746
*)
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
   747
      fun cut_and_ex_tac axiom =
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
   748
        cut_rules_tac [axiom] 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
   749
        THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1)
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   750
      fun rotation_for_subgoal i =
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   751
        find_index (fn (_, (subgoal_no, _)) => subgoal_no = i) substs
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   752
    in
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   753
      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
   754
          (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
   755
                                  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
   756
                      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
   757
                      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
   758
              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
   759
              THEN match_tac [prems_imp_false] 1
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   760
              THEN ALLGOALS (fn i =>
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   761
                       rtac @{thm Meson.skolem_COMBK_I} i
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   762
                       THEN rotate_tac (rotation_for_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
   763
                       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
   764
                       THEN assume_tac i
42270
5f2960582e45 make new Skolemizer more robust
blanchet
parents: 42107
diff changeset
   765
                       THEN flexflex_tac)))
40158
a88d6073b190 clearer error messages
blanchet
parents: 39978
diff changeset
   766
      handle ERROR _ =>
a88d6073b190 clearer error messages
blanchet
parents: 39978
diff changeset
   767
             error ("Cannot replay Metis proof in Isabelle:\n\
a88d6073b190 clearer error messages
blanchet
parents: 39978
diff changeset
   768
                    \Error when discharging Skolem assumptions.")
39964
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   769
    end
8ca95d819c7c move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents: 39958
diff changeset
   770
39495
bb4fb9ffe2d1 added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff changeset
   771
end;