src/HOL/Tools/metis_tools.ML
author wenzelm
Wed, 17 Sep 2008 21:27:08 +0200
changeset 28262 aa7ca36d67fd
parent 28233 f14f34194f63
child 28528 0cf2749e8ef7
permissions -rw-r--r--
back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
     1
(*  Title:      HOL/Tools/metis_tools.ML
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
     2
    Author:     Kong W. Susanto and Lawrence C. Paulson, CU Computer Laboratory
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
     3
    Copyright   Cambridge University 2007
23447
1f16190e3836 tuned comments;
wenzelm
parents: 23442
diff changeset
     4
1f16190e3836 tuned comments;
wenzelm
parents: 23442
diff changeset
     5
HOL setup for the Metis prover (version 2.0 from 2007).
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
     6
*)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
     7
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
     8
signature METIS_TOOLS =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
     9
sig
24309
01f3e1a43c24 turned type_lits into configuration option (with attribute);
wenzelm
parents: 24300
diff changeset
    10
  val type_lits: bool Config.T
24319
944705cc79d2 export more tactics;
wenzelm
parents: 24309
diff changeset
    11
  val metis_tac: Proof.context -> thm list -> int -> tactic
944705cc79d2 export more tactics;
wenzelm
parents: 24309
diff changeset
    12
  val metisF_tac: Proof.context -> thm list -> int -> tactic
944705cc79d2 export more tactics;
wenzelm
parents: 24309
diff changeset
    13
  val metisH_tac: Proof.context -> thm list -> int -> tactic
