--- a/src/HOL/ATP.thy Tue May 31 11:21:47 2011 +0200
+++ b/src/HOL/ATP.thy Tue May 31 16:38:36 2011 +0200
@@ -6,12 +6,44 @@
header {* Automatic Theorem Provers (ATPs) *}
theory ATP
-imports Plain
-uses "Tools/ATP/atp_problem.ML"
+imports Meson
+uses "Tools/ATP/atp_util.ML"
+ "Tools/ATP/atp_problem.ML"
"Tools/ATP/atp_proof.ML"
"Tools/ATP/atp_systems.ML"
+ ("Tools/ATP/atp_translate.ML")
+ ("Tools/ATP/atp_reconstruct.ML")
begin
+subsection {* Higher-order reasoning helpers *}
+
+definition fFalse :: bool where [no_atp]:
+"fFalse \<longleftrightarrow> False"
+
+definition fTrue :: bool where [no_atp]:
+"fTrue \<longleftrightarrow> True"
+
+definition fNot :: "bool \<Rightarrow> bool" where [no_atp]:
+"fNot P \<longleftrightarrow> \<not> P"
+
+definition fconj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
+"fconj P Q \<longleftrightarrow> P \<and> Q"
+
+definition fdisj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
+"fdisj P Q \<longleftrightarrow> P \<or> Q"
+
+definition fimplies :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
+"fimplies P Q \<longleftrightarrow> (P \<longrightarrow> Q)"
+
+definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
+"fequal x y \<longleftrightarrow> (x = y)"
+
+
+subsection {* Setup *}
+
+use "Tools/ATP/atp_translate.ML"
+use "Tools/ATP/atp_reconstruct.ML"
+
setup ATP_Systems.setup
end
--- a/src/HOL/IsaMakefile Tue May 31 11:21:47 2011 +0200
+++ b/src/HOL/IsaMakefile Tue May 31 16:38:36 2011 +0200
@@ -300,7 +300,10 @@
$(SRC)/Provers/Arith/extract_common_term.ML \
Tools/ATP/atp_problem.ML \
Tools/ATP/atp_proof.ML \
+ Tools/ATP/atp_reconstruct.ML \
Tools/ATP/atp_systems.ML \
+ Tools/ATP/atp_translate.ML \
+ Tools/ATP/atp_util.ML \
Tools/choice_specification.ML \
Tools/code_evaluation.ML \
Tools/groebner.ML \
@@ -353,8 +356,6 @@
Tools/record.ML \
Tools/semiring_normalizer.ML \
Tools/Sledgehammer/async_manager.ML \
- Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML \
- Tools/Sledgehammer/sledgehammer_atp_translate.ML \
Tools/Sledgehammer/sledgehammer_filter.ML \
Tools/Sledgehammer/sledgehammer_minimize.ML \
Tools/Sledgehammer/sledgehammer_isar.ML \
--- a/src/HOL/Metis.thy Tue May 31 11:21:47 2011 +0200
+++ b/src/HOL/Metis.thy Tue May 31 16:38:36 2011 +0200
@@ -7,7 +7,7 @@
header {* Metis Proof Method *}
theory Metis
-imports Meson
+imports ATP
uses "~~/src/Tools/Metis/metis.ML"
("Tools/Metis/metis_translate.ML")
("Tools/Metis/metis_reconstruct.ML")
@@ -15,31 +15,6 @@
("Tools/try_methods.ML")
begin
-
-subsection {* Higher-order reasoning helpers *}
-
-definition fFalse :: bool where [no_atp]:
-"fFalse \<longleftrightarrow> False"
-
-definition fTrue :: bool where [no_atp]:
-"fTrue \<longleftrightarrow> True"
-
-definition fNot :: "bool \<Rightarrow> bool" where [no_atp]:
-"fNot P \<longleftrightarrow> \<not> P"
-
-definition fconj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
-"fconj P Q \<longleftrightarrow> P \<and> Q"
-
-definition fdisj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
-"fdisj P Q \<longleftrightarrow> P \<or> Q"
-
-definition fimplies :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
-"fimplies P Q \<longleftrightarrow> (P \<longrightarrow> Q)"
-
-definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
-"fequal x y \<longleftrightarrow> (x = y)"
-
-
subsection {* Literal selection helpers *}
definition select :: "'a \<Rightarrow> 'a" where
--- a/src/HOL/Sledgehammer.thy Tue May 31 11:21:47 2011 +0200
+++ b/src/HOL/Sledgehammer.thy Tue May 31 16:38:36 2011 +0200
@@ -11,8 +11,6 @@
uses "Tools/Sledgehammer/async_manager.ML"
"Tools/Sledgehammer/sledgehammer_util.ML"
"Tools/Sledgehammer/sledgehammer_filter.ML"
- "Tools/Sledgehammer/sledgehammer_atp_translate.ML"
- "Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML"
"Tools/Sledgehammer/sledgehammer_provers.ML"
"Tools/Sledgehammer/sledgehammer_minimize.ML"
"Tools/Sledgehammer/sledgehammer_run.ML"
--- a/src/HOL/Tools/ATP/atp_problem.ML Tue May 31 11:21:47 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Tue May 31 16:38:36 2011 +0200
@@ -70,9 +70,6 @@
-> 'd -> 'd
val formula_map : ('c -> 'd) -> ('a, 'b, 'c) formula -> ('a, 'b, 'd) formula
val is_format_typed : format -> bool
- val timestamp : unit -> string
- val hashw : word * word -> word
- val hashw_string : string * word -> word
val tptp_strings_for_atp_problem : format -> string problem -> string list
val filter_cnf_ueq_problem :
(string * string) problem -> (string * string) problem
@@ -87,6 +84,9 @@
structure ATP_Problem : ATP_PROBLEM =
struct
+open ATP_Util
+
+
(** ATP problem **)
datatype 'a fo_term = ATerm of 'a * 'a fo_term list
@@ -172,15 +172,6 @@
val is_format_typed = member (op =) [TFF, THF]
-val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now
-
-(* This hash function is recommended in "Compilers: Principles, Techniques, and
- Tools" by Aho, Sethi, and Ullman. The "hashpjw" function, which they
- particularly recommend, triggers a bug in versions of Poly/ML up to 4.2.0. *)
-fun hashw (u, w) = Word.+ (u, Word.* (0w65599, w))
-fun hashw_char (c, w) = hashw (Word.fromInt (Char.ord c), w)
-fun hashw_string (s : string, w) = CharVector.foldl hashw_char w s
-
fun string_for_kind Axiom = "axiom"
| string_for_kind Definition = "definition"
| string_for_kind Lemma = "lemma"
--- a/src/HOL/Tools/ATP/atp_proof.ML Tue May 31 11:21:47 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Tue May 31 16:38:36 2011 +0200
@@ -28,7 +28,6 @@
VampireTooOld |
NoPerl |
NoLibwwwPerl |
- NoRealZ3 |
MalformedInput |
MalformedOutput |
Interrupted |
@@ -44,7 +43,6 @@
type 'a proof = ('a, 'a, 'a fo_term) formula step list
- val strip_spaces : bool -> (char -> bool) -> string -> string
val short_output : bool -> string -> string
val string_for_failure : failure -> string
val extract_important_message : string -> string
@@ -67,6 +65,7 @@
structure ATP_Proof : ATP_PROOF =
struct
+open ATP_Util
open ATP_Problem
exception UNRECOGNIZED_ATP_PROOF of unit
@@ -85,7 +84,6 @@
VampireTooOld |
NoPerl |
NoLibwwwPerl |
- NoRealZ3 |
MalformedInput |
MalformedOutput |
Interrupted |
@@ -93,34 +91,6 @@
InternalError |
UnknownError of string
-fun strip_c_style_comment _ [] = []
- | strip_c_style_comment is_evil (#"*" :: #"/" :: cs) =
- strip_spaces_in_list true is_evil cs
- | strip_c_style_comment is_evil (_ :: cs) = strip_c_style_comment is_evil cs
-and strip_spaces_in_list _ _ [] = []
- | strip_spaces_in_list true is_evil (#"%" :: cs) =
- strip_spaces_in_list true is_evil
- (cs |> chop_while (not_equal #"\n") |> snd)
- | strip_spaces_in_list true is_evil (#"/" :: #"*" :: cs) =
- strip_c_style_comment is_evil cs
- | strip_spaces_in_list _ _ [c1] = if Char.isSpace c1 then [] else [str c1]
- | strip_spaces_in_list skip_comments is_evil [c1, c2] =
- strip_spaces_in_list skip_comments is_evil [c1] @
- strip_spaces_in_list skip_comments is_evil [c2]
- | strip_spaces_in_list skip_comments is_evil (c1 :: c2 :: c3 :: cs) =
- if Char.isSpace c1 then
- strip_spaces_in_list skip_comments is_evil (c2 :: c3 :: cs)
- else if Char.isSpace c2 then
- if Char.isSpace c3 then
- strip_spaces_in_list skip_comments is_evil (c1 :: c3 :: cs)
- else
- str c1 :: (if forall is_evil [c1, c3] then [" "] else []) @
- strip_spaces_in_list skip_comments is_evil (c3 :: cs)
- else
- str c1 :: strip_spaces_in_list skip_comments is_evil (c2 :: c3 :: cs)
-fun strip_spaces skip_comments is_evil =
- implode o strip_spaces_in_list skip_comments is_evil o String.explode
-
fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
val strip_spaces_except_between_ident_chars = strip_spaces true is_ident_char
@@ -182,12 +152,11 @@
| string_for_failure NoPerl = "Perl" ^ missing_message_tail
| string_for_failure NoLibwwwPerl =
"The Perl module \"libwww-perl\"" ^ missing_message_tail
- | string_for_failure NoRealZ3 =
- "The environment variable \"Z3_REAL_SOLVER\" must be set to Z3's full path."
| string_for_failure MalformedInput =
"The generated problem is malformed. Please report this to the Isabelle \
\developers."
| string_for_failure MalformedOutput = "The prover output is malformed."
+ | string_for_failure Interrupted = "The prover was interrupted."
| string_for_failure Crashed = "The prover crashed."
| string_for_failure InternalError = "An internal prover error occurred."
| string_for_failure (UnknownError string) =
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Tue May 31 16:38:36 2011 +0200
@@ -0,0 +1,1100 @@
+(* Title: HOL/Tools/ATP/atp_reconstruct.ML
+ Author: Lawrence C. Paulson, Cambridge University Computer Laboratory
+ Author: Claire Quigley, Cambridge University Computer Laboratory
+ Author: Jasmin Blanchette, TU Muenchen
+
+Proof reconstruction from ATP proofs.
+*)
+
+signature ATP_RECONSTRUCT =
+sig
+ type 'a proof = 'a ATP_Proof.proof
+ type locality = ATP_Translate.locality
+ type type_system = ATP_Translate.type_system
+
+ datatype reconstructor =
+ Metis |
+ MetisFT |
+ SMT of string
+
+ datatype play =
+ Played of reconstructor * Time.time |
+ Trust_Playable of reconstructor * Time.time option|
+ Failed_to_Play
+
+ type minimize_command = string list -> string
+ type one_line_params =
+ play * string * (string * locality) list * minimize_command * int * int
+ type isar_params =
+ bool * bool * int * type_system * string Symtab.table * int list list
+ * int * (string * locality) list vector * int Symtab.table * string proof
+ * thm
+ val repair_conjecture_shape_and_fact_names :
+ type_system -> string -> int list list -> int
+ -> (string * locality) list vector -> int list
+ -> int list list * int * (string * locality) list vector * int list
+ val used_facts_in_atp_proof :
+ Proof.context -> type_system -> int -> (string * locality) list vector
+ -> string proof -> (string * locality) list
+ val used_facts_in_unsound_atp_proof :
+ Proof.context -> type_system -> int list list -> int
+ -> (string * locality) list vector -> 'a proof -> string list option
+ val uses_typed_helpers : int list -> 'a proof -> bool
+ val reconstructor_name : reconstructor -> string
+ val one_line_proof_text : one_line_params -> string
+ val isar_proof_text :
+ Proof.context -> bool -> isar_params -> one_line_params -> string
+ val proof_text :
+ Proof.context -> bool -> isar_params -> one_line_params -> string
+end;
+
+structure ATP_Reconstruct : ATP_RECONSTRUCT =
+struct
+
+open ATP_Util
+open ATP_Problem
+open ATP_Proof
+open ATP_Translate
+
+datatype reconstructor =
+ Metis |
+ MetisFT |
+ SMT of string
+
+datatype play =
+ Played of reconstructor * Time.time |
+ Trust_Playable of reconstructor * Time.time option |
+ Failed_to_Play
+
+type minimize_command = string list -> string
+type one_line_params =
+ play * string * (string * locality) list * minimize_command * int * int
+type isar_params =
+ bool * bool * int * type_system * string Symtab.table * int list list * int
+ * (string * locality) list vector * int Symtab.table * string proof * thm
+
+fun is_head_digit s = Char.isDigit (String.sub (s, 0))
+val scan_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode)
+
+val is_typed_helper_name =
+ String.isPrefix helper_prefix andf String.isSuffix typed_helper_suffix
+
+fun find_first_in_list_vector vec key =
+ Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key
+ | (_, value) => value) NONE vec
+
+
+(** SPASS's FLOTTER hack **)
+
+(* This is a hack required for keeping track of facts after they have been
+ clausified by SPASS's FLOTTER preprocessor. The "ATP/scripts/spass" script is
+ also part of this hack. *)
+
+val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation"
+
+fun extract_clause_sequence output =
+ let
+ val tokens_of = String.tokens (not o Char.isAlphaNum)
+ fun extract_num ("clause" :: (ss as _ :: _)) = Int.fromString (List.last ss)
+ | extract_num _ = NONE
+ in output |> split_lines |> map_filter (extract_num o tokens_of) end
+
+val parse_clause_formula_pair =
+ $$ "(" |-- scan_integer --| $$ ","
+ -- (Symbol.scan_id ::: Scan.repeat ($$ "," |-- Symbol.scan_id)) --| $$ ")"
+ --| Scan.option ($$ ",")
+val parse_clause_formula_relation =
+ Scan.this_string set_ClauseFormulaRelationN |-- $$ "("
+ |-- Scan.repeat parse_clause_formula_pair
+val extract_clause_formula_relation =
+ Substring.full #> Substring.position set_ClauseFormulaRelationN
+ #> snd #> Substring.position "." #> fst #> Substring.string
+ #> raw_explode #> filter_out Symbol.is_blank #> parse_clause_formula_relation
+ #> fst
+
+fun maybe_unprefix_fact_number type_sys =
+ polymorphism_of_type_sys type_sys <> Polymorphic
+ ? (space_implode "_" o tl o space_explode "_")
+
+fun repair_conjecture_shape_and_fact_names type_sys output conjecture_shape
+ fact_offset fact_names typed_helpers =
+ if String.isSubstring set_ClauseFormulaRelationN output then
+ let
+ val j0 = hd (hd conjecture_shape)
+ val seq = extract_clause_sequence output
+ val name_map = extract_clause_formula_relation output
+ fun renumber_conjecture j =
+ conjecture_prefix ^ string_of_int (j - j0)
+ |> AList.find (fn (s, ss) => member (op =) ss s) name_map
+ |> map (fn s => find_index (curry (op =) s) seq + 1)
+ fun names_for_number j =
+ j |> AList.lookup (op =) name_map |> these
+ |> map_filter (try (unascii_of o maybe_unprefix_fact_number type_sys
+ o unprefix fact_prefix))
+ |> map (fn name =>
+ (name, name |> find_first_in_list_vector fact_names |> the)
+ handle Option.Option =>
+ error ("No such fact: " ^ quote name ^ "."))
+ in
+ (conjecture_shape |> map (maps renumber_conjecture), 0,
+ seq |> map names_for_number |> Vector.fromList,
+ name_map |> filter (forall is_typed_helper_name o snd) |> map fst)
+ end
+ else
+ (conjecture_shape, fact_offset, fact_names, typed_helpers)
+
+val vampire_step_prefix = "f" (* grrr... *)
+
+val extract_step_number =
+ Int.fromString o perhaps (try (unprefix vampire_step_prefix))
+
+fun resolve_fact type_sys _ fact_names (_, SOME s) =
+ (case try (unprefix fact_prefix) s of
+ SOME s' =>
+ let val s' = s' |> maybe_unprefix_fact_number type_sys |> unascii_of in
+ case find_first_in_list_vector fact_names s' of
+ SOME x => [(s', x)]
+ | NONE => []
+ end
+ | NONE => [])
+ | resolve_fact _ facts_offset fact_names (num, NONE) =
+ (case extract_step_number num of
+ SOME j =>
+ let val j = j - facts_offset in
+ if j > 0 andalso j <= Vector.length fact_names then
+ Vector.sub (fact_names, j - 1)
+ else
+ []
+ end
+ | NONE => [])
+
+fun is_fact type_sys conjecture_shape =
+ not o null o resolve_fact type_sys 0 conjecture_shape
+
+fun resolve_conjecture _ (_, SOME s) =
+ (case try (unprefix conjecture_prefix) s of
+ SOME s' =>
+ (case Int.fromString s' of
+ SOME j => [j]
+ | NONE => [])
+ | NONE => [])
+ | resolve_conjecture conjecture_shape (num, NONE) =
+ case extract_step_number num of
+ SOME i => (case find_index (exists (curry (op =) i)) conjecture_shape of
+ ~1 => []
+ | j => [j])
+ | NONE => []
+
+fun is_conjecture conjecture_shape =
+ not o null o resolve_conjecture conjecture_shape
+
+fun is_typed_helper _ (_, SOME s) = is_typed_helper_name s
+ | is_typed_helper typed_helpers (num, NONE) =
+ (case extract_step_number num of
+ SOME i => member (op =) typed_helpers i
+ | NONE => false)
+
+val leo2_ext = "extcnf_equal_neg"
+val isa_ext = Thm.get_name_hint @{thm ext}
+val isa_short_ext = Long_Name.base_name isa_ext
+
+fun ext_name ctxt =
+ if Thm.eq_thm_prop (@{thm ext},
+ singleton (Attrib.eval_thms ctxt) (Facts.named isa_short_ext, [])) then
+ isa_short_ext
+ else
+ isa_ext
+
+fun add_fact _ type_sys facts_offset fact_names (Inference (name, _, [])) =
+ union (op =) (resolve_fact type_sys facts_offset fact_names name)
+ | add_fact ctxt _ _ _ (Inference (_, _, deps)) =
+ if AList.defined (op =) deps leo2_ext then
+ insert (op =) (ext_name ctxt, General (* or Chained... *))
+ else
+ I
+ | add_fact _ _ _ _ _ = I
+
+fun used_facts_in_atp_proof ctxt type_sys facts_offset fact_names atp_proof =
+ if null atp_proof then Vector.foldl (op @) [] fact_names
+ else fold (add_fact ctxt type_sys facts_offset fact_names) atp_proof []
+
+fun is_conjecture_referred_to_in_proof conjecture_shape =
+ exists (fn Inference (name, _, []) => is_conjecture conjecture_shape name
+ | _ => false)
+
+fun used_facts_in_unsound_atp_proof ctxt type_sys conjecture_shape facts_offset
+ fact_names atp_proof =
+ let
+ val used_facts =
+ used_facts_in_atp_proof ctxt type_sys facts_offset fact_names atp_proof
+ in
+ if forall (is_locality_global o snd) used_facts andalso
+ not (is_conjecture_referred_to_in_proof conjecture_shape atp_proof) then
+ SOME (map fst used_facts)
+ else
+ NONE
+ end
+
+fun uses_typed_helpers typed_helpers =
+ exists (fn Inference (name, _, []) => is_typed_helper typed_helpers name
+ | _ => false)
+
+
+(** Soft-core proof reconstruction: Metis one-liner **)
+
+fun reconstructor_name Metis = "metis"
+ | reconstructor_name MetisFT = "metisFT"
+ | reconstructor_name (SMT _) = "smt"
+
+fun reconstructor_settings (SMT settings) = settings
+ | reconstructor_settings _ = ""
+
+fun string_for_label (s, num) = s ^ string_of_int num
+
+fun show_time NONE = ""
+ | show_time (SOME ext_time) = " (" ^ string_from_ext_time ext_time ^ ")"
+
+fun set_settings "" = ""
+ | set_settings settings = "using [[" ^ settings ^ "]] "
+fun apply_on_subgoal settings _ 1 = set_settings settings ^ "by "
+ | apply_on_subgoal settings 1 _ = set_settings settings ^ "apply "
+ | apply_on_subgoal settings i n =
+ "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal settings 1 n
+fun command_call name [] = name
+ | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
+fun try_command_line banner time command =
+ banner ^ ": " ^ Markup.markup Markup.sendback command ^ show_time time ^ "."
+fun using_labels [] = ""
+ | using_labels ls =
+ "using " ^ space_implode " " (map string_for_label ls) ^ " "
+fun reconstructor_command reconstructor i n (ls, ss) =
+ using_labels ls ^
+ apply_on_subgoal (reconstructor_settings reconstructor) i n ^
+ command_call (reconstructor_name reconstructor) ss
+fun minimize_line _ [] = ""
+ | minimize_line minimize_command ss =
+ case minimize_command ss of
+ "" => ""
+ | command => "\nTo minimize: " ^ Markup.markup Markup.sendback command ^ "."
+
+val split_used_facts =
+ List.partition (curry (op =) Chained o snd)
+ #> pairself (sort_distinct (string_ord o pairself fst))
+
+fun one_line_proof_text (preplay, banner, used_facts, minimize_command,
+ subgoal, subgoal_count) =
+ let
+ val (chained, extra) = split_used_facts used_facts
+ val (reconstructor, ext_time) =
+ case preplay of
+ Played (reconstructor, time) =>
+ (SOME reconstructor, (SOME (false, time)))
+ | Trust_Playable (reconstructor, time) =>
+ (SOME reconstructor,
+ case time of
+ NONE => NONE
+ | SOME time =>
+ if time = Time.zeroTime then NONE else SOME (true, time))
+ | Failed_to_Play => (NONE, NONE)
+ val try_line =
+ case reconstructor of
+ SOME r => ([], map fst extra)
+ |> reconstructor_command r subgoal subgoal_count
+ |> try_command_line banner ext_time
+ | NONE => "One-line proof reconstruction failed."
+ in try_line ^ minimize_line minimize_command (map fst (extra @ chained)) end
+
+(** Hard-core proof reconstruction: structured Isar proofs **)
+
+(* Simple simplifications to ensure that sort annotations don't leave a trail of
+ spurious "True"s. *)
+fun s_not (Const (@{const_name All}, T) $ Abs (s, T', t')) =
+ Const (@{const_name Ex}, T) $ Abs (s, T', s_not t')
+ | s_not (Const (@{const_name Ex}, T) $ Abs (s, T', t')) =
+ Const (@{const_name All}, T) $ Abs (s, T', s_not t')
+ | s_not (@{const HOL.implies} $ t1 $ t2) = @{const HOL.conj} $ t1 $ s_not t2
+ | s_not (@{const HOL.conj} $ t1 $ t2) =
+ @{const HOL.disj} $ s_not t1 $ s_not t2
+ | s_not (@{const HOL.disj} $ t1 $ t2) =
+ @{const HOL.conj} $ s_not t1 $ s_not t2
+ | s_not (@{const False}) = @{const True}
+ | s_not (@{const True}) = @{const False}
+ | s_not (@{const Not} $ t) = t
+ | s_not t = @{const Not} $ t
+fun s_conj (@{const True}, t2) = t2
+ | s_conj (t1, @{const True}) = t1
+ | s_conj p = HOLogic.mk_conj p
+fun s_disj (@{const False}, t2) = t2
+ | s_disj (t1, @{const False}) = t1
+ | s_disj p = HOLogic.mk_disj p
+fun s_imp (@{const True}, t2) = t2
+ | s_imp (t1, @{const False}) = s_not t1
+ | s_imp p = HOLogic.mk_imp p
+fun s_iff (@{const True}, t2) = t2
+ | s_iff (t1, @{const True}) = t1
+ | s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2
+
+fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda v t
+fun exists_of v t = HOLogic.exists_const (fastype_of v) $ lambda v t
+
+val indent_size = 2
+val no_label = ("", ~1)
+
+val raw_prefix = "X"
+val assum_prefix = "A"
+val have_prefix = "F"
+
+fun raw_label_for_name conjecture_shape name =
+ case resolve_conjecture conjecture_shape name of
+ [j] => (conjecture_prefix, j)
+ | _ => case Int.fromString (fst name) of
+ SOME j => (raw_prefix, j)
+ | NONE => (raw_prefix ^ fst name, 0)
+
+(**** INTERPRETATION OF TSTP SYNTAX TREES ****)
+
+exception FO_TERM of string fo_term list
+exception FORMULA of (string, string, string fo_term) formula list
+exception SAME of unit
+
+(* Type variables are given the basic sort "HOL.type". Some will later be
+ constrained by information from type literals, or by type inference. *)
+fun typ_from_fo_term tfrees (u as ATerm (a, us)) =
+ let val Ts = map (typ_from_fo_term tfrees) us in
+ case strip_prefix_and_unascii type_const_prefix a of
+ SOME b => Type (invert_const b, Ts)
+ | NONE =>
+ if not (null us) then
+ raise FO_TERM [u] (* only "tconst"s have type arguments *)
+ else case strip_prefix_and_unascii tfree_prefix a of
+ SOME b =>
+ let val s = "'" ^ b in
+ TFree (s, AList.lookup (op =) tfrees s |> the_default HOLogic.typeS)
+ end
+ | NONE =>
+ case strip_prefix_and_unascii tvar_prefix a of
+ SOME b => TVar (("'" ^ b, 0), HOLogic.typeS)
+ | NONE =>
+ (* Variable from the ATP, say "X1" *)
+ Type_Infer.param 0 (a, HOLogic.typeS)
+ end
+
+(* Type class literal applied to a type. Returns triple of polarity, class,
+ type. *)
+fun type_constraint_from_term tfrees (u as ATerm (a, us)) =
+ case (strip_prefix_and_unascii class_prefix a,
+ map (typ_from_fo_term tfrees) us) of
+ (SOME b, [T]) => (b, T)
+ | _ => raise FO_TERM [u]
+
+(** Accumulate type constraints in a formula: negative type literals **)
+fun add_var (key, z) = Vartab.map_default (key, []) (cons z)
+fun add_type_constraint false (cl, TFree (a ,_)) = add_var ((a, ~1), cl)
+ | add_type_constraint false (cl, TVar (ix, _)) = add_var (ix, cl)
+ | add_type_constraint _ _ = I
+
+fun repair_tptp_variable_name f s =
+ let
+ fun subscript_name s n = s ^ nat_subscript n
+ val s = String.map f s
+ in
+ case space_explode "_" s of
+ [_] => (case take_suffix Char.isDigit (String.explode s) of
+ (cs1 as _ :: _, cs2 as _ :: _) =>
+ subscript_name (String.implode cs1)
+ (the (Int.fromString (String.implode cs2)))
+ | (_, _) => s)
+ | [s1, s2] => (case Int.fromString s2 of
+ SOME n => subscript_name s1 n
+ | NONE => s)
+ | _ => s
+ end
+
+fun num_type_args thy s =
+ (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
+
+(* First-order translation. No types are known for variables. "HOLogic.typeT"
+ should allow them to be inferred. *)
+fun raw_term_from_pred thy sym_tab tfrees =
+ let
+ fun aux opt_T extra_us u =
+ case u of
+ ATerm (a, us) =>
+ if String.isPrefix simple_type_prefix a then
+ @{const True} (* ignore TPTP type information *)
+ else if a = tptp_equal then
+ let val ts = map (aux NONE []) us in
+ if length ts = 2 andalso hd ts aconv List.last ts then
+ (* Vampire is keen on producing these. *)
+ @{const True}
+ else
+ list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts)
+ end
+ else case strip_prefix_and_unascii const_prefix a of
+ SOME s =>
+ let
+ val ((s', s), mangled_us) = s |> unmangled_const |>> `invert_const
+ in
+ if s' = type_tag_name then
+ case mangled_us @ us of
+ [typ_u, term_u] =>
+ aux (SOME (typ_from_fo_term tfrees typ_u)) extra_us term_u
+ | _ => raise FO_TERM us
+ else if s' = predicator_name then
+ aux (SOME @{typ bool}) [] (hd us)
+ else if s' = app_op_name then
+ aux opt_T (nth us 1 :: extra_us) (hd us)
+ else if s' = type_pred_name then
+ @{const True} (* ignore type predicates *)
+ else
+ let
+ val num_ty_args =
+ length us - the_default 0 (Symtab.lookup sym_tab s)
+ val (type_us, term_us) =
+ chop num_ty_args us |>> append mangled_us
+ (* Extra args from "hAPP" come after any arguments given
+ directly to the constant. *)
+ val term_ts = map (aux NONE []) term_us
+ val extra_ts = map (aux NONE []) extra_us
+ val T =
+ if not (null type_us) andalso
+ num_type_args thy s' = length type_us then
+ Sign.const_instance thy
+ (s', map (typ_from_fo_term tfrees) type_us)
+ else case opt_T of
+ SOME T => map fastype_of (term_ts @ extra_ts) ---> T
+ | NONE => HOLogic.typeT
+ val s' = s' |> unproxify_const
+ in list_comb (Const (s', T), term_ts @ extra_ts) end
+ end
+ | NONE => (* a free or schematic variable *)
+ let
+ val ts = map (aux NONE []) (us @ extra_us)
+ val T = map fastype_of ts ---> HOLogic.typeT
+ val t =
+ case strip_prefix_and_unascii fixed_var_prefix a of
+ SOME b => Free (b, T)
+ | NONE =>
+ case strip_prefix_and_unascii schematic_var_prefix a of
+ SOME b => Var ((b, 0), T)
+ | NONE =>
+ if is_tptp_variable a then
+ Var ((repair_tptp_variable_name Char.toLower a, 0), T)
+ else
+ (* Skolem constants? *)
+ Var ((repair_tptp_variable_name Char.toUpper a, 0), T)
+ in list_comb (t, ts) end
+ in aux (SOME HOLogic.boolT) [] end
+
+fun term_from_pred thy sym_tab tfrees pos (u as ATerm (s, _)) =
+ if String.isPrefix class_prefix s then
+ add_type_constraint pos (type_constraint_from_term tfrees u)
+ #> pair @{const True}
+ else
+ pair (raw_term_from_pred thy sym_tab tfrees u)
+
+val combinator_table =
+ [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def_raw}),
+ (@{const_name Meson.COMBK}, @{thm Meson.COMBK_def_raw}),
+ (@{const_name Meson.COMBB}, @{thm Meson.COMBB_def_raw}),
+ (@{const_name Meson.COMBC}, @{thm Meson.COMBC_def_raw}),
+ (@{const_name Meson.COMBS}, @{thm Meson.COMBS_def_raw})]
+
+fun uncombine_term thy =
+ let
+ fun aux (t1 $ t2) = betapply (pairself aux (t1, t2))
+ | aux (Abs (s, T, t')) = Abs (s, T, aux t')
+ | aux (t as Const (x as (s, _))) =
+ (case AList.lookup (op =) combinator_table s of
+ SOME thm => thm |> prop_of |> specialize_type thy x
+ |> Logic.dest_equals |> snd
+ | NONE => t)
+ | aux t = t
+ in aux end
+
+(* Update schematic type variables with detected sort constraints. It's not
+ totally clear whether this code is necessary. *)
+fun repair_tvar_sorts (t, tvar_tab) =
+ let
+ fun do_type (Type (a, Ts)) = Type (a, map do_type Ts)
+ | do_type (TVar (xi, s)) =
+ TVar (xi, the_default s (Vartab.lookup tvar_tab xi))
+ | do_type (TFree z) = TFree z
+ fun do_term (Const (a, T)) = Const (a, do_type T)
+ | do_term (Free (a, T)) = Free (a, do_type T)
+ | do_term (Var (xi, T)) = Var (xi, do_type T)
+ | do_term (t as Bound _) = t
+ | do_term (Abs (a, T, t)) = Abs (a, do_type T, do_term t)
+ | do_term (t1 $ t2) = do_term t1 $ do_term t2
+ in t |> not (Vartab.is_empty tvar_tab) ? do_term end
+
+fun quantify_over_var quant_of var_s t =
+ let
+ val vars = [] |> Term.add_vars t |> filter (fn ((s, _), _) => s = var_s)
+ |> map Var
+ in fold_rev quant_of vars t end
+
+(* Interpret an ATP formula as a HOL term, extracting sort constraints as they
+ appear in the formula. *)
+fun prop_from_formula thy sym_tab tfrees phi =
+ let
+ fun do_formula pos phi =
+ case phi of
+ AQuant (_, [], phi) => do_formula pos phi
+ | AQuant (q, (s, _) :: xs, phi') =>
+ do_formula pos (AQuant (q, xs, phi'))
+ (* FIXME: TFF *)
+ #>> quantify_over_var (case q of
+ AForall => forall_of
+ | AExists => exists_of)
+ (repair_tptp_variable_name Char.toLower s)
+ | AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not
+ | AConn (c, [phi1, phi2]) =>
+ do_formula (pos |> c = AImplies ? not) phi1
+ ##>> do_formula pos phi2
+ #>> (case c of
+ AAnd => s_conj
+ | AOr => s_disj
+ | AImplies => s_imp
+ | AIf => s_imp o swap
+ | AIff => s_iff
+ | ANotIff => s_not o s_iff
+ | _ => raise Fail "unexpected connective")
+ | AAtom tm => term_from_pred thy sym_tab tfrees pos tm
+ | _ => raise FORMULA [phi]
+ in repair_tvar_sorts (do_formula true phi Vartab.empty) end
+
+fun check_formula ctxt =
+ Type.constraint HOLogic.boolT
+ #> Syntax.check_term
+ (Proof_Context.set_mode Proof_Context.mode_schematic ctxt)
+
+(**** Translation of TSTP files to Isar Proofs ****)
+
+fun unvarify_term (Var ((s, 0), T)) = Free (s, T)
+ | unvarify_term t = raise TERM ("unvarify_term: non-Var", [t])
+
+fun decode_line sym_tab tfrees (Definition (name, phi1, phi2)) ctxt =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val t1 = prop_from_formula thy sym_tab tfrees phi1
+ val vars = snd (strip_comb t1)
+ val frees = map unvarify_term vars
+ val unvarify_args = subst_atomic (vars ~~ frees)
+ val t2 = prop_from_formula thy sym_tab tfrees phi2
+ val (t1, t2) =
+ HOLogic.eq_const HOLogic.typeT $ t1 $ t2
+ |> unvarify_args |> uncombine_term thy |> check_formula ctxt
+ |> HOLogic.dest_eq
+ in
+ (Definition (name, t1, t2),
+ fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt)
+ end
+ | decode_line sym_tab tfrees (Inference (name, u, deps)) ctxt =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val t = u |> prop_from_formula thy sym_tab tfrees
+ |> uncombine_term thy |> check_formula ctxt
+ in
+ (Inference (name, t, deps),
+ fold Variable.declare_term (OldTerm.term_frees t) ctxt)
+ end
+fun decode_lines ctxt sym_tab tfrees lines =
+ fst (fold_map (decode_line sym_tab tfrees) lines ctxt)
+
+fun is_same_inference _ (Definition _) = false
+ | is_same_inference t (Inference (_, t', _)) = t aconv t'
+
+(* No "real" literals means only type information (tfree_tcs, clsrel, or
+ clsarity). *)
+val is_only_type_information = curry (op aconv) HOLogic.true_const
+
+fun replace_one_dependency (old, new) dep =
+ if is_same_atp_step dep old then new else [dep]
+fun replace_dependencies_in_line _ (line as Definition _) = line
+ | replace_dependencies_in_line p (Inference (name, t, deps)) =
+ Inference (name, t, fold (union (op =) o replace_one_dependency p) deps [])
+
+(* Discard facts; consolidate adjacent lines that prove the same formula, since
+ they differ only in type information.*)
+fun add_line _ _ _ (line as Definition _) lines = line :: lines
+ | add_line type_sys conjecture_shape fact_names (Inference (name, t, []))
+ lines =
+ (* No dependencies: fact, conjecture, or (for Vampire) internal facts or
+ definitions. *)
+ if is_fact type_sys fact_names name then
+ (* Facts are not proof lines. *)
+ if is_only_type_information t then
+ map (replace_dependencies_in_line (name, [])) lines
+ (* Is there a repetition? If so, replace later line by earlier one. *)
+ else case take_prefix (not o is_same_inference t) lines of
+ (_, []) => lines (* no repetition of proof line *)
+ | (pre, Inference (name', _, _) :: post) =>
+ pre @ map (replace_dependencies_in_line (name', [name])) post
+ | _ => raise Fail "unexpected inference"
+ else if is_conjecture conjecture_shape name then
+ Inference (name, s_not t, []) :: lines
+ else
+ map (replace_dependencies_in_line (name, [])) lines
+ | add_line _ _ _ (Inference (name, t, deps)) lines =
+ (* Type information will be deleted later; skip repetition test. *)
+ if is_only_type_information t then
+ Inference (name, t, deps) :: lines
+ (* Is there a repetition? If so, replace later line by earlier one. *)
+ else case take_prefix (not o is_same_inference t) lines of
+ (* FIXME: Doesn't this code risk conflating proofs involving different
+ types? *)
+ (_, []) => Inference (name, t, deps) :: lines
+ | (pre, Inference (name', t', _) :: post) =>
+ Inference (name, t', deps) ::
+ pre @ map (replace_dependencies_in_line (name', [name])) post
+ | _ => raise Fail "unexpected inference"
+
+(* Recursively delete empty lines (type information) from the proof. *)
+fun add_nontrivial_line (Inference (name, t, [])) lines =
+ if is_only_type_information t then delete_dependency name lines
+ else Inference (name, t, []) :: lines
+ | add_nontrivial_line line lines = line :: lines
+and delete_dependency name lines =
+ fold_rev add_nontrivial_line
+ (map (replace_dependencies_in_line (name, [])) lines) []
+
+(* ATPs sometimes reuse free variable names in the strangest ways. Removing
+ offending lines often does the trick. *)
+fun is_bad_free frees (Free x) = not (member (op =) frees x)
+ | is_bad_free _ _ = false
+
+fun add_desired_line _ _ _ _ _ (line as Definition (name, _, _)) (j, lines) =
+ (j, line :: map (replace_dependencies_in_line (name, [])) lines)
+ | add_desired_line type_sys isar_shrink_factor conjecture_shape fact_names
+ frees (Inference (name, t, deps)) (j, lines) =
+ (j + 1,
+ if is_fact type_sys fact_names name orelse
+ is_conjecture conjecture_shape name orelse
+ (* the last line must be kept *)
+ j = 0 orelse
+ (not (is_only_type_information t) andalso
+ null (Term.add_tvars t []) andalso
+ not (exists_subterm (is_bad_free frees) t) andalso
+ length deps >= 2 andalso j mod isar_shrink_factor = 0 andalso
+ (* kill next to last line, which usually results in a trivial step *)
+ j <> 1) then
+ Inference (name, t, deps) :: lines (* keep line *)
+ else
+ map (replace_dependencies_in_line (name, deps)) lines) (* drop line *)
+
+(** Isar proof construction and manipulation **)
+
+fun merge_fact_sets (ls1, ss1) (ls2, ss2) =
+ (union (op =) ls1 ls2, union (op =) ss1 ss2)
+
+type label = string * int
+type facts = label list * string list
+
+datatype isar_qualifier = Show | Then | Moreover | Ultimately
+
+datatype isar_step =
+ Fix of (string * typ) list |
+ Let of term * term |
+ Assume of label * term |
+ Have of isar_qualifier list * label * term * byline
+and byline =
+ ByMetis of facts |
+ CaseSplit of isar_step list list * facts
+
+fun smart_case_split [] facts = ByMetis facts
+ | smart_case_split proofs facts = CaseSplit (proofs, facts)
+
+fun add_fact_from_dependency type_sys conjecture_shape facts_offset fact_names
+ name =
+ if is_fact type_sys fact_names name then
+ apsnd (union (op =)
+ (map fst (resolve_fact type_sys facts_offset fact_names name)))
+ else
+ apfst (insert (op =) (raw_label_for_name conjecture_shape name))
+
+fun step_for_line _ _ _ _ _ (Definition (_, t1, t2)) = Let (t1, t2)
+ | step_for_line _ conjecture_shape _ _ _ (Inference (name, t, [])) =
+ Assume (raw_label_for_name conjecture_shape name, t)
+ | step_for_line type_sys conjecture_shape facts_offset
+ fact_names j (Inference (name, t, deps)) =
+ Have (if j = 1 then [Show] else [],
+ raw_label_for_name conjecture_shape name,
+ fold_rev forall_of (map Var (Term.add_vars t [])) t,
+ ByMetis (fold (add_fact_from_dependency type_sys conjecture_shape
+ facts_offset fact_names)
+ deps ([], [])))
+
+fun repair_name "$true" = "c_True"
+ | repair_name "$false" = "c_False"
+ | repair_name "$$e" = tptp_equal (* seen in Vampire proofs *)
+ | repair_name s =
+ if is_tptp_equal s orelse
+ (* seen in Vampire proofs *)
+ (String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s) then
+ tptp_equal
+ else
+ s
+
+fun isar_proof_from_atp_proof pool ctxt type_sys tfrees isar_shrink_factor
+ conjecture_shape facts_offset fact_names sym_tab params frees
+ atp_proof =
+ let
+ val lines =
+ atp_proof
+ |> clean_up_atp_proof_dependencies
+ |> nasty_atp_proof pool
+ |> map_term_names_in_atp_proof repair_name
+ |> decode_lines ctxt sym_tab tfrees
+ |> rpair [] |-> fold_rev (add_line type_sys conjecture_shape fact_names)
+ |> rpair [] |-> fold_rev add_nontrivial_line
+ |> rpair (0, [])
+ |-> fold_rev (add_desired_line type_sys isar_shrink_factor
+ conjecture_shape fact_names frees)
+ |> snd
+ in
+ (if null params then [] else [Fix params]) @
+ map2 (step_for_line type_sys conjecture_shape facts_offset fact_names)
+ (length lines downto 1) lines
+ end
+
+(* When redirecting proofs, we keep information about the labels seen so far in
+ the "backpatches" data structure. The first component indicates which facts
+ should be associated with forthcoming proof steps. The second component is a
+ pair ("assum_ls", "drop_ls"), where "assum_ls" are the labels that should
+ become assumptions and "drop_ls" are the labels that should be dropped in a
+ case split. *)
+type backpatches = (label * facts) list * (label list * label list)
+
+fun used_labels_of_step (Have (_, _, _, by)) =
+ (case by of
+ ByMetis (ls, _) => ls
+ | CaseSplit (proofs, (ls, _)) =>
+ fold (union (op =) o used_labels_of) proofs ls)
+ | used_labels_of_step _ = []
+and used_labels_of proof = fold (union (op =) o used_labels_of_step) proof []
+
+fun new_labels_of_step (Fix _) = []
+ | new_labels_of_step (Let _) = []
+ | new_labels_of_step (Assume (l, _)) = [l]
+ | new_labels_of_step (Have (_, l, _, _)) = [l]
+val new_labels_of = maps new_labels_of_step
+
+val join_proofs =
+ let
+ fun aux _ [] = NONE
+ | aux proof_tail (proofs as (proof1 :: _)) =
+ if exists null proofs then
+ NONE
+ else if forall (curry (op =) (hd proof1) o hd) (tl proofs) then
+ aux (hd proof1 :: proof_tail) (map tl proofs)
+ else case hd proof1 of
+ Have ([], l, t, _) => (* FIXME: should we really ignore the "by"? *)
+ if forall (fn Have ([], l', t', _) :: _ => (l, t) = (l', t')
+ | _ => false) (tl proofs) andalso
+ not (exists (member (op =) (maps new_labels_of proofs))
+ (used_labels_of proof_tail)) then
+ SOME (l, t, map rev proofs, proof_tail)
+ else
+ NONE
+ | _ => NONE
+ in aux [] o map rev end
+
+fun case_split_qualifiers proofs =
+ case length proofs of
+ 0 => []
+ | 1 => [Then]
+ | _ => [Ultimately]
+
+fun redirect_proof hyp_ts concl_t proof =
+ let
+ (* The first pass outputs those steps that are independent of the negated
+ conjecture. The second pass flips the proof by contradiction to obtain a
+ direct proof, introducing case splits when an inference depends on
+ several facts that depend on the negated conjecture. *)
+ val concl_l = (conjecture_prefix, length hyp_ts)
+ fun first_pass ([], contra) = ([], contra)
+ | first_pass ((step as Fix _) :: proof, contra) =
+ first_pass (proof, contra) |>> cons step
+ | first_pass ((step as Let _) :: proof, contra) =
+ first_pass (proof, contra) |>> cons step
+ | first_pass ((step as Assume (l as (_, j), _)) :: proof, contra) =
+ if l = concl_l then first_pass (proof, contra ||> cons step)
+ else first_pass (proof, contra) |>> cons (Assume (l, nth hyp_ts j))
+ | first_pass (Have (qs, l, t, ByMetis (ls, ss)) :: proof, contra) =
+ let val step = Have (qs, l, t, ByMetis (ls, ss)) in
+ if exists (member (op =) (fst contra)) ls then
+ first_pass (proof, contra |>> cons l ||> cons step)
+ else
+ first_pass (proof, contra) |>> cons step
+ end
+ | first_pass _ = raise Fail "malformed proof"
+ val (proof_top, (contra_ls, contra_proof)) =
+ first_pass (proof, ([concl_l], []))
+ val backpatch_label = the_default ([], []) oo AList.lookup (op =) o fst
+ fun backpatch_labels patches ls =
+ fold merge_fact_sets (map (backpatch_label patches) ls) ([], [])
+ fun second_pass end_qs ([], assums, patches) =
+ ([Have (end_qs, no_label, concl_t,
+ ByMetis (backpatch_labels patches (map snd assums)))], patches)
+ | second_pass end_qs (Assume (l, t) :: proof, assums, patches) =
+ second_pass end_qs (proof, (t, l) :: assums, patches)
+ | second_pass end_qs (Have (qs, l, t, ByMetis (ls, ss)) :: proof, assums,
+ patches) =
+ (if member (op =) (snd (snd patches)) l andalso
+ not (member (op =) (fst (snd patches)) l) andalso
+ not (AList.defined (op =) (fst patches) l) then
+ second_pass end_qs (proof, assums, patches ||> apsnd (append ls))
+ else case List.partition (member (op =) contra_ls) ls of
+ ([contra_l], co_ls) =>
+ if member (op =) qs Show then
+ second_pass end_qs (proof, assums,
+ patches |>> cons (contra_l, (co_ls, ss)))
+ else
+ second_pass end_qs
+ (proof, assums,
+ patches |>> cons (contra_l, (l :: co_ls, ss)))
+ |>> cons (if member (op =) (fst (snd patches)) l then
+ Assume (l, s_not t)
+ else
+ Have (qs, l, s_not t,
+ ByMetis (backpatch_label patches l)))
+ | (contra_ls as _ :: _, co_ls) =>
+ let
+ val proofs =
+ map_filter
+ (fn l =>
+ if l = concl_l then
+ NONE
+ else
+ let
+ val drop_ls = filter (curry (op <>) l) contra_ls
+ in
+ second_pass []
+ (proof, assums,
+ patches ||> apfst (insert (op =) l)
+ ||> apsnd (union (op =) drop_ls))
+ |> fst |> SOME
+ end) contra_ls
+ val (assumes, facts) =
+ if member (op =) (fst (snd patches)) l then
+ ([Assume (l, s_not t)], (l :: co_ls, ss))
+ else
+ ([], (co_ls, ss))
+ in
+ (case join_proofs proofs of
+ SOME (l, t, proofs, proof_tail) =>
+ Have (case_split_qualifiers proofs @
+ (if null proof_tail then end_qs else []), l, t,
+ smart_case_split proofs facts) :: proof_tail
+ | NONE =>
+ [Have (case_split_qualifiers proofs @ end_qs, no_label,
+ concl_t, smart_case_split proofs facts)],
+ patches)
+ |>> append assumes
+ end
+ | _ => raise Fail "malformed proof")
+ | second_pass _ _ = raise Fail "malformed proof"
+ val proof_bottom =
+ second_pass [Show] (contra_proof, [], ([], ([], []))) |> fst
+ in proof_top @ proof_bottom end
+
+(* FIXME: Still needed? Probably not. *)
+val kill_duplicate_assumptions_in_proof =
+ let
+ fun relabel_facts subst =
+ apfst (map (fn l => AList.lookup (op =) subst l |> the_default l))
+ fun do_step (step as Assume (l, t)) (proof, subst, assums) =
+ (case AList.lookup (op aconv) assums t of
+ SOME l' => (proof, (l, l') :: subst, assums)
+ | NONE => (step :: proof, subst, (t, l) :: assums))
+ | do_step (Have (qs, l, t, by)) (proof, subst, assums) =
+ (Have (qs, l, t,
+ case by of
+ ByMetis facts => ByMetis (relabel_facts subst facts)
+ | CaseSplit (proofs, facts) =>
+ CaseSplit (map do_proof proofs, relabel_facts subst facts)) ::
+ proof, subst, assums)
+ | do_step step (proof, subst, assums) = (step :: proof, subst, assums)
+ and do_proof proof = fold do_step proof ([], [], []) |> #1 |> rev
+ in do_proof end
+
+val then_chain_proof =
+ let
+ fun aux _ [] = []
+ | aux _ ((step as Assume (l, _)) :: proof) = step :: aux l proof
+ | aux l' (Have (qs, l, t, by) :: proof) =
+ (case by of
+ ByMetis (ls, ss) =>
+ Have (if member (op =) ls l' then
+ (Then :: qs, l, t,
+ ByMetis (filter_out (curry (op =) l') ls, ss))
+ else
+ (qs, l, t, ByMetis (ls, ss)))
+ | CaseSplit (proofs, facts) =>
+ Have (qs, l, t, CaseSplit (map (aux no_label) proofs, facts))) ::
+ aux l proof
+ | aux _ (step :: proof) = step :: aux no_label proof
+ in aux no_label end
+
+fun kill_useless_labels_in_proof proof =
+ let
+ val used_ls = used_labels_of proof
+ fun do_label l = if member (op =) used_ls l then l else no_label
+ fun do_step (Assume (l, t)) = Assume (do_label l, t)
+ | do_step (Have (qs, l, t, by)) =
+ Have (qs, do_label l, t,
+ case by of
+ CaseSplit (proofs, facts) =>
+ CaseSplit (map (map do_step) proofs, facts)
+ | _ => by)
+ | do_step step = step
+ in map do_step proof end
+
+fun prefix_for_depth n = replicate_string (n + 1)
+
+val relabel_proof =
+ let
+ fun aux _ _ _ [] = []
+ | aux subst depth (next_assum, next_fact) (Assume (l, t) :: proof) =
+ if l = no_label then
+ Assume (l, t) :: aux subst depth (next_assum, next_fact) proof
+ else
+ let val l' = (prefix_for_depth depth assum_prefix, next_assum) in
+ Assume (l', t) ::
+ aux ((l, l') :: subst) depth (next_assum + 1, next_fact) proof
+ end
+ | aux subst depth (next_assum, next_fact) (Have (qs, l, t, by) :: proof) =
+ let
+ val (l', subst, next_fact) =
+ if l = no_label then
+ (l, subst, next_fact)
+ else
+ let
+ val l' = (prefix_for_depth depth have_prefix, next_fact)
+ in (l', (l, l') :: subst, next_fact + 1) end
+ val relabel_facts =
+ apfst (maps (the_list o AList.lookup (op =) subst))
+ val by =
+ case by of
+ ByMetis facts => ByMetis (relabel_facts facts)
+ | CaseSplit (proofs, facts) =>
+ CaseSplit (map (aux subst (depth + 1) (1, 1)) proofs,
+ relabel_facts facts)
+ in
+ Have (qs, l', t, by) ::
+ aux subst depth (next_assum, next_fact) proof
+ end
+ | aux subst depth nextp (step :: proof) =
+ step :: aux subst depth nextp proof
+ in aux [] 0 (1, 1) end
+
+fun string_for_proof ctxt0 full_types i n =
+ let
+ val ctxt =
+ ctxt0 |> Config.put show_free_types false
+ |> Config.put show_types true
+ |> Config.put show_sorts true
+ fun fix_print_mode f x =
+ Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
+ (print_mode_value ())) f x
+ fun do_indent ind = replicate_string (ind * indent_size) " "
+ fun do_free (s, T) =
+ maybe_quote s ^ " :: " ^
+ maybe_quote (fix_print_mode (Syntax.string_of_typ ctxt) T)
+ fun do_label l = if l = no_label then "" else string_for_label l ^ ": "
+ fun do_have qs =
+ (if member (op =) qs Moreover then "moreover " else "") ^
+ (if member (op =) qs Ultimately then "ultimately " else "") ^
+ (if member (op =) qs Then then
+ if member (op =) qs Show then "thus" else "hence"
+ else
+ if member (op =) qs Show then "show" else "have")
+ val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
+ val reconstructor = if full_types then MetisFT else Metis
+ fun do_facts (ls, ss) =
+ reconstructor_command reconstructor 1 1
+ (ls |> sort_distinct (prod_ord string_ord int_ord),
+ ss |> sort_distinct string_ord)
+ and do_step ind (Fix xs) =
+ do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n"
+ | do_step ind (Let (t1, t2)) =
+ do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n"
+ | do_step ind (Assume (l, t)) =
+ do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n"
+ | do_step ind (Have (qs, l, t, ByMetis facts)) =
+ do_indent ind ^ do_have qs ^ " " ^
+ do_label l ^ do_term t ^ " " ^ do_facts facts ^ "\n"
+ | do_step ind (Have (qs, l, t, CaseSplit (proofs, facts))) =
+ space_implode (do_indent ind ^ "moreover\n")
+ (map (do_block ind) proofs) ^
+ do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ " " ^
+ do_facts facts ^ "\n"
+ and do_steps prefix suffix ind steps =
+ let val s = implode (map (do_step ind) steps) in
+ replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
+ String.extract (s, ind * indent_size,
+ SOME (size s - ind * indent_size - 1)) ^
+ suffix ^ "\n"
+ end
+ and do_block ind proof = do_steps "{ " " }" (ind + 1) proof
+ (* One-step proofs are pointless; better use the Metis one-liner
+ directly. *)
+ and do_proof [Have (_, _, _, ByMetis _)] = ""
+ | do_proof proof =
+ (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
+ do_indent 0 ^ "proof -\n" ^ do_steps "" "" 1 proof ^ do_indent 0 ^
+ (if n <> 1 then "next" else "qed")
+ in do_proof end
+
+fun isar_proof_text ctxt isar_proof_requested
+ (debug, full_types, isar_shrink_factor, type_sys, pool,
+ conjecture_shape, facts_offset, fact_names, sym_tab, atp_proof, goal)
+ (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
+ let
+ val isar_shrink_factor =
+ (if isar_proof_requested then 1 else 2) * isar_shrink_factor
+ val (params, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal
+ val frees = fold Term.add_frees (concl_t :: hyp_ts) []
+ val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) []
+ val one_line_proof = one_line_proof_text one_line_params
+ fun isar_proof_for () =
+ case atp_proof
+ |> isar_proof_from_atp_proof pool ctxt type_sys tfrees
+ isar_shrink_factor conjecture_shape facts_offset
+ fact_names sym_tab params frees
+ |> redirect_proof hyp_ts concl_t
+ |> kill_duplicate_assumptions_in_proof
+ |> then_chain_proof
+ |> kill_useless_labels_in_proof
+ |> relabel_proof
+ |> string_for_proof ctxt full_types subgoal subgoal_count of
+ "" =>
+ if isar_proof_requested then
+ "\nNo structured proof available (proof too short)."
+ else
+ ""
+ | proof =>
+ "\n\n" ^ (if isar_proof_requested then "Structured proof"
+ else "Perhaps this will work") ^
+ ":\n" ^ Markup.markup Markup.sendback proof
+ val isar_proof =
+ if debug then
+ isar_proof_for ()
+ else
+ case try isar_proof_for () of
+ SOME s => s
+ | NONE => if isar_proof_requested then
+ "\nWarning: The Isar proof construction failed."
+ else
+ ""
+ in one_line_proof ^ isar_proof end
+
+fun proof_text ctxt isar_proof isar_params
+ (one_line_params as (preplay, _, _, _, _, _)) =
+ (if isar_proof orelse preplay = Failed_to_Play then
+ isar_proof_text ctxt isar_proof isar_params
+ else
+ one_line_proof_text) one_line_params
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP/atp_translate.ML Tue May 31 16:38:36 2011 +0200
@@ -0,0 +1,1858 @@
+(* Title: HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
+ Author: Fabian Immler, TU Muenchen
+ Author: Makarius
+ Author: Jasmin Blanchette, TU Muenchen
+
+Translation of HOL to FOL for Sledgehammer.
+*)
+
+signature ATP_TRANSLATE =
+sig
+ type 'a fo_term = 'a ATP_Problem.fo_term
+ type format = ATP_Problem.format
+ type formula_kind = ATP_Problem.formula_kind
+ type 'a problem = 'a ATP_Problem.problem
+
+ type name = string * string
+
+ datatype type_literal =
+ TyLitVar of name * name |
+ TyLitFree of name * name
+
+ datatype arity_literal =
+ TConsLit of name * name * name list |
+ TVarLit of name * name
+
+ datatype arity_clause =
+ ArityClause of
+ {name: string,
+ prem_lits: arity_literal list,
+ concl_lits: arity_literal}
+
+ datatype class_rel_clause =
+ ClassRelClause of {name: string, subclass: name, superclass: name}
+
+ datatype combterm =
+ CombConst of name * typ * typ list |
+ CombVar of name * typ |
+ CombApp of combterm * combterm
+
+ datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained
+
+ datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
+ datatype type_level =
+ All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
+ datatype type_heaviness = Heavy | Light
+
+ datatype type_system =
+ Simple_Types of type_level |
+ Preds of polymorphism * type_level * type_heaviness |
+ Tags of polymorphism * type_level * type_heaviness
+
+ type translated_formula
+
+ val readable_names : bool Config.T
+ val type_tag_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 skolem_const_prefix : string
+ val old_skolem_const_prefix : string
+ val new_skolem_const_prefix : string
+ val fact_prefix : string
+ val conjecture_prefix : string
+ val helper_prefix : string
+ val typed_helper_suffix : string
+ val predicator_name : string
+ val app_op_name : string
+ val type_pred_name : string
+ val simple_type_prefix : string
+ val ascii_of: string -> string
+ val unascii_of: string -> string
+ val strip_prefix_and_unascii : string -> string -> string option
+ val proxify_const : string -> (int * (string * string)) option
+ val invert_const: string -> string
+ val unproxify_const: string -> string
+ 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 make_arity_clauses :
+ theory -> string list -> class list -> class list * arity_clause list
+ val make_class_rel_clauses :
+ theory -> class list -> class list -> class_rel_clause list
+ val combtyp_of : combterm -> typ
+ val strip_combterm_comb : combterm -> combterm * combterm list
+ val atyps_of : typ -> typ list
+ val combterm_from_term :
+ theory -> (string * typ) list -> term -> combterm * typ list
+ val is_locality_global : locality -> bool
+ val type_sys_from_string : string -> type_system
+ val polymorphism_of_type_sys : type_system -> polymorphism
+ val level_of_type_sys : type_system -> type_level
+ val is_type_sys_virtually_sound : type_system -> bool
+ val is_type_sys_fairly_sound : type_system -> bool
+ val raw_type_literals_for_types : typ list -> type_literal list
+ val unmangled_const : string -> string * string fo_term list
+ val translate_atp_fact :
+ Proof.context -> format -> type_system -> bool -> (string * locality) * thm
+ -> translated_formula option * ((string * locality) * thm)
+ val helper_table : (string * (bool * thm list)) list
+ 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 prepare_atp_problem :
+ Proof.context -> format -> formula_kind -> formula_kind -> type_system
+ -> bool option -> term list -> term
+ -> (translated_formula option * ((string * 'a) * thm)) list
+ -> string problem * string Symtab.table * int * int
+ * (string * 'a) list vector * int list * int Symtab.table
+ val atp_problem_weights : string problem -> (string * real) list
+end;
+
+structure ATP_Translate : ATP_TRANSLATE =
+struct
+
+open ATP_Util
+open ATP_Problem
+
+type name = string * string
+
+(* FIXME: avoid *)
+fun union_all xss = fold (union (op =)) xss []
+
+(* experimental *)
+val generate_useful_info = false
+
+fun useful_isabelle_info s =
+ if generate_useful_info then
+ SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])]))
+ else
+ NONE
+
+val intro_info = useful_isabelle_info "intro"
+val elim_info = useful_isabelle_info "elim"
+val simp_info = useful_isabelle_info "simp"
+
+(* Readable names are often much shorter, especially if types are mangled in
+ names. Also, the logic for generating legal SNARK sort names is only
+ implemented for readable names. Finally, readable names are, well, more
+ readable. For these reason, they are enabled by default. *)
+val readable_names =
+ Attrib.setup_config_bool @{binding sledgehammer_atp_readable_names} (K true)
+
+val type_tag_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 = "cl_"
+
+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"
+
+val type_decl_prefix = "ty_"
+val sym_decl_prefix = "sy_"
+val sym_formula_prefix = "sym_"
+val fact_prefix = "fact_"
+val conjecture_prefix = "conj_"
+val helper_prefix = "help_"
+val class_rel_clause_prefix = "crel_";
+val arity_clause_prefix = "arity_"
+val tfree_clause_prefix = "tfree_"
+
+val typed_helper_suffix = "_T"
+val untyped_helper_suffix = "_U"
+
+val predicator_name = "hBOOL"
+val app_op_name = "hAPP"
+val type_pred_name = "is"
+val simple_type_prefix = "ty_"
+
+(* Freshness almost guaranteed! *)
+val sledgehammer_weak_prefix = "Sledgehammer:"
+
+(*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 upper_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) ^ string_of_int (n mod 10)
+
+fun ascii_of_char 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 + upper_a_minus_space))
+ else
+ (* fixed width, in case more digits follow *)
+ "_" ^ stringN_of_int 3 (Char.ord c)
+
+val ascii_of = String.translate ascii_of_char
+
+(** Remove ASCII armoring from names in proof files **)
+
+(* We don't raise error exceptions because this code can run inside a worker
+ thread. Also, the errors are impossible. *)
+val unascii_of =
+ let
+ fun un rcs [] = String.implode(rev rcs)
+ | un rcs [#"_"] = un (#"_" :: rcs) [] (* ERROR *)
+ (* Three types of _ escapes: __, _A to _P, _nnn *)
+ | un rcs (#"_" :: #"_" :: cs) = un (#"_"::rcs) cs
+ | un rcs (#"_" :: c :: cs) =
+ if #"A" <= c andalso c<= #"P" then
+ (* translation of #" " to #"/" *)
+ un (Char.chr (Char.ord c - upper_a_minus_space) :: rcs) cs
+ else
+ let val digits = List.take (c::cs, 3) handle Subscript => [] in
+ case Int.fromString (String.implode digits) of
+ SOME n => un (Char.chr n :: rcs) (List.drop (cs, 2))
+ | NONE => un (c:: #"_"::rcs) cs (* ERROR *)
+ end
+ | un rcs (c :: cs) = un (c :: rcs) cs
+ in un [] o String.explode end
+
+(* 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
+
+val proxies =
+ [("c_False",
+ (@{const_name False}, (0, ("fFalse", @{const_name ATP.fFalse})))),
+ ("c_True", (@{const_name True}, (0, ("fTrue", @{const_name ATP.fTrue})))),
+ ("c_Not", (@{const_name Not}, (1, ("fNot", @{const_name ATP.fNot})))),
+ ("c_conj", (@{const_name conj}, (2, ("fconj", @{const_name ATP.fconj})))),
+ ("c_disj", (@{const_name disj}, (2, ("fdisj", @{const_name ATP.fdisj})))),
+ ("c_implies",
+ (@{const_name implies}, (2, ("fimplies", @{const_name ATP.fimplies})))),
+ ("equal",
+ (@{const_name HOL.eq}, (2, ("fequal", @{const_name ATP.fequal}))))]
+
+val proxify_const = AList.lookup (op =) proxies #> Option.map snd
+
+(* Readable names for the more common symbolic functions. Do not mess with the
+ table unless you know what you are doing. *)
+val const_trans_table =
+ [(@{type_name Product_Type.prod}, "prod"),
+ (@{type_name Sum_Type.sum}, "sum"),
+ (@{const_name False}, "False"),
+ (@{const_name True}, "True"),
+ (@{const_name Not}, "Not"),
+ (@{const_name conj}, "conj"),
+ (@{const_name disj}, "disj"),
+ (@{const_name implies}, "implies"),
+ (@{const_name HOL.eq}, "equal"),
+ (@{const_name If}, "If"),
+ (@{const_name Set.member}, "member"),
+ (@{const_name Meson.COMBI}, "COMBI"),
+ (@{const_name Meson.COMBK}, "COMBK"),
+ (@{const_name Meson.COMBB}, "COMBB"),
+ (@{const_name Meson.COMBC}, "COMBC"),
+ (@{const_name Meson.COMBS}, "COMBS")]
+ |> Symtab.make
+ |> fold (Symtab.update o swap o snd o snd o snd) proxies
+
+(* Invert the table of translations between Isabelle and ATPs. *)
+val const_trans_table_inv =
+ const_trans_table |> Symtab.dest |> map swap |> Symtab.make
+val const_trans_table_unprox =
+ Symtab.empty
+ |> fold (fn (_, (isa, (_, (_, metis)))) => Symtab.update (metis, isa)) proxies
+
+val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
+val unproxify_const = perhaps (Symtab.lookup const_trans_table_unprox)
+
+fun lookup_const c =
+ case Symtab.lookup const_trans_table c of
+ SOME c' => c'
+ | NONE => ascii_of c
+
+(*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 raise Fail ("trim_type: Malformed type variable encountered: " ^ s)
+
+fun ascii_of_indexname (v,0) = ascii_of v
+ | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ string_of_int 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))
+
+(* 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
+
+(** Definitions and functions for FOL clauses and formulas for TPTP **)
+
+(* 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
+
+
+(** Isabelle arities **)
+
+datatype arity_literal =
+ TConsLit of name * name * name list |
+ TVarLit of name * name
+
+fun gen_TVars 0 = []
+ | gen_TVars n = ("T_" ^ string_of_int 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, `I tvar) :: pack_sort (tvar, srt)
+
+datatype arity_clause =
+ ArityClause of
+ {name: string,
+ prem_lits: arity_literal list,
+ concl_lits: arity_literal}
+
+(* 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,
+ prem_lits = map TVarLit (union_all (map pack_sort tvars_srts)),
+ concl_lits = TConsLit (`make_type_class cls,
+ `make_fixed_type_const tcons,
+ tvars ~~ tvars)}
+ end
+
+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 ^ "_" ^ string_of_int 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 =
+ iter_type_class_pairs thy tycons ##> multi_arity_clause
+
+
+(** 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);
+
+datatype combterm =
+ CombConst of name * typ * typ list |
+ CombVar of name * typ |
+ CombApp of combterm * combterm
+
+fun combtyp_of (CombConst (_, T, _)) = T
+ | combtyp_of (CombVar (_, T)) = T
+ | combtyp_of (CombApp (t1, _)) = snd (dest_funT (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 atyps_of T = fold_atyps (insert (op =)) T []
+
+fun new_skolem_const_name s num_T_args =
+ [new_skolem_const_prefix, s, string_of_int num_T_args]
+ |> space_implode Long_Name.separator
+
+(* Converts a term (with combinators) into a combterm. Also accumulates sort
+ infomation. *)
+fun combterm_from_term thy bs (P $ Q) =
+ let
+ val (P', P_atomics_Ts) = combterm_from_term thy bs P
+ val (Q', Q_atomics_Ts) = combterm_from_term thy bs Q
+ in (CombApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
+ | combterm_from_term thy _ (Const (c, T)) =
+ let
+ 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)
+ val c' = CombConst (`make_fixed_const c, T, tvar_list)
+ in (c', atyps_of T) end
+ | combterm_from_term _ _ (Free (v, T)) =
+ (CombConst (`make_fixed_var v, T, []), atyps_of T)
+ | combterm_from_term _ _ (Var (v as (s, _), T)) =
+ (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
+ let
+ val Ts = T |> strip_type |> swap |> op ::
+ val s' = new_skolem_const_name s (length Ts)
+ in CombConst (`make_fixed_const s', T, Ts) end
+ else
+ CombVar ((make_schematic_var v, s), T), atyps_of T)
+ | combterm_from_term _ bs (Bound j) =
+ nth bs j
+ |> (fn (s, T) => (CombConst (`make_bound_var s, T, []), atyps_of T))
+ | combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs"
+
+datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained
+
+(* (quasi-)underapproximation of the truth *)
+fun is_locality_global Local = false
+ | is_locality_global Assum = false
+ | is_locality_global Chained = false
+ | is_locality_global _ = true
+
+datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
+datatype type_level =
+ All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
+datatype type_heaviness = Heavy | Light
+
+datatype type_system =
+ Simple_Types of type_level |
+ Preds of polymorphism * type_level * type_heaviness |
+ Tags of polymorphism * type_level * type_heaviness
+
+fun try_unsuffixes ss s =
+ fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
+
+fun type_sys_from_string s =
+ (case try (unprefix "poly_") s of
+ SOME s => (SOME Polymorphic, s)
+ | NONE =>
+ case try (unprefix "mono_") s of
+ SOME s => (SOME Monomorphic, s)
+ | NONE =>
+ case try (unprefix "mangled_") s of
+ SOME s => (SOME Mangled_Monomorphic, s)
+ | NONE => (NONE, s))
+ ||> (fn s =>
+ (* "_query" and "_bang" are for the ASCII-challenged Mirabelle. *)
+ case try_unsuffixes ["?", "_query"] s of
+ SOME s => (Nonmonotonic_Types, s)
+ | NONE =>
+ case try_unsuffixes ["!", "_bang"] s of
+ SOME s => (Finite_Types, s)
+ | NONE => (All_Types, s))
+ ||> apsnd (fn s =>
+ case try (unsuffix "_heavy") s of
+ SOME s => (Heavy, s)
+ | NONE => (Light, s))
+ |> (fn (poly, (level, (heaviness, core))) =>
+ case (core, (poly, level, heaviness)) of
+ ("simple", (NONE, _, Light)) => Simple_Types level
+ | ("preds", (SOME poly, _, _)) => Preds (poly, level, heaviness)
+ | ("tags", (SOME Polymorphic, All_Types, _)) =>
+ Tags (Polymorphic, All_Types, heaviness)
+ | ("tags", (SOME Polymorphic, _, _)) =>
+ (* The actual light encoding is very unsound. *)
+ Tags (Polymorphic, level, Heavy)
+ | ("tags", (SOME poly, _, _)) => Tags (poly, level, heaviness)
+ | ("args", (SOME poly, All_Types (* naja *), Light)) =>
+ Preds (poly, Const_Arg_Types, Light)
+ | ("erased", (NONE, All_Types (* naja *), Light)) =>
+ Preds (Polymorphic, No_Types, Light)
+ | _ => raise Same.SAME)
+ handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")
+
+fun polymorphism_of_type_sys (Simple_Types _) = Mangled_Monomorphic
+ | polymorphism_of_type_sys (Preds (poly, _, _)) = poly
+ | polymorphism_of_type_sys (Tags (poly, _, _)) = poly
+
+fun level_of_type_sys (Simple_Types level) = level
+ | level_of_type_sys (Preds (_, level, _)) = level
+ | level_of_type_sys (Tags (_, level, _)) = level
+
+fun heaviness_of_type_sys (Simple_Types _) = Heavy
+ | heaviness_of_type_sys (Preds (_, _, heaviness)) = heaviness
+ | heaviness_of_type_sys (Tags (_, _, heaviness)) = heaviness
+
+fun is_type_level_virtually_sound level =
+ level = All_Types orelse level = Nonmonotonic_Types
+val is_type_sys_virtually_sound =
+ is_type_level_virtually_sound o level_of_type_sys
+
+fun is_type_level_fairly_sound level =
+ is_type_level_virtually_sound level orelse level = Finite_Types
+val is_type_sys_fairly_sound = is_type_level_fairly_sound o level_of_type_sys
+
+fun is_setting_higher_order THF (Simple_Types _) = true
+ | is_setting_higher_order _ _ = false
+
+type translated_formula =
+ {name: string,
+ locality: locality,
+ kind: formula_kind,
+ combformula: (name, typ, combterm) formula,
+ atomic_types: typ list}
+
+fun update_combformula f ({name, locality, kind, combformula, atomic_types}
+ : translated_formula) =
+ {name = name, locality = locality, kind = kind, combformula = f combformula,
+ atomic_types = atomic_types} : translated_formula
+
+fun fact_lift f ({combformula, ...} : translated_formula) = f combformula
+
+val type_instance = Sign.typ_instance o Proof_Context.theory_of
+
+fun insert_type ctxt get_T x xs =
+ let val T = get_T x in
+ if exists (curry (type_instance ctxt) T o get_T) xs then xs
+ else x :: filter_out (curry (type_instance ctxt o swap) T o get_T) xs
+ end
+
+(* The Booleans indicate whether all type arguments should be kept. *)
+datatype type_arg_policy =
+ Explicit_Type_Args of bool |
+ Mangled_Type_Args of bool |
+ No_Type_Args
+
+fun should_drop_arg_type_args (Simple_Types _) =
+ false (* since TFF doesn't support overloading *)
+ | should_drop_arg_type_args type_sys =
+ level_of_type_sys type_sys = All_Types andalso
+ heaviness_of_type_sys type_sys = Heavy
+
+fun general_type_arg_policy type_sys =
+ if level_of_type_sys type_sys = No_Types then
+ No_Type_Args
+ else if polymorphism_of_type_sys type_sys = Mangled_Monomorphic then
+ Mangled_Type_Args (should_drop_arg_type_args type_sys)
+ else
+ Explicit_Type_Args (should_drop_arg_type_args type_sys)
+
+fun type_arg_policy type_sys s =
+ if s = @{const_name HOL.eq} orelse
+ (s = app_op_name andalso level_of_type_sys type_sys = Const_Arg_Types) then
+ No_Type_Args
+ else
+ general_type_arg_policy type_sys
+
+(*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 = the_single @{sort 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)
+ | sorts_on_typs _ = raise Fail "expected \"TVar\" or \"TFree\""
+
+(*Given a list of sorted type variables, return a list of type literals.*)
+val raw_type_literals_for_types = union_all o map sorts_on_typs
+
+fun type_literals_for_types format type_sys kind Ts =
+ if level_of_type_sys type_sys = No_Types orelse format = CNF_UEQ then
+ []
+ else
+ Ts |> raw_type_literals_for_types
+ |> filter (fn TyLitVar _ => kind <> Conjecture
+ | TyLitFree _ => kind = Conjecture)
+
+fun mk_aconns c phis =
+ let val (phis', phi') = split_last phis in
+ fold_rev (mk_aconn c) phis' phi'
+ end
+fun mk_ahorn [] phi = phi
+ | mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi])
+fun mk_aquant _ [] phi = phi
+ | mk_aquant q xs (phi as AQuant (q', xs', phi')) =
+ if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi)
+ | mk_aquant q xs phi = AQuant (q, xs, phi)
+
+fun close_universally atom_vars phi =
+ let
+ fun formula_vars bounds (AQuant (_, xs, phi)) =
+ formula_vars (map fst xs @ bounds) phi
+ | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
+ | formula_vars bounds (AAtom tm) =
+ union (op =) (atom_vars tm []
+ |> filter_out (member (op =) bounds o fst))
+ in mk_aquant AForall (formula_vars [] phi []) phi end
+
+fun combterm_vars (CombApp (tm1, tm2)) = fold combterm_vars [tm1, tm2]
+ | combterm_vars (CombConst _) = I
+ | combterm_vars (CombVar (name, T)) = insert (op =) (name, SOME T)
+fun close_combformula_universally phi = close_universally combterm_vars phi
+
+fun term_vars (ATerm (name as (s, _), tms)) =
+ is_tptp_variable s ? insert (op =) (name, NONE) #> fold term_vars tms
+fun close_formula_universally phi = close_universally term_vars phi
+
+val homo_infinite_type_name = @{type_name ind} (* any infinite type *)
+val homo_infinite_type = Type (homo_infinite_type_name, [])
+
+fun fo_term_from_typ higher_order =
+ let
+ fun term (Type (s, Ts)) =
+ ATerm (case (higher_order, s) of
+ (true, @{type_name bool}) => `I tptp_bool_type
+ | (true, @{type_name fun}) => `I tptp_fun_type
+ | _ => if s = homo_infinite_type_name then `I tptp_individual_type
+ else `make_fixed_type_const s,
+ map term Ts)
+ | term (TFree (s, _)) = ATerm (`make_fixed_type_var s, [])
+ | term (TVar ((x as (s, _)), _)) =
+ ATerm ((make_schematic_type_var x, s), [])
+ in term end
+
+(* This shouldn't clash with anything else. *)
+val mangled_type_sep = "\000"
+
+fun generic_mangled_type_name f (ATerm (name, [])) = f name
+ | generic_mangled_type_name f (ATerm (name, tys)) =
+ f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys)
+ ^ ")"
+
+val bool_atype = AType (`I tptp_bool_type)
+
+fun make_simple_type s =
+ if s = tptp_bool_type orelse s = tptp_fun_type orelse
+ s = tptp_individual_type then
+ s
+ else
+ simple_type_prefix ^ ascii_of s
+
+fun ho_type_from_fo_term higher_order pred_sym ary =
+ let
+ fun to_atype ty =
+ AType ((make_simple_type (generic_mangled_type_name fst ty),
+ generic_mangled_type_name snd ty))
+ fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))
+ fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
+ | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
+ fun to_ho (ty as ATerm ((s, _), tys)) =
+ if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
+ in if higher_order then to_ho else to_fo ary end
+
+fun mangled_type higher_order pred_sym ary =
+ ho_type_from_fo_term higher_order pred_sym ary o fo_term_from_typ higher_order
+
+fun mangled_const_name T_args (s, s') =
+ let
+ val ty_args = map (fo_term_from_typ false) T_args
+ fun type_suffix f g =
+ fold_rev (curry (op ^) o g o prefix mangled_type_sep
+ o generic_mangled_type_name f) ty_args ""
+ in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end
+
+val parse_mangled_ident =
+ Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode
+
+fun parse_mangled_type x =
+ (parse_mangled_ident
+ -- Scan.optional ($$ "(" |-- Scan.optional parse_mangled_types [] --| $$ ")")
+ [] >> ATerm) x
+and parse_mangled_types x =
+ (parse_mangled_type ::: Scan.repeat ($$ "," |-- parse_mangled_type)) x
+
+fun unmangled_type s =
+ s |> suffix ")" |> raw_explode
+ |> Scan.finite Symbol.stopper
+ (Scan.error (!! (fn _ => raise Fail ("unrecognized mangled type " ^
+ quote s)) parse_mangled_type))
+ |> fst
+
+val unmangled_const_name = space_explode mangled_type_sep #> hd
+fun unmangled_const s =
+ let val ss = space_explode mangled_type_sep s in
+ (hd ss, map unmangled_type (tl ss))
+ end
+
+fun introduce_proxies format type_sys =
+ let
+ fun intro top_level (CombApp (tm1, tm2)) =
+ CombApp (intro top_level tm1, intro false tm2)
+ | intro top_level (CombConst (name as (s, _), T, T_args)) =
+ (case proxify_const s of
+ SOME (_, proxy_base) =>
+ if top_level orelse is_setting_higher_order format type_sys then
+ case (top_level, s) of
+ (_, "c_False") => (`I tptp_false, [])
+ | (_, "c_True") => (`I tptp_true, [])
+ | (false, "c_Not") => (`I tptp_not, [])
+ | (false, "c_conj") => (`I tptp_and, [])
+ | (false, "c_disj") => (`I tptp_or, [])
+ | (false, "c_implies") => (`I tptp_implies, [])
+ | (false, s) =>
+ if is_tptp_equal s then (`I tptp_equal, [])
+ else (proxy_base |>> prefix const_prefix, T_args)
+ | _ => (name, [])
+ else
+ (proxy_base |>> prefix const_prefix, T_args)
+ | NONE => (name, T_args))
+ |> (fn (name, T_args) => CombConst (name, T, T_args))
+ | intro _ tm = tm
+ in intro true end
+
+fun combformula_from_prop thy format type_sys eq_as_iff =
+ let
+ fun do_term bs t atomic_types =
+ combterm_from_term thy bs (Envir.eta_contract t)
+ |>> (introduce_proxies format type_sys #> AAtom)
+ ||> union (op =) atomic_types
+ fun do_quant bs q s T t' =
+ let val s = Name.variant (map fst bs) s in
+ do_formula ((s, T) :: bs) t'
+ #>> mk_aquant q [(`make_bound_var s, SOME T)]
+ end
+ and do_conn bs c t1 t2 =
+ do_formula bs t1 ##>> do_formula bs t2
+ #>> uncurry (mk_aconn c)
+ and do_formula bs t =
+ case t of
+ @{const Not} $ t1 => do_formula bs t1 #>> mk_anot
+ | Const (@{const_name All}, _) $ Abs (s, T, t') =>
+ do_quant bs AForall s T t'
+ | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
+ do_quant bs AExists s T t'
+ | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd t1 t2
+ | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2
+ | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2
+ | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
+ if eq_as_iff then do_conn bs AIff t1 t2 else do_term bs t
+ | _ => do_term bs t
+ in do_formula [] end
+
+fun presimplify_term ctxt =
+ Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
+ #> Meson.presimplify ctxt
+ #> prop_of
+
+fun concealed_bound_name j = sledgehammer_weak_prefix ^ string_of_int j
+fun conceal_bounds Ts t =
+ subst_bounds (map (Free o apfst concealed_bound_name)
+ (0 upto length Ts - 1 ~~ Ts), t)
+fun reveal_bounds Ts =
+ subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
+ (0 upto length Ts - 1 ~~ Ts))
+
+fun extensionalize_term ctxt t =
+ let val thy = Proof_Context.theory_of ctxt in
+ t |> cterm_of thy |> Meson.extensionalize_conv ctxt
+ |> prop_of |> Logic.dest_equals |> snd
+ end
+
+fun introduce_combinators_in_term ctxt kind t =
+ let val thy = Proof_Context.theory_of ctxt in
+ if Meson.is_fol_term thy t then
+ t
+ else
+ let
+ fun aux Ts t =
+ case t of
+ @{const Not} $ t1 => @{const Not} $ aux Ts t1
+ | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
+ t0 $ Abs (s, T, aux (T :: Ts) t')
+ | (t0 as Const (@{const_name All}, _)) $ t1 =>
+ aux Ts (t0 $ eta_expand Ts t1 1)
+ | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
+ t0 $ Abs (s, T, aux (T :: Ts) t')
+ | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
+ aux Ts (t0 $ eta_expand Ts t1 1)
+ | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+ | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+ | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+ | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
+ $ t1 $ t2 =>
+ t0 $ aux Ts t1 $ aux Ts t2
+ | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
+ t
+ else
+ t |> conceal_bounds Ts
+ |> Envir.eta_contract
+ |> cterm_of thy
+ |> Meson_Clausify.introduce_combinators_in_cterm
+ |> prop_of |> Logic.dest_equals |> snd
+ |> reveal_bounds Ts
+ val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
+ in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
+ handle THM _ =>
+ (* A type variable of sort "{}" will make abstraction fail. *)
+ if kind = Conjecture then HOLogic.false_const
+ else HOLogic.true_const
+ end
+
+(* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
+ same in Sledgehammer to prevent the discovery of unreplayable proofs. *)
+fun freeze_term t =
+ let
+ fun aux (t $ u) = aux t $ aux u
+ | aux (Abs (s, T, t)) = Abs (s, T, aux t)
+ | aux (Var ((s, i), T)) =
+ Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
+ | aux t = t
+ in t |> exists_subterm is_Var t ? aux end
+
+(* making fact and conjecture formulas *)
+fun make_formula ctxt format type_sys eq_as_iff presimp name loc kind t =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val t = t |> Envir.beta_eta_contract
+ |> transform_elim_prop
+ |> Object_Logic.atomize_term thy
+ val need_trueprop = (fastype_of t = @{typ bool})
+ val t = t |> need_trueprop ? HOLogic.mk_Trueprop
+ |> Raw_Simplifier.rewrite_term thy
+ (Meson.unfold_set_const_simps ctxt) []
+ |> extensionalize_term ctxt
+ |> presimp ? presimplify_term ctxt
+ |> perhaps (try (HOLogic.dest_Trueprop))
+ |> introduce_combinators_in_term ctxt kind
+ |> kind <> Axiom ? freeze_term
+ val (combformula, atomic_types) =
+ combformula_from_prop thy format type_sys eq_as_iff t []
+ in
+ {name = name, locality = loc, kind = kind, combformula = combformula,
+ atomic_types = atomic_types}
+ end
+
+fun make_fact ctxt format type_sys keep_trivial eq_as_iff presimp
+ ((name, loc), t) =
+ case (keep_trivial,
+ make_formula ctxt format type_sys eq_as_iff presimp name loc Axiom t) of
+ (false, formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...}) =>
+ if s = tptp_true then NONE else SOME formula
+ | (_, formula) => SOME formula
+
+fun make_conjecture ctxt format prem_kind type_sys ts =
+ let val last = length ts - 1 in
+ map2 (fn j => fn t =>
+ let
+ val (kind, maybe_negate) =
+ if j = last then
+ (Conjecture, I)
+ else
+ (prem_kind,
+ if prem_kind = Conjecture then update_combformula mk_anot
+ else I)
+ in
+ t |> make_formula ctxt format type_sys true true
+ (string_of_int j) General kind
+ |> maybe_negate
+ end)
+ (0 upto last) ts
+ end
+
+(** Finite and infinite type inference **)
+
+fun deep_freeze_atyp (TVar (_, S)) = TFree ("v", S)
+ | deep_freeze_atyp T = T
+val deep_freeze_type = map_atyps deep_freeze_atyp
+
+(* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
+ dangerous because their "exhaust" properties can easily lead to unsound ATP
+ proofs. On the other hand, all HOL infinite types can be given the same
+ models in first-order logic (via Löwenheim-Skolem). *)
+
+fun should_encode_type ctxt (nonmono_Ts as _ :: _) _ T =
+ exists (curry (type_instance ctxt) (deep_freeze_type T)) nonmono_Ts
+ | should_encode_type _ _ All_Types _ = true
+ | should_encode_type ctxt _ Finite_Types T = is_type_surely_finite ctxt T
+ | should_encode_type _ _ _ _ = false
+
+fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level, heaviness))
+ should_predicate_on_var T =
+ (heaviness = Heavy orelse should_predicate_on_var ()) andalso
+ should_encode_type ctxt nonmono_Ts level T
+ | should_predicate_on_type _ _ _ _ _ = false
+
+fun is_var_or_bound_var (CombConst ((s, _), _, _)) =
+ String.isPrefix bound_var_prefix s
+ | is_var_or_bound_var (CombVar _) = true
+ | is_var_or_bound_var _ = false
+
+datatype tag_site = Top_Level | Eq_Arg | Elsewhere
+
+fun should_tag_with_type _ _ _ Top_Level _ _ = false
+ | should_tag_with_type ctxt nonmono_Ts (Tags (_, level, heaviness)) site u T =
+ (case heaviness of
+ Heavy => should_encode_type ctxt nonmono_Ts level T
+ | Light =>
+ case (site, is_var_or_bound_var u) of
+ (Eq_Arg, true) => should_encode_type ctxt nonmono_Ts level T
+ | _ => false)
+ | should_tag_with_type _ _ _ _ _ _ = false
+
+fun homogenized_type ctxt nonmono_Ts level =
+ let
+ val should_encode = should_encode_type ctxt nonmono_Ts level
+ fun homo 0 T = if should_encode T then T else homo_infinite_type
+ | homo ary (Type (@{type_name fun}, [T1, T2])) =
+ homo 0 T1 --> homo (ary - 1) T2
+ | homo _ _ = raise Fail "expected function type"
+ in homo end
+
+(** "hBOOL" and "hAPP" **)
+
+type sym_info =
+ {pred_sym : bool, min_ary : int, max_ary : int, types : typ list}
+
+fun add_combterm_syms_to_table ctxt explicit_apply =
+ let
+ fun consider_var_arity const_T var_T max_ary =
+ let
+ fun iter ary T =
+ if ary = max_ary orelse type_instance ctxt (var_T, T) then ary
+ else iter (ary + 1) (range_type T)
+ in iter 0 const_T end
+ fun add top_level tm (accum as (ho_var_Ts, sym_tab)) =
+ let val (head, args) = strip_combterm_comb tm in
+ (case head of
+ CombConst ((s, _), T, _) =>
+ if String.isPrefix bound_var_prefix s then
+ if explicit_apply = NONE andalso can dest_funT T then
+ let
+ fun repair_min_arity {pred_sym, min_ary, max_ary, types} =
+ {pred_sym = pred_sym,
+ min_ary =
+ fold (fn T' => consider_var_arity T' T) types min_ary,
+ max_ary = max_ary, types = types}
+ val ho_var_Ts' = ho_var_Ts |> insert_type ctxt I T
+ in
+ if pointer_eq (ho_var_Ts', ho_var_Ts) then accum
+ else (ho_var_Ts', Symtab.map (K repair_min_arity) sym_tab)
+ end
+ else
+ accum
+ else
+ let
+ val ary = length args
+ in
+ (ho_var_Ts,
+ case Symtab.lookup sym_tab s of
+ SOME {pred_sym, min_ary, max_ary, types} =>
+ let
+ val types' = types |> insert_type ctxt I T
+ val min_ary =
+ if is_some explicit_apply orelse
+ pointer_eq (types', types) then
+ min_ary
+ else
+ fold (consider_var_arity T) ho_var_Ts min_ary
+ in
+ Symtab.update (s, {pred_sym = pred_sym andalso top_level,
+ min_ary = Int.min (ary, min_ary),
+ max_ary = Int.max (ary, max_ary),
+ types = types'})
+ sym_tab
+ end
+ | NONE =>
+ let
+ val min_ary =
+ case explicit_apply of
+ SOME true => 0
+ | SOME false => ary
+ | NONE => fold (consider_var_arity T) ho_var_Ts ary
+ in
+ Symtab.update_new (s, {pred_sym = top_level,
+ min_ary = min_ary, max_ary = ary,
+ types = [T]})
+ sym_tab
+ end)
+ end
+ | _ => accum)
+ |> fold (add false) args
+ end
+ in add true end
+fun add_fact_syms_to_table ctxt explicit_apply =
+ fact_lift (formula_fold NONE
+ (K (add_combterm_syms_to_table ctxt explicit_apply)))
+
+val default_sym_table_entries : (string * sym_info) list =
+ [(tptp_equal, {pred_sym = true, min_ary = 2, max_ary = 2, types = []}),
+ (tptp_old_equal, {pred_sym = true, min_ary = 2, max_ary = 2, types = []}),
+ (make_fixed_const predicator_name,
+ {pred_sym = true, min_ary = 1, max_ary = 1, types = []})] @
+ ([tptp_false, tptp_true]
+ |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []}))
+
+fun sym_table_for_facts ctxt explicit_apply facts =
+ Symtab.empty
+ |> fold Symtab.default default_sym_table_entries
+ |> pair [] |> fold (add_fact_syms_to_table ctxt explicit_apply) facts |> snd
+
+fun min_arity_of sym_tab s =
+ case Symtab.lookup sym_tab s of
+ SOME ({min_ary, ...} : sym_info) => min_ary
+ | NONE =>
+ case strip_prefix_and_unascii const_prefix s of
+ SOME s =>
+ let val s = s |> unmangled_const_name |> invert_const in
+ if s = predicator_name then 1
+ else if s = app_op_name then 2
+ else if s = type_pred_name then 1
+ else 0
+ end
+ | NONE => 0
+
+(* True if the constant ever appears outside of the top-level position in
+ literals, or if it appears with different arities (e.g., because of different
+ type instantiations). If false, the constant always receives all of its
+ arguments and is used as a predicate. *)
+fun is_pred_sym sym_tab s =
+ case Symtab.lookup sym_tab s of
+ SOME ({pred_sym, min_ary, max_ary, ...} : sym_info) =>
+ pred_sym andalso min_ary = max_ary
+ | NONE => false
+
+val predicator_combconst =
+ CombConst (`make_fixed_const predicator_name, @{typ "bool => bool"}, [])
+fun predicator tm = CombApp (predicator_combconst, tm)
+
+fun introduce_predicators_in_combterm sym_tab tm =
+ case strip_combterm_comb tm of
+ (CombConst ((s, _), _, _), _) =>
+ if is_pred_sym sym_tab s then tm else predicator tm
+ | _ => predicator tm
+
+fun list_app head args = fold (curry (CombApp o swap)) args head
+
+fun explicit_app arg head =
+ let
+ val head_T = combtyp_of head
+ val (arg_T, res_T) = dest_funT head_T
+ val explicit_app =
+ CombConst (`make_fixed_const app_op_name, head_T --> head_T,
+ [arg_T, res_T])
+ in list_app explicit_app [head, arg] end
+fun list_explicit_app head args = fold explicit_app args head
+
+fun introduce_explicit_apps_in_combterm sym_tab =
+ let
+ fun aux tm =
+ case strip_combterm_comb tm of
+ (head as CombConst ((s, _), _, _), args) =>
+ args |> map aux
+ |> chop (min_arity_of sym_tab s)
+ |>> list_app head
+ |-> list_explicit_app
+ | (head, args) => list_explicit_app head (map aux args)
+ in aux end
+
+fun chop_fun 0 T = ([], T)
+ | chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) =
+ chop_fun (n - 1) ran_T |>> cons dom_T
+ | chop_fun _ _ = raise Fail "unexpected non-function"
+
+fun filter_type_args _ _ _ [] = []
+ | filter_type_args thy s arity T_args =
+ let
+ (* will throw "TYPE" for pseudo-constants *)
+ val U = if s = app_op_name then
+ @{typ "('a => 'b) => 'a => 'b"} |> Logic.varifyT_global
+ else
+ s |> Sign.the_const_type thy
+ in
+ case Term.add_tvarsT (U |> chop_fun arity |> snd) [] of
+ [] => []
+ | res_U_vars =>
+ let val U_args = (s, U) |> Sign.const_typargs thy in
+ U_args ~~ T_args
+ |> map_filter (fn (U, T) =>
+ if member (op =) res_U_vars (dest_TVar U) then
+ SOME T
+ else
+ NONE)
+ end
+ end
+ handle TYPE _ => T_args
+
+fun enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ fun aux arity (CombApp (tm1, tm2)) =
+ CombApp (aux (arity + 1) tm1, aux 0 tm2)
+ | aux arity (CombConst (name as (s, _), T, T_args)) =
+ let
+ val level = level_of_type_sys type_sys
+ val (T, T_args) =
+ (* Aggressively merge most "hAPPs" if the type system is unsound
+ anyway, by distinguishing overloads only on the homogenized
+ result type. Don't do it for lightweight type systems, though,
+ since it leads to too many unsound proofs. *)
+ if s = const_prefix ^ app_op_name andalso
+ length T_args = 2 andalso
+ not (is_type_sys_virtually_sound type_sys) andalso
+ heaviness_of_type_sys type_sys = Heavy then
+ T_args |> map (homogenized_type ctxt nonmono_Ts level 0)
+ |> (fn Ts => let val T = hd Ts --> nth Ts 1 in
+ (T --> T, tl Ts)
+ end)
+ else
+ (T, T_args)
+ in
+ (case strip_prefix_and_unascii const_prefix s of
+ NONE => (name, T_args)
+ | SOME s'' =>
+ let
+ val s'' = invert_const s''
+ fun filtered_T_args false = T_args
+ | filtered_T_args true = filter_type_args thy s'' arity T_args
+ in
+ case type_arg_policy type_sys s'' of
+ Explicit_Type_Args drop_args =>
+ (name, filtered_T_args drop_args)
+ | Mangled_Type_Args drop_args =>
+ (mangled_const_name (filtered_T_args drop_args) name, [])
+ | No_Type_Args => (name, [])
+ end)
+ |> (fn (name, T_args) => CombConst (name, T, T_args))
+ end
+ | aux _ tm = tm
+ in aux 0 end
+
+fun repair_combterm ctxt format nonmono_Ts type_sys sym_tab =
+ not (is_setting_higher_order format type_sys)
+ ? (introduce_explicit_apps_in_combterm sym_tab
+ #> introduce_predicators_in_combterm sym_tab)
+ #> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys
+fun repair_fact ctxt format nonmono_Ts type_sys sym_tab =
+ update_combformula (formula_map
+ (repair_combterm ctxt format nonmono_Ts type_sys sym_tab))
+
+(** Helper facts **)
+
+(* The Boolean indicates that a fairly sound type encoding is needed. *)
+val helper_table =
+ [("COMBI", (false, @{thms Meson.COMBI_def})),
+ ("COMBK", (false, @{thms Meson.COMBK_def})),
+ ("COMBB", (false, @{thms Meson.COMBB_def})),
+ ("COMBC", (false, @{thms Meson.COMBC_def})),
+ ("COMBS", (false, @{thms Meson.COMBS_def})),
+ ("fequal",
+ (* This is a lie: Higher-order equality doesn't need a sound type encoding.
+ However, this is done so for backward compatibility: Including the
+ equality helpers by default in Metis breaks a few existing proofs. *)
+ (true, @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]
+ fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]})),
+ ("fFalse", (true, @{thms True_or_False})),
+ ("fFalse", (false, [@{lemma "~ fFalse" by (unfold fFalse_def) fast}])),
+ ("fTrue", (true, @{thms True_or_False})),
+ ("fTrue", (false, [@{lemma "fTrue" by (unfold fTrue_def) fast}])),
+ ("fNot",
+ (false, @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]
+ fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]})),
+ ("fconj",
+ (false,
+ @{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q"
+ by (unfold fconj_def) fast+})),
+ ("fdisj",
+ (false,
+ @{lemma "~ P | fdisj P Q" "~ Q | fdisj P Q" "~ fdisj P Q | P | Q"
+ by (unfold fdisj_def) fast+})),
+ ("fimplies",
+ (false, @{lemma "P | fimplies P Q" "~ Q | fimplies P Q"
+ "~ fimplies P Q | ~ P | Q"
+ by (unfold fimplies_def) fast+})),
+ ("If", (true, @{thms if_True if_False True_or_False}))]
+
+fun ti_ti_helper_fact () =
+ let
+ fun var s = ATerm (`I s, [])
+ fun tag tm = ATerm (`make_fixed_const type_tag_name, [var "X", tm])
+ in
+ Formula (helper_prefix ^ "ti_ti", Axiom,
+ AAtom (ATerm (`I tptp_equal, [tag (tag (var "Y")), tag (var "Y")]))
+ |> close_formula_universally, simp_info, NONE)
+ end
+
+fun helper_facts_for_sym ctxt format type_sys (s, {types, ...} : sym_info) =
+ case strip_prefix_and_unascii const_prefix s of
+ SOME mangled_s =>
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val unmangled_s = mangled_s |> unmangled_const_name
+ fun dub_and_inst c needs_fairly_sound (th, j) =
+ ((c ^ "_" ^ string_of_int j ^
+ (if needs_fairly_sound then typed_helper_suffix
+ else untyped_helper_suffix),
+ General),
+ let val t = th |> prop_of in
+ t |> ((case general_type_arg_policy type_sys of
+ Mangled_Type_Args _ => true
+ | _ => false) andalso
+ not (null (Term.hidden_polymorphism t)))
+ ? (case types of
+ [T] => specialize_type thy (invert_const unmangled_s, T)
+ | _ => I)
+ end)
+ fun make_facts eq_as_iff =
+ map_filter (make_fact ctxt format type_sys false eq_as_iff false)
+ val fairly_sound = is_type_sys_fairly_sound type_sys
+ in
+ helper_table
+ |> maps (fn (metis_s, (needs_fairly_sound, ths)) =>
+ if metis_s <> unmangled_s orelse
+ (needs_fairly_sound andalso not fairly_sound) then
+ []
+ else
+ ths ~~ (1 upto length ths)
+ |> map (dub_and_inst mangled_s needs_fairly_sound)
+ |> make_facts (not needs_fairly_sound))
+ end
+ | NONE => []
+fun helper_facts_for_sym_table ctxt format type_sys sym_tab =
+ Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_sys) sym_tab
+ []
+
+fun translate_atp_fact ctxt format type_sys keep_trivial =
+ `(make_fact ctxt format type_sys keep_trivial true true o apsnd prop_of)
+
+(***************************************************************)
+(* 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 (FIXME: similar code elsewhere) *)
+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 (@{const_name Meson.skolem}, _) $ _) = I
+ | aux (t $ u) = aux t #> aux u
+ | aux (Const x) =
+ fold (fold_type_consts set_insert) (Sign.const_typargs thy x)
+ | aux (Abs (_, _, u)) = 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);
+
+
+fun translate_formulas ctxt format prem_kind type_sys hyp_ts concl_t
+ rich_facts =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val fact_ts = map (prop_of o snd o snd) rich_facts
+ val (facts, fact_names) =
+ rich_facts
+ |> map_filter (fn (NONE, _) => NONE
+ | (SOME fact, (name, _)) => SOME (fact, name))
+ |> ListPair.unzip
+ (* Remove existing facts from the conjecture, as this can dramatically
+ boost an ATP's performance (for some reason). *)
+ val hyp_ts = hyp_ts |> filter_out (member (op aconv) fact_ts)
+ val goal_t = Logic.list_implies (hyp_ts, concl_t)
+ val all_ts = goal_t :: fact_ts
+ val subs = tfree_classes_of_terms all_ts
+ val supers = tvar_classes_of_terms all_ts
+ val tycons = type_consts_of_terms thy all_ts
+ val conjs =
+ hyp_ts @ [concl_t] |> make_conjecture ctxt format prem_kind type_sys
+ val (supers', arity_clauses) =
+ if level_of_type_sys type_sys = No_Types then ([], [])
+ else make_arity_clauses thy tycons supers
+ val class_rel_clauses = make_class_rel_clauses thy subs supers'
+ in
+ (fact_names |> map single, (conjs, facts, class_rel_clauses, arity_clauses))
+ end
+
+fun fo_literal_from_type_literal (TyLitVar (class, name)) =
+ (true, ATerm (class, [ATerm (name, [])]))
+ | fo_literal_from_type_literal (TyLitFree (class, name)) =
+ (true, ATerm (class, [ATerm (name, [])]))
+
+fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
+
+fun type_pred_combterm ctxt nonmono_Ts type_sys T tm =
+ CombApp (CombConst (`make_fixed_const type_pred_name, T --> @{typ bool}, [T])
+ |> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys,
+ tm)
+
+fun var_occurs_positively_naked_in_term _ (SOME false) _ accum = accum
+ | var_occurs_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
+ accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, [])))
+fun is_var_nonmonotonic_in_formula _ _ (SOME false) _ = false
+ | is_var_nonmonotonic_in_formula pos phi _ name =
+ formula_fold pos (var_occurs_positively_naked_in_term name) phi false
+
+fun mk_const_aterm x T_args args =
+ ATerm (x, map (fo_term_from_typ false) T_args @ args)
+
+fun tag_with_type ctxt format nonmono_Ts type_sys T tm =
+ CombConst (`make_fixed_const type_tag_name, T --> T, [T])
+ |> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys
+ |> term_from_combterm ctxt format nonmono_Ts type_sys Top_Level
+ |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm]))
+and term_from_combterm ctxt format nonmono_Ts type_sys =
+ let
+ fun aux site u =
+ let
+ val (head, args) = strip_combterm_comb u
+ val (x as (s, _), T_args) =
+ case head of
+ CombConst (name, _, T_args) => (name, T_args)
+ | CombVar (name, _) => (name, [])
+ | CombApp _ => raise Fail "impossible \"CombApp\""
+ val arg_site = if site = Top_Level andalso is_tptp_equal s then Eq_Arg
+ else Elsewhere
+ val t = mk_const_aterm x T_args (map (aux arg_site) args)
+ val T = combtyp_of u
+ in
+ t |> (if should_tag_with_type ctxt nonmono_Ts type_sys site u T then
+ tag_with_type ctxt format nonmono_Ts type_sys T
+ else
+ I)
+ end
+ in aux end
+and formula_from_combformula ctxt format nonmono_Ts type_sys
+ should_predicate_on_var =
+ let
+ val higher_order = is_setting_higher_order format type_sys
+ val do_term = term_from_combterm ctxt format nonmono_Ts type_sys Top_Level
+ val do_bound_type =
+ case type_sys of
+ Simple_Types level =>
+ homogenized_type ctxt nonmono_Ts level 0
+ #> mangled_type higher_order false 0 #> SOME
+ | _ => K NONE
+ fun do_out_of_bound_type pos phi universal (name, T) =
+ if should_predicate_on_type ctxt nonmono_Ts type_sys
+ (fn () => should_predicate_on_var pos phi universal name) T then
+ CombVar (name, T)
+ |> type_pred_combterm ctxt nonmono_Ts type_sys T
+ |> do_term |> AAtom |> SOME
+ else
+ NONE
+ fun do_formula pos (AQuant (q, xs, phi)) =
+ let
+ val phi = phi |> do_formula pos
+ val universal = Option.map (q = AExists ? not) pos
+ in
+ AQuant (q, xs |> map (apsnd (fn NONE => NONE
+ | SOME T => do_bound_type T)),
+ (if q = AForall then mk_ahorn else fold_rev (mk_aconn AAnd))
+ (map_filter
+ (fn (_, NONE) => NONE
+ | (s, SOME T) =>
+ do_out_of_bound_type pos phi universal (s, T))
+ xs)
+ phi)
+ end
+ | do_formula pos (AConn conn) = aconn_map pos do_formula conn
+ | do_formula _ (AAtom tm) = AAtom (do_term tm)
+ in do_formula o SOME end
+
+fun bound_atomic_types format type_sys Ts =
+ mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal)
+ (type_literals_for_types format type_sys Axiom Ts))
+
+fun formula_for_fact ctxt format nonmono_Ts type_sys
+ ({combformula, atomic_types, ...} : translated_formula) =
+ combformula
+ |> close_combformula_universally
+ |> formula_from_combformula ctxt format nonmono_Ts type_sys
+ is_var_nonmonotonic_in_formula true
+ |> bound_atomic_types format type_sys atomic_types
+ |> close_formula_universally
+
+(* Each fact is given a unique fact number to avoid name clashes (e.g., because
+ of monomorphization). The TPTP explicitly forbids name clashes, and some of
+ the remote provers might care. *)
+fun formula_line_for_fact ctxt format prefix nonmono_Ts type_sys
+ (j, formula as {name, locality, kind, ...}) =
+ Formula (prefix ^ (if polymorphism_of_type_sys type_sys = Polymorphic then ""
+ else string_of_int j ^ "_") ^
+ ascii_of name,
+ kind, formula_for_fact ctxt format nonmono_Ts type_sys formula, NONE,
+ case locality of
+ Intro => intro_info
+ | Elim => elim_info
+ | Simp => simp_info
+ | _ => NONE)
+
+fun formula_line_for_class_rel_clause
+ (ClassRelClause {name, subclass, superclass, ...}) =
+ let val ty_arg = ATerm (`I "T", []) in
+ Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
+ AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
+ AAtom (ATerm (superclass, [ty_arg]))])
+ |> close_formula_universally, intro_info, NONE)
+ end
+
+fun fo_literal_from_arity_literal (TConsLit (c, t, args)) =
+ (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
+ | fo_literal_from_arity_literal (TVarLit (c, sort)) =
+ (false, ATerm (c, [ATerm (sort, [])]))
+
+fun formula_line_for_arity_clause
+ (ArityClause {name, prem_lits, concl_lits, ...}) =
+ Formula (arity_clause_prefix ^ ascii_of name, Axiom,
+ mk_ahorn (map (formula_from_fo_literal o apfst not
+ o fo_literal_from_arity_literal) prem_lits)
+ (formula_from_fo_literal
+ (fo_literal_from_arity_literal concl_lits))
+ |> close_formula_universally, intro_info, NONE)
+
+fun formula_line_for_conjecture ctxt format nonmono_Ts type_sys
+ ({name, kind, combformula, ...} : translated_formula) =
+ Formula (conjecture_prefix ^ name, kind,
+ formula_from_combformula ctxt format nonmono_Ts type_sys
+ is_var_nonmonotonic_in_formula false
+ (close_combformula_universally combformula)
+ |> close_formula_universally, NONE, NONE)
+
+fun free_type_literals format type_sys
+ ({atomic_types, ...} : translated_formula) =
+ atomic_types |> type_literals_for_types format type_sys Conjecture
+ |> map fo_literal_from_type_literal
+
+fun formula_line_for_free_type j lit =
+ Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis,
+ formula_from_fo_literal lit, NONE, NONE)
+fun formula_lines_for_free_types format type_sys facts =
+ let
+ val litss = map (free_type_literals format type_sys) facts
+ val lits = fold (union (op =)) litss []
+ in map2 formula_line_for_free_type (0 upto length lits - 1) lits end
+
+(** Symbol declarations **)
+
+fun should_declare_sym type_sys pred_sym s =
+ is_tptp_user_symbol s andalso not (String.isPrefix bound_var_prefix s) andalso
+ (case type_sys of
+ Simple_Types _ => true
+ | Tags (_, _, Light) => true
+ | _ => not pred_sym)
+
+fun sym_decl_table_for_facts ctxt type_sys repaired_sym_tab (conjs, facts) =
+ let
+ fun add_combterm in_conj tm =
+ let val (head, args) = strip_combterm_comb tm in
+ (case head of
+ CombConst ((s, s'), T, T_args) =>
+ let val pred_sym = is_pred_sym repaired_sym_tab s in
+ if should_declare_sym type_sys pred_sym s then
+ Symtab.map_default (s, [])
+ (insert_type ctxt #3 (s', T_args, T, pred_sym, length args,
+ in_conj))
+ else
+ I
+ end
+ | _ => I)
+ #> fold (add_combterm in_conj) args
+ end
+ fun add_fact in_conj =
+ fact_lift (formula_fold NONE (K (add_combterm in_conj)))
+ in
+ Symtab.empty
+ |> is_type_sys_fairly_sound type_sys
+ ? (fold (add_fact true) conjs #> fold (add_fact false) facts)
+ end
+
+(* These types witness that the type classes they belong to allow infinite
+ models and hence that any types with these type classes is monotonic. *)
+val known_infinite_types =
+ [@{typ nat}, Type ("Int.int", []), @{typ "nat => bool"}]
+
+(* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
+ out with monotonicity" paper presented at CADE 2011. *)
+fun add_combterm_nonmonotonic_types _ _ (SOME false) _ = I
+ | add_combterm_nonmonotonic_types ctxt level _
+ (CombApp (CombApp (CombConst ((s, _), Type (_, [T, _]), _), tm1), tm2)) =
+ (is_tptp_equal s andalso exists is_var_or_bound_var [tm1, tm2] andalso
+ (case level of
+ Nonmonotonic_Types =>
+ not (is_type_surely_infinite ctxt known_infinite_types T)
+ | Finite_Types => is_type_surely_finite ctxt T
+ | _ => true)) ? insert_type ctxt I (deep_freeze_type T)
+ | add_combterm_nonmonotonic_types _ _ _ _ = I
+fun add_fact_nonmonotonic_types ctxt level ({kind, combformula, ...}
+ : translated_formula) =
+ formula_fold (SOME (kind <> Conjecture))
+ (add_combterm_nonmonotonic_types ctxt level) combformula
+fun nonmonotonic_types_for_facts ctxt type_sys facts =
+ let val level = level_of_type_sys type_sys in
+ if level = Nonmonotonic_Types orelse level = Finite_Types then
+ [] |> fold (add_fact_nonmonotonic_types ctxt level) facts
+ (* We must add "bool" in case the helper "True_or_False" is added
+ later. In addition, several places in the code rely on the list of
+ nonmonotonic types not being empty. *)
+ |> insert_type ctxt I @{typ bool}
+ else
+ []
+ end
+
+fun decl_line_for_sym ctxt format nonmono_Ts type_sys s
+ (s', T_args, T, pred_sym, ary, _) =
+ let
+ val (higher_order, T_arg_Ts, level) =
+ case type_sys of
+ Simple_Types level => (format = THF, [], level)
+ | _ => (false, replicate (length T_args) homo_infinite_type, No_Types)
+ in
+ Decl (sym_decl_prefix ^ s, (s, s'),
+ (T_arg_Ts ---> (T |> homogenized_type ctxt nonmono_Ts level ary))
+ |> mangled_type higher_order pred_sym (length T_arg_Ts + ary))
+ end
+
+fun is_polymorphic_type T = fold_atyps (fn TVar _ => K true | _ => I) T false
+
+fun formula_line_for_pred_sym_decl ctxt format conj_sym_kind nonmono_Ts type_sys
+ n s j (s', T_args, T, _, ary, in_conj) =
+ let
+ val (kind, maybe_negate) =
+ if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
+ else (Axiom, I)
+ val (arg_Ts, res_T) = chop_fun ary T
+ val bound_names =
+ 1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)
+ val bounds =
+ bound_names ~~ arg_Ts |> map (fn (name, T) => CombConst (name, T, []))
+ val bound_Ts =
+ arg_Ts |> map (fn T => if n > 1 orelse is_polymorphic_type T then SOME T
+ else NONE)
+ in
+ Formula (sym_formula_prefix ^ s ^
+ (if n > 1 then "_" ^ string_of_int j else ""), kind,
+ CombConst ((s, s'), T, T_args)
+ |> fold (curry (CombApp o swap)) bounds
+ |> type_pred_combterm ctxt nonmono_Ts type_sys res_T
+ |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
+ |> formula_from_combformula ctxt format nonmono_Ts type_sys
+ (K (K (K (K true)))) true
+ |> n > 1 ? bound_atomic_types format type_sys (atyps_of T)
+ |> close_formula_universally
+ |> maybe_negate,
+ intro_info, NONE)
+ end
+
+fun formula_lines_for_tag_sym_decl ctxt format conj_sym_kind nonmono_Ts type_sys
+ n s (j, (s', T_args, T, pred_sym, ary, in_conj)) =
+ let
+ val ident_base =
+ sym_formula_prefix ^ s ^ (if n > 1 then "_" ^ string_of_int j else "")
+ val (kind, maybe_negate) =
+ if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
+ else (Axiom, I)
+ val (arg_Ts, res_T) = chop_fun ary T
+ val bound_names =
+ 1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)
+ val bounds = bound_names |> map (fn name => ATerm (name, []))
+ val cst = mk_const_aterm (s, s') T_args
+ val atomic_Ts = atyps_of T
+ fun eq tms =
+ (if pred_sym then AConn (AIff, map AAtom tms)
+ else AAtom (ATerm (`I tptp_equal, tms)))
+ |> bound_atomic_types format type_sys atomic_Ts
+ |> close_formula_universally
+ |> maybe_negate
+ val should_encode = should_encode_type ctxt nonmono_Ts All_Types
+ val tag_with = tag_with_type ctxt format nonmono_Ts type_sys
+ val add_formula_for_res =
+ if should_encode res_T then
+ cons (Formula (ident_base ^ "_res", kind,
+ eq [tag_with res_T (cst bounds), cst bounds],
+ simp_info, NONE))
+ else
+ I
+ fun add_formula_for_arg k =
+ let val arg_T = nth arg_Ts k in
+ if should_encode arg_T then
+ case chop k bounds of
+ (bounds1, bound :: bounds2) =>
+ cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), kind,
+ eq [cst (bounds1 @ tag_with arg_T bound :: bounds2),
+ cst bounds],
+ simp_info, NONE))
+ | _ => raise Fail "expected nonempty tail"
+ else
+ I
+ end
+ in
+ [] |> not pred_sym ? add_formula_for_res
+ |> fold add_formula_for_arg (ary - 1 downto 0)
+ end
+
+fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
+
+fun problem_lines_for_sym_decls ctxt format conj_sym_kind nonmono_Ts type_sys
+ (s, decls) =
+ case type_sys of
+ Simple_Types _ =>
+ decls |> map (decl_line_for_sym ctxt format nonmono_Ts type_sys s)
+ | Preds _ =>
+ let
+ val decls =
+ case decls of
+ decl :: (decls' as _ :: _) =>
+ let val T = result_type_of_decl decl in
+ if forall (curry (type_instance ctxt o swap) T
+ o result_type_of_decl) decls' then
+ [decl]
+ else
+ decls
+ end
+ | _ => decls
+ val n = length decls
+ val decls =
+ decls
+ |> filter (should_predicate_on_type ctxt nonmono_Ts type_sys (K true)
+ o result_type_of_decl)
+ in
+ (0 upto length decls - 1, decls)
+ |-> map2 (formula_line_for_pred_sym_decl ctxt format conj_sym_kind
+ nonmono_Ts type_sys n s)
+ end
+ | Tags (_, _, heaviness) =>
+ (case heaviness of
+ Heavy => []
+ | Light =>
+ let val n = length decls in
+ (0 upto n - 1 ~~ decls)
+ |> maps (formula_lines_for_tag_sym_decl ctxt format conj_sym_kind
+ nonmono_Ts type_sys n s)
+ end)
+
+fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts
+ type_sys sym_decl_tab =
+ sym_decl_tab
+ |> Symtab.dest
+ |> sort_wrt fst
+ |> rpair []
+ |-> fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind
+ nonmono_Ts type_sys)
+
+fun should_add_ti_ti_helper (Tags (Polymorphic, level, Heavy)) =
+ level = Nonmonotonic_Types orelse level = Finite_Types
+ | should_add_ti_ti_helper _ = false
+
+fun offset_of_heading_in_problem _ [] j = j
+ | offset_of_heading_in_problem needle ((heading, lines) :: problem) j =
+ if heading = needle then j
+ else offset_of_heading_in_problem needle problem (j + length lines)
+
+val implicit_declsN = "Should-be-implicit typings"
+val explicit_declsN = "Explicit typings"
+val factsN = "Relevant facts"
+val class_relsN = "Class relationships"
+val aritiesN = "Arities"
+val helpersN = "Helper facts"
+val conjsN = "Conjectures"
+val free_typesN = "Type variables"
+
+fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys
+ explicit_apply hyp_ts concl_t facts =
+ let
+ val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
+ translate_formulas ctxt format prem_kind type_sys hyp_ts concl_t facts
+ val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
+ val nonmono_Ts = conjs @ facts |> nonmonotonic_types_for_facts ctxt type_sys
+ val repair = repair_fact ctxt format nonmono_Ts type_sys sym_tab
+ val (conjs, facts) = (conjs, facts) |> pairself (map repair)
+ val repaired_sym_tab =
+ conjs @ facts |> sym_table_for_facts ctxt (SOME false)
+ val helpers =
+ repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_sys
+ |> map repair
+ val lavish_nonmono_Ts =
+ if null nonmono_Ts orelse
+ polymorphism_of_type_sys type_sys <> Polymorphic then
+ nonmono_Ts
+ else
+ [TVar (("'a", 0), HOLogic.typeS)]
+ val sym_decl_lines =
+ (conjs, helpers @ facts)
+ |> sym_decl_table_for_facts ctxt type_sys repaired_sym_tab
+ |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind
+ lavish_nonmono_Ts type_sys
+ val helper_lines =
+ 0 upto length helpers - 1 ~~ helpers
+ |> map (formula_line_for_fact ctxt format helper_prefix lavish_nonmono_Ts
+ type_sys)
+ |> (if should_add_ti_ti_helper type_sys then cons (ti_ti_helper_fact ())
+ else I)
+ (* Reordering these might confuse the proof reconstruction code or the SPASS
+ FLOTTER hack. *)
+ val problem =
+ [(explicit_declsN, sym_decl_lines),
+ (factsN,
+ map (formula_line_for_fact ctxt format fact_prefix nonmono_Ts type_sys)
+ (0 upto length facts - 1 ~~ facts)),
+ (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses),
+ (aritiesN, map formula_line_for_arity_clause arity_clauses),
+ (helpersN, helper_lines),
+ (conjsN,
+ map (formula_line_for_conjecture ctxt format nonmono_Ts type_sys)
+ conjs),
+ (free_typesN,
+ formula_lines_for_free_types format type_sys (facts @ conjs))]
+ val problem =
+ problem
+ |> (if format = CNF_UEQ then filter_cnf_ueq_problem else I)
+ |> (if is_format_typed format then
+ declare_undeclared_syms_in_atp_problem type_decl_prefix
+ implicit_declsN
+ else
+ I)
+ val (problem, pool) =
+ problem |> nice_atp_problem (Config.get ctxt readable_names)
+ val helpers_offset = offset_of_heading_in_problem helpersN problem 0
+ val typed_helpers =
+ map_filter (fn (j, {name, ...}) =>
+ if String.isSuffix typed_helper_suffix name then SOME j
+ else NONE)
+ ((helpers_offset + 1 upto helpers_offset + length helpers)
+ ~~ helpers)
+ fun add_sym_arity (s, {min_ary, ...} : sym_info) =
+ if min_ary > 0 then
+ case strip_prefix_and_unascii const_prefix s of
+ SOME s => Symtab.insert (op =) (s, min_ary)
+ | NONE => I
+ else
+ I
+ in
+ (problem,
+ case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
+ offset_of_heading_in_problem conjsN problem 0,
+ offset_of_heading_in_problem factsN problem 0,
+ fact_names |> Vector.fromList,
+ typed_helpers,
+ Symtab.empty |> Symtab.fold add_sym_arity sym_tab)
+ end
+
+(* FUDGE *)
+val conj_weight = 0.0
+val hyp_weight = 0.1
+val fact_min_weight = 0.2
+val fact_max_weight = 1.0
+val type_info_default_weight = 0.8
+
+fun add_term_weights weight (ATerm (s, tms)) =
+ is_tptp_user_symbol s ? Symtab.default (s, weight)
+ #> fold (add_term_weights weight) tms
+fun add_problem_line_weights weight (Formula (_, _, phi, _, _)) =
+ formula_fold NONE (K (add_term_weights weight)) phi
+ | add_problem_line_weights _ _ = I
+
+fun add_conjectures_weights [] = I
+ | add_conjectures_weights conjs =
+ let val (hyps, conj) = split_last conjs in
+ add_problem_line_weights conj_weight conj
+ #> fold (add_problem_line_weights hyp_weight) hyps
+ end
+
+fun add_facts_weights facts =
+ let
+ val num_facts = length facts
+ fun weight_of j =
+ fact_min_weight + (fact_max_weight - fact_min_weight) * Real.fromInt j
+ / Real.fromInt num_facts
+ in
+ map weight_of (0 upto num_facts - 1) ~~ facts
+ |> fold (uncurry add_problem_line_weights)
+ end
+
+(* Weights are from 0.0 (most important) to 1.0 (least important). *)
+fun atp_problem_weights problem =
+ let val get = these o AList.lookup (op =) problem in
+ Symtab.empty
+ |> add_conjectures_weights (get free_typesN @ get conjsN)
+ |> add_facts_weights (get factsN)
+ |> fold (fold (add_problem_line_weights type_info_default_weight) o get)
+ [explicit_declsN, class_relsN, aritiesN]
+ |> Symtab.dest
+ |> sort (prod_ord Real.compare string_ord o pairself swap)
+ end
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP/atp_util.ML Tue May 31 16:38:36 2011 +0200
@@ -0,0 +1,257 @@
+(* Title: HOL/Tools/ATP/atp_util.ML
+ Author: Jasmin Blanchette, TU Muenchen
+
+General-purpose functions used by the ATP module.
+*)
+
+signature ATP_UTIL =
+sig
+ val timestamp : unit -> string
+ val hashw : word * word -> word
+ val hashw_string : string * word -> word
+ val strip_spaces : bool -> (char -> bool) -> string -> string
+ val nat_subscript : int -> string
+ val unyxml : string -> string
+ val maybe_quote : string -> string
+ val string_from_ext_time : bool * Time.time -> string
+ val string_from_time : Time.time -> string
+ val varify_type : Proof.context -> typ -> typ
+ val instantiate_type : theory -> typ -> typ -> typ -> typ
+ val varify_and_instantiate_type : Proof.context -> typ -> typ -> typ -> typ
+ val typ_of_dtyp :
+ Datatype_Aux.descr -> (Datatype_Aux.dtyp * typ) list -> Datatype_Aux.dtyp
+ -> typ
+ val is_type_surely_finite : Proof.context -> typ -> bool
+ val is_type_surely_infinite : Proof.context -> typ list -> typ -> bool
+ val monomorphic_term : Type.tyenv -> term -> term
+ val eta_expand : typ list -> term -> int -> term
+ val transform_elim_prop : term -> term
+ val specialize_type : theory -> (string * typ) -> term -> term
+ val strip_subgoal :
+ Proof.context -> thm -> int -> (string * typ) list * term list * term
+end;
+
+structure ATP_Util : ATP_UTIL =
+struct
+
+val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now
+
+(* This hash function is recommended in "Compilers: Principles, Techniques, and
+ Tools" by Aho, Sethi, and Ullman. The "hashpjw" function, which they
+ particularly recommend, triggers a bug in versions of Poly/ML up to 4.2.0. *)
+fun hashw (u, w) = Word.+ (u, Word.* (0w65599, w))
+fun hashw_char (c, w) = hashw (Word.fromInt (Char.ord c), w)
+fun hashw_string (s : string, w) = CharVector.foldl hashw_char w s
+
+fun strip_c_style_comment _ [] = []
+ | strip_c_style_comment is_evil (#"*" :: #"/" :: cs) =
+ strip_spaces_in_list true is_evil cs
+ | strip_c_style_comment is_evil (_ :: cs) = strip_c_style_comment is_evil cs
+and strip_spaces_in_list _ _ [] = []
+ | strip_spaces_in_list true is_evil (#"%" :: cs) =
+ strip_spaces_in_list true is_evil
+ (cs |> chop_while (not_equal #"\n") |> snd)
+ | strip_spaces_in_list true is_evil (#"/" :: #"*" :: cs) =
+ strip_c_style_comment is_evil cs
+ | strip_spaces_in_list _ _ [c1] = if Char.isSpace c1 then [] else [str c1]
+ | strip_spaces_in_list skip_comments is_evil [c1, c2] =
+ strip_spaces_in_list skip_comments is_evil [c1] @
+ strip_spaces_in_list skip_comments is_evil [c2]
+ | strip_spaces_in_list skip_comments is_evil (c1 :: c2 :: c3 :: cs) =
+ if Char.isSpace c1 then
+ strip_spaces_in_list skip_comments is_evil (c2 :: c3 :: cs)
+ else if Char.isSpace c2 then
+ if Char.isSpace c3 then
+ strip_spaces_in_list skip_comments is_evil (c1 :: c3 :: cs)
+ else
+ str c1 :: (if forall is_evil [c1, c3] then [" "] else []) @
+ strip_spaces_in_list skip_comments is_evil (c3 :: cs)
+ else
+ str c1 :: strip_spaces_in_list skip_comments is_evil (c2 :: c3 :: cs)
+fun strip_spaces skip_comments is_evil =
+ implode o strip_spaces_in_list skip_comments is_evil o String.explode
+
+val subscript = implode o map (prefix "\<^isub>") o raw_explode (* FIXME Symbol.explode (?) *)
+fun nat_subscript n =
+ n |> string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript
+
+val unyxml = XML.content_of o YXML.parse_body
+
+val is_long_identifier = forall Lexicon.is_identifier o space_explode "."
+fun maybe_quote y =
+ let val s = unyxml y in
+ y |> ((not (is_long_identifier (perhaps (try (unprefix "'")) s)) andalso
+ not (is_long_identifier (perhaps (try (unprefix "?")) s))) orelse
+ Keyword.is_keyword s) ? quote
+ end
+
+fun string_from_ext_time (plus, time) =
+ let val ms = Time.toMilliseconds time in
+ (if plus then "> " else "") ^
+ (if plus andalso ms mod 1000 = 0 then
+ signed_string_of_int (ms div 1000) ^ " s"
+ else if ms < 1000 then
+ signed_string_of_int ms ^ " ms"
+ else
+ string_of_real (0.01 * Real.fromInt (ms div 10)) ^ " s")
+ end
+
+val string_from_time = string_from_ext_time o pair false
+
+fun varify_type ctxt T =
+ Variable.polymorphic_types ctxt [Const (@{const_name undefined}, T)]
+ |> snd |> the_single |> dest_Const |> snd
+
+(* TODO: use "Term_Subst.instantiateT" instead? *)
+fun instantiate_type thy T1 T1' T2 =
+ Same.commit (Envir.subst_type_same
+ (Sign.typ_match thy (T1, T1') Vartab.empty)) T2
+ handle Type.TYPE_MATCH => raise TYPE ("instantiate_type", [T1, T1'], [])
+
+fun varify_and_instantiate_type ctxt T1 T1' T2 =
+ let val thy = Proof_Context.theory_of ctxt in
+ instantiate_type thy (varify_type ctxt T1) T1' (varify_type ctxt T2)
+ end
+
+fun typ_of_dtyp _ typ_assoc (Datatype_Aux.DtTFree a) =
+ the (AList.lookup (op =) typ_assoc (Datatype_Aux.DtTFree a))
+ | typ_of_dtyp descr typ_assoc (Datatype_Aux.DtType (s, Us)) =
+ Type (s, map (typ_of_dtyp descr typ_assoc) Us)
+ | typ_of_dtyp descr typ_assoc (Datatype_Aux.DtRec i) =
+ let val (s, ds, _) = the (AList.lookup (op =) descr i) in
+ Type (s, map (typ_of_dtyp descr typ_assoc) ds)
+ end
+
+fun datatype_constrs thy (T as Type (s, Ts)) =
+ (case Datatype.get_info thy s of
+ SOME {index, descr, ...} =>
+ let val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the in
+ map (apsnd (fn Us => map (typ_of_dtyp descr (dtyps ~~ Ts)) Us ---> T))
+ constrs
+ end
+ | NONE => [])
+ | datatype_constrs _ _ = []
+
+(* Similar to "Nitpick_HOL.bounded_exact_card_of_type".
+ 0 means infinite type, 1 means singleton type (e.g., "unit"), and 2 means
+ cardinality 2 or more. The specified default cardinality is returned if the
+ cardinality of the type can't be determined. *)
+fun tiny_card_of_type ctxt default_card assigns T =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val max = 2 (* 1 would be too small for the "fun" case *)
+ fun aux slack avoid T =
+ if member (op =) avoid T then
+ 0
+ else case AList.lookup (Sign.typ_instance thy o swap) assigns T of
+ SOME k => k
+ | NONE =>
+ case T of
+ Type (@{type_name fun}, [T1, T2]) =>
+ (case (aux slack avoid T1, aux slack avoid T2) of
+ (k, 1) => if slack andalso k = 0 then 0 else 1
+ | (0, _) => 0
+ | (_, 0) => 0
+ | (k1, k2) =>
+ if k1 >= max orelse k2 >= max then max
+ else Int.min (max, Integer.pow k2 k1))
+ | @{typ prop} => 2
+ | @{typ bool} => 2 (* optimization *)
+ | @{typ nat} => 0 (* optimization *)
+ | Type ("Int.int", []) => 0 (* optimization *)
+ | Type (s, _) =>
+ (case datatype_constrs thy T of
+ constrs as _ :: _ =>
+ let
+ val constr_cards =
+ map (Integer.prod o map (aux slack (T :: avoid)) o binder_types
+ o snd) constrs
+ in
+ if exists (curry (op =) 0) constr_cards then 0
+ else Int.min (max, Integer.sum constr_cards)
+ end
+ | [] =>
+ case Typedef.get_info ctxt s of
+ ({abs_type, rep_type, ...}, _) :: _ =>
+ (* We cheat here by assuming that typedef types are infinite if
+ their underlying type is infinite. This is unsound in general
+ but it's hard to think of a realistic example where this would
+ not be the case. We are also slack with representation types:
+ If a representation type has the form "sigma => tau", we
+ consider it enough to check "sigma" for infiniteness. (Look
+ for "slack" in this function.) *)
+ (case varify_and_instantiate_type ctxt
+ (Logic.varifyT_global abs_type) T
+ (Logic.varifyT_global rep_type)
+ |> aux true avoid of
+ 0 => 0
+ | 1 => 1
+ | _ => default_card)
+ | [] => default_card)
+ (* Very slightly unsound: Type variables are assumed not to be
+ constrained to cardinality 1. (In practice, the user would most
+ likely have used "unit" directly anyway.) *)
+ | TFree _ => if default_card = 1 then 2 else default_card
+ (* Schematic type variables that contain only unproblematic sorts
+ (with no finiteness axiom) can safely be considered infinite. *)
+ | TVar _ => default_card
+ in Int.min (max, aux false [] T) end
+
+fun is_type_surely_finite ctxt T = tiny_card_of_type ctxt 0 [] T <> 0
+fun is_type_surely_infinite ctxt infinite_Ts T =
+ tiny_card_of_type ctxt 1 (map (rpair 0) infinite_Ts) T = 0
+
+fun monomorphic_term subst t =
+ map_types (map_type_tvar (fn v =>
+ case Type.lookup subst v of
+ SOME typ => typ
+ | NONE => raise TERM ("monomorphic_term: uninstanitated schematic type \
+ \variable", [t]))) t
+
+fun eta_expand _ t 0 = t
+ | eta_expand Ts (Abs (s, T, t')) n =
+ Abs (s, T, eta_expand (T :: Ts) t' (n - 1))
+ | eta_expand Ts t n =
+ fold_rev (fn T => fn t' => Abs ("x" ^ nat_subscript n, T, t'))
+ (List.take (binder_types (fastype_of1 (Ts, t)), n))
+ (list_comb (incr_boundvars n t, map Bound (n - 1 downto 0)))
+
+(* Converts an elim-rule into an equivalent theorem that does not have the
+ predicate variable. Leaves other theorems unchanged. We simply instantiate
+ the conclusion variable to False. (Cf. "transform_elim_theorem" in
+ "Meson_Clausify".) *)
+fun transform_elim_prop t =
+ case Logic.strip_imp_concl t of
+ @{const Trueprop} $ Var (z, @{typ bool}) =>
+ subst_Vars [(z, @{const False})] t
+ | Var (z, @{typ prop}) => subst_Vars [(z, @{prop False})] t
+ | _ => t
+
+fun specialize_type thy (s, T) t =
+ let
+ fun subst_for (Const (s', T')) =
+ if s = s' then
+ SOME (Sign.typ_match thy (T', T) Vartab.empty)
+ handle Type.TYPE_MATCH => NONE
+ else
+ NONE
+ | subst_for (t1 $ t2) =
+ (case subst_for t1 of SOME x => SOME x | NONE => subst_for t2)
+ | subst_for (Abs (_, _, t')) = subst_for t'
+ | subst_for _ = NONE
+ in
+ case subst_for t of
+ SOME subst => monomorphic_term subst t
+ | NONE => raise Type.TYPE_MATCH
+ end
+
+fun strip_subgoal ctxt goal i =
+ let
+ val (t, (frees, params)) =
+ Logic.goal_params (prop_of goal) i
+ ||> (map dest_Free #> Variable.variant_frees ctxt [] #> `(map Free))
+ val hyp_ts = t |> Logic.strip_assums_hyp |> map (curry subst_bounds frees)
+ val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees
+ in (rev params, hyp_ts, concl_t) end
+
+end;
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Tue May 31 11:21:47 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Tue May 31 16:38:36 2011 +0200
@@ -30,6 +30,7 @@
structure Metis_Reconstruct : METIS_RECONSTRUCT =
struct
+open ATP_Translate
open Metis_Translate
exception METIS of string * string
--- a/src/HOL/Tools/Metis/metis_tactics.ML Tue May 31 11:21:47 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML Tue May 31 16:38:36 2011 +0200
@@ -26,6 +26,7 @@
structure Metis_Tactics : METIS_TACTICS =
struct
+open ATP_Translate
open Metis_Translate
open Metis_Reconstruct
--- a/src/HOL/Tools/Metis/metis_translate.ML Tue May 31 11:21:47 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML Tue May 31 16:38:36 2011 +0200
@@ -9,76 +9,21 @@
signature METIS_TRANSLATE =
sig
- type name = string * string
-
- datatype type_literal =
- TyLitVar of name * name |
- TyLitFree of name * name
- datatype arity_literal =
- TConsLit of name * name * name list |
- TVarLit of name * name
- datatype arity_clause =
- ArityClause of
- {name: string,
- prem_lits: arity_literal list,
- concl_lits: arity_literal}
- datatype class_rel_clause =
- ClassRelClause of {name: string, subclass: name, superclass: name}
- datatype combterm =
- CombConst of name * typ * typ list |
- CombVar of name * typ |
- CombApp of combterm * combterm
- datatype fol_literal = FOLLiteral of bool * combterm
+ type type_literal = ATP_Translate.type_literal
datatype mode = FO | HO | FT
+
type metis_problem =
{axioms: (Metis_Thm.thm * thm) list,
tfrees: type_literal list,
old_skolems: (string * term) list}
val metis_generated_var_prefix : string
- val type_tag_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 proxify_const : string -> (int * (string * string)) option
- val invert_const: string -> string
- val unproxify_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_name_from_const : string -> string
- 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 -> typ
- val strip_combterm_comb : combterm -> combterm * combterm list
- val atyps_of : typ -> typ list
- val combterm_from_term :
- theory -> (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 metis_helpers : (string * (bool * thm list)) list
val prepare_metis_problem :
mode -> Proof.context -> bool -> thm list -> thm list list
-> mode * metis_problem
@@ -87,150 +32,9 @@
structure Metis_Translate : METIS_TRANSLATE =
struct
-val metis_generated_var_prefix = "_"
-
-val type_tag_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 []
-
-val metis_proxies =
- [("c_False",
- (@{const_name False}, (0, ("fFalse", @{const_name Metis.fFalse})))),
- ("c_True", (@{const_name True}, (0, ("fTrue", @{const_name Metis.fTrue})))),
- ("c_Not", (@{const_name Not}, (1, ("fNot", @{const_name Metis.fNot})))),
- ("c_conj", (@{const_name conj}, (2, ("fconj", @{const_name Metis.fconj})))),
- ("c_disj", (@{const_name disj}, (2, ("fdisj", @{const_name Metis.fdisj})))),
- ("c_implies",
- (@{const_name implies}, (2, ("fimplies", @{const_name Metis.fimplies})))),
- ("equal",
- (@{const_name HOL.eq}, (2, ("fequal", @{const_name Metis.fequal}))))]
-
-val proxify_const = AList.lookup (op =) metis_proxies #> Option.map snd
-
-(* Readable names for the more common symbolic functions. Do not mess with the
- table unless you know what you are doing. *)
-val const_trans_table =
- [(@{type_name Product_Type.prod}, "prod"),
- (@{type_name Sum_Type.sum}, "sum"),
- (@{const_name False}, "False"),
- (@{const_name True}, "True"),
- (@{const_name Not}, "Not"),
- (@{const_name conj}, "conj"),
- (@{const_name disj}, "disj"),
- (@{const_name implies}, "implies"),
- (@{const_name HOL.eq}, "equal"),
- (@{const_name If}, "If"),
- (@{const_name Set.member}, "member"),
- (@{const_name Meson.COMBI}, "COMBI"),
- (@{const_name Meson.COMBK}, "COMBK"),
- (@{const_name Meson.COMBB}, "COMBB"),
- (@{const_name Meson.COMBC}, "COMBC"),
- (@{const_name Meson.COMBS}, "COMBS")]
- |> Symtab.make
- |> fold (Symtab.update o swap o snd o snd o snd) metis_proxies
-
-(* Invert the table of translations between Isabelle and Metis. *)
-val const_trans_table_inv =
- const_trans_table |> Symtab.dest |> map swap |> Symtab.make
-val const_trans_table_unprox =
- Symtab.empty
- |> fold (fn (_, (isa, (_, (_, metis)))) => Symtab.update (metis, isa))
- metis_proxies
-
-val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
-val unproxify_const = perhaps (Symtab.lookup const_trans_table_unprox)
+open ATP_Translate
-(*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) ^ string_of_int (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 raise Fail ("trim_type: Malformed type variable encountered: " ^ s)
-
-fun ascii_of_indexname (v,0) = ascii_of v
- | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ string_of_int 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;
+val metis_generated_var_prefix = "_"
(* The number of type arguments of a constant, zero if it's monomorphic. For
(instances of) Skolem pseudoconstants, this information is encoded in the
@@ -246,192 +50,6 @@
nth ss (length ss - 2)
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 = the_single @{sort 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 arity_literal =
- TConsLit of name * name * name list |
- TVarLit of name * name
-
-datatype arity_clause =
- ArityClause of
- {name: string,
- prem_lits: arity_literal list,
- concl_lits: arity_literal}
-
-fun gen_TVars 0 = []
- | gen_TVars n = ("T_" ^ string_of_int 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, `I 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,
- prem_lits = map TVarLit (union_all (map pack_sort tvars_srts)),
- concl_lits = TConsLit (`make_type_class cls,
- `make_fixed_type_const tcons,
- tvars ~~ tvars)}
- 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 ^ "_" ^ string_of_int 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 =
- iter_type_class_pairs thy tycons ##> multi_arity_clause
-
-datatype combterm =
- CombConst of name * typ * typ list (* Const and Free *) |
- CombVar of name * typ |
- CombApp of combterm * combterm
-
-datatype fol_literal = FOLLiteral of bool * combterm
-
-(*********************************************************************)
-(* convert a clause with type Term.term to a clause with type clause *)
-(*********************************************************************)
-
-fun combtyp_of (CombConst (_, T, _)) = T
- | combtyp_of (CombVar (_, T)) = T
- | combtyp_of (CombApp (t1, _)) = snd (dest_funT (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 atyps_of T = fold_atyps (insert (op =)) T []
-
-fun new_skolem_const_name s num_T_args =
- [new_skolem_const_prefix, s, string_of_int num_T_args]
- |> space_implode Long_Name.separator
-
-(* Converts a term (with combinators) into a combterm. Also accumulates sort
- infomation. *)
-fun combterm_from_term thy bs (P $ Q) =
- let
- val (P', P_atomics_Ts) = combterm_from_term thy bs P
- val (Q', Q_atomics_Ts) = combterm_from_term thy bs Q
- in (CombApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
- | combterm_from_term thy _ (Const (c, T)) =
- let
- 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)
- val c' = CombConst (`make_fixed_const c, T, tvar_list)
- in (c', atyps_of T) end
- | combterm_from_term _ _ (Free (v, T)) =
- (CombConst (`make_fixed_var v, T, []), atyps_of T)
- | combterm_from_term _ _ (Var (v as (s, _), T)) =
- (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
- let
- val Ts = T |> strip_type |> swap |> op ::
- val s' = new_skolem_const_name s (length Ts)
- in CombConst (`make_fixed_const s', T, Ts) end
- else
- CombVar ((make_schematic_var v, s), T), atyps_of T)
- | combterm_from_term _ bs (Bound j) =
- nth bs j
- |> (fn (s, T) => (CombConst (`make_bound_var s, T, []), atyps_of T))
- | combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs"
-
fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos)
| predicate_of thy (t, pos) =
(combterm_from_term thy [] (Envir.eta_contract t), pos)
@@ -442,7 +60,7 @@
literals_of_term1 (literals_of_term1 args thy P) thy Q
| literals_of_term1 (lits, ts) thy P =
let val ((pred, ts'), pol) = predicate_of thy (P, true) in
- (FOLLiteral (pol, pred) :: lits, union (op =) ts ts')
+ ((pol, pred) :: lits, union (op =) ts ts')
end
val literals_of_term = literals_of_term1 ([], [])
@@ -491,43 +109,6 @@
| 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 (@{const_name Meson.skolem}, _) $ _) = I
- | aux (t $ u) = aux t #> aux u
- | aux (Const x) =
- fold (fold_type_consts set_insert) (Sign.const_typargs thy x)
- | aux (Abs (_, _, u)) = 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) *)
(* ------------------------------------------------------------------------- *)
@@ -589,18 +170,18 @@
tag_with_type (Metis_Term.Fn (".", map hol_term_to_fol_FT [tm1, tm2]))
(combtyp_of tm)
-fun hol_literal_to_fol FO (FOLLiteral (pos, tm)) =
+fun hol_literal_to_fol FO (pos, tm) =
let
val (CombConst((p, _), _, Ts), tms) = strip_combterm_comb tm
val tylits = if p = "equal" then [] else map metis_term_from_typ Ts
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)) =
+ | hol_literal_to_fol HO (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)) =
+ | hol_literal_to_fol FT (pos, tm) =
(case strip_combterm_comb tm of
(CombConst(("equal", _), _, _), tms) =>
metis_lit pos "=" (map hol_term_to_fol_FT tms)
@@ -634,11 +215,11 @@
in
if is_conjecture then
(Metis_Thm.axiom (Metis_LiteralSet.fromList mlits),
- type_literals_for_types types_sorts, old_skolems)
+ raw_type_literals_for_types types_sorts, old_skolems)
else
let
val tylits = types_sorts |> filter_out (has_default_sort ctxt)
- |> type_literals_for_types
+ |> raw_type_literals_for_types
val mtylits =
if type_lits then map (metis_of_type_literals false) tylits else []
in
@@ -647,40 +228,6 @@
end
end;
-(* The Boolean indicates that a fairly sound type encoding is needed. *)
-val metis_helpers =
- [("COMBI", (false, @{thms Meson.COMBI_def})),
- ("COMBK", (false, @{thms Meson.COMBK_def})),
- ("COMBB", (false, @{thms Meson.COMBB_def})),
- ("COMBC", (false, @{thms Meson.COMBC_def})),
- ("COMBS", (false, @{thms Meson.COMBS_def})),
- ("fequal",
- (* This is a lie: Higher-order equality doesn't need a sound type encoding.
- However, this is done so for backward compatibility: Including the
- equality helpers by default in Metis breaks a few existing proofs. *)
- (true, @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]
- fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]})),
- ("fFalse", (true, @{thms True_or_False})),
- ("fFalse", (false, [@{lemma "~ fFalse" by (unfold fFalse_def) fast}])),
- ("fTrue", (true, @{thms True_or_False})),
- ("fTrue", (false, [@{lemma "fTrue" by (unfold fTrue_def) fast}])),
- ("fNot",
- (false, @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]
- fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]})),
- ("fconj",
- (false,
- @{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q"
- by (unfold fconj_def) fast+})),
- ("fdisj",
- (false,
- @{lemma "~ P | fdisj P Q" "~ Q | fdisj P Q" "~ fdisj P Q | P | Q"
- by (unfold fdisj_def) fast+})),
- ("fimplies",
- (false, @{lemma "P | fimplies P Q" "~ Q | fimplies P Q"
- "~ fimplies P Q | ~ P | Q"
- by (unfold fimplies_def) fast+})),
- ("If", (true, @{thms if_True if_False True_or_False}))]
-
(* ------------------------------------------------------------------------- *)
(* Logic maps manage the interface between HOL and first-order logic. *)
(* ------------------------------------------------------------------------- *)
@@ -697,7 +244,7 @@
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
+ |> raw_type_literals_for_types
end;
(*Insert non-logical axioms corresponding to all accumulated TFrees*)
@@ -785,7 +332,7 @@
#> `(Meson.make_meta_clause
#> rewrite_rule (map safe_mk_meta_eq fdefs))
val helper_ths =
- metis_helpers
+ helper_table
|> filter (is_used o prefix const_prefix o fst)
|> maps (fn (_, (needs_full_types, thms)) =>
if needs_full_types andalso mode <> FT then []
--- a/src/HOL/Tools/Nitpick/kodkod.ML Tue May 31 11:21:47 2011 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Tue May 31 16:38:36 2011 +0200
@@ -860,7 +860,7 @@
out "solve "; out_outmost_f formula; out ";\n")
in
out ("// This file was generated by Isabelle (most likely Nitpick)\n" ^
- "// " ^ ATP_Problem.timestamp () ^ "\n");
+ "// " ^ ATP_Util.timestamp () ^ "\n");
map out_problem problems
end
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue May 31 11:21:47 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue May 31 16:38:36 2011 +0200
@@ -969,7 +969,7 @@
handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
default_card)
-(* Similar to "Sledgehammer_ATP_Translate.tiny_card_of_type". *)
+(* Similar to "ATP_Translate.tiny_card_of_type". *)
fun bounded_exact_card_of_type hol_ctxt finitizable_dataTs max default_card
assigns T =
let
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Tue May 31 11:21:47 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Tue May 31 16:38:36 2011 +0200
@@ -240,7 +240,7 @@
val parse_bool_option = Sledgehammer_Util.parse_bool_option
val parse_time_option = Sledgehammer_Util.parse_time_option
-val string_from_time = Sledgehammer_Util.string_from_time
+val string_from_time = ATP_Util.string_from_time
val i_subscript = implode o map (prefix "\<^isub>") o raw_explode (* FIXME Symbol.explode (?) *)
fun be_subscript s = "\<^bsub>" ^ s ^ "\<^esub>"
@@ -265,15 +265,15 @@
val simple_string_of_typ = Refute.string_of_typ
val is_real_constr = Refute.is_IDT_constructor
-val typ_of_dtyp = Sledgehammer_Util.typ_of_dtyp
-val varify_type = Sledgehammer_Util.varify_type
-val instantiate_type = Sledgehammer_Util.instantiate_type
-val varify_and_instantiate_type = Sledgehammer_Util.varify_and_instantiate_type
+val typ_of_dtyp = ATP_Util.typ_of_dtyp
+val varify_type = ATP_Util.varify_type
+val instantiate_type = ATP_Util.instantiate_type
+val varify_and_instantiate_type = ATP_Util.varify_and_instantiate_type
val is_of_class_const = Refute.is_const_of_class
val get_class_def = Refute.get_classdef
-val monomorphic_term = Sledgehammer_Util.monomorphic_term
-val specialize_type = Sledgehammer_Util.specialize_type
-val eta_expand = Sledgehammer_Util.eta_expand
+val monomorphic_term = ATP_Util.monomorphic_term
+val specialize_type = ATP_Util.specialize_type
+val eta_expand = ATP_Util.eta_expand
fun time_limit NONE = I
| time_limit (SOME delay) = TimeLimit.timeLimit delay
@@ -290,15 +290,15 @@
val pstrs = Pretty.breaks o map Pretty.str o space_explode " "
-val unyxml = Sledgehammer_Util.unyxml
+val unyxml = ATP_Util.unyxml
-val maybe_quote = Sledgehammer_Util.maybe_quote
+val maybe_quote = ATP_Util.maybe_quote
fun pretty_maybe_quote pretty =
let val s = Pretty.str_of pretty in
if maybe_quote s = s then pretty else Pretty.enum "" "\"" "\"" [pretty]
end
-val hashw = ATP_Problem.hashw
-val hashw_string = ATP_Problem.hashw_string
+val hashw = ATP_Util.hashw
+val hashw_string = ATP_Util.hashw_string
end;
--- a/src/HOL/Tools/Nitpick/nitrox.ML Tue May 31 11:21:47 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitrox.ML Tue May 31 16:38:36 2011 +0200
@@ -13,6 +13,7 @@
structure Nitrox : NITROX =
struct
+open ATP_Util
open ATP_Problem
open ATP_Proof
open Nitpick
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Tue May 31 11:21:47 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1098 +0,0 @@
-(* Title: HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
- Author: Lawrence C. Paulson, Cambridge University Computer Laboratory
- Author: Claire Quigley, Cambridge University Computer Laboratory
- Author: Jasmin Blanchette, TU Muenchen
-
-Proof reconstruction for Sledgehammer.
-*)
-
-signature SLEDGEHAMMER_ATP_RECONSTRUCT =
-sig
- type 'a proof = 'a ATP_Proof.proof
- type locality = Sledgehammer_Filter.locality
- type type_system = Sledgehammer_ATP_Translate.type_system
-
- datatype reconstructor =
- Metis |
- MetisFT |
- SMT of string
-
- datatype play =
- Played of reconstructor * Time.time |
- Trust_Playable of reconstructor * Time.time option|
- Failed_to_Play
-
- type minimize_command = string list -> string
- type one_line_params =
- play * string * (string * locality) list * minimize_command * int * int
- type isar_params =
- bool * bool * int * type_system * string Symtab.table * int list list
- * int * (string * locality) list vector * int Symtab.table * string proof
- * thm
- val repair_conjecture_shape_and_fact_names :
- type_system -> string -> int list list -> int
- -> (string * locality) list vector -> int list
- -> int list list * int * (string * locality) list vector * int list
- val used_facts_in_atp_proof :
- Proof.context -> type_system -> int -> (string * locality) list vector
- -> string proof -> (string * locality) list
- val used_facts_in_unsound_atp_proof :
- Proof.context -> type_system -> int list list -> int
- -> (string * locality) list vector -> 'a proof -> string list option
- val uses_typed_helpers : int list -> 'a proof -> bool
- val reconstructor_name : reconstructor -> string
- val one_line_proof_text : one_line_params -> string
- val isar_proof_text :
- Proof.context -> bool -> isar_params -> one_line_params -> string
- val proof_text :
- Proof.context -> bool -> isar_params -> one_line_params -> string
-end;
-
-structure Sledgehammer_ATP_Reconstruct : SLEDGEHAMMER_ATP_RECONSTRUCT =
-struct
-
-open ATP_Problem
-open ATP_Proof
-open Metis_Translate
-open Sledgehammer_Util
-open Sledgehammer_Filter
-open Sledgehammer_ATP_Translate
-
-datatype reconstructor =
- Metis |
- MetisFT |
- SMT of string
-
-datatype play =
- Played of reconstructor * Time.time |
- Trust_Playable of reconstructor * Time.time option |
- Failed_to_Play
-
-type minimize_command = string list -> string
-type one_line_params =
- play * string * (string * locality) list * minimize_command * int * int
-type isar_params =
- bool * bool * int * type_system * string Symtab.table * int list list * int
- * (string * locality) list vector * int Symtab.table * string proof * thm
-
-fun is_head_digit s = Char.isDigit (String.sub (s, 0))
-val scan_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode)
-
-val is_typed_helper_name =
- String.isPrefix helper_prefix andf String.isSuffix typed_helper_suffix
-
-fun find_first_in_list_vector vec key =
- Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key
- | (_, value) => value) NONE vec
-
-
-(** SPASS's FLOTTER hack **)
-
-(* This is a hack required for keeping track of facts after they have been
- clausified by SPASS's FLOTTER preprocessor. The "ATP/scripts/spass" script is
- also part of this hack. *)
-
-val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation"
-
-fun extract_clause_sequence output =
- let
- val tokens_of = String.tokens (not o Char.isAlphaNum)
- fun extract_num ("clause" :: (ss as _ :: _)) = Int.fromString (List.last ss)
- | extract_num _ = NONE
- in output |> split_lines |> map_filter (extract_num o tokens_of) end
-
-val parse_clause_formula_pair =
- $$ "(" |-- scan_integer --| $$ ","
- -- (Symbol.scan_id ::: Scan.repeat ($$ "," |-- Symbol.scan_id)) --| $$ ")"
- --| Scan.option ($$ ",")
-val parse_clause_formula_relation =
- Scan.this_string set_ClauseFormulaRelationN |-- $$ "("
- |-- Scan.repeat parse_clause_formula_pair
-val extract_clause_formula_relation =
- Substring.full #> Substring.position set_ClauseFormulaRelationN
- #> snd #> Substring.position "." #> fst #> Substring.string
- #> raw_explode #> filter_out Symbol.is_blank #> parse_clause_formula_relation
- #> fst
-
-fun maybe_unprefix_fact_number type_sys =
- polymorphism_of_type_sys type_sys <> Polymorphic
- ? (space_implode "_" o tl o space_explode "_")
-
-fun repair_conjecture_shape_and_fact_names type_sys output conjecture_shape
- fact_offset fact_names typed_helpers =
- if String.isSubstring set_ClauseFormulaRelationN output then
- let
- val j0 = hd (hd conjecture_shape)
- val seq = extract_clause_sequence output
- val name_map = extract_clause_formula_relation output
- fun renumber_conjecture j =
- conjecture_prefix ^ string_of_int (j - j0)
- |> AList.find (fn (s, ss) => member (op =) ss s) name_map
- |> map (fn s => find_index (curry (op =) s) seq + 1)
- fun names_for_number j =
- j |> AList.lookup (op =) name_map |> these
- |> map_filter (try (unascii_of o maybe_unprefix_fact_number type_sys
- o unprefix fact_prefix))
- |> map (fn name =>
- (name, name |> find_first_in_list_vector fact_names |> the)
- handle Option.Option =>
- error ("No such fact: " ^ quote name ^ "."))
- in
- (conjecture_shape |> map (maps renumber_conjecture), 0,
- seq |> map names_for_number |> Vector.fromList,
- name_map |> filter (forall is_typed_helper_name o snd) |> map fst)
- end
- else
- (conjecture_shape, fact_offset, fact_names, typed_helpers)
-
-val vampire_step_prefix = "f" (* grrr... *)
-
-val extract_step_number =
- Int.fromString o perhaps (try (unprefix vampire_step_prefix))
-
-fun resolve_fact type_sys _ fact_names (_, SOME s) =
- (case try (unprefix fact_prefix) s of
- SOME s' =>
- let val s' = s' |> maybe_unprefix_fact_number type_sys |> unascii_of in
- case find_first_in_list_vector fact_names s' of
- SOME x => [(s', x)]
- | NONE => []
- end
- | NONE => [])
- | resolve_fact _ facts_offset fact_names (num, NONE) =
- (case extract_step_number num of
- SOME j =>
- let val j = j - facts_offset in
- if j > 0 andalso j <= Vector.length fact_names then
- Vector.sub (fact_names, j - 1)
- else
- []
- end
- | NONE => [])
-
-fun is_fact type_sys conjecture_shape =
- not o null o resolve_fact type_sys 0 conjecture_shape
-
-fun resolve_conjecture _ (_, SOME s) =
- (case try (unprefix conjecture_prefix) s of
- SOME s' =>
- (case Int.fromString s' of
- SOME j => [j]
- | NONE => [])
- | NONE => [])
- | resolve_conjecture conjecture_shape (num, NONE) =
- case extract_step_number num of
- SOME i => (case find_index (exists (curry (op =) i)) conjecture_shape of
- ~1 => []
- | j => [j])
- | NONE => []
-
-fun is_conjecture conjecture_shape =
- not o null o resolve_conjecture conjecture_shape
-
-fun is_typed_helper _ (_, SOME s) = is_typed_helper_name s
- | is_typed_helper typed_helpers (num, NONE) =
- (case extract_step_number num of
- SOME i => member (op =) typed_helpers i
- | NONE => false)
-
-val leo2_ext = "extcnf_equal_neg"
-val isa_ext = Thm.get_name_hint @{thm ext}
-val isa_short_ext = Long_Name.base_name isa_ext
-
-fun ext_name ctxt =
- if Thm.eq_thm_prop (@{thm ext},
- singleton (Attrib.eval_thms ctxt) (Facts.named isa_short_ext, [])) then
- isa_short_ext
- else
- isa_ext
-
-fun add_fact _ type_sys facts_offset fact_names (Inference (name, _, [])) =
- union (op =) (resolve_fact type_sys facts_offset fact_names name)
- | add_fact ctxt _ _ _ (Inference (_, _, deps)) =
- if AList.defined (op =) deps leo2_ext then
- insert (op =) (ext_name ctxt, General (* or Chained... *))
- else
- I
- | add_fact _ _ _ _ _ = I
-
-fun used_facts_in_atp_proof ctxt type_sys facts_offset fact_names atp_proof =
- if null atp_proof then Vector.foldl (op @) [] fact_names
- else fold (add_fact ctxt type_sys facts_offset fact_names) atp_proof []
-
-fun is_conjecture_referred_to_in_proof conjecture_shape =
- exists (fn Inference (name, _, []) => is_conjecture conjecture_shape name
- | _ => false)
-
-fun used_facts_in_unsound_atp_proof ctxt type_sys conjecture_shape facts_offset
- fact_names atp_proof =
- let
- val used_facts =
- used_facts_in_atp_proof ctxt type_sys facts_offset fact_names atp_proof
- in
- if forall (is_locality_global o snd) used_facts andalso
- not (is_conjecture_referred_to_in_proof conjecture_shape atp_proof) then
- SOME (map fst used_facts)
- else
- NONE
- end
-
-fun uses_typed_helpers typed_helpers =
- exists (fn Inference (name, _, []) => is_typed_helper typed_helpers name
- | _ => false)
-
-
-(** Soft-core proof reconstruction: Metis one-liner **)
-
-fun reconstructor_name Metis = "metis"
- | reconstructor_name MetisFT = "metisFT"
- | reconstructor_name (SMT _) = "smt"
-
-fun reconstructor_settings (SMT settings) = settings
- | reconstructor_settings _ = ""
-
-fun string_for_label (s, num) = s ^ string_of_int num
-
-fun show_time NONE = ""
- | show_time (SOME ext_time) = " (" ^ string_from_ext_time ext_time ^ ")"
-
-fun set_settings "" = ""
- | set_settings settings = "using [[" ^ settings ^ "]] "
-fun apply_on_subgoal settings _ 1 = set_settings settings ^ "by "
- | apply_on_subgoal settings 1 _ = set_settings settings ^ "apply "
- | apply_on_subgoal settings i n =
- "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal settings 1 n
-fun command_call name [] = name
- | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
-fun try_command_line banner time command =
- banner ^ ": " ^ Markup.markup Markup.sendback command ^ show_time time ^ "."
-fun using_labels [] = ""
- | using_labels ls =
- "using " ^ space_implode " " (map string_for_label ls) ^ " "
-fun reconstructor_command reconstructor i n (ls, ss) =
- using_labels ls ^
- apply_on_subgoal (reconstructor_settings reconstructor) i n ^
- command_call (reconstructor_name reconstructor) ss
-fun minimize_line _ [] = ""
- | minimize_line minimize_command ss =
- case minimize_command ss of
- "" => ""
- | command => "\nTo minimize: " ^ Markup.markup Markup.sendback command ^ "."
-
-val split_used_facts =
- List.partition (curry (op =) Chained o snd)
- #> pairself (sort_distinct (string_ord o pairself fst))
-
-fun one_line_proof_text (preplay, banner, used_facts, minimize_command,
- subgoal, subgoal_count) =
- let
- val (chained, extra) = split_used_facts used_facts
- val (reconstructor, ext_time) =
- case preplay of
- Played (reconstructor, time) =>
- (SOME reconstructor, (SOME (false, time)))
- | Trust_Playable (reconstructor, time) =>
- (SOME reconstructor,
- case time of
- NONE => NONE
- | SOME time =>
- if time = Time.zeroTime then NONE else SOME (true, time))
- | Failed_to_Play => (NONE, NONE)
- val try_line =
- case reconstructor of
- SOME r => ([], map fst extra)
- |> reconstructor_command r subgoal subgoal_count
- |> try_command_line banner ext_time
- | NONE => "One-line proof reconstruction failed."
- in try_line ^ minimize_line minimize_command (map fst (extra @ chained)) end
-
-(** Hard-core proof reconstruction: structured Isar proofs **)
-
-(* Simple simplifications to ensure that sort annotations don't leave a trail of
- spurious "True"s. *)
-fun s_not (Const (@{const_name All}, T) $ Abs (s, T', t')) =
- Const (@{const_name Ex}, T) $ Abs (s, T', s_not t')
- | s_not (Const (@{const_name Ex}, T) $ Abs (s, T', t')) =
- Const (@{const_name All}, T) $ Abs (s, T', s_not t')
- | s_not (@{const HOL.implies} $ t1 $ t2) = @{const HOL.conj} $ t1 $ s_not t2
- | s_not (@{const HOL.conj} $ t1 $ t2) =
- @{const HOL.disj} $ s_not t1 $ s_not t2
- | s_not (@{const HOL.disj} $ t1 $ t2) =
- @{const HOL.conj} $ s_not t1 $ s_not t2
- | s_not (@{const False}) = @{const True}
- | s_not (@{const True}) = @{const False}
- | s_not (@{const Not} $ t) = t
- | s_not t = @{const Not} $ t
-fun s_conj (@{const True}, t2) = t2
- | s_conj (t1, @{const True}) = t1
- | s_conj p = HOLogic.mk_conj p
-fun s_disj (@{const False}, t2) = t2
- | s_disj (t1, @{const False}) = t1
- | s_disj p = HOLogic.mk_disj p
-fun s_imp (@{const True}, t2) = t2
- | s_imp (t1, @{const False}) = s_not t1
- | s_imp p = HOLogic.mk_imp p
-fun s_iff (@{const True}, t2) = t2
- | s_iff (t1, @{const True}) = t1
- | s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2
-
-fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda v t
-fun exists_of v t = HOLogic.exists_const (fastype_of v) $ lambda v t
-
-val indent_size = 2
-val no_label = ("", ~1)
-
-val raw_prefix = "X"
-val assum_prefix = "A"
-val have_prefix = "F"
-
-fun raw_label_for_name conjecture_shape name =
- case resolve_conjecture conjecture_shape name of
- [j] => (conjecture_prefix, j)
- | _ => case Int.fromString (fst name) of
- SOME j => (raw_prefix, j)
- | NONE => (raw_prefix ^ fst name, 0)
-
-(**** INTERPRETATION OF TSTP SYNTAX TREES ****)
-
-exception FO_TERM of string fo_term list
-exception FORMULA of (string, string, string fo_term) formula list
-exception SAME of unit
-
-(* Type variables are given the basic sort "HOL.type". Some will later be
- constrained by information from type literals, or by type inference. *)
-fun typ_from_fo_term tfrees (u as ATerm (a, us)) =
- let val Ts = map (typ_from_fo_term tfrees) us in
- case strip_prefix_and_unascii type_const_prefix a of
- SOME b => Type (invert_const b, Ts)
- | NONE =>
- if not (null us) then
- raise FO_TERM [u] (* only "tconst"s have type arguments *)
- else case strip_prefix_and_unascii tfree_prefix a of
- SOME b =>
- let val s = "'" ^ b in
- TFree (s, AList.lookup (op =) tfrees s |> the_default HOLogic.typeS)
- end
- | NONE =>
- case strip_prefix_and_unascii tvar_prefix a of
- SOME b => TVar (("'" ^ b, 0), HOLogic.typeS)
- | NONE =>
- (* Variable from the ATP, say "X1" *)
- Type_Infer.param 0 (a, HOLogic.typeS)
- end
-
-(* Type class literal applied to a type. Returns triple of polarity, class,
- type. *)
-fun type_constraint_from_term tfrees (u as ATerm (a, us)) =
- case (strip_prefix_and_unascii class_prefix a,
- map (typ_from_fo_term tfrees) us) of
- (SOME b, [T]) => (b, T)
- | _ => raise FO_TERM [u]
-
-(** Accumulate type constraints in a formula: negative type literals **)
-fun add_var (key, z) = Vartab.map_default (key, []) (cons z)
-fun add_type_constraint false (cl, TFree (a ,_)) = add_var ((a, ~1), cl)
- | add_type_constraint false (cl, TVar (ix, _)) = add_var (ix, cl)
- | add_type_constraint _ _ = I
-
-fun repair_tptp_variable_name f s =
- let
- fun subscript_name s n = s ^ nat_subscript n
- val s = String.map f s
- in
- case space_explode "_" s of
- [_] => (case take_suffix Char.isDigit (String.explode s) of
- (cs1 as _ :: _, cs2 as _ :: _) =>
- subscript_name (String.implode cs1)
- (the (Int.fromString (String.implode cs2)))
- | (_, _) => s)
- | [s1, s2] => (case Int.fromString s2 of
- SOME n => subscript_name s1 n
- | NONE => s)
- | _ => s
- end
-
-(* First-order translation. No types are known for variables. "HOLogic.typeT"
- should allow them to be inferred. *)
-fun raw_term_from_pred thy sym_tab tfrees =
- let
- fun aux opt_T extra_us u =
- case u of
- ATerm (a, us) =>
- if String.isPrefix simple_type_prefix a then
- @{const True} (* ignore TPTP type information *)
- else if a = tptp_equal then
- let val ts = map (aux NONE []) us in
- if length ts = 2 andalso hd ts aconv List.last ts then
- (* Vampire is keen on producing these. *)
- @{const True}
- else
- list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts)
- end
- else case strip_prefix_and_unascii const_prefix a of
- SOME s =>
- let
- val ((s', s), mangled_us) = s |> unmangled_const |>> `invert_const
- in
- if s' = type_tag_name then
- case mangled_us @ us of
- [typ_u, term_u] =>
- aux (SOME (typ_from_fo_term tfrees typ_u)) extra_us term_u
- | _ => raise FO_TERM us
- else if s' = predicator_name then
- aux (SOME @{typ bool}) [] (hd us)
- else if s' = app_op_name then
- aux opt_T (nth us 1 :: extra_us) (hd us)
- else if s' = type_pred_name then
- @{const True} (* ignore type predicates *)
- else
- let
- val num_ty_args =
- length us - the_default 0 (Symtab.lookup sym_tab s)
- val (type_us, term_us) =
- chop num_ty_args us |>> append mangled_us
- (* Extra args from "hAPP" come after any arguments given
- directly to the constant. *)
- val term_ts = map (aux NONE []) term_us
- val extra_ts = map (aux NONE []) extra_us
- val T =
- if num_type_args thy s' = length type_us then
- Sign.const_instance thy
- (s', map (typ_from_fo_term tfrees) type_us)
- else case opt_T of
- SOME T => map fastype_of (term_ts @ extra_ts) ---> T
- | NONE => HOLogic.typeT
- val s' = s' |> unproxify_const
- in list_comb (Const (s', T), term_ts @ extra_ts) end
- end
- | NONE => (* a free or schematic variable *)
- let
- val ts = map (aux NONE []) (us @ extra_us)
- val T = map fastype_of ts ---> HOLogic.typeT
- val t =
- case strip_prefix_and_unascii fixed_var_prefix a of
- SOME b => Free (b, T)
- | NONE =>
- case strip_prefix_and_unascii schematic_var_prefix a of
- SOME b => Var ((b, 0), T)
- | NONE =>
- if is_tptp_variable a then
- Var ((repair_tptp_variable_name Char.toLower a, 0), T)
- else
- (* Skolem constants? *)
- Var ((repair_tptp_variable_name Char.toUpper a, 0), T)
- in list_comb (t, ts) end
- in aux (SOME HOLogic.boolT) [] end
-
-fun term_from_pred thy sym_tab tfrees pos (u as ATerm (s, _)) =
- if String.isPrefix class_prefix s then
- add_type_constraint pos (type_constraint_from_term tfrees u)
- #> pair @{const True}
- else
- pair (raw_term_from_pred thy sym_tab tfrees u)
-
-val combinator_table =
- [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def_raw}),
- (@{const_name Meson.COMBK}, @{thm Meson.COMBK_def_raw}),
- (@{const_name Meson.COMBB}, @{thm Meson.COMBB_def_raw}),
- (@{const_name Meson.COMBC}, @{thm Meson.COMBC_def_raw}),
- (@{const_name Meson.COMBS}, @{thm Meson.COMBS_def_raw})]
-
-fun uncombine_term thy =
- let
- fun aux (t1 $ t2) = betapply (pairself aux (t1, t2))
- | aux (Abs (s, T, t')) = Abs (s, T, aux t')
- | aux (t as Const (x as (s, _))) =
- (case AList.lookup (op =) combinator_table s of
- SOME thm => thm |> prop_of |> specialize_type thy x
- |> Logic.dest_equals |> snd
- | NONE => t)
- | aux t = t
- in aux end
-
-(* Update schematic type variables with detected sort constraints. It's not
- totally clear whether this code is necessary. *)
-fun repair_tvar_sorts (t, tvar_tab) =
- let
- fun do_type (Type (a, Ts)) = Type (a, map do_type Ts)
- | do_type (TVar (xi, s)) =
- TVar (xi, the_default s (Vartab.lookup tvar_tab xi))
- | do_type (TFree z) = TFree z
- fun do_term (Const (a, T)) = Const (a, do_type T)
- | do_term (Free (a, T)) = Free (a, do_type T)
- | do_term (Var (xi, T)) = Var (xi, do_type T)
- | do_term (t as Bound _) = t
- | do_term (Abs (a, T, t)) = Abs (a, do_type T, do_term t)
- | do_term (t1 $ t2) = do_term t1 $ do_term t2
- in t |> not (Vartab.is_empty tvar_tab) ? do_term end
-
-fun quantify_over_var quant_of var_s t =
- let
- val vars = [] |> Term.add_vars t |> filter (fn ((s, _), _) => s = var_s)
- |> map Var
- in fold_rev quant_of vars t end
-
-(* Interpret an ATP formula as a HOL term, extracting sort constraints as they
- appear in the formula. *)
-fun prop_from_formula thy sym_tab tfrees phi =
- let
- fun do_formula pos phi =
- case phi of
- AQuant (_, [], phi) => do_formula pos phi
- | AQuant (q, (s, _) :: xs, phi') =>
- do_formula pos (AQuant (q, xs, phi'))
- (* FIXME: TFF *)
- #>> quantify_over_var (case q of
- AForall => forall_of
- | AExists => exists_of)
- (repair_tptp_variable_name Char.toLower s)
- | AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not
- | AConn (c, [phi1, phi2]) =>
- do_formula (pos |> c = AImplies ? not) phi1
- ##>> do_formula pos phi2
- #>> (case c of
- AAnd => s_conj
- | AOr => s_disj
- | AImplies => s_imp
- | AIf => s_imp o swap
- | AIff => s_iff
- | ANotIff => s_not o s_iff
- | _ => raise Fail "unexpected connective")
- | AAtom tm => term_from_pred thy sym_tab tfrees pos tm
- | _ => raise FORMULA [phi]
- in repair_tvar_sorts (do_formula true phi Vartab.empty) end
-
-fun check_formula ctxt =
- Type.constraint HOLogic.boolT
- #> Syntax.check_term
- (Proof_Context.set_mode Proof_Context.mode_schematic ctxt)
-
-(**** Translation of TSTP files to Isar Proofs ****)
-
-fun unvarify_term (Var ((s, 0), T)) = Free (s, T)
- | unvarify_term t = raise TERM ("unvarify_term: non-Var", [t])
-
-fun decode_line sym_tab tfrees (Definition (name, phi1, phi2)) ctxt =
- let
- val thy = Proof_Context.theory_of ctxt
- val t1 = prop_from_formula thy sym_tab tfrees phi1
- val vars = snd (strip_comb t1)
- val frees = map unvarify_term vars
- val unvarify_args = subst_atomic (vars ~~ frees)
- val t2 = prop_from_formula thy sym_tab tfrees phi2
- val (t1, t2) =
- HOLogic.eq_const HOLogic.typeT $ t1 $ t2
- |> unvarify_args |> uncombine_term thy |> check_formula ctxt
- |> HOLogic.dest_eq
- in
- (Definition (name, t1, t2),
- fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt)
- end
- | decode_line sym_tab tfrees (Inference (name, u, deps)) ctxt =
- let
- val thy = Proof_Context.theory_of ctxt
- val t = u |> prop_from_formula thy sym_tab tfrees
- |> uncombine_term thy |> check_formula ctxt
- in
- (Inference (name, t, deps),
- fold Variable.declare_term (OldTerm.term_frees t) ctxt)
- end
-fun decode_lines ctxt sym_tab tfrees lines =
- fst (fold_map (decode_line sym_tab tfrees) lines ctxt)
-
-fun is_same_inference _ (Definition _) = false
- | is_same_inference t (Inference (_, t', _)) = t aconv t'
-
-(* No "real" literals means only type information (tfree_tcs, clsrel, or
- clsarity). *)
-val is_only_type_information = curry (op aconv) HOLogic.true_const
-
-fun replace_one_dependency (old, new) dep =
- if is_same_atp_step dep old then new else [dep]
-fun replace_dependencies_in_line _ (line as Definition _) = line
- | replace_dependencies_in_line p (Inference (name, t, deps)) =
- Inference (name, t, fold (union (op =) o replace_one_dependency p) deps [])
-
-(* Discard facts; consolidate adjacent lines that prove the same formula, since
- they differ only in type information.*)
-fun add_line _ _ _ (line as Definition _) lines = line :: lines
- | add_line type_sys conjecture_shape fact_names (Inference (name, t, []))
- lines =
- (* No dependencies: fact, conjecture, or (for Vampire) internal facts or
- definitions. *)
- if is_fact type_sys fact_names name then
- (* Facts are not proof lines. *)
- if is_only_type_information t then
- map (replace_dependencies_in_line (name, [])) lines
- (* Is there a repetition? If so, replace later line by earlier one. *)
- else case take_prefix (not o is_same_inference t) lines of
- (_, []) => lines (* no repetition of proof line *)
- | (pre, Inference (name', _, _) :: post) =>
- pre @ map (replace_dependencies_in_line (name', [name])) post
- | _ => raise Fail "unexpected inference"
- else if is_conjecture conjecture_shape name then
- Inference (name, s_not t, []) :: lines
- else
- map (replace_dependencies_in_line (name, [])) lines
- | add_line _ _ _ (Inference (name, t, deps)) lines =
- (* Type information will be deleted later; skip repetition test. *)
- if is_only_type_information t then
- Inference (name, t, deps) :: lines
- (* Is there a repetition? If so, replace later line by earlier one. *)
- else case take_prefix (not o is_same_inference t) lines of
- (* FIXME: Doesn't this code risk conflating proofs involving different
- types? *)
- (_, []) => Inference (name, t, deps) :: lines
- | (pre, Inference (name', t', _) :: post) =>
- Inference (name, t', deps) ::
- pre @ map (replace_dependencies_in_line (name', [name])) post
- | _ => raise Fail "unexpected inference"
-
-(* Recursively delete empty lines (type information) from the proof. *)
-fun add_nontrivial_line (Inference (name, t, [])) lines =
- if is_only_type_information t then delete_dependency name lines
- else Inference (name, t, []) :: lines
- | add_nontrivial_line line lines = line :: lines
-and delete_dependency name lines =
- fold_rev add_nontrivial_line
- (map (replace_dependencies_in_line (name, [])) lines) []
-
-(* ATPs sometimes reuse free variable names in the strangest ways. Removing
- offending lines often does the trick. *)
-fun is_bad_free frees (Free x) = not (member (op =) frees x)
- | is_bad_free _ _ = false
-
-fun add_desired_line _ _ _ _ _ (line as Definition (name, _, _)) (j, lines) =
- (j, line :: map (replace_dependencies_in_line (name, [])) lines)
- | add_desired_line type_sys isar_shrink_factor conjecture_shape fact_names
- frees (Inference (name, t, deps)) (j, lines) =
- (j + 1,
- if is_fact type_sys fact_names name orelse
- is_conjecture conjecture_shape name orelse
- (* the last line must be kept *)
- j = 0 orelse
- (not (is_only_type_information t) andalso
- null (Term.add_tvars t []) andalso
- not (exists_subterm (is_bad_free frees) t) andalso
- length deps >= 2 andalso j mod isar_shrink_factor = 0 andalso
- (* kill next to last line, which usually results in a trivial step *)
- j <> 1) then
- Inference (name, t, deps) :: lines (* keep line *)
- else
- map (replace_dependencies_in_line (name, deps)) lines) (* drop line *)
-
-(** Isar proof construction and manipulation **)
-
-fun merge_fact_sets (ls1, ss1) (ls2, ss2) =
- (union (op =) ls1 ls2, union (op =) ss1 ss2)
-
-type label = string * int
-type facts = label list * string list
-
-datatype isar_qualifier = Show | Then | Moreover | Ultimately
-
-datatype isar_step =
- Fix of (string * typ) list |
- Let of term * term |
- Assume of label * term |
- Have of isar_qualifier list * label * term * byline
-and byline =
- ByMetis of facts |
- CaseSplit of isar_step list list * facts
-
-fun smart_case_split [] facts = ByMetis facts
- | smart_case_split proofs facts = CaseSplit (proofs, facts)
-
-fun add_fact_from_dependency type_sys conjecture_shape facts_offset fact_names
- name =
- if is_fact type_sys fact_names name then
- apsnd (union (op =)
- (map fst (resolve_fact type_sys facts_offset fact_names name)))
- else
- apfst (insert (op =) (raw_label_for_name conjecture_shape name))
-
-fun step_for_line _ _ _ _ _ (Definition (_, t1, t2)) = Let (t1, t2)
- | step_for_line _ conjecture_shape _ _ _ (Inference (name, t, [])) =
- Assume (raw_label_for_name conjecture_shape name, t)
- | step_for_line type_sys conjecture_shape facts_offset
- fact_names j (Inference (name, t, deps)) =
- Have (if j = 1 then [Show] else [],
- raw_label_for_name conjecture_shape name,
- fold_rev forall_of (map Var (Term.add_vars t [])) t,
- ByMetis (fold (add_fact_from_dependency type_sys conjecture_shape
- facts_offset fact_names)
- deps ([], [])))
-
-fun repair_name "$true" = "c_True"
- | repair_name "$false" = "c_False"
- | repair_name "$$e" = tptp_equal (* seen in Vampire proofs *)
- | repair_name s =
- if is_tptp_equal s orelse
- (* seen in Vampire proofs *)
- (String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s) then
- tptp_equal
- else
- s
-
-fun isar_proof_from_atp_proof pool ctxt type_sys tfrees isar_shrink_factor
- conjecture_shape facts_offset fact_names sym_tab params frees
- atp_proof =
- let
- val lines =
- atp_proof
- |> clean_up_atp_proof_dependencies
- |> nasty_atp_proof pool
- |> map_term_names_in_atp_proof repair_name
- |> decode_lines ctxt sym_tab tfrees
- |> rpair [] |-> fold_rev (add_line type_sys conjecture_shape fact_names)
- |> rpair [] |-> fold_rev add_nontrivial_line
- |> rpair (0, [])
- |-> fold_rev (add_desired_line type_sys isar_shrink_factor
- conjecture_shape fact_names frees)
- |> snd
- in
- (if null params then [] else [Fix params]) @
- map2 (step_for_line type_sys conjecture_shape facts_offset fact_names)
- (length lines downto 1) lines
- end
-
-(* When redirecting proofs, we keep information about the labels seen so far in
- the "backpatches" data structure. The first component indicates which facts
- should be associated with forthcoming proof steps. The second component is a
- pair ("assum_ls", "drop_ls"), where "assum_ls" are the labels that should
- become assumptions and "drop_ls" are the labels that should be dropped in a
- case split. *)
-type backpatches = (label * facts) list * (label list * label list)
-
-fun used_labels_of_step (Have (_, _, _, by)) =
- (case by of
- ByMetis (ls, _) => ls
- | CaseSplit (proofs, (ls, _)) =>
- fold (union (op =) o used_labels_of) proofs ls)
- | used_labels_of_step _ = []
-and used_labels_of proof = fold (union (op =) o used_labels_of_step) proof []
-
-fun new_labels_of_step (Fix _) = []
- | new_labels_of_step (Let _) = []
- | new_labels_of_step (Assume (l, _)) = [l]
- | new_labels_of_step (Have (_, l, _, _)) = [l]
-val new_labels_of = maps new_labels_of_step
-
-val join_proofs =
- let
- fun aux _ [] = NONE
- | aux proof_tail (proofs as (proof1 :: _)) =
- if exists null proofs then
- NONE
- else if forall (curry (op =) (hd proof1) o hd) (tl proofs) then
- aux (hd proof1 :: proof_tail) (map tl proofs)
- else case hd proof1 of
- Have ([], l, t, _) => (* FIXME: should we really ignore the "by"? *)
- if forall (fn Have ([], l', t', _) :: _ => (l, t) = (l', t')
- | _ => false) (tl proofs) andalso
- not (exists (member (op =) (maps new_labels_of proofs))
- (used_labels_of proof_tail)) then
- SOME (l, t, map rev proofs, proof_tail)
- else
- NONE
- | _ => NONE
- in aux [] o map rev end
-
-fun case_split_qualifiers proofs =
- case length proofs of
- 0 => []
- | 1 => [Then]
- | _ => [Ultimately]
-
-fun redirect_proof hyp_ts concl_t proof =
- let
- (* The first pass outputs those steps that are independent of the negated
- conjecture. The second pass flips the proof by contradiction to obtain a
- direct proof, introducing case splits when an inference depends on
- several facts that depend on the negated conjecture. *)
- val concl_l = (conjecture_prefix, length hyp_ts)
- fun first_pass ([], contra) = ([], contra)
- | first_pass ((step as Fix _) :: proof, contra) =
- first_pass (proof, contra) |>> cons step
- | first_pass ((step as Let _) :: proof, contra) =
- first_pass (proof, contra) |>> cons step
- | first_pass ((step as Assume (l as (_, j), _)) :: proof, contra) =
- if l = concl_l then first_pass (proof, contra ||> cons step)
- else first_pass (proof, contra) |>> cons (Assume (l, nth hyp_ts j))
- | first_pass (Have (qs, l, t, ByMetis (ls, ss)) :: proof, contra) =
- let val step = Have (qs, l, t, ByMetis (ls, ss)) in
- if exists (member (op =) (fst contra)) ls then
- first_pass (proof, contra |>> cons l ||> cons step)
- else
- first_pass (proof, contra) |>> cons step
- end
- | first_pass _ = raise Fail "malformed proof"
- val (proof_top, (contra_ls, contra_proof)) =
- first_pass (proof, ([concl_l], []))
- val backpatch_label = the_default ([], []) oo AList.lookup (op =) o fst
- fun backpatch_labels patches ls =
- fold merge_fact_sets (map (backpatch_label patches) ls) ([], [])
- fun second_pass end_qs ([], assums, patches) =
- ([Have (end_qs, no_label, concl_t,
- ByMetis (backpatch_labels patches (map snd assums)))], patches)
- | second_pass end_qs (Assume (l, t) :: proof, assums, patches) =
- second_pass end_qs (proof, (t, l) :: assums, patches)
- | second_pass end_qs (Have (qs, l, t, ByMetis (ls, ss)) :: proof, assums,
- patches) =
- (if member (op =) (snd (snd patches)) l andalso
- not (member (op =) (fst (snd patches)) l) andalso
- not (AList.defined (op =) (fst patches) l) then
- second_pass end_qs (proof, assums, patches ||> apsnd (append ls))
- else case List.partition (member (op =) contra_ls) ls of
- ([contra_l], co_ls) =>
- if member (op =) qs Show then
- second_pass end_qs (proof, assums,
- patches |>> cons (contra_l, (co_ls, ss)))
- else
- second_pass end_qs
- (proof, assums,
- patches |>> cons (contra_l, (l :: co_ls, ss)))
- |>> cons (if member (op =) (fst (snd patches)) l then
- Assume (l, s_not t)
- else
- Have (qs, l, s_not t,
- ByMetis (backpatch_label patches l)))
- | (contra_ls as _ :: _, co_ls) =>
- let
- val proofs =
- map_filter
- (fn l =>
- if l = concl_l then
- NONE
- else
- let
- val drop_ls = filter (curry (op <>) l) contra_ls
- in
- second_pass []
- (proof, assums,
- patches ||> apfst (insert (op =) l)
- ||> apsnd (union (op =) drop_ls))
- |> fst |> SOME
- end) contra_ls
- val (assumes, facts) =
- if member (op =) (fst (snd patches)) l then
- ([Assume (l, s_not t)], (l :: co_ls, ss))
- else
- ([], (co_ls, ss))
- in
- (case join_proofs proofs of
- SOME (l, t, proofs, proof_tail) =>
- Have (case_split_qualifiers proofs @
- (if null proof_tail then end_qs else []), l, t,
- smart_case_split proofs facts) :: proof_tail
- | NONE =>
- [Have (case_split_qualifiers proofs @ end_qs, no_label,
- concl_t, smart_case_split proofs facts)],
- patches)
- |>> append assumes
- end
- | _ => raise Fail "malformed proof")
- | second_pass _ _ = raise Fail "malformed proof"
- val proof_bottom =
- second_pass [Show] (contra_proof, [], ([], ([], []))) |> fst
- in proof_top @ proof_bottom end
-
-(* FIXME: Still needed? Probably not. *)
-val kill_duplicate_assumptions_in_proof =
- let
- fun relabel_facts subst =
- apfst (map (fn l => AList.lookup (op =) subst l |> the_default l))
- fun do_step (step as Assume (l, t)) (proof, subst, assums) =
- (case AList.lookup (op aconv) assums t of
- SOME l' => (proof, (l, l') :: subst, assums)
- | NONE => (step :: proof, subst, (t, l) :: assums))
- | do_step (Have (qs, l, t, by)) (proof, subst, assums) =
- (Have (qs, l, t,
- case by of
- ByMetis facts => ByMetis (relabel_facts subst facts)
- | CaseSplit (proofs, facts) =>
- CaseSplit (map do_proof proofs, relabel_facts subst facts)) ::
- proof, subst, assums)
- | do_step step (proof, subst, assums) = (step :: proof, subst, assums)
- and do_proof proof = fold do_step proof ([], [], []) |> #1 |> rev
- in do_proof end
-
-val then_chain_proof =
- let
- fun aux _ [] = []
- | aux _ ((step as Assume (l, _)) :: proof) = step :: aux l proof
- | aux l' (Have (qs, l, t, by) :: proof) =
- (case by of
- ByMetis (ls, ss) =>
- Have (if member (op =) ls l' then
- (Then :: qs, l, t,
- ByMetis (filter_out (curry (op =) l') ls, ss))
- else
- (qs, l, t, ByMetis (ls, ss)))
- | CaseSplit (proofs, facts) =>
- Have (qs, l, t, CaseSplit (map (aux no_label) proofs, facts))) ::
- aux l proof
- | aux _ (step :: proof) = step :: aux no_label proof
- in aux no_label end
-
-fun kill_useless_labels_in_proof proof =
- let
- val used_ls = used_labels_of proof
- fun do_label l = if member (op =) used_ls l then l else no_label
- fun do_step (Assume (l, t)) = Assume (do_label l, t)
- | do_step (Have (qs, l, t, by)) =
- Have (qs, do_label l, t,
- case by of
- CaseSplit (proofs, facts) =>
- CaseSplit (map (map do_step) proofs, facts)
- | _ => by)
- | do_step step = step
- in map do_step proof end
-
-fun prefix_for_depth n = replicate_string (n + 1)
-
-val relabel_proof =
- let
- fun aux _ _ _ [] = []
- | aux subst depth (next_assum, next_fact) (Assume (l, t) :: proof) =
- if l = no_label then
- Assume (l, t) :: aux subst depth (next_assum, next_fact) proof
- else
- let val l' = (prefix_for_depth depth assum_prefix, next_assum) in
- Assume (l', t) ::
- aux ((l, l') :: subst) depth (next_assum + 1, next_fact) proof
- end
- | aux subst depth (next_assum, next_fact) (Have (qs, l, t, by) :: proof) =
- let
- val (l', subst, next_fact) =
- if l = no_label then
- (l, subst, next_fact)
- else
- let
- val l' = (prefix_for_depth depth have_prefix, next_fact)
- in (l', (l, l') :: subst, next_fact + 1) end
- val relabel_facts =
- apfst (maps (the_list o AList.lookup (op =) subst))
- val by =
- case by of
- ByMetis facts => ByMetis (relabel_facts facts)
- | CaseSplit (proofs, facts) =>
- CaseSplit (map (aux subst (depth + 1) (1, 1)) proofs,
- relabel_facts facts)
- in
- Have (qs, l', t, by) ::
- aux subst depth (next_assum, next_fact) proof
- end
- | aux subst depth nextp (step :: proof) =
- step :: aux subst depth nextp proof
- in aux [] 0 (1, 1) end
-
-fun string_for_proof ctxt0 full_types i n =
- let
- val ctxt =
- ctxt0 |> Config.put show_free_types false
- |> Config.put show_types true
- |> Config.put show_sorts true
- fun fix_print_mode f x =
- Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
- (print_mode_value ())) f x
- fun do_indent ind = replicate_string (ind * indent_size) " "
- fun do_free (s, T) =
- maybe_quote s ^ " :: " ^
- maybe_quote (fix_print_mode (Syntax.string_of_typ ctxt) T)
- fun do_label l = if l = no_label then "" else string_for_label l ^ ": "
- fun do_have qs =
- (if member (op =) qs Moreover then "moreover " else "") ^
- (if member (op =) qs Ultimately then "ultimately " else "") ^
- (if member (op =) qs Then then
- if member (op =) qs Show then "thus" else "hence"
- else
- if member (op =) qs Show then "show" else "have")
- val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
- val reconstructor = if full_types then MetisFT else Metis
- fun do_facts (ls, ss) =
- reconstructor_command reconstructor 1 1
- (ls |> sort_distinct (prod_ord string_ord int_ord),
- ss |> sort_distinct string_ord)
- and do_step ind (Fix xs) =
- do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n"
- | do_step ind (Let (t1, t2)) =
- do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n"
- | do_step ind (Assume (l, t)) =
- do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n"
- | do_step ind (Have (qs, l, t, ByMetis facts)) =
- do_indent ind ^ do_have qs ^ " " ^
- do_label l ^ do_term t ^ " " ^ do_facts facts ^ "\n"
- | do_step ind (Have (qs, l, t, CaseSplit (proofs, facts))) =
- space_implode (do_indent ind ^ "moreover\n")
- (map (do_block ind) proofs) ^
- do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ " " ^
- do_facts facts ^ "\n"
- and do_steps prefix suffix ind steps =
- let val s = implode (map (do_step ind) steps) in
- replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
- String.extract (s, ind * indent_size,
- SOME (size s - ind * indent_size - 1)) ^
- suffix ^ "\n"
- end
- and do_block ind proof = do_steps "{ " " }" (ind + 1) proof
- (* One-step proofs are pointless; better use the Metis one-liner
- directly. *)
- and do_proof [Have (_, _, _, ByMetis _)] = ""
- | do_proof proof =
- (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
- do_indent 0 ^ "proof -\n" ^ do_steps "" "" 1 proof ^ do_indent 0 ^
- (if n <> 1 then "next" else "qed")
- in do_proof end
-
-fun isar_proof_text ctxt isar_proof_requested
- (debug, full_types, isar_shrink_factor, type_sys, pool,
- conjecture_shape, facts_offset, fact_names, sym_tab, atp_proof, goal)
- (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
- let
- val isar_shrink_factor =
- (if isar_proof_requested then 1 else 2) * isar_shrink_factor
- val (params, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal
- val frees = fold Term.add_frees (concl_t :: hyp_ts) []
- val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) []
- val one_line_proof = one_line_proof_text one_line_params
- fun isar_proof_for () =
- case atp_proof
- |> isar_proof_from_atp_proof pool ctxt type_sys tfrees
- isar_shrink_factor conjecture_shape facts_offset
- fact_names sym_tab params frees
- |> redirect_proof hyp_ts concl_t
- |> kill_duplicate_assumptions_in_proof
- |> then_chain_proof
- |> kill_useless_labels_in_proof
- |> relabel_proof
- |> string_for_proof ctxt full_types subgoal subgoal_count of
- "" =>
- if isar_proof_requested then
- "\nNo structured proof available (proof too short)."
- else
- ""
- | proof =>
- "\n\n" ^ (if isar_proof_requested then "Structured proof"
- else "Perhaps this will work") ^
- ":\n" ^ Markup.markup Markup.sendback proof
- val isar_proof =
- if debug then
- isar_proof_for ()
- else
- case try isar_proof_for () of
- SOME s => s
- | NONE => if isar_proof_requested then
- "\nWarning: The Isar proof construction failed."
- else
- ""
- in one_line_proof ^ isar_proof end
-
-fun proof_text ctxt isar_proof isar_params
- (one_line_params as (preplay, _, _, _, _, _)) =
- (if isar_proof orelse preplay = Failed_to_Play then
- isar_proof_text ctxt isar_proof isar_params
- else
- one_line_proof_text) one_line_params
-
-end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Tue May 31 11:21:47 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1389 +0,0 @@
-(* Title: HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
- Author: Fabian Immler, TU Muenchen
- Author: Makarius
- Author: Jasmin Blanchette, TU Muenchen
-
-Translation of HOL to FOL for Sledgehammer.
-*)
-
-signature SLEDGEHAMMER_ATP_TRANSLATE =
-sig
- type 'a fo_term = 'a ATP_Problem.fo_term
- type format = ATP_Problem.format
- type formula_kind = ATP_Problem.formula_kind
- type 'a problem = 'a ATP_Problem.problem
- type locality = Sledgehammer_Filter.locality
-
- datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
- datatype type_level =
- All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
- datatype type_heaviness = Heavy | Light
-
- datatype type_system =
- Simple_Types of type_level |
- Preds of polymorphism * type_level * type_heaviness |
- Tags of polymorphism * type_level * type_heaviness
-
- type translated_formula
-
- val readable_names : bool Config.T
- val fact_prefix : string
- val conjecture_prefix : string
- val helper_prefix : string
- val typed_helper_suffix : string
- val predicator_name : string
- val app_op_name : string
- val type_pred_name : string
- val simple_type_prefix : string
- val type_sys_from_string : string -> type_system
- val polymorphism_of_type_sys : type_system -> polymorphism
- val level_of_type_sys : type_system -> type_level
- val is_type_sys_virtually_sound : type_system -> bool
- val is_type_sys_fairly_sound : type_system -> bool
- val unmangled_const : string -> string * string fo_term list
- val translate_atp_fact :
- Proof.context -> format -> type_system -> bool -> (string * locality) * thm
- -> translated_formula option * ((string * locality) * thm)
- val prepare_atp_problem :
- Proof.context -> format -> formula_kind -> formula_kind -> type_system
- -> bool option -> term list -> term
- -> (translated_formula option * ((string * 'a) * thm)) list
- -> string problem * string Symtab.table * int * int
- * (string * 'a) list vector * int list * int Symtab.table
- val atp_problem_weights : string problem -> (string * real) list
-end;
-
-structure Sledgehammer_ATP_Translate : SLEDGEHAMMER_ATP_TRANSLATE =
-struct
-
-open ATP_Problem
-open Metis_Translate
-open Sledgehammer_Util
-open Sledgehammer_Filter
-
-(* experimental *)
-val generate_useful_info = false
-
-fun useful_isabelle_info s =
- if generate_useful_info then
- SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])]))
- else
- NONE
-
-val intro_info = useful_isabelle_info "intro"
-val elim_info = useful_isabelle_info "elim"
-val simp_info = useful_isabelle_info "simp"
-
-(* Readable names are often much shorter, especially if types are mangled in
- names. Also, the logic for generating legal SNARK sort names is only
- implemented for readable names. Finally, readable names are, well, more
- readable. For these reason, they are enabled by default. *)
-val readable_names =
- Attrib.setup_config_bool @{binding sledgehammer_atp_readable_names} (K true)
-
-val type_decl_prefix = "ty_"
-val sym_decl_prefix = "sy_"
-val sym_formula_prefix = "sym_"
-val fact_prefix = "fact_"
-val conjecture_prefix = "conj_"
-val helper_prefix = "help_"
-val class_rel_clause_prefix = "crel_";
-val arity_clause_prefix = "arity_"
-val tfree_prefix = "tfree_"
-
-val typed_helper_suffix = "_T"
-val untyped_helper_suffix = "_U"
-
-val predicator_name = "hBOOL"
-val app_op_name = "hAPP"
-val type_pred_name = "is"
-val simple_type_prefix = "ty_"
-
-fun make_simple_type s =
- if s = tptp_bool_type orelse s = tptp_fun_type orelse
- s = tptp_individual_type then
- s
- else
- simple_type_prefix ^ ascii_of s
-
-(* Freshness almost guaranteed! *)
-val sledgehammer_weak_prefix = "Sledgehammer:"
-
-datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
-datatype type_level =
- All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
-datatype type_heaviness = Heavy | Light
-
-datatype type_system =
- Simple_Types of type_level |
- Preds of polymorphism * type_level * type_heaviness |
- Tags of polymorphism * type_level * type_heaviness
-
-fun try_unsuffixes ss s =
- fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
-
-fun type_sys_from_string s =
- (case try (unprefix "poly_") s of
- SOME s => (SOME Polymorphic, s)
- | NONE =>
- case try (unprefix "mono_") s of
- SOME s => (SOME Monomorphic, s)
- | NONE =>
- case try (unprefix "mangled_") s of
- SOME s => (SOME Mangled_Monomorphic, s)
- | NONE => (NONE, s))
- ||> (fn s =>
- (* "_query" and "_bang" are for the ASCII-challenged Mirabelle. *)
- case try_unsuffixes ["?", "_query"] s of
- SOME s => (Nonmonotonic_Types, s)
- | NONE =>
- case try_unsuffixes ["!", "_bang"] s of
- SOME s => (Finite_Types, s)
- | NONE => (All_Types, s))
- ||> apsnd (fn s =>
- case try (unsuffix "_heavy") s of
- SOME s => (Heavy, s)
- | NONE => (Light, s))
- |> (fn (poly, (level, (heaviness, core))) =>
- case (core, (poly, level, heaviness)) of
- ("simple", (NONE, _, Light)) => Simple_Types level
- | ("preds", (SOME poly, _, _)) => Preds (poly, level, heaviness)
- | ("tags", (SOME Polymorphic, All_Types, _)) =>
- Tags (Polymorphic, All_Types, heaviness)
- | ("tags", (SOME Polymorphic, _, _)) =>
- (* The actual light encoding is very unsound. *)
- Tags (Polymorphic, level, Heavy)
- | ("tags", (SOME poly, _, _)) => Tags (poly, level, heaviness)
- | ("args", (SOME poly, All_Types (* naja *), Light)) =>
- Preds (poly, Const_Arg_Types, Light)
- | ("erased", (NONE, All_Types (* naja *), Light)) =>
- Preds (Polymorphic, No_Types, Light)
- | _ => raise Same.SAME)
- handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")
-
-fun polymorphism_of_type_sys (Simple_Types _) = Mangled_Monomorphic
- | polymorphism_of_type_sys (Preds (poly, _, _)) = poly
- | polymorphism_of_type_sys (Tags (poly, _, _)) = poly
-
-fun level_of_type_sys (Simple_Types level) = level
- | level_of_type_sys (Preds (_, level, _)) = level
- | level_of_type_sys (Tags (_, level, _)) = level
-
-fun heaviness_of_type_sys (Simple_Types _) = Heavy
- | heaviness_of_type_sys (Preds (_, _, heaviness)) = heaviness
- | heaviness_of_type_sys (Tags (_, _, heaviness)) = heaviness
-
-fun is_type_level_virtually_sound level =
- level = All_Types orelse level = Nonmonotonic_Types
-val is_type_sys_virtually_sound =
- is_type_level_virtually_sound o level_of_type_sys
-
-fun is_type_level_fairly_sound level =
- is_type_level_virtually_sound level orelse level = Finite_Types
-val is_type_sys_fairly_sound = is_type_level_fairly_sound o level_of_type_sys
-
-fun is_setting_higher_order THF (Simple_Types _) = true
- | is_setting_higher_order _ _ = false
-
-type translated_formula =
- {name: string,
- locality: locality,
- kind: formula_kind,
- combformula: (name, typ, combterm) formula,
- atomic_types: typ list}
-
-fun update_combformula f ({name, locality, kind, combformula, atomic_types}
- : translated_formula) =
- {name = name, locality = locality, kind = kind, combformula = f combformula,
- atomic_types = atomic_types} : translated_formula
-
-fun fact_lift f ({combformula, ...} : translated_formula) = f combformula
-
-val type_instance = Sign.typ_instance o Proof_Context.theory_of
-
-fun insert_type ctxt get_T x xs =
- let val T = get_T x in
- if exists (curry (type_instance ctxt) T o get_T) xs then xs
- else x :: filter_out (curry (type_instance ctxt o swap) T o get_T) xs
- end
-
-(* The Booleans indicate whether all type arguments should be kept. *)
-datatype type_arg_policy =
- Explicit_Type_Args of bool |
- Mangled_Type_Args of bool |
- No_Type_Args
-
-fun should_drop_arg_type_args (Simple_Types _) =
- false (* since TFF doesn't support overloading *)
- | should_drop_arg_type_args type_sys =
- level_of_type_sys type_sys = All_Types andalso
- heaviness_of_type_sys type_sys = Heavy
-
-fun general_type_arg_policy type_sys =
- if level_of_type_sys type_sys = No_Types then
- No_Type_Args
- else if polymorphism_of_type_sys type_sys = Mangled_Monomorphic then
- Mangled_Type_Args (should_drop_arg_type_args type_sys)
- else
- Explicit_Type_Args (should_drop_arg_type_args type_sys)
-
-fun type_arg_policy type_sys s =
- if s = @{const_name HOL.eq} orelse
- (s = app_op_name andalso level_of_type_sys type_sys = Const_Arg_Types) then
- No_Type_Args
- else
- general_type_arg_policy type_sys
-
-fun atp_type_literals_for_types format type_sys kind Ts =
- if level_of_type_sys type_sys = No_Types orelse format = CNF_UEQ then
- []
- else
- Ts |> type_literals_for_types
- |> filter (fn TyLitVar _ => kind <> Conjecture
- | TyLitFree _ => kind = Conjecture)
-
-fun mk_aconns c phis =
- let val (phis', phi') = split_last phis in
- fold_rev (mk_aconn c) phis' phi'
- end
-fun mk_ahorn [] phi = phi
- | mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi])
-fun mk_aquant _ [] phi = phi
- | mk_aquant q xs (phi as AQuant (q', xs', phi')) =
- if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi)
- | mk_aquant q xs phi = AQuant (q, xs, phi)
-
-fun close_universally atom_vars phi =
- let
- fun formula_vars bounds (AQuant (_, xs, phi)) =
- formula_vars (map fst xs @ bounds) phi
- | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
- | formula_vars bounds (AAtom tm) =
- union (op =) (atom_vars tm []
- |> filter_out (member (op =) bounds o fst))
- in mk_aquant AForall (formula_vars [] phi []) phi end
-
-fun combterm_vars (CombApp (tm1, tm2)) = fold combterm_vars [tm1, tm2]
- | combterm_vars (CombConst _) = I
- | combterm_vars (CombVar (name, T)) = insert (op =) (name, SOME T)
-fun close_combformula_universally phi = close_universally combterm_vars phi
-
-fun term_vars (ATerm (name as (s, _), tms)) =
- is_tptp_variable s ? insert (op =) (name, NONE) #> fold term_vars tms
-fun close_formula_universally phi = close_universally term_vars phi
-
-val homo_infinite_type_name = @{type_name ind} (* any infinite type *)
-val homo_infinite_type = Type (homo_infinite_type_name, [])
-
-fun fo_term_from_typ higher_order =
- let
- fun term (Type (s, Ts)) =
- ATerm (case (higher_order, s) of
- (true, @{type_name bool}) => `I tptp_bool_type
- | (true, @{type_name fun}) => `I tptp_fun_type
- | _ => if s = homo_infinite_type_name then `I tptp_individual_type
- else `make_fixed_type_const s,
- map term Ts)
- | term (TFree (s, _)) = ATerm (`make_fixed_type_var s, [])
- | term (TVar ((x as (s, _)), _)) =
- ATerm ((make_schematic_type_var x, s), [])
- in term end
-
-(* This shouldn't clash with anything else. *)
-val mangled_type_sep = "\000"
-
-fun generic_mangled_type_name f (ATerm (name, [])) = f name
- | generic_mangled_type_name f (ATerm (name, tys)) =
- f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys)
- ^ ")"
-
-val bool_atype = AType (`I tptp_bool_type)
-
-fun ho_type_from_fo_term higher_order pred_sym ary =
- let
- fun to_atype ty =
- AType ((make_simple_type (generic_mangled_type_name fst ty),
- generic_mangled_type_name snd ty))
- fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))
- fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
- | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
- fun to_ho (ty as ATerm ((s, _), tys)) =
- if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
- in if higher_order then to_ho else to_fo ary end
-
-fun mangled_type higher_order pred_sym ary =
- ho_type_from_fo_term higher_order pred_sym ary o fo_term_from_typ higher_order
-
-fun mangled_const_name T_args (s, s') =
- let
- val ty_args = map (fo_term_from_typ false) T_args
- fun type_suffix f g =
- fold_rev (curry (op ^) o g o prefix mangled_type_sep
- o generic_mangled_type_name f) ty_args ""
- in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end
-
-val parse_mangled_ident =
- Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode
-
-fun parse_mangled_type x =
- (parse_mangled_ident
- -- Scan.optional ($$ "(" |-- Scan.optional parse_mangled_types [] --| $$ ")")
- [] >> ATerm) x
-and parse_mangled_types x =
- (parse_mangled_type ::: Scan.repeat ($$ "," |-- parse_mangled_type)) x
-
-fun unmangled_type s =
- s |> suffix ")" |> raw_explode
- |> Scan.finite Symbol.stopper
- (Scan.error (!! (fn _ => raise Fail ("unrecognized mangled type " ^
- quote s)) parse_mangled_type))
- |> fst
-
-val unmangled_const_name = space_explode mangled_type_sep #> hd
-fun unmangled_const s =
- let val ss = space_explode mangled_type_sep s in
- (hd ss, map unmangled_type (tl ss))
- end
-
-fun introduce_proxies format type_sys =
- let
- fun intro top_level (CombApp (tm1, tm2)) =
- CombApp (intro top_level tm1, intro false tm2)
- | intro top_level (CombConst (name as (s, _), T, T_args)) =
- (case proxify_const s of
- SOME (_, proxy_base) =>
- if top_level orelse is_setting_higher_order format type_sys then
- case (top_level, s) of
- (_, "c_False") => (`I tptp_false, [])
- | (_, "c_True") => (`I tptp_true, [])
- | (false, "c_Not") => (`I tptp_not, [])
- | (false, "c_conj") => (`I tptp_and, [])
- | (false, "c_disj") => (`I tptp_or, [])
- | (false, "c_implies") => (`I tptp_implies, [])
- | (false, s) =>
- if is_tptp_equal s then (`I tptp_equal, [])
- else (proxy_base |>> prefix const_prefix, T_args)
- | _ => (name, [])
- else
- (proxy_base |>> prefix const_prefix, T_args)
- | NONE => (name, T_args))
- |> (fn (name, T_args) => CombConst (name, T, T_args))
- | intro _ tm = tm
- in intro true end
-
-fun combformula_from_prop thy format type_sys eq_as_iff =
- let
- fun do_term bs t atomic_types =
- combterm_from_term thy bs (Envir.eta_contract t)
- |>> (introduce_proxies format type_sys #> AAtom)
- ||> union (op =) atomic_types
- fun do_quant bs q s T t' =
- let val s = Name.variant (map fst bs) s in
- do_formula ((s, T) :: bs) t'
- #>> mk_aquant q [(`make_bound_var s, SOME T)]
- end
- and do_conn bs c t1 t2 =
- do_formula bs t1 ##>> do_formula bs t2
- #>> uncurry (mk_aconn c)
- and do_formula bs t =
- case t of
- @{const Not} $ t1 => do_formula bs t1 #>> mk_anot
- | Const (@{const_name All}, _) $ Abs (s, T, t') =>
- do_quant bs AForall s T t'
- | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
- do_quant bs AExists s T t'
- | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd t1 t2
- | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2
- | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2
- | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
- if eq_as_iff then do_conn bs AIff t1 t2 else do_term bs t
- | _ => do_term bs t
- in do_formula [] end
-
-fun presimplify_term ctxt =
- Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
- #> Meson.presimplify ctxt
- #> prop_of
-
-fun concealed_bound_name j = sledgehammer_weak_prefix ^ string_of_int j
-fun conceal_bounds Ts t =
- subst_bounds (map (Free o apfst concealed_bound_name)
- (0 upto length Ts - 1 ~~ Ts), t)
-fun reveal_bounds Ts =
- subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
- (0 upto length Ts - 1 ~~ Ts))
-
-fun extensionalize_term ctxt t =
- let val thy = Proof_Context.theory_of ctxt in
- t |> cterm_of thy |> Meson.extensionalize_conv ctxt
- |> prop_of |> Logic.dest_equals |> snd
- end
-
-fun introduce_combinators_in_term ctxt kind t =
- let val thy = Proof_Context.theory_of ctxt in
- if Meson.is_fol_term thy t then
- t
- else
- let
- fun aux Ts t =
- case t of
- @{const Not} $ t1 => @{const Not} $ aux Ts t1
- | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
- t0 $ Abs (s, T, aux (T :: Ts) t')
- | (t0 as Const (@{const_name All}, _)) $ t1 =>
- aux Ts (t0 $ eta_expand Ts t1 1)
- | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
- t0 $ Abs (s, T, aux (T :: Ts) t')
- | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
- aux Ts (t0 $ eta_expand Ts t1 1)
- | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
- | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
- | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
- | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
- $ t1 $ t2 =>
- t0 $ aux Ts t1 $ aux Ts t2
- | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
- t
- else
- t |> conceal_bounds Ts
- |> Envir.eta_contract
- |> cterm_of thy
- |> Meson_Clausify.introduce_combinators_in_cterm
- |> prop_of |> Logic.dest_equals |> snd
- |> reveal_bounds Ts
- val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
- in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
- handle THM _ =>
- (* A type variable of sort "{}" will make abstraction fail. *)
- if kind = Conjecture then HOLogic.false_const
- else HOLogic.true_const
- end
-
-(* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
- same in Sledgehammer to prevent the discovery of unreplayable proofs. *)
-fun freeze_term t =
- let
- fun aux (t $ u) = aux t $ aux u
- | aux (Abs (s, T, t)) = Abs (s, T, aux t)
- | aux (Var ((s, i), T)) =
- Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
- | aux t = t
- in t |> exists_subterm is_Var t ? aux end
-
-(* making fact and conjecture formulas *)
-fun make_formula ctxt format type_sys eq_as_iff presimp name loc kind t =
- let
- val thy = Proof_Context.theory_of ctxt
- val t = t |> Envir.beta_eta_contract
- |> transform_elim_prop
- |> Object_Logic.atomize_term thy
- val need_trueprop = (fastype_of t = @{typ bool})
- val t = t |> need_trueprop ? HOLogic.mk_Trueprop
- |> Raw_Simplifier.rewrite_term thy
- (Meson.unfold_set_const_simps ctxt) []
- |> extensionalize_term ctxt
- |> presimp ? presimplify_term ctxt
- |> perhaps (try (HOLogic.dest_Trueprop))
- |> introduce_combinators_in_term ctxt kind
- |> kind <> Axiom ? freeze_term
- val (combformula, atomic_types) =
- combformula_from_prop thy format type_sys eq_as_iff t []
- in
- {name = name, locality = loc, kind = kind, combformula = combformula,
- atomic_types = atomic_types}
- end
-
-fun make_fact ctxt format type_sys keep_trivial eq_as_iff presimp
- ((name, loc), t) =
- case (keep_trivial,
- make_formula ctxt format type_sys eq_as_iff presimp name loc Axiom t) of
- (false, formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...}) =>
- if s = tptp_true then NONE else SOME formula
- | (_, formula) => SOME formula
-
-fun make_conjecture ctxt format prem_kind type_sys ts =
- let val last = length ts - 1 in
- map2 (fn j => fn t =>
- let
- val (kind, maybe_negate) =
- if j = last then
- (Conjecture, I)
- else
- (prem_kind,
- if prem_kind = Conjecture then update_combformula mk_anot
- else I)
- in
- t |> make_formula ctxt format type_sys true true
- (string_of_int j) General kind
- |> maybe_negate
- end)
- (0 upto last) ts
- end
-
-(** Finite and infinite type inference **)
-
-fun deep_freeze_atyp (TVar (_, S)) = TFree ("v", S)
- | deep_freeze_atyp T = T
-val deep_freeze_type = map_atyps deep_freeze_atyp
-
-(* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
- dangerous because their "exhaust" properties can easily lead to unsound ATP
- proofs. On the other hand, all HOL infinite types can be given the same
- models in first-order logic (via Löwenheim-Skolem). *)
-
-fun should_encode_type ctxt (nonmono_Ts as _ :: _) _ T =
- exists (curry (type_instance ctxt) (deep_freeze_type T)) nonmono_Ts
- | should_encode_type _ _ All_Types _ = true
- | should_encode_type ctxt _ Finite_Types T = is_type_surely_finite ctxt T
- | should_encode_type _ _ _ _ = false
-
-fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level, heaviness))
- should_predicate_on_var T =
- (heaviness = Heavy orelse should_predicate_on_var ()) andalso
- should_encode_type ctxt nonmono_Ts level T
- | should_predicate_on_type _ _ _ _ _ = false
-
-fun is_var_or_bound_var (CombConst ((s, _), _, _)) =
- String.isPrefix bound_var_prefix s
- | is_var_or_bound_var (CombVar _) = true
- | is_var_or_bound_var _ = false
-
-datatype tag_site = Top_Level | Eq_Arg | Elsewhere
-
-fun should_tag_with_type _ _ _ Top_Level _ _ = false
- | should_tag_with_type ctxt nonmono_Ts (Tags (_, level, heaviness)) site u T =
- (case heaviness of
- Heavy => should_encode_type ctxt nonmono_Ts level T
- | Light =>
- case (site, is_var_or_bound_var u) of
- (Eq_Arg, true) => should_encode_type ctxt nonmono_Ts level T
- | _ => false)
- | should_tag_with_type _ _ _ _ _ _ = false
-
-fun homogenized_type ctxt nonmono_Ts level =
- let
- val should_encode = should_encode_type ctxt nonmono_Ts level
- fun homo 0 T = if should_encode T then T else homo_infinite_type
- | homo ary (Type (@{type_name fun}, [T1, T2])) =
- homo 0 T1 --> homo (ary - 1) T2
- | homo _ _ = raise Fail "expected function type"
- in homo end
-
-(** "hBOOL" and "hAPP" **)
-
-type sym_info =
- {pred_sym : bool, min_ary : int, max_ary : int, types : typ list}
-
-fun add_combterm_syms_to_table ctxt explicit_apply =
- let
- fun consider_var_arity const_T var_T max_ary =
- let
- fun iter ary T =
- if ary = max_ary orelse type_instance ctxt (var_T, T) then ary
- else iter (ary + 1) (range_type T)
- in iter 0 const_T end
- fun add top_level tm (accum as (ho_var_Ts, sym_tab)) =
- let val (head, args) = strip_combterm_comb tm in
- (case head of
- CombConst ((s, _), T, _) =>
- if String.isPrefix bound_var_prefix s then
- if explicit_apply = NONE andalso can dest_funT T then
- let
- fun repair_min_arity {pred_sym, min_ary, max_ary, types} =
- {pred_sym = pred_sym,
- min_ary =
- fold (fn T' => consider_var_arity T' T) types min_ary,
- max_ary = max_ary, types = types}
- val ho_var_Ts' = ho_var_Ts |> insert_type ctxt I T
- in
- if pointer_eq (ho_var_Ts', ho_var_Ts) then accum
- else (ho_var_Ts', Symtab.map (K repair_min_arity) sym_tab)
- end
- else
- accum
- else
- let
- val ary = length args
- in
- (ho_var_Ts,
- case Symtab.lookup sym_tab s of
- SOME {pred_sym, min_ary, max_ary, types} =>
- let
- val types' = types |> insert_type ctxt I T
- val min_ary =
- if is_some explicit_apply orelse
- pointer_eq (types', types) then
- min_ary
- else
- fold (consider_var_arity T) ho_var_Ts min_ary
- in
- Symtab.update (s, {pred_sym = pred_sym andalso top_level,
- min_ary = Int.min (ary, min_ary),
- max_ary = Int.max (ary, max_ary),
- types = types'})
- sym_tab
- end
- | NONE =>
- let
- val min_ary =
- case explicit_apply of
- SOME true => 0
- | SOME false => ary
- | NONE => fold (consider_var_arity T) ho_var_Ts ary
- in
- Symtab.update_new (s, {pred_sym = top_level,
- min_ary = min_ary, max_ary = ary,
- types = [T]})
- sym_tab
- end)
- end
- | _ => accum)
- |> fold (add false) args
- end
- in add true end
-fun add_fact_syms_to_table ctxt explicit_apply =
- fact_lift (formula_fold NONE
- (K (add_combterm_syms_to_table ctxt explicit_apply)))
-
-val default_sym_table_entries : (string * sym_info) list =
- [(tptp_equal, {pred_sym = true, min_ary = 2, max_ary = 2, types = []}),
- (tptp_old_equal, {pred_sym = true, min_ary = 2, max_ary = 2, types = []}),
- (make_fixed_const predicator_name,
- {pred_sym = true, min_ary = 1, max_ary = 1, types = []})] @
- ([tptp_false, tptp_true]
- |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []}))
-
-fun sym_table_for_facts ctxt explicit_apply facts =
- Symtab.empty
- |> fold Symtab.default default_sym_table_entries
- |> pair [] |> fold (add_fact_syms_to_table ctxt explicit_apply) facts |> snd
-
-fun min_arity_of sym_tab s =
- case Symtab.lookup sym_tab s of
- SOME ({min_ary, ...} : sym_info) => min_ary
- | NONE =>
- case strip_prefix_and_unascii const_prefix s of
- SOME s =>
- let val s = s |> unmangled_const_name |> invert_const in
- if s = predicator_name then 1
- else if s = app_op_name then 2
- else if s = type_pred_name then 1
- else 0
- end
- | NONE => 0
-
-(* True if the constant ever appears outside of the top-level position in
- literals, or if it appears with different arities (e.g., because of different
- type instantiations). If false, the constant always receives all of its
- arguments and is used as a predicate. *)
-fun is_pred_sym sym_tab s =
- case Symtab.lookup sym_tab s of
- SOME ({pred_sym, min_ary, max_ary, ...} : sym_info) =>
- pred_sym andalso min_ary = max_ary
- | NONE => false
-
-val predicator_combconst =
- CombConst (`make_fixed_const predicator_name, @{typ "bool => bool"}, [])
-fun predicator tm = CombApp (predicator_combconst, tm)
-
-fun introduce_predicators_in_combterm sym_tab tm =
- case strip_combterm_comb tm of
- (CombConst ((s, _), _, _), _) =>
- if is_pred_sym sym_tab s then tm else predicator tm
- | _ => predicator tm
-
-fun list_app head args = fold (curry (CombApp o swap)) args head
-
-fun explicit_app arg head =
- let
- val head_T = combtyp_of head
- val (arg_T, res_T) = dest_funT head_T
- val explicit_app =
- CombConst (`make_fixed_const app_op_name, head_T --> head_T,
- [arg_T, res_T])
- in list_app explicit_app [head, arg] end
-fun list_explicit_app head args = fold explicit_app args head
-
-fun introduce_explicit_apps_in_combterm sym_tab =
- let
- fun aux tm =
- case strip_combterm_comb tm of
- (head as CombConst ((s, _), _, _), args) =>
- args |> map aux
- |> chop (min_arity_of sym_tab s)
- |>> list_app head
- |-> list_explicit_app
- | (head, args) => list_explicit_app head (map aux args)
- in aux end
-
-fun chop_fun 0 T = ([], T)
- | chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) =
- chop_fun (n - 1) ran_T |>> cons dom_T
- | chop_fun _ _ = raise Fail "unexpected non-function"
-
-fun filter_type_args _ _ _ [] = []
- | filter_type_args thy s arity T_args =
- let
- (* will throw "TYPE" for pseudo-constants *)
- val U = if s = app_op_name then
- @{typ "('a => 'b) => 'a => 'b"} |> Logic.varifyT_global
- else
- s |> Sign.the_const_type thy
- in
- case Term.add_tvarsT (U |> chop_fun arity |> snd) [] of
- [] => []
- | res_U_vars =>
- let val U_args = (s, U) |> Sign.const_typargs thy in
- U_args ~~ T_args
- |> map_filter (fn (U, T) =>
- if member (op =) res_U_vars (dest_TVar U) then
- SOME T
- else
- NONE)
- end
- end
- handle TYPE _ => T_args
-
-fun enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys =
- let
- val thy = Proof_Context.theory_of ctxt
- fun aux arity (CombApp (tm1, tm2)) =
- CombApp (aux (arity + 1) tm1, aux 0 tm2)
- | aux arity (CombConst (name as (s, _), T, T_args)) =
- let
- val level = level_of_type_sys type_sys
- val (T, T_args) =
- (* Aggressively merge most "hAPPs" if the type system is unsound
- anyway, by distinguishing overloads only on the homogenized
- result type. Don't do it for lightweight type systems, though,
- since it leads to too many unsound proofs. *)
- if s = const_prefix ^ app_op_name andalso
- length T_args = 2 andalso
- not (is_type_sys_virtually_sound type_sys) andalso
- heaviness_of_type_sys type_sys = Heavy then
- T_args |> map (homogenized_type ctxt nonmono_Ts level 0)
- |> (fn Ts => let val T = hd Ts --> nth Ts 1 in
- (T --> T, tl Ts)
- end)
- else
- (T, T_args)
- in
- (case strip_prefix_and_unascii const_prefix s of
- NONE => (name, T_args)
- | SOME s'' =>
- let
- val s'' = invert_const s''
- fun filtered_T_args false = T_args
- | filtered_T_args true = filter_type_args thy s'' arity T_args
- in
- case type_arg_policy type_sys s'' of
- Explicit_Type_Args drop_args =>
- (name, filtered_T_args drop_args)
- | Mangled_Type_Args drop_args =>
- (mangled_const_name (filtered_T_args drop_args) name, [])
- | No_Type_Args => (name, [])
- end)
- |> (fn (name, T_args) => CombConst (name, T, T_args))
- end
- | aux _ tm = tm
- in aux 0 end
-
-fun repair_combterm ctxt format nonmono_Ts type_sys sym_tab =
- not (is_setting_higher_order format type_sys)
- ? (introduce_explicit_apps_in_combterm sym_tab
- #> introduce_predicators_in_combterm sym_tab)
- #> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys
-fun repair_fact ctxt format nonmono_Ts type_sys sym_tab =
- update_combformula (formula_map
- (repair_combterm ctxt format nonmono_Ts type_sys sym_tab))
-
-(** Helper facts **)
-
-fun ti_ti_helper_fact () =
- let
- fun var s = ATerm (`I s, [])
- fun tag tm = ATerm (`make_fixed_const type_tag_name, [var "X", tm])
- in
- Formula (helper_prefix ^ "ti_ti", Axiom,
- AAtom (ATerm (`I tptp_equal, [tag (tag (var "Y")), tag (var "Y")]))
- |> close_formula_universally, simp_info, NONE)
- end
-
-fun helper_facts_for_sym ctxt format type_sys (s, {types, ...} : sym_info) =
- case strip_prefix_and_unascii const_prefix s of
- SOME mangled_s =>
- let
- val thy = Proof_Context.theory_of ctxt
- val unmangled_s = mangled_s |> unmangled_const_name
- fun dub_and_inst c needs_fairly_sound (th, j) =
- ((c ^ "_" ^ string_of_int j ^
- (if needs_fairly_sound then typed_helper_suffix
- else untyped_helper_suffix),
- General),
- let val t = th |> prop_of in
- t |> ((case general_type_arg_policy type_sys of
- Mangled_Type_Args _ => true
- | _ => false) andalso
- not (null (Term.hidden_polymorphism t)))
- ? (case types of
- [T] => specialize_type thy (invert_const unmangled_s, T)
- | _ => I)
- end)
- fun make_facts eq_as_iff =
- map_filter (make_fact ctxt format type_sys false eq_as_iff false)
- val fairly_sound = is_type_sys_fairly_sound type_sys
- in
- metis_helpers
- |> maps (fn (metis_s, (needs_fairly_sound, ths)) =>
- if metis_s <> unmangled_s orelse
- (needs_fairly_sound andalso not fairly_sound) then
- []
- else
- ths ~~ (1 upto length ths)
- |> map (dub_and_inst mangled_s needs_fairly_sound)
- |> make_facts (not needs_fairly_sound))
- end
- | NONE => []
-fun helper_facts_for_sym_table ctxt format type_sys sym_tab =
- Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_sys) sym_tab
- []
-
-fun translate_atp_fact ctxt format type_sys keep_trivial =
- `(make_fact ctxt format type_sys keep_trivial true true o apsnd prop_of)
-
-fun translate_formulas ctxt format prem_kind type_sys hyp_ts concl_t
- rich_facts =
- let
- val thy = Proof_Context.theory_of ctxt
- val fact_ts = map (prop_of o snd o snd) rich_facts
- val (facts, fact_names) =
- rich_facts
- |> map_filter (fn (NONE, _) => NONE
- | (SOME fact, (name, _)) => SOME (fact, name))
- |> ListPair.unzip
- (* Remove existing facts from the conjecture, as this can dramatically
- boost an ATP's performance (for some reason). *)
- val hyp_ts = hyp_ts |> filter_out (member (op aconv) fact_ts)
- val goal_t = Logic.list_implies (hyp_ts, concl_t)
- val all_ts = goal_t :: fact_ts
- val subs = tfree_classes_of_terms all_ts
- val supers = tvar_classes_of_terms all_ts
- val tycons = type_consts_of_terms thy all_ts
- val conjs =
- hyp_ts @ [concl_t] |> make_conjecture ctxt format prem_kind type_sys
- val (supers', arity_clauses) =
- if level_of_type_sys type_sys = No_Types then ([], [])
- else make_arity_clauses thy tycons supers
- val class_rel_clauses = make_class_rel_clauses thy subs supers'
- in
- (fact_names |> map single, (conjs, facts, class_rel_clauses, arity_clauses))
- end
-
-fun fo_literal_from_type_literal (TyLitVar (class, name)) =
- (true, ATerm (class, [ATerm (name, [])]))
- | fo_literal_from_type_literal (TyLitFree (class, name)) =
- (true, ATerm (class, [ATerm (name, [])]))
-
-fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
-
-fun type_pred_combterm ctxt nonmono_Ts type_sys T tm =
- CombApp (CombConst (`make_fixed_const type_pred_name, T --> @{typ bool}, [T])
- |> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys,
- tm)
-
-fun var_occurs_positively_naked_in_term _ (SOME false) _ accum = accum
- | var_occurs_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
- accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, [])))
-fun is_var_nonmonotonic_in_formula _ _ (SOME false) _ = false
- | is_var_nonmonotonic_in_formula pos phi _ name =
- formula_fold pos (var_occurs_positively_naked_in_term name) phi false
-
-fun mk_const_aterm x T_args args =
- ATerm (x, map (fo_term_from_typ false) T_args @ args)
-
-fun tag_with_type ctxt format nonmono_Ts type_sys T tm =
- CombConst (`make_fixed_const type_tag_name, T --> T, [T])
- |> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys
- |> term_from_combterm ctxt format nonmono_Ts type_sys Top_Level
- |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm]))
-and term_from_combterm ctxt format nonmono_Ts type_sys =
- let
- fun aux site u =
- let
- val (head, args) = strip_combterm_comb u
- val (x as (s, _), T_args) =
- case head of
- CombConst (name, _, T_args) => (name, T_args)
- | CombVar (name, _) => (name, [])
- | CombApp _ => raise Fail "impossible \"CombApp\""
- val arg_site = if site = Top_Level andalso is_tptp_equal s then Eq_Arg
- else Elsewhere
- val t = mk_const_aterm x T_args (map (aux arg_site) args)
- val T = combtyp_of u
- in
- t |> (if should_tag_with_type ctxt nonmono_Ts type_sys site u T then
- tag_with_type ctxt format nonmono_Ts type_sys T
- else
- I)
- end
- in aux end
-and formula_from_combformula ctxt format nonmono_Ts type_sys
- should_predicate_on_var =
- let
- val higher_order = is_setting_higher_order format type_sys
- val do_term = term_from_combterm ctxt format nonmono_Ts type_sys Top_Level
- val do_bound_type =
- case type_sys of
- Simple_Types level =>
- homogenized_type ctxt nonmono_Ts level 0
- #> mangled_type higher_order false 0 #> SOME
- | _ => K NONE
- fun do_out_of_bound_type pos phi universal (name, T) =
- if should_predicate_on_type ctxt nonmono_Ts type_sys
- (fn () => should_predicate_on_var pos phi universal name) T then
- CombVar (name, T)
- |> type_pred_combterm ctxt nonmono_Ts type_sys T
- |> do_term |> AAtom |> SOME
- else
- NONE
- fun do_formula pos (AQuant (q, xs, phi)) =
- let
- val phi = phi |> do_formula pos
- val universal = Option.map (q = AExists ? not) pos
- in
- AQuant (q, xs |> map (apsnd (fn NONE => NONE
- | SOME T => do_bound_type T)),
- (if q = AForall then mk_ahorn else fold_rev (mk_aconn AAnd))
- (map_filter
- (fn (_, NONE) => NONE
- | (s, SOME T) =>
- do_out_of_bound_type pos phi universal (s, T))
- xs)
- phi)
- end
- | do_formula pos (AConn conn) = aconn_map pos do_formula conn
- | do_formula _ (AAtom tm) = AAtom (do_term tm)
- in do_formula o SOME end
-
-fun bound_atomic_types format type_sys Ts =
- mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal)
- (atp_type_literals_for_types format type_sys Axiom Ts))
-
-fun formula_for_fact ctxt format nonmono_Ts type_sys
- ({combformula, atomic_types, ...} : translated_formula) =
- combformula
- |> close_combformula_universally
- |> formula_from_combformula ctxt format nonmono_Ts type_sys
- is_var_nonmonotonic_in_formula true
- |> bound_atomic_types format type_sys atomic_types
- |> close_formula_universally
-
-(* Each fact is given a unique fact number to avoid name clashes (e.g., because
- of monomorphization). The TPTP explicitly forbids name clashes, and some of
- the remote provers might care. *)
-fun formula_line_for_fact ctxt format prefix nonmono_Ts type_sys
- (j, formula as {name, locality, kind, ...}) =
- Formula (prefix ^ (if polymorphism_of_type_sys type_sys = Polymorphic then ""
- else string_of_int j ^ "_") ^
- ascii_of name,
- kind, formula_for_fact ctxt format nonmono_Ts type_sys formula, NONE,
- case locality of
- Intro => intro_info
- | Elim => elim_info
- | Simp => simp_info
- | _ => NONE)
-
-fun formula_line_for_class_rel_clause
- (ClassRelClause {name, subclass, superclass, ...}) =
- let val ty_arg = ATerm (`I "T", []) in
- Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
- AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
- AAtom (ATerm (superclass, [ty_arg]))])
- |> close_formula_universally, intro_info, NONE)
- end
-
-fun fo_literal_from_arity_literal (TConsLit (c, t, args)) =
- (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
- | fo_literal_from_arity_literal (TVarLit (c, sort)) =
- (false, ATerm (c, [ATerm (sort, [])]))
-
-fun formula_line_for_arity_clause
- (ArityClause {name, prem_lits, concl_lits, ...}) =
- Formula (arity_clause_prefix ^ ascii_of name, Axiom,
- mk_ahorn (map (formula_from_fo_literal o apfst not
- o fo_literal_from_arity_literal) prem_lits)
- (formula_from_fo_literal
- (fo_literal_from_arity_literal concl_lits))
- |> close_formula_universally, intro_info, NONE)
-
-fun formula_line_for_conjecture ctxt format nonmono_Ts type_sys
- ({name, kind, combformula, ...} : translated_formula) =
- Formula (conjecture_prefix ^ name, kind,
- formula_from_combformula ctxt format nonmono_Ts type_sys
- is_var_nonmonotonic_in_formula false
- (close_combformula_universally combformula)
- |> close_formula_universally, NONE, NONE)
-
-fun free_type_literals format type_sys
- ({atomic_types, ...} : translated_formula) =
- atomic_types |> atp_type_literals_for_types format type_sys Conjecture
- |> map fo_literal_from_type_literal
-
-fun formula_line_for_free_type j lit =
- Formula (tfree_prefix ^ string_of_int j, Hypothesis,
- formula_from_fo_literal lit, NONE, NONE)
-fun formula_lines_for_free_types format type_sys facts =
- let
- val litss = map (free_type_literals format type_sys) facts
- val lits = fold (union (op =)) litss []
- in map2 formula_line_for_free_type (0 upto length lits - 1) lits end
-
-(** Symbol declarations **)
-
-fun should_declare_sym type_sys pred_sym s =
- is_tptp_user_symbol s andalso not (String.isPrefix bound_var_prefix s) andalso
- (case type_sys of
- Simple_Types _ => true
- | Tags (_, _, Light) => true
- | _ => not pred_sym)
-
-fun sym_decl_table_for_facts ctxt type_sys repaired_sym_tab (conjs, facts) =
- let
- fun add_combterm in_conj tm =
- let val (head, args) = strip_combterm_comb tm in
- (case head of
- CombConst ((s, s'), T, T_args) =>
- let val pred_sym = is_pred_sym repaired_sym_tab s in
- if should_declare_sym type_sys pred_sym s then
- Symtab.map_default (s, [])
- (insert_type ctxt #3 (s', T_args, T, pred_sym, length args,
- in_conj))
- else
- I
- end
- | _ => I)
- #> fold (add_combterm in_conj) args
- end
- fun add_fact in_conj =
- fact_lift (formula_fold NONE (K (add_combterm in_conj)))
- in
- Symtab.empty
- |> is_type_sys_fairly_sound type_sys
- ? (fold (add_fact true) conjs #> fold (add_fact false) facts)
- end
-
-(* These types witness that the type classes they belong to allow infinite
- models and hence that any types with these type classes is monotonic. *)
-val known_infinite_types = [@{typ nat}, @{typ int}, @{typ "nat => bool"}]
-
-(* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
- out with monotonicity" paper presented at CADE 2011. *)
-fun add_combterm_nonmonotonic_types _ _ (SOME false) _ = I
- | add_combterm_nonmonotonic_types ctxt level _
- (CombApp (CombApp (CombConst ((s, _), Type (_, [T, _]), _), tm1), tm2)) =
- (is_tptp_equal s andalso exists is_var_or_bound_var [tm1, tm2] andalso
- (case level of
- Nonmonotonic_Types =>
- not (is_type_surely_infinite ctxt known_infinite_types T)
- | Finite_Types => is_type_surely_finite ctxt T
- | _ => true)) ? insert_type ctxt I (deep_freeze_type T)
- | add_combterm_nonmonotonic_types _ _ _ _ = I
-fun add_fact_nonmonotonic_types ctxt level ({kind, combformula, ...}
- : translated_formula) =
- formula_fold (SOME (kind <> Conjecture))
- (add_combterm_nonmonotonic_types ctxt level) combformula
-fun nonmonotonic_types_for_facts ctxt type_sys facts =
- let val level = level_of_type_sys type_sys in
- if level = Nonmonotonic_Types orelse level = Finite_Types then
- [] |> fold (add_fact_nonmonotonic_types ctxt level) facts
- (* We must add "bool" in case the helper "True_or_False" is added
- later. In addition, several places in the code rely on the list of
- nonmonotonic types not being empty. *)
- |> insert_type ctxt I @{typ bool}
- else
- []
- end
-
-fun decl_line_for_sym ctxt format nonmono_Ts type_sys s
- (s', T_args, T, pred_sym, ary, _) =
- let
- val (higher_order, T_arg_Ts, level) =
- case type_sys of
- Simple_Types level => (format = THF, [], level)
- | _ => (false, replicate (length T_args) homo_infinite_type, No_Types)
- in
- Decl (sym_decl_prefix ^ s, (s, s'),
- (T_arg_Ts ---> (T |> homogenized_type ctxt nonmono_Ts level ary))
- |> mangled_type higher_order pred_sym (length T_arg_Ts + ary))
- end
-
-fun is_polymorphic_type T = fold_atyps (fn TVar _ => K true | _ => I) T false
-
-fun formula_line_for_pred_sym_decl ctxt format conj_sym_kind nonmono_Ts type_sys
- n s j (s', T_args, T, _, ary, in_conj) =
- let
- val (kind, maybe_negate) =
- if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
- else (Axiom, I)
- val (arg_Ts, res_T) = chop_fun ary T
- val bound_names =
- 1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)
- val bounds =
- bound_names ~~ arg_Ts |> map (fn (name, T) => CombConst (name, T, []))
- val bound_Ts =
- arg_Ts |> map (fn T => if n > 1 orelse is_polymorphic_type T then SOME T
- else NONE)
- in
- Formula (sym_formula_prefix ^ s ^
- (if n > 1 then "_" ^ string_of_int j else ""), kind,
- CombConst ((s, s'), T, T_args)
- |> fold (curry (CombApp o swap)) bounds
- |> type_pred_combterm ctxt nonmono_Ts type_sys res_T
- |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
- |> formula_from_combformula ctxt format nonmono_Ts type_sys
- (K (K (K (K true)))) true
- |> n > 1 ? bound_atomic_types format type_sys (atyps_of T)
- |> close_formula_universally
- |> maybe_negate,
- intro_info, NONE)
- end
-
-fun formula_lines_for_tag_sym_decl ctxt format conj_sym_kind nonmono_Ts type_sys
- n s (j, (s', T_args, T, pred_sym, ary, in_conj)) =
- let
- val ident_base =
- sym_formula_prefix ^ s ^ (if n > 1 then "_" ^ string_of_int j else "")
- val (kind, maybe_negate) =
- if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
- else (Axiom, I)
- val (arg_Ts, res_T) = chop_fun ary T
- val bound_names =
- 1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)
- val bounds = bound_names |> map (fn name => ATerm (name, []))
- val cst = mk_const_aterm (s, s') T_args
- val atomic_Ts = atyps_of T
- fun eq tms =
- (if pred_sym then AConn (AIff, map AAtom tms)
- else AAtom (ATerm (`I tptp_equal, tms)))
- |> bound_atomic_types format type_sys atomic_Ts
- |> close_formula_universally
- |> maybe_negate
- val should_encode = should_encode_type ctxt nonmono_Ts All_Types
- val tag_with = tag_with_type ctxt format nonmono_Ts type_sys
- val add_formula_for_res =
- if should_encode res_T then
- cons (Formula (ident_base ^ "_res", kind,
- eq [tag_with res_T (cst bounds), cst bounds],
- simp_info, NONE))
- else
- I
- fun add_formula_for_arg k =
- let val arg_T = nth arg_Ts k in
- if should_encode arg_T then
- case chop k bounds of
- (bounds1, bound :: bounds2) =>
- cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), kind,
- eq [cst (bounds1 @ tag_with arg_T bound :: bounds2),
- cst bounds],
- simp_info, NONE))
- | _ => raise Fail "expected nonempty tail"
- else
- I
- end
- in
- [] |> not pred_sym ? add_formula_for_res
- |> fold add_formula_for_arg (ary - 1 downto 0)
- end
-
-fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
-
-fun problem_lines_for_sym_decls ctxt format conj_sym_kind nonmono_Ts type_sys
- (s, decls) =
- case type_sys of
- Simple_Types _ =>
- decls |> map (decl_line_for_sym ctxt format nonmono_Ts type_sys s)
- | Preds _ =>
- let
- val decls =
- case decls of
- decl :: (decls' as _ :: _) =>
- let val T = result_type_of_decl decl in
- if forall (curry (type_instance ctxt o swap) T
- o result_type_of_decl) decls' then
- [decl]
- else
- decls
- end
- | _ => decls
- val n = length decls
- val decls =
- decls
- |> filter (should_predicate_on_type ctxt nonmono_Ts type_sys (K true)
- o result_type_of_decl)
- in
- (0 upto length decls - 1, decls)
- |-> map2 (formula_line_for_pred_sym_decl ctxt format conj_sym_kind
- nonmono_Ts type_sys n s)
- end
- | Tags (_, _, heaviness) =>
- (case heaviness of
- Heavy => []
- | Light =>
- let val n = length decls in
- (0 upto n - 1 ~~ decls)
- |> maps (formula_lines_for_tag_sym_decl ctxt format conj_sym_kind
- nonmono_Ts type_sys n s)
- end)
-
-fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts
- type_sys sym_decl_tab =
- sym_decl_tab
- |> Symtab.dest
- |> sort_wrt fst
- |> rpair []
- |-> fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind
- nonmono_Ts type_sys)
-
-fun should_add_ti_ti_helper (Tags (Polymorphic, level, Heavy)) =
- level = Nonmonotonic_Types orelse level = Finite_Types
- | should_add_ti_ti_helper _ = false
-
-fun offset_of_heading_in_problem _ [] j = j
- | offset_of_heading_in_problem needle ((heading, lines) :: problem) j =
- if heading = needle then j
- else offset_of_heading_in_problem needle problem (j + length lines)
-
-val implicit_declsN = "Should-be-implicit typings"
-val explicit_declsN = "Explicit typings"
-val factsN = "Relevant facts"
-val class_relsN = "Class relationships"
-val aritiesN = "Arities"
-val helpersN = "Helper facts"
-val conjsN = "Conjectures"
-val free_typesN = "Type variables"
-
-fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys
- explicit_apply hyp_ts concl_t facts =
- let
- val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
- translate_formulas ctxt format prem_kind type_sys hyp_ts concl_t facts
- val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
- val nonmono_Ts = conjs @ facts |> nonmonotonic_types_for_facts ctxt type_sys
- val repair = repair_fact ctxt format nonmono_Ts type_sys sym_tab
- val (conjs, facts) = (conjs, facts) |> pairself (map repair)
- val repaired_sym_tab =
- conjs @ facts |> sym_table_for_facts ctxt (SOME false)
- val helpers =
- repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_sys
- |> map repair
- val lavish_nonmono_Ts =
- if null nonmono_Ts orelse
- polymorphism_of_type_sys type_sys <> Polymorphic then
- nonmono_Ts
- else
- [TVar (("'a", 0), HOLogic.typeS)]
- val sym_decl_lines =
- (conjs, helpers @ facts)
- |> sym_decl_table_for_facts ctxt type_sys repaired_sym_tab
- |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind
- lavish_nonmono_Ts type_sys
- val helper_lines =
- 0 upto length helpers - 1 ~~ helpers
- |> map (formula_line_for_fact ctxt format helper_prefix lavish_nonmono_Ts
- type_sys)
- |> (if should_add_ti_ti_helper type_sys then cons (ti_ti_helper_fact ())
- else I)
- (* Reordering these might confuse the proof reconstruction code or the SPASS
- FLOTTER hack. *)
- val problem =
- [(explicit_declsN, sym_decl_lines),
- (factsN,
- map (formula_line_for_fact ctxt format fact_prefix nonmono_Ts type_sys)
- (0 upto length facts - 1 ~~ facts)),
- (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses),
- (aritiesN, map formula_line_for_arity_clause arity_clauses),
- (helpersN, helper_lines),
- (conjsN,
- map (formula_line_for_conjecture ctxt format nonmono_Ts type_sys)
- conjs),
- (free_typesN,
- formula_lines_for_free_types format type_sys (facts @ conjs))]
- val problem =
- problem
- |> (if format = CNF_UEQ then filter_cnf_ueq_problem else I)
- |> (if is_format_typed format then
- declare_undeclared_syms_in_atp_problem type_decl_prefix
- implicit_declsN
- else
- I)
- val (problem, pool) =
- problem |> nice_atp_problem (Config.get ctxt readable_names)
- val helpers_offset = offset_of_heading_in_problem helpersN problem 0
- val typed_helpers =
- map_filter (fn (j, {name, ...}) =>
- if String.isSuffix typed_helper_suffix name then SOME j
- else NONE)
- ((helpers_offset + 1 upto helpers_offset + length helpers)
- ~~ helpers)
- fun add_sym_arity (s, {min_ary, ...} : sym_info) =
- if min_ary > 0 then
- case strip_prefix_and_unascii const_prefix s of
- SOME s => Symtab.insert (op =) (s, min_ary)
- | NONE => I
- else
- I
- in
- (problem,
- case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
- offset_of_heading_in_problem conjsN problem 0,
- offset_of_heading_in_problem factsN problem 0,
- fact_names |> Vector.fromList,
- typed_helpers,
- Symtab.empty |> Symtab.fold add_sym_arity sym_tab)
- end
-
-(* FUDGE *)
-val conj_weight = 0.0
-val hyp_weight = 0.1
-val fact_min_weight = 0.2
-val fact_max_weight = 1.0
-val type_info_default_weight = 0.8
-
-fun add_term_weights weight (ATerm (s, tms)) =
- is_tptp_user_symbol s ? Symtab.default (s, weight)
- #> fold (add_term_weights weight) tms
-fun add_problem_line_weights weight (Formula (_, _, phi, _, _)) =
- formula_fold NONE (K (add_term_weights weight)) phi
- | add_problem_line_weights _ _ = I
-
-fun add_conjectures_weights [] = I
- | add_conjectures_weights conjs =
- let val (hyps, conj) = split_last conjs in
- add_problem_line_weights conj_weight conj
- #> fold (add_problem_line_weights hyp_weight) hyps
- end
-
-fun add_facts_weights facts =
- let
- val num_facts = length facts
- fun weight_of j =
- fact_min_weight + (fact_max_weight - fact_min_weight) * Real.fromInt j
- / Real.fromInt num_facts
- in
- map weight_of (0 upto num_facts - 1) ~~ facts
- |> fold (uncurry add_problem_line_weights)
- end
-
-(* Weights are from 0.0 (most important) to 1.0 (least important). *)
-fun atp_problem_weights problem =
- let val get = these o AList.lookup (op =) problem in
- Symtab.empty
- |> add_conjectures_weights (get free_typesN @ get conjsN)
- |> add_facts_weights (get factsN)
- |> fold (fold (add_problem_line_weights type_info_default_weight) o get)
- [explicit_declsN, class_relsN, aritiesN]
- |> Symtab.dest
- |> sort (prod_ord Real.compare string_ord o pairself swap)
- end
-
-end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Tue May 31 11:21:47 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Tue May 31 16:38:36 2011 +0200
@@ -7,7 +7,7 @@
signature SLEDGEHAMMER_FILTER =
sig
- datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained
+ type locality = ATP_Translate.locality
type relevance_fudge =
{local_const_multiplier : real,
@@ -39,7 +39,6 @@
val new_monomorphizer : bool Config.T
val ignore_no_atp : bool Config.T
val instantiate_inducts : bool Config.T
- val is_locality_global : locality -> bool
val fact_from_ref :
Proof.context -> unit Symtab.table -> thm list
-> Facts.ref * Attrib.src list -> ((string * locality) * thm) list
@@ -59,6 +58,7 @@
structure Sledgehammer_Filter : SLEDGEHAMMER_FILTER =
struct
+open ATP_Translate
open Sledgehammer_Util
val trace =
@@ -73,14 +73,6 @@
val instantiate_inducts =
Attrib.setup_config_bool @{binding sledgehammer_instantiate_inducts} (K false)
-datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained
-
-(* (quasi-)underapproximation of the truth *)
-fun is_locality_global Local = false
- | is_locality_global Assum = false
- | is_locality_global Chained = false
- | is_locality_global _ = true
-
type relevance_fudge =
{local_const_multiplier : real,
worse_irrel_freq : real,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue May 31 11:21:47 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue May 31 16:38:36 2011 +0200
@@ -21,8 +21,8 @@
struct
open ATP_Systems
+open ATP_Translate
open Sledgehammer_Util
-open Sledgehammer_ATP_Translate
open Sledgehammer_Provers
open Sledgehammer_Minimize
open Sledgehammer_Run
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Tue May 31 11:21:47 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Tue May 31 16:38:36 2011 +0200
@@ -7,8 +7,8 @@
signature SLEDGEHAMMER_MINIMIZE =
sig
- type locality = Sledgehammer_Filter.locality
- type play = Sledgehammer_ATP_Reconstruct.play
+ type locality = ATP_Translate.locality
+ type play = ATP_Reconstruct.play
type params = Sledgehammer_Provers.params
val binary_min_facts : int Config.T
@@ -24,10 +24,12 @@
structure Sledgehammer_Minimize : SLEDGEHAMMER_MINIMIZE =
struct
+open ATP_Util
open ATP_Proof
+open ATP_Translate
+open ATP_Reconstruct
open Sledgehammer_Util
open Sledgehammer_Filter
-open Sledgehammer_ATP_Reconstruct
open Sledgehammer_Provers
(* wrapper for calling external prover *)
@@ -53,7 +55,7 @@
print silent (fn () =>
"Testing " ^ n_facts (map fst facts) ^
(if verbose then " (timeout: " ^ string_from_time timeout ^ ")"
- else "") ^ "...")
+ else "") ^ "...")
val {goal, ...} = Proof.goal state
val params =
{debug = debug, verbose = verbose, overlord = overlord, blocking = true,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue May 31 11:21:47 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue May 31 16:38:36 2011 +0200
@@ -9,12 +9,12 @@
signature SLEDGEHAMMER_PROVERS =
sig
type failure = ATP_Proof.failure
- type locality = Sledgehammer_Filter.locality
+ type locality = ATP_Translate.locality
type relevance_fudge = Sledgehammer_Filter.relevance_fudge
- type translated_formula = Sledgehammer_ATP_Translate.translated_formula
- type type_system = Sledgehammer_ATP_Translate.type_system
- type play = Sledgehammer_ATP_Reconstruct.play
- type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command
+ type translated_formula = ATP_Translate.translated_formula
+ type type_system = ATP_Translate.type_system
+ type play = ATP_Reconstruct.play
+ type minimize_command = ATP_Reconstruct.minimize_command
datatype mode = Auto_Try | Try | Normal | Minimize
@@ -111,14 +111,14 @@
structure Sledgehammer_Provers : SLEDGEHAMMER_PROVERS =
struct
+open ATP_Util
open ATP_Problem
open ATP_Proof
open ATP_Systems
-open Metis_Translate
+open ATP_Translate
+open ATP_Reconstruct
open Sledgehammer_Util
open Sledgehammer_Filter
-open Sledgehammer_ATP_Translate
-open Sledgehammer_ATP_Reconstruct
(** The Sledgehammer **)
@@ -838,8 +838,7 @@
[(22, CantConnect),
(2, NoLibwwwPerl)]
val z3_wrapper_failures =
- [(10, NoRealZ3),
- (11, InternalError),
+ [(11, InternalError),
(12, InternalError),
(13, InternalError)]
val z3_failures =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue May 31 11:21:47 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue May 31 16:38:36 2011 +0200
@@ -8,8 +8,8 @@
signature SLEDGEHAMMER_RUN =
sig
+ type minimize_command = ATP_Reconstruct.minimize_command
type relevance_override = Sledgehammer_Filter.relevance_override
- type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command
type mode = Sledgehammer_Provers.mode
type params = Sledgehammer_Provers.params
type prover = Sledgehammer_Provers.prover
@@ -29,10 +29,11 @@
structure Sledgehammer_Run : SLEDGEHAMMER_RUN =
struct
+open ATP_Util
+open ATP_Translate
+open ATP_Reconstruct
open Sledgehammer_Util
open Sledgehammer_Filter
-open Sledgehammer_ATP_Translate
-open Sledgehammer_ATP_Reconstruct
open Sledgehammer_Provers
open Sledgehammer_Minimize
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue May 31 11:21:47 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue May 31 16:38:36 2011 +0200
@@ -11,26 +11,7 @@
val simplify_spaces : string -> string
val parse_bool_option : bool -> string -> string -> bool option
val parse_time_option : string -> string -> Time.time option
- val string_from_ext_time : bool * Time.time -> string
- val string_from_time : Time.time -> string
- val nat_subscript : int -> string
- val unyxml : string -> string
- val maybe_quote : string -> string
- val typ_of_dtyp :
- Datatype_Aux.descr -> (Datatype_Aux.dtyp * typ) list -> Datatype_Aux.dtyp
- -> typ
- val varify_type : Proof.context -> typ -> typ
- val instantiate_type : theory -> typ -> typ -> typ -> typ
- val varify_and_instantiate_type : Proof.context -> typ -> typ -> typ -> typ
- val is_type_surely_finite : Proof.context -> typ -> bool
- val is_type_surely_infinite : Proof.context -> typ list -> typ -> bool
- val monomorphic_term : Type.tyenv -> term -> term
- val eta_expand : typ list -> term -> int -> term
- val transform_elim_prop : term -> term
- val specialize_type : theory -> (string * typ) -> term -> term
val subgoal_count : Proof.state -> int
- val strip_subgoal :
- Proof.context -> thm -> int -> (string * typ) list * term list * term
val normalize_chained_theorems : thm list -> thm list
val reserved_isar_keyword_table : unit -> unit Symtab.table
end;
@@ -38,10 +19,12 @@
structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
struct
+open ATP_Util
+
fun plural_s n = if n = 1 then "" else "s"
val serial_commas = Try.serial_commas
-val simplify_spaces = ATP_Proof.strip_spaces false (K true)
+val simplify_spaces = strip_spaces false (K true)
fun parse_bool_option option name s =
(case s of
@@ -69,191 +52,8 @@
SOME (seconds (the secs))
end
-fun string_from_ext_time (plus, time) =
- let val ms = Time.toMilliseconds time in
- (if plus then "> " else "") ^
- (if plus andalso ms mod 1000 = 0 then
- signed_string_of_int (ms div 1000) ^ " s"
- else if ms < 1000 then
- signed_string_of_int ms ^ " ms"
- else
- string_of_real (0.01 * Real.fromInt (ms div 10)) ^ " s")
- end
-
-val string_from_time = string_from_ext_time o pair false
-
-val subscript = implode o map (prefix "\<^isub>") o raw_explode (* FIXME Symbol.explode (?) *)
-fun nat_subscript n =
- n |> string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript
-
-val unyxml = XML.content_of o YXML.parse_body
-
-val is_long_identifier = forall Lexicon.is_identifier o space_explode "."
-fun maybe_quote y =
- let val s = unyxml y in
- y |> ((not (is_long_identifier (perhaps (try (unprefix "'")) s)) andalso
- not (is_long_identifier (perhaps (try (unprefix "?")) s))) orelse
- Keyword.is_keyword s) ? quote
- end
-
-fun typ_of_dtyp _ typ_assoc (Datatype_Aux.DtTFree a) =
- the (AList.lookup (op =) typ_assoc (Datatype_Aux.DtTFree a))
- | typ_of_dtyp descr typ_assoc (Datatype_Aux.DtType (s, Us)) =
- Type (s, map (typ_of_dtyp descr typ_assoc) Us)
- | typ_of_dtyp descr typ_assoc (Datatype_Aux.DtRec i) =
- let val (s, ds, _) = the (AList.lookup (op =) descr i) in
- Type (s, map (typ_of_dtyp descr typ_assoc) ds)
- end
-
-fun varify_type ctxt T =
- Variable.polymorphic_types ctxt [Const (@{const_name undefined}, T)]
- |> snd |> the_single |> dest_Const |> snd
-
-(* TODO: use "Term_Subst.instantiateT" instead? *)
-fun instantiate_type thy T1 T1' T2 =
- Same.commit (Envir.subst_type_same
- (Sign.typ_match thy (T1, T1') Vartab.empty)) T2
- handle Type.TYPE_MATCH => raise TYPE ("instantiate_type", [T1, T1'], [])
-
-fun varify_and_instantiate_type ctxt T1 T1' T2 =
- let val thy = Proof_Context.theory_of ctxt in
- instantiate_type thy (varify_type ctxt T1) T1' (varify_type ctxt T2)
- end
-
-fun datatype_constrs thy (T as Type (s, Ts)) =
- (case Datatype.get_info thy s of
- SOME {index, descr, ...} =>
- let val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the in
- map (apsnd (fn Us => map (typ_of_dtyp descr (dtyps ~~ Ts)) Us ---> T))
- constrs
- end
- | NONE => [])
- | datatype_constrs _ _ = []
-
-(* Similar to "Nitpick_HOL.bounded_exact_card_of_type".
- 0 means infinite type, 1 means singleton type (e.g., "unit"), and 2 means
- cardinality 2 or more. The specified default cardinality is returned if the
- cardinality of the type can't be determined. *)
-fun tiny_card_of_type ctxt default_card assigns T =
- let
- val thy = Proof_Context.theory_of ctxt
- val max = 2 (* 1 would be too small for the "fun" case *)
- fun aux slack avoid T =
- if member (op =) avoid T then
- 0
- else case AList.lookup (Sign.typ_instance thy o swap) assigns T of
- SOME k => k
- | NONE =>
- case T of
- Type (@{type_name fun}, [T1, T2]) =>
- (case (aux slack avoid T1, aux slack avoid T2) of
- (k, 1) => if slack andalso k = 0 then 0 else 1
- | (0, _) => 0
- | (_, 0) => 0
- | (k1, k2) =>
- if k1 >= max orelse k2 >= max then max
- else Int.min (max, Integer.pow k2 k1))
- | @{typ prop} => 2
- | @{typ bool} => 2 (* optimization *)
- | @{typ nat} => 0 (* optimization *)
- | @{typ int} => 0 (* optimization *)
- | Type (s, _) =>
- (case datatype_constrs thy T of
- constrs as _ :: _ =>
- let
- val constr_cards =
- map (Integer.prod o map (aux slack (T :: avoid)) o binder_types
- o snd) constrs
- in
- if exists (curry (op =) 0) constr_cards then 0
- else Int.min (max, Integer.sum constr_cards)
- end
- | [] =>
- case Typedef.get_info ctxt s of
- ({abs_type, rep_type, ...}, _) :: _ =>
- (* We cheat here by assuming that typedef types are infinite if
- their underlying type is infinite. This is unsound in general
- but it's hard to think of a realistic example where this would
- not be the case. We are also slack with representation types:
- If a representation type has the form "sigma => tau", we
- consider it enough to check "sigma" for infiniteness. (Look
- for "slack" in this function.) *)
- (case varify_and_instantiate_type ctxt
- (Logic.varifyT_global abs_type) T
- (Logic.varifyT_global rep_type)
- |> aux true avoid of
- 0 => 0
- | 1 => 1
- | _ => default_card)
- | [] => default_card)
- (* Very slightly unsound: Type variables are assumed not to be
- constrained to cardinality 1. (In practice, the user would most
- likely have used "unit" directly anyway.) *)
- | TFree _ => if default_card = 1 then 2 else default_card
- (* Schematic type variables that contain only unproblematic sorts
- (with no finiteness axiom) can safely be considered infinite. *)
- | TVar _ => default_card
- in Int.min (max, aux false [] T) end
-
-fun is_type_surely_finite ctxt T = tiny_card_of_type ctxt 0 [] T <> 0
-fun is_type_surely_infinite ctxt infinite_Ts T =
- tiny_card_of_type ctxt 1 (map (rpair 0) infinite_Ts) T = 0
-
-fun monomorphic_term subst t =
- map_types (map_type_tvar (fn v =>
- case Type.lookup subst v of
- SOME typ => typ
- | NONE => raise TERM ("monomorphic_term: uninstanitated schematic type \
- \variable", [t]))) t
-
-fun eta_expand _ t 0 = t
- | eta_expand Ts (Abs (s, T, t')) n =
- Abs (s, T, eta_expand (T :: Ts) t' (n - 1))
- | eta_expand Ts t n =
- fold_rev (fn T => fn t' => Abs ("x" ^ nat_subscript n, T, t'))
- (List.take (binder_types (fastype_of1 (Ts, t)), n))
- (list_comb (incr_boundvars n t, map Bound (n - 1 downto 0)))
-
-(* Converts an elim-rule into an equivalent theorem that does not have the
- predicate variable. Leaves other theorems unchanged. We simply instantiate
- the conclusion variable to False. (Cf. "transform_elim_theorem" in
- "Meson_Clausify".) *)
-fun transform_elim_prop t =
- case Logic.strip_imp_concl t of
- @{const Trueprop} $ Var (z, @{typ bool}) =>
- subst_Vars [(z, @{const False})] t
- | Var (z, @{typ prop}) => subst_Vars [(z, @{prop False})] t
- | _ => t
-
-fun specialize_type thy (s, T) t =
- let
- fun subst_for (Const (s', T')) =
- if s = s' then
- SOME (Sign.typ_match thy (T', T) Vartab.empty)
- handle Type.TYPE_MATCH => NONE
- else
- NONE
- | subst_for (t1 $ t2) =
- (case subst_for t1 of SOME x => SOME x | NONE => subst_for t2)
- | subst_for (Abs (_, _, t')) = subst_for t'
- | subst_for _ = NONE
- in
- case subst_for t of
- SOME subst => monomorphic_term subst t
- | NONE => raise Type.TYPE_MATCH
- end
-
val subgoal_count = Try.subgoal_count
-fun strip_subgoal ctxt goal i =
- let
- val (t, (frees, params)) =
- Logic.goal_params (prop_of goal) i
- ||> (map dest_Free #> Variable.variant_frees ctxt [] #> `(map Free))
- val hyp_ts = t |> Logic.strip_assums_hyp |> map (curry subst_bounds frees)
- val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees
- in (rev params, hyp_ts, concl_t) end
-
val normalize_chained_theorems =
maps (fn th => insert Thm.eq_thm_prop (zero_var_indexes th) [th])
fun reserved_isar_keyword_table () =
--- a/src/HOL/Tools/refute.ML Tue May 31 11:21:47 2011 +0200
+++ b/src/HOL/Tools/refute.ML Tue May 31 16:38:36 2011 +0200
@@ -393,7 +393,7 @@
(* TRANSLATION HOL -> PROPOSITIONAL LOGIC, BOOLEAN ASSIGNMENT -> MODEL *)
(* ------------------------------------------------------------------------- *)
-val typ_of_dtyp = Sledgehammer_Util.typ_of_dtyp
+val typ_of_dtyp = ATP_Util.typ_of_dtyp
(* ------------------------------------------------------------------------- *)
(* close_form: universal closure over schematic variables in 't' *)
@@ -410,8 +410,8 @@
Term.all T $ Abs (x, T, abstract_over (Var ((x, i), T), t'))) vars t
end;
-val monomorphic_term = Sledgehammer_Util.monomorphic_term
-val specialize_type = Sledgehammer_Util.specialize_type
+val monomorphic_term = ATP_Util.monomorphic_term
+val specialize_type = ATP_Util.specialize_type
(* ------------------------------------------------------------------------- *)
(* is_const_of_class: returns 'true' iff 'Const (s, T)' is a constant that *)