1.1 --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Nov 19 17:07:52 2013 +0100
1.2 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Nov 19 17:12:58 2013 +0100
1.3 @@ -10,6 +10,8 @@
1.4 sig
1.5 type ('a, 'b) atp_term = ('a, 'b) ATP_Problem.atp_term
1.6 type ('a, 'b, 'c, 'd) atp_formula = ('a, 'b, 'c, 'd) ATP_Problem.atp_formula
1.7 + type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step
1.8 + type 'a atp_proof = 'a ATP_Proof.atp_proof
1.9
1.10 val metisN : string
1.11 val full_typesN : string
1.12 @@ -32,6 +34,10 @@
1.13 val prop_of_atp :
1.14 Proof.context -> bool -> int Symtab.table ->
1.15 (string, string, (string, string) atp_term, string) atp_formula -> term
1.16 +
1.17 + val termify_atp_proof :
1.18 + Proof.context -> string Symtab.table -> (string * term) list ->
1.19 + int Symtab.table -> string atp_proof -> (term, string) atp_step list
1.20 end;
1.21
1.22 structure ATP_Proof_Reconstruct : ATP_PROOF_RECONSTRUCT =
1.23 @@ -339,4 +345,80 @@
1.24 | _ => raise ATP_FORMULA [phi]
1.25 in repair_tvar_sorts (do_formula true phi Vartab.empty) end
1.26
1.27 +fun repair_name "$true" = "c_True"
1.28 + | repair_name "$false" = "c_False"
1.29 + | repair_name "$$e" = tptp_equal (* seen in Vampire proofs *)
1.30 + | repair_name s =
1.31 + if is_tptp_equal s orelse
1.32 + (* seen in Vampire proofs *)
1.33 + (String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s) then
1.34 + tptp_equal
1.35 + else
1.36 + s
1.37 +
1.38 +fun infer_formula_types ctxt =
1.39 + Type.constraint HOLogic.boolT
1.40 + #> Syntax.check_term
1.41 + (Proof_Context.set_mode Proof_Context.mode_schematic ctxt)
1.42 +
1.43 +val combinator_table =
1.44 + [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def [abs_def]}),
1.45 + (@{const_name Meson.COMBK}, @{thm Meson.COMBK_def [abs_def]}),
1.46 + (@{const_name Meson.COMBB}, @{thm Meson.COMBB_def [abs_def]}),
1.47 + (@{const_name Meson.COMBC}, @{thm Meson.COMBC_def [abs_def]}),
1.48 + (@{const_name Meson.COMBS}, @{thm Meson.COMBS_def [abs_def]})]
1.49 +
1.50 +fun uncombine_term thy =
1.51 + let
1.52 + fun aux (t1 $ t2) = betapply (pairself aux (t1, t2))
1.53 + | aux (Abs (s, T, t')) = Abs (s, T, aux t')
1.54 + | aux (t as Const (x as (s, _))) =
1.55 + (case AList.lookup (op =) combinator_table s of
1.56 + SOME thm => thm |> prop_of |> specialize_type thy x
1.57 + |> Logic.dest_equals |> snd
1.58 + | NONE => t)
1.59 + | aux t = t
1.60 + in aux end
1.61 +
1.62 +fun unlift_term lifted =
1.63 + map_aterms (fn t as Const (s, _) =>
1.64 + if String.isPrefix lam_lifted_prefix s then
1.65 + case AList.lookup (op =) lifted s of
1.66 + SOME t =>
1.67 + (* FIXME: do something about the types *)
1.68 + unlift_term lifted t
1.69 + | NONE => t
1.70 + else
1.71 + t
1.72 + | t => t)
1.73 +
1.74 +fun decode_line ctxt lifted sym_tab (name, role, u, rule, deps) =
1.75 + let
1.76 + val thy = Proof_Context.theory_of ctxt
1.77 + val t =
1.78 + u |> prop_of_atp ctxt true sym_tab
1.79 + |> uncombine_term thy
1.80 + |> unlift_term lifted
1.81 + |> infer_formula_types ctxt
1.82 + in (name, role, t, rule, deps) end
1.83 +
1.84 +val waldmeister_conjecture_num = "1.0.0.0"
1.85 +
1.86 +fun repair_waldmeister_endgame arg =
1.87 + let
1.88 + fun do_tail (name, _, t, rule, deps) =
1.89 + (name, Negated_Conjecture, s_not t, rule, deps)
1.90 + fun do_body [] = []
1.91 + | do_body ((line as ((num, _), _, _, _, _)) :: lines) =
1.92 + if num = waldmeister_conjecture_num then map do_tail (line :: lines)
1.93 + else line :: do_body lines
1.94 + in do_body arg end
1.95 +
1.96 +fun termify_atp_proof ctxt pool lifted sym_tab =
1.97 + clean_up_atp_proof_dependencies
1.98 + #> nasty_atp_proof pool
1.99 + #> map_term_names_in_atp_proof repair_name
1.100 + #> map (decode_line ctxt lifted sym_tab)
1.101 + #> repair_waldmeister_endgame
1.102 +
1.103 end;
2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Tue Nov 19 17:07:52 2013 +0100
2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Tue Nov 19 17:12:58 2013 +0100
2.3 @@ -24,9 +24,6 @@
2.4 val used_facts_in_unsound_atp_proof :
2.5 Proof.context -> (string * stature) list vector -> 'a atp_proof ->
2.6 string list option
2.7 - val termify_atp_proof :
2.8 - Proof.context -> string Symtab.table -> (string * term) list ->
2.9 - int Symtab.table -> string atp_proof -> (term, string) atp_step list
2.10 val isar_proof_text :
2.11 Proof.context -> bool option -> isar_params -> one_line_params -> string
2.12 val proof_text :
2.13 @@ -187,63 +184,6 @@
2.14 | add_fact_of_dependencies _ names =
2.15 apfst (insert (op =) (label_of_clause names))
2.16
2.17 -fun repair_name "$true" = "c_True"
2.18 - | repair_name "$false" = "c_False"
2.19 - | repair_name "$$e" = tptp_equal (* seen in Vampire proofs *)
2.20 - | repair_name s =
2.21 - if is_tptp_equal s orelse
2.22 - (* seen in Vampire proofs *)
2.23 - (String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s) then
2.24 - tptp_equal
2.25 - else
2.26 - s
2.27 -
2.28 -fun infer_formula_types ctxt =
2.29 - Type.constraint HOLogic.boolT
2.30 - #> Syntax.check_term
2.31 - (Proof_Context.set_mode Proof_Context.mode_schematic ctxt)
2.32 -
2.33 -val combinator_table =
2.34 - [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def [abs_def]}),
2.35 - (@{const_name Meson.COMBK}, @{thm Meson.COMBK_def [abs_def]}),
2.36 - (@{const_name Meson.COMBB}, @{thm Meson.COMBB_def [abs_def]}),
2.37 - (@{const_name Meson.COMBC}, @{thm Meson.COMBC_def [abs_def]}),
2.38 - (@{const_name Meson.COMBS}, @{thm Meson.COMBS_def [abs_def]})]
2.39 -
2.40 -fun uncombine_term thy =
2.41 - let
2.42 - fun aux (t1 $ t2) = betapply (pairself aux (t1, t2))
2.43 - | aux (Abs (s, T, t')) = Abs (s, T, aux t')
2.44 - | aux (t as Const (x as (s, _))) =
2.45 - (case AList.lookup (op =) combinator_table s of
2.46 - SOME thm => thm |> prop_of |> specialize_type thy x
2.47 - |> Logic.dest_equals |> snd
2.48 - | NONE => t)
2.49 - | aux t = t
2.50 - in aux end
2.51 -
2.52 -fun unlift_term lifted =
2.53 - map_aterms (fn t as Const (s, _) =>
2.54 - if String.isPrefix lam_lifted_prefix s then
2.55 - case AList.lookup (op =) lifted s of
2.56 - SOME t =>
2.57 - (* FIXME: do something about the types *)
2.58 - unlift_term lifted t
2.59 - | NONE => t
2.60 - else
2.61 - t
2.62 - | t => t)
2.63 -
2.64 -fun decode_line ctxt lifted sym_tab (name, role, u, rule, deps) =
2.65 - let
2.66 - val thy = Proof_Context.theory_of ctxt
2.67 - val t =
2.68 - u |> prop_of_atp ctxt true sym_tab
2.69 - |> uncombine_term thy
2.70 - |> unlift_term lifted
2.71 - |> infer_formula_types ctxt
2.72 - in (name, role, t, rule, deps) end
2.73 -
2.74 fun replace_one_dependency (old, new) dep =
2.75 if is_same_atp_step dep old then new else [dep]
2.76 fun replace_dependencies_in_line p (name, role, t, rule, deps) =
2.77 @@ -283,18 +223,6 @@
2.78 | (pre, (name', _, _, _, _) :: post) =>
2.79 line :: pre @ map (replace_dependencies_in_line (name', [name])) post
2.80
2.81 -val waldmeister_conjecture_num = "1.0.0.0"
2.82 -
2.83 -fun repair_waldmeister_endgame arg =
2.84 - let
2.85 - fun do_tail (name, _, t, rule, deps) =
2.86 - (name, Negated_Conjecture, s_not t, rule, deps)
2.87 - fun do_body [] = []
2.88 - | do_body ((line as ((num, _), _, _, _, _)) :: lines) =
2.89 - if num = waldmeister_conjecture_num then map do_tail (line :: lines)
2.90 - else line :: do_body lines
2.91 - in do_body arg end
2.92 -
2.93 (* Recursively delete empty lines (type information) from the proof. *)
2.94 fun add_nontrivial_line (line as (name, _, t, _, [])) lines =
2.95 if is_only_type_information t then delete_dependency name lines
2.96 @@ -410,13 +338,6 @@
2.97 and chain_proofs proofs = map (chain_proof) proofs
2.98 in chain_proof end
2.99
2.100 -fun termify_atp_proof ctxt pool lifted sym_tab =
2.101 - clean_up_atp_proof_dependencies
2.102 - #> nasty_atp_proof pool
2.103 - #> map_term_names_in_atp_proof repair_name
2.104 - #> map (decode_line ctxt lifted sym_tab)
2.105 - #> repair_waldmeister_endgame
2.106 -
2.107 type isar_params =
2.108 bool * bool * Time.time option * real * bool * (string * stature) list vector
2.109 * (unit -> (term, string) atp_step list) * thm