944705cc79d2 export more tactics;
wenzelm
parents: 24309
diff changeset
    14
  val setup: theory -> theory
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    15
end
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    16
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    17
structure MetisTools: METIS_TOOLS =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    18
struct
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    19
24424
90500d3b5b5d Reconstruction bug fix
paulson
parents: 24319
diff changeset
    20
  structure Recon = ResReconstruct;
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    21
24309
01f3e1a43c24 turned type_lits into configuration option (with attribute);
wenzelm
parents: 24300
diff changeset
    22
  val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" true;
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    23
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    24
  (* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    25
  (* Useful Theorems                                                           *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    26
  (* ------------------------------------------------------------------------- *)
27239
f2f42f9fa09d pervasive RuleInsts;
wenzelm
parents: 27230
diff changeset
    27
  val EXCLUDED_MIDDLE = rotate_prems 1 (read_instantiate @{context} [(("R", 0), "False")] notE);
27230
c0103bc7f7eb RuleInsts.read_instantiate;
wenzelm
parents: 27178
diff changeset
    28
  val REFL_THM = incr_indexes 2 (Meson.make_meta_clause refl);  (*Rename from 0,1*)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    29
  val subst_em  = zero_var_indexes (subst RS EXCLUDED_MIDDLE);
27239
f2f42f9fa09d pervasive RuleInsts;
wenzelm
parents: 27230
diff changeset
    30
  val ssubst_em = read_instantiate @{context} [(("t", 0), "?s"), (("s", 0), "?t")] (sym RS subst_em);
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    31
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    32
  (* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    33
  (* Useful Functions                                                          *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    34
  (* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    35
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    36
  (* match untyped terms*)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    37
  fun untyped_aconv (Const(a,_))   (Const(b,_))   = (a=b)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    38
    | untyped_aconv (Free(a,_))    (Free(b,_))    = (a=b)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    39
    | untyped_aconv (Var((a,_),_)) (Var((b,_),_)) = (a=b)   (*the index is ignored!*)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    40
    | untyped_aconv (Bound i)      (Bound j)      = (i=j)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    41
    | untyped_aconv (Abs(a,_,t))  (Abs(b,_,u))    = (a=b) andalso untyped_aconv t u
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    42
    | untyped_aconv (t1$t2) (u1$u2)  = untyped_aconv t1 u1 andalso untyped_aconv t2 u2
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    43
    | untyped_aconv _              _              = false;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    44
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    45
  (* Finding the relative location of an untyped term within a list of terms *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    46
  fun get_index lit =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    47
    let val lit = Envir.eta_contract lit
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    48
        fun get n [] = raise Empty
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    49
          | get n (x::xs) = if untyped_aconv lit (Envir.eta_contract (HOLogic.dest_Trueprop x))
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    50
                            then n  else get (n+1) xs
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    51
    in get 1 end;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    52
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    53
  (* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    54
  (* HOL to FOL  (Isabelle to Metis)                                           *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    55
  (* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    56
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    57
  fun fn_isa_to_met "equal" = "="
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    58
    | fn_isa_to_met x       = x;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    59
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    60
  fun metis_lit b c args = (b, (c, args));
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    61
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    62
  fun hol_type_to_fol (ResClause.AtomV x) = Metis.Term.Var x
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    63
    | hol_type_to_fol (ResClause.AtomF x) = Metis.Term.Fn(x,[])
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    64
    | hol_type_to_fol (ResClause.Comp(tc,tps)) = Metis.Term.Fn(tc, map hol_type_to_fol tps);
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    65
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    66
  (*These two functions insert type literals before the real literals. That is the
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    67
    opposite order from TPTP linkup, but maybe OK.*)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    68
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    69
  fun hol_term_to_fol_FO tm =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    70
    case ResHolClause.strip_comb tm of
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    71
        (ResHolClause.CombConst(c,_,tys), tms) =>
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    72
          let val tyargs = map hol_type_to_fol tys
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    73
              val args   = map hol_term_to_fol_FO tms
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    74
          in Metis.Term.Fn (c, tyargs @ args) end
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    75
      | (ResHolClause.CombVar(v,_), []) => Metis.Term.Var v
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    76
      | _ => error "hol_term_to_fol_FO";
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    77
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    78
  fun hol_term_to_fol_HO (ResHolClause.CombVar(a, ty)) = Metis.Term.Var a
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    79
    | hol_term_to_fol_HO (ResHolClause.CombConst(a, ty, tylist)) =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    80
        Metis.Term.Fn(fn_isa_to_met a, map hol_type_to_fol tylist)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    81
    | hol_term_to_fol_HO (ResHolClause.CombApp(tm1,tm2)) =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    82
         Metis.Term.Fn(".", map hol_term_to_fol_HO [tm1,tm2]);
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    83
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    84
  fun hol_literal_to_fol true (ResHolClause.Literal (pol, tm)) =  (*first-order*)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    85
        let val (ResHolClause.CombConst(p,_,tys), tms) = ResHolClause.strip_comb tm
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    86
            val tylits = if p = "equal" then [] else map hol_type_to_fol tys
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    87
            val lits = map hol_term_to_fol_FO tms
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    88
        in metis_lit pol (fn_isa_to_met p) (tylits @ lits) end
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    89
    | hol_literal_to_fol false (ResHolClause.Literal (pol, tm)) =    (*higher-order*)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    90
        case ResHolClause.strip_comb tm of
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    91
            (ResHolClause.CombConst("equal",_,_), tms) =>
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    92
              metis_lit pol "=" (map hol_term_to_fol_HO tms)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    93
          | _ => metis_lit pol "{}" [hol_term_to_fol_HO tm];
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    94
24319
944705cc79d2 export more tactics;
wenzelm
parents: 24309
diff changeset
    95
  fun literals_of_hol_thm thy isFO t =
944705cc79d2 export more tactics;
wenzelm
parents: 24309
diff changeset
    96
        let val (lits, types_sorts) = ResHolClause.literals_of_term thy t
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    97
        in  (map (hol_literal_to_fol isFO) lits, types_sorts) end;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    98
24937
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24920
diff changeset
    99
  (*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*)
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24920
diff changeset
   100
  fun metis_of_typeLit pos (ResClause.LTVar (s,x))  = metis_lit pos s [Metis.Term.Var x]
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24920
diff changeset
   101
    | metis_of_typeLit pos (ResClause.LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])];
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   102
24940
8f9dea697b8d getting rid of type typ_var
paulson
parents: 24937
diff changeset
   103
  fun default_sort ctxt (TVar _) = false
8f9dea697b8d getting rid of type typ_var
paulson
parents: 24937
diff changeset
   104
    | default_sort ctxt (TFree(x,s)) = (s = Option.getOpt (Variable.def_sort ctxt (x,~1), []));
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   105
25713
1c45623e0edf removed duplicate CRITICAL markup;
wenzelm
parents: 25710
diff changeset
   106
  fun metis_of_tfree tf =
24937
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24920
diff changeset
   107
    Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_typeLit true tf));
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24920
diff changeset
   108
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24920
diff changeset
   109
  fun hol_thm_to_fol is_conjecture ctxt isFO th =
24319
944705cc79d2 export more tactics;
wenzelm
parents: 24309
diff changeset
   110
    let val thy = ProofContext.theory_of ctxt
944705cc79d2 export more tactics;
wenzelm
parents: 24309
diff changeset
   111
        val (mlits, types_sorts) =
944705cc79d2 export more tactics;
wenzelm
parents: 24309
diff changeset
   112
               (literals_of_hol_thm thy isFO o HOLogic.dest_Trueprop o prop_of) th
25713
1c45623e0edf removed duplicate CRITICAL markup;
wenzelm
parents: 25710
diff changeset
   113
    in
24937
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24920
diff changeset
   114
        if is_conjecture then
25713
1c45623e0edf removed duplicate CRITICAL markup;
wenzelm
parents: 25710
diff changeset
   115
            (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits), ResClause.add_typs types_sorts)
24937
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24920
diff changeset
   116
        else
25713
1c45623e0edf removed duplicate CRITICAL markup;
wenzelm
parents: 25710
diff changeset
   117
          let val tylits = ResClause.add_typs
24937
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24920
diff changeset
   118
                             (filter (not o default_sort ctxt) types_sorts)
25713
1c45623e0edf removed duplicate CRITICAL markup;
wenzelm
parents: 25710
diff changeset
   119
              val mtylits = if Config.get ctxt type_lits
24937
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24920
diff changeset
   120
                            then map (metis_of_typeLit false) tylits else []
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24920
diff changeset
   121
          in
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24920
diff changeset
   122
            (Metis.Thm.axiom (Metis.LiteralSet.fromList(mtylits @ mlits)), [])
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24920
diff changeset
   123
          end
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24920
diff changeset
   124
    end;
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   125
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   126
  (* ARITY CLAUSE *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   127
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   128
  fun m_arity_cls (ResClause.TConsLit (c,t,args)) =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   129
        metis_lit true (ResClause.make_type_class c) [Metis.Term.Fn(t, map Metis.Term.Var args)]
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   130
    | m_arity_cls (ResClause.TVarLit (c,str))     =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   131
        metis_lit false (ResClause.make_type_class c) [Metis.Term.Var str];
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   132
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   133
  (*TrueI is returned as the Isabelle counterpart because there isn't any.*)
24937
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24920
diff changeset
   134
  fun arity_cls (ResClause.ArityClause{conclLit,premLits,...}) =
25713
1c45623e0edf removed duplicate CRITICAL markup;
wenzelm
parents: 25710
diff changeset
   135
    (TrueI,
24937
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24920
diff changeset
   136
     Metis.Thm.axiom (Metis.LiteralSet.fromList (map m_arity_cls (conclLit :: premLits))));
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   137
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   138
  (* CLASSREL CLAUSE *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   139
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   140
  fun m_classrel_cls subclass superclass =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   141
    [metis_lit false subclass [Metis.Term.Var "T"], metis_lit true superclass [Metis.Term.Var "T"]];
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   142
24309
01f3e1a43c24 turned type_lits into configuration option (with attribute);
wenzelm
parents: 24300
diff changeset
   143
  fun classrel_cls (ResClause.ClassrelClause {axiom_name,subclass,superclass,...}) =
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   144
    (TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (m_classrel_cls subclass superclass)));
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   145
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   146
  (* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   147
  (* FOL to HOL  (Metis to Isabelle)                                           *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   148
  (* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   149
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   150
 datatype term_or_type = Term of Term.term | Type of Term.typ;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   151
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   152
  fun terms_of [] = []
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   153
    | terms_of (Term t :: tts) = t :: terms_of tts
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   154
    | terms_of (Type _ :: tts) = terms_of tts;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   155
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   156
  fun types_of [] = []
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   157
    | types_of (Term (Term.Var((a,idx), T)) :: tts) =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   158
        if String.isPrefix "_" a then
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   159
            (*Variable generated by Metis, which might have been a type variable.*)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   160
            TVar(("'" ^ a, idx), HOLogic.typeS) :: types_of tts
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   161
        else types_of tts
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   162
    | types_of (Term _ :: tts) = types_of tts
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   163
    | types_of (Type T :: tts) = T :: types_of tts;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   164
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   165
  fun apply_list rator nargs rands =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   166
    let val trands = terms_of rands
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   167
    in  if length trands = nargs then Term (list_comb(rator, trands))
26423
8408edac8f6b removed Display.raw_string_of_XXX (use regular Sign.string_of_XXX);
wenzelm
parents: 25761
diff changeset
   168
        else error
26957
e3f04fdd994d eliminated theory CPure;
wenzelm
parents: 26939
diff changeset
   169
          ("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global Pure.thy rator ^
26939
1035c89b4c02 moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents: 26931
diff changeset
   170
            " expected " ^ Int.toString nargs ^
26957
e3f04fdd994d eliminated theory CPure;
wenzelm
parents: 26939
diff changeset
   171
            " received " ^ commas (map (Syntax.string_of_term_global Pure.thy) trands))
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   172
    end;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   173
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   174
(*Instantiate constant c with the supplied types, but if they don't match its declared
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   175
  sort constraints, replace by a general type.*)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   176
fun const_of ctxt (c,Ts) =  Const (c, dummyT)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   177
24500
5e135602f660 type_infer: mode_pattern;
wenzelm
parents: 24494
diff changeset
   178
fun infer_types ctxt =
5e135602f660 type_infer: mode_pattern;
wenzelm
parents: 24494
diff changeset
   179
  Syntax.check_terms (ProofContext.set_mode ProofContext.mode_pattern ctxt);
25713
1c45623e0edf removed duplicate CRITICAL markup;
wenzelm
parents: 25710
diff changeset
   180
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   181
  (*We use 1 rather than 0 because variable references in clauses may otherwise conflict
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   182
    with variable constraints in the goal...at least, type inference often fails otherwise.
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   183
    SEE ALSO axiom_inf below.*)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   184
  fun mk_var w = Term.Var((w,1), HOLogic.typeT);
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   185
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   186
  (*include the default sort, if available*)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   187
  fun mk_tfree ctxt w =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   188
    let val ww = "'" ^ w
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   189
    in  TFree(ww, getOpt (Variable.def_sort ctxt (ww,~1), HOLogic.typeS))  end;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   190
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   191
  (*Remove the "apply" operator from an HO term*)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   192
  fun strip_happ args (Metis.Term.Fn(".",[t,u])) = strip_happ (u::args) t
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   193
    | strip_happ args x = (x, args);
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   194
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   195
  (*Maps metis terms to isabelle terms*)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   196
  fun fol_term_to_hol_RAW ctxt fol_tm =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   197
    let val thy = ProofContext.theory_of ctxt
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   198
        val _ = Output.debug (fn () => "fol_term_to_hol: " ^ Metis.Term.toString fol_tm)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   199
        fun tm_to_tt (Metis.Term.Var v) =
24424
90500d3b5b5d Reconstruction bug fix
paulson
parents: 24319
diff changeset
   200
               (case Recon.strip_prefix ResClause.tvar_prefix v of
90500d3b5b5d Reconstruction bug fix
paulson
parents: 24319
diff changeset
   201
                    SOME w => Type (Recon.make_tvar w)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   202
                  | NONE =>
24424
90500d3b5b5d Reconstruction bug fix
paulson
parents: 24319
diff changeset
   203
                case Recon.strip_prefix ResClause.schematic_var_prefix v of
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   204
                    SOME w => Term (mk_var w)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   205
                  | NONE   => Term (mk_var v) )
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   206
                      (*Var from Metis with a name like _nnn; possibly a type variable*)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   207
          | tm_to_tt (Metis.Term.Fn ("{}", [arg])) = tm_to_tt arg   (*hBOOL*)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   208
          | tm_to_tt (t as Metis.Term.Fn (".",_)) =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   209
              let val (rator,rands) = strip_happ [] t
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   210
              in  case rator of
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   211
                      Metis.Term.Fn(fname,ts) => applic_to_tt (fname, ts @ rands)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   212
                    | _ => case tm_to_tt rator of
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   213
                               Term t => Term (list_comb(t, terms_of (map tm_to_tt rands)))
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   214
                             | _ => error "tm_to_tt: HO application"
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   215
              end
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   216
          | tm_to_tt (Metis.Term.Fn (fname, args)) = applic_to_tt (fname,args)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   217
        and applic_to_tt ("=",ts) =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   218
              Term (list_comb(Const ("op =", HOLogic.typeT), terms_of (map tm_to_tt ts)))
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   219
          | applic_to_tt (a,ts) =
24424
90500d3b5b5d Reconstruction bug fix
paulson
parents: 24319
diff changeset
   220
              case Recon.strip_prefix ResClause.const_prefix a of
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   221
                  SOME b =>
24424
90500d3b5b5d Reconstruction bug fix
paulson
parents: 24319
diff changeset
   222
                    let val c = Recon.invert_const b
90500d3b5b5d Reconstruction bug fix
paulson
parents: 24319
diff changeset
   223
                        val ntypes = Recon.num_typargs thy c
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   224
                        val nterms = length ts - ntypes
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   225
                        val tts = map tm_to_tt ts
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   226
                        val tys = types_of (List.take(tts,ntypes))
24424
90500d3b5b5d Reconstruction bug fix
paulson
parents: 24319
diff changeset
   227
                        val ntyargs = Recon.num_typargs thy c
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   228
                    in if length tys = ntyargs then
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   229
                           apply_list (const_of ctxt (c, tys)) nterms (List.drop(tts,ntypes))
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   230
                       else error ("Constant " ^ c ^ " expects " ^ Int.toString ntyargs ^
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   231
                                   " but gets " ^ Int.toString (length tys) ^
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   232
                                   " type arguments\n" ^
26931
aa226d8405a8 cat_lines;
wenzelm
parents: 26928
diff changeset
   233
                                   cat_lines (map (Syntax.string_of_typ ctxt) tys) ^
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   234
                                   " the terms are \n" ^
26931
aa226d8405a8 cat_lines;
wenzelm
parents: 26928
diff changeset
   235
                                   cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   236
                       end
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   237
                | NONE => (*Not a constant. Is it a type constructor?*)
24424
90500d3b5b5d Reconstruction bug fix
paulson
parents: 24319
diff changeset
   238
              case Recon.strip_prefix ResClause.tconst_prefix a of
90500d3b5b5d Reconstruction bug fix
paulson
parents: 24319
diff changeset
   239
                  SOME b => Type (Term.Type(Recon.invert_type_const b, types_of (map tm_to_tt ts)))
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   240
                | NONE => (*Maybe a TFree. Should then check that ts=[].*)
24424
90500d3b5b5d Reconstruction bug fix
paulson
parents: 24319
diff changeset
   241
              case Recon.strip_prefix ResClause.tfree_prefix a of
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   242
                  SOME b => Type (mk_tfree ctxt b)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   243
                | NONE => (*a fixed variable? They are Skolem functions.*)
24424
90500d3b5b5d Reconstruction bug fix
paulson
parents: 24319
diff changeset
   244
              case Recon.strip_prefix ResClause.fixed_var_prefix a of
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   245
                  SOME b =>
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   246
                    let val opr = Term.Free(b, HOLogic.typeT)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   247
                    in  apply_list opr (length ts) (map tm_to_tt ts)  end
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   248
                | NONE => error ("unexpected metis function: " ^ a)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   249
    in  case tm_to_tt fol_tm of Term t => t | _ => error "fol_tm_to_tt: Term expected"  end;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   250
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   251
  fun fol_terms_to_hol ctxt fol_tms =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   252
    let val ts = map (fol_term_to_hol_RAW ctxt) fol_tms
24494
dc387e3999ec replaced ProofContext.infer_types by general Syntax.check_terms;
wenzelm
parents: 24424
diff changeset
   253
        val _ = Output.debug (fn () => "  calling type inference:")
24920
2a45e400fdad generic Syntax.pretty/string_of operations;
wenzelm
parents: 24855
diff changeset
   254
        val _ = app (fn t => Output.debug (fn () => Syntax.string_of_term ctxt t)) ts
24500
5e135602f660 type_infer: mode_pattern;
wenzelm
parents: 24494
diff changeset
   255
        val ts' = infer_types ctxt ts;
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   256
        val _ = app (fn t => Output.debug
24920
2a45e400fdad generic Syntax.pretty/string_of operations;
wenzelm
parents: 24855
diff changeset
   257
                      (fn () => "  final term: " ^ Syntax.string_of_term ctxt t ^
2a45e400fdad generic Syntax.pretty/string_of operations;
wenzelm
parents: 24855
diff changeset
   258
                                "  of type  " ^ Syntax.string_of_typ ctxt (type_of t)))
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   259
                    ts'
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   260
    in  ts'  end;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   261
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   262
  fun mk_not (Const ("Not", _) $ b) = b
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   263
    | mk_not b = HOLogic.mk_not b;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   264
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   265
  (* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   266
  (* FOL step Inference Rules                                                  *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   267
  (* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   268
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   269
  (*for debugging only*)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   270
  fun print_thpair (fth,th) =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   271
    (Output.debug (fn () => "=============================================");
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   272
     Output.debug (fn () => "Metis: " ^ Metis.Thm.toString fth);
26928
ca87aff1ad2d structure Display: less pervasive operations;
wenzelm
parents: 26561
diff changeset
   273
     Output.debug (fn () => "Isabelle: " ^ Display.string_of_thm th));
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   274
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   275
  fun lookth thpairs (fth : Metis.Thm.thm) =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   276
    valOf (AList.lookup (uncurry Metis.Thm.equal) thpairs fth)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   277
    handle Option => error ("Failed to find a Metis theorem " ^ Metis.Thm.toString fth);
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   278
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   279
  fun is_TrueI th = Thm.eq_thm(TrueI,th);
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   280
24974
a2f15968a6f2 reconstruction bug fix
paulson
parents: 24958
diff changeset
   281
  fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx));
a2f15968a6f2 reconstruction bug fix
paulson
parents: 24958
diff changeset
   282
a2f15968a6f2 reconstruction bug fix
paulson
parents: 24958
diff changeset
   283
  fun inst_excluded_middle th thy i_atm =
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   284
    let val vx = hd (term_vars (prop_of th))
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   285
        val substs = [(cterm_of thy vx, cterm_of thy i_atm)]
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   286
    in  cterm_instantiate substs th  end;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   287
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   288
  (* INFERENCE RULE: AXIOM *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   289
  fun axiom_inf ctxt thpairs th = incr_indexes 1 (lookth thpairs th);
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   290
      (*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   291
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   292
  (* INFERENCE RULE: ASSUME *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   293
  fun assume_inf ctxt atm =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   294
    inst_excluded_middle EXCLUDED_MIDDLE
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   295
      (ProofContext.theory_of ctxt)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   296
      (singleton (fol_terms_to_hol ctxt) (Metis.Term.Fn atm));
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   297
26561
394cd765643d Superficial changes
paulson
parents: 26423
diff changeset
   298
  (* INFERENCE RULE: INSTANTIATE (Subst). Type instantiations are ignored. Trying to reconstruct
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   299
     them admits new possibilities of errors, e.g. concerning sorts. Instead we try to arrange
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   300
     that new TVars are distinct and that types can be inferred from terms.*)
26561
394cd765643d Superficial changes
paulson
parents: 26423
diff changeset
   301
  fun inst_inf ctxt thpairs fsubst th =    
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   302
    let val thy = ProofContext.theory_of ctxt
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   303
        val i_th   = lookth thpairs th
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   304
        val i_th_vars = term_vars (prop_of i_th)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   305
        fun find_var x = valOf (List.find (fn Term.Var((a,_),_) => a=x) i_th_vars)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   306
        fun subst_translation (x,y) =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   307
              let val v = find_var x
26561
394cd765643d Superficial changes
paulson
parents: 26423
diff changeset
   308
                  val t = fol_term_to_hol_RAW ctxt y (*we call infer_types below*)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   309
              in  SOME (cterm_of thy v, t)  end
25713
1c45623e0edf removed duplicate CRITICAL markup;
wenzelm
parents: 25710
diff changeset
   310
              handle Option =>
1c45623e0edf removed duplicate CRITICAL markup;
wenzelm
parents: 25710
diff changeset
   311
                  (Output.debug (fn() => "List.find failed for the variable " ^ x ^
26928
ca87aff1ad2d structure Display: less pervasive operations;
wenzelm
parents: 26561
diff changeset
   312
                                         " in " ^ Display.string_of_thm i_th);
25713
1c45623e0edf removed duplicate CRITICAL markup;
wenzelm
parents: 25710
diff changeset
   313
                   NONE)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   314
        fun remove_typeinst (a, t) =
24424
90500d3b5b5d Reconstruction bug fix
paulson
parents: 24319
diff changeset
   315
              case Recon.strip_prefix ResClause.schematic_var_prefix a of
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   316
                  SOME b => SOME (b, t)
24424
90500d3b5b5d Reconstruction bug fix
paulson
parents: 24319
diff changeset
   317
                | NONE   => case Recon.strip_prefix ResClause.tvar_prefix a of
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   318
                  SOME _ => NONE          (*type instantiations are forbidden!*)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   319
                | NONE   => SOME (a,t)    (*internal Metis var?*)
26928
ca87aff1ad2d structure Display: less pervasive operations;
wenzelm
parents: 26561
diff changeset
   320
        val _ = Output.debug (fn () => "  isa th: " ^ Display.string_of_thm i_th)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   321
        val substs = List.mapPartial remove_typeinst (Metis.Subst.toList fsubst)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   322
        val (vars,rawtms) = ListPair.unzip (List.mapPartial subst_translation substs)
24500
5e135602f660 type_infer: mode_pattern;
wenzelm
parents: 24494
diff changeset
   323
        val tms = infer_types ctxt rawtms;
24974
a2f15968a6f2 reconstruction bug fix
paulson
parents: 24958
diff changeset
   324
        val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   325
        val substs' = ListPair.zip (vars, map ctm_of tms)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   326
        val _ = Output.debug (fn() => "subst_translations:")
26928
ca87aff1ad2d structure Display: less pervasive operations;
wenzelm
parents: 26561
diff changeset
   327
        val _ = app (fn (x,y) => Output.debug (fn () => Display.string_of_cterm x ^ " |-> " ^
ca87aff1ad2d structure Display: less pervasive operations;
wenzelm
parents: 26561
diff changeset
   328
                                                        Display.string_of_cterm y))
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   329
                  substs'
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   330
    in  cterm_instantiate substs' i_th  end;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   331
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   332
  (* INFERENCE RULE: RESOLVE *)
25713
1c45623e0edf removed duplicate CRITICAL markup;
wenzelm
parents: 25710
diff changeset
   333
24424
90500d3b5b5d Reconstruction bug fix
paulson
parents: 24319
diff changeset
   334
  (*Like RSN, but we rename apart only the type variables. Vars here typically have an index
90500d3b5b5d Reconstruction bug fix
paulson
parents: 24319
diff changeset
   335
    of 1, and the use of RSN would increase this typically to 3. Instantiations of those Vars
90500d3b5b5d Reconstruction bug fix
paulson
parents: 24319
diff changeset
   336
    could then fail. See comment on mk_var.*)
90500d3b5b5d Reconstruction bug fix
paulson
parents: 24319
diff changeset
   337
  fun resolve_inc_tyvars(tha,i,thb) =
90500d3b5b5d Reconstruction bug fix
paulson
parents: 24319
diff changeset
   338
    let val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
90500d3b5b5d Reconstruction bug fix
paulson
parents: 24319
diff changeset
   339
	val ths = Seq.list_of (bicompose false (false,tha,nprems_of tha) i thb)
25713
1c45623e0edf removed duplicate CRITICAL markup;
wenzelm
parents: 25710
diff changeset
   340
    in
24424
90500d3b5b5d Reconstruction bug fix
paulson
parents: 24319
diff changeset
   341
	case distinct Thm.eq_thm ths of
90500d3b5b5d Reconstruction bug fix
paulson
parents: 24319
diff changeset
   342
	  [th] => th
90500d3b5b5d Reconstruction bug fix
paulson
parents: 24319
diff changeset
   343
	| _ => raise THM ("resolve_inc_tyvars: unique result expected", i, [tha,thb])
90500d3b5b5d Reconstruction bug fix
paulson
parents: 24319
diff changeset
   344
    end;
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   345
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   346
  fun resolve_inf ctxt thpairs atm th1 th2 =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   347
    let
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   348
      val thy = ProofContext.theory_of ctxt
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   349
      val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
26928
ca87aff1ad2d structure Display: less pervasive operations;
wenzelm
parents: 26561
diff changeset
   350
      val _ = Output.debug (fn () => "  isa th1 (pos): " ^ Display.string_of_thm i_th1)
ca87aff1ad2d structure Display: less pervasive operations;
wenzelm
parents: 26561
diff changeset
   351
      val _ = Output.debug (fn () => "  isa th2 (neg): " ^ Display.string_of_thm i_th2)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   352
    in
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   353
      if is_TrueI i_th1 then i_th2 (*Trivial cases where one operand is type info*)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   354
      else if is_TrueI i_th2 then i_th1
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   355
      else
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   356
        let
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   357
          val i_atm = singleton (fol_terms_to_hol ctxt) (Metis.Term.Fn atm)
24920
2a45e400fdad generic Syntax.pretty/string_of operations;
wenzelm
parents: 24855
diff changeset
   358
          val _ = Output.debug (fn () => "  atom: " ^ Syntax.string_of_term ctxt i_atm)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   359
          val prems_th1 = prems_of i_th1
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   360
          val prems_th2 = prems_of i_th2
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   361
          val index_th1 = get_index (mk_not i_atm) prems_th1
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   362
                handle Empty => error "Failed to find literal in th1"
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   363
          val _ = Output.debug (fn () => "  index_th1: " ^ Int.toString index_th1)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   364
          val index_th2 = get_index i_atm prems_th2
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   365
                handle Empty => error "Failed to find literal in th2"
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   366
          val _ = Output.debug (fn () => "  index_th2: " ^ Int.toString index_th2)
24424
90500d3b5b5d Reconstruction bug fix
paulson
parents: 24319
diff changeset
   367
      in  resolve_inc_tyvars (Meson.select_literal index_th1 i_th1, index_th2, i_th2)  end
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   368
    end;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   369
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   370
  (* INFERENCE RULE: REFL *)
28262
aa7ca36d67fd back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
wenzelm
parents: 28233
diff changeset
   371
  val refl_x = cterm_of (the_context ()) (hd (term_vars (prop_of REFL_THM)));
24974
a2f15968a6f2 reconstruction bug fix
paulson
parents: 24958
diff changeset
   372
  val refl_idx = 1 + Thm.maxidx_of REFL_THM;
25713
1c45623e0edf removed duplicate CRITICAL markup;
wenzelm
parents: 25710
diff changeset
   373
24974
a2f15968a6f2 reconstruction bug fix
paulson
parents: 24958
diff changeset
   374
  fun refl_inf ctxt t =
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   375
    let val thy = ProofContext.theory_of ctxt
24974
a2f15968a6f2 reconstruction bug fix
paulson
parents: 24958
diff changeset
   376
        val i_t = singleton (fol_terms_to_hol ctxt) t
a2f15968a6f2 reconstruction bug fix
paulson
parents: 24958
diff changeset
   377
        val _ = Output.debug (fn () => "  term: " ^ Syntax.string_of_term ctxt i_t)
a2f15968a6f2 reconstruction bug fix
paulson
parents: 24958
diff changeset
   378
        val c_t = cterm_incr_types thy refl_idx i_t
a2f15968a6f2 reconstruction bug fix
paulson
parents: 24958
diff changeset
   379
    in  cterm_instantiate [(refl_x, c_t)] REFL_THM  end;
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   380
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   381
  fun get_ty_arg_size thy (Const("op =",_)) = 0  (*equality has no type arguments*)
24424
90500d3b5b5d Reconstruction bug fix
paulson
parents: 24319
diff changeset
   382
    | get_ty_arg_size thy (Const(c,_))      = (Recon.num_typargs thy c handle TYPE _ => 0)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   383
    | get_ty_arg_size thy _      = 0;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   384
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   385
  (* INFERENCE RULE: EQUALITY *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   386
  fun equality_inf ctxt isFO thpairs (pos,atm) fp fr =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   387
    let val thy = ProofContext.theory_of ctxt
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   388
        val [i_atm,i_tm] = fol_terms_to_hol ctxt [Metis.Term.Fn atm, fr]
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   389
        val _ = Output.debug (fn () => "sign of the literal: " ^ Bool.toString pos)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   390
        fun replace_item_list lx 0 (l::ls) = lx::ls
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   391
          | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   392
        fun path_finder_FO tm (p::ps) =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   393
              let val (tm1,args) = Term.strip_comb tm
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   394
                  val adjustment = get_ty_arg_size thy tm1
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   395
                  val p' = if adjustment > p then p else p-adjustment
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   396
                  val tm_p = List.nth(args,p')
24920
2a45e400fdad generic Syntax.pretty/string_of operations;
wenzelm
parents: 24855
diff changeset
   397
                    handle Subscript => error ("equality_inf: " ^ Int.toString p ^ " adj " ^
2a45e400fdad generic Syntax.pretty/string_of operations;
wenzelm
parents: 24855
diff changeset
   398
                      Int.toString adjustment  ^ " term " ^  Syntax.string_of_term ctxt tm)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   399
              in
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   400
                  Output.debug (fn () => "path_finder: " ^ Int.toString p ^
24920
2a45e400fdad generic Syntax.pretty/string_of operations;
wenzelm
parents: 24855
diff changeset
   401
                                        "  " ^ Syntax.string_of_term ctxt tm_p);
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   402
                  if null ps   (*FIXME: why not use pattern-matching and avoid repetition*)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   403
                  then (tm_p, list_comb (tm1, replace_item_list (Term.Bound 0) p' args))
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   404
                  else let val (r,t) = path_finder_FO tm_p ps
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   405
                       in (r, list_comb (tm1, replace_item_list t p' args)) end
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   406
              end
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   407
        fun path_finder_HO tm [] = (tm, Term.Bound 0)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   408
          | path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   409
          | path_finder_HO (t$u) (p::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   410
        fun path_finder true tm ps = path_finder_FO tm ps
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   411
          | path_finder false (tm as Const("op =",_) $ _ $ _) (p::ps) =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   412
               (*equality: not curried, as other predicates are*)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   413
               if p=0 then path_finder_HO tm (0::1::ps)  (*select first operand*)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   414
               else path_finder_HO tm (p::ps)        (*1 selects second operand*)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   415
          | path_finder false tm (p::ps) =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   416
               path_finder_HO tm ps      (*if not equality, ignore head to skip hBOOL*)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   417
        fun path_finder_lit ((nt as Term.Const ("Not", _)) $ tm_a) idx =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   418
              let val (tm, tm_rslt) = path_finder isFO tm_a idx
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   419
              in (tm, nt $ tm_rslt) end
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   420
          | path_finder_lit tm_a idx = path_finder isFO tm_a idx
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   421
        val (tm_subst, body) = path_finder_lit i_atm fp
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   422
        val tm_abs = Term.Abs("x", Term.type_of tm_subst, body)
24920
2a45e400fdad generic Syntax.pretty/string_of operations;
wenzelm
parents: 24855
diff changeset
   423
        val _ = Output.debug (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
2a45e400fdad generic Syntax.pretty/string_of operations;
wenzelm
parents: 24855
diff changeset
   424
        val _ = Output.debug (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
2a45e400fdad generic Syntax.pretty/string_of operations;
wenzelm
parents: 24855
diff changeset
   425
        val _ = Output.debug (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   426
        val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst)  (*ill typed but gives right max*)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   427
        val subst' = incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
26928
ca87aff1ad2d structure Display: less pervasive operations;
wenzelm
parents: 26561
diff changeset
   428
        val _ = Output.debug (fn () => "subst' " ^ Display.string_of_thm subst')
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   429
        val eq_terms = map (pairself (cterm_of thy))
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   430
                           (ListPair.zip (term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   431
    in  cterm_instantiate eq_terms subst'  end;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   432
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   433
  fun step ctxt isFO thpairs (fol_th, Metis.Proof.Axiom _)                        =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   434
        axiom_inf ctxt thpairs fol_th
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   435
    | step ctxt isFO thpairs (_, Metis.Proof.Assume f_atm)                        =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   436
        assume_inf ctxt f_atm
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   437
    | step ctxt isFO thpairs (_, Metis.Proof.Subst(f_subst, f_th1))                =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   438
        inst_inf ctxt thpairs f_subst f_th1
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   439
    | step ctxt isFO thpairs (_, Metis.Proof.Resolve(f_atm, f_th1, f_th2))        =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   440
        resolve_inf ctxt thpairs f_atm f_th1 f_th2
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   441
    | step ctxt isFO thpairs (_, Metis.Proof.Refl f_tm)                           =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   442
        refl_inf ctxt f_tm
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   443
    | step ctxt isFO thpairs (_, Metis.Proof.Equality(f_lit, f_p, f_r)) =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   444
        equality_inf ctxt isFO thpairs f_lit f_p f_r;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   445
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   446
  val factor = Seq.hd o distinct_subgoals_tac;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   447
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   448
  fun real_literal (b, (c, _)) = not (String.isPrefix ResClause.class_prefix c);
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   449
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   450
  fun translate isFO _    thpairs [] = thpairs
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   451
    | translate isFO ctxt thpairs ((fol_th, inf) :: infpairs) =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   452
        let val _ = Output.debug (fn () => "=============================================")
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   453
            val _ = Output.debug (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   454
            val _ = Output.debug (fn () => "INFERENCE: " ^ Metis.Proof.inferenceToString inf)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   455
            val th = Meson.flexflex_first_order (factor (step ctxt isFO thpairs (fol_th, inf)))
26928
ca87aff1ad2d structure Display: less pervasive operations;
wenzelm
parents: 26561
diff changeset
   456
            val _ = Output.debug (fn () => "ISABELLE THM: " ^ Display.string_of_thm th)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   457
            val _ = Output.debug (fn () => "=============================================")
24424
90500d3b5b5d Reconstruction bug fix
paulson
parents: 24319
diff changeset
   458
            val n_metis_lits = length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th)))
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   459
        in
24424
90500d3b5b5d Reconstruction bug fix
paulson
parents: 24319
diff changeset
   460
            if nprems_of th = n_metis_lits then ()
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   461
            else error "Metis: proof reconstruction has gone wrong";
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   462
            translate isFO ctxt ((fol_th, th) :: thpairs) infpairs
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   463
        end;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   464
24855
161eb8381b49 metis method: used theorems
paulson
parents: 24827
diff changeset
   465
  (*Determining which axiom clauses are actually used*)
25713
1c45623e0edf removed duplicate CRITICAL markup;
wenzelm
parents: 25710
diff changeset
   466
  fun used_axioms axioms (th, Metis.Proof.Axiom _) = SOME (lookth axioms th)
24855
161eb8381b49 metis method: used theorems
paulson
parents: 24827
diff changeset
   467
    | used_axioms axioms _                         = NONE;
161eb8381b49 metis method: used theorems
paulson
parents: 24827
diff changeset
   468
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   469
  (* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   470
  (* Translation of HO Clauses                                                 *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   471
  (* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   472
27178
c8ddb3000743 ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27153
diff changeset
   473
  fun cnf_th thy th = hd (ResAxioms.cnf_axiom thy th);
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   474
28262
aa7ca36d67fd back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
wenzelm
parents: 28233
diff changeset
   475
  val equal_imp_fequal' = cnf_th (the_context ()) (thm"equal_imp_fequal");
aa7ca36d67fd back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
wenzelm
parents: 28233
diff changeset
   476
  val fequal_imp_equal' = cnf_th (the_context ()) (thm"fequal_imp_equal");
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   477
28262
aa7ca36d67fd back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
wenzelm
parents: 28233
diff changeset
   478
  val comb_I = cnf_th (the_context ()) ResHolClause.comb_I;
aa7ca36d67fd back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
wenzelm
parents: 28233
diff changeset
   479
  val comb_K = cnf_th (the_context ()) ResHolClause.comb_K;
aa7ca36d67fd back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
wenzelm
parents: 28233
diff changeset
   480
  val comb_B = cnf_th (the_context ()) ResHolClause.comb_B;
aa7ca36d67fd back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
wenzelm
parents: 28233
diff changeset
   481
  val comb_C = cnf_th (the_context ()) ResHolClause.comb_C;
aa7ca36d67fd back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
wenzelm
parents: 28233
diff changeset
   482
  val comb_S = cnf_th (the_context ()) ResHolClause.comb_S;
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   483
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   484
  fun type_ext thy tms =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   485
    let val subs = ResAtp.tfree_classes_of_terms tms
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   486
        val supers = ResAtp.tvar_classes_of_terms tms
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   487
        and tycons = ResAtp.type_consts_of_terms thy tms
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   488
        val arity_clauses = ResClause.make_arity_clauses thy tycons supers
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   489
        val (supers',arity_clauses) = ResClause.make_arity_clauses thy tycons supers
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   490
        val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
24309
01f3e1a43c24 turned type_lits into configuration option (with attribute);
wenzelm
parents: 24300
diff changeset
   491
    in  map classrel_cls classrel_clauses @ map arity_cls arity_clauses
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   492
    end;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   493
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   494
  (* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   495
  (* Logic maps manage the interface between HOL and first-order logic.        *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   496
  (* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   497
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   498
  type logic_map =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   499
    {isFO   : bool,
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   500
     axioms : (Metis.Thm.thm * Thm.thm) list,
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   501
     tfrees : ResClause.type_literal list};
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   502
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   503
  fun const_in_metis c (pol,(pred,tm_list)) =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   504
    let
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   505
      fun in_mterm (Metis.Term.Var nm) = false
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   506
        | in_mterm (Metis.Term.Fn (".", tm_list)) = exists in_mterm tm_list
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   507
        | in_mterm (Metis.Term.Fn (nm, tm_list)) = c=nm orelse exists in_mterm tm_list
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   508
    in  c=pred orelse exists in_mterm tm_list  end;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   509
24937
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24920
diff changeset
   510
  (*Extract TFree constraints from context to include as conjecture clauses*)
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24920
diff changeset
   511
  fun init_tfrees ctxt =
24940
8f9dea697b8d getting rid of type typ_var
paulson
parents: 24937
diff changeset
   512
    let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts
24937
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24920
diff changeset
   513
    in  ResClause.add_typs (Vartab.fold add (#2 (Variable.constraints_of ctxt)) []) end;
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24920
diff changeset
   514
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   515
  (*transform isabelle clause to metis clause *)
24937
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24920
diff changeset
   516
  fun add_thm is_conjecture ctxt (ith, {isFO, axioms, tfrees}) : logic_map =
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24920
diff changeset
   517
    let val (mth, tfree_lits) = hol_thm_to_fol is_conjecture ctxt isFO ith
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   518
    in
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   519
       {isFO = isFO,
24937
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24920
diff changeset
   520
        axioms = (mth, Meson.make_meta_clause ith) :: axioms,
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   521
        tfrees = tfree_lits union tfrees}
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   522
    end;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   523
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   524
  (*transform isabelle type / arity clause to metis clause *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   525
  fun add_type_thm [] lmap = lmap
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   526
    | add_type_thm ((ith, mth) :: cls) {isFO, axioms, tfrees} =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   527
        add_type_thm cls {isFO = isFO,
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   528
                          axioms = (mth, ith) :: axioms,
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   529
                          tfrees = tfrees}
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   530
24937
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24920
diff changeset
   531
  (*Insert non-logical axioms corresponding to all accumulated TFrees*)
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24920
diff changeset
   532
  fun add_tfrees {isFO, axioms, tfrees} : logic_map =
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24920
diff changeset
   533
       {isFO = isFO,
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24920
diff changeset
   534
        axioms = (map (fn tf => (metis_of_tfree tf, TrueI)) (distinct op= tfrees)) @ axioms,
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24920
diff changeset
   535
        tfrees = tfrees};
25713
1c45623e0edf removed duplicate CRITICAL markup;
wenzelm
parents: 25710
diff changeset
   536
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   537
  (* Function to generate metis clauses, including comb and type clauses *)
24958
ff15f76741bd rationalized redundant code
paulson
parents: 24940
diff changeset
   538
  fun build_map mode ctxt cls ths =
ff15f76741bd rationalized redundant code
paulson
parents: 24940
diff changeset
   539
    let val thy = ProofContext.theory_of ctxt
ff15f76741bd rationalized redundant code
paulson
parents: 24940
diff changeset
   540
        val all_thms_FO = forall (Meson.is_fol_term thy o prop_of)
ff15f76741bd rationalized redundant code
paulson
parents: 24940
diff changeset
   541
        val isFO = (mode = ResAtp.Fol) orelse
ff15f76741bd rationalized redundant code
paulson
parents: 24940
diff changeset
   542
                   (mode <> ResAtp.Hol andalso all_thms_FO (cls @ ths))
25713
1c45623e0edf removed duplicate CRITICAL markup;
wenzelm
parents: 25710
diff changeset
   543
        val lmap0 = foldl (add_thm true ctxt)
24937
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24920
diff changeset
   544
                          {isFO = isFO, axioms = [], tfrees = init_tfrees ctxt} cls
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24920
diff changeset
   545
        val lmap = foldl (add_thm false ctxt) (add_tfrees lmap0) ths
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   546
        val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   547
        fun used c = exists (Metis.LiteralSet.exists (const_in_metis c)) clause_lists
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   548
        (*Now check for the existence of certain combinators*)
24827
646bdc51eb7d combinator translation
paulson
parents: 24500
diff changeset
   549
        val thI  = if used "c_COMBI" then [comb_I] else []
646bdc51eb7d combinator translation
paulson
parents: 24500
diff changeset
   550
        val thK  = if used "c_COMBK" then [comb_K] else []
646bdc51eb7d combinator translation
paulson
parents: 24500
diff changeset
   551
        val thB   = if used "c_COMBB" then [comb_B] else []
646bdc51eb7d combinator translation
paulson
parents: 24500
diff changeset
   552
        val thC   = if used "c_COMBC" then [comb_C] else []
646bdc51eb7d combinator translation
paulson
parents: 24500
diff changeset
   553
        val thS   = if used "c_COMBS" then [comb_S] else []
646bdc51eb7d combinator translation
paulson
parents: 24500
diff changeset
   554
        val thEQ  = if used "c_fequal" then [fequal_imp_equal', equal_imp_fequal'] else []
25713
1c45623e0edf removed duplicate CRITICAL markup;
wenzelm
parents: 25710
diff changeset
   555
        val lmap' = if isFO then lmap
24937
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24920
diff changeset
   556
                    else foldl (add_thm false ctxt) lmap (thEQ @ thS @ thC @ thB @ thK @ thI)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   557
    in
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   558
        add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap'
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   559
    end;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   560
25724
31e7bd574eb9 made refute non-critical (seems to work after avoiding floating point random numbers);
wenzelm
parents: 25713
diff changeset
   561
  fun refute cls =
31e7bd574eb9 made refute non-critical (seems to work after avoiding floating point random numbers);
wenzelm
parents: 25713
diff changeset
   562
      Metis.Resolution.loop (Metis.Resolution.new Metis.Resolution.default cls);
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   563
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   564
  fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const);
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   565
24855
161eb8381b49 metis method: used theorems
paulson
parents: 24827
diff changeset
   566
  fun common_thm ths1 ths2 = exists (member Thm.eq_thm ths1) (map Meson.make_meta_clause ths2);
161eb8381b49 metis method: used theorems
paulson
parents: 24827
diff changeset
   567
28233
f14f34194f63 The metis method now fails in the usual manner, rather than raising an exception,
paulson
parents: 28175
diff changeset
   568
  exception METIS of string;
f14f34194f63 The metis method now fails in the usual manner, rather than raising an exception,
paulson
parents: 28175
diff changeset
   569
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   570
  (* Main function to start metis prove and reconstruction *)
24855
161eb8381b49 metis method: used theorems
paulson
parents: 24827
diff changeset
   571
  fun FOL_SOLVE mode ctxt cls ths0 =
27178
c8ddb3000743 ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27153
diff changeset
   572
    let val thy = ProofContext.theory_of ctxt
27865
27a8ad9612a3 moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
wenzelm
parents: 27239
diff changeset
   573
        val th_cls_pairs = map (fn th => (Thm.get_name_hint th, ResAxioms.cnf_axiom thy th)) ths0
24855
161eb8381b49 metis method: used theorems
paulson
parents: 24827
diff changeset
   574
        val ths = List.concat (map #2 th_cls_pairs)
28233
f14f34194f63 The metis method now fails in the usual manner, rather than raising an exception,
paulson
parents: 28175
diff changeset
   575
        val _ = if exists(is_false o prop_of) cls 
f14f34194f63 The metis method now fails in the usual manner, rather than raising an exception,
paulson
parents: 28175
diff changeset
   576
                then raise METIS "problem contains the empty clause"
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   577
                else ();
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   578
        val _ = Output.debug (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
26928
ca87aff1ad2d structure Display: less pervasive operations;
wenzelm
parents: 26561
diff changeset
   579
        val _ = app (fn th => Output.debug (fn () => Display.string_of_thm th)) cls
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   580
        val _ = Output.debug (fn () => "THEOREM CLAUSES")
26928
ca87aff1ad2d structure Display: less pervasive operations;
wenzelm
parents: 26561
diff changeset
   581
        val _ = app (fn th => Output.debug (fn () => Display.string_of_thm th)) ths
24958
ff15f76741bd rationalized redundant code
paulson
parents: 24940
diff changeset
   582
        val {isFO,axioms,tfrees} = build_map mode ctxt cls ths
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   583
        val _ = if null tfrees then ()
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   584
                else (Output.debug (fn () => "TFREE CLAUSES");
24937
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24920
diff changeset
   585
                      app (fn tf => Output.debug (fn _ => ResClause.tptp_of_typeLit true tf)) tfrees)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   586
        val _ = Output.debug (fn () => "CLAUSES GIVEN TO METIS")
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   587
        val thms = map #1 axioms
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   588
        val _ = app (fn th => Output.debug (fn () => Metis.Thm.toString th)) thms
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   589
        val _ = if isFO
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   590
                then Output.debug (fn () => "goal is first-order")
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   591
                else Output.debug (fn () => "goal is higher-order")
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   592
        val _ = Output.debug (fn () => "START METIS PROVE PROCESS")
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   593
    in
25713
1c45623e0edf removed duplicate CRITICAL markup;
wenzelm
parents: 25710
diff changeset
   594
        case refute thms of
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   595
            Metis.Resolution.Contradiction mth =>
28233
f14f34194f63 The metis method now fails in the usual manner, rather than raising an exception,
paulson
parents: 28175
diff changeset
   596
              let val _ = Output.debug (fn () => "METIS RECONSTRUCTION START: " ^
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   597
                            Metis.Thm.toString mth)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   598
                  val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   599
                               (*add constraints arising from converting goal to clause form*)
24855
161eb8381b49 metis method: used theorems
paulson
parents: 24827
diff changeset
   600
                  val proof = Metis.Proof.proof mth
161eb8381b49 metis method: used theorems
paulson
parents: 24827
diff changeset
   601
                  val result = translate isFO ctxt' axioms proof
161eb8381b49 metis method: used theorems
paulson
parents: 24827
diff changeset
   602
                  and used = List.mapPartial (used_axioms axioms) proof
161eb8381b49 metis method: used theorems
paulson
parents: 24827
diff changeset
   603
                  val _ = Output.debug (fn () => "METIS COMPLETED...clauses actually used:")
26928
ca87aff1ad2d structure Display: less pervasive operations;
wenzelm
parents: 26561
diff changeset
   604
	          val _ = app (fn th => Output.debug (fn () => Display.string_of_thm th)) used
24855
161eb8381b49 metis method: used theorems
paulson
parents: 24827
diff changeset
   605
	          val unused = filter (fn (a,cls) => not (common_thm used cls)) th_cls_pairs
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   606
              in
24855
161eb8381b49 metis method: used theorems
paulson
parents: 24827
diff changeset
   607
                  if null unused then ()
161eb8381b49 metis method: used theorems
paulson
parents: 24827
diff changeset
   608
                  else warning ("Unused theorems: " ^ commas (map #1 unused));
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   609
                  case result of
28233
f14f34194f63 The metis method now fails in the usual manner, rather than raising an exception,
paulson
parents: 28175
diff changeset
   610
                      (_,ith)::_ => 
f14f34194f63 The metis method now fails in the usual manner, rather than raising an exception,
paulson
parents: 28175
diff changeset
   611
                          (Output.debug (fn () => "success: " ^ Display.string_of_thm ith); 
f14f34194f63 The metis method now fails in the usual manner, rather than raising an exception,
paulson
parents: 28175
diff changeset
   612
                           [ith])
f14f34194f63 The metis method now fails in the usual manner, rather than raising an exception,
paulson
parents: 28175
diff changeset
   613
                    | _ => (Output.debug (fn () => "Metis: no result"); 
f14f34194f63 The metis method now fails in the usual manner, rather than raising an exception,
paulson
parents: 28175
diff changeset
   614
                            [])
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   615
              end
28233
f14f34194f63 The metis method now fails in the usual manner, rather than raising an exception,
paulson
parents: 28175
diff changeset
   616
          | Metis.Resolution.Satisfiable _ => 
f14f34194f63 The metis method now fails in the usual manner, rather than raising an exception,
paulson
parents: 28175
diff changeset
   617
	      (Output.debug (fn () => "Metis: No first-order proof with the lemmas supplied"); 
f14f34194f63 The metis method now fails in the usual manner, rather than raising an exception,
paulson
parents: 28175
diff changeset
   618
	       [])
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   619
    end;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   620
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   621
  fun metis_general_tac mode ctxt ths i st0 =
24041
d5845b7c1a24 metis_tac: proper context (ProofContext.init it *not* sufficient);
wenzelm
parents: 23447
diff changeset
   622
    let val _ = Output.debug (fn () =>
26928
ca87aff1ad2d structure Display: less pervasive operations;
wenzelm
parents: 26561
diff changeset
   623
          "Metis called with theorems " ^ cat_lines (map Display.string_of_thm ths))
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   624
    in
25761
466e714de2fc testing for empty sort
paulson
parents: 25724
diff changeset
   625
       if exists_type ResAxioms.type_has_empty_sort (prop_of st0)  
28233
f14f34194f63 The metis method now fails in the usual manner, rather than raising an exception,
paulson
parents: 28175
diff changeset
   626
       then (warning "Proof state contains the empty sort"; Seq.empty)
f14f34194f63 The metis method now fails in the usual manner, rather than raising an exception,
paulson
parents: 28175
diff changeset
   627
       else 
f14f34194f63 The metis method now fails in the usual manner, rather than raising an exception,
paulson
parents: 28175
diff changeset
   628
	 (Meson.MESON ResAxioms.neg_clausify (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) i
f14f34194f63 The metis method now fails in the usual manner, rather than raising an exception,
paulson
parents: 28175
diff changeset
   629
	  THEN ResAxioms.expand_defs_tac st0) st0
f14f34194f63 The metis method now fails in the usual manner, rather than raising an exception,
paulson
parents: 28175
diff changeset
   630
    end
f14f34194f63 The metis method now fails in the usual manner, rather than raising an exception,
paulson
parents: 28175
diff changeset
   631
    handle METIS s => (warning ("Metis: " ^ s); Seq.empty);
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   632
24041
d5845b7c1a24 metis_tac: proper context (ProofContext.init it *not* sufficient);
wenzelm
parents: 23447
diff changeset
   633
  val metis_tac = metis_general_tac ResAtp.Auto;
d5845b7c1a24 metis_tac: proper context (ProofContext.init it *not* sufficient);
wenzelm
parents: 23447
diff changeset
   634
  val metisF_tac = metis_general_tac ResAtp.Fol;
d5845b7c1a24 metis_tac: proper context (ProofContext.init it *not* sufficient);
wenzelm
parents: 23447
diff changeset
   635
  val metisH_tac = metis_general_tac ResAtp.Hol;
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   636
24041
d5845b7c1a24 metis_tac: proper context (ProofContext.init it *not* sufficient);
wenzelm
parents: 23447
diff changeset
   637
  fun method mode = Method.thms_ctxt_args (fn ths => fn ctxt =>
25693
31232fe5a6ad Deleted redundant setmp calls
paulson
parents: 24974
diff changeset
   638
    Method.SIMPLE_METHOD' (CHANGED_PROP o metis_general_tac mode ctxt ths));
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   639
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   640
  val setup =
24309
01f3e1a43c24 turned type_lits into configuration option (with attribute);
wenzelm
parents: 24300
diff changeset
   641
    type_lits_setup #>
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   642
    Method.add_methods
24041
d5845b7c1a24 metis_tac: proper context (ProofContext.init it *not* sufficient);
wenzelm
parents: 23447
diff changeset
   643
      [("metis", method ResAtp.Auto, "METIS for FOL & HOL problems"),
d5845b7c1a24 metis_tac: proper context (ProofContext.init it *not* sufficient);
wenzelm
parents: 23447
diff changeset
   644
       ("metisF", method ResAtp.Fol, "METIS for FOL problems"),
d5845b7c1a24 metis_tac: proper context (ProofContext.init it *not* sufficient);
wenzelm
parents: 23447
diff changeset
   645
       ("metisH", method ResAtp.Hol, "METIS for HOL problems"),
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   646
       ("finish_clausify",
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   647
         Method.no_args (Method.SIMPLE_METHOD' (K (ResAxioms.expand_defs_tac refl))),
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   648
    "cleanup after conversion to clauses")];
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   649
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   650
end;