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