--- a/src/HOL/IsaMakefile Mon Oct 04 22:01:34 2010 +0200
+++ b/src/HOL/IsaMakefile Mon Oct 04 22:45:09 2010 +0200
@@ -155,6 +155,7 @@
Inductive.thy \
Lattices.thy \
Meson.thy \
+ Metis.thy \
Nat.thy \
Option.thy \
Orderings.thy \
@@ -204,6 +205,9 @@
Tools/lin_arith.ML \
Tools/Meson/meson.ML \
Tools/Meson/meson_clausify.ML \
+ Tools/Metis/metis_reconstruct.ML \
+ Tools/Metis/metis_translate.ML \
+ Tools/Metis/metis_tactics.ML \
Tools/nat_arith.ML \
Tools/primrec.ML \
Tools/prop_logic.ML \
@@ -222,6 +226,7 @@
$(SRC)/Provers/Arith/fast_lin_arith.ML \
$(SRC)/Provers/order.ML \
$(SRC)/Provers/trancl.ML \
+ $(SRC)/Tools/Metis/metis.ML \
$(SRC)/Tools/rat.ML
$(OUT)/HOL-Plain: plain.ML $(PLAIN_DEPENDENCIES)
@@ -267,7 +272,6 @@
$(SRC)/Provers/Arith/cancel_numerals.ML \
$(SRC)/Provers/Arith/combine_numerals.ML \
$(SRC)/Provers/Arith/extract_common_term.ML \
- $(SRC)/Tools/Metis/metis.ML \
Tools/async_manager.ML \
Tools/ATP/atp_problem.ML \
Tools/ATP/atp_proof.ML \
@@ -317,9 +321,6 @@
Tools/recdef.ML \
Tools/record.ML \
Tools/semiring_normalizer.ML \
- Tools/Sledgehammer/metis_reconstruct.ML \
- Tools/Sledgehammer/metis_translate.ML \
- Tools/Sledgehammer/metis_tactics.ML \
Tools/Sledgehammer/sledgehammer.ML \
Tools/Sledgehammer/sledgehammer_filter.ML \
Tools/Sledgehammer/sledgehammer_minimize.ML \
--- a/src/HOL/List.thy Mon Oct 04 22:01:34 2010 +0200
+++ b/src/HOL/List.thy Mon Oct 04 22:45:09 2010 +0200
@@ -5,7 +5,7 @@
header {* The datatype of finite lists *}
theory List
-imports Plain Quotient Presburger Code_Numeral Sledgehammer Recdef
+imports Plain Quotient Presburger Code_Numeral Recdef
uses ("Tools/list_code.ML")
begin
--- a/src/HOL/Meson.thy Mon Oct 04 22:01:34 2010 +0200
+++ b/src/HOL/Meson.thy Mon Oct 04 22:45:09 2010 +0200
@@ -8,7 +8,7 @@
header {* MESON Proof Procedure (Model Elimination) *}
theory Meson
-imports Nat
+imports Datatype
uses ("Tools/Meson/meson.ML")
("Tools/Meson/meson_clausify.ML")
begin
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Metis.thy Mon Oct 04 22:45:09 2010 +0200
@@ -0,0 +1,35 @@
+(* Title: HOL/Metis.thy
+ Author: Lawrence C. Paulson, Cambridge University Computer Laboratory
+ Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
+ Author: Jasmin Blanchette, TU Muenchen
+*)
+
+header {* Metis Proof Method *}
+
+theory Metis
+imports Meson
+uses "~~/src/Tools/Metis/metis.ML"
+ ("Tools/Metis/metis_translate.ML")
+ ("Tools/Metis/metis_reconstruct.ML")
+ ("Tools/Metis/metis_tactics.ML")
+begin
+
+definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
+"fequal X Y \<longleftrightarrow> (X = Y)"
+
+lemma fequal_imp_equal [no_atp]: "\<not> fequal X Y \<or> X = Y"
+by (simp add: fequal_def)
+
+lemma equal_imp_fequal [no_atp]: "\<not> X = Y \<or> fequal X Y"
+by (simp add: fequal_def)
+
+lemma equal_imp_equal [no_atp]: "X = Y ==> X = Y"
+by auto
+
+use "Tools/Metis/metis_translate.ML"
+use "Tools/Metis/metis_reconstruct.ML"
+use "Tools/Metis/metis_tactics.ML"
+
+setup Metis_Tactics.setup
+
+end
--- a/src/HOL/Plain.thy Mon Oct 04 22:01:34 2010 +0200
+++ b/src/HOL/Plain.thy Mon Oct 04 22:45:09 2010 +0200
@@ -1,7 +1,7 @@
header {* Plain HOL *}
theory Plain
-imports Datatype FunDef Extraction Meson
+imports Datatype FunDef Extraction Metis
begin
text {*
--- a/src/HOL/Quotient.thy Mon Oct 04 22:01:34 2010 +0200
+++ b/src/HOL/Quotient.thy Mon Oct 04 22:45:09 2010 +0200
@@ -5,7 +5,7 @@
header {* Definition of Quotient Types *}
theory Quotient
-imports Plain Sledgehammer
+imports Plain Hilbert_Choice
uses
("Tools/Quotient/quotient_info.ML")
("Tools/Quotient/quotient_typ.ML")
--- a/src/HOL/Refute.thy Mon Oct 04 22:01:34 2010 +0200
+++ b/src/HOL/Refute.thy Mon Oct 04 22:45:09 2010 +0200
@@ -8,7 +8,7 @@
header {* Refute *}
theory Refute
-imports Hilbert_Choice List
+imports Hilbert_Choice List Sledgehammer
uses "Tools/refute.ML"
begin
--- a/src/HOL/Sledgehammer.thy Mon Oct 04 22:01:34 2010 +0200
+++ b/src/HOL/Sledgehammer.thy Mon Oct 04 22:45:09 2010 +0200
@@ -8,15 +8,11 @@
header {* Sledgehammer: Isabelle--ATP Linkup *}
theory Sledgehammer
-imports Plain Hilbert_Choice
+imports Plain
uses
("Tools/ATP/atp_problem.ML")
("Tools/ATP/atp_proof.ML")
("Tools/ATP/atp_systems.ML")
- ("~~/src/Tools/Metis/metis.ML")
- ("Tools/Sledgehammer/metis_translate.ML")
- ("Tools/Sledgehammer/metis_reconstruct.ML")
- ("Tools/Sledgehammer/metis_tactics.ML")
("Tools/Sledgehammer/sledgehammer_util.ML")
("Tools/Sledgehammer/sledgehammer_filter.ML")
("Tools/Sledgehammer/sledgehammer_translate.ML")
@@ -26,88 +22,11 @@
("Tools/Sledgehammer/sledgehammer_isar.ML")
begin
-lemma TruepropI: "P \<equiv> Q \<Longrightarrow> Trueprop P \<equiv> Trueprop Q"
-by simp
-
-definition skolem :: "'a \<Rightarrow> 'a" where
-[no_atp]: "skolem = (\<lambda>x. x)"
-
-definition COMBI :: "'a \<Rightarrow> 'a" where
-[no_atp]: "COMBI P = P"
-
-definition COMBK :: "'a \<Rightarrow> 'b \<Rightarrow> 'a" where
-[no_atp]: "COMBK P Q = P"
-
-definition COMBB :: "('b => 'c) \<Rightarrow> ('a => 'b) \<Rightarrow> 'a \<Rightarrow> 'c" where [no_atp]:
-"COMBB P Q R = P (Q R)"
-
-definition COMBC :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
-[no_atp]: "COMBC P Q R = P R Q"
-
-definition COMBS :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" where
-[no_atp]: "COMBS P Q R = P R (Q R)"
-
-definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
-"fequal X Y \<longleftrightarrow> (X = Y)"
-
-lemma fequal_imp_equal [no_atp]: "\<not> fequal X Y \<or> X = Y"
-by (simp add: fequal_def)
-
-lemma equal_imp_fequal [no_atp]: "\<not> X = Y \<or> fequal X Y"
-by (simp add: fequal_def)
-
-lemma equal_imp_equal [no_atp]: "X = Y ==> X = Y"
-by auto
-
-lemma skolem_COMBK_iff: "P \<longleftrightarrow> skolem (COMBK P (i\<Colon>nat))"
-unfolding skolem_def COMBK_def by (rule refl)
-
-lemmas skolem_COMBK_I = iffD1 [OF skolem_COMBK_iff]
-lemmas skolem_COMBK_D = iffD2 [OF skolem_COMBK_iff]
-
-text{*Theorems for translation to combinators*}
-
-lemma abs_S [no_atp]: "\<lambda>x. (f x) (g x) \<equiv> COMBS f g"
-apply (rule eq_reflection)
-apply (rule ext)
-apply (simp add: COMBS_def)
-done
-
-lemma abs_I [no_atp]: "\<lambda>x. x \<equiv> COMBI"
-apply (rule eq_reflection)
-apply (rule ext)
-apply (simp add: COMBI_def)
-done
-
-lemma abs_K [no_atp]: "\<lambda>x. y \<equiv> COMBK y"
-apply (rule eq_reflection)
-apply (rule ext)
-apply (simp add: COMBK_def)
-done
-
-lemma abs_B [no_atp]: "\<lambda>x. a (g x) \<equiv> COMBB a g"
-apply (rule eq_reflection)
-apply (rule ext)
-apply (simp add: COMBB_def)
-done
-
-lemma abs_C [no_atp]: "\<lambda>x. (f x) b \<equiv> COMBC f b"
-apply (rule eq_reflection)
-apply (rule ext)
-apply (simp add: COMBC_def)
-done
-
use "Tools/ATP/atp_problem.ML"
use "Tools/ATP/atp_proof.ML"
use "Tools/ATP/atp_systems.ML"
setup ATP_Systems.setup
-use "~~/src/Tools/Metis/metis.ML"
-use "Tools/Sledgehammer/metis_translate.ML"
-use "Tools/Sledgehammer/metis_reconstruct.ML"
-use "Tools/Sledgehammer/metis_tactics.ML"
-setup Metis_Tactics.setup
-
use "Tools/Sledgehammer/sledgehammer_util.ML"
use "Tools/Sledgehammer/sledgehammer_filter.ML"
use "Tools/Sledgehammer/sledgehammer_translate.ML"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Mon Oct 04 22:45:09 2010 +0200
@@ -0,0 +1,557 @@
+(* Title: HOL/Tools/Sledgehammer/metis_reconstruct.ML
+ Author: Kong W. Susanto, Cambridge University Computer Laboratory
+ Author: Lawrence C. Paulson, Cambridge University Computer Laboratory
+ Author: Jasmin Blanchette, TU Muenchen
+ Copyright Cambridge University 2007
+
+Proof reconstruction for Metis.
+*)
+
+signature METIS_RECONSTRUCT =
+sig
+ type mode = Metis_Translate.mode
+
+ val trace : bool Unsynchronized.ref
+ val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
+ val untyped_aconv : term -> term -> bool
+ val replay_one_inference :
+ Proof.context -> mode -> (string * term) list
+ -> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list
+ -> (Metis_Thm.thm * thm) list
+end;
+
+structure Metis_Reconstruct : METIS_RECONSTRUCT =
+struct
+
+open Metis_Translate
+
+val trace = Unsynchronized.ref false
+fun trace_msg msg = if !trace then tracing (msg ()) else ()
+
+datatype term_or_type = SomeTerm of term | SomeType of typ
+
+fun terms_of [] = []
+ | terms_of (SomeTerm t :: tts) = t :: terms_of tts
+ | terms_of (SomeType _ :: tts) = terms_of tts;
+
+fun types_of [] = []
+ | types_of (SomeTerm (Var ((a,idx), _)) :: tts) =
+ if String.isPrefix "_" a then
+ (*Variable generated by Metis, which might have been a type variable.*)
+ TVar (("'" ^ a, idx), HOLogic.typeS) :: types_of tts
+ else types_of tts
+ | types_of (SomeTerm _ :: tts) = types_of tts
+ | types_of (SomeType T :: tts) = T :: types_of tts;
+
+fun apply_list rator nargs rands =
+ let val trands = terms_of rands
+ in if length trands = nargs then SomeTerm (list_comb(rator, trands))
+ else raise Fail
+ ("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global Pure.thy rator ^
+ " expected " ^ Int.toString nargs ^
+ " received " ^ commas (map (Syntax.string_of_term_global Pure.thy) trands))
+ end;
+
+fun infer_types ctxt =
+ Syntax.check_terms (ProofContext.set_mode ProofContext.mode_pattern ctxt);
+
+(*We use 1 rather than 0 because variable references in clauses may otherwise conflict
+ with variable constraints in the goal...at least, type inference often fails otherwise.
+ SEE ALSO axiom_inf below.*)
+fun mk_var (w, T) = Var ((w, 1), T)
+
+(*include the default sort, if available*)
+fun mk_tfree ctxt w =
+ let val ww = "'" ^ w
+ in TFree(ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1))) end;
+
+(*Remove the "apply" operator from an HO term*)
+fun strip_happ args (Metis_Term.Fn(".",[t,u])) = strip_happ (u::args) t
+ | strip_happ args x = (x, args);
+
+fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS)
+
+fun smart_invert_const "fequal" = @{const_name HOL.eq}
+ | smart_invert_const s = invert_const s
+
+fun hol_type_from_metis_term _ (Metis_Term.Var v) =
+ (case strip_prefix_and_unascii tvar_prefix v of
+ SOME w => make_tvar w
+ | NONE => make_tvar v)
+ | hol_type_from_metis_term ctxt (Metis_Term.Fn(x, tys)) =
+ (case strip_prefix_and_unascii type_const_prefix x of
+ SOME tc => Type (smart_invert_const tc,
+ map (hol_type_from_metis_term ctxt) tys)
+ | NONE =>
+ case strip_prefix_and_unascii tfree_prefix x of
+ SOME tf => mk_tfree ctxt tf
+ | NONE => raise Fail ("hol_type_from_metis_term: " ^ x));
+
+(*Maps metis terms to isabelle terms*)
+fun hol_term_from_metis_PT ctxt fol_tm =
+ let val thy = ProofContext.theory_of ctxt
+ val _ = trace_msg (fn () => "hol_term_from_metis_PT: " ^
+ Metis_Term.toString fol_tm)
+ fun tm_to_tt (Metis_Term.Var v) =
+ (case strip_prefix_and_unascii tvar_prefix v of
+ SOME w => SomeType (make_tvar w)
+ | NONE =>
+ case strip_prefix_and_unascii schematic_var_prefix v of
+ SOME w => SomeTerm (mk_var (w, HOLogic.typeT))
+ | NONE => SomeTerm (mk_var (v, HOLogic.typeT)) )
+ (*Var from Metis with a name like _nnn; possibly a type variable*)
+ | tm_to_tt (Metis_Term.Fn ("{}", [arg])) = tm_to_tt arg (*hBOOL*)
+ | tm_to_tt (t as Metis_Term.Fn (".",_)) =
+ let val (rator,rands) = strip_happ [] t
+ in case rator of
+ Metis_Term.Fn(fname,ts) => applic_to_tt (fname, ts @ rands)
+ | _ => case tm_to_tt rator of
+ SomeTerm t => SomeTerm (list_comb(t, terms_of (map tm_to_tt rands)))
+ | _ => raise Fail "tm_to_tt: HO application"
+ end
+ | tm_to_tt (Metis_Term.Fn (fname, args)) = applic_to_tt (fname,args)
+ and applic_to_tt ("=",ts) =
+ SomeTerm (list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
+ | applic_to_tt (a,ts) =
+ case strip_prefix_and_unascii const_prefix a of
+ SOME b =>
+ let
+ val c = smart_invert_const b
+ val ntypes = num_type_args thy c
+ val nterms = length ts - ntypes
+ val tts = map tm_to_tt ts
+ val tys = types_of (List.take(tts,ntypes))
+ val t =
+ if String.isPrefix new_skolem_const_prefix c then
+ Var (new_skolem_var_from_const c,
+ Type_Infer.paramify_vars (tl tys ---> hd tys))
+ else
+ Const (c, dummyT)
+ in if length tys = ntypes then
+ apply_list t nterms (List.drop(tts,ntypes))
+ else
+ raise Fail ("Constant " ^ c ^ " expects " ^ Int.toString ntypes ^
+ " but gets " ^ Int.toString (length tys) ^
+ " type arguments\n" ^
+ cat_lines (map (Syntax.string_of_typ ctxt) tys) ^
+ " the terms are \n" ^
+ cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
+ end
+ | NONE => (*Not a constant. Is it a type constructor?*)
+ case strip_prefix_and_unascii type_const_prefix a of
+ SOME b =>
+ SomeType (Type (smart_invert_const b, types_of (map tm_to_tt ts)))
+ | NONE => (*Maybe a TFree. Should then check that ts=[].*)
+ case strip_prefix_and_unascii tfree_prefix a of
+ SOME b => SomeType (mk_tfree ctxt b)
+ | NONE => (*a fixed variable? They are Skolem functions.*)
+ case strip_prefix_and_unascii fixed_var_prefix a of
+ SOME b =>
+ let val opr = Free (b, HOLogic.typeT)
+ in apply_list opr (length ts) (map tm_to_tt ts) end
+ | NONE => raise Fail ("unexpected metis function: " ^ a)
+ in
+ case tm_to_tt fol_tm of
+ SomeTerm t => t
+ | SomeType T => raise TYPE ("fol_tm_to_tt: Term expected", [T], [])
+ end
+
+(*Maps fully-typed metis terms to isabelle terms*)
+fun hol_term_from_metis_FT ctxt fol_tm =
+ let val _ = trace_msg (fn () => "hol_term_from_metis_FT: " ^
+ Metis_Term.toString fol_tm)
+ fun cvt (Metis_Term.Fn ("ti", [Metis_Term.Var v, _])) =
+ (case strip_prefix_and_unascii schematic_var_prefix v of
+ SOME w => mk_var(w, dummyT)
+ | NONE => mk_var(v, dummyT))
+ | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn ("=",[]), _])) =
+ Const (@{const_name HOL.eq}, HOLogic.typeT)
+ | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn (x,[]), ty])) =
+ (case strip_prefix_and_unascii const_prefix x of
+ SOME c => Const (smart_invert_const c, dummyT)
+ | NONE => (*Not a constant. Is it a fixed variable??*)
+ case strip_prefix_and_unascii fixed_var_prefix x of
+ SOME v => Free (v, hol_type_from_metis_term ctxt ty)
+ | NONE => raise Fail ("hol_term_from_metis_FT bad constant: " ^ x))
+ | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn (".",[tm1,tm2]), _])) =
+ cvt tm1 $ cvt tm2
+ | cvt (Metis_Term.Fn (".",[tm1,tm2])) = (*untyped application*)
+ cvt tm1 $ cvt tm2
+ | cvt (Metis_Term.Fn ("{}", [arg])) = cvt arg (*hBOOL*)
+ | cvt (Metis_Term.Fn ("=", [tm1,tm2])) =
+ list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), map cvt [tm1,tm2])
+ | cvt (t as Metis_Term.Fn (x, [])) =
+ (case strip_prefix_and_unascii const_prefix x of
+ SOME c => Const (smart_invert_const c, dummyT)
+ | NONE => (*Not a constant. Is it a fixed variable??*)
+ case strip_prefix_and_unascii fixed_var_prefix x of
+ SOME v => Free (v, dummyT)
+ | NONE => (trace_msg (fn () => "hol_term_from_metis_FT bad const: " ^ x);
+ hol_term_from_metis_PT ctxt t))
+ | cvt t = (trace_msg (fn () => "hol_term_from_metis_FT bad term: " ^ Metis_Term.toString t);
+ hol_term_from_metis_PT ctxt t)
+ in fol_tm |> cvt end
+
+fun hol_term_from_metis FT = hol_term_from_metis_FT
+ | hol_term_from_metis _ = hol_term_from_metis_PT
+
+fun hol_terms_from_fol ctxt mode old_skolems fol_tms =
+ let val ts = map (hol_term_from_metis mode ctxt) fol_tms
+ val _ = trace_msg (fn () => " calling type inference:")
+ val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts
+ val ts' = ts |> map (reveal_old_skolem_terms old_skolems)
+ |> infer_types ctxt
+ val _ = app (fn t => trace_msg
+ (fn () => " final term: " ^ Syntax.string_of_term ctxt t ^
+ " of type " ^ Syntax.string_of_typ ctxt (type_of t)))
+ ts'
+ in ts' end;
+
+(* ------------------------------------------------------------------------- *)
+(* FOL step Inference Rules *)
+(* ------------------------------------------------------------------------- *)
+
+(*for debugging only*)
+(*
+fun print_thpair (fth,th) =
+ (trace_msg (fn () => "=============================================");
+ trace_msg (fn () => "Metis: " ^ Metis_Thm.toString fth);
+ trace_msg (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th));
+*)
+
+fun lookth thpairs (fth : Metis_Thm.thm) =
+ the (AList.lookup (uncurry Metis_Thm.equal) thpairs fth)
+ handle Option.Option =>
+ raise Fail ("Failed to find Metis theorem " ^ Metis_Thm.toString fth)
+
+fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx));
+
+(* INFERENCE RULE: AXIOM *)
+
+fun axiom_inf thpairs th = Thm.incr_indexes 1 (lookth thpairs th);
+ (*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*)
+
+(* INFERENCE RULE: ASSUME *)
+
+val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)}
+
+fun inst_excluded_middle thy i_atm =
+ let val th = EXCLUDED_MIDDLE
+ val [vx] = Term.add_vars (prop_of th) []
+ val substs = [(cterm_of thy (Var vx), cterm_of thy i_atm)]
+ in cterm_instantiate substs th end;
+
+fun assume_inf ctxt mode old_skolems atm =
+ inst_excluded_middle
+ (ProofContext.theory_of ctxt)
+ (singleton (hol_terms_from_fol ctxt mode old_skolems) (Metis_Term.Fn atm))
+
+(* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying
+ to reconstruct them admits new possibilities of errors, e.g. concerning
+ sorts. Instead we try to arrange that new TVars are distinct and that types
+ can be inferred from terms. *)
+
+fun inst_inf ctxt mode old_skolems thpairs fsubst th =
+ let val thy = ProofContext.theory_of ctxt
+ val i_th = lookth thpairs th
+ val i_th_vars = Term.add_vars (prop_of i_th) []
+ fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars)
+ fun subst_translation (x,y) =
+ let val v = find_var x
+ (* We call "reveal_old_skolem_terms" and "infer_types" below. *)
+ val t = hol_term_from_metis mode ctxt y
+ in SOME (cterm_of thy (Var v), t) end
+ handle Option.Option =>
+ (trace_msg (fn () => "\"find_var\" failed for " ^ x ^
+ " in " ^ Display.string_of_thm ctxt i_th);
+ NONE)
+ | TYPE _ =>
+ (trace_msg (fn () => "\"hol_term_from_metis\" failed for " ^ x ^
+ " in " ^ Display.string_of_thm ctxt i_th);
+ NONE)
+ fun remove_typeinst (a, t) =
+ case strip_prefix_and_unascii schematic_var_prefix a of
+ SOME b => SOME (b, t)
+ | NONE => case strip_prefix_and_unascii tvar_prefix a of
+ SOME _ => NONE (*type instantiations are forbidden!*)
+ | NONE => SOME (a,t) (*internal Metis var?*)
+ val _ = trace_msg (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th)
+ val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst)
+ val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs)
+ val tms = rawtms |> map (reveal_old_skolem_terms old_skolems)
+ |> infer_types ctxt
+ val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
+ val substs' = ListPair.zip (vars, map ctm_of tms)
+ val _ = trace_msg (fn () =>
+ cat_lines ("subst_translations:" ::
+ (substs' |> map (fn (x, y) =>
+ Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
+ Syntax.string_of_term ctxt (term_of y)))));
+ in cterm_instantiate substs' i_th end
+ handle THM (msg, _, _) =>
+ error ("Cannot replay Metis proof in Isabelle:\n" ^ msg)
+
+(* INFERENCE RULE: RESOLVE *)
+
+(* Like RSN, but we rename apart only the type variables. Vars here typically
+ have an index of 1, and the use of RSN would increase this typically to 3.
+ Instantiations of those Vars could then fail. See comment on "mk_var". *)
+fun resolve_inc_tyvars thy tha i thb =
+ let
+ val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
+ fun aux tha thb =
+ case Thm.bicompose false (false, tha, nprems_of tha) i thb
+ |> Seq.list_of |> distinct Thm.eq_thm of
+ [th] => th
+ | _ => raise THM ("resolve_inc_tyvars: unique result expected", i,
+ [tha, thb])
+ in
+ aux tha thb
+ handle TERM z =>
+ (* The unifier, which is invoked from "Thm.bicompose", will sometimes
+ refuse to unify "?a::?'a" with "?a::?'b" or "?a::nat" and throw a
+ "TERM" exception (with "add_ffpair" as first argument). We then
+ perform unification of the types of variables by hand and try
+ again. We could do this the first time around but this error
+ occurs seldom and we don't want to break existing proofs in subtle
+ ways or slow them down needlessly. *)
+ case [] |> fold (Term.add_vars o prop_of) [tha, thb]
+ |> AList.group (op =)
+ |> maps (fn ((s, _), T :: Ts) =>
+ map (fn T' => (Free (s, T), Free (s, T'))) Ts)
+ |> rpair (Envir.empty ~1)
+ |-> fold (Pattern.unify thy)
+ |> Envir.type_env |> Vartab.dest
+ |> map (fn (x, (S, T)) =>
+ pairself (ctyp_of thy) (TVar (x, S), T)) of
+ [] => raise TERM z
+ | ps => aux (instantiate (ps, []) tha) (instantiate (ps, []) thb)
+ end
+
+fun mk_not (Const (@{const_name Not}, _) $ b) = b
+ | mk_not b = HOLogic.mk_not b
+
+(* Match untyped terms. *)
+fun untyped_aconv (Const (a, _)) (Const(b, _)) = (a = b)
+ | untyped_aconv (Free (a, _)) (Free (b, _)) = (a = b)
+ | untyped_aconv (Var ((a, _), _)) (Var ((b, _), _)) =
+ (a = b) (* The index is ignored, for some reason. *)
+ | untyped_aconv (Bound i) (Bound j) = (i = j)
+ | untyped_aconv (Abs (_, _, t)) (Abs (_, _, u)) = untyped_aconv t u
+ | untyped_aconv (t1 $ t2) (u1 $ u2) =
+ untyped_aconv t1 u1 andalso untyped_aconv t2 u2
+ | untyped_aconv _ _ = false
+
+(* Finding the relative location of an untyped term within a list of terms *)
+fun literal_index lit =
+ let
+ val lit = Envir.eta_contract lit
+ fun get _ [] = raise Empty
+ | get n (x :: xs) =
+ if untyped_aconv lit (Envir.eta_contract (HOLogic.dest_Trueprop x)) then
+ n
+ else
+ get (n+1) xs
+ in get 1 end
+
+(* Permute a rule's premises to move the i-th premise to the last position. *)
+fun make_last i th =
+ let val n = nprems_of th
+ in if 1 <= i andalso i <= n
+ then Thm.permute_prems (i-1) 1 th
+ else raise THM("select_literal", i, [th])
+ end;
+
+(* Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing
+ double-negations. *)
+val negate_head = rewrite_rule [@{thm atomize_not}, not_not RS eq_reflection]
+
+(* Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *)
+val select_literal = negate_head oo make_last
+
+fun resolve_inf ctxt mode old_skolems thpairs atm th1 th2 =
+ let
+ val thy = ProofContext.theory_of ctxt
+ val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
+ val _ = trace_msg (fn () => " isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
+ val _ = trace_msg (fn () => " isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
+ in
+ (* Trivial cases where one operand is type info *)
+ if Thm.eq_thm (TrueI, i_th1) then
+ i_th2
+ else if Thm.eq_thm (TrueI, i_th2) then
+ i_th1
+ else
+ let
+ val i_atm = singleton (hol_terms_from_fol ctxt mode old_skolems)
+ (Metis_Term.Fn atm)
+ val _ = trace_msg (fn () => " atom: " ^ Syntax.string_of_term ctxt i_atm)
+ val prems_th1 = prems_of i_th1
+ val prems_th2 = prems_of i_th2
+ val index_th1 = literal_index (mk_not i_atm) prems_th1
+ handle Empty => raise Fail "Failed to find literal in th1"
+ val _ = trace_msg (fn () => " index_th1: " ^ Int.toString index_th1)
+ val index_th2 = literal_index i_atm prems_th2
+ handle Empty => raise Fail "Failed to find literal in th2"
+ val _ = trace_msg (fn () => " index_th2: " ^ Int.toString index_th2)
+ in
+ resolve_inc_tyvars thy (select_literal index_th1 i_th1) index_th2 i_th2
+ end
+ end;
+
+(* INFERENCE RULE: REFL *)
+
+val REFL_THM = Thm.incr_indexes 2 @{lemma "t ~= t ==> False" by simp}
+
+val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
+val refl_idx = 1 + Thm.maxidx_of REFL_THM;
+
+fun refl_inf ctxt mode old_skolems t =
+ let val thy = ProofContext.theory_of ctxt
+ val i_t = singleton (hol_terms_from_fol ctxt mode old_skolems) t
+ val _ = trace_msg (fn () => " term: " ^ Syntax.string_of_term ctxt i_t)
+ val c_t = cterm_incr_types thy refl_idx i_t
+ in cterm_instantiate [(refl_x, c_t)] REFL_THM end;
+
+(* INFERENCE RULE: EQUALITY *)
+
+val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp}
+val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp}
+
+val metis_eq = Metis_Term.Fn ("=", []);
+
+fun get_ty_arg_size _ (Const (@{const_name HOL.eq}, _)) = 0 (*equality has no type arguments*)
+ | get_ty_arg_size thy (Const (c, _)) = (num_type_args thy c handle TYPE _ => 0)
+ | get_ty_arg_size _ _ = 0;
+
+fun equality_inf ctxt mode old_skolems (pos, atm) fp fr =
+ let val thy = ProofContext.theory_of ctxt
+ val m_tm = Metis_Term.Fn atm
+ val [i_atm,i_tm] = hol_terms_from_fol ctxt mode old_skolems [m_tm, fr]
+ val _ = trace_msg (fn () => "sign of the literal: " ^ Bool.toString pos)
+ fun replace_item_list lx 0 (_::ls) = lx::ls
+ | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
+ fun path_finder_FO tm [] = (tm, Bound 0)
+ | path_finder_FO tm (p::ps) =
+ let val (tm1,args) = strip_comb tm
+ val adjustment = get_ty_arg_size thy tm1
+ val p' = if adjustment > p then p else p-adjustment
+ val tm_p = List.nth(args,p')
+ handle Subscript =>
+ error ("Cannot replay Metis proof in Isabelle:\n" ^
+ "equality_inf: " ^ Int.toString p ^ " adj " ^
+ Int.toString adjustment ^ " term " ^
+ Syntax.string_of_term ctxt tm)
+ val _ = trace_msg (fn () => "path_finder: " ^ Int.toString p ^
+ " " ^ Syntax.string_of_term ctxt tm_p)
+ val (r,t) = path_finder_FO tm_p ps
+ in
+ (r, list_comb (tm1, replace_item_list t p' args))
+ end
+ fun path_finder_HO tm [] = (tm, Bound 0)
+ | path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps)
+ | path_finder_HO (t$u) (_::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps)
+ | path_finder_HO tm ps =
+ raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^
+ "equality_inf, path_finder_HO: path = " ^
+ space_implode " " (map Int.toString ps) ^
+ " isa-term: " ^ Syntax.string_of_term ctxt tm)
+ fun path_finder_FT tm [] _ = (tm, Bound 0)
+ | path_finder_FT tm (0::ps) (Metis_Term.Fn ("ti", [t1, _])) =
+ path_finder_FT tm ps t1
+ | path_finder_FT (t$u) (0::ps) (Metis_Term.Fn (".", [t1, _])) =
+ (fn(x,y) => (x, y$u)) (path_finder_FT t ps t1)
+ | path_finder_FT (t$u) (1::ps) (Metis_Term.Fn (".", [_, t2])) =
+ (fn(x,y) => (x, t$y)) (path_finder_FT u ps t2)
+ | path_finder_FT tm ps t =
+ raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^
+ "equality_inf, path_finder_FT: path = " ^
+ space_implode " " (map Int.toString ps) ^
+ " isa-term: " ^ Syntax.string_of_term ctxt tm ^
+ " fol-term: " ^ Metis_Term.toString t)
+ fun path_finder FO tm ps _ = path_finder_FO tm ps
+ | path_finder HO (tm as Const(@{const_name HOL.eq},_) $ _ $ _) (p::ps) _ =
+ (*equality: not curried, as other predicates are*)
+ if p=0 then path_finder_HO tm (0::1::ps) (*select first operand*)
+ else path_finder_HO tm (p::ps) (*1 selects second operand*)
+ | path_finder HO tm (_ :: ps) (Metis_Term.Fn ("{}", [_])) =
+ path_finder_HO tm ps (*if not equality, ignore head to skip hBOOL*)
+ | path_finder FT (tm as Const(@{const_name HOL.eq}, _) $ _ $ _) (p::ps)
+ (Metis_Term.Fn ("=", [t1,t2])) =
+ (*equality: not curried, as other predicates are*)
+ if p=0 then path_finder_FT tm (0::1::ps)
+ (Metis_Term.Fn (".", [Metis_Term.Fn (".", [metis_eq,t1]), t2]))
+ (*select first operand*)
+ else path_finder_FT tm (p::ps)
+ (Metis_Term.Fn (".", [metis_eq,t2]))
+ (*1 selects second operand*)
+ | path_finder FT tm (_ :: ps) (Metis_Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1
+ (*if not equality, ignore head to skip the hBOOL predicate*)
+ | path_finder FT tm ps t = path_finder_FT tm ps t (*really an error case!*)
+ fun path_finder_lit ((nt as Const (@{const_name Not}, _)) $ tm_a) idx =
+ let val (tm, tm_rslt) = path_finder mode tm_a idx m_tm
+ in (tm, nt $ tm_rslt) end
+ | path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm
+ val (tm_subst, body) = path_finder_lit i_atm fp
+ val tm_abs = Abs ("x", type_of tm_subst, body)
+ val _ = trace_msg (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
+ val _ = trace_msg (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
+ val _ = trace_msg (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
+ val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst) (*ill typed but gives right max*)
+ val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
+ val _ = trace_msg (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
+ val eq_terms = map (pairself (cterm_of thy))
+ (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
+ in cterm_instantiate eq_terms subst' end;
+
+val factor = Seq.hd o distinct_subgoals_tac;
+
+fun step ctxt mode old_skolems thpairs p =
+ case p of
+ (fol_th, Metis_Proof.Axiom _) => factor (axiom_inf thpairs fol_th)
+ | (_, Metis_Proof.Assume f_atm) => assume_inf ctxt mode old_skolems f_atm
+ | (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) =>
+ factor (inst_inf ctxt mode old_skolems thpairs f_subst f_th1)
+ | (_, Metis_Proof.Resolve(f_atm, f_th1, f_th2)) =>
+ factor (resolve_inf ctxt mode old_skolems thpairs f_atm f_th1 f_th2)
+ | (_, Metis_Proof.Refl f_tm) => refl_inf ctxt mode old_skolems f_tm
+ | (_, Metis_Proof.Equality (f_lit, f_p, f_r)) =>
+ equality_inf ctxt mode old_skolems f_lit f_p f_r
+
+fun flexflex_first_order th =
+ case Thm.tpairs_of th of
+ [] => th
+ | pairs =>
+ let val thy = theory_of_thm th
+ val (_, tenv) =
+ fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
+ val t_pairs = map Meson.term_pair_of (Vartab.dest tenv)
+ val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th
+ in th' end
+ handle THM _ => th;
+
+fun is_metis_literal_genuine (_, (s, _)) = not (String.isPrefix class_prefix s)
+fun is_isabelle_literal_genuine t =
+ case t of _ $ (Const (@{const_name skolem}, _) $ _) => false | _ => true
+
+fun count p xs = fold (fn x => if p x then Integer.add 1 else I) xs 0
+
+fun replay_one_inference ctxt mode old_skolems (fol_th, inf) thpairs =
+ let
+ val _ = trace_msg (fn () => "=============================================")
+ val _ = trace_msg (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)
+ val _ = trace_msg (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)
+ val th = step ctxt mode old_skolems thpairs (fol_th, inf)
+ |> flexflex_first_order
+ val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
+ val _ = trace_msg (fn () => "=============================================")
+ val num_metis_lits =
+ fol_th |> Metis_Thm.clause |> Metis_LiteralSet.toList
+ |> count is_metis_literal_genuine
+ val num_isabelle_lits =
+ th |> prems_of |> count is_isabelle_literal_genuine
+ val _ = if num_metis_lits = num_isabelle_lits then ()
+ else error "Cannot replay Metis proof in Isabelle: Out of sync."
+ in (fol_th, th) :: thpairs end
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Metis/metis_tactics.ML Mon Oct 04 22:45:09 2010 +0200
@@ -0,0 +1,449 @@
+(* Title: HOL/Tools/Sledgehammer/metis_tactics.ML
+ Author: Kong W. Susanto, Cambridge University Computer Laboratory
+ Author: Lawrence C. Paulson, Cambridge University Computer Laboratory
+ Author: Jasmin Blanchette, TU Muenchen
+ Copyright Cambridge University 2007
+
+HOL setup for the Metis prover.
+*)
+
+signature METIS_TACTICS =
+sig
+ val trace : bool Unsynchronized.ref
+ val type_lits : bool Config.T
+ val new_skolemizer : bool Config.T
+ val metis_tac : Proof.context -> thm list -> int -> tactic
+ val metisF_tac : Proof.context -> thm list -> int -> tactic
+ val metisFT_tac : Proof.context -> thm list -> int -> tactic
+ val setup : theory -> theory
+end
+
+structure Metis_Tactics : METIS_TACTICS =
+struct
+
+open Metis_Translate
+open Metis_Reconstruct
+
+structure Int_Pair_Graph =
+ Graph(type key = int * int val ord = prod_ord int_ord int_ord)
+
+fun trace_msg msg = if !trace then tracing (msg ()) else ()
+
+val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" (K true)
+val (new_skolemizer, new_skolemizer_setup) =
+ Attrib.config_bool "metis_new_skolemizer" (K false)
+
+fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const);
+
+fun have_common_thm ths1 ths2 =
+ exists (member Thm.eq_thm ths1) (map Meson.make_meta_clause ths2)
+
+(*Determining which axiom clauses are actually used*)
+fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th)
+ | used_axioms _ _ = NONE;
+
+val clause_params =
+ {ordering = Metis_KnuthBendixOrder.default,
+ orderLiterals = Metis_Clause.UnsignedLiteralOrder,
+ orderTerms = true}
+val active_params =
+ {clause = clause_params,
+ prefactor = #prefactor Metis_Active.default,
+ postfactor = #postfactor Metis_Active.default}
+val waiting_params =
+ {symbolsWeight = 1.0,
+ variablesWeight = 0.0,
+ literalsWeight = 0.0,
+ models = []}
+val resolution_params = {active = active_params, waiting = waiting_params}
+
+fun instantiate_theorem thy inst th =
+ let
+ val tyenv = Vartab.empty |> fold (Type.raw_unify o pairself fastype_of) inst
+ val instT =
+ [] |> Vartab.fold (fn (z, (S, T)) =>
+ cons (TVar (z, S), Type.devar tyenv T)) tyenv
+ val inst = inst |> map (pairself (subst_atomic_types instT))
+ val _ = tracing (cat_lines (map (fn (T, U) =>
+ Syntax.string_of_typ @{context} T ^ " |-> " ^
+ Syntax.string_of_typ @{context} U) instT))
+ val _ = tracing (cat_lines (map (fn (t, u) =>
+ Syntax.string_of_term @{context} t ^ " |-> " ^
+ Syntax.string_of_term @{context} u) inst))
+ val cinstT = instT |> map (pairself (ctyp_of thy))
+ val cinst = inst |> map (pairself (cterm_of thy))
+ in th |> Thm.instantiate (cinstT, cinst) end
+
+(* In principle, it should be sufficient to apply "assume_tac" to unify the
+ conclusion with one of the premises. However, in practice, this is unreliable
+ because of the mildly higher-order nature of the unification problems.
+ Typical constraints are of the form
+ "?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",
+ where the nonvariables are goal parameters. *)
+fun unify_first_prem_with_concl thy i th =
+ let
+ val goal = Logic.get_goal (prop_of th) i |> Envir.beta_eta_contract
+ val prem = goal |> Logic.strip_assums_hyp |> hd
+ val concl = goal |> Logic.strip_assums_concl
+ fun pair_untyped_aconv (t1, t2) (u1, u2) =
+ untyped_aconv t1 u1 andalso untyped_aconv t2 u2
+ fun add_terms tp inst =
+ if exists (pair_untyped_aconv tp) inst then inst
+ else tp :: map (apsnd (subst_atomic [tp])) inst
+ fun is_flex t =
+ case strip_comb t of
+ (Var _, args) => forall is_Bound args
+ | _ => false
+ fun unify_flex flex rigid =
+ case strip_comb flex of
+ (Var (z as (_, T)), args) =>
+ add_terms (Var z,
+ fold_rev (curry absdummy) (take (length args) (binder_types T)) rigid)
+ | _ => raise TERM ("unify_flex: expected flex", [flex])
+ fun unify_potential_flex comb atom =
+ if is_flex comb then unify_flex comb atom
+ else if is_Var atom then add_terms (atom, comb)
+ else raise TERM ("unify_terms", [comb, atom])
+ fun unify_terms (t, u) =
+ case (t, u) of
+ (t1 $ t2, u1 $ u2) =>
+ if is_flex t then unify_flex t u
+ else if is_flex u then unify_flex u t
+ else fold unify_terms [(t1, u1), (t2, u2)]
+ | (_ $ _, _) => unify_potential_flex t u
+ | (_, _ $ _) => unify_potential_flex u t
+ | (Var _, _) => add_terms (t, u)
+ | (_, Var _) => add_terms (u, t)
+ | _ => if untyped_aconv t u then I else raise TERM ("unify_terms", [t, u])
+ in th |> instantiate_theorem thy (unify_terms (prem, concl) []) end
+
+fun shuffle_key (((axiom_no, (_, index_no)), _), _) = (index_no, axiom_no)
+fun shuffle_ord p =
+ rev_order (prod_ord int_ord int_ord (pairself shuffle_key p))
+
+val copy_prem = @{lemma "P ==> (P ==> P ==> Q) ==> Q" by fast}
+
+fun copy_prems_tac [] ns i =
+ if forall (curry (op =) 1) ns then all_tac else copy_prems_tac (rev ns) [] i
+ | copy_prems_tac (1 :: ms) ns i =
+ rotate_tac 1 i THEN copy_prems_tac ms (1 :: ns) i
+ | copy_prems_tac (m :: ms) ns i =
+ etac copy_prem i THEN copy_prems_tac ms (m div 2 :: (m + 1) div 2 :: ns) i
+
+fun instantiate_forall_tac thy params t i =
+ let
+ fun repair (t as (Var ((s, _), _))) =
+ (case find_index (fn ((s', _), _) => s' = s) params of
+ ~1 => t
+ | j => Bound j)
+ | repair (t $ u) = repair t $ repair u
+ | repair t = t
+ val t' = t |> repair |> fold (curry absdummy) (map snd params)
+ fun do_instantiate th =
+ let val var = Term.add_vars (prop_of th) [] |> the_single in
+ th |> instantiate_theorem thy [(Var var, t')]
+ end
+ in
+ etac @{thm allE} i
+ THEN rotate_tac ~1 i
+ THEN PRIMITIVE do_instantiate
+ end
+
+fun release_clusters_tac _ _ _ _ [] = K all_tac
+ | release_clusters_tac thy ax_counts substs params
+ ((ax_no, cluster_no) :: clusters) =
+ let
+ fun in_right_cluster s =
+ (s |> Meson_Clausify.cluster_of_zapped_var_name |> fst |> snd |> fst)
+ = cluster_no
+ val cluster_substs =
+ substs
+ |> map_filter (fn (ax_no', (_, (_, tsubst))) =>
+ if ax_no' = ax_no then
+ tsubst |> filter (in_right_cluster
+ o fst o fst o dest_Var o fst)
+ |> map snd |> SOME
+ else
+ NONE)
+ val n = length cluster_substs
+ fun do_cluster_subst cluster_subst =
+ map (instantiate_forall_tac thy params) cluster_subst @ [rotate_tac 1]
+ val params' = params (* FIXME ### existentials! *)
+ val first_prem = find_index (fn (ax_no', _) => ax_no' = ax_no) substs
+ in
+ rotate_tac first_prem
+ THEN' (EVERY' (maps do_cluster_subst cluster_substs))
+ THEN' rotate_tac (~ first_prem - length cluster_substs)
+ THEN' release_clusters_tac thy ax_counts substs params' clusters
+ end
+
+val cluster_ord =
+ prod_ord (prod_ord int_ord (prod_ord int_ord int_ord)) bool_ord
+
+val tysubst_ord =
+ list_ord (prod_ord Term_Ord.fast_indexname_ord
+ (prod_ord Term_Ord.sort_ord Term_Ord.typ_ord))
+
+structure Int_Tysubst_Table =
+ Table(type key = int * (indexname * (sort * typ)) list
+ val ord = prod_ord int_ord tysubst_ord)
+
+(* Attempts to derive the theorem "False" from a theorem of the form
+ "P1 ==> ... ==> Pn ==> False", where the "Pi"s are to be discharged using the
+ specified axioms. The axioms have leading "All" and "Ex" quantifiers, which
+ must be eliminated first. *)
+fun discharge_skolem_premises ctxt axioms prems_imp_false =
+ if prop_of prems_imp_false aconv @{prop False} then
+ prems_imp_false
+ else
+ let
+ val thy = ProofContext.theory_of ctxt
+ (* distinguish variables with same name but different types *)
+ val prems_imp_false' =
+ prems_imp_false |> try (forall_intr_vars #> gen_all)
+ |> the_default prems_imp_false
+ val prems_imp_false =
+ if prop_of prems_imp_false aconv prop_of prems_imp_false' then
+ prems_imp_false
+ else
+ prems_imp_false'
+ fun match_term p =
+ let
+ val (tyenv, tenv) =
+ Pattern.first_order_match thy p (Vartab.empty, Vartab.empty)
+ val tsubst =
+ tenv |> Vartab.dest
+ |> sort (cluster_ord
+ o pairself (Meson_Clausify.cluster_of_zapped_var_name
+ o fst o fst))
+ |> map (Meson.term_pair_of
+ #> pairself (Envir.subst_term_types tyenv))
+ val tysubst = tyenv |> Vartab.dest
+ in (tysubst, tsubst) end
+ fun subst_info_for_prem subgoal_no prem =
+ case prem of
+ _ $ (Const (@{const_name skolem}, _) $ (_ $ t $ num)) =>
+ let val ax_no = HOLogic.dest_nat num in
+ (ax_no, (subgoal_no,
+ match_term (nth axioms ax_no |> the |> snd, t)))
+ end
+ | _ => raise TERM ("discharge_skolem_premises: Malformed premise",
+ [prem])
+ fun cluster_of_var_name skolem s =
+ let
+ val ((ax_no, (cluster_no, _)), skolem') =
+ Meson_Clausify.cluster_of_zapped_var_name s
+ in
+ if skolem' = skolem andalso cluster_no > 0 then
+ SOME (ax_no, cluster_no)
+ else
+ NONE
+ end
+ fun clusters_in_term skolem t =
+ Term.add_var_names t [] |> map_filter (cluster_of_var_name skolem o fst)
+ fun deps_for_term_subst (var, t) =
+ case clusters_in_term false var of
+ [] => NONE
+ | [(ax_no, cluster_no)] =>
+ SOME ((ax_no, cluster_no),
+ clusters_in_term true t
+ |> cluster_no > 1 ? cons (ax_no, cluster_no - 1))
+ | _ => raise TERM ("discharge_skolem_premises: Expected Var", [var])
+ val prems = Logic.strip_imp_prems (prop_of prems_imp_false)
+ val substs = prems |> map2 subst_info_for_prem (1 upto length prems)
+ |> sort (int_ord o pairself fst)
+ val depss = maps (map_filter deps_for_term_subst o snd o snd o snd) substs
+ val clusters = maps (op ::) depss
+ val ordered_clusters =
+ Int_Pair_Graph.empty
+ |> fold Int_Pair_Graph.default_node (map (rpair ()) clusters)
+ |> fold Int_Pair_Graph.add_deps_acyclic depss
+ |> Int_Pair_Graph.topological_order
+ handle Int_Pair_Graph.CYCLES _ =>
+ error "Cannot replay Metis proof in Isabelle without axiom of \
+ \choice."
+ val params0 =
+ [] |> fold (Term.add_vars o snd) (map_filter I axioms)
+ |> map (`(Meson_Clausify.cluster_of_zapped_var_name o fst o fst))
+ |> filter (fn (((_, (cluster_no, _)), skolem), _) =>
+ cluster_no = 0 andalso skolem)
+ |> sort shuffle_ord |> map snd
+ val ax_counts =
+ Int_Tysubst_Table.empty
+ |> fold (fn (ax_no, (_, (tysubst, _))) =>
+ Int_Tysubst_Table.map_default ((ax_no, tysubst), 0)
+ (Integer.add 1)) substs
+ |> Int_Tysubst_Table.dest
+(* for debugging:
+ fun string_for_subst_info (ax_no, (subgoal_no, (tysubst, tsubst))) =
+ "ax: " ^ string_of_int ax_no ^ "; asm: " ^ string_of_int subgoal_no ^
+ "; tysubst: " ^ PolyML.makestring tysubst ^ "; tsubst: {" ^
+ commas (map ((fn (s, t) => s ^ " |-> " ^ t)
+ o pairself (Syntax.string_of_term ctxt)) tsubst) ^ "}"
+ val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^
+ cat_lines (map string_for_subst_info substs))
+ val _ = tracing ("OUTERMOST SKOLEMS: " ^ PolyML.makestring params0)
+ val _ = tracing ("ORDERED CLUSTERS: " ^ PolyML.makestring ordered_clusters)
+ val _ = tracing ("AXIOM COUNTS: " ^ PolyML.makestring ax_counts)
+*)
+ fun rotation_for_subgoal i =
+ find_index (fn (_, (subgoal_no, _)) => subgoal_no = i) substs
+ in
+ Goal.prove ctxt [] [] @{prop False}
+ (K (cut_rules_tac
+ (map (fst o the o nth axioms o fst o fst) ax_counts) 1
+ THEN print_tac "cut:"
+ THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1)
+ THEN copy_prems_tac (map snd ax_counts) [] 1
+ THEN print_tac "eliminated exist and copied prems:"
+ THEN release_clusters_tac thy ax_counts substs params0
+ ordered_clusters 1
+ THEN print_tac "released clusters:"
+ THEN match_tac [prems_imp_false] 1
+ THEN print_tac "applied rule:"
+ THEN ALLGOALS (fn i =>
+ rtac @{thm skolem_COMBK_I} i
+ THEN rotate_tac (rotation_for_subgoal i) i
+ THEN PRIMITIVE (unify_first_prem_with_concl thy i)
+ THEN assume_tac i)))
+ end
+
+(* Main function to start Metis proof and reconstruction *)
+fun FOL_SOLVE mode ctxt cls ths0 =
+ let val thy = ProofContext.theory_of ctxt
+ val type_lits = Config.get ctxt type_lits
+ val new_skolemizer =
+ Config.get ctxt new_skolemizer orelse null (Meson_Choices.get ctxt)
+ val th_cls_pairs =
+ map2 (fn j => fn th =>
+ (Thm.get_name_hint th,
+ Meson_Clausify.cnf_axiom ctxt new_skolemizer j th))
+ (0 upto length ths0 - 1) ths0
+ val thss = map (snd o snd) th_cls_pairs
+ val dischargers = map (fst o snd) th_cls_pairs
+ val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
+ val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
+ val _ = trace_msg (fn () => "THEOREM CLAUSES")
+ val _ = app (app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th))) thss
+ val (mode, {axioms, tfrees, old_skolems}) =
+ build_logic_map mode ctxt type_lits cls thss
+ val _ = if null tfrees then ()
+ else (trace_msg (fn () => "TFREE CLAUSES");
+ app (fn TyLitFree ((s, _), (s', _)) =>
+ trace_msg (fn () => s ^ "(" ^ s' ^ ")")) tfrees)
+ val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS")
+ val thms = map #1 axioms
+ val _ = app (fn th => trace_msg (fn () => Metis_Thm.toString th)) thms
+ val _ = trace_msg (fn () => "mode = " ^ string_of_mode mode)
+ val _ = trace_msg (fn () => "START METIS PROVE PROCESS")
+ in
+ case filter (is_false o prop_of) cls of
+ false_th::_ => [false_th RS @{thm FalseE}]
+ | [] =>
+ case Metis_Resolution.new resolution_params {axioms = thms, conjecture = []}
+ |> Metis_Resolution.loop of
+ Metis_Resolution.Contradiction mth =>
+ let val _ = trace_msg (fn () => "METIS RECONSTRUCTION START: " ^
+ Metis_Thm.toString mth)
+ val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
+ (*add constraints arising from converting goal to clause form*)
+ val proof = Metis_Proof.proof mth
+ val result =
+ fold (replay_one_inference ctxt' mode old_skolems) proof axioms
+ and used = map_filter (used_axioms axioms) proof
+ val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:")
+ val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used
+ val unused = th_cls_pairs |> map_filter (fn (name, (_, cls)) =>
+ if have_common_thm used cls then NONE else SOME name)
+ in
+ if not (null cls) andalso not (have_common_thm used cls) then
+ warning "Metis: The assumptions are inconsistent."
+ else
+ ();
+ if not (null unused) then
+ warning ("Metis: Unused theorems: " ^ commas_quote unused
+ ^ ".")
+ else
+ ();
+ case result of
+ (_,ith)::_ =>
+ (trace_msg (fn () => "Success: " ^ Display.string_of_thm ctxt ith);
+ [discharge_skolem_premises ctxt dischargers ith])
+ | _ => (trace_msg (fn () => "Metis: No result"); [])
+ end
+ | Metis_Resolution.Satisfiable _ =>
+ (trace_msg (fn () => "Metis: No first-order proof with the lemmas supplied");
+ [])
+ end;
+
+(* Extensionalize "th", because that makes sense and that's what Sledgehammer
+ does, but also keep an unextensionalized version of "th" for backward
+ compatibility. *)
+fun also_extensionalize_theorem th =
+ let val th' = Meson_Clausify.extensionalize_theorem th in
+ if Thm.eq_thm (th, th') then [th]
+ else th :: Meson.make_clauses_unsorted [th']
+ end
+
+val neg_clausify =
+ single
+ #> Meson.make_clauses_unsorted
+ #> maps also_extensionalize_theorem
+ #> map Meson_Clausify.introduce_combinators_in_theorem
+ #> Meson.finish_cnf
+
+fun preskolem_tac ctxt st0 =
+ (if exists (Meson.has_too_many_clauses ctxt)
+ (Logic.prems_of_goal (prop_of st0) 1) then
+ cnf.cnfx_rewrite_tac ctxt 1
+ else
+ all_tac) st0
+
+val type_has_top_sort =
+ exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
+
+fun generic_metis_tac mode ctxt ths i st0 =
+ let
+ val _ = trace_msg (fn () =>
+ "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
+ in
+ if exists_type type_has_top_sort (prop_of st0) then
+ (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty)
+ else
+ Meson.MESON (preskolem_tac ctxt) (maps neg_clausify)
+ (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
+ ctxt i st0
+ end
+
+val metis_tac = generic_metis_tac HO
+val metisF_tac = generic_metis_tac FO
+val metisFT_tac = generic_metis_tac FT
+
+(* Whenever "X" has schematic type variables, we treat "using X by metis" as
+ "by (metis X)", to prevent "Subgoal.FOCUS" from freezing the type variables.
+ We don't do it for nonschematic facts "X" because this breaks a few proofs
+ (in the rare and subtle case where a proof relied on extensionality not being
+ applied) and brings few benefits. *)
+val has_tvar =
+ exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of
+fun method name mode =
+ Method.setup name (Attrib.thms >> (fn ths => fn ctxt =>
+ METHOD (fn facts =>
+ let
+ val (schem_facts, nonschem_facts) =
+ List.partition has_tvar facts
+ in
+ HEADGOAL (Method.insert_tac nonschem_facts THEN'
+ CHANGED_PROP
+ o generic_metis_tac mode ctxt (schem_facts @ ths))
+ end)))
+
+val setup =
+ type_lits_setup
+ #> new_skolemizer_setup
+ #> method @{binding metis} HO "Metis for FOL/HOL problems"
+ #> method @{binding metisF} FO "Metis for FOL problems"
+ #> method @{binding metisFT} FT
+ "Metis for FOL/HOL problems with fully-typed translation"
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Metis/metis_translate.ML Mon Oct 04 22:45:09 2010 +0200
@@ -0,0 +1,771 @@
+(* Title: HOL/Tools/Sledgehammer/metis_translate.ML
+ Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
+ Author: Kong W. Susanto, Cambridge University Computer Laboratory
+ Author: Lawrence C. Paulson, Cambridge University Computer Laboratory
+ Author: Jasmin Blanchette, TU Muenchen
+
+Translation of HOL to FOL for Metis.
+*)
+
+signature METIS_TRANSLATE =
+sig
+ type name = string * string
+ datatype type_literal =
+ TyLitVar of name * name |
+ TyLitFree of name * name
+ datatype arLit =
+ TConsLit of name * name * name list |
+ TVarLit of name * name
+ datatype arity_clause =
+ ArityClause of {name: string, conclLit: arLit, premLits: arLit list}
+ datatype class_rel_clause =
+ ClassRelClause of {name: string, subclass: name, superclass: name}
+ datatype combtyp =
+ CombTVar of name |
+ CombTFree of name |
+ CombType of name * combtyp list
+ datatype combterm =
+ CombConst of name * combtyp * combtyp list (* Const and Free *) |
+ CombVar of name * combtyp |
+ CombApp of combterm * combterm
+ datatype fol_literal = FOLLiteral of bool * combterm
+
+ datatype mode = FO | HO | FT
+ type logic_map =
+ {axioms: (Metis_Thm.thm * thm) list,
+ tfrees: type_literal list,
+ old_skolems: (string * term) list}
+
+ val type_wrapper_name : string
+ val bound_var_prefix : string
+ val schematic_var_prefix: string
+ val fixed_var_prefix: string
+ val tvar_prefix: string
+ val tfree_prefix: string
+ val const_prefix: string
+ val type_const_prefix: string
+ val class_prefix: string
+ val new_skolem_const_prefix : string
+ val invert_const: string -> string
+ val ascii_of: string -> string
+ val unascii_of: string -> string
+ val strip_prefix_and_unascii: string -> string -> string option
+ val make_bound_var : string -> string
+ val make_schematic_var : string * int -> string
+ val make_fixed_var : string -> string
+ val make_schematic_type_var : string * int -> string
+ val make_fixed_type_var : string -> string
+ val make_fixed_const : string -> string
+ val make_fixed_type_const : string -> string
+ val make_type_class : string -> string
+ val num_type_args: theory -> string -> int
+ val new_skolem_var_from_const: string -> indexname
+ val type_literals_for_types : typ list -> type_literal list
+ val make_class_rel_clauses :
+ theory -> class list -> class list -> class_rel_clause list
+ val make_arity_clauses :
+ theory -> string list -> class list -> class list * arity_clause list
+ val combtyp_of : combterm -> combtyp
+ val strip_combterm_comb : combterm -> combterm * combterm list
+ val combterm_from_term :
+ theory -> int -> (string * typ) list -> term -> combterm * typ list
+ val reveal_old_skolem_terms : (string * term) list -> term -> term
+ val tfree_classes_of_terms : term list -> string list
+ val tvar_classes_of_terms : term list -> string list
+ val type_consts_of_terms : theory -> term list -> string list
+ val string_of_mode : mode -> string
+ val build_logic_map :
+ mode -> Proof.context -> bool -> thm list -> thm list list
+ -> mode * logic_map
+end
+
+structure Metis_Translate : METIS_TRANSLATE =
+struct
+
+val type_wrapper_name = "ti"
+
+val bound_var_prefix = "B_"
+val schematic_var_prefix = "V_"
+val fixed_var_prefix = "v_"
+
+val tvar_prefix = "T_";
+val tfree_prefix = "t_";
+
+val const_prefix = "c_";
+val type_const_prefix = "tc_";
+val class_prefix = "class_";
+
+val skolem_const_prefix = "Sledgehammer" ^ Long_Name.separator ^ "Sko"
+val old_skolem_const_prefix = skolem_const_prefix ^ "o"
+val new_skolem_const_prefix = skolem_const_prefix ^ "n"
+
+fun union_all xss = fold (union (op =)) xss []
+
+(* Readable names for the more common symbolic functions. Do not mess with the
+ last nine entries of the table unless you know what you are doing. *)
+val const_trans_table =
+ Symtab.make [(@{type_name Product_Type.prod}, "prod"),
+ (@{type_name Sum_Type.sum}, "sum"),
+ (@{const_name HOL.eq}, "equal"),
+ (@{const_name HOL.conj}, "and"),
+ (@{const_name HOL.disj}, "or"),
+ (@{const_name HOL.implies}, "implies"),
+ (@{const_name Set.member}, "member"),
+ (@{const_name fequal}, "fequal"),
+ (@{const_name COMBI}, "COMBI"),
+ (@{const_name COMBK}, "COMBK"),
+ (@{const_name COMBB}, "COMBB"),
+ (@{const_name COMBC}, "COMBC"),
+ (@{const_name COMBS}, "COMBS"),
+ (@{const_name True}, "True"),
+ (@{const_name False}, "False"),
+ (@{const_name If}, "If")]
+
+(* Invert the table of translations between Isabelle and ATPs. *)
+val const_trans_table_inv =
+ Symtab.update ("fequal", @{const_name HOL.eq})
+ (Symtab.make (map swap (Symtab.dest const_trans_table)))
+
+val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
+
+(*Escaping of special characters.
+ Alphanumeric characters are left unchanged.
+ The character _ goes to __
+ Characters in the range ASCII space to / go to _A to _P, respectively.
+ Other characters go to _nnn where nnn is the decimal ASCII code.*)
+val A_minus_space = Char.ord #"A" - Char.ord #" ";
+
+fun stringN_of_int 0 _ = ""
+ | stringN_of_int k n = stringN_of_int (k-1) (n div 10) ^ Int.toString (n mod 10);
+
+fun ascii_of_c c =
+ if Char.isAlphaNum c then String.str c
+ else if c = #"_" then "__"
+ else if #" " <= c andalso c <= #"/"
+ then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space))
+ else ("_" ^ stringN_of_int 3 (Char.ord c)) (*fixed width, in case more digits follow*)
+
+val ascii_of = String.translate ascii_of_c;
+
+(** Remove ASCII armouring from names in proof files **)
+
+(*We don't raise error exceptions because this code can run inside the watcher.
+ Also, the errors are "impossible" (hah!)*)
+fun unascii_aux rcs [] = String.implode(rev rcs)
+ | unascii_aux rcs [#"_"] = unascii_aux (#"_"::rcs) [] (*ERROR*)
+ (*Three types of _ escapes: __, _A to _P, _nnn*)
+ | unascii_aux rcs (#"_" :: #"_" :: cs) = unascii_aux (#"_"::rcs) cs
+ | unascii_aux rcs (#"_" :: c :: cs) =
+ if #"A" <= c andalso c<= #"P" (*translation of #" " to #"/"*)
+ then unascii_aux (Char.chr(Char.ord c - A_minus_space) :: rcs) cs
+ else
+ let val digits = List.take (c::cs, 3) handle Subscript => []
+ in
+ case Int.fromString (String.implode digits) of
+ NONE => unascii_aux (c:: #"_"::rcs) cs (*ERROR*)
+ | SOME n => unascii_aux (Char.chr n :: rcs) (List.drop (cs, 2))
+ end
+ | unascii_aux rcs (c::cs) = unascii_aux (c::rcs) cs
+val unascii_of = unascii_aux [] o String.explode
+
+(* If string s has the prefix s1, return the result of deleting it,
+ un-ASCII'd. *)
+fun strip_prefix_and_unascii s1 s =
+ if String.isPrefix s1 s then
+ SOME (unascii_of (String.extract (s, size s1, NONE)))
+ else
+ NONE
+
+(*Remove the initial ' character from a type variable, if it is present*)
+fun trim_type_var s =
+ if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE)
+ else error ("trim_type: Malformed type variable encountered: " ^ s);
+
+fun ascii_of_indexname (v,0) = ascii_of v
+ | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ Int.toString i;
+
+fun make_bound_var x = bound_var_prefix ^ ascii_of x
+fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v
+fun make_fixed_var x = fixed_var_prefix ^ ascii_of x
+
+fun make_schematic_type_var (x,i) =
+ tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i));
+fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x));
+
+fun lookup_const c =
+ case Symtab.lookup const_trans_table c of
+ SOME c' => c'
+ | NONE => ascii_of c
+
+(* HOL.eq MUST BE "equal" because it's built into ATPs. *)
+fun make_fixed_const @{const_name HOL.eq} = "equal"
+ | make_fixed_const c = const_prefix ^ lookup_const c
+
+fun make_fixed_type_const c = type_const_prefix ^ lookup_const c
+
+fun make_type_class clas = class_prefix ^ ascii_of clas;
+
+(* The number of type arguments of a constant, zero if it's monomorphic. For
+ (instances of) Skolem pseudoconstants, this information is encoded in the
+ constant name. *)
+fun num_type_args thy s =
+ if String.isPrefix skolem_const_prefix s then
+ s |> space_explode Long_Name.separator |> List.last |> Int.fromString |> the
+ else
+ (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
+
+fun new_skolem_var_from_const s =
+ let
+ val ss = s |> space_explode Long_Name.separator
+ val n = length ss
+ in (nth ss (n - 2), nth ss (n - 3) |> Int.fromString |> the) end
+
+
+(**** Definitions and functions for FOL clauses for TPTP format output ****)
+
+type name = string * string
+
+(**** Isabelle FOL clauses ****)
+
+(* The first component is the type class; the second is a TVar or TFree. *)
+datatype type_literal =
+ TyLitVar of name * name |
+ TyLitFree of name * name
+
+(*Make literals for sorted type variables*)
+fun sorts_on_typs_aux (_, []) = []
+ | sorts_on_typs_aux ((x,i), s::ss) =
+ let val sorts = sorts_on_typs_aux ((x,i), ss)
+ in
+ if s = "HOL.type" then sorts
+ else if i = ~1 then TyLitFree (`make_type_class s, `make_fixed_type_var x) :: sorts
+ else TyLitVar (`make_type_class s, (make_schematic_type_var (x,i), x)) :: sorts
+ end;
+
+fun sorts_on_typs (TFree (a,s)) = sorts_on_typs_aux ((a,~1),s)
+ | sorts_on_typs (TVar (v,s)) = sorts_on_typs_aux (v,s);
+
+(*Given a list of sorted type variables, return a list of type literals.*)
+fun type_literals_for_types Ts =
+ fold (union (op =)) (map sorts_on_typs Ts) []
+
+(** make axiom and conjecture clauses. **)
+
+(**** Isabelle arities ****)
+
+datatype arLit =
+ TConsLit of name * name * name list |
+ TVarLit of name * name
+
+datatype arity_clause =
+ ArityClause of {name: string, conclLit: arLit, premLits: arLit list}
+
+
+fun gen_TVars 0 = []
+ | gen_TVars n = ("T_" ^ Int.toString n) :: gen_TVars (n-1);
+
+fun pack_sort(_,[]) = []
+ | pack_sort(tvar, "HOL.type"::srt) = pack_sort (tvar, srt) (*IGNORE sort "type"*)
+ | pack_sort(tvar, cls::srt) =
+ (`make_type_class cls, (tvar, tvar)) :: pack_sort (tvar, srt)
+
+(*Arity of type constructor tcon :: (arg1,...,argN)res*)
+fun make_axiom_arity_clause (tcons, name, (cls,args)) =
+ let
+ val tvars = gen_TVars (length args)
+ val tvars_srts = ListPair.zip (tvars, args)
+ in
+ ArityClause {name = name,
+ conclLit = TConsLit (`make_type_class cls,
+ `make_fixed_type_const tcons,
+ tvars ~~ tvars),
+ premLits = map TVarLit (union_all (map pack_sort tvars_srts))}
+ end
+
+
+(**** Isabelle class relations ****)
+
+datatype class_rel_clause =
+ ClassRelClause of {name: string, subclass: name, superclass: name}
+
+(*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)
+fun class_pairs _ [] _ = []
+ | class_pairs thy subs supers =
+ let
+ val class_less = Sorts.class_less (Sign.classes_of thy)
+ fun add_super sub super = class_less (sub, super) ? cons (sub, super)
+ fun add_supers sub = fold (add_super sub) supers
+ in fold add_supers subs [] end
+
+fun make_class_rel_clause (sub,super) =
+ ClassRelClause {name = sub ^ "_" ^ super,
+ subclass = `make_type_class sub,
+ superclass = `make_type_class super}
+
+fun make_class_rel_clauses thy subs supers =
+ map make_class_rel_clause (class_pairs thy subs supers);
+
+
+(** Isabelle arities **)
+
+fun arity_clause _ _ (_, []) = []
+ | arity_clause seen n (tcons, ("HOL.type",_)::ars) = (*ignore*)
+ arity_clause seen n (tcons,ars)
+ | arity_clause seen n (tcons, (ar as (class,_)) :: ars) =
+ if member (op =) seen class then (*multiple arities for the same tycon, class pair*)
+ make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) ::
+ arity_clause seen (n+1) (tcons,ars)
+ else
+ make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class, ar) ::
+ arity_clause (class::seen) n (tcons,ars)
+
+fun multi_arity_clause [] = []
+ | multi_arity_clause ((tcons, ars) :: tc_arlists) =
+ arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists
+
+(*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy
+ provided its arguments have the corresponding sorts.*)
+fun type_class_pairs thy tycons classes =
+ let val alg = Sign.classes_of thy
+ fun domain_sorts tycon = Sorts.mg_domain alg tycon o single
+ fun add_class tycon class =
+ cons (class, domain_sorts tycon class)
+ handle Sorts.CLASS_ERROR _ => I
+ fun try_classes tycon = (tycon, fold (add_class tycon) classes [])
+ in map try_classes tycons end;
+
+(*Proving one (tycon, class) membership may require proving others, so iterate.*)
+fun iter_type_class_pairs _ _ [] = ([], [])
+ | iter_type_class_pairs thy tycons classes =
+ let val cpairs = type_class_pairs thy tycons classes
+ val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs)))
+ |> subtract (op =) classes |> subtract (op =) HOLogic.typeS
+ val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
+ in (union (op =) classes' classes, union (op =) cpairs' cpairs) end;
+
+fun make_arity_clauses thy tycons classes =
+ let val (classes', cpairs) = iter_type_class_pairs thy tycons classes
+ in (classes', multi_arity_clause cpairs) end;
+
+datatype combtyp =
+ CombTVar of name |
+ CombTFree of name |
+ CombType of name * combtyp list
+
+datatype combterm =
+ CombConst of name * combtyp * combtyp list (* Const and Free *) |
+ CombVar of name * combtyp |
+ CombApp of combterm * combterm
+
+datatype fol_literal = FOLLiteral of bool * combterm
+
+(*********************************************************************)
+(* convert a clause with type Term.term to a clause with type clause *)
+(*********************************************************************)
+
+(*Result of a function type; no need to check that the argument type matches.*)
+fun result_type (CombType (_, [_, tp2])) = tp2
+ | result_type _ = raise Fail "non-function type"
+
+fun combtyp_of (CombConst (_, tp, _)) = tp
+ | combtyp_of (CombVar (_, tp)) = tp
+ | combtyp_of (CombApp (t1, _)) = result_type (combtyp_of t1)
+
+(*gets the head of a combinator application, along with the list of arguments*)
+fun strip_combterm_comb u =
+ let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
+ | stripc x = x
+ in stripc(u,[]) end
+
+fun combtype_of (Type (a, Ts)) =
+ let val (folTypes, ts) = combtypes_of Ts in
+ (CombType (`make_fixed_type_const a, folTypes), ts)
+ end
+ | combtype_of (tp as TFree (a, _)) = (CombTFree (`make_fixed_type_var a), [tp])
+ | combtype_of (tp as TVar (x, _)) =
+ (CombTVar (make_schematic_type_var x, string_of_indexname x), [tp])
+and combtypes_of Ts =
+ let val (folTyps, ts) = ListPair.unzip (map combtype_of Ts) in
+ (folTyps, union_all ts)
+ end
+
+(* same as above, but no gathering of sort information *)
+fun simple_combtype_of (Type (a, Ts)) =
+ CombType (`make_fixed_type_const a, map simple_combtype_of Ts)
+ | simple_combtype_of (TFree (a, _)) = CombTFree (`make_fixed_type_var a)
+ | simple_combtype_of (TVar (x, _)) =
+ CombTVar (make_schematic_type_var x, string_of_indexname x)
+
+fun new_skolem_const_name th_no s num_T_args =
+ [new_skolem_const_prefix, string_of_int th_no, s, string_of_int num_T_args]
+ |> space_implode Long_Name.separator
+
+(* Converts a term (with combinators) into a combterm. Also accummulates sort
+ infomation. *)
+fun combterm_from_term thy th_no bs (P $ Q) =
+ let val (P', tsP) = combterm_from_term thy th_no bs P
+ val (Q', tsQ) = combterm_from_term thy th_no bs Q
+ in (CombApp (P', Q'), union (op =) tsP tsQ) end
+ | combterm_from_term thy _ _ (Const (c, T)) =
+ let
+ val (tp, ts) = combtype_of T
+ val tvar_list =
+ (if String.isPrefix old_skolem_const_prefix c then
+ [] |> Term.add_tvarsT T |> map TVar
+ else
+ (c, T) |> Sign.const_typargs thy)
+ |> map simple_combtype_of
+ val c' = CombConst (`make_fixed_const c, tp, tvar_list)
+ in (c',ts) end
+ | combterm_from_term _ _ _ (Free (v, T)) =
+ let val (tp, ts) = combtype_of T
+ val v' = CombConst (`make_fixed_var v, tp, [])
+ in (v',ts) end
+ | combterm_from_term _ th_no _ (Var (v as (s, _), T)) =
+ let
+ val (tp, ts) = combtype_of T
+ val v' =
+ if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
+ let
+ val tys = T |> strip_type |> swap |> op ::
+ val s' = new_skolem_const_name th_no s (length tys)
+ in
+ CombConst (`make_fixed_const s', tp, map simple_combtype_of tys)
+ end
+ else
+ CombVar ((make_schematic_var v, string_of_indexname v), tp)
+ in (v', ts) end
+ | combterm_from_term _ _ bs (Bound j) =
+ let
+ val (s, T) = nth bs j
+ val (tp, ts) = combtype_of T
+ val v' = CombConst (`make_bound_var s, tp, [])
+ in (v', ts) end
+ | combterm_from_term _ _ _ (Abs _) = raise Fail "HOL clause: Abs"
+
+fun predicate_of thy th_no ((@{const Not} $ P), pos) =
+ predicate_of thy th_no (P, not pos)
+ | predicate_of thy th_no (t, pos) =
+ (combterm_from_term thy th_no [] (Envir.eta_contract t), pos)
+
+fun literals_of_term1 args thy th_no (@{const Trueprop} $ P) =
+ literals_of_term1 args thy th_no P
+ | literals_of_term1 args thy th_no (@{const HOL.disj} $ P $ Q) =
+ literals_of_term1 (literals_of_term1 args thy th_no P) thy th_no Q
+ | literals_of_term1 (lits, ts) thy th_no P =
+ let val ((pred, ts'), pol) = predicate_of thy th_no (P, true) in
+ (FOLLiteral (pol, pred) :: lits, union (op =) ts ts')
+ end
+val literals_of_term = literals_of_term1 ([], [])
+
+fun old_skolem_const_name i j num_T_args =
+ old_skolem_const_prefix ^ Long_Name.separator ^
+ (space_implode Long_Name.separator (map Int.toString [i, j, num_T_args]))
+
+fun conceal_old_skolem_terms i old_skolems t =
+ if exists_Const (curry (op =) @{const_name skolem} o fst) t then
+ let
+ fun aux old_skolems
+ (t as (Const (@{const_name skolem}, Type (_, [_, T])) $ _)) =
+ let
+ val (old_skolems, s) =
+ if i = ~1 then
+ (old_skolems, @{const_name undefined})
+ else case AList.find (op aconv) old_skolems t of
+ s :: _ => (old_skolems, s)
+ | [] =>
+ let
+ val s = old_skolem_const_name i (length old_skolems)
+ (length (Term.add_tvarsT T []))
+ in ((s, t) :: old_skolems, s) end
+ in (old_skolems, Const (s, T)) end
+ | aux old_skolems (t1 $ t2) =
+ let
+ val (old_skolems, t1) = aux old_skolems t1
+ val (old_skolems, t2) = aux old_skolems t2
+ in (old_skolems, t1 $ t2) end
+ | aux old_skolems (Abs (s, T, t')) =
+ let val (old_skolems, t') = aux old_skolems t' in
+ (old_skolems, Abs (s, T, t'))
+ end
+ | aux old_skolems t = (old_skolems, t)
+ in aux old_skolems t end
+ else
+ (old_skolems, t)
+
+fun reveal_old_skolem_terms old_skolems =
+ map_aterms (fn t as Const (s, _) =>
+ if String.isPrefix old_skolem_const_prefix s then
+ AList.lookup (op =) old_skolems s |> the
+ |> map_types Type_Infer.paramify_vars
+ else
+ t
+ | t => t)
+
+
+(***************************************************************)
+(* Type Classes Present in the Axiom or Conjecture Clauses *)
+(***************************************************************)
+
+fun set_insert (x, s) = Symtab.update (x, ()) s
+
+fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts)
+
+(*Remove this trivial type class*)
+fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset;
+
+fun tfree_classes_of_terms ts =
+ let val sorts_list = map (map #2 o OldTerm.term_tfrees) ts
+ in Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list)) end;
+
+fun tvar_classes_of_terms ts =
+ let val sorts_list = map (map #2 o OldTerm.term_tvars) ts
+ in Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list)) end;
+
+(*fold type constructors*)
+fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x))
+ | fold_type_consts _ _ x = x;
+
+(*Type constructors used to instantiate overloaded constants are the only ones needed.*)
+fun add_type_consts_in_term thy =
+ let
+ fun aux (Const x) =
+ fold (fold_type_consts set_insert) (Sign.const_typargs thy x)
+ | aux (Abs (_, _, u)) = aux u
+ | aux (Const (@{const_name skolem}, _) $ _) = I
+ | aux (t $ u) = aux t #> aux u
+ | aux _ = I
+ in aux end
+
+fun type_consts_of_terms thy ts =
+ Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty);
+
+(* ------------------------------------------------------------------------- *)
+(* HOL to FOL (Isabelle to Metis) *)
+(* ------------------------------------------------------------------------- *)
+
+datatype mode = FO | HO | FT (* first-order, higher-order, fully-typed *)
+
+fun string_of_mode FO = "FO"
+ | string_of_mode HO = "HO"
+ | string_of_mode FT = "FT"
+
+fun fn_isa_to_met_sublevel "equal" = "=" (* FIXME: "c_fequal" *)
+ | fn_isa_to_met_sublevel x = x
+fun fn_isa_to_met_toplevel "equal" = "="
+ | fn_isa_to_met_toplevel x = x
+
+fun metis_lit b c args = (b, (c, args));
+
+fun metis_term_from_combtyp (CombTVar (s, _)) = Metis_Term.Var s
+ | metis_term_from_combtyp (CombTFree (s, _)) = Metis_Term.Fn (s, [])
+ | metis_term_from_combtyp (CombType ((s, _), tps)) =
+ Metis_Term.Fn (s, map metis_term_from_combtyp tps);
+
+(*These two functions insert type literals before the real literals. That is the
+ opposite order from TPTP linkup, but maybe OK.*)
+
+fun hol_term_to_fol_FO tm =
+ case strip_combterm_comb tm of
+ (CombConst ((c, _), _, tys), tms) =>
+ let val tyargs = map metis_term_from_combtyp tys
+ val args = map hol_term_to_fol_FO tms
+ in Metis_Term.Fn (c, tyargs @ args) end
+ | (CombVar ((v, _), _), []) => Metis_Term.Var v
+ | _ => raise Fail "non-first-order combterm"
+
+fun hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) =
+ Metis_Term.Fn (fn_isa_to_met_sublevel a, map metis_term_from_combtyp tylist)
+ | hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis_Term.Var s
+ | hol_term_to_fol_HO (CombApp (tm1, tm2)) =
+ Metis_Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]);
+
+(*The fully-typed translation, to avoid type errors*)
+fun wrap_type (tm, ty) =
+ Metis_Term.Fn (type_wrapper_name, [tm, metis_term_from_combtyp ty])
+
+fun hol_term_to_fol_FT (CombVar ((s, _), ty)) = wrap_type (Metis_Term.Var s, ty)
+ | hol_term_to_fol_FT (CombConst((a, _), ty, _)) =
+ wrap_type (Metis_Term.Fn(fn_isa_to_met_sublevel a, []), ty)
+ | hol_term_to_fol_FT (tm as CombApp(tm1,tm2)) =
+ wrap_type (Metis_Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]),
+ combtyp_of tm)
+
+fun hol_literal_to_fol FO (FOLLiteral (pos, tm)) =
+ let val (CombConst((p, _), _, tys), tms) = strip_combterm_comb tm
+ val tylits = if p = "equal" then [] else map metis_term_from_combtyp tys
+ val lits = map hol_term_to_fol_FO tms
+ in metis_lit pos (fn_isa_to_met_toplevel p) (tylits @ lits) end
+ | hol_literal_to_fol HO (FOLLiteral (pos, tm)) =
+ (case strip_combterm_comb tm of
+ (CombConst(("equal", _), _, _), tms) =>
+ metis_lit pos "=" (map hol_term_to_fol_HO tms)
+ | _ => metis_lit pos "{}" [hol_term_to_fol_HO tm]) (*hBOOL*)
+ | hol_literal_to_fol FT (FOLLiteral (pos, tm)) =
+ (case strip_combterm_comb tm of
+ (CombConst(("equal", _), _, _), tms) =>
+ metis_lit pos "=" (map hol_term_to_fol_FT tms)
+ | _ => metis_lit pos "{}" [hol_term_to_fol_FT tm]) (*hBOOL*);
+
+fun literals_of_hol_term thy th_no mode t =
+ let val (lits, types_sorts) = literals_of_term thy th_no t
+ in (map (hol_literal_to_fol mode) lits, types_sorts) end;
+
+(*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*)
+fun metis_of_type_literals pos (TyLitVar ((s, _), (s', _))) =
+ metis_lit pos s [Metis_Term.Var s']
+ | metis_of_type_literals pos (TyLitFree ((s, _), (s', _))) =
+ metis_lit pos s [Metis_Term.Fn (s',[])]
+
+fun default_sort _ (TVar _) = false
+ | default_sort ctxt (TFree (x, s)) = (s = the_default [] (Variable.def_sort ctxt (x, ~1)));
+
+fun metis_of_tfree tf =
+ Metis_Thm.axiom (Metis_LiteralSet.singleton (metis_of_type_literals true tf));
+
+fun hol_thm_to_fol is_conjecture th_no ctxt type_lits mode j old_skolems th =
+ let
+ val thy = ProofContext.theory_of ctxt
+ val (old_skolems, (mlits, types_sorts)) =
+ th |> prop_of |> Logic.strip_imp_concl
+ |> conceal_old_skolem_terms j old_skolems
+ ||> (HOLogic.dest_Trueprop #> literals_of_hol_term thy th_no mode)
+ in
+ if is_conjecture then
+ (Metis_Thm.axiom (Metis_LiteralSet.fromList mlits),
+ type_literals_for_types types_sorts, old_skolems)
+ else
+ let
+ val tylits = filter_out (default_sort ctxt) types_sorts
+ |> type_literals_for_types
+ val mtylits =
+ if type_lits then map (metis_of_type_literals false) tylits else []
+ in
+ (Metis_Thm.axiom (Metis_LiteralSet.fromList(mtylits @ mlits)), [],
+ old_skolems)
+ end
+ end;
+
+val helpers =
+ [("c_COMBI", (false, map (`I) @{thms COMBI_def})),
+ ("c_COMBK", (false, map (`I) @{thms COMBK_def})),
+ ("c_COMBB", (false, map (`I) @{thms COMBB_def})),
+ ("c_COMBC", (false, map (`I) @{thms COMBC_def})),
+ ("c_COMBS", (false, map (`I) @{thms COMBS_def})),
+ ("c_fequal", (false, map (rpair @{thm equal_imp_equal})
+ @{thms fequal_imp_equal equal_imp_fequal})),
+ ("c_True", (true, map (`I) @{thms True_or_False})),
+ ("c_False", (true, map (`I) @{thms True_or_False})),
+ ("c_If", (true, map (`I) @{thms if_True if_False True_or_False}))]
+
+(* ------------------------------------------------------------------------- *)
+(* Logic maps manage the interface between HOL and first-order logic. *)
+(* ------------------------------------------------------------------------- *)
+
+type logic_map =
+ {axioms: (Metis_Thm.thm * thm) list,
+ tfrees: type_literal list,
+ old_skolems: (string * term) list}
+
+fun is_quasi_fol_clause thy =
+ Meson.is_fol_term thy o snd o conceal_old_skolem_terms ~1 [] o prop_of
+
+(*Extract TFree constraints from context to include as conjecture clauses*)
+fun init_tfrees ctxt =
+ let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts in
+ Vartab.fold add (#2 (Variable.constraints_of ctxt)) []
+ |> type_literals_for_types
+ end;
+
+(*Insert non-logical axioms corresponding to all accumulated TFrees*)
+fun add_tfrees {axioms, tfrees, old_skolems} : logic_map =
+ {axioms = map (rpair TrueI o metis_of_tfree) (distinct (op =) tfrees) @
+ axioms,
+ tfrees = tfrees, old_skolems = old_skolems}
+
+(*transform isabelle type / arity clause to metis clause *)
+fun add_type_thm [] lmap = lmap
+ | add_type_thm ((ith, mth) :: cls) {axioms, tfrees, old_skolems} =
+ add_type_thm cls {axioms = (mth, ith) :: axioms, tfrees = tfrees,
+ old_skolems = old_skolems}
+
+fun const_in_metis c (pred, tm_list) =
+ let
+ fun in_mterm (Metis_Term.Var _) = false
+ | in_mterm (Metis_Term.Fn (".", tm_list)) = exists in_mterm tm_list
+ | in_mterm (Metis_Term.Fn (nm, tm_list)) = c=nm orelse exists in_mterm tm_list
+ in c = pred orelse exists in_mterm tm_list end;
+
+(* ARITY CLAUSE *)
+fun m_arity_cls (TConsLit ((c, _), (t, _), args)) =
+ metis_lit true c [Metis_Term.Fn(t, map (Metis_Term.Var o fst) args)]
+ | m_arity_cls (TVarLit ((c, _), (s, _))) =
+ metis_lit false c [Metis_Term.Var s]
+(*TrueI is returned as the Isabelle counterpart because there isn't any.*)
+fun arity_cls (ArityClause {conclLit, premLits, ...}) =
+ (TrueI,
+ Metis_Thm.axiom (Metis_LiteralSet.fromList (map m_arity_cls (conclLit :: premLits))));
+
+(* CLASSREL CLAUSE *)
+fun m_class_rel_cls (subclass, _) (superclass, _) =
+ [metis_lit false subclass [Metis_Term.Var "T"], metis_lit true superclass [Metis_Term.Var "T"]];
+fun class_rel_cls (ClassRelClause {subclass, superclass, ...}) =
+ (TrueI, Metis_Thm.axiom (Metis_LiteralSet.fromList (m_class_rel_cls subclass superclass)));
+
+fun type_ext thy tms =
+ let val subs = tfree_classes_of_terms tms
+ val supers = tvar_classes_of_terms tms
+ and tycons = type_consts_of_terms thy tms
+ val (supers', arity_clauses) = make_arity_clauses thy tycons supers
+ val class_rel_clauses = make_class_rel_clauses thy subs supers'
+ in map class_rel_cls class_rel_clauses @ map arity_cls arity_clauses
+ end;
+
+(* Function to generate metis clauses, including comb and type clauses *)
+fun build_logic_map mode0 ctxt type_lits cls thss =
+ let val thy = ProofContext.theory_of ctxt
+ (*The modes FO and FT are sticky. HO can be downgraded to FO.*)
+ fun set_mode FO = FO
+ | set_mode HO =
+ if forall (forall (is_quasi_fol_clause thy)) (cls :: thss) then FO
+ else HO
+ | set_mode FT = FT
+ val mode = set_mode mode0
+ (*transform isabelle clause to metis clause *)
+ fun add_thm th_no is_conjecture (metis_ith, isa_ith)
+ {axioms, tfrees, old_skolems} : logic_map =
+ let
+ val (mth, tfree_lits, old_skolems) =
+ hol_thm_to_fol is_conjecture th_no ctxt type_lits mode (length axioms)
+ old_skolems metis_ith
+ in
+ {axioms = (mth, Meson.make_meta_clause isa_ith) :: axioms,
+ tfrees = union (op =) tfree_lits tfrees, old_skolems = old_skolems}
+ end;
+ val lmap = {axioms = [], tfrees = init_tfrees ctxt, old_skolems = []}
+ |> fold (add_thm 0 true o `I) cls
+ |> add_tfrees
+ |> fold (fn (th_no, ths) => fold (add_thm th_no false o `I) ths)
+ (1 upto length thss ~~ thss)
+ val clause_lists = map (Metis_Thm.clause o #1) (#axioms lmap)
+ fun is_used c =
+ exists (Metis_LiteralSet.exists (const_in_metis c o #2)) clause_lists
+ val lmap =
+ if mode = FO then
+ lmap
+ else
+ let
+ val helper_ths =
+ helpers |> filter (is_used o fst)
+ |> maps (fn (c, (needs_full_types, thms)) =>
+ if not (is_used c) orelse
+ needs_full_types andalso mode <> FT then
+ []
+ else
+ thms)
+ in lmap |> fold (add_thm ~1 false) helper_ths end
+ in
+ (mode, add_type_thm (type_ext thy (maps (map prop_of) (cls :: thss))) lmap)
+ end
+
+end;
--- a/src/HOL/Tools/Sledgehammer/metis_reconstruct.ML Mon Oct 04 22:01:34 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,557 +0,0 @@
-(* Title: HOL/Tools/Sledgehammer/metis_reconstruct.ML
- Author: Kong W. Susanto, Cambridge University Computer Laboratory
- Author: Lawrence C. Paulson, Cambridge University Computer Laboratory
- Author: Jasmin Blanchette, TU Muenchen
- Copyright Cambridge University 2007
-
-Proof reconstruction for Metis.
-*)
-
-signature METIS_RECONSTRUCT =
-sig
- type mode = Metis_Translate.mode
-
- val trace : bool Unsynchronized.ref
- val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
- val untyped_aconv : term -> term -> bool
- val replay_one_inference :
- Proof.context -> mode -> (string * term) list
- -> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list
- -> (Metis_Thm.thm * thm) list
-end;
-
-structure Metis_Reconstruct : METIS_RECONSTRUCT =
-struct
-
-open Metis_Translate
-
-val trace = Unsynchronized.ref false
-fun trace_msg msg = if !trace then tracing (msg ()) else ()
-
-datatype term_or_type = SomeTerm of term | SomeType of typ
-
-fun terms_of [] = []
- | terms_of (SomeTerm t :: tts) = t :: terms_of tts
- | terms_of (SomeType _ :: tts) = terms_of tts;
-
-fun types_of [] = []
- | types_of (SomeTerm (Var ((a,idx), _)) :: tts) =
- if String.isPrefix "_" a then
- (*Variable generated by Metis, which might have been a type variable.*)
- TVar (("'" ^ a, idx), HOLogic.typeS) :: types_of tts
- else types_of tts
- | types_of (SomeTerm _ :: tts) = types_of tts
- | types_of (SomeType T :: tts) = T :: types_of tts;
-
-fun apply_list rator nargs rands =
- let val trands = terms_of rands
- in if length trands = nargs then SomeTerm (list_comb(rator, trands))
- else raise Fail
- ("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global Pure.thy rator ^
- " expected " ^ Int.toString nargs ^
- " received " ^ commas (map (Syntax.string_of_term_global Pure.thy) trands))
- end;
-
-fun infer_types ctxt =
- Syntax.check_terms (ProofContext.set_mode ProofContext.mode_pattern ctxt);
-
-(*We use 1 rather than 0 because variable references in clauses may otherwise conflict
- with variable constraints in the goal...at least, type inference often fails otherwise.
- SEE ALSO axiom_inf below.*)
-fun mk_var (w, T) = Var ((w, 1), T)
-
-(*include the default sort, if available*)
-fun mk_tfree ctxt w =
- let val ww = "'" ^ w
- in TFree(ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1))) end;
-
-(*Remove the "apply" operator from an HO term*)
-fun strip_happ args (Metis_Term.Fn(".",[t,u])) = strip_happ (u::args) t
- | strip_happ args x = (x, args);
-
-fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS)
-
-fun smart_invert_const "fequal" = @{const_name HOL.eq}
- | smart_invert_const s = invert_const s
-
-fun hol_type_from_metis_term _ (Metis_Term.Var v) =
- (case strip_prefix_and_unascii tvar_prefix v of
- SOME w => make_tvar w
- | NONE => make_tvar v)
- | hol_type_from_metis_term ctxt (Metis_Term.Fn(x, tys)) =
- (case strip_prefix_and_unascii type_const_prefix x of
- SOME tc => Type (smart_invert_const tc,
- map (hol_type_from_metis_term ctxt) tys)
- | NONE =>
- case strip_prefix_and_unascii tfree_prefix x of
- SOME tf => mk_tfree ctxt tf
- | NONE => raise Fail ("hol_type_from_metis_term: " ^ x));
-
-(*Maps metis terms to isabelle terms*)
-fun hol_term_from_metis_PT ctxt fol_tm =
- let val thy = ProofContext.theory_of ctxt
- val _ = trace_msg (fn () => "hol_term_from_metis_PT: " ^
- Metis_Term.toString fol_tm)
- fun tm_to_tt (Metis_Term.Var v) =
- (case strip_prefix_and_unascii tvar_prefix v of
- SOME w => SomeType (make_tvar w)
- | NONE =>
- case strip_prefix_and_unascii schematic_var_prefix v of
- SOME w => SomeTerm (mk_var (w, HOLogic.typeT))
- | NONE => SomeTerm (mk_var (v, HOLogic.typeT)) )
- (*Var from Metis with a name like _nnn; possibly a type variable*)
- | tm_to_tt (Metis_Term.Fn ("{}", [arg])) = tm_to_tt arg (*hBOOL*)
- | tm_to_tt (t as Metis_Term.Fn (".",_)) =
- let val (rator,rands) = strip_happ [] t
- in case rator of
- Metis_Term.Fn(fname,ts) => applic_to_tt (fname, ts @ rands)
- | _ => case tm_to_tt rator of
- SomeTerm t => SomeTerm (list_comb(t, terms_of (map tm_to_tt rands)))
- | _ => raise Fail "tm_to_tt: HO application"
- end
- | tm_to_tt (Metis_Term.Fn (fname, args)) = applic_to_tt (fname,args)
- and applic_to_tt ("=",ts) =
- SomeTerm (list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
- | applic_to_tt (a,ts) =
- case strip_prefix_and_unascii const_prefix a of
- SOME b =>
- let
- val c = smart_invert_const b
- val ntypes = num_type_args thy c
- val nterms = length ts - ntypes
- val tts = map tm_to_tt ts
- val tys = types_of (List.take(tts,ntypes))
- val t =
- if String.isPrefix new_skolem_const_prefix c then
- Var (new_skolem_var_from_const c,
- Type_Infer.paramify_vars (tl tys ---> hd tys))
- else
- Const (c, dummyT)
- in if length tys = ntypes then
- apply_list t nterms (List.drop(tts,ntypes))
- else
- raise Fail ("Constant " ^ c ^ " expects " ^ Int.toString ntypes ^
- " but gets " ^ Int.toString (length tys) ^
- " type arguments\n" ^
- cat_lines (map (Syntax.string_of_typ ctxt) tys) ^
- " the terms are \n" ^
- cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
- end
- | NONE => (*Not a constant. Is it a type constructor?*)
- case strip_prefix_and_unascii type_const_prefix a of
- SOME b =>
- SomeType (Type (smart_invert_const b, types_of (map tm_to_tt ts)))
- | NONE => (*Maybe a TFree. Should then check that ts=[].*)
- case strip_prefix_and_unascii tfree_prefix a of
- SOME b => SomeType (mk_tfree ctxt b)
- | NONE => (*a fixed variable? They are Skolem functions.*)
- case strip_prefix_and_unascii fixed_var_prefix a of
- SOME b =>
- let val opr = Free (b, HOLogic.typeT)
- in apply_list opr (length ts) (map tm_to_tt ts) end
- | NONE => raise Fail ("unexpected metis function: " ^ a)
- in
- case tm_to_tt fol_tm of
- SomeTerm t => t
- | SomeType T => raise TYPE ("fol_tm_to_tt: Term expected", [T], [])
- end
-
-(*Maps fully-typed metis terms to isabelle terms*)
-fun hol_term_from_metis_FT ctxt fol_tm =
- let val _ = trace_msg (fn () => "hol_term_from_metis_FT: " ^
- Metis_Term.toString fol_tm)
- fun cvt (Metis_Term.Fn ("ti", [Metis_Term.Var v, _])) =
- (case strip_prefix_and_unascii schematic_var_prefix v of
- SOME w => mk_var(w, dummyT)
- | NONE => mk_var(v, dummyT))
- | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn ("=",[]), _])) =
- Const (@{const_name HOL.eq}, HOLogic.typeT)
- | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn (x,[]), ty])) =
- (case strip_prefix_and_unascii const_prefix x of
- SOME c => Const (smart_invert_const c, dummyT)
- | NONE => (*Not a constant. Is it a fixed variable??*)
- case strip_prefix_and_unascii fixed_var_prefix x of
- SOME v => Free (v, hol_type_from_metis_term ctxt ty)
- | NONE => raise Fail ("hol_term_from_metis_FT bad constant: " ^ x))
- | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn (".",[tm1,tm2]), _])) =
- cvt tm1 $ cvt tm2
- | cvt (Metis_Term.Fn (".",[tm1,tm2])) = (*untyped application*)
- cvt tm1 $ cvt tm2
- | cvt (Metis_Term.Fn ("{}", [arg])) = cvt arg (*hBOOL*)
- | cvt (Metis_Term.Fn ("=", [tm1,tm2])) =
- list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), map cvt [tm1,tm2])
- | cvt (t as Metis_Term.Fn (x, [])) =
- (case strip_prefix_and_unascii const_prefix x of
- SOME c => Const (smart_invert_const c, dummyT)
- | NONE => (*Not a constant. Is it a fixed variable??*)
- case strip_prefix_and_unascii fixed_var_prefix x of
- SOME v => Free (v, dummyT)
- | NONE => (trace_msg (fn () => "hol_term_from_metis_FT bad const: " ^ x);
- hol_term_from_metis_PT ctxt t))
- | cvt t = (trace_msg (fn () => "hol_term_from_metis_FT bad term: " ^ Metis_Term.toString t);
- hol_term_from_metis_PT ctxt t)
- in fol_tm |> cvt end
-
-fun hol_term_from_metis FT = hol_term_from_metis_FT
- | hol_term_from_metis _ = hol_term_from_metis_PT
-
-fun hol_terms_from_fol ctxt mode old_skolems fol_tms =
- let val ts = map (hol_term_from_metis mode ctxt) fol_tms
- val _ = trace_msg (fn () => " calling type inference:")
- val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts
- val ts' = ts |> map (reveal_old_skolem_terms old_skolems)
- |> infer_types ctxt
- val _ = app (fn t => trace_msg
- (fn () => " final term: " ^ Syntax.string_of_term ctxt t ^
- " of type " ^ Syntax.string_of_typ ctxt (type_of t)))
- ts'
- in ts' end;
-
-(* ------------------------------------------------------------------------- *)
-(* FOL step Inference Rules *)
-(* ------------------------------------------------------------------------- *)
-
-(*for debugging only*)
-(*
-fun print_thpair (fth,th) =
- (trace_msg (fn () => "=============================================");
- trace_msg (fn () => "Metis: " ^ Metis_Thm.toString fth);
- trace_msg (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th));
-*)
-
-fun lookth thpairs (fth : Metis_Thm.thm) =
- the (AList.lookup (uncurry Metis_Thm.equal) thpairs fth)
- handle Option.Option =>
- raise Fail ("Failed to find Metis theorem " ^ Metis_Thm.toString fth)
-
-fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx));
-
-(* INFERENCE RULE: AXIOM *)
-
-fun axiom_inf thpairs th = Thm.incr_indexes 1 (lookth thpairs th);
- (*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*)
-
-(* INFERENCE RULE: ASSUME *)
-
-val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)}
-
-fun inst_excluded_middle thy i_atm =
- let val th = EXCLUDED_MIDDLE
- val [vx] = Term.add_vars (prop_of th) []
- val substs = [(cterm_of thy (Var vx), cterm_of thy i_atm)]
- in cterm_instantiate substs th end;
-
-fun assume_inf ctxt mode old_skolems atm =
- inst_excluded_middle
- (ProofContext.theory_of ctxt)
- (singleton (hol_terms_from_fol ctxt mode old_skolems) (Metis_Term.Fn atm))
-
-(* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying
- to reconstruct them admits new possibilities of errors, e.g. concerning
- sorts. Instead we try to arrange that new TVars are distinct and that types
- can be inferred from terms. *)
-
-fun inst_inf ctxt mode old_skolems thpairs fsubst th =
- let val thy = ProofContext.theory_of ctxt
- val i_th = lookth thpairs th
- val i_th_vars = Term.add_vars (prop_of i_th) []
- fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars)
- fun subst_translation (x,y) =
- let val v = find_var x
- (* We call "reveal_old_skolem_terms" and "infer_types" below. *)
- val t = hol_term_from_metis mode ctxt y
- in SOME (cterm_of thy (Var v), t) end
- handle Option.Option =>
- (trace_msg (fn () => "\"find_var\" failed for " ^ x ^
- " in " ^ Display.string_of_thm ctxt i_th);
- NONE)
- | TYPE _ =>
- (trace_msg (fn () => "\"hol_term_from_metis\" failed for " ^ x ^
- " in " ^ Display.string_of_thm ctxt i_th);
- NONE)
- fun remove_typeinst (a, t) =
- case strip_prefix_and_unascii schematic_var_prefix a of
- SOME b => SOME (b, t)
- | NONE => case strip_prefix_and_unascii tvar_prefix a of
- SOME _ => NONE (*type instantiations are forbidden!*)
- | NONE => SOME (a,t) (*internal Metis var?*)
- val _ = trace_msg (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th)
- val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst)
- val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs)
- val tms = rawtms |> map (reveal_old_skolem_terms old_skolems)
- |> infer_types ctxt
- val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
- val substs' = ListPair.zip (vars, map ctm_of tms)
- val _ = trace_msg (fn () =>
- cat_lines ("subst_translations:" ::
- (substs' |> map (fn (x, y) =>
- Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
- Syntax.string_of_term ctxt (term_of y)))));
- in cterm_instantiate substs' i_th end
- handle THM (msg, _, _) =>
- error ("Cannot replay Metis proof in Isabelle:\n" ^ msg)
-
-(* INFERENCE RULE: RESOLVE *)
-
-(* Like RSN, but we rename apart only the type variables. Vars here typically
- have an index of 1, and the use of RSN would increase this typically to 3.
- Instantiations of those Vars could then fail. See comment on "mk_var". *)
-fun resolve_inc_tyvars thy tha i thb =
- let
- val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
- fun aux tha thb =
- case Thm.bicompose false (false, tha, nprems_of tha) i thb
- |> Seq.list_of |> distinct Thm.eq_thm of
- [th] => th
- | _ => raise THM ("resolve_inc_tyvars: unique result expected", i,
- [tha, thb])
- in
- aux tha thb
- handle TERM z =>
- (* The unifier, which is invoked from "Thm.bicompose", will sometimes
- refuse to unify "?a::?'a" with "?a::?'b" or "?a::nat" and throw a
- "TERM" exception (with "add_ffpair" as first argument). We then
- perform unification of the types of variables by hand and try
- again. We could do this the first time around but this error
- occurs seldom and we don't want to break existing proofs in subtle
- ways or slow them down needlessly. *)
- case [] |> fold (Term.add_vars o prop_of) [tha, thb]
- |> AList.group (op =)
- |> maps (fn ((s, _), T :: Ts) =>
- map (fn T' => (Free (s, T), Free (s, T'))) Ts)
- |> rpair (Envir.empty ~1)
- |-> fold (Pattern.unify thy)
- |> Envir.type_env |> Vartab.dest
- |> map (fn (x, (S, T)) =>
- pairself (ctyp_of thy) (TVar (x, S), T)) of
- [] => raise TERM z
- | ps => aux (instantiate (ps, []) tha) (instantiate (ps, []) thb)
- end
-
-fun mk_not (Const (@{const_name Not}, _) $ b) = b
- | mk_not b = HOLogic.mk_not b
-
-(* Match untyped terms. *)
-fun untyped_aconv (Const (a, _)) (Const(b, _)) = (a = b)
- | untyped_aconv (Free (a, _)) (Free (b, _)) = (a = b)
- | untyped_aconv (Var ((a, _), _)) (Var ((b, _), _)) =
- (a = b) (* The index is ignored, for some reason. *)
- | untyped_aconv (Bound i) (Bound j) = (i = j)
- | untyped_aconv (Abs (_, _, t)) (Abs (_, _, u)) = untyped_aconv t u
- | untyped_aconv (t1 $ t2) (u1 $ u2) =
- untyped_aconv t1 u1 andalso untyped_aconv t2 u2
- | untyped_aconv _ _ = false
-
-(* Finding the relative location of an untyped term within a list of terms *)
-fun literal_index lit =
- let
- val lit = Envir.eta_contract lit
- fun get _ [] = raise Empty
- | get n (x :: xs) =
- if untyped_aconv lit (Envir.eta_contract (HOLogic.dest_Trueprop x)) then
- n
- else
- get (n+1) xs
- in get 1 end
-
-(* Permute a rule's premises to move the i-th premise to the last position. *)
-fun make_last i th =
- let val n = nprems_of th
- in if 1 <= i andalso i <= n
- then Thm.permute_prems (i-1) 1 th
- else raise THM("select_literal", i, [th])
- end;
-
-(* Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing
- double-negations. *)
-val negate_head = rewrite_rule [@{thm atomize_not}, not_not RS eq_reflection]
-
-(* Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *)
-val select_literal = negate_head oo make_last
-
-fun resolve_inf ctxt mode old_skolems thpairs atm th1 th2 =
- let
- val thy = ProofContext.theory_of ctxt
- val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
- val _ = trace_msg (fn () => " isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
- val _ = trace_msg (fn () => " isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
- in
- (* Trivial cases where one operand is type info *)
- if Thm.eq_thm (TrueI, i_th1) then
- i_th2
- else if Thm.eq_thm (TrueI, i_th2) then
- i_th1
- else
- let
- val i_atm = singleton (hol_terms_from_fol ctxt mode old_skolems)
- (Metis_Term.Fn atm)
- val _ = trace_msg (fn () => " atom: " ^ Syntax.string_of_term ctxt i_atm)
- val prems_th1 = prems_of i_th1
- val prems_th2 = prems_of i_th2
- val index_th1 = literal_index (mk_not i_atm) prems_th1
- handle Empty => raise Fail "Failed to find literal in th1"
- val _ = trace_msg (fn () => " index_th1: " ^ Int.toString index_th1)
- val index_th2 = literal_index i_atm prems_th2
- handle Empty => raise Fail "Failed to find literal in th2"
- val _ = trace_msg (fn () => " index_th2: " ^ Int.toString index_th2)
- in
- resolve_inc_tyvars thy (select_literal index_th1 i_th1) index_th2 i_th2
- end
- end;
-
-(* INFERENCE RULE: REFL *)
-
-val REFL_THM = Thm.incr_indexes 2 @{lemma "t ~= t ==> False" by simp}
-
-val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
-val refl_idx = 1 + Thm.maxidx_of REFL_THM;
-
-fun refl_inf ctxt mode old_skolems t =
- let val thy = ProofContext.theory_of ctxt
- val i_t = singleton (hol_terms_from_fol ctxt mode old_skolems) t
- val _ = trace_msg (fn () => " term: " ^ Syntax.string_of_term ctxt i_t)
- val c_t = cterm_incr_types thy refl_idx i_t
- in cterm_instantiate [(refl_x, c_t)] REFL_THM end;
-
-(* INFERENCE RULE: EQUALITY *)
-
-val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp}
-val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp}
-
-val metis_eq = Metis_Term.Fn ("=", []);
-
-fun get_ty_arg_size _ (Const (@{const_name HOL.eq}, _)) = 0 (*equality has no type arguments*)
- | get_ty_arg_size thy (Const (c, _)) = (num_type_args thy c handle TYPE _ => 0)
- | get_ty_arg_size _ _ = 0;
-
-fun equality_inf ctxt mode old_skolems (pos, atm) fp fr =
- let val thy = ProofContext.theory_of ctxt
- val m_tm = Metis_Term.Fn atm
- val [i_atm,i_tm] = hol_terms_from_fol ctxt mode old_skolems [m_tm, fr]
- val _ = trace_msg (fn () => "sign of the literal: " ^ Bool.toString pos)
- fun replace_item_list lx 0 (_::ls) = lx::ls
- | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
- fun path_finder_FO tm [] = (tm, Bound 0)
- | path_finder_FO tm (p::ps) =
- let val (tm1,args) = strip_comb tm
- val adjustment = get_ty_arg_size thy tm1
- val p' = if adjustment > p then p else p-adjustment
- val tm_p = List.nth(args,p')
- handle Subscript =>
- error ("Cannot replay Metis proof in Isabelle:\n" ^
- "equality_inf: " ^ Int.toString p ^ " adj " ^
- Int.toString adjustment ^ " term " ^
- Syntax.string_of_term ctxt tm)
- val _ = trace_msg (fn () => "path_finder: " ^ Int.toString p ^
- " " ^ Syntax.string_of_term ctxt tm_p)
- val (r,t) = path_finder_FO tm_p ps
- in
- (r, list_comb (tm1, replace_item_list t p' args))
- end
- fun path_finder_HO tm [] = (tm, Bound 0)
- | path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps)
- | path_finder_HO (t$u) (_::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps)
- | path_finder_HO tm ps =
- raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^
- "equality_inf, path_finder_HO: path = " ^
- space_implode " " (map Int.toString ps) ^
- " isa-term: " ^ Syntax.string_of_term ctxt tm)
- fun path_finder_FT tm [] _ = (tm, Bound 0)
- | path_finder_FT tm (0::ps) (Metis_Term.Fn ("ti", [t1, _])) =
- path_finder_FT tm ps t1
- | path_finder_FT (t$u) (0::ps) (Metis_Term.Fn (".", [t1, _])) =
- (fn(x,y) => (x, y$u)) (path_finder_FT t ps t1)
- | path_finder_FT (t$u) (1::ps) (Metis_Term.Fn (".", [_, t2])) =
- (fn(x,y) => (x, t$y)) (path_finder_FT u ps t2)
- | path_finder_FT tm ps t =
- raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^
- "equality_inf, path_finder_FT: path = " ^
- space_implode " " (map Int.toString ps) ^
- " isa-term: " ^ Syntax.string_of_term ctxt tm ^
- " fol-term: " ^ Metis_Term.toString t)
- fun path_finder FO tm ps _ = path_finder_FO tm ps
- | path_finder HO (tm as Const(@{const_name HOL.eq},_) $ _ $ _) (p::ps) _ =
- (*equality: not curried, as other predicates are*)
- if p=0 then path_finder_HO tm (0::1::ps) (*select first operand*)
- else path_finder_HO tm (p::ps) (*1 selects second operand*)
- | path_finder HO tm (_ :: ps) (Metis_Term.Fn ("{}", [_])) =
- path_finder_HO tm ps (*if not equality, ignore head to skip hBOOL*)
- | path_finder FT (tm as Const(@{const_name HOL.eq}, _) $ _ $ _) (p::ps)
- (Metis_Term.Fn ("=", [t1,t2])) =
- (*equality: not curried, as other predicates are*)
- if p=0 then path_finder_FT tm (0::1::ps)
- (Metis_Term.Fn (".", [Metis_Term.Fn (".", [metis_eq,t1]), t2]))
- (*select first operand*)
- else path_finder_FT tm (p::ps)
- (Metis_Term.Fn (".", [metis_eq,t2]))
- (*1 selects second operand*)
- | path_finder FT tm (_ :: ps) (Metis_Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1
- (*if not equality, ignore head to skip the hBOOL predicate*)
- | path_finder FT tm ps t = path_finder_FT tm ps t (*really an error case!*)
- fun path_finder_lit ((nt as Const (@{const_name Not}, _)) $ tm_a) idx =
- let val (tm, tm_rslt) = path_finder mode tm_a idx m_tm
- in (tm, nt $ tm_rslt) end
- | path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm
- val (tm_subst, body) = path_finder_lit i_atm fp
- val tm_abs = Abs ("x", type_of tm_subst, body)
- val _ = trace_msg (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
- val _ = trace_msg (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
- val _ = trace_msg (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
- val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst) (*ill typed but gives right max*)
- val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
- val _ = trace_msg (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
- val eq_terms = map (pairself (cterm_of thy))
- (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
- in cterm_instantiate eq_terms subst' end;
-
-val factor = Seq.hd o distinct_subgoals_tac;
-
-fun step ctxt mode old_skolems thpairs p =
- case p of
- (fol_th, Metis_Proof.Axiom _) => factor (axiom_inf thpairs fol_th)
- | (_, Metis_Proof.Assume f_atm) => assume_inf ctxt mode old_skolems f_atm
- | (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) =>
- factor (inst_inf ctxt mode old_skolems thpairs f_subst f_th1)
- | (_, Metis_Proof.Resolve(f_atm, f_th1, f_th2)) =>
- factor (resolve_inf ctxt mode old_skolems thpairs f_atm f_th1 f_th2)
- | (_, Metis_Proof.Refl f_tm) => refl_inf ctxt mode old_skolems f_tm
- | (_, Metis_Proof.Equality (f_lit, f_p, f_r)) =>
- equality_inf ctxt mode old_skolems f_lit f_p f_r
-
-fun flexflex_first_order th =
- case Thm.tpairs_of th of
- [] => th
- | pairs =>
- let val thy = theory_of_thm th
- val (_, tenv) =
- fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
- val t_pairs = map Meson.term_pair_of (Vartab.dest tenv)
- val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th
- in th' end
- handle THM _ => th;
-
-fun is_metis_literal_genuine (_, (s, _)) = not (String.isPrefix class_prefix s)
-fun is_isabelle_literal_genuine t =
- case t of _ $ (Const (@{const_name skolem}, _) $ _) => false | _ => true
-
-fun count p xs = fold (fn x => if p x then Integer.add 1 else I) xs 0
-
-fun replay_one_inference ctxt mode old_skolems (fol_th, inf) thpairs =
- let
- val _ = trace_msg (fn () => "=============================================")
- val _ = trace_msg (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)
- val _ = trace_msg (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)
- val th = step ctxt mode old_skolems thpairs (fol_th, inf)
- |> flexflex_first_order
- val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
- val _ = trace_msg (fn () => "=============================================")
- val num_metis_lits =
- fol_th |> Metis_Thm.clause |> Metis_LiteralSet.toList
- |> count is_metis_literal_genuine
- val num_isabelle_lits =
- th |> prems_of |> count is_isabelle_literal_genuine
- val _ = if num_metis_lits = num_isabelle_lits then ()
- else error "Cannot replay Metis proof in Isabelle: Out of sync."
- in (fol_th, th) :: thpairs end
-
-end;
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Oct 04 22:01:34 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,449 +0,0 @@
-(* Title: HOL/Tools/Sledgehammer/metis_tactics.ML
- Author: Kong W. Susanto, Cambridge University Computer Laboratory
- Author: Lawrence C. Paulson, Cambridge University Computer Laboratory
- Author: Jasmin Blanchette, TU Muenchen
- Copyright Cambridge University 2007
-
-HOL setup for the Metis prover.
-*)
-
-signature METIS_TACTICS =
-sig
- val trace : bool Unsynchronized.ref
- val type_lits : bool Config.T
- val new_skolemizer : bool Config.T
- val metis_tac : Proof.context -> thm list -> int -> tactic
- val metisF_tac : Proof.context -> thm list -> int -> tactic
- val metisFT_tac : Proof.context -> thm list -> int -> tactic
- val setup : theory -> theory
-end
-
-structure Metis_Tactics : METIS_TACTICS =
-struct
-
-open Metis_Translate
-open Metis_Reconstruct
-
-structure Int_Pair_Graph =
- Graph(type key = int * int val ord = prod_ord int_ord int_ord)
-
-fun trace_msg msg = if !trace then tracing (msg ()) else ()
-
-val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" (K true)
-val (new_skolemizer, new_skolemizer_setup) =
- Attrib.config_bool "metis_new_skolemizer" (K false)
-
-fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const);
-
-fun have_common_thm ths1 ths2 =
- exists (member Thm.eq_thm ths1) (map Meson.make_meta_clause ths2)
-
-(*Determining which axiom clauses are actually used*)
-fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th)
- | used_axioms _ _ = NONE;
-
-val clause_params =
- {ordering = Metis_KnuthBendixOrder.default,
- orderLiterals = Metis_Clause.UnsignedLiteralOrder,
- orderTerms = true}
-val active_params =
- {clause = clause_params,
- prefactor = #prefactor Metis_Active.default,
- postfactor = #postfactor Metis_Active.default}
-val waiting_params =
- {symbolsWeight = 1.0,
- variablesWeight = 0.0,
- literalsWeight = 0.0,
- models = []}
-val resolution_params = {active = active_params, waiting = waiting_params}
-
-fun instantiate_theorem thy inst th =
- let
- val tyenv = Vartab.empty |> fold (Type.raw_unify o pairself fastype_of) inst
- val instT =
- [] |> Vartab.fold (fn (z, (S, T)) =>
- cons (TVar (z, S), Type.devar tyenv T)) tyenv
- val inst = inst |> map (pairself (subst_atomic_types instT))
- val _ = tracing (cat_lines (map (fn (T, U) =>
- Syntax.string_of_typ @{context} T ^ " |-> " ^
- Syntax.string_of_typ @{context} U) instT))
- val _ = tracing (cat_lines (map (fn (t, u) =>
- Syntax.string_of_term @{context} t ^ " |-> " ^
- Syntax.string_of_term @{context} u) inst))
- val cinstT = instT |> map (pairself (ctyp_of thy))
- val cinst = inst |> map (pairself (cterm_of thy))
- in th |> Thm.instantiate (cinstT, cinst) end
-
-(* In principle, it should be sufficient to apply "assume_tac" to unify the
- conclusion with one of the premises. However, in practice, this is unreliable
- because of the mildly higher-order nature of the unification problems.
- Typical constraints are of the form
- "?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",
- where the nonvariables are goal parameters. *)
-fun unify_first_prem_with_concl thy i th =
- let
- val goal = Logic.get_goal (prop_of th) i |> Envir.beta_eta_contract
- val prem = goal |> Logic.strip_assums_hyp |> hd
- val concl = goal |> Logic.strip_assums_concl
- fun pair_untyped_aconv (t1, t2) (u1, u2) =
- untyped_aconv t1 u1 andalso untyped_aconv t2 u2
- fun add_terms tp inst =
- if exists (pair_untyped_aconv tp) inst then inst
- else tp :: map (apsnd (subst_atomic [tp])) inst
- fun is_flex t =
- case strip_comb t of
- (Var _, args) => forall is_Bound args
- | _ => false
- fun unify_flex flex rigid =
- case strip_comb flex of
- (Var (z as (_, T)), args) =>
- add_terms (Var z,
- fold_rev (curry absdummy) (take (length args) (binder_types T)) rigid)
- | _ => raise TERM ("unify_flex: expected flex", [flex])
- fun unify_potential_flex comb atom =
- if is_flex comb then unify_flex comb atom
- else if is_Var atom then add_terms (atom, comb)
- else raise TERM ("unify_terms", [comb, atom])
- fun unify_terms (t, u) =
- case (t, u) of
- (t1 $ t2, u1 $ u2) =>
- if is_flex t then unify_flex t u
- else if is_flex u then unify_flex u t
- else fold unify_terms [(t1, u1), (t2, u2)]
- | (_ $ _, _) => unify_potential_flex t u
- | (_, _ $ _) => unify_potential_flex u t
- | (Var _, _) => add_terms (t, u)
- | (_, Var _) => add_terms (u, t)
- | _ => if untyped_aconv t u then I else raise TERM ("unify_terms", [t, u])
- in th |> instantiate_theorem thy (unify_terms (prem, concl) []) end
-
-fun shuffle_key (((axiom_no, (_, index_no)), _), _) = (index_no, axiom_no)
-fun shuffle_ord p =
- rev_order (prod_ord int_ord int_ord (pairself shuffle_key p))
-
-val copy_prem = @{lemma "P ==> (P ==> P ==> Q) ==> Q" by fast}
-
-fun copy_prems_tac [] ns i =
- if forall (curry (op =) 1) ns then all_tac else copy_prems_tac (rev ns) [] i
- | copy_prems_tac (1 :: ms) ns i =
- rotate_tac 1 i THEN copy_prems_tac ms (1 :: ns) i
- | copy_prems_tac (m :: ms) ns i =
- etac copy_prem i THEN copy_prems_tac ms (m div 2 :: (m + 1) div 2 :: ns) i
-
-fun instantiate_forall_tac thy params t i =
- let
- fun repair (t as (Var ((s, _), _))) =
- (case find_index (fn ((s', _), _) => s' = s) params of
- ~1 => t
- | j => Bound j)
- | repair (t $ u) = repair t $ repair u
- | repair t = t
- val t' = t |> repair |> fold (curry absdummy) (map snd params)
- fun do_instantiate th =
- let val var = Term.add_vars (prop_of th) [] |> the_single in
- th |> instantiate_theorem thy [(Var var, t')]
- end
- in
- etac @{thm allE} i
- THEN rotate_tac ~1 i
- THEN PRIMITIVE do_instantiate
- end
-
-fun release_clusters_tac _ _ _ _ [] = K all_tac
- | release_clusters_tac thy ax_counts substs params
- ((ax_no, cluster_no) :: clusters) =
- let
- fun in_right_cluster s =
- (s |> Meson_Clausify.cluster_of_zapped_var_name |> fst |> snd |> fst)
- = cluster_no
- val cluster_substs =
- substs
- |> map_filter (fn (ax_no', (_, (_, tsubst))) =>
- if ax_no' = ax_no then
- tsubst |> filter (in_right_cluster
- o fst o fst o dest_Var o fst)
- |> map snd |> SOME
- else
- NONE)
- val n = length cluster_substs
- fun do_cluster_subst cluster_subst =
- map (instantiate_forall_tac thy params) cluster_subst @ [rotate_tac 1]
- val params' = params (* FIXME ### existentials! *)
- val first_prem = find_index (fn (ax_no', _) => ax_no' = ax_no) substs
- in
- rotate_tac first_prem
- THEN' (EVERY' (maps do_cluster_subst cluster_substs))
- THEN' rotate_tac (~ first_prem - length cluster_substs)
- THEN' release_clusters_tac thy ax_counts substs params' clusters
- end
-
-val cluster_ord =
- prod_ord (prod_ord int_ord (prod_ord int_ord int_ord)) bool_ord
-
-val tysubst_ord =
- list_ord (prod_ord Term_Ord.fast_indexname_ord
- (prod_ord Term_Ord.sort_ord Term_Ord.typ_ord))
-
-structure Int_Tysubst_Table =
- Table(type key = int * (indexname * (sort * typ)) list
- val ord = prod_ord int_ord tysubst_ord)
-
-(* Attempts to derive the theorem "False" from a theorem of the form
- "P1 ==> ... ==> Pn ==> False", where the "Pi"s are to be discharged using the
- specified axioms. The axioms have leading "All" and "Ex" quantifiers, which
- must be eliminated first. *)
-fun discharge_skolem_premises ctxt axioms prems_imp_false =
- if prop_of prems_imp_false aconv @{prop False} then
- prems_imp_false
- else
- let
- val thy = ProofContext.theory_of ctxt
- (* distinguish variables with same name but different types *)
- val prems_imp_false' =
- prems_imp_false |> try (forall_intr_vars #> gen_all)
- |> the_default prems_imp_false
- val prems_imp_false =
- if prop_of prems_imp_false aconv prop_of prems_imp_false' then
- prems_imp_false
- else
- prems_imp_false'
- fun match_term p =
- let
- val (tyenv, tenv) =
- Pattern.first_order_match thy p (Vartab.empty, Vartab.empty)
- val tsubst =
- tenv |> Vartab.dest
- |> sort (cluster_ord
- o pairself (Meson_Clausify.cluster_of_zapped_var_name
- o fst o fst))
- |> map (Meson.term_pair_of
- #> pairself (Envir.subst_term_types tyenv))
- val tysubst = tyenv |> Vartab.dest
- in (tysubst, tsubst) end
- fun subst_info_for_prem subgoal_no prem =
- case prem of
- _ $ (Const (@{const_name skolem}, _) $ (_ $ t $ num)) =>
- let val ax_no = HOLogic.dest_nat num in
- (ax_no, (subgoal_no,
- match_term (nth axioms ax_no |> the |> snd, t)))
- end
- | _ => raise TERM ("discharge_skolem_premises: Malformed premise",
- [prem])
- fun cluster_of_var_name skolem s =
- let
- val ((ax_no, (cluster_no, _)), skolem') =
- Meson_Clausify.cluster_of_zapped_var_name s
- in
- if skolem' = skolem andalso cluster_no > 0 then
- SOME (ax_no, cluster_no)
- else
- NONE
- end
- fun clusters_in_term skolem t =
- Term.add_var_names t [] |> map_filter (cluster_of_var_name skolem o fst)
- fun deps_for_term_subst (var, t) =
- case clusters_in_term false var of
- [] => NONE
- | [(ax_no, cluster_no)] =>
- SOME ((ax_no, cluster_no),
- clusters_in_term true t
- |> cluster_no > 1 ? cons (ax_no, cluster_no - 1))
- | _ => raise TERM ("discharge_skolem_premises: Expected Var", [var])
- val prems = Logic.strip_imp_prems (prop_of prems_imp_false)
- val substs = prems |> map2 subst_info_for_prem (1 upto length prems)
- |> sort (int_ord o pairself fst)
- val depss = maps (map_filter deps_for_term_subst o snd o snd o snd) substs
- val clusters = maps (op ::) depss
- val ordered_clusters =
- Int_Pair_Graph.empty
- |> fold Int_Pair_Graph.default_node (map (rpair ()) clusters)
- |> fold Int_Pair_Graph.add_deps_acyclic depss
- |> Int_Pair_Graph.topological_order
- handle Int_Pair_Graph.CYCLES _ =>
- error "Cannot replay Metis proof in Isabelle without axiom of \
- \choice."
- val params0 =
- [] |> fold (Term.add_vars o snd) (map_filter I axioms)
- |> map (`(Meson_Clausify.cluster_of_zapped_var_name o fst o fst))
- |> filter (fn (((_, (cluster_no, _)), skolem), _) =>
- cluster_no = 0 andalso skolem)
- |> sort shuffle_ord |> map snd
- val ax_counts =
- Int_Tysubst_Table.empty
- |> fold (fn (ax_no, (_, (tysubst, _))) =>
- Int_Tysubst_Table.map_default ((ax_no, tysubst), 0)
- (Integer.add 1)) substs
- |> Int_Tysubst_Table.dest
-(* for debugging:
- fun string_for_subst_info (ax_no, (subgoal_no, (tysubst, tsubst))) =
- "ax: " ^ string_of_int ax_no ^ "; asm: " ^ string_of_int subgoal_no ^
- "; tysubst: " ^ PolyML.makestring tysubst ^ "; tsubst: {" ^
- commas (map ((fn (s, t) => s ^ " |-> " ^ t)
- o pairself (Syntax.string_of_term ctxt)) tsubst) ^ "}"
- val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^
- cat_lines (map string_for_subst_info substs))
- val _ = tracing ("OUTERMOST SKOLEMS: " ^ PolyML.makestring params0)
- val _ = tracing ("ORDERED CLUSTERS: " ^ PolyML.makestring ordered_clusters)
- val _ = tracing ("AXIOM COUNTS: " ^ PolyML.makestring ax_counts)
-*)
- fun rotation_for_subgoal i =
- find_index (fn (_, (subgoal_no, _)) => subgoal_no = i) substs
- in
- Goal.prove ctxt [] [] @{prop False}
- (K (cut_rules_tac
- (map (fst o the o nth axioms o fst o fst) ax_counts) 1
- THEN print_tac "cut:"
- THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1)
- THEN copy_prems_tac (map snd ax_counts) [] 1
- THEN print_tac "eliminated exist and copied prems:"
- THEN release_clusters_tac thy ax_counts substs params0
- ordered_clusters 1
- THEN print_tac "released clusters:"
- THEN match_tac [prems_imp_false] 1
- THEN print_tac "applied rule:"
- THEN ALLGOALS (fn i =>
- rtac @{thm skolem_COMBK_I} i
- THEN rotate_tac (rotation_for_subgoal i) i
- THEN PRIMITIVE (unify_first_prem_with_concl thy i)
- THEN assume_tac i)))
- end
-
-(* Main function to start Metis proof and reconstruction *)
-fun FOL_SOLVE mode ctxt cls ths0 =
- let val thy = ProofContext.theory_of ctxt
- val type_lits = Config.get ctxt type_lits
- val new_skolemizer =
- Config.get ctxt new_skolemizer orelse null (Meson_Choices.get ctxt)
- val th_cls_pairs =
- map2 (fn j => fn th =>
- (Thm.get_name_hint th,
- Meson_Clausify.cnf_axiom ctxt new_skolemizer j th))
- (0 upto length ths0 - 1) ths0
- val thss = map (snd o snd) th_cls_pairs
- val dischargers = map (fst o snd) th_cls_pairs
- val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
- val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
- val _ = trace_msg (fn () => "THEOREM CLAUSES")
- val _ = app (app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th))) thss
- val (mode, {axioms, tfrees, old_skolems}) =
- build_logic_map mode ctxt type_lits cls thss
- val _ = if null tfrees then ()
- else (trace_msg (fn () => "TFREE CLAUSES");
- app (fn TyLitFree ((s, _), (s', _)) =>
- trace_msg (fn () => s ^ "(" ^ s' ^ ")")) tfrees)
- val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS")
- val thms = map #1 axioms
- val _ = app (fn th => trace_msg (fn () => Metis_Thm.toString th)) thms
- val _ = trace_msg (fn () => "mode = " ^ string_of_mode mode)
- val _ = trace_msg (fn () => "START METIS PROVE PROCESS")
- in
- case filter (is_false o prop_of) cls of
- false_th::_ => [false_th RS @{thm FalseE}]
- | [] =>
- case Metis_Resolution.new resolution_params {axioms = thms, conjecture = []}
- |> Metis_Resolution.loop of
- Metis_Resolution.Contradiction mth =>
- let val _ = trace_msg (fn () => "METIS RECONSTRUCTION START: " ^
- Metis_Thm.toString mth)
- val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
- (*add constraints arising from converting goal to clause form*)
- val proof = Metis_Proof.proof mth
- val result =
- fold (replay_one_inference ctxt' mode old_skolems) proof axioms
- and used = map_filter (used_axioms axioms) proof
- val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:")
- val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used
- val unused = th_cls_pairs |> map_filter (fn (name, (_, cls)) =>
- if have_common_thm used cls then NONE else SOME name)
- in
- if not (null cls) andalso not (have_common_thm used cls) then
- warning "Metis: The assumptions are inconsistent."
- else
- ();
- if not (null unused) then
- warning ("Metis: Unused theorems: " ^ commas_quote unused
- ^ ".")
- else
- ();
- case result of
- (_,ith)::_ =>
- (trace_msg (fn () => "Success: " ^ Display.string_of_thm ctxt ith);
- [discharge_skolem_premises ctxt dischargers ith])
- | _ => (trace_msg (fn () => "Metis: No result"); [])
- end
- | Metis_Resolution.Satisfiable _ =>
- (trace_msg (fn () => "Metis: No first-order proof with the lemmas supplied");
- [])
- end;
-
-(* Extensionalize "th", because that makes sense and that's what Sledgehammer
- does, but also keep an unextensionalized version of "th" for backward
- compatibility. *)
-fun also_extensionalize_theorem th =
- let val th' = Meson_Clausify.extensionalize_theorem th in
- if Thm.eq_thm (th, th') then [th]
- else th :: Meson.make_clauses_unsorted [th']
- end
-
-val neg_clausify =
- single
- #> Meson.make_clauses_unsorted
- #> maps also_extensionalize_theorem
- #> map Meson_Clausify.introduce_combinators_in_theorem
- #> Meson.finish_cnf
-
-fun preskolem_tac ctxt st0 =
- (if exists (Meson.has_too_many_clauses ctxt)
- (Logic.prems_of_goal (prop_of st0) 1) then
- cnf.cnfx_rewrite_tac ctxt 1
- else
- all_tac) st0
-
-val type_has_top_sort =
- exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
-
-fun generic_metis_tac mode ctxt ths i st0 =
- let
- val _ = trace_msg (fn () =>
- "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
- in
- if exists_type type_has_top_sort (prop_of st0) then
- (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty)
- else
- Meson.MESON (preskolem_tac ctxt) (maps neg_clausify)
- (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
- ctxt i st0
- end
-
-val metis_tac = generic_metis_tac HO
-val metisF_tac = generic_metis_tac FO
-val metisFT_tac = generic_metis_tac FT
-
-(* Whenever "X" has schematic type variables, we treat "using X by metis" as
- "by (metis X)", to prevent "Subgoal.FOCUS" from freezing the type variables.
- We don't do it for nonschematic facts "X" because this breaks a few proofs
- (in the rare and subtle case where a proof relied on extensionality not being
- applied) and brings few benefits. *)
-val has_tvar =
- exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of
-fun method name mode =
- Method.setup name (Attrib.thms >> (fn ths => fn ctxt =>
- METHOD (fn facts =>
- let
- val (schem_facts, nonschem_facts) =
- List.partition has_tvar facts
- in
- HEADGOAL (Method.insert_tac nonschem_facts THEN'
- CHANGED_PROP
- o generic_metis_tac mode ctxt (schem_facts @ ths))
- end)))
-
-val setup =
- type_lits_setup
- #> new_skolemizer_setup
- #> method @{binding metis} HO "Metis for FOL/HOL problems"
- #> method @{binding metisF} FO "Metis for FOL problems"
- #> method @{binding metisFT} FT
- "Metis for FOL/HOL problems with fully-typed translation"
-
-end;
--- a/src/HOL/Tools/Sledgehammer/metis_translate.ML Mon Oct 04 22:01:34 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,771 +0,0 @@
-(* Title: HOL/Tools/Sledgehammer/metis_translate.ML
- Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
- Author: Kong W. Susanto, Cambridge University Computer Laboratory
- Author: Lawrence C. Paulson, Cambridge University Computer Laboratory
- Author: Jasmin Blanchette, TU Muenchen
-
-Translation of HOL to FOL for Metis.
-*)
-
-signature METIS_TRANSLATE =
-sig
- type name = string * string
- datatype type_literal =
- TyLitVar of name * name |
- TyLitFree of name * name
- datatype arLit =
- TConsLit of name * name * name list |
- TVarLit of name * name
- datatype arity_clause =
- ArityClause of {name: string, conclLit: arLit, premLits: arLit list}
- datatype class_rel_clause =
- ClassRelClause of {name: string, subclass: name, superclass: name}
- datatype combtyp =
- CombTVar of name |
- CombTFree of name |
- CombType of name * combtyp list
- datatype combterm =
- CombConst of name * combtyp * combtyp list (* Const and Free *) |
- CombVar of name * combtyp |
- CombApp of combterm * combterm
- datatype fol_literal = FOLLiteral of bool * combterm
-
- datatype mode = FO | HO | FT
- type logic_map =
- {axioms: (Metis_Thm.thm * thm) list,
- tfrees: type_literal list,
- old_skolems: (string * term) list}
-
- val type_wrapper_name : string
- val bound_var_prefix : string
- val schematic_var_prefix: string
- val fixed_var_prefix: string
- val tvar_prefix: string
- val tfree_prefix: string
- val const_prefix: string
- val type_const_prefix: string
- val class_prefix: string
- val new_skolem_const_prefix : string
- val invert_const: string -> string
- val ascii_of: string -> string
- val unascii_of: string -> string
- val strip_prefix_and_unascii: string -> string -> string option
- val make_bound_var : string -> string
- val make_schematic_var : string * int -> string
- val make_fixed_var : string -> string
- val make_schematic_type_var : string * int -> string
- val make_fixed_type_var : string -> string
- val make_fixed_const : string -> string
- val make_fixed_type_const : string -> string
- val make_type_class : string -> string
- val num_type_args: theory -> string -> int
- val new_skolem_var_from_const: string -> indexname
- val type_literals_for_types : typ list -> type_literal list
- val make_class_rel_clauses :
- theory -> class list -> class list -> class_rel_clause list
- val make_arity_clauses :
- theory -> string list -> class list -> class list * arity_clause list
- val combtyp_of : combterm -> combtyp
- val strip_combterm_comb : combterm -> combterm * combterm list
- val combterm_from_term :
- theory -> int -> (string * typ) list -> term -> combterm * typ list
- val reveal_old_skolem_terms : (string * term) list -> term -> term
- val tfree_classes_of_terms : term list -> string list
- val tvar_classes_of_terms : term list -> string list
- val type_consts_of_terms : theory -> term list -> string list
- val string_of_mode : mode -> string
- val build_logic_map :
- mode -> Proof.context -> bool -> thm list -> thm list list
- -> mode * logic_map
-end
-
-structure Metis_Translate : METIS_TRANSLATE =
-struct
-
-val type_wrapper_name = "ti"
-
-val bound_var_prefix = "B_"
-val schematic_var_prefix = "V_"
-val fixed_var_prefix = "v_"
-
-val tvar_prefix = "T_";
-val tfree_prefix = "t_";
-
-val const_prefix = "c_";
-val type_const_prefix = "tc_";
-val class_prefix = "class_";
-
-val skolem_const_prefix = "Sledgehammer" ^ Long_Name.separator ^ "Sko"
-val old_skolem_const_prefix = skolem_const_prefix ^ "o"
-val new_skolem_const_prefix = skolem_const_prefix ^ "n"
-
-fun union_all xss = fold (union (op =)) xss []
-
-(* Readable names for the more common symbolic functions. Do not mess with the
- last nine entries of the table unless you know what you are doing. *)
-val const_trans_table =
- Symtab.make [(@{type_name Product_Type.prod}, "prod"),
- (@{type_name Sum_Type.sum}, "sum"),
- (@{const_name HOL.eq}, "equal"),
- (@{const_name HOL.conj}, "and"),
- (@{const_name HOL.disj}, "or"),
- (@{const_name HOL.implies}, "implies"),
- (@{const_name Set.member}, "member"),
- (@{const_name fequal}, "fequal"),
- (@{const_name COMBI}, "COMBI"),
- (@{const_name COMBK}, "COMBK"),
- (@{const_name COMBB}, "COMBB"),
- (@{const_name COMBC}, "COMBC"),
- (@{const_name COMBS}, "COMBS"),
- (@{const_name True}, "True"),
- (@{const_name False}, "False"),
- (@{const_name If}, "If")]
-
-(* Invert the table of translations between Isabelle and ATPs. *)
-val const_trans_table_inv =
- Symtab.update ("fequal", @{const_name HOL.eq})
- (Symtab.make (map swap (Symtab.dest const_trans_table)))
-
-val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
-
-(*Escaping of special characters.
- Alphanumeric characters are left unchanged.
- The character _ goes to __
- Characters in the range ASCII space to / go to _A to _P, respectively.
- Other characters go to _nnn where nnn is the decimal ASCII code.*)
-val A_minus_space = Char.ord #"A" - Char.ord #" ";
-
-fun stringN_of_int 0 _ = ""
- | stringN_of_int k n = stringN_of_int (k-1) (n div 10) ^ Int.toString (n mod 10);
-
-fun ascii_of_c c =
- if Char.isAlphaNum c then String.str c
- else if c = #"_" then "__"
- else if #" " <= c andalso c <= #"/"
- then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space))
- else ("_" ^ stringN_of_int 3 (Char.ord c)) (*fixed width, in case more digits follow*)
-
-val ascii_of = String.translate ascii_of_c;
-
-(** Remove ASCII armouring from names in proof files **)
-
-(*We don't raise error exceptions because this code can run inside the watcher.
- Also, the errors are "impossible" (hah!)*)
-fun unascii_aux rcs [] = String.implode(rev rcs)
- | unascii_aux rcs [#"_"] = unascii_aux (#"_"::rcs) [] (*ERROR*)
- (*Three types of _ escapes: __, _A to _P, _nnn*)
- | unascii_aux rcs (#"_" :: #"_" :: cs) = unascii_aux (#"_"::rcs) cs
- | unascii_aux rcs (#"_" :: c :: cs) =
- if #"A" <= c andalso c<= #"P" (*translation of #" " to #"/"*)
- then unascii_aux (Char.chr(Char.ord c - A_minus_space) :: rcs) cs
- else
- let val digits = List.take (c::cs, 3) handle Subscript => []
- in
- case Int.fromString (String.implode digits) of
- NONE => unascii_aux (c:: #"_"::rcs) cs (*ERROR*)
- | SOME n => unascii_aux (Char.chr n :: rcs) (List.drop (cs, 2))
- end
- | unascii_aux rcs (c::cs) = unascii_aux (c::rcs) cs
-val unascii_of = unascii_aux [] o String.explode
-
-(* If string s has the prefix s1, return the result of deleting it,
- un-ASCII'd. *)
-fun strip_prefix_and_unascii s1 s =
- if String.isPrefix s1 s then
- SOME (unascii_of (String.extract (s, size s1, NONE)))
- else
- NONE
-
-(*Remove the initial ' character from a type variable, if it is present*)
-fun trim_type_var s =
- if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE)
- else error ("trim_type: Malformed type variable encountered: " ^ s);
-
-fun ascii_of_indexname (v,0) = ascii_of v
- | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ Int.toString i;
-
-fun make_bound_var x = bound_var_prefix ^ ascii_of x
-fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v
-fun make_fixed_var x = fixed_var_prefix ^ ascii_of x
-
-fun make_schematic_type_var (x,i) =
- tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i));
-fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x));
-
-fun lookup_const c =
- case Symtab.lookup const_trans_table c of
- SOME c' => c'
- | NONE => ascii_of c
-
-(* HOL.eq MUST BE "equal" because it's built into ATPs. *)
-fun make_fixed_const @{const_name HOL.eq} = "equal"
- | make_fixed_const c = const_prefix ^ lookup_const c
-
-fun make_fixed_type_const c = type_const_prefix ^ lookup_const c
-
-fun make_type_class clas = class_prefix ^ ascii_of clas;
-
-(* The number of type arguments of a constant, zero if it's monomorphic. For
- (instances of) Skolem pseudoconstants, this information is encoded in the
- constant name. *)
-fun num_type_args thy s =
- if String.isPrefix skolem_const_prefix s then
- s |> space_explode Long_Name.separator |> List.last |> Int.fromString |> the
- else
- (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
-
-fun new_skolem_var_from_const s =
- let
- val ss = s |> space_explode Long_Name.separator
- val n = length ss
- in (nth ss (n - 2), nth ss (n - 3) |> Int.fromString |> the) end
-
-
-(**** Definitions and functions for FOL clauses for TPTP format output ****)
-
-type name = string * string
-
-(**** Isabelle FOL clauses ****)
-
-(* The first component is the type class; the second is a TVar or TFree. *)
-datatype type_literal =
- TyLitVar of name * name |
- TyLitFree of name * name
-
-(*Make literals for sorted type variables*)
-fun sorts_on_typs_aux (_, []) = []
- | sorts_on_typs_aux ((x,i), s::ss) =
- let val sorts = sorts_on_typs_aux ((x,i), ss)
- in
- if s = "HOL.type" then sorts
- else if i = ~1 then TyLitFree (`make_type_class s, `make_fixed_type_var x) :: sorts
- else TyLitVar (`make_type_class s, (make_schematic_type_var (x,i), x)) :: sorts
- end;
-
-fun sorts_on_typs (TFree (a,s)) = sorts_on_typs_aux ((a,~1),s)
- | sorts_on_typs (TVar (v,s)) = sorts_on_typs_aux (v,s);
-
-(*Given a list of sorted type variables, return a list of type literals.*)
-fun type_literals_for_types Ts =
- fold (union (op =)) (map sorts_on_typs Ts) []
-
-(** make axiom and conjecture clauses. **)
-
-(**** Isabelle arities ****)
-
-datatype arLit =
- TConsLit of name * name * name list |
- TVarLit of name * name
-
-datatype arity_clause =
- ArityClause of {name: string, conclLit: arLit, premLits: arLit list}
-
-
-fun gen_TVars 0 = []
- | gen_TVars n = ("T_" ^ Int.toString n) :: gen_TVars (n-1);
-
-fun pack_sort(_,[]) = []
- | pack_sort(tvar, "HOL.type"::srt) = pack_sort (tvar, srt) (*IGNORE sort "type"*)
- | pack_sort(tvar, cls::srt) =
- (`make_type_class cls, (tvar, tvar)) :: pack_sort (tvar, srt)
-
-(*Arity of type constructor tcon :: (arg1,...,argN)res*)
-fun make_axiom_arity_clause (tcons, name, (cls,args)) =
- let
- val tvars = gen_TVars (length args)
- val tvars_srts = ListPair.zip (tvars, args)
- in
- ArityClause {name = name,
- conclLit = TConsLit (`make_type_class cls,
- `make_fixed_type_const tcons,
- tvars ~~ tvars),
- premLits = map TVarLit (union_all (map pack_sort tvars_srts))}
- end
-
-
-(**** Isabelle class relations ****)
-
-datatype class_rel_clause =
- ClassRelClause of {name: string, subclass: name, superclass: name}
-
-(*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)
-fun class_pairs _ [] _ = []
- | class_pairs thy subs supers =
- let
- val class_less = Sorts.class_less (Sign.classes_of thy)
- fun add_super sub super = class_less (sub, super) ? cons (sub, super)
- fun add_supers sub = fold (add_super sub) supers
- in fold add_supers subs [] end
-
-fun make_class_rel_clause (sub,super) =
- ClassRelClause {name = sub ^ "_" ^ super,
- subclass = `make_type_class sub,
- superclass = `make_type_class super}
-
-fun make_class_rel_clauses thy subs supers =
- map make_class_rel_clause (class_pairs thy subs supers);
-
-
-(** Isabelle arities **)
-
-fun arity_clause _ _ (_, []) = []
- | arity_clause seen n (tcons, ("HOL.type",_)::ars) = (*ignore*)
- arity_clause seen n (tcons,ars)
- | arity_clause seen n (tcons, (ar as (class,_)) :: ars) =
- if member (op =) seen class then (*multiple arities for the same tycon, class pair*)
- make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) ::
- arity_clause seen (n+1) (tcons,ars)
- else
- make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class, ar) ::
- arity_clause (class::seen) n (tcons,ars)
-
-fun multi_arity_clause [] = []
- | multi_arity_clause ((tcons, ars) :: tc_arlists) =
- arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists
-
-(*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy
- provided its arguments have the corresponding sorts.*)
-fun type_class_pairs thy tycons classes =
- let val alg = Sign.classes_of thy
- fun domain_sorts tycon = Sorts.mg_domain alg tycon o single
- fun add_class tycon class =
- cons (class, domain_sorts tycon class)
- handle Sorts.CLASS_ERROR _ => I
- fun try_classes tycon = (tycon, fold (add_class tycon) classes [])
- in map try_classes tycons end;
-
-(*Proving one (tycon, class) membership may require proving others, so iterate.*)
-fun iter_type_class_pairs _ _ [] = ([], [])
- | iter_type_class_pairs thy tycons classes =
- let val cpairs = type_class_pairs thy tycons classes
- val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs)))
- |> subtract (op =) classes |> subtract (op =) HOLogic.typeS
- val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
- in (union (op =) classes' classes, union (op =) cpairs' cpairs) end;
-
-fun make_arity_clauses thy tycons classes =
- let val (classes', cpairs) = iter_type_class_pairs thy tycons classes
- in (classes', multi_arity_clause cpairs) end;
-
-datatype combtyp =
- CombTVar of name |
- CombTFree of name |
- CombType of name * combtyp list
-
-datatype combterm =
- CombConst of name * combtyp * combtyp list (* Const and Free *) |
- CombVar of name * combtyp |
- CombApp of combterm * combterm
-
-datatype fol_literal = FOLLiteral of bool * combterm
-
-(*********************************************************************)
-(* convert a clause with type Term.term to a clause with type clause *)
-(*********************************************************************)
-
-(*Result of a function type; no need to check that the argument type matches.*)
-fun result_type (CombType (_, [_, tp2])) = tp2
- | result_type _ = raise Fail "non-function type"
-
-fun combtyp_of (CombConst (_, tp, _)) = tp
- | combtyp_of (CombVar (_, tp)) = tp
- | combtyp_of (CombApp (t1, _)) = result_type (combtyp_of t1)
-
-(*gets the head of a combinator application, along with the list of arguments*)
-fun strip_combterm_comb u =
- let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
- | stripc x = x
- in stripc(u,[]) end
-
-fun combtype_of (Type (a, Ts)) =
- let val (folTypes, ts) = combtypes_of Ts in
- (CombType (`make_fixed_type_const a, folTypes), ts)
- end
- | combtype_of (tp as TFree (a, _)) = (CombTFree (`make_fixed_type_var a), [tp])
- | combtype_of (tp as TVar (x, _)) =
- (CombTVar (make_schematic_type_var x, string_of_indexname x), [tp])
-and combtypes_of Ts =
- let val (folTyps, ts) = ListPair.unzip (map combtype_of Ts) in
- (folTyps, union_all ts)
- end
-
-(* same as above, but no gathering of sort information *)
-fun simple_combtype_of (Type (a, Ts)) =
- CombType (`make_fixed_type_const a, map simple_combtype_of Ts)
- | simple_combtype_of (TFree (a, _)) = CombTFree (`make_fixed_type_var a)
- | simple_combtype_of (TVar (x, _)) =
- CombTVar (make_schematic_type_var x, string_of_indexname x)
-
-fun new_skolem_const_name th_no s num_T_args =
- [new_skolem_const_prefix, string_of_int th_no, s, string_of_int num_T_args]
- |> space_implode Long_Name.separator
-
-(* Converts a term (with combinators) into a combterm. Also accummulates sort
- infomation. *)
-fun combterm_from_term thy th_no bs (P $ Q) =
- let val (P', tsP) = combterm_from_term thy th_no bs P
- val (Q', tsQ) = combterm_from_term thy th_no bs Q
- in (CombApp (P', Q'), union (op =) tsP tsQ) end
- | combterm_from_term thy _ _ (Const (c, T)) =
- let
- val (tp, ts) = combtype_of T
- val tvar_list =
- (if String.isPrefix old_skolem_const_prefix c then
- [] |> Term.add_tvarsT T |> map TVar
- else
- (c, T) |> Sign.const_typargs thy)
- |> map simple_combtype_of
- val c' = CombConst (`make_fixed_const c, tp, tvar_list)
- in (c',ts) end
- | combterm_from_term _ _ _ (Free (v, T)) =
- let val (tp, ts) = combtype_of T
- val v' = CombConst (`make_fixed_var v, tp, [])
- in (v',ts) end
- | combterm_from_term _ th_no _ (Var (v as (s, _), T)) =
- let
- val (tp, ts) = combtype_of T
- val v' =
- if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
- let
- val tys = T |> strip_type |> swap |> op ::
- val s' = new_skolem_const_name th_no s (length tys)
- in
- CombConst (`make_fixed_const s', tp, map simple_combtype_of tys)
- end
- else
- CombVar ((make_schematic_var v, string_of_indexname v), tp)
- in (v', ts) end
- | combterm_from_term _ _ bs (Bound j) =
- let
- val (s, T) = nth bs j
- val (tp, ts) = combtype_of T
- val v' = CombConst (`make_bound_var s, tp, [])
- in (v', ts) end
- | combterm_from_term _ _ _ (Abs _) = raise Fail "HOL clause: Abs"
-
-fun predicate_of thy th_no ((@{const Not} $ P), pos) =
- predicate_of thy th_no (P, not pos)
- | predicate_of thy th_no (t, pos) =
- (combterm_from_term thy th_no [] (Envir.eta_contract t), pos)
-
-fun literals_of_term1 args thy th_no (@{const Trueprop} $ P) =
- literals_of_term1 args thy th_no P
- | literals_of_term1 args thy th_no (@{const HOL.disj} $ P $ Q) =
- literals_of_term1 (literals_of_term1 args thy th_no P) thy th_no Q
- | literals_of_term1 (lits, ts) thy th_no P =
- let val ((pred, ts'), pol) = predicate_of thy th_no (P, true) in
- (FOLLiteral (pol, pred) :: lits, union (op =) ts ts')
- end
-val literals_of_term = literals_of_term1 ([], [])
-
-fun old_skolem_const_name i j num_T_args =
- old_skolem_const_prefix ^ Long_Name.separator ^
- (space_implode Long_Name.separator (map Int.toString [i, j, num_T_args]))
-
-fun conceal_old_skolem_terms i old_skolems t =
- if exists_Const (curry (op =) @{const_name skolem} o fst) t then
- let
- fun aux old_skolems
- (t as (Const (@{const_name skolem}, Type (_, [_, T])) $ _)) =
- let
- val (old_skolems, s) =
- if i = ~1 then
- (old_skolems, @{const_name undefined})
- else case AList.find (op aconv) old_skolems t of
- s :: _ => (old_skolems, s)
- | [] =>
- let
- val s = old_skolem_const_name i (length old_skolems)
- (length (Term.add_tvarsT T []))
- in ((s, t) :: old_skolems, s) end
- in (old_skolems, Const (s, T)) end
- | aux old_skolems (t1 $ t2) =
- let
- val (old_skolems, t1) = aux old_skolems t1
- val (old_skolems, t2) = aux old_skolems t2
- in (old_skolems, t1 $ t2) end
- | aux old_skolems (Abs (s, T, t')) =
- let val (old_skolems, t') = aux old_skolems t' in
- (old_skolems, Abs (s, T, t'))
- end
- | aux old_skolems t = (old_skolems, t)
- in aux old_skolems t end
- else
- (old_skolems, t)
-
-fun reveal_old_skolem_terms old_skolems =
- map_aterms (fn t as Const (s, _) =>
- if String.isPrefix old_skolem_const_prefix s then
- AList.lookup (op =) old_skolems s |> the
- |> map_types Type_Infer.paramify_vars
- else
- t
- | t => t)
-
-
-(***************************************************************)
-(* Type Classes Present in the Axiom or Conjecture Clauses *)
-(***************************************************************)
-
-fun set_insert (x, s) = Symtab.update (x, ()) s
-
-fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts)
-
-(*Remove this trivial type class*)
-fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset;
-
-fun tfree_classes_of_terms ts =
- let val sorts_list = map (map #2 o OldTerm.term_tfrees) ts
- in Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list)) end;
-
-fun tvar_classes_of_terms ts =
- let val sorts_list = map (map #2 o OldTerm.term_tvars) ts
- in Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list)) end;
-
-(*fold type constructors*)
-fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x))
- | fold_type_consts _ _ x = x;
-
-(*Type constructors used to instantiate overloaded constants are the only ones needed.*)
-fun add_type_consts_in_term thy =
- let
- fun aux (Const x) =
- fold (fold_type_consts set_insert) (Sign.const_typargs thy x)
- | aux (Abs (_, _, u)) = aux u
- | aux (Const (@{const_name skolem}, _) $ _) = I
- | aux (t $ u) = aux t #> aux u
- | aux _ = I
- in aux end
-
-fun type_consts_of_terms thy ts =
- Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty);
-
-(* ------------------------------------------------------------------------- *)
-(* HOL to FOL (Isabelle to Metis) *)
-(* ------------------------------------------------------------------------- *)
-
-datatype mode = FO | HO | FT (* first-order, higher-order, fully-typed *)
-
-fun string_of_mode FO = "FO"
- | string_of_mode HO = "HO"
- | string_of_mode FT = "FT"
-
-fun fn_isa_to_met_sublevel "equal" = "=" (* FIXME: "c_fequal" *)
- | fn_isa_to_met_sublevel x = x
-fun fn_isa_to_met_toplevel "equal" = "="
- | fn_isa_to_met_toplevel x = x
-
-fun metis_lit b c args = (b, (c, args));
-
-fun metis_term_from_combtyp (CombTVar (s, _)) = Metis_Term.Var s
- | metis_term_from_combtyp (CombTFree (s, _)) = Metis_Term.Fn (s, [])
- | metis_term_from_combtyp (CombType ((s, _), tps)) =
- Metis_Term.Fn (s, map metis_term_from_combtyp tps);
-
-(*These two functions insert type literals before the real literals. That is the
- opposite order from TPTP linkup, but maybe OK.*)
-
-fun hol_term_to_fol_FO tm =
- case strip_combterm_comb tm of
- (CombConst ((c, _), _, tys), tms) =>
- let val tyargs = map metis_term_from_combtyp tys
- val args = map hol_term_to_fol_FO tms
- in Metis_Term.Fn (c, tyargs @ args) end
- | (CombVar ((v, _), _), []) => Metis_Term.Var v
- | _ => raise Fail "non-first-order combterm"
-
-fun hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) =
- Metis_Term.Fn (fn_isa_to_met_sublevel a, map metis_term_from_combtyp tylist)
- | hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis_Term.Var s
- | hol_term_to_fol_HO (CombApp (tm1, tm2)) =
- Metis_Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]);
-
-(*The fully-typed translation, to avoid type errors*)
-fun wrap_type (tm, ty) =
- Metis_Term.Fn (type_wrapper_name, [tm, metis_term_from_combtyp ty])
-
-fun hol_term_to_fol_FT (CombVar ((s, _), ty)) = wrap_type (Metis_Term.Var s, ty)
- | hol_term_to_fol_FT (CombConst((a, _), ty, _)) =
- wrap_type (Metis_Term.Fn(fn_isa_to_met_sublevel a, []), ty)
- | hol_term_to_fol_FT (tm as CombApp(tm1,tm2)) =
- wrap_type (Metis_Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]),
- combtyp_of tm)
-
-fun hol_literal_to_fol FO (FOLLiteral (pos, tm)) =
- let val (CombConst((p, _), _, tys), tms) = strip_combterm_comb tm
- val tylits = if p = "equal" then [] else map metis_term_from_combtyp tys
- val lits = map hol_term_to_fol_FO tms
- in metis_lit pos (fn_isa_to_met_toplevel p) (tylits @ lits) end
- | hol_literal_to_fol HO (FOLLiteral (pos, tm)) =
- (case strip_combterm_comb tm of
- (CombConst(("equal", _), _, _), tms) =>
- metis_lit pos "=" (map hol_term_to_fol_HO tms)
- | _ => metis_lit pos "{}" [hol_term_to_fol_HO tm]) (*hBOOL*)
- | hol_literal_to_fol FT (FOLLiteral (pos, tm)) =
- (case strip_combterm_comb tm of
- (CombConst(("equal", _), _, _), tms) =>
- metis_lit pos "=" (map hol_term_to_fol_FT tms)
- | _ => metis_lit pos "{}" [hol_term_to_fol_FT tm]) (*hBOOL*);
-
-fun literals_of_hol_term thy th_no mode t =
- let val (lits, types_sorts) = literals_of_term thy th_no t
- in (map (hol_literal_to_fol mode) lits, types_sorts) end;
-
-(*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*)
-fun metis_of_type_literals pos (TyLitVar ((s, _), (s', _))) =
- metis_lit pos s [Metis_Term.Var s']
- | metis_of_type_literals pos (TyLitFree ((s, _), (s', _))) =
- metis_lit pos s [Metis_Term.Fn (s',[])]
-
-fun default_sort _ (TVar _) = false
- | default_sort ctxt (TFree (x, s)) = (s = the_default [] (Variable.def_sort ctxt (x, ~1)));
-
-fun metis_of_tfree tf =
- Metis_Thm.axiom (Metis_LiteralSet.singleton (metis_of_type_literals true tf));
-
-fun hol_thm_to_fol is_conjecture th_no ctxt type_lits mode j old_skolems th =
- let
- val thy = ProofContext.theory_of ctxt
- val (old_skolems, (mlits, types_sorts)) =
- th |> prop_of |> Logic.strip_imp_concl
- |> conceal_old_skolem_terms j old_skolems
- ||> (HOLogic.dest_Trueprop #> literals_of_hol_term thy th_no mode)
- in
- if is_conjecture then
- (Metis_Thm.axiom (Metis_LiteralSet.fromList mlits),
- type_literals_for_types types_sorts, old_skolems)
- else
- let
- val tylits = filter_out (default_sort ctxt) types_sorts
- |> type_literals_for_types
- val mtylits =
- if type_lits then map (metis_of_type_literals false) tylits else []
- in
- (Metis_Thm.axiom (Metis_LiteralSet.fromList(mtylits @ mlits)), [],
- old_skolems)
- end
- end;
-
-val helpers =
- [("c_COMBI", (false, map (`I) @{thms COMBI_def})),
- ("c_COMBK", (false, map (`I) @{thms COMBK_def})),
- ("c_COMBB", (false, map (`I) @{thms COMBB_def})),
- ("c_COMBC", (false, map (`I) @{thms COMBC_def})),
- ("c_COMBS", (false, map (`I) @{thms COMBS_def})),
- ("c_fequal", (false, map (rpair @{thm equal_imp_equal})
- @{thms fequal_imp_equal equal_imp_fequal})),
- ("c_True", (true, map (`I) @{thms True_or_False})),
- ("c_False", (true, map (`I) @{thms True_or_False})),
- ("c_If", (true, map (`I) @{thms if_True if_False True_or_False}))]
-
-(* ------------------------------------------------------------------------- *)
-(* Logic maps manage the interface between HOL and first-order logic. *)
-(* ------------------------------------------------------------------------- *)
-
-type logic_map =
- {axioms: (Metis_Thm.thm * thm) list,
- tfrees: type_literal list,
- old_skolems: (string * term) list}
-
-fun is_quasi_fol_clause thy =
- Meson.is_fol_term thy o snd o conceal_old_skolem_terms ~1 [] o prop_of
-
-(*Extract TFree constraints from context to include as conjecture clauses*)
-fun init_tfrees ctxt =
- let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts in
- Vartab.fold add (#2 (Variable.constraints_of ctxt)) []
- |> type_literals_for_types
- end;
-
-(*Insert non-logical axioms corresponding to all accumulated TFrees*)
-fun add_tfrees {axioms, tfrees, old_skolems} : logic_map =
- {axioms = map (rpair TrueI o metis_of_tfree) (distinct (op =) tfrees) @
- axioms,
- tfrees = tfrees, old_skolems = old_skolems}
-
-(*transform isabelle type / arity clause to metis clause *)
-fun add_type_thm [] lmap = lmap
- | add_type_thm ((ith, mth) :: cls) {axioms, tfrees, old_skolems} =
- add_type_thm cls {axioms = (mth, ith) :: axioms, tfrees = tfrees,
- old_skolems = old_skolems}
-
-fun const_in_metis c (pred, tm_list) =
- let
- fun in_mterm (Metis_Term.Var _) = false
- | in_mterm (Metis_Term.Fn (".", tm_list)) = exists in_mterm tm_list
- | in_mterm (Metis_Term.Fn (nm, tm_list)) = c=nm orelse exists in_mterm tm_list
- in c = pred orelse exists in_mterm tm_list end;
-
-(* ARITY CLAUSE *)
-fun m_arity_cls (TConsLit ((c, _), (t, _), args)) =
- metis_lit true c [Metis_Term.Fn(t, map (Metis_Term.Var o fst) args)]
- | m_arity_cls (TVarLit ((c, _), (s, _))) =
- metis_lit false c [Metis_Term.Var s]
-(*TrueI is returned as the Isabelle counterpart because there isn't any.*)
-fun arity_cls (ArityClause {conclLit, premLits, ...}) =
- (TrueI,
- Metis_Thm.axiom (Metis_LiteralSet.fromList (map m_arity_cls (conclLit :: premLits))));
-
-(* CLASSREL CLAUSE *)
-fun m_class_rel_cls (subclass, _) (superclass, _) =
- [metis_lit false subclass [Metis_Term.Var "T"], metis_lit true superclass [Metis_Term.Var "T"]];
-fun class_rel_cls (ClassRelClause {subclass, superclass, ...}) =
- (TrueI, Metis_Thm.axiom (Metis_LiteralSet.fromList (m_class_rel_cls subclass superclass)));
-
-fun type_ext thy tms =
- let val subs = tfree_classes_of_terms tms
- val supers = tvar_classes_of_terms tms
- and tycons = type_consts_of_terms thy tms
- val (supers', arity_clauses) = make_arity_clauses thy tycons supers
- val class_rel_clauses = make_class_rel_clauses thy subs supers'
- in map class_rel_cls class_rel_clauses @ map arity_cls arity_clauses
- end;
-
-(* Function to generate metis clauses, including comb and type clauses *)
-fun build_logic_map mode0 ctxt type_lits cls thss =
- let val thy = ProofContext.theory_of ctxt
- (*The modes FO and FT are sticky. HO can be downgraded to FO.*)
- fun set_mode FO = FO
- | set_mode HO =
- if forall (forall (is_quasi_fol_clause thy)) (cls :: thss) then FO
- else HO
- | set_mode FT = FT
- val mode = set_mode mode0
- (*transform isabelle clause to metis clause *)
- fun add_thm th_no is_conjecture (metis_ith, isa_ith)
- {axioms, tfrees, old_skolems} : logic_map =
- let
- val (mth, tfree_lits, old_skolems) =
- hol_thm_to_fol is_conjecture th_no ctxt type_lits mode (length axioms)
- old_skolems metis_ith
- in
- {axioms = (mth, Meson.make_meta_clause isa_ith) :: axioms,
- tfrees = union (op =) tfree_lits tfrees, old_skolems = old_skolems}
- end;
- val lmap = {axioms = [], tfrees = init_tfrees ctxt, old_skolems = []}
- |> fold (add_thm 0 true o `I) cls
- |> add_tfrees
- |> fold (fn (th_no, ths) => fold (add_thm th_no false o `I) ths)
- (1 upto length thss ~~ thss)
- val clause_lists = map (Metis_Thm.clause o #1) (#axioms lmap)
- fun is_used c =
- exists (Metis_LiteralSet.exists (const_in_metis c o #2)) clause_lists
- val lmap =
- if mode = FO then
- lmap
- else
- let
- val helper_ths =
- helpers |> filter (is_used o fst)
- |> maps (fn (c, (needs_full_types, thms)) =>
- if not (is_used c) orelse
- needs_full_types andalso mode <> FT then
- []
- else
- thms)
- in lmap |> fold (add_thm ~1 false) helper_ths end
- in
- (mode, add_type_thm (type_ext thy (maps (map prop_of) (cls :: thss))) lmap)
- end
-
-end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Mon Oct 04 22:01:34 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Mon Oct 04 22:45:09 2010 +0200
@@ -585,6 +585,7 @@
fun is_formula_too_complex t =
apply_depth t > max_apply_depth orelse formula_has_too_many_lambdas [] t
+(* FIXME: Extend to "Meson" and "Metis" *)
val exists_sledgehammer_const =
exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s)