move Metis into Plain
authorblanchet
Mon Oct 04 22:45:09 2010 +0200 (2010-10-04)
changeset 3994678faa9b31202
parent 39945 277addece9b7
child 39947 f95834c8bb4d
move Metis into Plain
src/HOL/IsaMakefile
src/HOL/List.thy
src/HOL/Meson.thy
src/HOL/Metis.thy
src/HOL/Plain.thy
src/HOL/Quotient.thy
src/HOL/Refute.thy
src/HOL/Sledgehammer.thy
src/HOL/Tools/Metis/metis_reconstruct.ML
src/HOL/Tools/Metis/metis_tactics.ML
src/HOL/Tools/Metis/metis_translate.ML
src/HOL/Tools/Sledgehammer/metis_reconstruct.ML
src/HOL/Tools/Sledgehammer/metis_tactics.ML
src/HOL/Tools/Sledgehammer/metis_translate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
     1.1 --- a/src/HOL/IsaMakefile	Mon Oct 04 22:01:34 2010 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Mon Oct 04 22:45:09 2010 +0200
     1.3 @@ -155,6 +155,7 @@
     1.4    Inductive.thy \
     1.5    Lattices.thy \
     1.6    Meson.thy \
     1.7 +  Metis.thy \
     1.8    Nat.thy \
     1.9    Option.thy \
    1.10    Orderings.thy \
    1.11 @@ -204,6 +205,9 @@
    1.12    Tools/lin_arith.ML \
    1.13    Tools/Meson/meson.ML \
    1.14    Tools/Meson/meson_clausify.ML \
    1.15 +  Tools/Metis/metis_reconstruct.ML \
    1.16 +  Tools/Metis/metis_translate.ML \
    1.17 +  Tools/Metis/metis_tactics.ML \
    1.18    Tools/nat_arith.ML \
    1.19    Tools/primrec.ML \
    1.20    Tools/prop_logic.ML \
    1.21 @@ -222,6 +226,7 @@
    1.22    $(SRC)/Provers/Arith/fast_lin_arith.ML \
    1.23    $(SRC)/Provers/order.ML \
    1.24    $(SRC)/Provers/trancl.ML \
    1.25 +  $(SRC)/Tools/Metis/metis.ML \
    1.26    $(SRC)/Tools/rat.ML
    1.27  
    1.28  $(OUT)/HOL-Plain: plain.ML $(PLAIN_DEPENDENCIES)
    1.29 @@ -267,7 +272,6 @@
    1.30    $(SRC)/Provers/Arith/cancel_numerals.ML \
    1.31    $(SRC)/Provers/Arith/combine_numerals.ML \
    1.32    $(SRC)/Provers/Arith/extract_common_term.ML \
    1.33 -  $(SRC)/Tools/Metis/metis.ML \
    1.34    Tools/async_manager.ML \
    1.35    Tools/ATP/atp_problem.ML \
    1.36    Tools/ATP/atp_proof.ML \
    1.37 @@ -317,9 +321,6 @@
    1.38    Tools/recdef.ML \
    1.39    Tools/record.ML \
    1.40    Tools/semiring_normalizer.ML \
    1.41 -  Tools/Sledgehammer/metis_reconstruct.ML \
    1.42 -  Tools/Sledgehammer/metis_translate.ML \
    1.43 -  Tools/Sledgehammer/metis_tactics.ML \
    1.44    Tools/Sledgehammer/sledgehammer.ML \
    1.45    Tools/Sledgehammer/sledgehammer_filter.ML \
    1.46    Tools/Sledgehammer/sledgehammer_minimize.ML \
     2.1 --- a/src/HOL/List.thy	Mon Oct 04 22:01:34 2010 +0200
     2.2 +++ b/src/HOL/List.thy	Mon Oct 04 22:45:09 2010 +0200
     2.3 @@ -5,7 +5,7 @@
     2.4  header {* The datatype of finite lists *}
     2.5  
     2.6  theory List
     2.7 -imports Plain Quotient Presburger Code_Numeral Sledgehammer Recdef
     2.8 +imports Plain Quotient Presburger Code_Numeral Recdef
     2.9  uses ("Tools/list_code.ML")
    2.10  begin
    2.11  
     3.1 --- a/src/HOL/Meson.thy	Mon Oct 04 22:01:34 2010 +0200
     3.2 +++ b/src/HOL/Meson.thy	Mon Oct 04 22:45:09 2010 +0200
     3.3 @@ -8,7 +8,7 @@
     3.4  header {* MESON Proof Procedure (Model Elimination) *}
     3.5  
     3.6  theory Meson
     3.7 -imports Nat
     3.8 +imports Datatype
     3.9  uses ("Tools/Meson/meson.ML")
    3.10       ("Tools/Meson/meson_clausify.ML")
    3.11  begin
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Metis.thy	Mon Oct 04 22:45:09 2010 +0200
     4.3 @@ -0,0 +1,35 @@
     4.4 +(*  Title:      HOL/Metis.thy
     4.5 +    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
     4.6 +    Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
     4.7 +    Author:     Jasmin Blanchette, TU Muenchen
     4.8 +*)
     4.9 +
    4.10 +header {* Metis Proof Method *}
    4.11 +
    4.12 +theory Metis
    4.13 +imports Meson
    4.14 +uses "~~/src/Tools/Metis/metis.ML"
    4.15 +     ("Tools/Metis/metis_translate.ML")
    4.16 +     ("Tools/Metis/metis_reconstruct.ML")
    4.17 +     ("Tools/Metis/metis_tactics.ML")
    4.18 +begin
    4.19 +
    4.20 +definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
    4.21 +"fequal X Y \<longleftrightarrow> (X = Y)"
    4.22 +
    4.23 +lemma fequal_imp_equal [no_atp]: "\<not> fequal X Y \<or> X = Y"
    4.24 +by (simp add: fequal_def)
    4.25 +
    4.26 +lemma equal_imp_fequal [no_atp]: "\<not> X = Y \<or> fequal X Y"
    4.27 +by (simp add: fequal_def)
    4.28 +
    4.29 +lemma equal_imp_equal [no_atp]: "X = Y ==> X = Y"
    4.30 +by auto
    4.31 +
    4.32 +use "Tools/Metis/metis_translate.ML"
    4.33 +use "Tools/Metis/metis_reconstruct.ML"
    4.34 +use "Tools/Metis/metis_tactics.ML"
    4.35 +
    4.36 +setup Metis_Tactics.setup
    4.37 +
    4.38 +end
     5.1 --- a/src/HOL/Plain.thy	Mon Oct 04 22:01:34 2010 +0200
     5.2 +++ b/src/HOL/Plain.thy	Mon Oct 04 22:45:09 2010 +0200
     5.3 @@ -1,7 +1,7 @@
     5.4  header {* Plain HOL *}
     5.5  
     5.6  theory Plain
     5.7 -imports Datatype FunDef Extraction Meson
     5.8 +imports Datatype FunDef Extraction Metis
     5.9  begin
    5.10  
    5.11  text {*
     6.1 --- a/src/HOL/Quotient.thy	Mon Oct 04 22:01:34 2010 +0200
     6.2 +++ b/src/HOL/Quotient.thy	Mon Oct 04 22:45:09 2010 +0200
     6.3 @@ -5,7 +5,7 @@
     6.4  header {* Definition of Quotient Types *}
     6.5  
     6.6  theory Quotient
     6.7 -imports Plain Sledgehammer
     6.8 +imports Plain Hilbert_Choice
     6.9  uses
    6.10    ("Tools/Quotient/quotient_info.ML")
    6.11    ("Tools/Quotient/quotient_typ.ML")
     7.1 --- a/src/HOL/Refute.thy	Mon Oct 04 22:01:34 2010 +0200
     7.2 +++ b/src/HOL/Refute.thy	Mon Oct 04 22:45:09 2010 +0200
     7.3 @@ -8,7 +8,7 @@
     7.4  header {* Refute *}
     7.5  
     7.6  theory Refute
     7.7 -imports Hilbert_Choice List
     7.8 +imports Hilbert_Choice List Sledgehammer
     7.9  uses "Tools/refute.ML"
    7.10  begin
    7.11  
     8.1 --- a/src/HOL/Sledgehammer.thy	Mon Oct 04 22:01:34 2010 +0200
     8.2 +++ b/src/HOL/Sledgehammer.thy	Mon Oct 04 22:45:09 2010 +0200
     8.3 @@ -8,15 +8,11 @@
     8.4  header {* Sledgehammer: Isabelle--ATP Linkup *}
     8.5  
     8.6  theory Sledgehammer
     8.7 -imports Plain Hilbert_Choice
     8.8 +imports Plain
     8.9  uses
    8.10    ("Tools/ATP/atp_problem.ML")
    8.11    ("Tools/ATP/atp_proof.ML")
    8.12    ("Tools/ATP/atp_systems.ML")
    8.13 -  ("~~/src/Tools/Metis/metis.ML")
    8.14 -  ("Tools/Sledgehammer/metis_translate.ML")
    8.15 -  ("Tools/Sledgehammer/metis_reconstruct.ML")
    8.16 -  ("Tools/Sledgehammer/metis_tactics.ML")
    8.17    ("Tools/Sledgehammer/sledgehammer_util.ML")
    8.18    ("Tools/Sledgehammer/sledgehammer_filter.ML")
    8.19    ("Tools/Sledgehammer/sledgehammer_translate.ML")
    8.20 @@ -26,88 +22,11 @@
    8.21    ("Tools/Sledgehammer/sledgehammer_isar.ML")
    8.22  begin
    8.23  
    8.24 -lemma TruepropI: "P \<equiv> Q \<Longrightarrow> Trueprop P \<equiv> Trueprop Q"
    8.25 -by simp
    8.26 -
    8.27 -definition skolem :: "'a \<Rightarrow> 'a" where
    8.28 -[no_atp]: "skolem = (\<lambda>x. x)"
    8.29 -
    8.30 -definition COMBI :: "'a \<Rightarrow> 'a" where
    8.31 -[no_atp]: "COMBI P = P"
    8.32 -
    8.33 -definition COMBK :: "'a \<Rightarrow> 'b \<Rightarrow> 'a" where
    8.34 -[no_atp]: "COMBK P Q = P"
    8.35 -
    8.36 -definition COMBB :: "('b => 'c) \<Rightarrow> ('a => 'b) \<Rightarrow> 'a \<Rightarrow> 'c" where [no_atp]:
    8.37 -"COMBB P Q R = P (Q R)"
    8.38 -
    8.39 -definition COMBC :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
    8.40 -[no_atp]: "COMBC P Q R = P R Q"
    8.41 -
    8.42 -definition COMBS :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" where
    8.43 -[no_atp]: "COMBS P Q R = P R (Q R)"
    8.44 -
    8.45 -definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
    8.46 -"fequal X Y \<longleftrightarrow> (X = Y)"
    8.47 -
    8.48 -lemma fequal_imp_equal [no_atp]: "\<not> fequal X Y \<or> X = Y"
    8.49 -by (simp add: fequal_def)
    8.50 -
    8.51 -lemma equal_imp_fequal [no_atp]: "\<not> X = Y \<or> fequal X Y"
    8.52 -by (simp add: fequal_def)
    8.53 -
    8.54 -lemma equal_imp_equal [no_atp]: "X = Y ==> X = Y"
    8.55 -by auto
    8.56 -
    8.57 -lemma skolem_COMBK_iff: "P \<longleftrightarrow> skolem (COMBK P (i\<Colon>nat))"
    8.58 -unfolding skolem_def COMBK_def by (rule refl)
    8.59 -
    8.60 -lemmas skolem_COMBK_I = iffD1 [OF skolem_COMBK_iff]
    8.61 -lemmas skolem_COMBK_D = iffD2 [OF skolem_COMBK_iff]
    8.62 -
    8.63 -text{*Theorems for translation to combinators*}
    8.64 -
    8.65 -lemma abs_S [no_atp]: "\<lambda>x. (f x) (g x) \<equiv> COMBS f g"
    8.66 -apply (rule eq_reflection)
    8.67 -apply (rule ext) 
    8.68 -apply (simp add: COMBS_def) 
    8.69 -done
    8.70 -
    8.71 -lemma abs_I [no_atp]: "\<lambda>x. x \<equiv> COMBI"
    8.72 -apply (rule eq_reflection)
    8.73 -apply (rule ext) 
    8.74 -apply (simp add: COMBI_def) 
    8.75 -done
    8.76 -
    8.77 -lemma abs_K [no_atp]: "\<lambda>x. y \<equiv> COMBK y"
    8.78 -apply (rule eq_reflection)
    8.79 -apply (rule ext) 
    8.80 -apply (simp add: COMBK_def) 
    8.81 -done
    8.82 -
    8.83 -lemma abs_B [no_atp]: "\<lambda>x. a (g x) \<equiv> COMBB a g"
    8.84 -apply (rule eq_reflection)
    8.85 -apply (rule ext) 
    8.86 -apply (simp add: COMBB_def) 
    8.87 -done
    8.88 -
    8.89 -lemma abs_C [no_atp]: "\<lambda>x. (f x) b \<equiv> COMBC f b"
    8.90 -apply (rule eq_reflection)
    8.91 -apply (rule ext) 
    8.92 -apply (simp add: COMBC_def) 
    8.93 -done
    8.94 -
    8.95  use "Tools/ATP/atp_problem.ML"
    8.96  use "Tools/ATP/atp_proof.ML"
    8.97  use "Tools/ATP/atp_systems.ML"
    8.98  setup ATP_Systems.setup
    8.99  
   8.100 -use "~~/src/Tools/Metis/metis.ML"
   8.101 -use "Tools/Sledgehammer/metis_translate.ML"
   8.102 -use "Tools/Sledgehammer/metis_reconstruct.ML"
   8.103 -use "Tools/Sledgehammer/metis_tactics.ML"
   8.104 -setup Metis_Tactics.setup
   8.105 -
   8.106  use "Tools/Sledgehammer/sledgehammer_util.ML"
   8.107  use "Tools/Sledgehammer/sledgehammer_filter.ML"
   8.108  use "Tools/Sledgehammer/sledgehammer_translate.ML"
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Oct 04 22:45:09 2010 +0200
     9.3 @@ -0,0 +1,557 @@
     9.4 +(*  Title:      HOL/Tools/Sledgehammer/metis_reconstruct.ML
     9.5 +    Author:     Kong W. Susanto, Cambridge University Computer Laboratory
     9.6 +    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
     9.7 +    Author:     Jasmin Blanchette, TU Muenchen
     9.8 +    Copyright   Cambridge University 2007
     9.9 +
    9.10 +Proof reconstruction for Metis.
    9.11 +*)
    9.12 +
    9.13 +signature METIS_RECONSTRUCT =
    9.14 +sig
    9.15 +  type mode = Metis_Translate.mode
    9.16 +
    9.17 +  val trace : bool Unsynchronized.ref
    9.18 +  val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
    9.19 +  val untyped_aconv : term -> term -> bool
    9.20 +  val replay_one_inference :
    9.21 +    Proof.context -> mode -> (string * term) list
    9.22 +    -> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list
    9.23 +    -> (Metis_Thm.thm * thm) list
    9.24 +end;
    9.25 +
    9.26 +structure Metis_Reconstruct : METIS_RECONSTRUCT =
    9.27 +struct
    9.28 +
    9.29 +open Metis_Translate
    9.30 +
    9.31 +val trace = Unsynchronized.ref false
    9.32 +fun trace_msg msg = if !trace then tracing (msg ()) else ()
    9.33 +
    9.34 +datatype term_or_type = SomeTerm of term | SomeType of typ
    9.35 +
    9.36 +fun terms_of [] = []
    9.37 +  | terms_of (SomeTerm t :: tts) = t :: terms_of tts
    9.38 +  | terms_of (SomeType _ :: tts) = terms_of tts;
    9.39 +
    9.40 +fun types_of [] = []
    9.41 +  | types_of (SomeTerm (Var ((a,idx), _)) :: tts) =
    9.42 +      if String.isPrefix "_" a then
    9.43 +          (*Variable generated by Metis, which might have been a type variable.*)
    9.44 +          TVar (("'" ^ a, idx), HOLogic.typeS) :: types_of tts
    9.45 +      else types_of tts
    9.46 +  | types_of (SomeTerm _ :: tts) = types_of tts
    9.47 +  | types_of (SomeType T :: tts) = T :: types_of tts;
    9.48 +
    9.49 +fun apply_list rator nargs rands =
    9.50 +  let val trands = terms_of rands
    9.51 +  in  if length trands = nargs then SomeTerm (list_comb(rator, trands))
    9.52 +      else raise Fail
    9.53 +        ("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global Pure.thy rator ^
    9.54 +          " expected " ^ Int.toString nargs ^
    9.55 +          " received " ^ commas (map (Syntax.string_of_term_global Pure.thy) trands))
    9.56 +  end;
    9.57 +
    9.58 +fun infer_types ctxt =
    9.59 +  Syntax.check_terms (ProofContext.set_mode ProofContext.mode_pattern ctxt);
    9.60 +
    9.61 +(*We use 1 rather than 0 because variable references in clauses may otherwise conflict
    9.62 +  with variable constraints in the goal...at least, type inference often fails otherwise.
    9.63 +  SEE ALSO axiom_inf below.*)
    9.64 +fun mk_var (w, T) = Var ((w, 1), T)
    9.65 +
    9.66 +(*include the default sort, if available*)
    9.67 +fun mk_tfree ctxt w =
    9.68 +  let val ww = "'" ^ w
    9.69 +  in  TFree(ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1)))  end;
    9.70 +
    9.71 +(*Remove the "apply" operator from an HO term*)
    9.72 +fun strip_happ args (Metis_Term.Fn(".",[t,u])) = strip_happ (u::args) t
    9.73 +  | strip_happ args x = (x, args);
    9.74 +
    9.75 +fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS)
    9.76 +
    9.77 +fun smart_invert_const "fequal" = @{const_name HOL.eq}
    9.78 +  | smart_invert_const s = invert_const s
    9.79 +
    9.80 +fun hol_type_from_metis_term _ (Metis_Term.Var v) =
    9.81 +     (case strip_prefix_and_unascii tvar_prefix v of
    9.82 +          SOME w => make_tvar w
    9.83 +        | NONE   => make_tvar v)
    9.84 +  | hol_type_from_metis_term ctxt (Metis_Term.Fn(x, tys)) =
    9.85 +     (case strip_prefix_and_unascii type_const_prefix x of
    9.86 +          SOME tc => Type (smart_invert_const tc,
    9.87 +                           map (hol_type_from_metis_term ctxt) tys)
    9.88 +        | NONE    =>
    9.89 +      case strip_prefix_and_unascii tfree_prefix x of
    9.90 +          SOME tf => mk_tfree ctxt tf
    9.91 +        | NONE    => raise Fail ("hol_type_from_metis_term: " ^ x));
    9.92 +
    9.93 +(*Maps metis terms to isabelle terms*)
    9.94 +fun hol_term_from_metis_PT ctxt fol_tm =
    9.95 +  let val thy = ProofContext.theory_of ctxt
    9.96 +      val _ = trace_msg (fn () => "hol_term_from_metis_PT: " ^
    9.97 +                                  Metis_Term.toString fol_tm)
    9.98 +      fun tm_to_tt (Metis_Term.Var v) =
    9.99 +             (case strip_prefix_and_unascii tvar_prefix v of
   9.100 +                  SOME w => SomeType (make_tvar w)
   9.101 +                | NONE =>
   9.102 +              case strip_prefix_and_unascii schematic_var_prefix v of
   9.103 +                  SOME w => SomeTerm (mk_var (w, HOLogic.typeT))
   9.104 +                | NONE   => SomeTerm (mk_var (v, HOLogic.typeT)) )
   9.105 +                    (*Var from Metis with a name like _nnn; possibly a type variable*)
   9.106 +        | tm_to_tt (Metis_Term.Fn ("{}", [arg])) = tm_to_tt arg   (*hBOOL*)
   9.107 +        | tm_to_tt (t as Metis_Term.Fn (".",_)) =
   9.108 +            let val (rator,rands) = strip_happ [] t
   9.109 +            in  case rator of
   9.110 +                    Metis_Term.Fn(fname,ts) => applic_to_tt (fname, ts @ rands)
   9.111 +                  | _ => case tm_to_tt rator of
   9.112 +                             SomeTerm t => SomeTerm (list_comb(t, terms_of (map tm_to_tt rands)))
   9.113 +                           | _ => raise Fail "tm_to_tt: HO application"
   9.114 +            end
   9.115 +        | tm_to_tt (Metis_Term.Fn (fname, args)) = applic_to_tt (fname,args)
   9.116 +      and applic_to_tt ("=",ts) =
   9.117 +            SomeTerm (list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
   9.118 +        | applic_to_tt (a,ts) =
   9.119 +            case strip_prefix_and_unascii const_prefix a of
   9.120 +                SOME b =>
   9.121 +                  let
   9.122 +                    val c = smart_invert_const b
   9.123 +                    val ntypes = num_type_args thy c
   9.124 +                    val nterms = length ts - ntypes
   9.125 +                    val tts = map tm_to_tt ts
   9.126 +                    val tys = types_of (List.take(tts,ntypes))
   9.127 +                    val t =
   9.128 +                      if String.isPrefix new_skolem_const_prefix c then
   9.129 +                        Var (new_skolem_var_from_const c,
   9.130 +                             Type_Infer.paramify_vars (tl tys ---> hd tys))
   9.131 +                      else
   9.132 +                        Const (c, dummyT)
   9.133 +                  in if length tys = ntypes then
   9.134 +                         apply_list t nterms (List.drop(tts,ntypes))
   9.135 +                     else
   9.136 +                       raise Fail ("Constant " ^ c ^ " expects " ^ Int.toString ntypes ^
   9.137 +                                   " but gets " ^ Int.toString (length tys) ^
   9.138 +                                   " type arguments\n" ^
   9.139 +                                   cat_lines (map (Syntax.string_of_typ ctxt) tys) ^
   9.140 +                                   " the terms are \n" ^
   9.141 +                                   cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
   9.142 +                     end
   9.143 +              | NONE => (*Not a constant. Is it a type constructor?*)
   9.144 +            case strip_prefix_and_unascii type_const_prefix a of
   9.145 +                SOME b =>
   9.146 +                SomeType (Type (smart_invert_const b, types_of (map tm_to_tt ts)))
   9.147 +              | NONE => (*Maybe a TFree. Should then check that ts=[].*)
   9.148 +            case strip_prefix_and_unascii tfree_prefix a of
   9.149 +                SOME b => SomeType (mk_tfree ctxt b)
   9.150 +              | NONE => (*a fixed variable? They are Skolem functions.*)
   9.151 +            case strip_prefix_and_unascii fixed_var_prefix a of
   9.152 +                SOME b =>
   9.153 +                  let val opr = Free (b, HOLogic.typeT)
   9.154 +                  in  apply_list opr (length ts) (map tm_to_tt ts)  end
   9.155 +              | NONE => raise Fail ("unexpected metis function: " ^ a)
   9.156 +  in
   9.157 +    case tm_to_tt fol_tm of
   9.158 +      SomeTerm t => t
   9.159 +    | SomeType T => raise TYPE ("fol_tm_to_tt: Term expected", [T], [])
   9.160 +  end
   9.161 +
   9.162 +(*Maps fully-typed metis terms to isabelle terms*)
   9.163 +fun hol_term_from_metis_FT ctxt fol_tm =
   9.164 +  let val _ = trace_msg (fn () => "hol_term_from_metis_FT: " ^
   9.165 +                                  Metis_Term.toString fol_tm)
   9.166 +      fun cvt (Metis_Term.Fn ("ti", [Metis_Term.Var v, _])) =
   9.167 +             (case strip_prefix_and_unascii schematic_var_prefix v of
   9.168 +                  SOME w =>  mk_var(w, dummyT)
   9.169 +                | NONE   => mk_var(v, dummyT))
   9.170 +        | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn ("=",[]), _])) =
   9.171 +            Const (@{const_name HOL.eq}, HOLogic.typeT)
   9.172 +        | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn (x,[]), ty])) =
   9.173 +           (case strip_prefix_and_unascii const_prefix x of
   9.174 +                SOME c => Const (smart_invert_const c, dummyT)
   9.175 +              | NONE => (*Not a constant. Is it a fixed variable??*)
   9.176 +            case strip_prefix_and_unascii fixed_var_prefix x of
   9.177 +                SOME v => Free (v, hol_type_from_metis_term ctxt ty)
   9.178 +              | NONE => raise Fail ("hol_term_from_metis_FT bad constant: " ^ x))
   9.179 +        | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn (".",[tm1,tm2]), _])) =
   9.180 +            cvt tm1 $ cvt tm2
   9.181 +        | cvt (Metis_Term.Fn (".",[tm1,tm2])) = (*untyped application*)
   9.182 +            cvt tm1 $ cvt tm2
   9.183 +        | cvt (Metis_Term.Fn ("{}", [arg])) = cvt arg   (*hBOOL*)
   9.184 +        | cvt (Metis_Term.Fn ("=", [tm1,tm2])) =
   9.185 +            list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), map cvt [tm1,tm2])
   9.186 +        | cvt (t as Metis_Term.Fn (x, [])) =
   9.187 +           (case strip_prefix_and_unascii const_prefix x of
   9.188 +                SOME c => Const (smart_invert_const c, dummyT)
   9.189 +              | NONE => (*Not a constant. Is it a fixed variable??*)
   9.190 +            case strip_prefix_and_unascii fixed_var_prefix x of
   9.191 +                SOME v => Free (v, dummyT)
   9.192 +              | NONE => (trace_msg (fn () => "hol_term_from_metis_FT bad const: " ^ x);
   9.193 +                  hol_term_from_metis_PT ctxt t))
   9.194 +        | cvt t = (trace_msg (fn () => "hol_term_from_metis_FT bad term: " ^ Metis_Term.toString t);
   9.195 +            hol_term_from_metis_PT ctxt t)
   9.196 +  in fol_tm |> cvt end
   9.197 +
   9.198 +fun hol_term_from_metis FT = hol_term_from_metis_FT
   9.199 +  | hol_term_from_metis _ = hol_term_from_metis_PT
   9.200 +
   9.201 +fun hol_terms_from_fol ctxt mode old_skolems fol_tms =
   9.202 +  let val ts = map (hol_term_from_metis mode ctxt) fol_tms
   9.203 +      val _ = trace_msg (fn () => "  calling type inference:")
   9.204 +      val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts
   9.205 +      val ts' = ts |> map (reveal_old_skolem_terms old_skolems)
   9.206 +                   |> infer_types ctxt
   9.207 +      val _ = app (fn t => trace_msg
   9.208 +                    (fn () => "  final term: " ^ Syntax.string_of_term ctxt t ^
   9.209 +                              "  of type  " ^ Syntax.string_of_typ ctxt (type_of t)))
   9.210 +                  ts'
   9.211 +  in  ts'  end;
   9.212 +
   9.213 +(* ------------------------------------------------------------------------- *)
   9.214 +(* FOL step Inference Rules                                                  *)
   9.215 +(* ------------------------------------------------------------------------- *)
   9.216 +
   9.217 +(*for debugging only*)
   9.218 +(*
   9.219 +fun print_thpair (fth,th) =
   9.220 +  (trace_msg (fn () => "=============================================");
   9.221 +   trace_msg (fn () => "Metis: " ^ Metis_Thm.toString fth);
   9.222 +   trace_msg (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th));
   9.223 +*)
   9.224 +
   9.225 +fun lookth thpairs (fth : Metis_Thm.thm) =
   9.226 +  the (AList.lookup (uncurry Metis_Thm.equal) thpairs fth)
   9.227 +  handle Option.Option =>
   9.228 +         raise Fail ("Failed to find Metis theorem " ^ Metis_Thm.toString fth)
   9.229 +
   9.230 +fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx));
   9.231 +
   9.232 +(* INFERENCE RULE: AXIOM *)
   9.233 +
   9.234 +fun axiom_inf thpairs th = Thm.incr_indexes 1 (lookth thpairs th);
   9.235 +    (*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*)
   9.236 +
   9.237 +(* INFERENCE RULE: ASSUME *)
   9.238 +
   9.239 +val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)}
   9.240 +
   9.241 +fun inst_excluded_middle thy i_atm =
   9.242 +  let val th = EXCLUDED_MIDDLE
   9.243 +      val [vx] = Term.add_vars (prop_of th) []
   9.244 +      val substs = [(cterm_of thy (Var vx), cterm_of thy i_atm)]
   9.245 +  in  cterm_instantiate substs th  end;
   9.246 +
   9.247 +fun assume_inf ctxt mode old_skolems atm =
   9.248 +  inst_excluded_middle
   9.249 +      (ProofContext.theory_of ctxt)
   9.250 +      (singleton (hol_terms_from_fol ctxt mode old_skolems) (Metis_Term.Fn atm))
   9.251 +
   9.252 +(* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying
   9.253 +   to reconstruct them admits new possibilities of errors, e.g. concerning
   9.254 +   sorts. Instead we try to arrange that new TVars are distinct and that types
   9.255 +   can be inferred from terms. *)
   9.256 +
   9.257 +fun inst_inf ctxt mode old_skolems thpairs fsubst th =
   9.258 +  let val thy = ProofContext.theory_of ctxt
   9.259 +      val i_th = lookth thpairs th
   9.260 +      val i_th_vars = Term.add_vars (prop_of i_th) []
   9.261 +      fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars)
   9.262 +      fun subst_translation (x,y) =
   9.263 +        let val v = find_var x
   9.264 +            (* We call "reveal_old_skolem_terms" and "infer_types" below. *)
   9.265 +            val t = hol_term_from_metis mode ctxt y
   9.266 +        in  SOME (cterm_of thy (Var v), t)  end
   9.267 +        handle Option.Option =>
   9.268 +               (trace_msg (fn () => "\"find_var\" failed for " ^ x ^
   9.269 +                                    " in " ^ Display.string_of_thm ctxt i_th);
   9.270 +                NONE)
   9.271 +             | TYPE _ =>
   9.272 +               (trace_msg (fn () => "\"hol_term_from_metis\" failed for " ^ x ^
   9.273 +                                    " in " ^ Display.string_of_thm ctxt i_th);
   9.274 +                NONE)
   9.275 +      fun remove_typeinst (a, t) =
   9.276 +            case strip_prefix_and_unascii schematic_var_prefix a of
   9.277 +                SOME b => SOME (b, t)
   9.278 +              | NONE => case strip_prefix_and_unascii tvar_prefix a of
   9.279 +                SOME _ => NONE          (*type instantiations are forbidden!*)
   9.280 +              | NONE => SOME (a,t)    (*internal Metis var?*)
   9.281 +      val _ = trace_msg (fn () => "  isa th: " ^ Display.string_of_thm ctxt i_th)
   9.282 +      val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst)
   9.283 +      val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs)
   9.284 +      val tms = rawtms |> map (reveal_old_skolem_terms old_skolems)
   9.285 +                       |> infer_types ctxt
   9.286 +      val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
   9.287 +      val substs' = ListPair.zip (vars, map ctm_of tms)
   9.288 +      val _ = trace_msg (fn () =>
   9.289 +        cat_lines ("subst_translations:" ::
   9.290 +          (substs' |> map (fn (x, y) =>
   9.291 +            Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
   9.292 +            Syntax.string_of_term ctxt (term_of y)))));
   9.293 +  in cterm_instantiate substs' i_th end
   9.294 +  handle THM (msg, _, _) =>
   9.295 +         error ("Cannot replay Metis proof in Isabelle:\n" ^ msg)
   9.296 +
   9.297 +(* INFERENCE RULE: RESOLVE *)
   9.298 +
   9.299 +(* Like RSN, but we rename apart only the type variables. Vars here typically
   9.300 +   have an index of 1, and the use of RSN would increase this typically to 3.
   9.301 +   Instantiations of those Vars could then fail. See comment on "mk_var". *)
   9.302 +fun resolve_inc_tyvars thy tha i thb =
   9.303 +  let
   9.304 +    val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
   9.305 +    fun aux tha thb =
   9.306 +      case Thm.bicompose false (false, tha, nprems_of tha) i thb
   9.307 +           |> Seq.list_of |> distinct Thm.eq_thm of
   9.308 +        [th] => th
   9.309 +      | _ => raise THM ("resolve_inc_tyvars: unique result expected", i,
   9.310 +                        [tha, thb])
   9.311 +  in
   9.312 +    aux tha thb
   9.313 +    handle TERM z =>
   9.314 +           (* The unifier, which is invoked from "Thm.bicompose", will sometimes
   9.315 +              refuse to unify "?a::?'a" with "?a::?'b" or "?a::nat" and throw a
   9.316 +              "TERM" exception (with "add_ffpair" as first argument). We then
   9.317 +              perform unification of the types of variables by hand and try
   9.318 +              again. We could do this the first time around but this error
   9.319 +              occurs seldom and we don't want to break existing proofs in subtle
   9.320 +              ways or slow them down needlessly. *)
   9.321 +           case [] |> fold (Term.add_vars o prop_of) [tha, thb]
   9.322 +                   |> AList.group (op =)
   9.323 +                   |> maps (fn ((s, _), T :: Ts) =>
   9.324 +                               map (fn T' => (Free (s, T), Free (s, T'))) Ts)
   9.325 +                   |> rpair (Envir.empty ~1)
   9.326 +                   |-> fold (Pattern.unify thy)
   9.327 +                   |> Envir.type_env |> Vartab.dest
   9.328 +                   |> map (fn (x, (S, T)) =>
   9.329 +                              pairself (ctyp_of thy) (TVar (x, S), T)) of
   9.330 +             [] => raise TERM z
   9.331 +           | ps => aux (instantiate (ps, []) tha) (instantiate (ps, []) thb)
   9.332 +  end
   9.333 +
   9.334 +fun mk_not (Const (@{const_name Not}, _) $ b) = b
   9.335 +  | mk_not b = HOLogic.mk_not b
   9.336 +
   9.337 +(* Match untyped terms. *)
   9.338 +fun untyped_aconv (Const (a, _)) (Const(b, _)) = (a = b)
   9.339 +  | untyped_aconv (Free (a, _)) (Free (b, _)) = (a = b)
   9.340 +  | untyped_aconv (Var ((a, _), _)) (Var ((b, _), _)) =
   9.341 +    (a = b) (* The index is ignored, for some reason. *)
   9.342 +  | untyped_aconv (Bound i) (Bound j) = (i = j)
   9.343 +  | untyped_aconv (Abs (_, _, t)) (Abs (_, _, u)) = untyped_aconv t u
   9.344 +  | untyped_aconv (t1 $ t2) (u1 $ u2) =
   9.345 +    untyped_aconv t1 u1 andalso untyped_aconv t2 u2
   9.346 +  | untyped_aconv _ _ = false
   9.347 +
   9.348 +(* Finding the relative location of an untyped term within a list of terms *)
   9.349 +fun literal_index lit =
   9.350 +  let
   9.351 +    val lit = Envir.eta_contract lit
   9.352 +    fun get _ [] = raise Empty
   9.353 +      | get n (x :: xs) =
   9.354 +        if untyped_aconv lit (Envir.eta_contract (HOLogic.dest_Trueprop x)) then
   9.355 +          n
   9.356 +        else
   9.357 +          get (n+1) xs
   9.358 +  in get 1 end
   9.359 +
   9.360 +(* Permute a rule's premises to move the i-th premise to the last position. *)
   9.361 +fun make_last i th =
   9.362 +  let val n = nprems_of th
   9.363 +  in  if 1 <= i andalso i <= n
   9.364 +      then Thm.permute_prems (i-1) 1 th
   9.365 +      else raise THM("select_literal", i, [th])
   9.366 +  end;
   9.367 +
   9.368 +(* Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing
   9.369 +   double-negations. *)
   9.370 +val negate_head = rewrite_rule [@{thm atomize_not}, not_not RS eq_reflection]
   9.371 +
   9.372 +(* Maps the clause  [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *)
   9.373 +val select_literal = negate_head oo make_last
   9.374 +
   9.375 +fun resolve_inf ctxt mode old_skolems thpairs atm th1 th2 =
   9.376 +  let
   9.377 +    val thy = ProofContext.theory_of ctxt
   9.378 +    val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
   9.379 +    val _ = trace_msg (fn () => "  isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
   9.380 +    val _ = trace_msg (fn () => "  isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
   9.381 +  in
   9.382 +    (* Trivial cases where one operand is type info *)
   9.383 +    if Thm.eq_thm (TrueI, i_th1) then
   9.384 +      i_th2
   9.385 +    else if Thm.eq_thm (TrueI, i_th2) then
   9.386 +      i_th1
   9.387 +    else
   9.388 +      let
   9.389 +        val i_atm = singleton (hol_terms_from_fol ctxt mode old_skolems)
   9.390 +                              (Metis_Term.Fn atm)
   9.391 +        val _ = trace_msg (fn () => "  atom: " ^ Syntax.string_of_term ctxt i_atm)
   9.392 +        val prems_th1 = prems_of i_th1
   9.393 +        val prems_th2 = prems_of i_th2
   9.394 +        val index_th1 = literal_index (mk_not i_atm) prems_th1
   9.395 +              handle Empty => raise Fail "Failed to find literal in th1"
   9.396 +        val _ = trace_msg (fn () => "  index_th1: " ^ Int.toString index_th1)
   9.397 +        val index_th2 = literal_index i_atm prems_th2
   9.398 +              handle Empty => raise Fail "Failed to find literal in th2"
   9.399 +        val _ = trace_msg (fn () => "  index_th2: " ^ Int.toString index_th2)
   9.400 +    in
   9.401 +      resolve_inc_tyvars thy (select_literal index_th1 i_th1) index_th2 i_th2
   9.402 +    end
   9.403 +  end;
   9.404 +
   9.405 +(* INFERENCE RULE: REFL *)
   9.406 +
   9.407 +val REFL_THM = Thm.incr_indexes 2 @{lemma "t ~= t ==> False" by simp}
   9.408 +
   9.409 +val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
   9.410 +val refl_idx = 1 + Thm.maxidx_of REFL_THM;
   9.411 +
   9.412 +fun refl_inf ctxt mode old_skolems t =
   9.413 +  let val thy = ProofContext.theory_of ctxt
   9.414 +      val i_t = singleton (hol_terms_from_fol ctxt mode old_skolems) t
   9.415 +      val _ = trace_msg (fn () => "  term: " ^ Syntax.string_of_term ctxt i_t)
   9.416 +      val c_t = cterm_incr_types thy refl_idx i_t
   9.417 +  in  cterm_instantiate [(refl_x, c_t)] REFL_THM  end;
   9.418 +
   9.419 +(* INFERENCE RULE: EQUALITY *)
   9.420 +
   9.421 +val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp}
   9.422 +val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp}
   9.423 +
   9.424 +val metis_eq = Metis_Term.Fn ("=", []);
   9.425 +
   9.426 +fun get_ty_arg_size _ (Const (@{const_name HOL.eq}, _)) = 0  (*equality has no type arguments*)
   9.427 +  | get_ty_arg_size thy (Const (c, _)) = (num_type_args thy c handle TYPE _ => 0)
   9.428 +  | get_ty_arg_size _ _ = 0;
   9.429 +
   9.430 +fun equality_inf ctxt mode old_skolems (pos, atm) fp fr =
   9.431 +  let val thy = ProofContext.theory_of ctxt
   9.432 +      val m_tm = Metis_Term.Fn atm
   9.433 +      val [i_atm,i_tm] = hol_terms_from_fol ctxt mode old_skolems [m_tm, fr]
   9.434 +      val _ = trace_msg (fn () => "sign of the literal: " ^ Bool.toString pos)
   9.435 +      fun replace_item_list lx 0 (_::ls) = lx::ls
   9.436 +        | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
   9.437 +      fun path_finder_FO tm [] = (tm, Bound 0)
   9.438 +        | path_finder_FO tm (p::ps) =
   9.439 +            let val (tm1,args) = strip_comb tm
   9.440 +                val adjustment = get_ty_arg_size thy tm1
   9.441 +                val p' = if adjustment > p then p else p-adjustment
   9.442 +                val tm_p = List.nth(args,p')
   9.443 +                  handle Subscript =>
   9.444 +                         error ("Cannot replay Metis proof in Isabelle:\n" ^
   9.445 +                                "equality_inf: " ^ Int.toString p ^ " adj " ^
   9.446 +                                Int.toString adjustment ^ " term " ^
   9.447 +                                Syntax.string_of_term ctxt tm)
   9.448 +                val _ = trace_msg (fn () => "path_finder: " ^ Int.toString p ^
   9.449 +                                      "  " ^ Syntax.string_of_term ctxt tm_p)
   9.450 +                val (r,t) = path_finder_FO tm_p ps
   9.451 +            in
   9.452 +                (r, list_comb (tm1, replace_item_list t p' args))
   9.453 +            end
   9.454 +      fun path_finder_HO tm [] = (tm, Bound 0)
   9.455 +        | path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps)
   9.456 +        | path_finder_HO (t$u) (_::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps)
   9.457 +        | path_finder_HO tm ps =
   9.458 +          raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^
   9.459 +                      "equality_inf, path_finder_HO: path = " ^
   9.460 +                      space_implode " " (map Int.toString ps) ^
   9.461 +                      " isa-term: " ^  Syntax.string_of_term ctxt tm)
   9.462 +      fun path_finder_FT tm [] _ = (tm, Bound 0)
   9.463 +        | path_finder_FT tm (0::ps) (Metis_Term.Fn ("ti", [t1, _])) =
   9.464 +            path_finder_FT tm ps t1
   9.465 +        | path_finder_FT (t$u) (0::ps) (Metis_Term.Fn (".", [t1, _])) =
   9.466 +            (fn(x,y) => (x, y$u)) (path_finder_FT t ps t1)
   9.467 +        | path_finder_FT (t$u) (1::ps) (Metis_Term.Fn (".", [_, t2])) =
   9.468 +            (fn(x,y) => (x, t$y)) (path_finder_FT u ps t2)
   9.469 +        | path_finder_FT tm ps t =
   9.470 +          raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^
   9.471 +                      "equality_inf, path_finder_FT: path = " ^
   9.472 +                      space_implode " " (map Int.toString ps) ^
   9.473 +                      " isa-term: " ^  Syntax.string_of_term ctxt tm ^
   9.474 +                      " fol-term: " ^ Metis_Term.toString t)
   9.475 +      fun path_finder FO tm ps _ = path_finder_FO tm ps
   9.476 +        | path_finder HO (tm as Const(@{const_name HOL.eq},_) $ _ $ _) (p::ps) _ =
   9.477 +             (*equality: not curried, as other predicates are*)
   9.478 +             if p=0 then path_finder_HO tm (0::1::ps)  (*select first operand*)
   9.479 +             else path_finder_HO tm (p::ps)        (*1 selects second operand*)
   9.480 +        | path_finder HO tm (_ :: ps) (Metis_Term.Fn ("{}", [_])) =
   9.481 +             path_finder_HO tm ps      (*if not equality, ignore head to skip hBOOL*)
   9.482 +        | path_finder FT (tm as Const(@{const_name HOL.eq}, _) $ _ $ _) (p::ps)
   9.483 +                            (Metis_Term.Fn ("=", [t1,t2])) =
   9.484 +             (*equality: not curried, as other predicates are*)
   9.485 +             if p=0 then path_finder_FT tm (0::1::ps)
   9.486 +                          (Metis_Term.Fn (".", [Metis_Term.Fn (".", [metis_eq,t1]), t2]))
   9.487 +                          (*select first operand*)
   9.488 +             else path_finder_FT tm (p::ps)
   9.489 +                   (Metis_Term.Fn (".", [metis_eq,t2]))
   9.490 +                   (*1 selects second operand*)
   9.491 +        | path_finder FT tm (_ :: ps) (Metis_Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1
   9.492 +             (*if not equality, ignore head to skip the hBOOL predicate*)
   9.493 +        | path_finder FT tm ps t = path_finder_FT tm ps t  (*really an error case!*)
   9.494 +      fun path_finder_lit ((nt as Const (@{const_name Not}, _)) $ tm_a) idx =
   9.495 +            let val (tm, tm_rslt) = path_finder mode tm_a idx m_tm
   9.496 +            in (tm, nt $ tm_rslt) end
   9.497 +        | path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm
   9.498 +      val (tm_subst, body) = path_finder_lit i_atm fp
   9.499 +      val tm_abs = Abs ("x", type_of tm_subst, body)
   9.500 +      val _ = trace_msg (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
   9.501 +      val _ = trace_msg (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
   9.502 +      val _ = trace_msg (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
   9.503 +      val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst)  (*ill typed but gives right max*)
   9.504 +      val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
   9.505 +      val _ = trace_msg (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
   9.506 +      val eq_terms = map (pairself (cterm_of thy))
   9.507 +        (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
   9.508 +  in  cterm_instantiate eq_terms subst'  end;
   9.509 +
   9.510 +val factor = Seq.hd o distinct_subgoals_tac;
   9.511 +
   9.512 +fun step ctxt mode old_skolems thpairs p =
   9.513 +  case p of
   9.514 +    (fol_th, Metis_Proof.Axiom _) => factor (axiom_inf thpairs fol_th)
   9.515 +  | (_, Metis_Proof.Assume f_atm) => assume_inf ctxt mode old_skolems f_atm
   9.516 +  | (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) =>
   9.517 +    factor (inst_inf ctxt mode old_skolems thpairs f_subst f_th1)
   9.518 +  | (_, Metis_Proof.Resolve(f_atm, f_th1, f_th2)) =>
   9.519 +    factor (resolve_inf ctxt mode old_skolems thpairs f_atm f_th1 f_th2)
   9.520 +  | (_, Metis_Proof.Refl f_tm) => refl_inf ctxt mode old_skolems f_tm
   9.521 +  | (_, Metis_Proof.Equality (f_lit, f_p, f_r)) =>
   9.522 +    equality_inf ctxt mode old_skolems f_lit f_p f_r
   9.523 +
   9.524 +fun flexflex_first_order th =
   9.525 +  case Thm.tpairs_of th of
   9.526 +      [] => th
   9.527 +    | pairs =>
   9.528 +        let val thy = theory_of_thm th
   9.529 +            val (_, tenv) =
   9.530 +              fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
   9.531 +            val t_pairs = map Meson.term_pair_of (Vartab.dest tenv)
   9.532 +            val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th
   9.533 +        in  th'  end
   9.534 +        handle THM _ => th;
   9.535 +
   9.536 +fun is_metis_literal_genuine (_, (s, _)) = not (String.isPrefix class_prefix s)
   9.537 +fun is_isabelle_literal_genuine t =
   9.538 +  case t of _ $ (Const (@{const_name skolem}, _) $ _) => false | _ => true
   9.539 +
   9.540 +fun count p xs = fold (fn x => if p x then Integer.add 1 else I) xs 0
   9.541 +
   9.542 +fun replay_one_inference ctxt mode old_skolems (fol_th, inf) thpairs =
   9.543 +  let
   9.544 +    val _ = trace_msg (fn () => "=============================================")
   9.545 +    val _ = trace_msg (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)
   9.546 +    val _ = trace_msg (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)
   9.547 +    val th = step ctxt mode old_skolems thpairs (fol_th, inf)
   9.548 +             |> flexflex_first_order
   9.549 +    val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
   9.550 +    val _ = trace_msg (fn () => "=============================================")
   9.551 +    val num_metis_lits =
   9.552 +      fol_th |> Metis_Thm.clause |> Metis_LiteralSet.toList
   9.553 +             |> count is_metis_literal_genuine
   9.554 +    val num_isabelle_lits =
   9.555 +      th |> prems_of |> count is_isabelle_literal_genuine
   9.556 +    val _ = if num_metis_lits = num_isabelle_lits then ()
   9.557 +            else error "Cannot replay Metis proof in Isabelle: Out of sync."
   9.558 +  in (fol_th, th) :: thpairs end
   9.559 +
   9.560 +end;
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/Tools/Metis/metis_tactics.ML	Mon Oct 04 22:45:09 2010 +0200
    10.3 @@ -0,0 +1,449 @@
    10.4 +(*  Title:      HOL/Tools/Sledgehammer/metis_tactics.ML
    10.5 +    Author:     Kong W. Susanto, Cambridge University Computer Laboratory
    10.6 +    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
    10.7 +    Author:     Jasmin Blanchette, TU Muenchen
    10.8 +    Copyright   Cambridge University 2007
    10.9 +
   10.10 +HOL setup for the Metis prover.
   10.11 +*)
   10.12 +
   10.13 +signature METIS_TACTICS =
   10.14 +sig
   10.15 +  val trace : bool Unsynchronized.ref
   10.16 +  val type_lits : bool Config.T
   10.17 +  val new_skolemizer : bool Config.T
   10.18 +  val metis_tac : Proof.context -> thm list -> int -> tactic
   10.19 +  val metisF_tac : Proof.context -> thm list -> int -> tactic
   10.20 +  val metisFT_tac : Proof.context -> thm list -> int -> tactic
   10.21 +  val setup : theory -> theory
   10.22 +end
   10.23 +
   10.24 +structure Metis_Tactics : METIS_TACTICS =
   10.25 +struct
   10.26 +
   10.27 +open Metis_Translate
   10.28 +open Metis_Reconstruct
   10.29 +
   10.30 +structure Int_Pair_Graph =
   10.31 +  Graph(type key = int * int val ord = prod_ord int_ord int_ord)
   10.32 +
   10.33 +fun trace_msg msg = if !trace then tracing (msg ()) else ()
   10.34 +
   10.35 +val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" (K true)
   10.36 +val (new_skolemizer, new_skolemizer_setup) =
   10.37 +  Attrib.config_bool "metis_new_skolemizer" (K false)
   10.38 +
   10.39 +fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const);
   10.40 +
   10.41 +fun have_common_thm ths1 ths2 =
   10.42 +  exists (member Thm.eq_thm ths1) (map Meson.make_meta_clause ths2)
   10.43 +
   10.44 +(*Determining which axiom clauses are actually used*)
   10.45 +fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th)
   10.46 +  | used_axioms _ _ = NONE;
   10.47 +
   10.48 +val clause_params =
   10.49 +  {ordering = Metis_KnuthBendixOrder.default,
   10.50 +   orderLiterals = Metis_Clause.UnsignedLiteralOrder,
   10.51 +   orderTerms = true}
   10.52 +val active_params =
   10.53 +  {clause = clause_params,
   10.54 +   prefactor = #prefactor Metis_Active.default,
   10.55 +   postfactor = #postfactor Metis_Active.default}
   10.56 +val waiting_params =
   10.57 +  {symbolsWeight = 1.0,
   10.58 +   variablesWeight = 0.0,
   10.59 +   literalsWeight = 0.0,
   10.60 +   models = []}
   10.61 +val resolution_params = {active = active_params, waiting = waiting_params}
   10.62 +
   10.63 +fun instantiate_theorem thy inst th =
   10.64 +  let
   10.65 +    val tyenv = Vartab.empty |> fold (Type.raw_unify o pairself fastype_of) inst
   10.66 +    val instT =
   10.67 +      [] |> Vartab.fold (fn (z, (S, T)) =>
   10.68 +                            cons (TVar (z, S), Type.devar tyenv T)) tyenv
   10.69 +    val inst = inst |> map (pairself (subst_atomic_types instT))
   10.70 +    val _ = tracing (cat_lines (map (fn (T, U) =>
   10.71 +        Syntax.string_of_typ @{context} T ^ " |-> " ^
   10.72 +        Syntax.string_of_typ @{context} U) instT))
   10.73 +    val _ = tracing (cat_lines (map (fn (t, u) =>
   10.74 +        Syntax.string_of_term @{context} t ^ " |-> " ^
   10.75 +        Syntax.string_of_term @{context} u) inst))
   10.76 +    val cinstT = instT |> map (pairself (ctyp_of thy))
   10.77 +    val cinst = inst |> map (pairself (cterm_of thy))
   10.78 +  in th |> Thm.instantiate (cinstT, cinst) end
   10.79 +
   10.80 +(* In principle, it should be sufficient to apply "assume_tac" to unify the
   10.81 +   conclusion with one of the premises. However, in practice, this is unreliable
   10.82 +   because of the mildly higher-order nature of the unification problems.
   10.83 +   Typical constraints are of the form
   10.84 +   "?SK_a_b_c_x SK_d_e_f_y ... SK_a_b_c_x ... SK_g_h_i_z =?= SK_a_b_c_x",
   10.85 +   where the nonvariables are goal parameters. *)
   10.86 +fun unify_first_prem_with_concl thy i th =
   10.87 +  let
   10.88 +    val goal = Logic.get_goal (prop_of th) i |> Envir.beta_eta_contract
   10.89 +    val prem = goal |> Logic.strip_assums_hyp |> hd
   10.90 +    val concl = goal |> Logic.strip_assums_concl
   10.91 +    fun pair_untyped_aconv (t1, t2) (u1, u2) =
   10.92 +      untyped_aconv t1 u1 andalso untyped_aconv t2 u2
   10.93 +    fun add_terms tp inst =
   10.94 +      if exists (pair_untyped_aconv tp) inst then inst
   10.95 +      else tp :: map (apsnd (subst_atomic [tp])) inst
   10.96 +    fun is_flex t =
   10.97 +      case strip_comb t of
   10.98 +        (Var _, args) => forall is_Bound args
   10.99 +      | _ => false
  10.100 +    fun unify_flex flex rigid =
  10.101 +      case strip_comb flex of
  10.102 +        (Var (z as (_, T)), args) =>
  10.103 +        add_terms (Var z,
  10.104 +          fold_rev (curry absdummy) (take (length args) (binder_types T)) rigid)
  10.105 +      | _ => raise TERM ("unify_flex: expected flex", [flex])
  10.106 +    fun unify_potential_flex comb atom =
  10.107 +      if is_flex comb then unify_flex comb atom
  10.108 +      else if is_Var atom then add_terms (atom, comb)
  10.109 +      else raise TERM ("unify_terms", [comb, atom])
  10.110 +    fun unify_terms (t, u) =
  10.111 +      case (t, u) of
  10.112 +        (t1 $ t2, u1 $ u2) =>
  10.113 +        if is_flex t then unify_flex t u
  10.114 +        else if is_flex u then unify_flex u t
  10.115 +        else fold unify_terms [(t1, u1), (t2, u2)]
  10.116 +      | (_ $ _, _) => unify_potential_flex t u
  10.117 +      | (_, _ $ _) => unify_potential_flex u t
  10.118 +      | (Var _, _) => add_terms (t, u)
  10.119 +      | (_, Var _) => add_terms (u, t)
  10.120 +      | _ => if untyped_aconv t u then I else raise TERM ("unify_terms", [t, u])
  10.121 +  in th |> instantiate_theorem thy (unify_terms (prem, concl) []) end
  10.122 +
  10.123 +fun shuffle_key (((axiom_no, (_, index_no)), _), _) = (index_no, axiom_no)
  10.124 +fun shuffle_ord p =
  10.125 +  rev_order (prod_ord int_ord int_ord (pairself shuffle_key p))
  10.126 +
  10.127 +val copy_prem = @{lemma "P ==> (P ==> P ==> Q) ==> Q" by fast}
  10.128 +
  10.129 +fun copy_prems_tac [] ns i =
  10.130 +    if forall (curry (op =) 1) ns then all_tac else copy_prems_tac (rev ns) [] i
  10.131 +  | copy_prems_tac (1 :: ms) ns i =
  10.132 +    rotate_tac 1 i THEN copy_prems_tac ms (1 :: ns) i
  10.133 +  | copy_prems_tac (m :: ms) ns i =
  10.134 +    etac copy_prem i THEN copy_prems_tac ms (m div 2 :: (m + 1) div 2 :: ns) i
  10.135 +
  10.136 +fun instantiate_forall_tac thy params t i =
  10.137 +  let
  10.138 +    fun repair (t as (Var ((s, _), _))) =
  10.139 +        (case find_index (fn ((s', _), _) => s' = s) params of
  10.140 +           ~1 => t
  10.141 +         | j => Bound j)
  10.142 +      | repair (t $ u) = repair t $ repair u
  10.143 +      | repair t = t
  10.144 +    val t' = t |> repair |> fold (curry absdummy) (map snd params)
  10.145 +    fun do_instantiate th =
  10.146 +      let val var = Term.add_vars (prop_of th) [] |> the_single in
  10.147 +        th |> instantiate_theorem thy [(Var var, t')]
  10.148 +      end
  10.149 +  in
  10.150 +    etac @{thm allE} i
  10.151 +    THEN rotate_tac ~1 i
  10.152 +    THEN PRIMITIVE do_instantiate
  10.153 +  end
  10.154 +
  10.155 +fun release_clusters_tac _ _ _ _ [] = K all_tac
  10.156 +  | release_clusters_tac thy ax_counts substs params
  10.157 +                         ((ax_no, cluster_no) :: clusters) =
  10.158 +    let
  10.159 +      fun in_right_cluster s =
  10.160 +        (s |> Meson_Clausify.cluster_of_zapped_var_name |> fst |> snd |> fst)
  10.161 +        = cluster_no
  10.162 +      val cluster_substs =
  10.163 +        substs
  10.164 +        |> map_filter (fn (ax_no', (_, (_, tsubst))) =>
  10.165 +                          if ax_no' = ax_no then
  10.166 +                            tsubst |> filter (in_right_cluster
  10.167 +                                               o fst o fst o dest_Var o fst)
  10.168 +                                    |> map snd |> SOME
  10.169 +                           else
  10.170 +                             NONE)
  10.171 +      val n = length cluster_substs
  10.172 +      fun do_cluster_subst cluster_subst =
  10.173 +        map (instantiate_forall_tac thy params) cluster_subst @ [rotate_tac 1]
  10.174 +      val params' = params (* FIXME ### existentials! *)
  10.175 +      val first_prem = find_index (fn (ax_no', _) => ax_no' = ax_no) substs
  10.176 +    in
  10.177 +      rotate_tac first_prem
  10.178 +      THEN' (EVERY' (maps do_cluster_subst cluster_substs))
  10.179 +      THEN' rotate_tac (~ first_prem - length cluster_substs)
  10.180 +      THEN' release_clusters_tac thy ax_counts substs params' clusters
  10.181 +    end
  10.182 +
  10.183 +val cluster_ord =
  10.184 +  prod_ord (prod_ord int_ord (prod_ord int_ord int_ord)) bool_ord
  10.185 +
  10.186 +val tysubst_ord =
  10.187 +  list_ord (prod_ord Term_Ord.fast_indexname_ord
  10.188 +                     (prod_ord Term_Ord.sort_ord Term_Ord.typ_ord))
  10.189 +
  10.190 +structure Int_Tysubst_Table =
  10.191 +  Table(type key = int * (indexname * (sort * typ)) list
  10.192 +        val ord = prod_ord int_ord tysubst_ord)
  10.193 +
  10.194 +(* Attempts to derive the theorem "False" from a theorem of the form
  10.195 +   "P1 ==> ... ==> Pn ==> False", where the "Pi"s are to be discharged using the
  10.196 +   specified axioms. The axioms have leading "All" and "Ex" quantifiers, which
  10.197 +   must be eliminated first. *)
  10.198 +fun discharge_skolem_premises ctxt axioms prems_imp_false =
  10.199 +  if prop_of prems_imp_false aconv @{prop False} then
  10.200 +    prems_imp_false
  10.201 +  else
  10.202 +    let
  10.203 +      val thy = ProofContext.theory_of ctxt
  10.204 +      (* distinguish variables with same name but different types *)
  10.205 +      val prems_imp_false' =
  10.206 +        prems_imp_false |> try (forall_intr_vars #> gen_all)
  10.207 +                        |> the_default prems_imp_false
  10.208 +      val prems_imp_false =
  10.209 +        if prop_of prems_imp_false aconv prop_of prems_imp_false' then
  10.210 +          prems_imp_false
  10.211 +        else
  10.212 +          prems_imp_false'
  10.213 +      fun match_term p =
  10.214 +        let
  10.215 +          val (tyenv, tenv) =
  10.216 +            Pattern.first_order_match thy p (Vartab.empty, Vartab.empty)
  10.217 +          val tsubst =
  10.218 +            tenv |> Vartab.dest
  10.219 +                 |> sort (cluster_ord
  10.220 +                          o pairself (Meson_Clausify.cluster_of_zapped_var_name
  10.221 +                                      o fst o fst))
  10.222 +                 |> map (Meson.term_pair_of
  10.223 +                         #> pairself (Envir.subst_term_types tyenv))
  10.224 +          val tysubst = tyenv |> Vartab.dest
  10.225 +        in (tysubst, tsubst) end
  10.226 +      fun subst_info_for_prem subgoal_no prem =
  10.227 +        case prem of
  10.228 +          _ $ (Const (@{const_name skolem}, _) $ (_ $ t $ num)) =>
  10.229 +          let val ax_no = HOLogic.dest_nat num in
  10.230 +            (ax_no, (subgoal_no,
  10.231 +                     match_term (nth axioms ax_no |> the |> snd, t)))
  10.232 +          end
  10.233 +        | _ => raise TERM ("discharge_skolem_premises: Malformed premise",
  10.234 +                           [prem])
  10.235 +      fun cluster_of_var_name skolem s =
  10.236 +        let
  10.237 +          val ((ax_no, (cluster_no, _)), skolem') =
  10.238 +            Meson_Clausify.cluster_of_zapped_var_name s
  10.239 +        in
  10.240 +          if skolem' = skolem andalso cluster_no > 0 then
  10.241 +            SOME (ax_no, cluster_no)
  10.242 +          else
  10.243 +            NONE
  10.244 +        end
  10.245 +      fun clusters_in_term skolem t =
  10.246 +        Term.add_var_names t [] |> map_filter (cluster_of_var_name skolem o fst)
  10.247 +      fun deps_for_term_subst (var, t) =
  10.248 +        case clusters_in_term false var of
  10.249 +          [] => NONE
  10.250 +        | [(ax_no, cluster_no)] =>
  10.251 +          SOME ((ax_no, cluster_no),
  10.252 +                clusters_in_term true t
  10.253 +                |> cluster_no > 1 ? cons (ax_no, cluster_no - 1))
  10.254 +        | _ => raise TERM ("discharge_skolem_premises: Expected Var", [var])
  10.255 +      val prems = Logic.strip_imp_prems (prop_of prems_imp_false)
  10.256 +      val substs = prems |> map2 subst_info_for_prem (1 upto length prems)
  10.257 +                         |> sort (int_ord o pairself fst)
  10.258 +      val depss = maps (map_filter deps_for_term_subst o snd o snd o snd) substs
  10.259 +      val clusters = maps (op ::) depss
  10.260 +      val ordered_clusters =
  10.261 +        Int_Pair_Graph.empty
  10.262 +        |> fold Int_Pair_Graph.default_node (map (rpair ()) clusters)
  10.263 +        |> fold Int_Pair_Graph.add_deps_acyclic depss
  10.264 +        |> Int_Pair_Graph.topological_order
  10.265 +        handle Int_Pair_Graph.CYCLES _ =>
  10.266 +               error "Cannot replay Metis proof in Isabelle without axiom of \
  10.267 +                     \choice."
  10.268 +      val params0 =
  10.269 +        [] |> fold (Term.add_vars o snd) (map_filter I axioms)
  10.270 +           |> map (`(Meson_Clausify.cluster_of_zapped_var_name o fst o fst))
  10.271 +           |> filter (fn (((_, (cluster_no, _)), skolem), _) =>
  10.272 +                         cluster_no = 0 andalso skolem)
  10.273 +           |> sort shuffle_ord |> map snd
  10.274 +      val ax_counts =
  10.275 +        Int_Tysubst_Table.empty
  10.276 +        |> fold (fn (ax_no, (_, (tysubst, _))) =>
  10.277 +                    Int_Tysubst_Table.map_default ((ax_no, tysubst), 0)
  10.278 +                                                  (Integer.add 1)) substs
  10.279 +        |> Int_Tysubst_Table.dest
  10.280 +(* for debugging:
  10.281 +      fun string_for_subst_info (ax_no, (subgoal_no, (tysubst, tsubst))) =
  10.282 +        "ax: " ^ string_of_int ax_no ^ "; asm: " ^ string_of_int subgoal_no ^
  10.283 +        "; tysubst: " ^ PolyML.makestring tysubst ^ "; tsubst: {" ^
  10.284 +        commas (map ((fn (s, t) => s ^ " |-> " ^ t)
  10.285 +                     o pairself (Syntax.string_of_term ctxt)) tsubst) ^ "}"
  10.286 +      val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^
  10.287 +                       cat_lines (map string_for_subst_info substs))
  10.288 +      val _ = tracing ("OUTERMOST SKOLEMS: " ^ PolyML.makestring params0)
  10.289 +      val _ = tracing ("ORDERED CLUSTERS: " ^ PolyML.makestring ordered_clusters)
  10.290 +      val _ = tracing ("AXIOM COUNTS: " ^ PolyML.makestring ax_counts)
  10.291 +*)
  10.292 +      fun rotation_for_subgoal i =
  10.293 +        find_index (fn (_, (subgoal_no, _)) => subgoal_no = i) substs
  10.294 +    in
  10.295 +      Goal.prove ctxt [] [] @{prop False}
  10.296 +          (K (cut_rules_tac
  10.297 +                  (map (fst o the o nth axioms o fst o fst) ax_counts) 1
  10.298 +              THEN print_tac "cut:"
  10.299 +              THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1)
  10.300 +              THEN copy_prems_tac (map snd ax_counts) [] 1
  10.301 +              THEN print_tac "eliminated exist and copied prems:"
  10.302 +              THEN release_clusters_tac thy ax_counts substs params0
  10.303 +                                        ordered_clusters 1
  10.304 +              THEN print_tac "released clusters:"
  10.305 +              THEN match_tac [prems_imp_false] 1
  10.306 +              THEN print_tac "applied rule:"
  10.307 +              THEN ALLGOALS (fn i =>
  10.308 +                       rtac @{thm skolem_COMBK_I} i
  10.309 +                       THEN rotate_tac (rotation_for_subgoal i) i
  10.310 +                       THEN PRIMITIVE (unify_first_prem_with_concl thy i)
  10.311 +                       THEN assume_tac i)))
  10.312 +    end
  10.313 +
  10.314 +(* Main function to start Metis proof and reconstruction *)
  10.315 +fun FOL_SOLVE mode ctxt cls ths0 =
  10.316 +  let val thy = ProofContext.theory_of ctxt
  10.317 +      val type_lits = Config.get ctxt type_lits
  10.318 +      val new_skolemizer =
  10.319 +        Config.get ctxt new_skolemizer orelse null (Meson_Choices.get ctxt)
  10.320 +      val th_cls_pairs =
  10.321 +        map2 (fn j => fn th =>
  10.322 +                (Thm.get_name_hint th,
  10.323 +                 Meson_Clausify.cnf_axiom ctxt new_skolemizer j th))
  10.324 +             (0 upto length ths0 - 1) ths0
  10.325 +      val thss = map (snd o snd) th_cls_pairs
  10.326 +      val dischargers = map (fst o snd) th_cls_pairs
  10.327 +      val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
  10.328 +      val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
  10.329 +      val _ = trace_msg (fn () => "THEOREM CLAUSES")
  10.330 +      val _ = app (app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th))) thss
  10.331 +      val (mode, {axioms, tfrees, old_skolems}) =
  10.332 +        build_logic_map mode ctxt type_lits cls thss
  10.333 +      val _ = if null tfrees then ()
  10.334 +              else (trace_msg (fn () => "TFREE CLAUSES");
  10.335 +                    app (fn TyLitFree ((s, _), (s', _)) =>
  10.336 +                            trace_msg (fn () => s ^ "(" ^ s' ^ ")")) tfrees)
  10.337 +      val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS")
  10.338 +      val thms = map #1 axioms
  10.339 +      val _ = app (fn th => trace_msg (fn () => Metis_Thm.toString th)) thms
  10.340 +      val _ = trace_msg (fn () => "mode = " ^ string_of_mode mode)
  10.341 +      val _ = trace_msg (fn () => "START METIS PROVE PROCESS")
  10.342 +  in
  10.343 +      case filter (is_false o prop_of) cls of
  10.344 +          false_th::_ => [false_th RS @{thm FalseE}]
  10.345 +        | [] =>
  10.346 +      case Metis_Resolution.new resolution_params {axioms = thms, conjecture = []}
  10.347 +           |> Metis_Resolution.loop of
  10.348 +          Metis_Resolution.Contradiction mth =>
  10.349 +            let val _ = trace_msg (fn () => "METIS RECONSTRUCTION START: " ^
  10.350 +                          Metis_Thm.toString mth)
  10.351 +                val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
  10.352 +                             (*add constraints arising from converting goal to clause form*)
  10.353 +                val proof = Metis_Proof.proof mth
  10.354 +                val result =
  10.355 +                  fold (replay_one_inference ctxt' mode old_skolems) proof axioms
  10.356 +                and used = map_filter (used_axioms axioms) proof
  10.357 +                val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:")
  10.358 +                val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used
  10.359 +                val unused = th_cls_pairs |> map_filter (fn (name, (_, cls)) =>
  10.360 +                  if have_common_thm used cls then NONE else SOME name)
  10.361 +            in
  10.362 +                if not (null cls) andalso not (have_common_thm used cls) then
  10.363 +                  warning "Metis: The assumptions are inconsistent."
  10.364 +                else
  10.365 +                  ();
  10.366 +                if not (null unused) then
  10.367 +                  warning ("Metis: Unused theorems: " ^ commas_quote unused
  10.368 +                           ^ ".")
  10.369 +                else
  10.370 +                  ();
  10.371 +                case result of
  10.372 +                    (_,ith)::_ =>
  10.373 +                        (trace_msg (fn () => "Success: " ^ Display.string_of_thm ctxt ith);
  10.374 +                         [discharge_skolem_premises ctxt dischargers ith])
  10.375 +                  | _ => (trace_msg (fn () => "Metis: No result"); [])
  10.376 +            end
  10.377 +        | Metis_Resolution.Satisfiable _ =>
  10.378 +            (trace_msg (fn () => "Metis: No first-order proof with the lemmas supplied");
  10.379 +             [])
  10.380 +  end;
  10.381 +
  10.382 +(* Extensionalize "th", because that makes sense and that's what Sledgehammer
  10.383 +   does, but also keep an unextensionalized version of "th" for backward
  10.384 +   compatibility. *)
  10.385 +fun also_extensionalize_theorem th =
  10.386 +  let val th' = Meson_Clausify.extensionalize_theorem th in
  10.387 +    if Thm.eq_thm (th, th') then [th]
  10.388 +    else th :: Meson.make_clauses_unsorted [th']
  10.389 +  end
  10.390 +
  10.391 +val neg_clausify =
  10.392 +  single
  10.393 +  #> Meson.make_clauses_unsorted
  10.394 +  #> maps also_extensionalize_theorem
  10.395 +  #> map Meson_Clausify.introduce_combinators_in_theorem
  10.396 +  #> Meson.finish_cnf
  10.397 +
  10.398 +fun preskolem_tac ctxt st0 =
  10.399 +  (if exists (Meson.has_too_many_clauses ctxt)
  10.400 +             (Logic.prems_of_goal (prop_of st0) 1) then
  10.401 +     cnf.cnfx_rewrite_tac ctxt 1
  10.402 +   else
  10.403 +     all_tac) st0
  10.404 +
  10.405 +val type_has_top_sort =
  10.406 +  exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
  10.407 +
  10.408 +fun generic_metis_tac mode ctxt ths i st0 =
  10.409 +  let
  10.410 +    val _ = trace_msg (fn () =>
  10.411 +        "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
  10.412 +  in
  10.413 +    if exists_type type_has_top_sort (prop_of st0) then
  10.414 +      (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty)
  10.415 +    else
  10.416 +      Meson.MESON (preskolem_tac ctxt) (maps neg_clausify)
  10.417 +                  (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
  10.418 +                  ctxt i st0
  10.419 +  end
  10.420 +
  10.421 +val metis_tac = generic_metis_tac HO
  10.422 +val metisF_tac = generic_metis_tac FO
  10.423 +val metisFT_tac = generic_metis_tac FT
  10.424 +
  10.425 +(* Whenever "X" has schematic type variables, we treat "using X by metis" as
  10.426 +   "by (metis X)", to prevent "Subgoal.FOCUS" from freezing the type variables.
  10.427 +   We don't do it for nonschematic facts "X" because this breaks a few proofs
  10.428 +   (in the rare and subtle case where a proof relied on extensionality not being
  10.429 +   applied) and brings few benefits. *)
  10.430 +val has_tvar =
  10.431 +  exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of
  10.432 +fun method name mode =
  10.433 +  Method.setup name (Attrib.thms >> (fn ths => fn ctxt =>
  10.434 +    METHOD (fn facts =>
  10.435 +               let
  10.436 +                 val (schem_facts, nonschem_facts) =
  10.437 +                   List.partition has_tvar facts
  10.438 +               in
  10.439 +                 HEADGOAL (Method.insert_tac nonschem_facts THEN'
  10.440 +                           CHANGED_PROP
  10.441 +                           o generic_metis_tac mode ctxt (schem_facts @ ths))
  10.442 +               end)))
  10.443 +
  10.444 +val setup =
  10.445 +  type_lits_setup
  10.446 +  #> new_skolemizer_setup
  10.447 +  #> method @{binding metis} HO "Metis for FOL/HOL problems"
  10.448 +  #> method @{binding metisF} FO "Metis for FOL problems"
  10.449 +  #> method @{binding metisFT} FT
  10.450 +            "Metis for FOL/HOL problems with fully-typed translation"
  10.451 +
  10.452 +end;
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML	Mon Oct 04 22:45:09 2010 +0200
    11.3 @@ -0,0 +1,771 @@
    11.4 +(*  Title:      HOL/Tools/Sledgehammer/metis_translate.ML
    11.5 +    Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
    11.6 +    Author:     Kong W. Susanto, Cambridge University Computer Laboratory
    11.7 +    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
    11.8 +    Author:     Jasmin Blanchette, TU Muenchen
    11.9 +
   11.10 +Translation of HOL to FOL for Metis.
   11.11 +*)
   11.12 +
   11.13 +signature METIS_TRANSLATE =
   11.14 +sig
   11.15 +  type name = string * string
   11.16 +  datatype type_literal =
   11.17 +    TyLitVar of name * name |
   11.18 +    TyLitFree of name * name
   11.19 +  datatype arLit =
   11.20 +    TConsLit of name * name * name list |
   11.21 +    TVarLit of name * name
   11.22 +  datatype arity_clause =
   11.23 +    ArityClause of {name: string, conclLit: arLit, premLits: arLit list}
   11.24 +  datatype class_rel_clause =
   11.25 +    ClassRelClause of {name: string, subclass: name, superclass: name}
   11.26 +  datatype combtyp =
   11.27 +    CombTVar of name |
   11.28 +    CombTFree of name |
   11.29 +    CombType of name * combtyp list
   11.30 +  datatype combterm =
   11.31 +    CombConst of name * combtyp * combtyp list (* Const and Free *) |
   11.32 +    CombVar of name * combtyp |
   11.33 +    CombApp of combterm * combterm
   11.34 +  datatype fol_literal = FOLLiteral of bool * combterm
   11.35 +
   11.36 +  datatype mode = FO | HO | FT
   11.37 +  type logic_map =
   11.38 +    {axioms: (Metis_Thm.thm * thm) list,
   11.39 +     tfrees: type_literal list,
   11.40 +     old_skolems: (string * term) list}
   11.41 +
   11.42 +  val type_wrapper_name : string
   11.43 +  val bound_var_prefix : string
   11.44 +  val schematic_var_prefix: string
   11.45 +  val fixed_var_prefix: string
   11.46 +  val tvar_prefix: string
   11.47 +  val tfree_prefix: string
   11.48 +  val const_prefix: string
   11.49 +  val type_const_prefix: string
   11.50 +  val class_prefix: string
   11.51 +  val new_skolem_const_prefix : string
   11.52 +  val invert_const: string -> string
   11.53 +  val ascii_of: string -> string
   11.54 +  val unascii_of: string -> string
   11.55 +  val strip_prefix_and_unascii: string -> string -> string option
   11.56 +  val make_bound_var : string -> string
   11.57 +  val make_schematic_var : string * int -> string
   11.58 +  val make_fixed_var : string -> string
   11.59 +  val make_schematic_type_var : string * int -> string
   11.60 +  val make_fixed_type_var : string -> string
   11.61 +  val make_fixed_const : string -> string
   11.62 +  val make_fixed_type_const : string -> string
   11.63 +  val make_type_class : string -> string
   11.64 +  val num_type_args: theory -> string -> int
   11.65 +  val new_skolem_var_from_const: string -> indexname
   11.66 +  val type_literals_for_types : typ list -> type_literal list
   11.67 +  val make_class_rel_clauses :
   11.68 +    theory -> class list -> class list -> class_rel_clause list
   11.69 +  val make_arity_clauses :
   11.70 +    theory -> string list -> class list -> class list * arity_clause list
   11.71 +  val combtyp_of : combterm -> combtyp
   11.72 +  val strip_combterm_comb : combterm -> combterm * combterm list
   11.73 +  val combterm_from_term :
   11.74 +    theory -> int -> (string * typ) list -> term -> combterm * typ list
   11.75 +  val reveal_old_skolem_terms : (string * term) list -> term -> term
   11.76 +  val tfree_classes_of_terms : term list -> string list
   11.77 +  val tvar_classes_of_terms : term list -> string list
   11.78 +  val type_consts_of_terms : theory -> term list -> string list
   11.79 +  val string_of_mode : mode -> string
   11.80 +  val build_logic_map :
   11.81 +    mode -> Proof.context -> bool -> thm list -> thm list list
   11.82 +    -> mode * logic_map
   11.83 +end
   11.84 +
   11.85 +structure Metis_Translate : METIS_TRANSLATE =
   11.86 +struct
   11.87 +
   11.88 +val type_wrapper_name = "ti"
   11.89 +
   11.90 +val bound_var_prefix = "B_"
   11.91 +val schematic_var_prefix = "V_"
   11.92 +val fixed_var_prefix = "v_"
   11.93 +
   11.94 +val tvar_prefix = "T_";
   11.95 +val tfree_prefix = "t_";
   11.96 +
   11.97 +val const_prefix = "c_";
   11.98 +val type_const_prefix = "tc_";
   11.99 +val class_prefix = "class_";
  11.100 +
  11.101 +val skolem_const_prefix = "Sledgehammer" ^ Long_Name.separator ^ "Sko"
  11.102 +val old_skolem_const_prefix = skolem_const_prefix ^ "o"
  11.103 +val new_skolem_const_prefix = skolem_const_prefix ^ "n"
  11.104 +
  11.105 +fun union_all xss = fold (union (op =)) xss []
  11.106 +
  11.107 +(* Readable names for the more common symbolic functions. Do not mess with the
  11.108 +   last nine entries of the table unless you know what you are doing. *)
  11.109 +val const_trans_table =
  11.110 +  Symtab.make [(@{type_name Product_Type.prod}, "prod"),
  11.111 +               (@{type_name Sum_Type.sum}, "sum"),
  11.112 +               (@{const_name HOL.eq}, "equal"),
  11.113 +               (@{const_name HOL.conj}, "and"),
  11.114 +               (@{const_name HOL.disj}, "or"),
  11.115 +               (@{const_name HOL.implies}, "implies"),
  11.116 +               (@{const_name Set.member}, "member"),
  11.117 +               (@{const_name fequal}, "fequal"),
  11.118 +               (@{const_name COMBI}, "COMBI"),
  11.119 +               (@{const_name COMBK}, "COMBK"),
  11.120 +               (@{const_name COMBB}, "COMBB"),
  11.121 +               (@{const_name COMBC}, "COMBC"),
  11.122 +               (@{const_name COMBS}, "COMBS"),
  11.123 +               (@{const_name True}, "True"),
  11.124 +               (@{const_name False}, "False"),
  11.125 +               (@{const_name If}, "If")]
  11.126 +
  11.127 +(* Invert the table of translations between Isabelle and ATPs. *)
  11.128 +val const_trans_table_inv =
  11.129 +  Symtab.update ("fequal", @{const_name HOL.eq})
  11.130 +                (Symtab.make (map swap (Symtab.dest const_trans_table)))
  11.131 +
  11.132 +val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
  11.133 +
  11.134 +(*Escaping of special characters.
  11.135 +  Alphanumeric characters are left unchanged.
  11.136 +  The character _ goes to __
  11.137 +  Characters in the range ASCII space to / go to _A to _P, respectively.
  11.138 +  Other characters go to _nnn where nnn is the decimal ASCII code.*)
  11.139 +val A_minus_space = Char.ord #"A" - Char.ord #" ";
  11.140 +
  11.141 +fun stringN_of_int 0 _ = ""
  11.142 +  | stringN_of_int k n = stringN_of_int (k-1) (n div 10) ^ Int.toString (n mod 10);
  11.143 +
  11.144 +fun ascii_of_c c =
  11.145 +  if Char.isAlphaNum c then String.str c
  11.146 +  else if c = #"_" then "__"
  11.147 +  else if #" " <= c andalso c <= #"/"
  11.148 +       then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space))
  11.149 +  else ("_" ^ stringN_of_int 3 (Char.ord c))  (*fixed width, in case more digits follow*)
  11.150 +
  11.151 +val ascii_of = String.translate ascii_of_c;
  11.152 +
  11.153 +(** Remove ASCII armouring from names in proof files **)
  11.154 +
  11.155 +(*We don't raise error exceptions because this code can run inside the watcher.
  11.156 +  Also, the errors are "impossible" (hah!)*)
  11.157 +fun unascii_aux rcs [] = String.implode(rev rcs)
  11.158 +  | unascii_aux rcs [#"_"] = unascii_aux (#"_"::rcs) []  (*ERROR*)
  11.159 +      (*Three types of _ escapes: __, _A to _P, _nnn*)
  11.160 +  | unascii_aux rcs (#"_" :: #"_" :: cs) = unascii_aux (#"_"::rcs) cs
  11.161 +  | unascii_aux rcs (#"_" :: c :: cs) =
  11.162 +      if #"A" <= c andalso c<= #"P"  (*translation of #" " to #"/"*)
  11.163 +      then unascii_aux (Char.chr(Char.ord c - A_minus_space) :: rcs) cs
  11.164 +      else
  11.165 +        let val digits = List.take (c::cs, 3) handle Subscript => []
  11.166 +        in
  11.167 +            case Int.fromString (String.implode digits) of
  11.168 +                NONE => unascii_aux (c:: #"_"::rcs) cs  (*ERROR*)
  11.169 +              | SOME n => unascii_aux (Char.chr n :: rcs) (List.drop (cs, 2))
  11.170 +        end
  11.171 +  | unascii_aux rcs (c::cs) = unascii_aux (c::rcs) cs
  11.172 +val unascii_of = unascii_aux [] o String.explode
  11.173 +
  11.174 +(* If string s has the prefix s1, return the result of deleting it,
  11.175 +   un-ASCII'd. *)
  11.176 +fun strip_prefix_and_unascii s1 s =
  11.177 +  if String.isPrefix s1 s then
  11.178 +    SOME (unascii_of (String.extract (s, size s1, NONE)))
  11.179 +  else
  11.180 +    NONE
  11.181 +
  11.182 +(*Remove the initial ' character from a type variable, if it is present*)
  11.183 +fun trim_type_var s =
  11.184 +  if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE)
  11.185 +  else error ("trim_type: Malformed type variable encountered: " ^ s);
  11.186 +
  11.187 +fun ascii_of_indexname (v,0) = ascii_of v
  11.188 +  | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ Int.toString i;
  11.189 +
  11.190 +fun make_bound_var x = bound_var_prefix ^ ascii_of x
  11.191 +fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v
  11.192 +fun make_fixed_var x = fixed_var_prefix ^ ascii_of x
  11.193 +
  11.194 +fun make_schematic_type_var (x,i) =
  11.195 +      tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i));
  11.196 +fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x));
  11.197 +
  11.198 +fun lookup_const c =
  11.199 +  case Symtab.lookup const_trans_table c of
  11.200 +    SOME c' => c'
  11.201 +  | NONE => ascii_of c
  11.202 +
  11.203 +(* HOL.eq MUST BE "equal" because it's built into ATPs. *)
  11.204 +fun make_fixed_const @{const_name HOL.eq} = "equal"
  11.205 +  | make_fixed_const c = const_prefix ^ lookup_const c
  11.206 +
  11.207 +fun make_fixed_type_const c = type_const_prefix ^ lookup_const c
  11.208 +
  11.209 +fun make_type_class clas = class_prefix ^ ascii_of clas;
  11.210 +
  11.211 +(* The number of type arguments of a constant, zero if it's monomorphic. For
  11.212 +   (instances of) Skolem pseudoconstants, this information is encoded in the
  11.213 +   constant name. *)
  11.214 +fun num_type_args thy s =
  11.215 +  if String.isPrefix skolem_const_prefix s then
  11.216 +    s |> space_explode Long_Name.separator |> List.last |> Int.fromString |> the
  11.217 +  else
  11.218 +    (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
  11.219 +
  11.220 +fun new_skolem_var_from_const s =
  11.221 +  let
  11.222 +    val ss = s |> space_explode Long_Name.separator
  11.223 +    val n = length ss
  11.224 +  in (nth ss (n - 2), nth ss (n - 3) |> Int.fromString |> the) end
  11.225 +
  11.226 +
  11.227 +(**** Definitions and functions for FOL clauses for TPTP format output ****)
  11.228 +
  11.229 +type name = string * string
  11.230 +
  11.231 +(**** Isabelle FOL clauses ****)
  11.232 +
  11.233 +(* The first component is the type class; the second is a TVar or TFree. *)
  11.234 +datatype type_literal =
  11.235 +  TyLitVar of name * name |
  11.236 +  TyLitFree of name * name
  11.237 +
  11.238 +(*Make literals for sorted type variables*)
  11.239 +fun sorts_on_typs_aux (_, [])   = []
  11.240 +  | sorts_on_typs_aux ((x,i),  s::ss) =
  11.241 +      let val sorts = sorts_on_typs_aux ((x,i), ss)
  11.242 +      in
  11.243 +          if s = "HOL.type" then sorts
  11.244 +          else if i = ~1 then TyLitFree (`make_type_class s, `make_fixed_type_var x) :: sorts
  11.245 +          else TyLitVar (`make_type_class s, (make_schematic_type_var (x,i), x)) :: sorts
  11.246 +      end;
  11.247 +
  11.248 +fun sorts_on_typs (TFree (a,s)) = sorts_on_typs_aux ((a,~1),s)
  11.249 +  | sorts_on_typs (TVar (v,s))  = sorts_on_typs_aux (v,s);
  11.250 +
  11.251 +(*Given a list of sorted type variables, return a list of type literals.*)
  11.252 +fun type_literals_for_types Ts =
  11.253 +  fold (union (op =)) (map sorts_on_typs Ts) []
  11.254 +
  11.255 +(** make axiom and conjecture clauses. **)
  11.256 +
  11.257 +(**** Isabelle arities ****)
  11.258 +
  11.259 +datatype arLit =
  11.260 +  TConsLit of name * name * name list |
  11.261 +  TVarLit of name * name
  11.262 +
  11.263 +datatype arity_clause =
  11.264 +  ArityClause of {name: string, conclLit: arLit, premLits: arLit list}
  11.265 +
  11.266 +
  11.267 +fun gen_TVars 0 = []
  11.268 +  | gen_TVars n = ("T_" ^ Int.toString n) :: gen_TVars (n-1);
  11.269 +
  11.270 +fun pack_sort(_,[])  = []
  11.271 +  | pack_sort(tvar, "HOL.type"::srt) = pack_sort (tvar, srt)   (*IGNORE sort "type"*)
  11.272 +  | pack_sort(tvar, cls::srt) =
  11.273 +    (`make_type_class cls, (tvar, tvar)) :: pack_sort (tvar, srt)
  11.274 +
  11.275 +(*Arity of type constructor tcon :: (arg1,...,argN)res*)
  11.276 +fun make_axiom_arity_clause (tcons, name, (cls,args)) =
  11.277 +  let
  11.278 +    val tvars = gen_TVars (length args)
  11.279 +    val tvars_srts = ListPair.zip (tvars, args)
  11.280 +  in
  11.281 +    ArityClause {name = name,
  11.282 +                 conclLit = TConsLit (`make_type_class cls,
  11.283 +                                      `make_fixed_type_const tcons,
  11.284 +                                      tvars ~~ tvars),
  11.285 +                 premLits = map TVarLit (union_all (map pack_sort tvars_srts))}
  11.286 +  end
  11.287 +
  11.288 +
  11.289 +(**** Isabelle class relations ****)
  11.290 +
  11.291 +datatype class_rel_clause =
  11.292 +  ClassRelClause of {name: string, subclass: name, superclass: name}
  11.293 +
  11.294 +(*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)
  11.295 +fun class_pairs _ [] _ = []
  11.296 +  | class_pairs thy subs supers =
  11.297 +      let
  11.298 +        val class_less = Sorts.class_less (Sign.classes_of thy)
  11.299 +        fun add_super sub super = class_less (sub, super) ? cons (sub, super)
  11.300 +        fun add_supers sub = fold (add_super sub) supers
  11.301 +      in fold add_supers subs [] end
  11.302 +
  11.303 +fun make_class_rel_clause (sub,super) =
  11.304 +  ClassRelClause {name = sub ^ "_" ^ super,
  11.305 +                  subclass = `make_type_class sub,
  11.306 +                  superclass = `make_type_class super}
  11.307 +
  11.308 +fun make_class_rel_clauses thy subs supers =
  11.309 +  map make_class_rel_clause (class_pairs thy subs supers);
  11.310 +
  11.311 +
  11.312 +(** Isabelle arities **)
  11.313 +
  11.314 +fun arity_clause _ _ (_, []) = []
  11.315 +  | arity_clause seen n (tcons, ("HOL.type",_)::ars) =  (*ignore*)
  11.316 +      arity_clause seen n (tcons,ars)
  11.317 +  | arity_clause seen n (tcons, (ar as (class,_)) :: ars) =
  11.318 +      if member (op =) seen class then (*multiple arities for the same tycon, class pair*)
  11.319 +          make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) ::
  11.320 +          arity_clause seen (n+1) (tcons,ars)
  11.321 +      else
  11.322 +          make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class, ar) ::
  11.323 +          arity_clause (class::seen) n (tcons,ars)
  11.324 +
  11.325 +fun multi_arity_clause [] = []
  11.326 +  | multi_arity_clause ((tcons, ars) :: tc_arlists) =
  11.327 +      arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists
  11.328 +
  11.329 +(*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy
  11.330 +  provided its arguments have the corresponding sorts.*)
  11.331 +fun type_class_pairs thy tycons classes =
  11.332 +  let val alg = Sign.classes_of thy
  11.333 +      fun domain_sorts tycon = Sorts.mg_domain alg tycon o single
  11.334 +      fun add_class tycon class =
  11.335 +        cons (class, domain_sorts tycon class)
  11.336 +        handle Sorts.CLASS_ERROR _ => I
  11.337 +      fun try_classes tycon = (tycon, fold (add_class tycon) classes [])
  11.338 +  in  map try_classes tycons  end;
  11.339 +
  11.340 +(*Proving one (tycon, class) membership may require proving others, so iterate.*)
  11.341 +fun iter_type_class_pairs _ _ [] = ([], [])
  11.342 +  | iter_type_class_pairs thy tycons classes =
  11.343 +      let val cpairs = type_class_pairs thy tycons classes
  11.344 +          val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs)))
  11.345 +            |> subtract (op =) classes |> subtract (op =) HOLogic.typeS
  11.346 +          val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
  11.347 +      in (union (op =) classes' classes, union (op =) cpairs' cpairs) end;
  11.348 +
  11.349 +fun make_arity_clauses thy tycons classes =
  11.350 +  let val (classes', cpairs) = iter_type_class_pairs thy tycons classes
  11.351 +  in  (classes', multi_arity_clause cpairs)  end;
  11.352 +
  11.353 +datatype combtyp =
  11.354 +  CombTVar of name |
  11.355 +  CombTFree of name |
  11.356 +  CombType of name * combtyp list
  11.357 +
  11.358 +datatype combterm =
  11.359 +  CombConst of name * combtyp * combtyp list (* Const and Free *) |
  11.360 +  CombVar of name * combtyp |
  11.361 +  CombApp of combterm * combterm
  11.362 +
  11.363 +datatype fol_literal = FOLLiteral of bool * combterm
  11.364 +
  11.365 +(*********************************************************************)
  11.366 +(* convert a clause with type Term.term to a clause with type clause *)
  11.367 +(*********************************************************************)
  11.368 +
  11.369 +(*Result of a function type; no need to check that the argument type matches.*)
  11.370 +fun result_type (CombType (_, [_, tp2])) = tp2
  11.371 +  | result_type _ = raise Fail "non-function type"
  11.372 +
  11.373 +fun combtyp_of (CombConst (_, tp, _)) = tp
  11.374 +  | combtyp_of (CombVar (_, tp)) = tp
  11.375 +  | combtyp_of (CombApp (t1, _)) = result_type (combtyp_of t1)
  11.376 +
  11.377 +(*gets the head of a combinator application, along with the list of arguments*)
  11.378 +fun strip_combterm_comb u =
  11.379 +    let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
  11.380 +        |   stripc  x =  x
  11.381 +    in stripc(u,[]) end
  11.382 +
  11.383 +fun combtype_of (Type (a, Ts)) =
  11.384 +    let val (folTypes, ts) = combtypes_of Ts in
  11.385 +      (CombType (`make_fixed_type_const a, folTypes), ts)
  11.386 +    end
  11.387 +  | combtype_of (tp as TFree (a, _)) = (CombTFree (`make_fixed_type_var a), [tp])
  11.388 +  | combtype_of (tp as TVar (x, _)) =
  11.389 +    (CombTVar (make_schematic_type_var x, string_of_indexname x), [tp])
  11.390 +and combtypes_of Ts =
  11.391 +  let val (folTyps, ts) = ListPair.unzip (map combtype_of Ts) in
  11.392 +    (folTyps, union_all ts)
  11.393 +  end
  11.394 +
  11.395 +(* same as above, but no gathering of sort information *)
  11.396 +fun simple_combtype_of (Type (a, Ts)) =
  11.397 +    CombType (`make_fixed_type_const a, map simple_combtype_of Ts)
  11.398 +  | simple_combtype_of (TFree (a, _)) = CombTFree (`make_fixed_type_var a)
  11.399 +  | simple_combtype_of (TVar (x, _)) =
  11.400 +    CombTVar (make_schematic_type_var x, string_of_indexname x)
  11.401 +
  11.402 +fun new_skolem_const_name th_no s num_T_args =
  11.403 +  [new_skolem_const_prefix, string_of_int th_no, s, string_of_int num_T_args]
  11.404 +  |> space_implode Long_Name.separator
  11.405 +
  11.406 +(* Converts a term (with combinators) into a combterm. Also accummulates sort
  11.407 +   infomation. *)
  11.408 +fun combterm_from_term thy th_no bs (P $ Q) =
  11.409 +      let val (P', tsP) = combterm_from_term thy th_no bs P
  11.410 +          val (Q', tsQ) = combterm_from_term thy th_no bs Q
  11.411 +      in  (CombApp (P', Q'), union (op =) tsP tsQ)  end
  11.412 +  | combterm_from_term thy _ _ (Const (c, T)) =
  11.413 +      let
  11.414 +        val (tp, ts) = combtype_of T
  11.415 +        val tvar_list =
  11.416 +          (if String.isPrefix old_skolem_const_prefix c then
  11.417 +             [] |> Term.add_tvarsT T |> map TVar
  11.418 +           else
  11.419 +             (c, T) |> Sign.const_typargs thy)
  11.420 +          |> map simple_combtype_of
  11.421 +        val c' = CombConst (`make_fixed_const c, tp, tvar_list)
  11.422 +      in  (c',ts)  end
  11.423 +  | combterm_from_term _ _ _ (Free (v, T)) =
  11.424 +      let val (tp, ts) = combtype_of T
  11.425 +          val v' = CombConst (`make_fixed_var v, tp, [])
  11.426 +      in  (v',ts)  end
  11.427 +  | combterm_from_term _ th_no _ (Var (v as (s, _), T)) =
  11.428 +    let
  11.429 +      val (tp, ts) = combtype_of T
  11.430 +      val v' =
  11.431 +        if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
  11.432 +          let
  11.433 +            val tys = T |> strip_type |> swap |> op ::
  11.434 +            val s' = new_skolem_const_name th_no s (length tys)
  11.435 +          in
  11.436 +            CombConst (`make_fixed_const s', tp, map simple_combtype_of tys)
  11.437 +          end
  11.438 +        else
  11.439 +          CombVar ((make_schematic_var v, string_of_indexname v), tp)
  11.440 +    in (v', ts) end
  11.441 +  | combterm_from_term _ _ bs (Bound j) =
  11.442 +      let
  11.443 +        val (s, T) = nth bs j
  11.444 +        val (tp, ts) = combtype_of T
  11.445 +        val v' = CombConst (`make_bound_var s, tp, [])
  11.446 +      in (v', ts) end
  11.447 +  | combterm_from_term _ _ _ (Abs _) = raise Fail "HOL clause: Abs"
  11.448 +
  11.449 +fun predicate_of thy th_no ((@{const Not} $ P), pos) =
  11.450 +    predicate_of thy th_no (P, not pos)
  11.451 +  | predicate_of thy th_no (t, pos) =
  11.452 +    (combterm_from_term thy th_no [] (Envir.eta_contract t), pos)
  11.453 +
  11.454 +fun literals_of_term1 args thy th_no (@{const Trueprop} $ P) =
  11.455 +    literals_of_term1 args thy th_no P
  11.456 +  | literals_of_term1 args thy th_no (@{const HOL.disj} $ P $ Q) =
  11.457 +    literals_of_term1 (literals_of_term1 args thy th_no P) thy th_no Q
  11.458 +  | literals_of_term1 (lits, ts) thy th_no P =
  11.459 +    let val ((pred, ts'), pol) = predicate_of thy th_no (P, true) in
  11.460 +      (FOLLiteral (pol, pred) :: lits, union (op =) ts ts')
  11.461 +    end
  11.462 +val literals_of_term = literals_of_term1 ([], [])
  11.463 +
  11.464 +fun old_skolem_const_name i j num_T_args =
  11.465 +  old_skolem_const_prefix ^ Long_Name.separator ^
  11.466 +  (space_implode Long_Name.separator (map Int.toString [i, j, num_T_args]))
  11.467 +
  11.468 +fun conceal_old_skolem_terms i old_skolems t =
  11.469 +  if exists_Const (curry (op =) @{const_name skolem} o fst) t then
  11.470 +    let
  11.471 +      fun aux old_skolems
  11.472 +              (t as (Const (@{const_name skolem}, Type (_, [_, T])) $ _)) =
  11.473 +          let
  11.474 +            val (old_skolems, s) =
  11.475 +              if i = ~1 then
  11.476 +                (old_skolems, @{const_name undefined})
  11.477 +              else case AList.find (op aconv) old_skolems t of
  11.478 +                s :: _ => (old_skolems, s)
  11.479 +              | [] =>
  11.480 +                let
  11.481 +                  val s = old_skolem_const_name i (length old_skolems)
  11.482 +                                                (length (Term.add_tvarsT T []))
  11.483 +                in ((s, t) :: old_skolems, s) end
  11.484 +          in (old_skolems, Const (s, T)) end
  11.485 +        | aux old_skolems (t1 $ t2) =
  11.486 +          let
  11.487 +            val (old_skolems, t1) = aux old_skolems t1
  11.488 +            val (old_skolems, t2) = aux old_skolems t2
  11.489 +          in (old_skolems, t1 $ t2) end
  11.490 +        | aux old_skolems (Abs (s, T, t')) =
  11.491 +          let val (old_skolems, t') = aux old_skolems t' in
  11.492 +            (old_skolems, Abs (s, T, t'))
  11.493 +          end
  11.494 +        | aux old_skolems t = (old_skolems, t)
  11.495 +    in aux old_skolems t end
  11.496 +  else
  11.497 +    (old_skolems, t)
  11.498 +
  11.499 +fun reveal_old_skolem_terms old_skolems =
  11.500 +  map_aterms (fn t as Const (s, _) =>
  11.501 +                 if String.isPrefix old_skolem_const_prefix s then
  11.502 +                   AList.lookup (op =) old_skolems s |> the
  11.503 +                   |> map_types Type_Infer.paramify_vars
  11.504 +                 else
  11.505 +                   t
  11.506 +               | t => t)
  11.507 +
  11.508 +
  11.509 +(***************************************************************)
  11.510 +(* Type Classes Present in the Axiom or Conjecture Clauses     *)
  11.511 +(***************************************************************)
  11.512 +
  11.513 +fun set_insert (x, s) = Symtab.update (x, ()) s
  11.514 +
  11.515 +fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts)
  11.516 +
  11.517 +(*Remove this trivial type class*)
  11.518 +fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset;
  11.519 +
  11.520 +fun tfree_classes_of_terms ts =
  11.521 +  let val sorts_list = map (map #2 o OldTerm.term_tfrees) ts
  11.522 +  in  Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list))  end;
  11.523 +
  11.524 +fun tvar_classes_of_terms ts =
  11.525 +  let val sorts_list = map (map #2 o OldTerm.term_tvars) ts
  11.526 +  in  Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list))  end;
  11.527 +
  11.528 +(*fold type constructors*)
  11.529 +fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x))
  11.530 +  | fold_type_consts _ _ x = x;
  11.531 +
  11.532 +(*Type constructors used to instantiate overloaded constants are the only ones needed.*)
  11.533 +fun add_type_consts_in_term thy =
  11.534 +  let
  11.535 +    fun aux (Const x) =
  11.536 +        fold (fold_type_consts set_insert) (Sign.const_typargs thy x)
  11.537 +      | aux (Abs (_, _, u)) = aux u
  11.538 +      | aux (Const (@{const_name skolem}, _) $ _) = I
  11.539 +      | aux (t $ u) = aux t #> aux u
  11.540 +      | aux _ = I
  11.541 +  in aux end
  11.542 +
  11.543 +fun type_consts_of_terms thy ts =
  11.544 +  Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty);
  11.545 +
  11.546 +(* ------------------------------------------------------------------------- *)
  11.547 +(* HOL to FOL  (Isabelle to Metis)                                           *)
  11.548 +(* ------------------------------------------------------------------------- *)
  11.549 +
  11.550 +datatype mode = FO | HO | FT  (* first-order, higher-order, fully-typed *)
  11.551 +
  11.552 +fun string_of_mode FO = "FO"
  11.553 +  | string_of_mode HO = "HO"
  11.554 +  | string_of_mode FT = "FT"
  11.555 +
  11.556 +fun fn_isa_to_met_sublevel "equal" = "=" (* FIXME: "c_fequal" *)
  11.557 +  | fn_isa_to_met_sublevel x = x
  11.558 +fun fn_isa_to_met_toplevel "equal" = "="
  11.559 +  | fn_isa_to_met_toplevel x = x
  11.560 +
  11.561 +fun metis_lit b c args = (b, (c, args));
  11.562 +
  11.563 +fun metis_term_from_combtyp (CombTVar (s, _)) = Metis_Term.Var s
  11.564 +  | metis_term_from_combtyp (CombTFree (s, _)) = Metis_Term.Fn (s, [])
  11.565 +  | metis_term_from_combtyp (CombType ((s, _), tps)) =
  11.566 +    Metis_Term.Fn (s, map metis_term_from_combtyp tps);
  11.567 +
  11.568 +(*These two functions insert type literals before the real literals. That is the
  11.569 +  opposite order from TPTP linkup, but maybe OK.*)
  11.570 +
  11.571 +fun hol_term_to_fol_FO tm =
  11.572 +  case strip_combterm_comb tm of
  11.573 +      (CombConst ((c, _), _, tys), tms) =>
  11.574 +        let val tyargs = map metis_term_from_combtyp tys
  11.575 +            val args   = map hol_term_to_fol_FO tms
  11.576 +        in Metis_Term.Fn (c, tyargs @ args) end
  11.577 +    | (CombVar ((v, _), _), []) => Metis_Term.Var v
  11.578 +    | _ => raise Fail "non-first-order combterm"
  11.579 +
  11.580 +fun hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) =
  11.581 +      Metis_Term.Fn (fn_isa_to_met_sublevel a, map metis_term_from_combtyp tylist)
  11.582 +  | hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis_Term.Var s
  11.583 +  | hol_term_to_fol_HO (CombApp (tm1, tm2)) =
  11.584 +       Metis_Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]);
  11.585 +
  11.586 +(*The fully-typed translation, to avoid type errors*)
  11.587 +fun wrap_type (tm, ty) =
  11.588 +  Metis_Term.Fn (type_wrapper_name, [tm, metis_term_from_combtyp ty])
  11.589 +
  11.590 +fun hol_term_to_fol_FT (CombVar ((s, _), ty)) = wrap_type (Metis_Term.Var s, ty)
  11.591 +  | hol_term_to_fol_FT (CombConst((a, _), ty, _)) =
  11.592 +      wrap_type (Metis_Term.Fn(fn_isa_to_met_sublevel a, []), ty)
  11.593 +  | hol_term_to_fol_FT (tm as CombApp(tm1,tm2)) =
  11.594 +       wrap_type (Metis_Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]),
  11.595 +                  combtyp_of tm)
  11.596 +
  11.597 +fun hol_literal_to_fol FO (FOLLiteral (pos, tm)) =
  11.598 +      let val (CombConst((p, _), _, tys), tms) = strip_combterm_comb tm
  11.599 +          val tylits = if p = "equal" then [] else map metis_term_from_combtyp tys
  11.600 +          val lits = map hol_term_to_fol_FO tms
  11.601 +      in metis_lit pos (fn_isa_to_met_toplevel p) (tylits @ lits) end
  11.602 +  | hol_literal_to_fol HO (FOLLiteral (pos, tm)) =
  11.603 +     (case strip_combterm_comb tm of
  11.604 +          (CombConst(("equal", _), _, _), tms) =>
  11.605 +            metis_lit pos "=" (map hol_term_to_fol_HO tms)
  11.606 +        | _ => metis_lit pos "{}" [hol_term_to_fol_HO tm])   (*hBOOL*)
  11.607 +  | hol_literal_to_fol FT (FOLLiteral (pos, tm)) =
  11.608 +     (case strip_combterm_comb tm of
  11.609 +          (CombConst(("equal", _), _, _), tms) =>
  11.610 +            metis_lit pos "=" (map hol_term_to_fol_FT tms)
  11.611 +        | _ => metis_lit pos "{}" [hol_term_to_fol_FT tm])   (*hBOOL*);
  11.612 +
  11.613 +fun literals_of_hol_term thy th_no mode t =
  11.614 +      let val (lits, types_sorts) = literals_of_term thy th_no t
  11.615 +      in  (map (hol_literal_to_fol mode) lits, types_sorts) end;
  11.616 +
  11.617 +(*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*)
  11.618 +fun metis_of_type_literals pos (TyLitVar ((s, _), (s', _))) =
  11.619 +    metis_lit pos s [Metis_Term.Var s']
  11.620 +  | metis_of_type_literals pos (TyLitFree ((s, _), (s', _))) =
  11.621 +    metis_lit pos s [Metis_Term.Fn (s',[])]
  11.622 +
  11.623 +fun default_sort _ (TVar _) = false
  11.624 +  | default_sort ctxt (TFree (x, s)) = (s = the_default [] (Variable.def_sort ctxt (x, ~1)));
  11.625 +
  11.626 +fun metis_of_tfree tf =
  11.627 +  Metis_Thm.axiom (Metis_LiteralSet.singleton (metis_of_type_literals true tf));
  11.628 +
  11.629 +fun hol_thm_to_fol is_conjecture th_no ctxt type_lits mode j old_skolems th =
  11.630 +  let
  11.631 +    val thy = ProofContext.theory_of ctxt
  11.632 +    val (old_skolems, (mlits, types_sorts)) =
  11.633 +     th |> prop_of |> Logic.strip_imp_concl
  11.634 +        |> conceal_old_skolem_terms j old_skolems
  11.635 +        ||> (HOLogic.dest_Trueprop #> literals_of_hol_term thy th_no mode)
  11.636 +  in
  11.637 +    if is_conjecture then
  11.638 +      (Metis_Thm.axiom (Metis_LiteralSet.fromList mlits),
  11.639 +       type_literals_for_types types_sorts, old_skolems)
  11.640 +    else
  11.641 +      let
  11.642 +        val tylits = filter_out (default_sort ctxt) types_sorts
  11.643 +                     |> type_literals_for_types
  11.644 +        val mtylits =
  11.645 +          if type_lits then map (metis_of_type_literals false) tylits else []
  11.646 +      in
  11.647 +        (Metis_Thm.axiom (Metis_LiteralSet.fromList(mtylits @ mlits)), [],
  11.648 +         old_skolems)
  11.649 +      end
  11.650 +  end;
  11.651 +
  11.652 +val helpers =
  11.653 +  [("c_COMBI", (false, map (`I) @{thms COMBI_def})),
  11.654 +   ("c_COMBK", (false, map (`I) @{thms COMBK_def})),
  11.655 +   ("c_COMBB", (false, map (`I) @{thms COMBB_def})),
  11.656 +   ("c_COMBC", (false, map (`I) @{thms COMBC_def})),
  11.657 +   ("c_COMBS", (false, map (`I) @{thms COMBS_def})),
  11.658 +   ("c_fequal", (false, map (rpair @{thm equal_imp_equal})
  11.659 +                            @{thms fequal_imp_equal equal_imp_fequal})),
  11.660 +   ("c_True", (true, map (`I) @{thms True_or_False})),
  11.661 +   ("c_False", (true, map (`I) @{thms True_or_False})),
  11.662 +   ("c_If", (true, map (`I) @{thms if_True if_False True_or_False}))]
  11.663 +
  11.664 +(* ------------------------------------------------------------------------- *)
  11.665 +(* Logic maps manage the interface between HOL and first-order logic.        *)
  11.666 +(* ------------------------------------------------------------------------- *)
  11.667 +
  11.668 +type logic_map =
  11.669 +  {axioms: (Metis_Thm.thm * thm) list,
  11.670 +   tfrees: type_literal list,
  11.671 +   old_skolems: (string * term) list}
  11.672 +
  11.673 +fun is_quasi_fol_clause thy =
  11.674 +  Meson.is_fol_term thy o snd o conceal_old_skolem_terms ~1 [] o prop_of
  11.675 +
  11.676 +(*Extract TFree constraints from context to include as conjecture clauses*)
  11.677 +fun init_tfrees ctxt =
  11.678 +  let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts in
  11.679 +    Vartab.fold add (#2 (Variable.constraints_of ctxt)) []
  11.680 +    |> type_literals_for_types
  11.681 +  end;
  11.682 +
  11.683 +(*Insert non-logical axioms corresponding to all accumulated TFrees*)
  11.684 +fun add_tfrees {axioms, tfrees, old_skolems} : logic_map =
  11.685 +     {axioms = map (rpair TrueI o metis_of_tfree) (distinct (op =) tfrees) @
  11.686 +               axioms,
  11.687 +      tfrees = tfrees, old_skolems = old_skolems}
  11.688 +
  11.689 +(*transform isabelle type / arity clause to metis clause *)
  11.690 +fun add_type_thm [] lmap = lmap
  11.691 +  | add_type_thm ((ith, mth) :: cls) {axioms, tfrees, old_skolems} =
  11.692 +      add_type_thm cls {axioms = (mth, ith) :: axioms, tfrees = tfrees,
  11.693 +                        old_skolems = old_skolems}
  11.694 +
  11.695 +fun const_in_metis c (pred, tm_list) =
  11.696 +  let
  11.697 +    fun in_mterm (Metis_Term.Var _) = false
  11.698 +      | in_mterm (Metis_Term.Fn (".", tm_list)) = exists in_mterm tm_list
  11.699 +      | in_mterm (Metis_Term.Fn (nm, tm_list)) = c=nm orelse exists in_mterm tm_list
  11.700 +  in  c = pred orelse exists in_mterm tm_list  end;
  11.701 +
  11.702 +(* ARITY CLAUSE *)
  11.703 +fun m_arity_cls (TConsLit ((c, _), (t, _), args)) =
  11.704 +    metis_lit true c [Metis_Term.Fn(t, map (Metis_Term.Var o fst) args)]
  11.705 +  | m_arity_cls (TVarLit ((c, _), (s, _))) =
  11.706 +    metis_lit false c [Metis_Term.Var s]
  11.707 +(*TrueI is returned as the Isabelle counterpart because there isn't any.*)
  11.708 +fun arity_cls (ArityClause {conclLit, premLits, ...}) =
  11.709 +  (TrueI,
  11.710 +   Metis_Thm.axiom (Metis_LiteralSet.fromList (map m_arity_cls (conclLit :: premLits))));
  11.711 +
  11.712 +(* CLASSREL CLAUSE *)
  11.713 +fun m_class_rel_cls (subclass, _) (superclass, _) =
  11.714 +  [metis_lit false subclass [Metis_Term.Var "T"], metis_lit true superclass [Metis_Term.Var "T"]];
  11.715 +fun class_rel_cls (ClassRelClause {subclass, superclass, ...}) =
  11.716 +  (TrueI, Metis_Thm.axiom (Metis_LiteralSet.fromList (m_class_rel_cls subclass superclass)));
  11.717 +
  11.718 +fun type_ext thy tms =
  11.719 +  let val subs = tfree_classes_of_terms tms
  11.720 +      val supers = tvar_classes_of_terms tms
  11.721 +      and tycons = type_consts_of_terms thy tms
  11.722 +      val (supers', arity_clauses) = make_arity_clauses thy tycons supers
  11.723 +      val class_rel_clauses = make_class_rel_clauses thy subs supers'
  11.724 +  in  map class_rel_cls class_rel_clauses @ map arity_cls arity_clauses
  11.725 +  end;
  11.726 +
  11.727 +(* Function to generate metis clauses, including comb and type clauses *)
  11.728 +fun build_logic_map mode0 ctxt type_lits cls thss =
  11.729 +  let val thy = ProofContext.theory_of ctxt
  11.730 +      (*The modes FO and FT are sticky. HO can be downgraded to FO.*)
  11.731 +      fun set_mode FO = FO
  11.732 +        | set_mode HO =
  11.733 +          if forall (forall (is_quasi_fol_clause thy)) (cls :: thss) then FO
  11.734 +          else HO
  11.735 +        | set_mode FT = FT
  11.736 +      val mode = set_mode mode0
  11.737 +      (*transform isabelle clause to metis clause *)
  11.738 +      fun add_thm th_no is_conjecture (metis_ith, isa_ith)
  11.739 +                  {axioms, tfrees, old_skolems} : logic_map =
  11.740 +        let
  11.741 +          val (mth, tfree_lits, old_skolems) =
  11.742 +            hol_thm_to_fol is_conjecture th_no ctxt type_lits mode (length axioms)
  11.743 +                           old_skolems metis_ith
  11.744 +        in
  11.745 +           {axioms = (mth, Meson.make_meta_clause isa_ith) :: axioms,
  11.746 +            tfrees = union (op =) tfree_lits tfrees, old_skolems = old_skolems}
  11.747 +        end;
  11.748 +      val lmap = {axioms = [], tfrees = init_tfrees ctxt, old_skolems = []}
  11.749 +                 |> fold (add_thm 0 true o `I) cls
  11.750 +                 |> add_tfrees
  11.751 +                 |> fold (fn (th_no, ths) => fold (add_thm th_no false o `I) ths)
  11.752 +                         (1 upto length thss ~~ thss)
  11.753 +      val clause_lists = map (Metis_Thm.clause o #1) (#axioms lmap)
  11.754 +      fun is_used c =
  11.755 +        exists (Metis_LiteralSet.exists (const_in_metis c o #2)) clause_lists
  11.756 +      val lmap =
  11.757 +        if mode = FO then
  11.758 +          lmap
  11.759 +        else
  11.760 +          let
  11.761 +            val helper_ths =
  11.762 +              helpers |> filter (is_used o fst)
  11.763 +                      |> maps (fn (c, (needs_full_types, thms)) =>
  11.764 +                                  if not (is_used c) orelse
  11.765 +                                     needs_full_types andalso mode <> FT then
  11.766 +                                    []
  11.767 +                                  else
  11.768 +                                    thms)
  11.769 +          in lmap |> fold (add_thm ~1 false) helper_ths end
  11.770 +  in
  11.771 +    (mode, add_type_thm (type_ext thy (maps (map prop_of) (cls :: thss))) lmap)
  11.772 +  end
  11.773 +
  11.774 +end;
    12.1 --- a/src/HOL/Tools/Sledgehammer/metis_reconstruct.ML	Mon Oct 04 22:01:34 2010 +0200
    12.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.3 @@ -1,557 +0,0 @@
    12.4 -(*  Title:      HOL/Tools/Sledgehammer/metis_reconstruct.ML
    12.5 -    Author:     Kong W. Susanto, Cambridge University Computer Laboratory
    12.6 -    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
    12.7 -    Author:     Jasmin Blanchette, TU Muenchen
    12.8 -    Copyright   Cambridge University 2007
    12.9 -
   12.10 -Proof reconstruction for Metis.
   12.11 -*)
   12.12 -
   12.13 -signature METIS_RECONSTRUCT =
   12.14 -sig
   12.15 -  type mode = Metis_Translate.mode
   12.16 -
   12.17 -  val trace : bool Unsynchronized.ref
   12.18 -  val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
   12.19 -  val untyped_aconv : term -> term -> bool
   12.20 -  val replay_one_inference :
   12.21 -    Proof.context -> mode -> (string * term) list
   12.22 -    -> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list
   12.23 -    -> (Metis_Thm.thm * thm) list
   12.24 -end;
   12.25 -
   12.26 -structure Metis_Reconstruct : METIS_RECONSTRUCT =
   12.27 -struct
   12.28 -
   12.29 -open Metis_Translate
   12.30 -
   12.31 -val trace = Unsynchronized.ref false
   12.32 -fun trace_msg msg = if !trace then tracing (msg ()) else ()
   12.33 -
   12.34 -datatype term_or_type = SomeTerm of term | SomeType of typ
   12.35 -
   12.36 -fun terms_of [] = []
   12.37 -  | terms_of (SomeTerm t :: tts) = t :: terms_of tts
   12.38 -  | terms_of (SomeType _ :: tts) = terms_of tts;
   12.39 -
   12.40 -fun types_of [] = []
   12.41 -  | types_of (SomeTerm (Var ((a,idx), _)) :: tts) =
   12.42 -      if String.isPrefix "_" a then
   12.43 -          (*Variable generated by Metis, which might have been a type variable.*)
   12.44 -          TVar (("'" ^ a, idx), HOLogic.typeS) :: types_of tts
   12.45 -      else types_of tts
   12.46 -  | types_of (SomeTerm _ :: tts) = types_of tts
   12.47 -  | types_of (SomeType T :: tts) = T :: types_of tts;
   12.48 -
   12.49 -fun apply_list rator nargs rands =
   12.50 -  let val trands = terms_of rands
   12.51 -  in  if length trands = nargs then SomeTerm (list_comb(rator, trands))
   12.52 -      else raise Fail
   12.53 -        ("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global Pure.thy rator ^
   12.54 -          " expected " ^ Int.toString nargs ^
   12.55 -          " received " ^ commas (map (Syntax.string_of_term_global Pure.thy) trands))
   12.56 -  end;
   12.57 -
   12.58 -fun infer_types ctxt =
   12.59 -  Syntax.check_terms (ProofContext.set_mode ProofContext.mode_pattern ctxt);
   12.60 -
   12.61 -(*We use 1 rather than 0 because variable references in clauses may otherwise conflict
   12.62 -  with variable constraints in the goal...at least, type inference often fails otherwise.
   12.63 -  SEE ALSO axiom_inf below.*)
   12.64 -fun mk_var (w, T) = Var ((w, 1), T)
   12.65 -
   12.66 -(*include the default sort, if available*)
   12.67 -fun mk_tfree ctxt w =
   12.68 -  let val ww = "'" ^ w
   12.69 -  in  TFree(ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1)))  end;
   12.70 -
   12.71 -(*Remove the "apply" operator from an HO term*)
   12.72 -fun strip_happ args (Metis_Term.Fn(".",[t,u])) = strip_happ (u::args) t
   12.73 -  | strip_happ args x = (x, args);
   12.74 -
   12.75 -fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS)
   12.76 -
   12.77 -fun smart_invert_const "fequal" = @{const_name HOL.eq}
   12.78 -  | smart_invert_const s = invert_const s
   12.79 -
   12.80 -fun hol_type_from_metis_term _ (Metis_Term.Var v) =
   12.81 -     (case strip_prefix_and_unascii tvar_prefix v of
   12.82 -          SOME w => make_tvar w
   12.83 -        | NONE   => make_tvar v)
   12.84 -  | hol_type_from_metis_term ctxt (Metis_Term.Fn(x, tys)) =
   12.85 -     (case strip_prefix_and_unascii type_const_prefix x of
   12.86 -          SOME tc => Type (smart_invert_const tc,
   12.87 -                           map (hol_type_from_metis_term ctxt) tys)
   12.88 -        | NONE    =>
   12.89 -      case strip_prefix_and_unascii tfree_prefix x of
   12.90 -          SOME tf => mk_tfree ctxt tf
   12.91 -        | NONE    => raise Fail ("hol_type_from_metis_term: " ^ x));
   12.92 -
   12.93 -(*Maps metis terms to isabelle terms*)
   12.94 -fun hol_term_from_metis_PT ctxt fol_tm =
   12.95 -  let val thy = ProofContext.theory_of ctxt
   12.96 -      val _ = trace_msg (fn () => "hol_term_from_metis_PT: " ^
   12.97 -                                  Metis_Term.toString fol_tm)
   12.98 -      fun tm_to_tt (Metis_Term.Var v) =
   12.99 -             (case strip_prefix_and_unascii tvar_prefix v of
  12.100 -                  SOME w => SomeType (make_tvar w)
  12.101 -                | NONE =>
  12.102 -              case strip_prefix_and_unascii schematic_var_prefix v of
  12.103 -                  SOME w => SomeTerm (mk_var (w, HOLogic.typeT))
  12.104 -                | NONE   => SomeTerm (mk_var (v, HOLogic.typeT)) )
  12.105 -                    (*Var from Metis with a name like _nnn; possibly a type variable*)
  12.106 -        | tm_to_tt (Metis_Term.Fn ("{}", [arg])) = tm_to_tt arg   (*hBOOL*)
  12.107 -        | tm_to_tt (t as Metis_Term.Fn (".",_)) =
  12.108 -            let val (rator,rands) = strip_happ [] t
  12.109 -            in  case rator of
  12.110 -                    Metis_Term.Fn(fname,ts) => applic_to_tt (fname, ts @ rands)
  12.111 -                  | _ => case tm_to_tt rator of
  12.112 -                             SomeTerm t => SomeTerm (list_comb(t, terms_of (map tm_to_tt rands)))
  12.113 -                           | _ => raise Fail "tm_to_tt: HO application"
  12.114 -            end
  12.115 -        | tm_to_tt (Metis_Term.Fn (fname, args)) = applic_to_tt (fname,args)
  12.116 -      and applic_to_tt ("=",ts) =
  12.117 -            SomeTerm (list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
  12.118 -        | applic_to_tt (a,ts) =
  12.119 -            case strip_prefix_and_unascii const_prefix a of
  12.120 -                SOME b =>
  12.121 -                  let
  12.122 -                    val c = smart_invert_const b
  12.123 -                    val ntypes = num_type_args thy c
  12.124 -                    val nterms = length ts - ntypes
  12.125 -                    val tts = map tm_to_tt ts
  12.126 -                    val tys = types_of (List.take(tts,ntypes))
  12.127 -                    val t =
  12.128 -                      if String.isPrefix new_skolem_const_prefix c then
  12.129 -                        Var (new_skolem_var_from_const c,
  12.130 -                             Type_Infer.paramify_vars (tl tys ---> hd tys))
  12.131 -                      else
  12.132 -                        Const (c, dummyT)
  12.133 -                  in if length tys = ntypes then
  12.134 -                         apply_list t nterms (List.drop(tts,ntypes))
  12.135 -                     else
  12.136 -                       raise Fail ("Constant " ^ c ^ " expects " ^ Int.toString ntypes ^
  12.137 -                                   " but gets " ^ Int.toString (length tys) ^
  12.138 -                                   " type arguments\n" ^
  12.139 -                                   cat_lines (map (Syntax.string_of_typ ctxt) tys) ^
  12.140 -                                   " the terms are \n" ^
  12.141 -                                   cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
  12.142 -                     end
  12.143 -              | NONE => (*Not a constant. Is it a type constructor?*)
  12.144 -            case strip_prefix_and_unascii type_const_prefix a of
  12.145 -                SOME b =>
  12.146 -                SomeType (Type (smart_invert_const b, types_of (map tm_to_tt ts)))
  12.147 -              | NONE => (*Maybe a TFree. Should then check that ts=[].*)
  12.148 -            case strip_prefix_and_unascii tfree_prefix a of
  12.149 -                SOME b => SomeType (mk_tfree ctxt b)
  12.150 -              | NONE => (*a fixed variable? They are Skolem functions.*)
  12.151 -            case strip_prefix_and_unascii fixed_var_prefix a of
  12.152 -                SOME b =>
  12.153 -                  let val opr = Free (b, HOLogic.typeT)
  12.154 -                  in  apply_list opr (length ts) (map tm_to_tt ts)  end
  12.155 -              | NONE => raise Fail ("unexpected metis function: " ^ a)
  12.156 -  in
  12.157 -    case tm_to_tt fol_tm of
  12.158 -      SomeTerm t => t
  12.159 -    | SomeType T => raise TYPE ("fol_tm_to_tt: Term expected", [T], [])
  12.160 -  end
  12.161 -
  12.162 -(*Maps fully-typed metis terms to isabelle terms*)
  12.163 -fun hol_term_from_metis_FT ctxt fol_tm =
  12.164 -  let val _ = trace_msg (fn () => "hol_term_from_metis_FT: " ^
  12.165 -                                  Metis_Term.toString fol_tm)
  12.166 -      fun cvt (Metis_Term.Fn ("ti", [Metis_Term.Var v, _])) =
  12.167 -             (case strip_prefix_and_unascii schematic_var_prefix v of
  12.168 -                  SOME w =>  mk_var(w, dummyT)
  12.169 -                | NONE   => mk_var(v, dummyT))
  12.170 -        | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn ("=",[]), _])) =
  12.171 -            Const (@{const_name HOL.eq}, HOLogic.typeT)
  12.172 -        | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn (x,[]), ty])) =
  12.173 -           (case strip_prefix_and_unascii const_prefix x of
  12.174 -                SOME c => Const (smart_invert_const c, dummyT)
  12.175 -              | NONE => (*Not a constant. Is it a fixed variable??*)
  12.176 -            case strip_prefix_and_unascii fixed_var_prefix x of
  12.177 -                SOME v => Free (v, hol_type_from_metis_term ctxt ty)
  12.178 -              | NONE => raise Fail ("hol_term_from_metis_FT bad constant: " ^ x))
  12.179 -        | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn (".",[tm1,tm2]), _])) =
  12.180 -            cvt tm1 $ cvt tm2
  12.181 -        | cvt (Metis_Term.Fn (".",[tm1,tm2])) = (*untyped application*)
  12.182 -            cvt tm1 $ cvt tm2
  12.183 -        | cvt (Metis_Term.Fn ("{}", [arg])) = cvt arg   (*hBOOL*)
  12.184 -        | cvt (Metis_Term.Fn ("=", [tm1,tm2])) =
  12.185 -            list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), map cvt [tm1,tm2])
  12.186 -        | cvt (t as Metis_Term.Fn (x, [])) =
  12.187 -           (case strip_prefix_and_unascii const_prefix x of
  12.188 -                SOME c => Const (smart_invert_const c, dummyT)
  12.189 -              | NONE => (*Not a constant. Is it a fixed variable??*)
  12.190 -            case strip_prefix_and_unascii fixed_var_prefix x of
  12.191 -                SOME v => Free (v, dummyT)
  12.192 -              | NONE => (trace_msg (fn () => "hol_term_from_metis_FT bad const: " ^ x);
  12.193 -                  hol_term_from_metis_PT ctxt t))
  12.194 -        | cvt t = (trace_msg (fn () => "hol_term_from_metis_FT bad term: " ^ Metis_Term.toString t);
  12.195 -            hol_term_from_metis_PT ctxt t)
  12.196 -  in fol_tm |> cvt end
  12.197 -
  12.198 -fun hol_term_from_metis FT = hol_term_from_metis_FT
  12.199 -  | hol_term_from_metis _ = hol_term_from_metis_PT
  12.200 -
  12.201 -fun hol_terms_from_fol ctxt mode old_skolems fol_tms =
  12.202 -  let val ts = map (hol_term_from_metis mode ctxt) fol_tms
  12.203 -      val _ = trace_msg (fn () => "  calling type inference:")
  12.204 -      val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts
  12.205 -      val ts' = ts |> map (reveal_old_skolem_terms old_skolems)
  12.206 -                   |> infer_types ctxt
  12.207 -      val _ = app (fn t => trace_msg
  12.208 -                    (fn () => "  final term: " ^ Syntax.string_of_term ctxt t ^
  12.209 -                              "  of type  " ^ Syntax.string_of_typ ctxt (type_of t)))
  12.210 -                  ts'
  12.211 -  in  ts'  end;
  12.212 -
  12.213 -(* ------------------------------------------------------------------------- *)
  12.214 -(* FOL step Inference Rules                                                  *)
  12.215 -(* ------------------------------------------------------------------------- *)
  12.216 -
  12.217 -(*for debugging only*)
  12.218 -(*
  12.219 -fun print_thpair (fth,th) =
  12.220 -  (trace_msg (fn () => "=============================================");
  12.221 -   trace_msg (fn () => "Metis: " ^ Metis_Thm.toString fth);
  12.222 -   trace_msg (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th));
  12.223 -*)
  12.224 -
  12.225 -fun lookth thpairs (fth : Metis_Thm.thm) =
  12.226 -  the (AList.lookup (uncurry Metis_Thm.equal) thpairs fth)
  12.227 -  handle Option.Option =>
  12.228 -         raise Fail ("Failed to find Metis theorem " ^ Metis_Thm.toString fth)
  12.229 -
  12.230 -fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx));
  12.231 -
  12.232 -(* INFERENCE RULE: AXIOM *)
  12.233 -
  12.234 -fun axiom_inf thpairs th = Thm.incr_indexes 1 (lookth thpairs th);
  12.235 -    (*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*)
  12.236 -
  12.237 -(* INFERENCE RULE: ASSUME *)
  12.238 -
  12.239 -val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)}
  12.240 -
  12.241 -fun inst_excluded_middle thy i_atm =
  12.242 -  let val th = EXCLUDED_MIDDLE
  12.243 -      val [vx] = Term.add_vars (prop_of th) []
  12.244 -      val substs = [(cterm_of thy (Var vx), cterm_of thy i_atm)]
  12.245 -  in  cterm_instantiate substs th  end;
  12.246 -
  12.247 -fun assume_inf ctxt mode old_skolems atm =
  12.248 -  inst_excluded_middle
  12.249 -      (ProofContext.theory_of ctxt)
  12.250 -      (singleton (hol_terms_from_fol ctxt mode old_skolems) (Metis_Term.Fn atm))
  12.251 -
  12.252 -(* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying
  12.253 -   to reconstruct them admits new possibilities of errors, e.g. concerning
  12.254 -   sorts. Instead we try to arrange that new TVars are distinct and that types
  12.255 -   can be inferred from terms. *)
  12.256 -
  12.257 -fun inst_inf ctxt mode old_skolems thpairs fsubst th =
  12.258 -  let val thy = ProofContext.theory_of ctxt
  12.259 -      val i_th = lookth thpairs th
  12.260 -      val i_th_vars = Term.add_vars (prop_of i_th) []
  12.261 -      fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars)
  12.262 -      fun subst_translation (x,y) =
  12.263 -        let val v = find_var x
  12.264 -            (* We call "reveal_old_skolem_terms" and "infer_types" below. *)
  12.265 -            val t = hol_term_from_metis mode ctxt y
  12.266 -        in  SOME (cterm_of thy (Var v), t)  end
  12.267 -        handle Option.Option =>
  12.268 -               (trace_msg (fn () => "\"find_var\" failed for " ^ x ^
  12.269 -                                    " in " ^ Display.string_of_thm ctxt i_th);
  12.270 -                NONE)
  12.271 -             | TYPE _ =>
  12.272 -               (trace_msg (fn () => "\"hol_term_from_metis\" failed for " ^ x ^
  12.273 -                                    " in " ^ Display.string_of_thm ctxt i_th);
  12.274 -                NONE)
  12.275 -      fun remove_typeinst (a, t) =
  12.276 -            case strip_prefix_and_unascii schematic_var_prefix a of
  12.277 -                SOME b => SOME (b, t)
  12.278 -              | NONE => case strip_prefix_and_unascii tvar_prefix a of
  12.279 -                SOME _ => NONE          (*type instantiations are forbidden!*)
  12.280 -              | NONE => SOME (a,t)    (*internal Metis var?*)
  12.281 -      val _ = trace_msg (fn () => "  isa th: " ^ Display.string_of_thm ctxt i_th)
  12.282 -      val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst)
  12.283 -      val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs)
  12.284 -      val tms = rawtms |> map (reveal_old_skolem_terms old_skolems)
  12.285 -                       |> infer_types ctxt
  12.286 -      val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
  12.287 -      val substs' = ListPair.zip (vars, map ctm_of tms)
  12.288 -      val _ = trace_msg (fn () =>
  12.289 -        cat_lines ("subst_translations:" ::
  12.290 -          (substs' |> map (fn (x, y) =>
  12.291 -            Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
  12.292 -            Syntax.string_of_term ctxt (term_of y)))));
  12.293 -  in cterm_instantiate substs' i_th end
  12.294 -  handle THM (msg, _, _) =>
  12.295 -         error ("Cannot replay Metis proof in Isabelle:\n" ^ msg)
  12.296 -
  12.297 -(* INFERENCE RULE: RESOLVE *)
  12.298 -
  12.299 -(* Like RSN, but we rename apart only the type variables. Vars here typically
  12.300 -   have an index of 1, and the use of RSN would increase this typically to 3.
  12.301 -   Instantiations of those Vars could then fail. See comment on "mk_var". *)
  12.302 -fun resolve_inc_tyvars thy tha i thb =
  12.303 -  let
  12.304 -    val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
  12.305 -    fun aux tha thb =
  12.306 -      case Thm.bicompose false (false, tha, nprems_of tha) i thb
  12.307 -           |> Seq.list_of |> distinct Thm.eq_thm of
  12.308 -        [th] => th
  12.309 -      | _ => raise THM ("resolve_inc_tyvars: unique result expected", i,
  12.310 -                        [tha, thb])
  12.311 -  in
  12.312 -    aux tha thb
  12.313 -    handle TERM z =>
  12.314 -           (* The unifier, which is invoked from "Thm.bicompose", will sometimes
  12.315 -              refuse to unify "?a::?'a" with "?a::?'b" or "?a::nat" and throw a
  12.316 -              "TERM" exception (with "add_ffpair" as first argument). We then
  12.317 -              perform unification of the types of variables by hand and try
  12.318 -              again. We could do this the first time around but this error
  12.319 -              occurs seldom and we don't want to break existing proofs in subtle
  12.320 -              ways or slow them down needlessly. *)
  12.321 -           case [] |> fold (Term.add_vars o prop_of) [tha, thb]
  12.322 -                   |> AList.group (op =)
  12.323 -                   |> maps (fn ((s, _), T :: Ts) =>
  12.324 -                               map (fn T' => (Free (s, T), Free (s, T'))) Ts)
  12.325 -                   |> rpair (Envir.empty ~1)
  12.326 -                   |-> fold (Pattern.unify thy)
  12.327 -                   |> Envir.type_env |> Vartab.dest
  12.328 -                   |> map (fn (x, (S, T)) =>
  12.329 -                              pairself (ctyp_of thy) (TVar (x, S), T)) of
  12.330 -             [] => raise TERM z
  12.331 -           | ps => aux (instantiate (ps, []) tha) (instantiate (ps, []) thb)
  12.332 -  end
  12.333 -
  12.334 -fun mk_not (Const (@{const_name Not}, _) $ b) = b
  12.335 -  | mk_not b = HOLogic.mk_not b
  12.336 -
  12.337 -(* Match untyped terms. *)
  12.338 -fun untyped_aconv (Const (a, _)) (Const(b, _)) = (a = b)
  12.339 -  | untyped_aconv (Free (a, _)) (Free (b, _)) = (a = b)
  12.340 -  | untyped_aconv (Var ((a, _), _)) (Var ((b, _), _)) =
  12.341 -    (a = b) (* The index is ignored, for some reason. *)
  12.342 -  | untyped_aconv (Bound i) (Bound j) = (i = j)
  12.343 -  | untyped_aconv (Abs (_, _, t)) (Abs (_, _, u)) = untyped_aconv t u
  12.344 -  | untyped_aconv (t1 $ t2) (u1 $ u2) =
  12.345 -    untyped_aconv t1 u1 andalso untyped_aconv t2 u2
  12.346 -  | untyped_aconv _ _ = false
  12.347 -
  12.348 -(* Finding the relative location of an untyped term within a list of terms *)
  12.349 -fun literal_index lit =
  12.350 -  let
  12.351 -    val lit = Envir.eta_contract lit
  12.352 -    fun get _ [] = raise Empty
  12.353 -      | get n (x :: xs) =
  12.354 -        if untyped_aconv lit (Envir.eta_contract (HOLogic.dest_Trueprop x)) then
  12.355 -          n
  12.356 -        else
  12.357 -          get (n+1) xs
  12.358 -  in get 1 end
  12.359 -
  12.360 -(* Permute a rule's premises to move the i-th premise to the last position. *)
  12.361 -fun make_last i th =
  12.362 -  let val n = nprems_of th
  12.363 -  in  if 1 <= i andalso i <= n
  12.364 -      then Thm.permute_prems (i-1) 1 th
  12.365 -      else raise THM("select_literal", i, [th])
  12.366 -  end;
  12.367 -
  12.368 -(* Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing
  12.369 -   double-negations. *)
  12.370 -val negate_head = rewrite_rule [@{thm atomize_not}, not_not RS eq_reflection]
  12.371 -
  12.372 -(* Maps the clause  [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *)
  12.373 -val select_literal = negate_head oo make_last
  12.374 -
  12.375 -fun resolve_inf ctxt mode old_skolems thpairs atm th1 th2 =
  12.376 -  let
  12.377 -    val thy = ProofContext.theory_of ctxt
  12.378 -    val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
  12.379 -    val _ = trace_msg (fn () => "  isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
  12.380 -    val _ = trace_msg (fn () => "  isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
  12.381 -  in
  12.382 -    (* Trivial cases where one operand is type info *)
  12.383 -    if Thm.eq_thm (TrueI, i_th1) then
  12.384 -      i_th2
  12.385 -    else if Thm.eq_thm (TrueI, i_th2) then
  12.386 -      i_th1
  12.387 -    else
  12.388 -      let
  12.389 -        val i_atm = singleton (hol_terms_from_fol ctxt mode old_skolems)
  12.390 -                              (Metis_Term.Fn atm)
  12.391 -        val _ = trace_msg (fn () => "  atom: " ^ Syntax.string_of_term ctxt i_atm)
  12.392 -        val prems_th1 = prems_of i_th1
  12.393 -        val prems_th2 = prems_of i_th2
  12.394 -        val index_th1 = literal_index (mk_not i_atm) prems_th1
  12.395 -              handle Empty => raise Fail "Failed to find literal in th1"
  12.396 -        val _ = trace_msg (fn () => "  index_th1: " ^ Int.toString index_th1)
  12.397 -        val index_th2 = literal_index i_atm prems_th2
  12.398 -              handle Empty => raise Fail "Failed to find literal in th2"
  12.399 -        val _ = trace_msg (fn () => "  index_th2: " ^ Int.toString index_th2)
  12.400 -    in
  12.401 -      resolve_inc_tyvars thy (select_literal index_th1 i_th1) index_th2 i_th2
  12.402 -    end
  12.403 -  end;
  12.404 -
  12.405 -(* INFERENCE RULE: REFL *)
  12.406 -
  12.407 -val REFL_THM = Thm.incr_indexes 2 @{lemma "t ~= t ==> False" by simp}
  12.408 -
  12.409 -val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
  12.410 -val refl_idx = 1 + Thm.maxidx_of REFL_THM;
  12.411 -
  12.412 -fun refl_inf ctxt mode old_skolems t =
  12.413 -  let val thy = ProofContext.theory_of ctxt
  12.414 -      val i_t = singleton (hol_terms_from_fol ctxt mode old_skolems) t
  12.415 -      val _ = trace_msg (fn () => "  term: " ^ Syntax.string_of_term ctxt i_t)
  12.416 -      val c_t = cterm_incr_types thy refl_idx i_t
  12.417 -  in  cterm_instantiate [(refl_x, c_t)] REFL_THM  end;
  12.418 -
  12.419 -(* INFERENCE RULE: EQUALITY *)
  12.420 -
  12.421 -val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp}
  12.422 -val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp}
  12.423 -
  12.424 -val metis_eq = Metis_Term.Fn ("=", []);
  12.425 -
  12.426 -fun get_ty_arg_size _ (Const (@{const_name HOL.eq}, _)) = 0  (*equality has no type arguments*)
  12.427 -  | get_ty_arg_size thy (Const (c, _)) = (num_type_args thy c handle TYPE _ => 0)
  12.428 -  | get_ty_arg_size _ _ = 0;
  12.429 -
  12.430 -fun equality_inf ctxt mode old_skolems (pos, atm) fp fr =
  12.431 -  let val thy = ProofContext.theory_of ctxt
  12.432 -      val m_tm = Metis_Term.Fn atm
  12.433 -      val [i_atm,i_tm] = hol_terms_from_fol ctxt mode old_skolems [m_tm, fr]
  12.434 -      val _ = trace_msg (fn () => "sign of the literal: " ^ Bool.toString pos)
  12.435 -      fun replace_item_list lx 0 (_::ls) = lx::ls
  12.436 -        | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
  12.437 -      fun path_finder_FO tm [] = (tm, Bound 0)
  12.438 -        | path_finder_FO tm (p::ps) =
  12.439 -            let val (tm1,args) = strip_comb tm
  12.440 -                val adjustment = get_ty_arg_size thy tm1
  12.441 -                val p' = if adjustment > p then p else p-adjustment
  12.442 -                val tm_p = List.nth(args,p')
  12.443 -                  handle Subscript =>
  12.444 -                         error ("Cannot replay Metis proof in Isabelle:\n" ^
  12.445 -                                "equality_inf: " ^ Int.toString p ^ " adj " ^
  12.446 -                                Int.toString adjustment ^ " term " ^
  12.447 -                                Syntax.string_of_term ctxt tm)
  12.448 -                val _ = trace_msg (fn () => "path_finder: " ^ Int.toString p ^
  12.449 -                                      "  " ^ Syntax.string_of_term ctxt tm_p)
  12.450 -                val (r,t) = path_finder_FO tm_p ps
  12.451 -            in
  12.452 -                (r, list_comb (tm1, replace_item_list t p' args))
  12.453 -            end
  12.454 -      fun path_finder_HO tm [] = (tm, Bound 0)
  12.455 -        | path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps)
  12.456 -        | path_finder_HO (t$u) (_::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps)
  12.457 -        | path_finder_HO tm ps =
  12.458 -          raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^
  12.459 -                      "equality_inf, path_finder_HO: path = " ^
  12.460 -                      space_implode " " (map Int.toString ps) ^
  12.461 -                      " isa-term: " ^  Syntax.string_of_term ctxt tm)
  12.462 -      fun path_finder_FT tm [] _ = (tm, Bound 0)
  12.463 -        | path_finder_FT tm (0::ps) (Metis_Term.Fn ("ti", [t1, _])) =
  12.464 -            path_finder_FT tm ps t1
  12.465 -        | path_finder_FT (t$u) (0::ps) (Metis_Term.Fn (".", [t1, _])) =
  12.466 -            (fn(x,y) => (x, y$u)) (path_finder_FT t ps t1)
  12.467 -        | path_finder_FT (t$u) (1::ps) (Metis_Term.Fn (".", [_, t2])) =
  12.468 -            (fn(x,y) => (x, t$y)) (path_finder_FT u ps t2)
  12.469 -        | path_finder_FT tm ps t =
  12.470 -          raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^
  12.471 -                      "equality_inf, path_finder_FT: path = " ^
  12.472 -                      space_implode " " (map Int.toString ps) ^
  12.473 -                      " isa-term: " ^  Syntax.string_of_term ctxt tm ^
  12.474 -                      " fol-term: " ^ Metis_Term.toString t)
  12.475 -      fun path_finder FO tm ps _ = path_finder_FO tm ps
  12.476 -        | path_finder HO (tm as Const(@{const_name HOL.eq},_) $ _ $ _) (p::ps) _ =
  12.477 -             (*equality: not curried, as other predicates are*)
  12.478 -             if p=0 then path_finder_HO tm (0::1::ps)  (*select first operand*)
  12.479 -             else path_finder_HO tm (p::ps)        (*1 selects second operand*)
  12.480 -        | path_finder HO tm (_ :: ps) (Metis_Term.Fn ("{}", [_])) =
  12.481 -             path_finder_HO tm ps      (*if not equality, ignore head to skip hBOOL*)
  12.482 -        | path_finder FT (tm as Const(@{const_name HOL.eq}, _) $ _ $ _) (p::ps)
  12.483 -                            (Metis_Term.Fn ("=", [t1,t2])) =
  12.484 -             (*equality: not curried, as other predicates are*)
  12.485 -             if p=0 then path_finder_FT tm (0::1::ps)
  12.486 -                          (Metis_Term.Fn (".", [Metis_Term.Fn (".", [metis_eq,t1]), t2]))
  12.487 -                          (*select first operand*)
  12.488 -             else path_finder_FT tm (p::ps)
  12.489 -                   (Metis_Term.Fn (".", [metis_eq,t2]))
  12.490 -                   (*1 selects second operand*)
  12.491 -        | path_finder FT tm (_ :: ps) (Metis_Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1
  12.492 -             (*if not equality, ignore head to skip the hBOOL predicate*)
  12.493 -        | path_finder FT tm ps t = path_finder_FT tm ps t  (*really an error case!*)
  12.494 -      fun path_finder_lit ((nt as Const (@{const_name Not}, _)) $ tm_a) idx =
  12.495 -            let val (tm, tm_rslt) = path_finder mode tm_a idx m_tm
  12.496 -            in (tm, nt $ tm_rslt) end
  12.497 -        | path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm
  12.498 -      val (tm_subst, body) = path_finder_lit i_atm fp
  12.499 -      val tm_abs = Abs ("x", type_of tm_subst, body)
  12.500 -      val _ = trace_msg (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
  12.501 -      val _ = trace_msg (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
  12.502 -      val _ = trace_msg (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
  12.503 -      val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst)  (*ill typed but gives right max*)
  12.504 -      val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
  12.505 -      val _ = trace_msg (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
  12.506 -      val eq_terms = map (pairself (cterm_of thy))
  12.507 -        (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
  12.508 -  in  cterm_instantiate eq_terms subst'  end;
  12.509 -
  12.510 -val factor = Seq.hd o distinct_subgoals_tac;
  12.511 -
  12.512 -fun step ctxt mode old_skolems thpairs p =
  12.513 -  case p of
  12.514 -    (fol_th, Metis_Proof.Axiom _) => factor (axiom_inf thpairs fol_th)
  12.515 -  | (_, Metis_Proof.Assume f_atm) => assume_inf ctxt mode old_skolems f_atm
  12.516 -  | (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) =>
  12.517 -    factor (inst_inf ctxt mode old_skolems thpairs f_subst f_th1)
  12.518 -  | (_, Metis_Proof.Resolve(f_atm, f_th1, f_th2)) =>
  12.519 -    factor (resolve_inf ctxt mode old_skolems thpairs f_atm f_th1 f_th2)
  12.520 -  | (_, Metis_Proof.Refl f_tm) => refl_inf ctxt mode old_skolems f_tm
  12.521 -  | (_, Metis_Proof.Equality (f_lit, f_p, f_r)) =>
  12.522 -    equality_inf ctxt mode old_skolems f_lit f_p f_r
  12.523 -
  12.524 -fun flexflex_first_order th =
  12.525 -  case Thm.tpairs_of th of
  12.526 -      [] => th
  12.527 -    | pairs =>
  12.528 -        let val thy = theory_of_thm th
  12.529 -            val (_, tenv) =
  12.530 -              fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
  12.531 -            val t_pairs = map Meson.term_pair_of (Vartab.dest tenv)
  12.532 -            val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th
  12.533 -        in  th'  end
  12.534 -        handle THM _ => th;
  12.535 -
  12.536 -fun is_metis_literal_genuine (_, (s, _)) = not (String.isPrefix class_prefix s)
  12.537 -fun is_isabelle_literal_genuine t =
  12.538 -  case t of _ $ (Const (@{const_name skolem}, _) $ _) => false | _ => true
  12.539 -
  12.540 -fun count p xs = fold (fn x => if p x then Integer.add 1 else I) xs 0
  12.541 -
  12.542 -fun replay_one_inference ctxt mode old_skolems (fol_th, inf) thpairs =
  12.543 -  let
  12.544 -    val _ = trace_msg (fn () => "=============================================")
  12.545 -    val _ = trace_msg (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)
  12.546 -    val _ = trace_msg (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)
  12.547 -    val th = step ctxt mode old_skolems thpairs (fol_th, inf)
  12.548 -             |> flexflex_first_order
  12.549 -    val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
  12.550 -    val _ = trace_msg (fn () => "=============================================")
  12.551 -    val num_metis_lits =
  12.552 -      fol_th |> Metis_Thm.clause |> Metis_LiteralSet.toList
  12.553 -             |> count is_metis_literal_genuine
  12.554 -    val num_isabelle_lits =
  12.555 -      th |> prems_of |> count is_isabelle_literal_genuine
  12.556 -    val _ = if num_metis_lits = num_isabelle_lits then ()
  12.557 -            else error "Cannot replay Metis proof in Isabelle: Out of sync."
  12.558 -  in (fol_th, th) :: thpairs end
  12.559 -
  12.560 -end;
    13.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon Oct 04 22:01:34 2010 +0200
    13.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.3 @@ -1,449 +0,0 @@
    13.4 -(*  Title:      HOL/Tools/Sledgehammer/metis_tactics.ML
    13.5 -    Author:     Kong W. Susanto, Cambridge University Computer Laboratory
    13.6 -    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
    13.7 -    Author:     Jasmin Blanchette, TU Muenchen
    13.8 -    Copyright   Cambridge University 2007
    13.9 -
   13.10 -HOL setup for the Metis prover.
   13.11 -*)
   13.12 -
   13.13 -signature METIS_TACTICS =
   13.14 -sig
   13.15 -  val trace : bool Unsynchronized.ref
   13.16 -  val type_lits : bool Config.T
   13.17 -  val new_skolemizer : bool Config.T
   13.18 -  val metis_tac : Proof.context -> thm list -> int -> tactic
   13.19 -  val metisF_tac : Proof.context -> thm list -> int -> tactic
   13.20 -  val metisFT_tac : Proof.context -> thm list -> int -> tactic
   13.21 -  val setup : theory -> theory
   13.22 -end
   13.23 -
   13.24 -structure Metis_Tactics : METIS_TACTICS =
   13.25 -struct
   13.26 -
   13.27 -open Metis_Translate
   13.28 -open Metis_Reconstruct
   13.29 -
   13.30 -structure Int_Pair_Graph =
   13.31 -  Graph(type key = int * int val ord = prod_ord int_ord int_ord)
   13.32 -
   13.33 -fun trace_msg msg = if !trace then tracing (msg ()) else ()
   13.34 -
   13.35 -val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" (K true)
   13.36 -val (new_skolemizer, new_skolemizer_setup) =
   13.37 -  Attrib.config_bool "metis_new_skolemizer" (K false)
   13.38 -
   13.39 -fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const);
   13.40 -
   13.41 -fun have_common_thm ths1 ths2 =
   13.42 -  exists (member Thm.eq_thm ths1) (map Meson.make_meta_clause ths2)
   13.43 -
   13.44 -(*Determining which axiom clauses are actually used*)
   13.45 -fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th)
   13.46 -  | used_axioms _ _ = NONE;
   13.47 -
   13.48 -val clause_params =
   13.49 -  {ordering = Metis_KnuthBendixOrder.default,
   13.50 -   orderLiterals = Metis_Clause.UnsignedLiteralOrder,
   13.51 -   orderTerms = true}
   13.52 -val active_params =
   13.53 -  {clause = clause_params,
   13.54 -   prefactor = #prefactor Metis_Active.default,
   13.55 -   postfactor = #postfactor Metis_Active.default}
   13.56 -val waiting_params =
   13.57 -  {symbolsWeight = 1.0,
   13.58 -   variablesWeight = 0.0,
   13.59 -   literalsWeight = 0.0,
   13.60 -   models = []}
   13.61 -val resolution_params = {active = active_params, waiting = waiting_params}
   13.62 -
   13.63 -fun instantiate_theorem thy inst th =
   13.64 -  let
   13.65 -    val tyenv = Vartab.empty |> fold (Type.raw_unify o pairself fastype_of) inst
   13.66 -    val instT =
   13.67 -      [] |> Vartab.fold (fn (z, (S, T)) =>
   13.68 -                            cons (TVar (z, S), Type.devar tyenv T)) tyenv
   13.69 -    val inst = inst |> map (pairself (subst_atomic_types instT))
   13.70 -    val _ = tracing (cat_lines (map (fn (T, U) =>
   13.71 -        Syntax.string_of_typ @{context} T ^ " |-> " ^
   13.72 -        Syntax.string_of_typ @{context} U) instT))
   13.73 -    val _ = tracing (cat_lines (map (fn (t, u) =>
   13.74 -        Syntax.string_of_term @{context} t ^ " |-> " ^
   13.75 -        Syntax.string_of_term @{context} u) inst))
   13.76 -    val cinstT = instT |> map (pairself (ctyp_of thy))
   13.77 -    val cinst = inst |> map (pairself (cterm_of thy))
   13.78 -  in th |> Thm.instantiate (cinstT, cinst) end
   13.79 -
   13.80 -(* In principle, it should be sufficient to apply "assume_tac" to unify the
   13.81 -   conclusion with one of the premises. However, in practice, this is unreliable
   13.82 -   because of the mildly higher-order nature of the unification problems.
   13.83 -   Typical constraints are of the form
   13.84 -   "?SK_a_b_c_x SK_d_e_f_y ... SK_a_b_c_x ... SK_g_h_i_z =?= SK_a_b_c_x",
   13.85 -   where the nonvariables are goal parameters. *)
   13.86 -fun unify_first_prem_with_concl thy i th =
   13.87 -  let
   13.88 -    val goal = Logic.get_goal (prop_of th) i |> Envir.beta_eta_contract
   13.89 -    val prem = goal |> Logic.strip_assums_hyp |> hd
   13.90 -    val concl = goal |> Logic.strip_assums_concl
   13.91 -    fun pair_untyped_aconv (t1, t2) (u1, u2) =
   13.92 -      untyped_aconv t1 u1 andalso untyped_aconv t2 u2
   13.93 -    fun add_terms tp inst =
   13.94 -      if exists (pair_untyped_aconv tp) inst then inst
   13.95 -      else tp :: map (apsnd (subst_atomic [tp])) inst
   13.96 -    fun is_flex t =
   13.97 -      case strip_comb t of
   13.98 -        (Var _, args) => forall is_Bound args
   13.99 -      | _ => false
  13.100 -    fun unify_flex flex rigid =
  13.101 -      case strip_comb flex of
  13.102 -        (Var (z as (_, T)), args) =>
  13.103 -        add_terms (Var z,
  13.104 -          fold_rev (curry absdummy) (take (length args) (binder_types T)) rigid)
  13.105 -      | _ => raise TERM ("unify_flex: expected flex", [flex])
  13.106 -    fun unify_potential_flex comb atom =
  13.107 -      if is_flex comb then unify_flex comb atom
  13.108 -      else if is_Var atom then add_terms (atom, comb)
  13.109 -      else raise TERM ("unify_terms", [comb, atom])
  13.110 -    fun unify_terms (t, u) =
  13.111 -      case (t, u) of
  13.112 -        (t1 $ t2, u1 $ u2) =>
  13.113 -        if is_flex t then unify_flex t u
  13.114 -        else if is_flex u then unify_flex u t
  13.115 -        else fold unify_terms [(t1, u1), (t2, u2)]
  13.116 -      | (_ $ _, _) => unify_potential_flex t u
  13.117 -      | (_, _ $ _) => unify_potential_flex u t
  13.118 -      | (Var _, _) => add_terms (t, u)
  13.119 -      | (_, Var _) => add_terms (u, t)
  13.120 -      | _ => if untyped_aconv t u then I else raise TERM ("unify_terms", [t, u])
  13.121 -  in th |> instantiate_theorem thy (unify_terms (prem, concl) []) end
  13.122 -
  13.123 -fun shuffle_key (((axiom_no, (_, index_no)), _), _) = (index_no, axiom_no)
  13.124 -fun shuffle_ord p =
  13.125 -  rev_order (prod_ord int_ord int_ord (pairself shuffle_key p))
  13.126 -
  13.127 -val copy_prem = @{lemma "P ==> (P ==> P ==> Q) ==> Q" by fast}
  13.128 -
  13.129 -fun copy_prems_tac [] ns i =
  13.130 -    if forall (curry (op =) 1) ns then all_tac else copy_prems_tac (rev ns) [] i
  13.131 -  | copy_prems_tac (1 :: ms) ns i =
  13.132 -    rotate_tac 1 i THEN copy_prems_tac ms (1 :: ns) i
  13.133 -  | copy_prems_tac (m :: ms) ns i =
  13.134 -    etac copy_prem i THEN copy_prems_tac ms (m div 2 :: (m + 1) div 2 :: ns) i
  13.135 -
  13.136 -fun instantiate_forall_tac thy params t i =
  13.137 -  let
  13.138 -    fun repair (t as (Var ((s, _), _))) =
  13.139 -        (case find_index (fn ((s', _), _) => s' = s) params of
  13.140 -           ~1 => t
  13.141 -         | j => Bound j)
  13.142 -      | repair (t $ u) = repair t $ repair u
  13.143 -      | repair t = t
  13.144 -    val t' = t |> repair |> fold (curry absdummy) (map snd params)
  13.145 -    fun do_instantiate th =
  13.146 -      let val var = Term.add_vars (prop_of th) [] |> the_single in
  13.147 -        th |> instantiate_theorem thy [(Var var, t')]
  13.148 -      end
  13.149 -  in
  13.150 -    etac @{thm allE} i
  13.151 -    THEN rotate_tac ~1 i
  13.152 -    THEN PRIMITIVE do_instantiate
  13.153 -  end
  13.154 -
  13.155 -fun release_clusters_tac _ _ _ _ [] = K all_tac
  13.156 -  | release_clusters_tac thy ax_counts substs params
  13.157 -                         ((ax_no, cluster_no) :: clusters) =
  13.158 -    let
  13.159 -      fun in_right_cluster s =
  13.160 -        (s |> Meson_Clausify.cluster_of_zapped_var_name |> fst |> snd |> fst)
  13.161 -        = cluster_no
  13.162 -      val cluster_substs =
  13.163 -        substs
  13.164 -        |> map_filter (fn (ax_no', (_, (_, tsubst))) =>
  13.165 -                          if ax_no' = ax_no then
  13.166 -                            tsubst |> filter (in_right_cluster
  13.167 -                                               o fst o fst o dest_Var o fst)
  13.168 -                                    |> map snd |> SOME
  13.169 -                           else
  13.170 -                             NONE)
  13.171 -      val n = length cluster_substs
  13.172 -      fun do_cluster_subst cluster_subst =
  13.173 -        map (instantiate_forall_tac thy params) cluster_subst @ [rotate_tac 1]
  13.174 -      val params' = params (* FIXME ### existentials! *)
  13.175 -      val first_prem = find_index (fn (ax_no', _) => ax_no' = ax_no) substs
  13.176 -    in
  13.177 -      rotate_tac first_prem
  13.178 -      THEN' (EVERY' (maps do_cluster_subst cluster_substs))
  13.179 -      THEN' rotate_tac (~ first_prem - length cluster_substs)
  13.180 -      THEN' release_clusters_tac thy ax_counts substs params' clusters
  13.181 -    end
  13.182 -
  13.183 -val cluster_ord =
  13.184 -  prod_ord (prod_ord int_ord (prod_ord int_ord int_ord)) bool_ord
  13.185 -
  13.186 -val tysubst_ord =
  13.187 -  list_ord (prod_ord Term_Ord.fast_indexname_ord
  13.188 -                     (prod_ord Term_Ord.sort_ord Term_Ord.typ_ord))
  13.189 -
  13.190 -structure Int_Tysubst_Table =
  13.191 -  Table(type key = int * (indexname * (sort * typ)) list
  13.192 -        val ord = prod_ord int_ord tysubst_ord)
  13.193 -
  13.194 -(* Attempts to derive the theorem "False" from a theorem of the form
  13.195 -   "P1 ==> ... ==> Pn ==> False", where the "Pi"s are to be discharged using the
  13.196 -   specified axioms. The axioms have leading "All" and "Ex" quantifiers, which
  13.197 -   must be eliminated first. *)
  13.198 -fun discharge_skolem_premises ctxt axioms prems_imp_false =
  13.199 -  if prop_of prems_imp_false aconv @{prop False} then
  13.200 -    prems_imp_false
  13.201 -  else
  13.202 -    let
  13.203 -      val thy = ProofContext.theory_of ctxt
  13.204 -      (* distinguish variables with same name but different types *)
  13.205 -      val prems_imp_false' =
  13.206 -        prems_imp_false |> try (forall_intr_vars #> gen_all)
  13.207 -                        |> the_default prems_imp_false
  13.208 -      val prems_imp_false =
  13.209 -        if prop_of prems_imp_false aconv prop_of prems_imp_false' then
  13.210 -          prems_imp_false
  13.211 -        else
  13.212 -          prems_imp_false'
  13.213 -      fun match_term p =
  13.214 -        let
  13.215 -          val (tyenv, tenv) =
  13.216 -            Pattern.first_order_match thy p (Vartab.empty, Vartab.empty)
  13.217 -          val tsubst =
  13.218 -            tenv |> Vartab.dest
  13.219 -                 |> sort (cluster_ord
  13.220 -                          o pairself (Meson_Clausify.cluster_of_zapped_var_name
  13.221 -                                      o fst o fst))
  13.222 -                 |> map (Meson.term_pair_of
  13.223 -                         #> pairself (Envir.subst_term_types tyenv))
  13.224 -          val tysubst = tyenv |> Vartab.dest
  13.225 -        in (tysubst, tsubst) end
  13.226 -      fun subst_info_for_prem subgoal_no prem =
  13.227 -        case prem of
  13.228 -          _ $ (Const (@{const_name skolem}, _) $ (_ $ t $ num)) =>
  13.229 -          let val ax_no = HOLogic.dest_nat num in
  13.230 -            (ax_no, (subgoal_no,
  13.231 -                     match_term (nth axioms ax_no |> the |> snd, t)))
  13.232 -          end
  13.233 -        | _ => raise TERM ("discharge_skolem_premises: Malformed premise",
  13.234 -                           [prem])
  13.235 -      fun cluster_of_var_name skolem s =
  13.236 -        let
  13.237 -          val ((ax_no, (cluster_no, _)), skolem') =
  13.238 -            Meson_Clausify.cluster_of_zapped_var_name s
  13.239 -        in
  13.240 -          if skolem' = skolem andalso cluster_no > 0 then
  13.241 -            SOME (ax_no, cluster_no)
  13.242 -          else
  13.243 -            NONE
  13.244 -        end
  13.245 -      fun clusters_in_term skolem t =
  13.246 -        Term.add_var_names t [] |> map_filter (cluster_of_var_name skolem o fst)
  13.247 -      fun deps_for_term_subst (var, t) =
  13.248 -        case clusters_in_term false var of
  13.249 -          [] => NONE
  13.250 -        | [(ax_no, cluster_no)] =>
  13.251 -          SOME ((ax_no, cluster_no),
  13.252 -                clusters_in_term true t
  13.253 -                |> cluster_no > 1 ? cons (ax_no, cluster_no - 1))
  13.254 -        | _ => raise TERM ("discharge_skolem_premises: Expected Var", [var])
  13.255 -      val prems = Logic.strip_imp_prems (prop_of prems_imp_false)
  13.256 -      val substs = prems |> map2 subst_info_for_prem (1 upto length prems)
  13.257 -                         |> sort (int_ord o pairself fst)
  13.258 -      val depss = maps (map_filter deps_for_term_subst o snd o snd o snd) substs
  13.259 -      val clusters = maps (op ::) depss
  13.260 -      val ordered_clusters =
  13.261 -        Int_Pair_Graph.empty
  13.262 -        |> fold Int_Pair_Graph.default_node (map (rpair ()) clusters)
  13.263 -        |> fold Int_Pair_Graph.add_deps_acyclic depss
  13.264 -        |> Int_Pair_Graph.topological_order
  13.265 -        handle Int_Pair_Graph.CYCLES _ =>
  13.266 -               error "Cannot replay Metis proof in Isabelle without axiom of \
  13.267 -                     \choice."
  13.268 -      val params0 =
  13.269 -        [] |> fold (Term.add_vars o snd) (map_filter I axioms)
  13.270 -           |> map (`(Meson_Clausify.cluster_of_zapped_var_name o fst o fst))
  13.271 -           |> filter (fn (((_, (cluster_no, _)), skolem), _) =>
  13.272 -                         cluster_no = 0 andalso skolem)
  13.273 -           |> sort shuffle_ord |> map snd
  13.274 -      val ax_counts =
  13.275 -        Int_Tysubst_Table.empty
  13.276 -        |> fold (fn (ax_no, (_, (tysubst, _))) =>
  13.277 -                    Int_Tysubst_Table.map_default ((ax_no, tysubst), 0)
  13.278 -                                                  (Integer.add 1)) substs
  13.279 -        |> Int_Tysubst_Table.dest
  13.280 -(* for debugging:
  13.281 -      fun string_for_subst_info (ax_no, (subgoal_no, (tysubst, tsubst))) =
  13.282 -        "ax: " ^ string_of_int ax_no ^ "; asm: " ^ string_of_int subgoal_no ^
  13.283 -        "; tysubst: " ^ PolyML.makestring tysubst ^ "; tsubst: {" ^
  13.284 -        commas (map ((fn (s, t) => s ^ " |-> " ^ t)
  13.285 -                     o pairself (Syntax.string_of_term ctxt)) tsubst) ^ "}"
  13.286 -      val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^
  13.287 -                       cat_lines (map string_for_subst_info substs))
  13.288 -      val _ = tracing ("OUTERMOST SKOLEMS: " ^ PolyML.makestring params0)
  13.289 -      val _ = tracing ("ORDERED CLUSTERS: " ^ PolyML.makestring ordered_clusters)
  13.290 -      val _ = tracing ("AXIOM COUNTS: " ^ PolyML.makestring ax_counts)
  13.291 -*)
  13.292 -      fun rotation_for_subgoal i =
  13.293 -        find_index (fn (_, (subgoal_no, _)) => subgoal_no = i) substs
  13.294 -    in
  13.295 -      Goal.prove ctxt [] [] @{prop False}
  13.296 -          (K (cut_rules_tac
  13.297 -                  (map (fst o the o nth axioms o fst o fst) ax_counts) 1
  13.298 -              THEN print_tac "cut:"
  13.299 -              THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1)
  13.300 -              THEN copy_prems_tac (map snd ax_counts) [] 1
  13.301 -              THEN print_tac "eliminated exist and copied prems:"
  13.302 -              THEN release_clusters_tac thy ax_counts substs params0
  13.303 -                                        ordered_clusters 1
  13.304 -              THEN print_tac "released clusters:"
  13.305 -              THEN match_tac [prems_imp_false] 1
  13.306 -              THEN print_tac "applied rule:"
  13.307 -              THEN ALLGOALS (fn i =>
  13.308 -                       rtac @{thm skolem_COMBK_I} i
  13.309 -                       THEN rotate_tac (rotation_for_subgoal i) i
  13.310 -                       THEN PRIMITIVE (unify_first_prem_with_concl thy i)
  13.311 -                       THEN assume_tac i)))
  13.312 -    end
  13.313 -
  13.314 -(* Main function to start Metis proof and reconstruction *)
  13.315 -fun FOL_SOLVE mode ctxt cls ths0 =
  13.316 -  let val thy = ProofContext.theory_of ctxt
  13.317 -      val type_lits = Config.get ctxt type_lits
  13.318 -      val new_skolemizer =
  13.319 -        Config.get ctxt new_skolemizer orelse null (Meson_Choices.get ctxt)
  13.320 -      val th_cls_pairs =
  13.321 -        map2 (fn j => fn th =>
  13.322 -                (Thm.get_name_hint th,
  13.323 -                 Meson_Clausify.cnf_axiom ctxt new_skolemizer j th))
  13.324 -             (0 upto length ths0 - 1) ths0
  13.325 -      val thss = map (snd o snd) th_cls_pairs
  13.326 -      val dischargers = map (fst o snd) th_cls_pairs
  13.327 -      val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
  13.328 -      val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
  13.329 -      val _ = trace_msg (fn () => "THEOREM CLAUSES")
  13.330 -      val _ = app (app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th))) thss
  13.331 -      val (mode, {axioms, tfrees, old_skolems}) =
  13.332 -        build_logic_map mode ctxt type_lits cls thss
  13.333 -      val _ = if null tfrees then ()
  13.334 -              else (trace_msg (fn () => "TFREE CLAUSES");
  13.335 -                    app (fn TyLitFree ((s, _), (s', _)) =>
  13.336 -                            trace_msg (fn () => s ^ "(" ^ s' ^ ")")) tfrees)
  13.337 -      val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS")
  13.338 -      val thms = map #1 axioms
  13.339 -      val _ = app (fn th => trace_msg (fn () => Metis_Thm.toString th)) thms
  13.340 -      val _ = trace_msg (fn () => "mode = " ^ string_of_mode mode)
  13.341 -      val _ = trace_msg (fn () => "START METIS PROVE PROCESS")
  13.342 -  in
  13.343 -      case filter (is_false o prop_of) cls of
  13.344 -          false_th::_ => [false_th RS @{thm FalseE}]
  13.345 -        | [] =>
  13.346 -      case Metis_Resolution.new resolution_params {axioms = thms, conjecture = []}
  13.347 -           |> Metis_Resolution.loop of
  13.348 -          Metis_Resolution.Contradiction mth =>
  13.349 -            let val _ = trace_msg (fn () => "METIS RECONSTRUCTION START: " ^
  13.350 -                          Metis_Thm.toString mth)
  13.351 -                val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
  13.352 -                             (*add constraints arising from converting goal to clause form*)
  13.353 -                val proof = Metis_Proof.proof mth
  13.354 -                val result =
  13.355 -                  fold (replay_one_inference ctxt' mode old_skolems) proof axioms
  13.356 -                and used = map_filter (used_axioms axioms) proof
  13.357 -                val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:")
  13.358 -                val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used
  13.359 -                val unused = th_cls_pairs |> map_filter (fn (name, (_, cls)) =>
  13.360 -                  if have_common_thm used cls then NONE else SOME name)
  13.361 -            in
  13.362 -                if not (null cls) andalso not (have_common_thm used cls) then
  13.363 -                  warning "Metis: The assumptions are inconsistent."
  13.364 -                else
  13.365 -                  ();
  13.366 -                if not (null unused) then
  13.367 -                  warning ("Metis: Unused theorems: " ^ commas_quote unused
  13.368 -                           ^ ".")
  13.369 -                else
  13.370 -                  ();
  13.371 -                case result of
  13.372 -                    (_,ith)::_ =>
  13.373 -                        (trace_msg (fn () => "Success: " ^ Display.string_of_thm ctxt ith);
  13.374 -                         [discharge_skolem_premises ctxt dischargers ith])
  13.375 -                  | _ => (trace_msg (fn () => "Metis: No result"); [])
  13.376 -            end
  13.377 -        | Metis_Resolution.Satisfiable _ =>
  13.378 -            (trace_msg (fn () => "Metis: No first-order proof with the lemmas supplied");
  13.379 -             [])
  13.380 -  end;
  13.381 -
  13.382 -(* Extensionalize "th", because that makes sense and that's what Sledgehammer
  13.383 -   does, but also keep an unextensionalized version of "th" for backward
  13.384 -   compatibility. *)
  13.385 -fun also_extensionalize_theorem th =
  13.386 -  let val th' = Meson_Clausify.extensionalize_theorem th in
  13.387 -    if Thm.eq_thm (th, th') then [th]
  13.388 -    else th :: Meson.make_clauses_unsorted [th']
  13.389 -  end
  13.390 -
  13.391 -val neg_clausify =
  13.392 -  single
  13.393 -  #> Meson.make_clauses_unsorted
  13.394 -  #> maps also_extensionalize_theorem
  13.395 -  #> map Meson_Clausify.introduce_combinators_in_theorem
  13.396 -  #> Meson.finish_cnf
  13.397 -
  13.398 -fun preskolem_tac ctxt st0 =
  13.399 -  (if exists (Meson.has_too_many_clauses ctxt)
  13.400 -             (Logic.prems_of_goal (prop_of st0) 1) then
  13.401 -     cnf.cnfx_rewrite_tac ctxt 1
  13.402 -   else
  13.403 -     all_tac) st0
  13.404 -
  13.405 -val type_has_top_sort =
  13.406 -  exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
  13.407 -
  13.408 -fun generic_metis_tac mode ctxt ths i st0 =
  13.409 -  let
  13.410 -    val _ = trace_msg (fn () =>
  13.411 -        "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
  13.412 -  in
  13.413 -    if exists_type type_has_top_sort (prop_of st0) then
  13.414 -      (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty)
  13.415 -    else
  13.416 -      Meson.MESON (preskolem_tac ctxt) (maps neg_clausify)
  13.417 -                  (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
  13.418 -                  ctxt i st0
  13.419 -  end
  13.420 -
  13.421 -val metis_tac = generic_metis_tac HO
  13.422 -val metisF_tac = generic_metis_tac FO
  13.423 -val metisFT_tac = generic_metis_tac FT
  13.424 -
  13.425 -(* Whenever "X" has schematic type variables, we treat "using X by metis" as
  13.426 -   "by (metis X)", to prevent "Subgoal.FOCUS" from freezing the type variables.
  13.427 -   We don't do it for nonschematic facts "X" because this breaks a few proofs
  13.428 -   (in the rare and subtle case where a proof relied on extensionality not being
  13.429 -   applied) and brings few benefits. *)
  13.430 -val has_tvar =
  13.431 -  exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of
  13.432 -fun method name mode =
  13.433 -  Method.setup name (Attrib.thms >> (fn ths => fn ctxt =>
  13.434 -    METHOD (fn facts =>
  13.435 -               let
  13.436 -                 val (schem_facts, nonschem_facts) =
  13.437 -                   List.partition has_tvar facts
  13.438 -               in
  13.439 -                 HEADGOAL (Method.insert_tac nonschem_facts THEN'
  13.440 -                           CHANGED_PROP
  13.441 -                           o generic_metis_tac mode ctxt (schem_facts @ ths))
  13.442 -               end)))
  13.443 -
  13.444 -val setup =
  13.445 -  type_lits_setup
  13.446 -  #> new_skolemizer_setup
  13.447 -  #> method @{binding metis} HO "Metis for FOL/HOL problems"
  13.448 -  #> method @{binding metisF} FO "Metis for FOL problems"
  13.449 -  #> method @{binding metisFT} FT
  13.450 -            "Metis for FOL/HOL problems with fully-typed translation"
  13.451 -
  13.452 -end;
    14.1 --- a/src/HOL/Tools/Sledgehammer/metis_translate.ML	Mon Oct 04 22:01:34 2010 +0200
    14.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.3 @@ -1,771 +0,0 @@
    14.4 -(*  Title:      HOL/Tools/Sledgehammer/metis_translate.ML
    14.5 -    Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
    14.6 -    Author:     Kong W. Susanto, Cambridge University Computer Laboratory
    14.7 -    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
    14.8 -    Author:     Jasmin Blanchette, TU Muenchen
    14.9 -
   14.10 -Translation of HOL to FOL for Metis.
   14.11 -*)
   14.12 -
   14.13 -signature METIS_TRANSLATE =
   14.14 -sig
   14.15 -  type name = string * string
   14.16 -  datatype type_literal =
   14.17 -    TyLitVar of name * name |
   14.18 -    TyLitFree of name * name
   14.19 -  datatype arLit =
   14.20 -    TConsLit of name * name * name list |
   14.21 -    TVarLit of name * name
   14.22 -  datatype arity_clause =
   14.23 -    ArityClause of {name: string, conclLit: arLit, premLits: arLit list}
   14.24 -  datatype class_rel_clause =
   14.25 -    ClassRelClause of {name: string, subclass: name, superclass: name}
   14.26 -  datatype combtyp =
   14.27 -    CombTVar of name |
   14.28 -    CombTFree of name |
   14.29 -    CombType of name * combtyp list
   14.30 -  datatype combterm =
   14.31 -    CombConst of name * combtyp * combtyp list (* Const and Free *) |
   14.32 -    CombVar of name * combtyp |
   14.33 -    CombApp of combterm * combterm
   14.34 -  datatype fol_literal = FOLLiteral of bool * combterm
   14.35 -
   14.36 -  datatype mode = FO | HO | FT
   14.37 -  type logic_map =
   14.38 -    {axioms: (Metis_Thm.thm * thm) list,
   14.39 -     tfrees: type_literal list,
   14.40 -     old_skolems: (string * term) list}
   14.41 -
   14.42 -  val type_wrapper_name : string
   14.43 -  val bound_var_prefix : string
   14.44 -  val schematic_var_prefix: string
   14.45 -  val fixed_var_prefix: string
   14.46 -  val tvar_prefix: string
   14.47 -  val tfree_prefix: string
   14.48 -  val const_prefix: string
   14.49 -  val type_const_prefix: string
   14.50 -  val class_prefix: string
   14.51 -  val new_skolem_const_prefix : string
   14.52 -  val invert_const: string -> string
   14.53 -  val ascii_of: string -> string
   14.54 -  val unascii_of: string -> string
   14.55 -  val strip_prefix_and_unascii: string -> string -> string option
   14.56 -  val make_bound_var : string -> string
   14.57 -  val make_schematic_var : string * int -> string
   14.58 -  val make_fixed_var : string -> string
   14.59 -  val make_schematic_type_var : string * int -> string
   14.60 -  val make_fixed_type_var : string -> string
   14.61 -  val make_fixed_const : string -> string
   14.62 -  val make_fixed_type_const : string -> string
   14.63 -  val make_type_class : string -> string
   14.64 -  val num_type_args: theory -> string -> int
   14.65 -  val new_skolem_var_from_const: string -> indexname
   14.66 -  val type_literals_for_types : typ list -> type_literal list
   14.67 -  val make_class_rel_clauses :
   14.68 -    theory -> class list -> class list -> class_rel_clause list
   14.69 -  val make_arity_clauses :
   14.70 -    theory -> string list -> class list -> class list * arity_clause list
   14.71 -  val combtyp_of : combterm -> combtyp
   14.72 -  val strip_combterm_comb : combterm -> combterm * combterm list
   14.73 -  val combterm_from_term :
   14.74 -    theory -> int -> (string * typ) list -> term -> combterm * typ list
   14.75 -  val reveal_old_skolem_terms : (string * term) list -> term -> term
   14.76 -  val tfree_classes_of_terms : term list -> string list
   14.77 -  val tvar_classes_of_terms : term list -> string list
   14.78 -  val type_consts_of_terms : theory -> term list -> string list
   14.79 -  val string_of_mode : mode -> string
   14.80 -  val build_logic_map :
   14.81 -    mode -> Proof.context -> bool -> thm list -> thm list list
   14.82 -    -> mode * logic_map
   14.83 -end
   14.84 -
   14.85 -structure Metis_Translate : METIS_TRANSLATE =
   14.86 -struct
   14.87 -
   14.88 -val type_wrapper_name = "ti"
   14.89 -
   14.90 -val bound_var_prefix = "B_"
   14.91 -val schematic_var_prefix = "V_"
   14.92 -val fixed_var_prefix = "v_"
   14.93 -
   14.94 -val tvar_prefix = "T_";
   14.95 -val tfree_prefix = "t_";
   14.96 -
   14.97 -val const_prefix = "c_";
   14.98 -val type_const_prefix = "tc_";
   14.99 -val class_prefix = "class_";
  14.100 -
  14.101 -val skolem_const_prefix = "Sledgehammer" ^ Long_Name.separator ^ "Sko"
  14.102 -val old_skolem_const_prefix = skolem_const_prefix ^ "o"
  14.103 -val new_skolem_const_prefix = skolem_const_prefix ^ "n"
  14.104 -
  14.105 -fun union_all xss = fold (union (op =)) xss []
  14.106 -
  14.107 -(* Readable names for the more common symbolic functions. Do not mess with the
  14.108 -   last nine entries of the table unless you know what you are doing. *)
  14.109 -val const_trans_table =
  14.110 -  Symtab.make [(@{type_name Product_Type.prod}, "prod"),
  14.111 -               (@{type_name Sum_Type.sum}, "sum"),
  14.112 -               (@{const_name HOL.eq}, "equal"),
  14.113 -               (@{const_name HOL.conj}, "and"),
  14.114 -               (@{const_name HOL.disj}, "or"),
  14.115 -               (@{const_name HOL.implies}, "implies"),
  14.116 -               (@{const_name Set.member}, "member"),
  14.117 -               (@{const_name fequal}, "fequal"),
  14.118 -               (@{const_name COMBI}, "COMBI"),
  14.119 -               (@{const_name COMBK}, "COMBK"),
  14.120 -               (@{const_name COMBB}, "COMBB"),
  14.121 -               (@{const_name COMBC}, "COMBC"),
  14.122 -               (@{const_name COMBS}, "COMBS"),
  14.123 -               (@{const_name True}, "True"),
  14.124 -               (@{const_name False}, "False"),
  14.125 -               (@{const_name If}, "If")]
  14.126 -
  14.127 -(* Invert the table of translations between Isabelle and ATPs. *)
  14.128 -val const_trans_table_inv =
  14.129 -  Symtab.update ("fequal", @{const_name HOL.eq})
  14.130 -                (Symtab.make (map swap (Symtab.dest const_trans_table)))
  14.131 -
  14.132 -val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
  14.133 -
  14.134 -(*Escaping of special characters.
  14.135 -  Alphanumeric characters are left unchanged.
  14.136 -  The character _ goes to __
  14.137 -  Characters in the range ASCII space to / go to _A to _P, respectively.
  14.138 -  Other characters go to _nnn where nnn is the decimal ASCII code.*)
  14.139 -val A_minus_space = Char.ord #"A" - Char.ord #" ";
  14.140 -
  14.141 -fun stringN_of_int 0 _ = ""
  14.142 -  | stringN_of_int k n = stringN_of_int (k-1) (n div 10) ^ Int.toString (n mod 10);
  14.143 -
  14.144 -fun ascii_of_c c =
  14.145 -  if Char.isAlphaNum c then String.str c
  14.146 -  else if c = #"_" then "__"
  14.147 -  else if #" " <= c andalso c <= #"/"
  14.148 -       then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space))
  14.149 -  else ("_" ^ stringN_of_int 3 (Char.ord c))  (*fixed width, in case more digits follow*)
  14.150 -
  14.151 -val ascii_of = String.translate ascii_of_c;
  14.152 -
  14.153 -(** Remove ASCII armouring from names in proof files **)
  14.154 -
  14.155 -(*We don't raise error exceptions because this code can run inside the watcher.
  14.156 -  Also, the errors are "impossible" (hah!)*)
  14.157 -fun unascii_aux rcs [] = String.implode(rev rcs)
  14.158 -  | unascii_aux rcs [#"_"] = unascii_aux (#"_"::rcs) []  (*ERROR*)
  14.159 -      (*Three types of _ escapes: __, _A to _P, _nnn*)
  14.160 -  | unascii_aux rcs (#"_" :: #"_" :: cs) = unascii_aux (#"_"::rcs) cs
  14.161 -  | unascii_aux rcs (#"_" :: c :: cs) =
  14.162 -      if #"A" <= c andalso c<= #"P"  (*translation of #" " to #"/"*)
  14.163 -      then unascii_aux (Char.chr(Char.ord c - A_minus_space) :: rcs) cs
  14.164 -      else
  14.165 -        let val digits = List.take (c::cs, 3) handle Subscript => []
  14.166 -        in
  14.167 -            case Int.fromString (String.implode digits) of
  14.168 -                NONE => unascii_aux (c:: #"_"::rcs) cs  (*ERROR*)
  14.169 -              | SOME n => unascii_aux (Char.chr n :: rcs) (List.drop (cs, 2))
  14.170 -        end
  14.171 -  | unascii_aux rcs (c::cs) = unascii_aux (c::rcs) cs
  14.172 -val unascii_of = unascii_aux [] o String.explode
  14.173 -
  14.174 -(* If string s has the prefix s1, return the result of deleting it,
  14.175 -   un-ASCII'd. *)
  14.176 -fun strip_prefix_and_unascii s1 s =
  14.177 -  if String.isPrefix s1 s then
  14.178 -    SOME (unascii_of (String.extract (s, size s1, NONE)))
  14.179 -  else
  14.180 -    NONE
  14.181 -
  14.182 -(*Remove the initial ' character from a type variable, if it is present*)
  14.183 -fun trim_type_var s =
  14.184 -  if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE)
  14.185 -  else error ("trim_type: Malformed type variable encountered: " ^ s);
  14.186 -
  14.187 -fun ascii_of_indexname (v,0) = ascii_of v
  14.188 -  | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ Int.toString i;
  14.189 -
  14.190 -fun make_bound_var x = bound_var_prefix ^ ascii_of x
  14.191 -fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v
  14.192 -fun make_fixed_var x = fixed_var_prefix ^ ascii_of x
  14.193 -
  14.194 -fun make_schematic_type_var (x,i) =
  14.195 -      tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i));
  14.196 -fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x));
  14.197 -
  14.198 -fun lookup_const c =
  14.199 -  case Symtab.lookup const_trans_table c of
  14.200 -    SOME c' => c'
  14.201 -  | NONE => ascii_of c
  14.202 -
  14.203 -(* HOL.eq MUST BE "equal" because it's built into ATPs. *)
  14.204 -fun make_fixed_const @{const_name HOL.eq} = "equal"
  14.205 -  | make_fixed_const c = const_prefix ^ lookup_const c
  14.206 -
  14.207 -fun make_fixed_type_const c = type_const_prefix ^ lookup_const c
  14.208 -
  14.209 -fun make_type_class clas = class_prefix ^ ascii_of clas;
  14.210 -
  14.211 -(* The number of type arguments of a constant, zero if it's monomorphic. For
  14.212 -   (instances of) Skolem pseudoconstants, this information is encoded in the
  14.213 -   constant name. *)
  14.214 -fun num_type_args thy s =
  14.215 -  if String.isPrefix skolem_const_prefix s then
  14.216 -    s |> space_explode Long_Name.separator |> List.last |> Int.fromString |> the
  14.217 -  else
  14.218 -    (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
  14.219 -
  14.220 -fun new_skolem_var_from_const s =
  14.221 -  let
  14.222 -    val ss = s |> space_explode Long_Name.separator
  14.223 -    val n = length ss
  14.224 -  in (nth ss (n - 2), nth ss (n - 3) |> Int.fromString |> the) end
  14.225 -
  14.226 -
  14.227 -(**** Definitions and functions for FOL clauses for TPTP format output ****)
  14.228 -
  14.229 -type name = string * string
  14.230 -
  14.231 -(**** Isabelle FOL clauses ****)
  14.232 -
  14.233 -(* The first component is the type class; the second is a TVar or TFree. *)
  14.234 -datatype type_literal =
  14.235 -  TyLitVar of name * name |
  14.236 -  TyLitFree of name * name
  14.237 -
  14.238 -(*Make literals for sorted type variables*)
  14.239 -fun sorts_on_typs_aux (_, [])   = []
  14.240 -  | sorts_on_typs_aux ((x,i),  s::ss) =
  14.241 -      let val sorts = sorts_on_typs_aux ((x,i), ss)
  14.242 -      in
  14.243 -          if s = "HOL.type" then sorts
  14.244 -          else if i = ~1 then TyLitFree (`make_type_class s, `make_fixed_type_var x) :: sorts
  14.245 -          else TyLitVar (`make_type_class s, (make_schematic_type_var (x,i), x)) :: sorts
  14.246 -      end;
  14.247 -
  14.248 -fun sorts_on_typs (TFree (a,s)) = sorts_on_typs_aux ((a,~1),s)
  14.249 -  | sorts_on_typs (TVar (v,s))  = sorts_on_typs_aux (v,s);
  14.250 -
  14.251 -(*Given a list of sorted type variables, return a list of type literals.*)
  14.252 -fun type_literals_for_types Ts =
  14.253 -  fold (union (op =)) (map sorts_on_typs Ts) []
  14.254 -
  14.255 -(** make axiom and conjecture clauses. **)
  14.256 -
  14.257 -(**** Isabelle arities ****)
  14.258 -
  14.259 -datatype arLit =
  14.260 -  TConsLit of name * name * name list |
  14.261 -  TVarLit of name * name
  14.262 -
  14.263 -datatype arity_clause =
  14.264 -  ArityClause of {name: string, conclLit: arLit, premLits: arLit list}
  14.265 -
  14.266 -
  14.267 -fun gen_TVars 0 = []
  14.268 -  | gen_TVars n = ("T_" ^ Int.toString n) :: gen_TVars (n-1);
  14.269 -
  14.270 -fun pack_sort(_,[])  = []
  14.271 -  | pack_sort(tvar, "HOL.type"::srt) = pack_sort (tvar, srt)   (*IGNORE sort "type"*)
  14.272 -  | pack_sort(tvar, cls::srt) =
  14.273 -    (`make_type_class cls, (tvar, tvar)) :: pack_sort (tvar, srt)
  14.274 -
  14.275 -(*Arity of type constructor tcon :: (arg1,...,argN)res*)
  14.276 -fun make_axiom_arity_clause (tcons, name, (cls,args)) =
  14.277 -  let
  14.278 -    val tvars = gen_TVars (length args)
  14.279 -    val tvars_srts = ListPair.zip (tvars, args)
  14.280 -  in
  14.281 -    ArityClause {name = name,
  14.282 -                 conclLit = TConsLit (`make_type_class cls,
  14.283 -                                      `make_fixed_type_const tcons,
  14.284 -                                      tvars ~~ tvars),
  14.285 -                 premLits = map TVarLit (union_all (map pack_sort tvars_srts))}
  14.286 -  end
  14.287 -
  14.288 -
  14.289 -(**** Isabelle class relations ****)
  14.290 -
  14.291 -datatype class_rel_clause =
  14.292 -  ClassRelClause of {name: string, subclass: name, superclass: name}
  14.293 -
  14.294 -(*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)
  14.295 -fun class_pairs _ [] _ = []
  14.296 -  | class_pairs thy subs supers =
  14.297 -      let
  14.298 -        val class_less = Sorts.class_less (Sign.classes_of thy)
  14.299 -        fun add_super sub super = class_less (sub, super) ? cons (sub, super)
  14.300 -        fun add_supers sub = fold (add_super sub) supers
  14.301 -      in fold add_supers subs [] end
  14.302 -
  14.303 -fun make_class_rel_clause (sub,super) =
  14.304 -  ClassRelClause {name = sub ^ "_" ^ super,
  14.305 -                  subclass = `make_type_class sub,
  14.306 -                  superclass = `make_type_class super}
  14.307 -
  14.308 -fun make_class_rel_clauses thy subs supers =
  14.309 -  map make_class_rel_clause (class_pairs thy subs supers);
  14.310 -
  14.311 -
  14.312 -(** Isabelle arities **)
  14.313 -
  14.314 -fun arity_clause _ _ (_, []) = []
  14.315 -  | arity_clause seen n (tcons, ("HOL.type",_)::ars) =  (*ignore*)
  14.316 -      arity_clause seen n (tcons,ars)
  14.317 -  | arity_clause seen n (tcons, (ar as (class,_)) :: ars) =
  14.318 -      if member (op =) seen class then (*multiple arities for the same tycon, class pair*)
  14.319 -          make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) ::
  14.320 -          arity_clause seen (n+1) (tcons,ars)
  14.321 -      else
  14.322 -          make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class, ar) ::
  14.323 -          arity_clause (class::seen) n (tcons,ars)
  14.324 -
  14.325 -fun multi_arity_clause [] = []
  14.326 -  | multi_arity_clause ((tcons, ars) :: tc_arlists) =
  14.327 -      arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists
  14.328 -
  14.329 -(*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy
  14.330 -  provided its arguments have the corresponding sorts.*)
  14.331 -fun type_class_pairs thy tycons classes =
  14.332 -  let val alg = Sign.classes_of thy
  14.333 -      fun domain_sorts tycon = Sorts.mg_domain alg tycon o single
  14.334 -      fun add_class tycon class =
  14.335 -        cons (class, domain_sorts tycon class)
  14.336 -        handle Sorts.CLASS_ERROR _ => I
  14.337 -      fun try_classes tycon = (tycon, fold (add_class tycon) classes [])
  14.338 -  in  map try_classes tycons  end;
  14.339 -
  14.340 -(*Proving one (tycon, class) membership may require proving others, so iterate.*)
  14.341 -fun iter_type_class_pairs _ _ [] = ([], [])
  14.342 -  | iter_type_class_pairs thy tycons classes =
  14.343 -      let val cpairs = type_class_pairs thy tycons classes
  14.344 -          val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs)))
  14.345 -            |> subtract (op =) classes |> subtract (op =) HOLogic.typeS
  14.346 -          val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
  14.347 -      in (union (op =) classes' classes, union (op =) cpairs' cpairs) end;
  14.348 -
  14.349 -fun make_arity_clauses thy tycons classes =
  14.350 -  let val (classes', cpairs) = iter_type_class_pairs thy tycons classes
  14.351 -  in  (classes', multi_arity_clause cpairs)  end;
  14.352 -
  14.353 -datatype combtyp =
  14.354 -  CombTVar of name |
  14.355 -  CombTFree of name |
  14.356 -  CombType of name * combtyp list
  14.357 -
  14.358 -datatype combterm =
  14.359 -  CombConst of name * combtyp * combtyp list (* Const and Free *) |
  14.360 -  CombVar of name * combtyp |
  14.361 -  CombApp of combterm * combterm
  14.362 -
  14.363 -datatype fol_literal = FOLLiteral of bool * combterm
  14.364 -
  14.365 -(*********************************************************************)
  14.366 -(* convert a clause with type Term.term to a clause with type clause *)
  14.367 -(*********************************************************************)
  14.368 -
  14.369 -(*Result of a function type; no need to check that the argument type matches.*)
  14.370 -fun result_type (CombType (_, [_, tp2])) = tp2
  14.371 -  | result_type _ = raise Fail "non-function type"
  14.372 -
  14.373 -fun combtyp_of (CombConst (_, tp, _)) = tp
  14.374 -  | combtyp_of (CombVar (_, tp)) = tp
  14.375 -  | combtyp_of (CombApp (t1, _)) = result_type (combtyp_of t1)
  14.376 -
  14.377 -(*gets the head of a combinator application, along with the list of arguments*)
  14.378 -fun strip_combterm_comb u =
  14.379 -    let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
  14.380 -        |   stripc  x =  x
  14.381 -    in stripc(u,[]) end
  14.382 -
  14.383 -fun combtype_of (Type (a, Ts)) =
  14.384 -    let val (folTypes, ts) = combtypes_of Ts in
  14.385 -      (CombType (`make_fixed_type_const a, folTypes), ts)
  14.386 -    end
  14.387 -  | combtype_of (tp as TFree (a, _)) = (CombTFree (`make_fixed_type_var a), [tp])
  14.388 -  | combtype_of (tp as TVar (x, _)) =
  14.389 -    (CombTVar (make_schematic_type_var x, string_of_indexname x), [tp])
  14.390 -and combtypes_of Ts =
  14.391 -  let val (folTyps, ts) = ListPair.unzip (map combtype_of Ts) in
  14.392 -    (folTyps, union_all ts)
  14.393 -  end
  14.394 -
  14.395 -(* same as above, but no gathering of sort information *)
  14.396 -fun simple_combtype_of (Type (a, Ts)) =
  14.397 -    CombType (`make_fixed_type_const a, map simple_combtype_of Ts)
  14.398 -  | simple_combtype_of (TFree (a, _)) = CombTFree (`make_fixed_type_var a)
  14.399 -  | simple_combtype_of (TVar (x, _)) =
  14.400 -    CombTVar (make_schematic_type_var x, string_of_indexname x)
  14.401 -
  14.402 -fun new_skolem_const_name th_no s num_T_args =
  14.403 -  [new_skolem_const_prefix, string_of_int th_no, s, string_of_int num_T_args]
  14.404 -  |> space_implode Long_Name.separator
  14.405 -
  14.406 -(* Converts a term (with combinators) into a combterm. Also accummulates sort
  14.407 -   infomation. *)
  14.408 -fun combterm_from_term thy th_no bs (P $ Q) =
  14.409 -      let val (P', tsP) = combterm_from_term thy th_no bs P
  14.410 -          val (Q', tsQ) = combterm_from_term thy th_no bs Q
  14.411 -      in  (CombApp (P', Q'), union (op =) tsP tsQ)  end
  14.412 -  | combterm_from_term thy _ _ (Const (c, T)) =
  14.413 -      let
  14.414 -        val (tp, ts) = combtype_of T
  14.415 -        val tvar_list =
  14.416 -          (if String.isPrefix old_skolem_const_prefix c then
  14.417 -             [] |> Term.add_tvarsT T |> map TVar
  14.418 -           else
  14.419 -             (c, T) |> Sign.const_typargs thy)
  14.420 -          |> map simple_combtype_of
  14.421 -        val c' = CombConst (`make_fixed_const c, tp, tvar_list)
  14.422 -      in  (c',ts)  end
  14.423 -  | combterm_from_term _ _ _ (Free (v, T)) =
  14.424 -      let val (tp, ts) = combtype_of T
  14.425 -          val v' = CombConst (`make_fixed_var v, tp, [])
  14.426 -      in  (v',ts)  end
  14.427 -  | combterm_from_term _ th_no _ (Var (v as (s, _), T)) =
  14.428 -    let
  14.429 -      val (tp, ts) = combtype_of T
  14.430 -      val v' =
  14.431 -        if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
  14.432 -          let
  14.433 -            val tys = T |> strip_type |> swap |> op ::
  14.434 -            val s' = new_skolem_const_name th_no s (length tys)
  14.435 -          in
  14.436 -            CombConst (`make_fixed_const s', tp, map simple_combtype_of tys)
  14.437 -          end
  14.438 -        else
  14.439 -          CombVar ((make_schematic_var v, string_of_indexname v), tp)
  14.440 -    in (v', ts) end
  14.441 -  | combterm_from_term _ _ bs (Bound j) =
  14.442 -      let
  14.443 -        val (s, T) = nth bs j
  14.444 -        val (tp, ts) = combtype_of T
  14.445 -        val v' = CombConst (`make_bound_var s, tp, [])
  14.446 -      in (v', ts) end
  14.447 -  | combterm_from_term _ _ _ (Abs _) = raise Fail "HOL clause: Abs"
  14.448 -
  14.449 -fun predicate_of thy th_no ((@{const Not} $ P), pos) =
  14.450 -    predicate_of thy th_no (P, not pos)
  14.451 -  | predicate_of thy th_no (t, pos) =
  14.452 -    (combterm_from_term thy th_no [] (Envir.eta_contract t), pos)
  14.453 -
  14.454 -fun literals_of_term1 args thy th_no (@{const Trueprop} $ P) =
  14.455 -    literals_of_term1 args thy th_no P
  14.456 -  | literals_of_term1 args thy th_no (@{const HOL.disj} $ P $ Q) =
  14.457 -    literals_of_term1 (literals_of_term1 args thy th_no P) thy th_no Q
  14.458 -  | literals_of_term1 (lits, ts) thy th_no P =
  14.459 -    let val ((pred, ts'), pol) = predicate_of thy th_no (P, true) in
  14.460 -      (FOLLiteral (pol, pred) :: lits, union (op =) ts ts')
  14.461 -    end
  14.462 -val literals_of_term = literals_of_term1 ([], [])
  14.463 -
  14.464 -fun old_skolem_const_name i j num_T_args =
  14.465 -  old_skolem_const_prefix ^ Long_Name.separator ^
  14.466 -  (space_implode Long_Name.separator (map Int.toString [i, j, num_T_args]))
  14.467 -
  14.468 -fun conceal_old_skolem_terms i old_skolems t =
  14.469 -  if exists_Const (curry (op =) @{const_name skolem} o fst) t then
  14.470 -    let
  14.471 -      fun aux old_skolems
  14.472 -              (t as (Const (@{const_name skolem}, Type (_, [_, T])) $ _)) =
  14.473 -          let
  14.474 -            val (old_skolems, s) =
  14.475 -              if i = ~1 then
  14.476 -                (old_skolems, @{const_name undefined})
  14.477 -              else case AList.find (op aconv) old_skolems t of
  14.478 -                s :: _ => (old_skolems, s)
  14.479 -              | [] =>
  14.480 -                let
  14.481 -                  val s = old_skolem_const_name i (length old_skolems)
  14.482 -                                                (length (Term.add_tvarsT T []))
  14.483 -                in ((s, t) :: old_skolems, s) end
  14.484 -          in (old_skolems, Const (s, T)) end
  14.485 -        | aux old_skolems (t1 $ t2) =
  14.486 -          let
  14.487 -            val (old_skolems, t1) = aux old_skolems t1
  14.488 -            val (old_skolems, t2) = aux old_skolems t2
  14.489 -          in (old_skolems, t1 $ t2) end
  14.490 -        | aux old_skolems (Abs (s, T, t')) =
  14.491 -          let val (old_skolems, t') = aux old_skolems t' in
  14.492 -            (old_skolems, Abs (s, T, t'))
  14.493 -          end
  14.494 -        | aux old_skolems t = (old_skolems, t)
  14.495 -    in aux old_skolems t end
  14.496 -  else
  14.497 -    (old_skolems, t)
  14.498 -
  14.499 -fun reveal_old_skolem_terms old_skolems =
  14.500 -  map_aterms (fn t as Const (s, _) =>
  14.501 -                 if String.isPrefix old_skolem_const_prefix s then
  14.502 -                   AList.lookup (op =) old_skolems s |> the
  14.503 -                   |> map_types Type_Infer.paramify_vars
  14.504 -                 else
  14.505 -                   t
  14.506 -               | t => t)
  14.507 -
  14.508 -
  14.509 -(***************************************************************)
  14.510 -(* Type Classes Present in the Axiom or Conjecture Clauses     *)
  14.511 -(***************************************************************)
  14.512 -
  14.513 -fun set_insert (x, s) = Symtab.update (x, ()) s
  14.514 -
  14.515 -fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts)
  14.516 -
  14.517 -(*Remove this trivial type class*)
  14.518 -fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset;
  14.519 -
  14.520 -fun tfree_classes_of_terms ts =
  14.521 -  let val sorts_list = map (map #2 o OldTerm.term_tfrees) ts
  14.522 -  in  Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list))  end;
  14.523 -
  14.524 -fun tvar_classes_of_terms ts =
  14.525 -  let val sorts_list = map (map #2 o OldTerm.term_tvars) ts
  14.526 -  in  Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list))  end;
  14.527 -
  14.528 -(*fold type constructors*)
  14.529 -fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x))
  14.530 -  | fold_type_consts _ _ x = x;
  14.531 -
  14.532 -(*Type constructors used to instantiate overloaded constants are the only ones needed.*)
  14.533 -fun add_type_consts_in_term thy =
  14.534 -  let
  14.535 -    fun aux (Const x) =
  14.536 -        fold (fold_type_consts set_insert) (Sign.const_typargs thy x)
  14.537 -      | aux (Abs (_, _, u)) = aux u
  14.538 -      | aux (Const (@{const_name skolem}, _) $ _) = I
  14.539 -      | aux (t $ u) = aux t #> aux u
  14.540 -      | aux _ = I
  14.541 -  in aux end
  14.542 -
  14.543 -fun type_consts_of_terms thy ts =
  14.544 -  Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty);
  14.545 -
  14.546 -(* ------------------------------------------------------------------------- *)
  14.547 -(* HOL to FOL  (Isabelle to Metis)                                           *)
  14.548 -(* ------------------------------------------------------------------------- *)
  14.549 -
  14.550 -datatype mode = FO | HO | FT  (* first-order, higher-order, fully-typed *)
  14.551 -
  14.552 -fun string_of_mode FO = "FO"
  14.553 -  | string_of_mode HO = "HO"
  14.554 -  | string_of_mode FT = "FT"
  14.555 -
  14.556 -fun fn_isa_to_met_sublevel "equal" = "=" (* FIXME: "c_fequal" *)
  14.557 -  | fn_isa_to_met_sublevel x = x
  14.558 -fun fn_isa_to_met_toplevel "equal" = "="
  14.559 -  | fn_isa_to_met_toplevel x = x
  14.560 -
  14.561 -fun metis_lit b c args = (b, (c, args));
  14.562 -
  14.563 -fun metis_term_from_combtyp (CombTVar (s, _)) = Metis_Term.Var s
  14.564 -  | metis_term_from_combtyp (CombTFree (s, _)) = Metis_Term.Fn (s, [])
  14.565 -  | metis_term_from_combtyp (CombType ((s, _), tps)) =
  14.566 -    Metis_Term.Fn (s, map metis_term_from_combtyp tps);
  14.567 -
  14.568 -(*These two functions insert type literals before the real literals. That is the
  14.569 -  opposite order from TPTP linkup, but maybe OK.*)
  14.570 -
  14.571 -fun hol_term_to_fol_FO tm =
  14.572 -  case strip_combterm_comb tm of
  14.573 -      (CombConst ((c, _), _, tys), tms) =>
  14.574 -        let val tyargs = map metis_term_from_combtyp tys
  14.575 -            val args   = map hol_term_to_fol_FO tms
  14.576 -        in Metis_Term.Fn (c, tyargs @ args) end
  14.577 -    | (CombVar ((v, _), _), []) => Metis_Term.Var v
  14.578 -    | _ => raise Fail "non-first-order combterm"
  14.579 -
  14.580 -fun hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) =
  14.581 -      Metis_Term.Fn (fn_isa_to_met_sublevel a, map metis_term_from_combtyp tylist)
  14.582 -  | hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis_Term.Var s
  14.583 -  | hol_term_to_fol_HO (CombApp (tm1, tm2)) =
  14.584 -       Metis_Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]);
  14.585 -
  14.586 -(*The fully-typed translation, to avoid type errors*)
  14.587 -fun wrap_type (tm, ty) =
  14.588 -  Metis_Term.Fn (type_wrapper_name, [tm, metis_term_from_combtyp ty])
  14.589 -
  14.590 -fun hol_term_to_fol_FT (CombVar ((s, _), ty)) = wrap_type (Metis_Term.Var s, ty)
  14.591 -  | hol_term_to_fol_FT (CombConst((a, _), ty, _)) =
  14.592 -      wrap_type (Metis_Term.Fn(fn_isa_to_met_sublevel a, []), ty)
  14.593 -  | hol_term_to_fol_FT (tm as CombApp(tm1,tm2)) =
  14.594 -       wrap_type (Metis_Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]),
  14.595 -                  combtyp_of tm)
  14.596 -
  14.597 -fun hol_literal_to_fol FO (FOLLiteral (pos, tm)) =
  14.598 -      let val (CombConst((p, _), _, tys), tms) = strip_combterm_comb tm
  14.599 -          val tylits = if p = "equal" then [] else map metis_term_from_combtyp tys
  14.600 -          val lits = map hol_term_to_fol_FO tms
  14.601 -      in metis_lit pos (fn_isa_to_met_toplevel p) (tylits @ lits) end
  14.602 -  | hol_literal_to_fol HO (FOLLiteral (pos, tm)) =
  14.603 -     (case strip_combterm_comb tm of
  14.604 -          (CombConst(("equal", _), _, _), tms) =>
  14.605 -            metis_lit pos "=" (map hol_term_to_fol_HO tms)
  14.606 -        | _ => metis_lit pos "{}" [hol_term_to_fol_HO tm])   (*hBOOL*)
  14.607 -  | hol_literal_to_fol FT (FOLLiteral (pos, tm)) =
  14.608 -     (case strip_combterm_comb tm of
  14.609 -          (CombConst(("equal", _), _, _), tms) =>
  14.610 -            metis_lit pos "=" (map hol_term_to_fol_FT tms)
  14.611 -        | _ => metis_lit pos "{}" [hol_term_to_fol_FT tm])   (*hBOOL*);
  14.612 -
  14.613 -fun literals_of_hol_term thy th_no mode t =
  14.614 -      let val (lits, types_sorts) = literals_of_term thy th_no t
  14.615 -      in  (map (hol_literal_to_fol mode) lits, types_sorts) end;
  14.616 -
  14.617 -(*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*)
  14.618 -fun metis_of_type_literals pos (TyLitVar ((s, _), (s', _))) =
  14.619 -    metis_lit pos s [Metis_Term.Var s']
  14.620 -  | metis_of_type_literals pos (TyLitFree ((s, _), (s', _))) =
  14.621 -    metis_lit pos s [Metis_Term.Fn (s',[])]
  14.622 -
  14.623 -fun default_sort _ (TVar _) = false
  14.624 -  | default_sort ctxt (TFree (x, s)) = (s = the_default [] (Variable.def_sort ctxt (x, ~1)));
  14.625 -
  14.626 -fun metis_of_tfree tf =
  14.627 -  Metis_Thm.axiom (Metis_LiteralSet.singleton (metis_of_type_literals true tf));
  14.628 -
  14.629 -fun hol_thm_to_fol is_conjecture th_no ctxt type_lits mode j old_skolems th =
  14.630 -  let
  14.631 -    val thy = ProofContext.theory_of ctxt
  14.632 -    val (old_skolems, (mlits, types_sorts)) =
  14.633 -     th |> prop_of |> Logic.strip_imp_concl
  14.634 -        |> conceal_old_skolem_terms j old_skolems
  14.635 -        ||> (HOLogic.dest_Trueprop #> literals_of_hol_term thy th_no mode)
  14.636 -  in
  14.637 -    if is_conjecture then
  14.638 -      (Metis_Thm.axiom (Metis_LiteralSet.fromList mlits),
  14.639 -       type_literals_for_types types_sorts, old_skolems)
  14.640 -    else
  14.641 -      let
  14.642 -        val tylits = filter_out (default_sort ctxt) types_sorts
  14.643 -                     |> type_literals_for_types
  14.644 -        val mtylits =
  14.645 -          if type_lits then map (metis_of_type_literals false) tylits else []
  14.646 -      in
  14.647 -        (Metis_Thm.axiom (Metis_LiteralSet.fromList(mtylits @ mlits)), [],
  14.648 -         old_skolems)
  14.649 -      end
  14.650 -  end;
  14.651 -
  14.652 -val helpers =
  14.653 -  [("c_COMBI", (false, map (`I) @{thms COMBI_def})),
  14.654 -   ("c_COMBK", (false, map (`I) @{thms COMBK_def})),
  14.655 -   ("c_COMBB", (false, map (`I) @{thms COMBB_def})),
  14.656 -   ("c_COMBC", (false, map (`I) @{thms COMBC_def})),
  14.657 -   ("c_COMBS", (false, map (`I) @{thms COMBS_def})),
  14.658 -   ("c_fequal", (false, map (rpair @{thm equal_imp_equal})
  14.659 -                            @{thms fequal_imp_equal equal_imp_fequal})),
  14.660 -   ("c_True", (true, map (`I) @{thms True_or_False})),
  14.661 -   ("c_False", (true, map (`I) @{thms True_or_False})),
  14.662 -   ("c_If", (true, map (`I) @{thms if_True if_False True_or_False}))]
  14.663 -
  14.664 -(* ------------------------------------------------------------------------- *)
  14.665 -(* Logic maps manage the interface between HOL and first-order logic.        *)
  14.666 -(* ------------------------------------------------------------------------- *)
  14.667 -
  14.668 -type logic_map =
  14.669 -  {axioms: (Metis_Thm.thm * thm) list,
  14.670 -   tfrees: type_literal list,
  14.671 -   old_skolems: (string * term) list}
  14.672 -
  14.673 -fun is_quasi_fol_clause thy =
  14.674 -  Meson.is_fol_term thy o snd o conceal_old_skolem_terms ~1 [] o prop_of
  14.675 -
  14.676 -(*Extract TFree constraints from context to include as conjecture clauses*)
  14.677 -fun init_tfrees ctxt =
  14.678 -  let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts in
  14.679 -    Vartab.fold add (#2 (Variable.constraints_of ctxt)) []
  14.680 -    |> type_literals_for_types
  14.681 -  end;
  14.682 -
  14.683 -(*Insert non-logical axioms corresponding to all accumulated TFrees*)
  14.684 -fun add_tfrees {axioms, tfrees, old_skolems} : logic_map =
  14.685 -     {axioms = map (rpair TrueI o metis_of_tfree) (distinct (op =) tfrees) @
  14.686 -               axioms,
  14.687 -      tfrees = tfrees, old_skolems = old_skolems}
  14.688 -
  14.689 -(*transform isabelle type / arity clause to metis clause *)
  14.690 -fun add_type_thm [] lmap = lmap
  14.691 -  | add_type_thm ((ith, mth) :: cls) {axioms, tfrees, old_skolems} =
  14.692 -      add_type_thm cls {axioms = (mth, ith) :: axioms, tfrees = tfrees,
  14.693 -                        old_skolems = old_skolems}
  14.694 -
  14.695 -fun const_in_metis c (pred, tm_list) =
  14.696 -  let
  14.697 -    fun in_mterm (Metis_Term.Var _) = false
  14.698 -      | in_mterm (Metis_Term.Fn (".", tm_list)) = exists in_mterm tm_list
  14.699 -      | in_mterm (Metis_Term.Fn (nm, tm_list)) = c=nm orelse exists in_mterm tm_list
  14.700 -  in  c = pred orelse exists in_mterm tm_list  end;
  14.701 -
  14.702 -(* ARITY CLAUSE *)
  14.703 -fun m_arity_cls (TConsLit ((c, _), (t, _), args)) =
  14.704 -    metis_lit true c [Metis_Term.Fn(t, map (Metis_Term.Var o fst) args)]
  14.705 -  | m_arity_cls (TVarLit ((c, _), (s, _))) =
  14.706 -    metis_lit false c [Metis_Term.Var s]
  14.707 -(*TrueI is returned as the Isabelle counterpart because there isn't any.*)
  14.708 -fun arity_cls (ArityClause {conclLit, premLits, ...}) =
  14.709 -  (TrueI,
  14.710 -   Metis_Thm.axiom (Metis_LiteralSet.fromList (map m_arity_cls (conclLit :: premLits))));
  14.711 -
  14.712 -(* CLASSREL CLAUSE *)
  14.713 -fun m_class_rel_cls (subclass, _) (superclass, _) =
  14.714 -  [metis_lit false subclass [Metis_Term.Var "T"], metis_lit true superclass [Metis_Term.Var "T"]];
  14.715 -fun class_rel_cls (ClassRelClause {subclass, superclass, ...}) =
  14.716 -  (TrueI, Metis_Thm.axiom (Metis_LiteralSet.fromList (m_class_rel_cls subclass superclass)));
  14.717 -
  14.718 -fun type_ext thy tms =
  14.719 -  let val subs = tfree_classes_of_terms tms
  14.720 -      val supers = tvar_classes_of_terms tms
  14.721 -      and tycons = type_consts_of_terms thy tms
  14.722 -      val (supers', arity_clauses) = make_arity_clauses thy tycons supers
  14.723 -      val class_rel_clauses = make_class_rel_clauses thy subs supers'
  14.724 -  in  map class_rel_cls class_rel_clauses @ map arity_cls arity_clauses
  14.725 -  end;
  14.726 -
  14.727 -(* Function to generate metis clauses, including comb and type clauses *)
  14.728 -fun build_logic_map mode0 ctxt type_lits cls thss =
  14.729 -  let val thy = ProofContext.theory_of ctxt
  14.730 -      (*The modes FO and FT are sticky. HO can be downgraded to FO.*)
  14.731 -      fun set_mode FO = FO
  14.732 -        | set_mode HO =
  14.733 -          if forall (forall (is_quasi_fol_clause thy)) (cls :: thss) then FO
  14.734 -          else HO
  14.735 -        | set_mode FT = FT
  14.736 -      val mode = set_mode mode0
  14.737 -      (*transform isabelle clause to metis clause *)
  14.738 -      fun add_thm th_no is_conjecture (metis_ith, isa_ith)
  14.739 -                  {axioms, tfrees, old_skolems} : logic_map =
  14.740 -        let
  14.741 -          val (mth, tfree_lits, old_skolems) =
  14.742 -            hol_thm_to_fol is_conjecture th_no ctxt type_lits mode (length axioms)
  14.743 -                           old_skolems metis_ith
  14.744 -        in
  14.745 -           {axioms = (mth, Meson.make_meta_clause isa_ith) :: axioms,
  14.746 -            tfrees = union (op =) tfree_lits tfrees, old_skolems = old_skolems}
  14.747 -        end;
  14.748 -      val lmap = {axioms = [], tfrees = init_tfrees ctxt, old_skolems = []}
  14.749 -                 |> fold (add_thm 0 true o `I) cls
  14.750 -                 |> add_tfrees
  14.751 -                 |> fold (fn (th_no, ths) => fold (add_thm th_no false o `I) ths)
  14.752 -                         (1 upto length thss ~~ thss)
  14.753 -      val clause_lists = map (Metis_Thm.clause o #1) (#axioms lmap)
  14.754 -      fun is_used c =
  14.755 -        exists (Metis_LiteralSet.exists (const_in_metis c o #2)) clause_lists
  14.756 -      val lmap =
  14.757 -        if mode = FO then
  14.758 -          lmap
  14.759 -        else
  14.760 -          let
  14.761 -            val helper_ths =
  14.762 -              helpers |> filter (is_used o fst)
  14.763 -                      |> maps (fn (c, (needs_full_types, thms)) =>
  14.764 -                                  if not (is_used c) orelse
  14.765 -                                     needs_full_types andalso mode <> FT then
  14.766 -                                    []
  14.767 -                                  else
  14.768 -                                    thms)
  14.769 -          in lmap |> fold (add_thm ~1 false) helper_ths end
  14.770 -  in
  14.771 -    (mode, add_type_thm (type_ext thy (maps (map prop_of) (cls :: thss))) lmap)
  14.772 -  end
  14.773 -
  14.774 -end;
    15.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Mon Oct 04 22:01:34 2010 +0200
    15.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Mon Oct 04 22:45:09 2010 +0200
    15.3 @@ -585,6 +585,7 @@
    15.4  fun is_formula_too_complex t =
    15.5    apply_depth t > max_apply_depth orelse formula_has_too_many_lambdas [] t
    15.6  
    15.7 +(* FIXME: Extend to "Meson" and "Metis" *)
    15.8  val exists_sledgehammer_const =
    15.9    exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s)
   15.10