split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
--- a/src/HOL/Sledgehammer.thy Mon Feb 18 12:16:02 2013 +0100
+++ b/src/HOL/Sledgehammer.thy Mon Feb 18 12:16:27 2013 +0100
@@ -19,7 +19,7 @@
ML_file "Tools/Sledgehammer/sledgehammer_annotate.ML"
ML_file "Tools/Sledgehammer/sledgehammer_preplay.ML"
ML_file "Tools/Sledgehammer/sledgehammer_compress.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_reconstruct.ML"
+ML_file "Tools/Sledgehammer/sledgehammer_reconstruct.ML"
ML_file "Tools/Sledgehammer/sledgehammer_provers.ML"
ML_file "Tools/Sledgehammer/sledgehammer_minimize.ML"
ML_file "Tools/Sledgehammer/sledgehammer_mepo.ML"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML Mon Feb 18 12:16:02 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML Mon Feb 18 12:16:27 2013 +0100
@@ -2,7 +2,7 @@
Author: Jasmin Blanchette, TU Muenchen
Author: Steffen Juilf Smolka, TU Muenchen
-Supplement term with explicit type constraints that show up as
+Supplement term with explicit type constraints that show up as
type annotations when printing the term.
*)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Mon Feb 18 12:16:02 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Mon Feb 18 12:16:27 2013 +0100
@@ -7,11 +7,11 @@
signature SLEDGEHAMMER_COMPRESS =
sig
- type isar_step = Sledgehammer_Proof.isar_step
+ type isar_proof = Sledgehammer_Proof.isar_proof
type preplay_time = Sledgehammer_Preplay.preplay_time
val compress_proof :
bool -> Proof.context -> string -> string -> bool -> Time.time option
- -> real -> isar_step list -> isar_step list * (bool * preplay_time)
+ -> real -> isar_proof -> isar_proof * (bool * preplay_time)
end
structure Sledgehammer_Compress : SLEDGEHAMMER_COMPRESS =
@@ -68,38 +68,37 @@
val metis_fail = fn () => !metis_fail
end
- (* compress proof on top level - do not compress subproofs *)
- fun compress_top_level on_top_level ctxt proof =
+ (* compress top level steps - do not compress subproofs *)
+ fun compress_top_level on_top_level ctxt steps =
let
- (* proof vector *)
- val proof_vect = proof |> map SOME |> Vector.fromList
- val n = Vector.length proof_vect
- val n_metis = metis_steps_top_level proof
+ (* proof step vector *)
+ val step_vect = steps |> map SOME |> Vector.fromList
+ val n = Vector.length step_vect
+ val n_metis = add_metis_steps_top_level steps 0
val target_n_metis = Real.fromInt n_metis / isar_compress |> Real.round
- (* table for mapping from (top-level-)label to proof position *)
- fun update_table (i, Assume (l, _)) = Label_Table.update_new (l, i)
+ (* table for mapping from (top-level-)label to step_vect position *)
+ fun update_table (i, Prove (_, l, _, _)) = Label_Table.update_new (l, i)
| update_table (i, Obtain (_, _, l, _, _)) = Label_Table.update_new (l, i)
- | update_table (i, Prove (_, l, _, _)) = Label_Table.update_new (l, i)
| update_table _ = I
- val label_index_table = fold_index update_table proof Label_Table.empty
+ val label_index_table = fold_index update_table steps Label_Table.empty
val lookup_indices = map_filter (Label_Table.lookup label_index_table)
- (* proof references *)
- fun refs (Obtain (_, _, _, _, By_Metis (subproofs, (lfs, _)))) =
- maps (maps refs) subproofs @ lookup_indices lfs
- | refs (Prove (_, _, _, By_Metis (subproofs, (lfs, _)))) =
- maps (maps refs) subproofs @ lookup_indices lfs
- | refs _ = []
+ (* proof step references *)
+ fun refs step =
+ (case byline_of_step step of
+ NONE => []
+ | SOME (By_Metis (subproofs, (lfs, _))) =>
+ maps (steps_of_proof #> maps refs) subproofs @ lookup_indices lfs)
val refed_by_vect =
Vector.tabulate (n, K [])
- |> fold_index (fn (i, step) => fold (update (cons i)) (refs step)) proof
+ |> fold_index (fn (i, step) => fold (update (cons i)) (refs step)) steps
|> Vector.map rev (* after rev, indices are sorted in ascending order *)
(* candidates for elimination, use table as priority queue (greedy
algorithm) *)
- fun add_if_cand proof_vect (i, [j]) =
- (case (the (get i proof_vect), the (get j proof_vect)) of
+ fun add_if_cand step_vect (i, [j]) =
+ (case (the (get i step_vect), the (get j step_vect)) of
(Prove (_, _, t, By_Metis _), Prove (_, _, _, By_Metis _)) =>
cons (Term.size_of_term t, i)
| (Prove (_, _, t, By_Metis _), Obtain (_, _, _, _, By_Metis _)) =>
@@ -107,7 +106,7 @@
| _ => I)
| add_if_cand _ _ = I
val cand_tab =
- v_fold_index (add_if_cand proof_vect) refed_by_vect []
+ v_fold_index (add_if_cand step_vect) refed_by_vect []
|> Inttab.make_list
(* cache metis preplay times in lazy time vector *)
@@ -119,7 +118,7 @@
#> try_metis debug type_enc lam_trans ctxt preplay_timeout
#> handle_metis_fail
#> Lazy.lazy)
- proof_vect
+ step_vect
fun sum_up_time lazy_time_vector =
Vector.foldl
@@ -127,17 +126,16 @@
zero_preplay_time lazy_time_vector
(* Merging *)
- fun merge (Prove (_, label1, _, By_Metis (subproofs1, (lfs1, gfs1))))
- step2 =
+ fun merge (Prove (_, lbl1, _, By_Metis (subproofs1, (lfs1, gfs1)))) step2 =
let
val (step_constructor, (subproofs2, (lfs2, gfs2))) =
(case step2 of
- Prove (qs2, label2, t, By_Metis x) =>
- (fn by => Prove (qs2, label2, t, by), x)
- | Obtain (qs2, xs, label2, t, By_Metis x) =>
- (fn by => Obtain (qs2, xs, label2, t, by), x)
+ Prove (qs2, lbl2, t, By_Metis x) =>
+ (fn by => Prove (qs2, lbl2, t, by), x)
+ | Obtain (qs2, xs, lbl2, t, By_Metis x) =>
+ (fn by => Obtain (qs2, xs, lbl2, t, by), x)
| _ => error "sledgehammer_compress: unmergeable Isar steps" )
- val lfs = remove (op =) label1 lfs2 |> union (op =) lfs1
+ val lfs = remove (op =) lbl1 lfs2 |> union (op =) lfs1
val gfs = union (op =) gfs1 gfs2
val subproofs = subproofs1 @ subproofs2
in step_constructor (By_Metis (subproofs, (lfs, gfs))) end
@@ -166,45 +164,45 @@
end))
- fun merge_steps metis_time proof_vect refed_by cand_tab n' n_metis' =
+ fun merge_steps metis_time step_vect refed_by cand_tab n' n_metis' =
if Inttab.is_empty cand_tab
orelse n_metis' <= target_n_metis
orelse (on_top_level andalso n'<3)
then
(Vector.foldr
- (fn (NONE, proof) => proof | (SOME s, proof) => s :: proof)
- [] proof_vect,
+ (fn (NONE, steps) => steps | (SOME s, steps) => s :: steps)
+ [] step_vect,
sum_up_time metis_time)
else
let
val (i, cand_tab) = pop_max cand_tab
val j = get i refed_by |> the_single
- val s1 = get i proof_vect |> the
- val s2 = get j proof_vect |> the
+ val s1 = get i step_vect |> the
+ val s2 = get j step_vect |> the
in
case try_merge metis_time (s1, i) (s2, j) of
(NONE, metis_time) =>
- merge_steps metis_time proof_vect refed_by cand_tab n' n_metis'
+ merge_steps metis_time step_vect refed_by cand_tab n' n_metis'
| (s, metis_time) =>
let
val refs = refs s1
val refed_by = refed_by |> fold
(update (Ord_List.remove int_ord i #> Ord_List.insert int_ord j)) refs
val new_candidates =
- fold (add_if_cand proof_vect)
+ fold (add_if_cand step_vect)
(map (fn i => (i, get i refed_by)) refs) []
val cand_tab = add_list cand_tab new_candidates
- val proof_vect = proof_vect |> replace NONE i |> replace s j
+ val step_vect = step_vect |> replace NONE i |> replace s j
in
- merge_steps metis_time proof_vect refed_by cand_tab (n' - 1)
+ merge_steps metis_time step_vect refed_by cand_tab (n' - 1)
(n_metis' - 1)
end
end
in
- merge_steps metis_time proof_vect refed_by_vect cand_tab n n_metis
+ merge_steps metis_time step_vect refed_by_vect cand_tab n n_metis
end
- fun do_proof on_top_level ctxt proof =
+ fun do_proof on_top_level ctxt (Proof (fix, assms,steps)) =
let
(* Enrich context with top-level facts *)
val thy = Proof_Context.theory_of ctxt
@@ -212,21 +210,25 @@
fun enrich_with_fact l t =
Proof_Context.put_thms false
(string_for_label l, SOME [Skip_Proof.make_thm thy t])
- fun enrich_with_step (Assume (l, t)) = enrich_with_fact l t
+ fun enrich_with_step (Prove (_, l, t, _)) = enrich_with_fact l t
| enrich_with_step (Obtain (_, _, l, t, _)) = enrich_with_fact l t
- | enrich_with_step (Prove (_, l, t, _)) = enrich_with_fact l t
| enrich_with_step _ = I
- val rich_ctxt = fold enrich_with_step proof ctxt
+ val enrich_with_steps = fold enrich_with_step
+ fun enrich_with_assms (Assume assms) =
+ fold (uncurry enrich_with_fact) assms
+ val rich_ctxt =
+ ctxt |> enrich_with_assms assms |> enrich_with_steps steps
- (* compress subproofs and top-levl proof *)
- val ((proof, top_level_time), lower_level_time) =
- proof |> do_subproofs rich_ctxt
+ (* compress subproofs and top-levl steps *)
+ val ((steps, top_level_time), lower_level_time) =
+ steps |> do_subproofs rich_ctxt
|>> compress_top_level on_top_level rich_ctxt
in
- (proof, add_preplay_time lower_level_time top_level_time)
+ (Proof (fix, assms, steps),
+ add_preplay_time lower_level_time top_level_time)
end
- and do_subproofs ctxt proof =
+ and do_subproofs ctxt subproofs =
let
fun compress_each_and_collect_time compress subproofs =
let fun f_m proof time = compress proof ||> add_preplay_time time
@@ -238,7 +240,7 @@
in (Prove (qs, l, t, By_Metis(subproofs, facts)), time) end
| compress atomic_step = (atomic_step, zero_preplay_time)
in
- compress_each_and_collect_time compress proof
+ compress_each_and_collect_time compress subproofs
end
in
do_proof true ctxt proof
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Mon Feb 18 12:16:02 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Mon Feb 18 12:16:27 2013 +0100
@@ -50,23 +50,25 @@
(* lookup facts in context *)
fun resolve_fact_names ctxt names =
- names
+ (names
|>> map string_for_label
|> op @
- |> maps (thms_of_name ctxt)
+ |> maps (thms_of_name ctxt))
+ handle ERROR msg => error ("preplay error: " ^ msg)
(* *)
fun thm_of_term ctxt = Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
-fun fact_of_subproof ctxt proof =
+fun fact_of_proof ctxt (Proof (Fix fixed_frees, Assume assms, steps)) =
let
- val (fixed_frees, assms, concl) = split_proof proof
+ val concl = (case try List.last steps of
+ SOME (Prove (_, _, t, _)) => t
+ | _ => error "preplay error: malformed subproof")
val var_idx = maxidx_of_term concl + 1
fun var_of_free (x, T) = Var((x, var_idx), T)
val substitutions =
map (`var_of_free #> swap #> apfst Free) fixed_frees
- val assms = assms |> map snd
in
- Logic.list_implies(assms, concl)
+ Logic.list_implies (assms |> map snd, concl)
|> subst_free substitutions
|> thm_of_term ctxt
end
@@ -78,7 +80,7 @@
(case step of
Prove (_, _, t, By_Metis (subproofs, fact_names)) =>
(t, subproofs, fact_names, false)
- | Obtain (_, xs, _, t, By_Metis (subproofs, fact_names)) =>
+ | Obtain (_, Fix xs, _, t, By_Metis (subproofs, fact_names)) =>
(* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis
(see ~~/src/Pure/Isar/obtain.ML) *)
let
@@ -98,7 +100,7 @@
end
| _ => raise ZEROTIME)
val facts =
- map (fact_of_subproof ctxt) subproofs @
+ map (fact_of_proof ctxt) subproofs @
resolve_fact_names ctxt fact_names
val ctxt = ctxt |> Config.put Metis_Tactic.verbose debug
|> obtain ? Config.put Metis_Tactic.new_skolem true
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Mon Feb 18 12:16:02 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Mon Feb 18 12:16:27 2013 +0100
@@ -9,83 +9,84 @@
signature SLEDGEHAMMER_PROOF =
sig
type label = string * int
- val no_label : label
type facts = label list * string list
- val no_facts : facts
datatype isar_qualifier = Show | Then
- datatype isar_step =
- Fix of (string * typ) list |
+ datatype fix = Fix of (string * typ) list
+ datatype assms = Assume of (label * term) list
+
+ datatype isar_proof =
+ Proof of fix * assms * isar_step list
+ and isar_step =
Let of term * term |
- Assume of label * term |
- Obtain of
- isar_qualifier list * (string * typ) list * label * term * byline |
- Prove of isar_qualifier list * label * term * byline
+ Prove of isar_qualifier list * label * term * byline |
+ Obtain of isar_qualifier list * fix * label * term * byline
and byline =
- By_Metis of isar_step list list * facts
+ By_Metis of isar_proof list * facts
+
+ val no_label : label
+ val no_facts : facts
val string_for_label : label -> string
- val metis_steps_top_level : isar_step list -> int
- val metis_steps_total : isar_step list -> int
- val term_of_assm : isar_step -> term
- val term_of_prove : isar_step -> term
- val split_proof :
- isar_step list -> (string * typ) list * (label * term) list * term
+ val fix_of_proof : isar_proof -> fix
+ val assms_of_proof : isar_proof -> assms
+ val steps_of_proof : isar_proof -> isar_step list
+
+ val label_of_step : isar_step -> label option
+ val byline_of_step : isar_step -> byline option
+
+ val add_metis_steps_top_level : isar_step list -> int -> int
+ val add_metis_steps : isar_step list -> int -> int
end
structure Sledgehammer_Proof : SLEDGEHAMMER_PROOF =
struct
type label = string * int
-val no_label = ("", ~1)
type facts = label list * string list
-val no_facts = ([],[])
datatype isar_qualifier = Show | Then
-datatype isar_step =
- Fix of (string * typ) list |
+datatype fix = Fix of (string * typ) list
+datatype assms = Assume of (label * term) list
+
+datatype isar_proof =
+ Proof of fix * assms * isar_step list
+and isar_step =
Let of term * term |
- Assume of label * term |
- Obtain of isar_qualifier list * (string * typ) list * label * term * byline |
- Prove of isar_qualifier list * label * term * byline
+ Prove of isar_qualifier list * label * term * byline |
+ Obtain of isar_qualifier list * fix * label * term * byline
and byline =
- By_Metis of isar_step list list * facts
+ By_Metis of isar_proof list * facts
+
+val no_label = ("", ~1)
+val no_facts = ([],[])
fun string_for_label (s, num) = s ^ string_of_int num
-fun metis_steps_top_level proof =
- fold (fn Obtain _ => Integer.add 1 | Prove _ => Integer.add 1 | _ => I)
- proof 0
-fun metis_steps_total proof =
- let
- fun add_substeps subproofs i =
- Integer.add (fold Integer.add (map metis_steps_total subproofs) i)
- in
- fold
- (fn Obtain (_, _, _, _, By_Metis (subproofs, _)) => add_substeps subproofs 1
- | Prove (_, _, _, By_Metis (subproofs, _)) => add_substeps subproofs 1
- | _ => I)
- proof 0
- end
+fun fix_of_proof (Proof (fix, _, _)) = fix
+fun assms_of_proof (Proof (_, assms, _)) = assms
+fun steps_of_proof (Proof (_, _, steps)) = steps
+(*fun map_steps_of_proof f (Proof (fix, assms, steps)) =
+ Proof(fix, assms, f steps)*)
+
+fun label_of_step (Obtain (_, _, l, _, _)) = SOME l
+ | label_of_step (Prove (_, l, _, _)) = SOME l
+ | label_of_step _ = NONE
-fun term_of_assm (Assume (_, t)) = t
- | term_of_assm _ = error "sledgehammer proof: unexpected constructor"
-fun term_of_prove (Prove (_, _, t, _)) = t
- | term_of_prove _ = error "sledgehammer proof: unexpected constructor"
+fun byline_of_step (Obtain (_, _, _, _, byline)) = SOME byline
+ | byline_of_step (Prove (_, _, _, byline)) = SOME byline
+ | byline_of_step _ = NONE
+
+val add_metis_steps_top_level =
+ fold (byline_of_step #> (fn SOME (By_Metis _) => Integer.add 1 | _ => I))
-fun split_proof proof =
- let
- fun split_step step (fixes, assms, _) =
- (case step of
- Fix xs => (xs@fixes, assms, step)
- | Assume a => (fixes, a::assms, step)
- | _ => (fixes, assms, step))
- val (fixes, assms, concl) =
- fold split_step proof ([], [], Let (Term.dummy, Term.dummy)) (* FIXME: hack *)
- in
- (rev fixes, rev assms, term_of_prove concl)
- end
+fun add_metis_steps steps =
+ fold (byline_of_step
+ #> (fn SOME (By_Metis (subproofs, _)) =>
+ Integer.add 1 #> add_substeps subproofs
+ | _ => I)) steps
+and add_substeps subproofs = fold (steps_of_proof #> add_metis_steps) subproofs
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Mon Feb 18 12:16:02 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Mon Feb 18 12:16:27 2013 +0100
@@ -457,158 +457,190 @@
val indent_size = 2
-fun string_for_proof ctxt type_enc lam_trans i n =
+fun string_for_proof ctxt type_enc lam_trans i n proof =
let
- fun maybe_show qs = if member (op =) qs Show then "show" else "have"
+ val register_fixes = map Free #> fold Variable.auto_fixes
+ fun add_suffix suffix (s, ctxt) = (s ^ suffix, ctxt)
fun of_indent ind = replicate_string (ind * indent_size) " "
- fun of_free (s, T) =
- maybe_quote s ^ " :: " ^
- maybe_quote (simplify_spaces (with_vanilla_print_mode
- (Syntax.string_of_typ ctxt) T))
- val of_frees = space_implode " and " o map of_free
- fun maybe_moreover ind qs nr_subproofs =
- if member (op =) qs Then andalso nr_subproofs > 0
- then of_indent ind ^ "moreover\n"
- else ""
+ fun of_moreover ind = of_indent ind ^ "moreover\n"
fun of_label l = if l = no_label then "" else string_for_label l ^ ": "
- fun of_have qs nr_subproofs =
- if (member (op =) qs Then andalso nr_subproofs>0) orelse (nr_subproofs>1)
- then "ultimately " ^ maybe_show qs
- else
- (if member (op =) qs Then orelse nr_subproofs>0 then
- if member (op =) qs Show then "thus" else "hence"
- else
- maybe_show qs)
- fun of_obtain qs xs =
- (if member (op =) qs Then then "then " else "") ^ "obtain " ^
- of_frees xs ^ " where"
- val of_term =
- annotate_types ctxt
- #> with_vanilla_print_mode (Syntax.string_of_term ctxt)
- #> simplify_spaces
- #> maybe_quote
+ fun of_obtain qs nr =
+ (if nr>1 orelse (nr=1 andalso member (op=) qs Then)
+ then "ultimately "
+ else if nr=1 orelse member (op=) qs Then
+ then "then "
+ else "") ^ "obtain"
+ fun of_show_have qs = if member (op=) qs Show then "show" else "have"
+ fun of_thus_hence qs = if member (op=) qs Show then "thus" else "hence"
+ fun of_prove qs nr =
+ if nr>1 orelse (nr=1 andalso member (op=) qs Then)
+ then "ultimately " ^ of_show_have qs
+ else if nr=1 orelse member (op=) qs Then
+ then of_thus_hence qs
+ else of_show_have qs
+ fun add_term term (s, ctxt)=
+ (s ^ (annotate_types ctxt term
+ |> with_vanilla_print_mode (Syntax.string_of_term ctxt)
+ |> simplify_spaces
+ |> maybe_quote),
+ ctxt |> Variable.auto_fixes term)
val reconstr = Metis (type_enc, lam_trans)
fun of_metis ind options (ls, ss) =
"\n" ^ of_indent (ind + 1) ^ options ^
reconstructor_command reconstr 1 1 [] 0
(ls |> sort_distinct (prod_ord string_ord int_ord),
ss |> sort_distinct string_ord)
- and of_step ind (Fix xs) = of_indent ind ^ "fix " ^ of_frees xs ^ "\n"
- | of_step ind (Let (t1, t2)) =
- of_indent ind ^ "let " ^ of_term t1 ^ " = " ^ of_term t2 ^ "\n"
- | of_step ind (Assume (l, t)) =
- of_indent ind ^ "assume " ^ of_label l ^ of_term t ^ "\n"
- | of_step ind (Obtain (qs, xs, l, t, By_Metis (subproofs, facts))) = (* FIXME *)
- maybe_moreover ind qs (length subproofs) ^
- of_subproofs ind subproofs ^
- of_indent ind ^ of_obtain qs xs ^ " " ^
- of_label l ^ of_term t ^
- (* The new skolemizer puts the arguments in the same order as the ATPs
- (E and Vampire -- but see also "atp_proof_reconstruct.ML" regarding
- Vampire). *)
- of_metis ind "using [[metis_new_skolem]] " facts ^ "\n"
- | of_step ind (Prove (qs, l, t, By_Metis (subproofs, facts))) =
- maybe_moreover ind qs (length subproofs) ^
- of_subproofs ind subproofs ^
- of_prove ind qs (length subproofs) l t facts
- and of_steps prefix suffix ind steps =
- let val s = implode (map (of_step ind) steps) in
+ fun of_free (s, T) =
+ maybe_quote s ^ " :: " ^
+ maybe_quote (simplify_spaces (with_vanilla_print_mode
+ (Syntax.string_of_typ ctxt) T))
+ fun add_frees xs (s, ctxt) =
+ (s ^ space_implode " and " (map of_free xs), ctxt |> register_fixes xs)
+ fun add_fix _ [] = I
+ | add_fix ind xs = add_suffix (of_indent ind ^ "fix ")
+ #> add_frees xs
+ #> add_suffix "\n"
+ fun add_assm ind (l, t) =
+ add_suffix (of_indent ind ^ "assume " ^ of_label l)
+ #> add_term t
+ #> add_suffix "\n"
+ fun add_assms ind assms = fold (add_assm ind) assms
+ fun add_step_post ind l t facts options =
+ add_suffix (of_label l)
+ #> add_term t
+ #> add_suffix (of_metis ind options facts ^ "\n")
+ fun of_subproof ind ctxt proof =
+ let
+ val ind = ind + 1
+ val s = of_proof ind ctxt proof
+ val prefix = "{ "
+ val suffix = " }"
+ 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 of_block ind proof = of_steps "{ " " }" (ind + 1) proof
- and of_subproofs ind subproofs =
- subproofs
- |> map (of_block ind)
- |> space_implode (of_indent ind ^ "moreover\n")
- and of_prove ind qs nr_subproofs l t facts =
- of_indent ind ^ of_have qs nr_subproofs ^ " " ^ of_label l ^ of_term t ^
- of_metis ind "" facts ^ "\n"
+ and of_subproofs _ _ _ [] = ""
+ | of_subproofs ind ctxt qs subproofs =
+ (if member (op=) qs Then then of_moreover ind else "") ^
+ space_implode (of_moreover ind) (map (of_subproof ind ctxt) subproofs)
+ and add_step_pre ind qs subproofs (s, ctxt) =
+ (s ^ of_subproofs ind ctxt qs subproofs ^ of_indent ind, ctxt)
+ and add_step ind (Let (t1, t2)) =
+ add_suffix (of_indent ind ^ "let ")
+ #> add_term t1
+ #> add_suffix " = "
+ #> add_term t2
+ #> add_suffix "\n"
+ | add_step ind (Prove (qs, l, t, By_Metis (subproofs, facts))) =
+ add_step_pre ind qs subproofs
+ #> add_suffix (of_prove qs (length subproofs) ^ " ")
+ #> add_step_post ind l t facts ""
+ | add_step ind (Obtain (qs, Fix xs, l, t,
+ By_Metis (subproofs, facts))) =
+ add_step_pre ind qs subproofs
+ #> add_suffix (of_obtain qs (length subproofs) ^ " ")
+ #> add_frees xs
+ #> add_suffix " where "
+ (* The new skolemizer puts the arguments in the same order as the ATPs
+ (E and Vampire -- but see also "atp_proof_reconstruct.ML" regarding
+ Vampire). *)
+ #> add_step_post ind l t facts "using [[metis_new_skolem]] "
+ and add_steps ind steps =
+ fold (add_step ind) steps
+ and of_proof ind ctxt (Proof (Fix xs, Assume assms, steps)) =
+ ("", ctxt)
+ |> add_fix ind xs
+ |> add_assms ind assms
+ |> add_steps ind steps
+ |> fst
+ in
(* One-step proofs are pointless; better use the Metis one-liner
directly. *)
- and of_proof [Prove (_, _, _, By_Metis ([], _))] = ""
- | of_proof proof =
- (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
- of_indent 0 ^ "proof -\n" ^ of_steps "" "" 1 proof ^ of_indent 0 ^
- (if n <> 1 then "next" else "qed")
- in of_proof end
+ case proof of
+ Proof (Fix [], Assume [], [Prove (_, _, _, By_Metis ([], _))]) => ""
+ | _ => (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
+ of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^
+ of_indent 0 ^ (if n <> 1 then "next" else "qed")
+ end
-fun add_labels_of_step (Obtain (_, _, _, _, By_Metis (subproofs, (ls, _)))) =
- union (op =) (add_labels_of_proofs subproofs ls)
- | add_labels_of_step (Prove (_, _, _, By_Metis (subproofs, (ls, _)))) =
- union (op =) (add_labels_of_proofs subproofs ls)
- | add_labels_of_step _ = I
-and add_labels_of_proof proof = fold add_labels_of_step proof
+fun add_labels_of_step step =
+ (case byline_of_step step of
+ NONE => I
+ | SOME (By_Metis (subproofs, (ls, _))) =>
+ union (op =) (add_labels_of_proofs subproofs ls))
+and add_labels_of_proof proof = fold add_labels_of_step (steps_of_proof proof)
and add_labels_of_proofs proofs = fold add_labels_of_proof proofs
fun kill_useless_labels_in_proof proof =
let
val used_ls = add_labels_of_proof 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 (Obtain (qs, xs, l, t, By_Metis (subproofs, facts))) =
+ fun do_assms (Assume assms) = Assume (map (apfst do_label) assms)
+ fun do_step (Obtain (qs, xs, l, t, By_Metis (subproofs, facts))) =
Obtain (qs, xs, do_label l, t, By_Metis (map do_proof subproofs, facts))
| do_step (Prove (qs, l, t, By_Metis (subproofs, facts))) =
Prove (qs, do_label l, t, By_Metis (map do_proof subproofs, facts))
| do_step step = step
- and do_proof proof = map do_step proof
+ and do_proof (Proof (fix, assms, steps)) =
+ Proof (fix, do_assms assms, map do_step steps)
in do_proof proof end
fun prefix_for_depth n = replicate_string (n + 1)
val relabel_proof =
let
- fun fresh_label depth (old as (l, subst, next_have)) =
+ fun fresh_label depth prefix (old as (l, subst, next)) =
if l = no_label then
old
else
- let val l' = (prefix_for_depth depth have_prefix, next_have) in
- (l', (l, l') :: subst, next_have + 1)
+ let val l' = (prefix_for_depth depth prefix, next) in
+ (l', (l, l') :: subst, next + 1)
end
fun do_facts subst =
apfst (maps (the_list o AList.lookup (op =) subst))
- fun do_byline subst depth nexts (By_Metis (subproofs, facts)) =
- By_Metis
- (map (do_proof subst (depth + 1) (1, 1)) subproofs, do_facts subst facts)
- and do_proof _ _ _ [] = []
- | do_proof subst depth (next_assum, next_have) (Assume (l, t) :: proof) =
- if l = no_label then
- Assume (l, t) :: do_proof subst depth (next_assum, next_have) proof
- else
- let val l' = (prefix_for_depth depth assume_prefix, next_assum) in
- Assume (l', t) ::
- do_proof ((l, l') :: subst) depth (next_assum + 1, next_have) proof
- end
- | do_proof subst depth (nexts as (next_assum, next_have))
- (Obtain (qs, xs, l, t, by) :: proof) =
+ fun do_assm depth (l, t) (subst, next) =
+ let
+ val (l, subst, next) =
+ (l, subst, next) |> fresh_label depth assume_prefix
+ in
+ ((l, t), (subst, next))
+ end
+ fun do_assms subst depth (Assume assms) =
+ fold_map (do_assm depth) assms (subst, 1)
+ |> apfst Assume
+ |> apsnd fst
+ fun do_steps _ _ _ [] = []
+ | do_steps subst depth next (Obtain (qs, xs, l, t, by) :: steps) =
let
- val (l, subst, next_have) = (l, subst, next_have) |> fresh_label depth
- val by = by |> do_byline subst depth nexts
+ val (l, subst, next) =
+ (l, subst, next) |> fresh_label depth have_prefix
+ val by = by |> do_byline subst depth
in
- Obtain (qs, xs, l, t, by) ::
- do_proof subst depth (next_assum, next_have) proof
+ Obtain (qs, xs, l, t, by) :: do_steps subst depth next steps
end
- | do_proof subst depth (nexts as (next_assum, next_have))
- (Prove (qs, l, t, by) :: proof) =
+ | do_steps subst depth next (Prove (qs, l, t, by) :: steps) =
let
- val (l, subst, next_have) = (l, subst, next_have) |> fresh_label depth
- val by = by |> do_byline subst depth nexts
+ val (l, subst, next) =
+ (l, subst, next) |> fresh_label depth have_prefix
+ val by = by |> do_byline subst depth
in
- Prove (qs, l, t, by) ::
- do_proof subst depth (next_assum, next_have) proof
+ Prove (qs, l, t, by) :: do_steps subst depth next steps
end
- | do_proof subst depth nexts (step :: proof) =
- step :: do_proof subst depth nexts proof
- in do_proof [] 0 (1, 1) end
+ | do_steps subst depth next (step :: steps) =
+ step :: do_steps subst depth next steps
+ and do_proof subst depth (Proof (fix, assms, steps)) =
+ let val (assms, subst) = do_assms subst depth assms in
+ Proof (fix, assms, do_steps subst depth 1 steps)
+ end
+ and do_byline subst depth (By_Metis (subproofs, facts)) =
+ By_Metis (do_proofs subst depth subproofs, do_facts subst facts)
+ and do_proofs subst depth = map (do_proof subst (depth + 1))
+ in do_proof [] 0 end
val chain_direct_proof =
let
- fun label_of (Assume (l, _)) = SOME l
- | label_of (Obtain (_, _, l, _, _)) = SOME l
- | label_of (Prove (_, l, _, _)) = SOME l
- | label_of _ = NONE
fun do_qs_lfs NONE lfs = ([], lfs)
| do_qs_lfs (SOME l0) lfs =
if member (op =) lfs l0 then ([Then], lfs |> remove (op =) l0)
@@ -621,16 +653,18 @@
end
| chain_step lbl (Prove (qs, l, t, By_Metis (subproofs, (lfs, gfs)))) =
let val (qs', lfs) = do_qs_lfs lbl lfs in
- Prove (qs' @ qs, l, t,
- By_Metis (chain_proofs subproofs, (lfs, gfs)))
+ Prove (qs' @ qs, l, t, By_Metis (chain_proofs subproofs, (lfs, gfs)))
end
| chain_step _ step = step
- and chain_proof _ [] = []
- | chain_proof (prev as SOME _) (i :: is) =
- chain_step prev i :: chain_proof (label_of i) is
- | chain_proof _ (i :: is) = i :: chain_proof (label_of i) is
- and chain_proofs proofs = map (chain_proof NONE) proofs
- in chain_proof NONE end
+ and chain_steps _ [] = []
+ | chain_steps (prev as SOME _) (i :: is) =
+ chain_step prev i :: chain_steps (label_of_step i) is
+ | chain_steps _ (i :: is) = i :: chain_steps (label_of_step i) is
+ and chain_proof (Proof (fix, Assume assms, steps)) =
+ Proof (fix, Assume assms,
+ chain_steps (try (List.last #> fst) assms) steps)
+ and chain_proofs proofs = map (chain_proof) proofs
+ in chain_proof end
type isar_params =
bool * bool * Time.time option * real * string Symtab.table
@@ -676,7 +710,7 @@
(case resolve_conjecture ss of
[j] =>
if j = length hyp_ts then NONE
- else SOME (Assume (raw_label_for_name name, nth hyp_ts j))
+ else SOME (raw_label_for_name name, nth hyp_ts j)
| _ => NONE)
| _ => NONE)
fun dep_of_step (Definition_Step _) = NONE
@@ -691,7 +725,7 @@
val steps =
Symtab.empty
|> fold (fn Definition_Step _ => I (* FIXME *)
- | Inference_Step (name as (s, ss), role, t, rule, _) =>
+ | Inference_Step (name as (s, _), role, t, rule, _) =>
Symtab.update_new (s, (rule,
t |> (if is_clause_tainted [name] then
s_maybe_not role
@@ -705,7 +739,7 @@
| is_clause_skolemize_rule _ = false
(* The assumptions and conjecture are "prop"s; the other formulas are
"bool"s. *)
- fun prop_of_clause [name as (s, ss)] =
+ fun prop_of_clause [(s, ss)] =
(case resolve_conjecture ss of
[j] => if j = length hyp_ts then concl_t else nth hyp_ts j
| _ => the_default ("", @{term False}) (Symtab.lookup steps s)
@@ -722,22 +756,16 @@
| _ => fold (curry s_disj) lits @{term False}
end
|> HOLogic.mk_Trueprop |> close_form
- fun isar_proof_of_direct_proof outer predecessor accum [] =
- rev accum |> outer ? (append assms
- #> not (null params) ? cons (Fix params))
- | isar_proof_of_direct_proof outer predecessor accum (inf :: infs) =
- let
- fun maybe_show outer c =
- (outer andalso length c = 1 andalso subset (op =) (c, conjs))
- ? cons Show
- fun do_rest lbl step =
- isar_proof_of_direct_proof outer lbl (step :: accum) infs
- val is_fixed = Variable.is_declared ctxt orf can Name.dest_skolem
- fun skolems_of t =
- Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev
- in
- case inf of
- Have (gamma, c) =>
+ fun isar_proof_of_direct_proof infs =
+ let
+ fun maybe_show outer c =
+ (outer andalso length c = 1 andalso subset (op =) (c, conjs))
+ ? cons Show
+ val is_fixed = Variable.is_declared ctxt orf can Name.dest_skolem
+ fun skolems_of t =
+ Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev
+ fun do_steps _ _ accum [] = rev accum
+ | do_steps outer _ accum (Have (gamma, c) :: infs) =
let
val l = label_of_clause c
val t = prop_of_clause c
@@ -745,7 +773,9 @@
By_Metis ([],
(fold (add_fact_from_dependencies fact_names)
gamma no_facts))
- fun prove outer = Prove (maybe_show outer c [], l, t, by)
+ fun prove by = Prove (maybe_show outer c [], l, t, by)
+ fun do_rest lbl step =
+ do_steps outer (SOME lbl) (step :: accum) infs
in
if is_clause_tainted c then
case gamma of
@@ -754,36 +784,40 @@
is_clause_tainted g then
let
val subproof =
- Fix (skolems_of (prop_of_clause g)) :: rev accum
+ Proof (Fix (skolems_of (prop_of_clause g)),
+ Assume [], rev accum)
in
- isar_proof_of_direct_proof outer l
- [Prove (maybe_show outer c [],
- label_of_clause c, prop_of_clause c,
- By_Metis ([subproof], no_facts))] []
+ do_steps outer (SOME l)
+ [prove (By_Metis ([subproof], no_facts))] []
end
else
- do_rest l (prove outer)
- | _ => do_rest l (prove outer)
+ do_rest l (prove by)
+ | _ => do_rest l (prove by)
else
if is_clause_skolemize_rule c then
- do_rest l (Obtain ([], skolems_of t, l, t, by))
+ do_rest l (Obtain ([], Fix (skolems_of t), l, t, by))
else
- do_rest l (prove outer)
+ do_rest l (prove by)
end
- | Cases cases =>
+ | do_steps outer predecessor accum (Cases cases :: infs) =
let
fun do_case (c, infs) =
- Assume (label_of_clause c, prop_of_clause c) ::
- isar_proof_of_direct_proof false no_label [] infs
+ do_proof false [] [(label_of_clause c, prop_of_clause c)] infs
val c = succedent_of_cases cases
val l = label_of_clause c
+ val t = prop_of_clause c
+ val step =
+ (Prove (maybe_show outer c [], l, t, By_Metis
+ (map do_case cases, (the_list predecessor, []))))
in
- do_rest l
- (Prove (maybe_show outer c [],
- l, prop_of_clause c,
- By_Metis (map do_case cases, ([predecessor], []))))
+ do_steps outer (SOME l) (step :: accum) infs
end
- end
+ and do_proof outer fix assms infs =
+ Proof (Fix fix, Assume assms, do_steps outer NONE [] infs)
+ in
+ do_proof true params assms infs
+ end
+
val cleanup_labels_in_proof =
chain_direct_proof
#> kill_useless_labels_in_proof
@@ -791,7 +825,7 @@
val (isar_proof, (preplay_fail, preplay_time)) =
refute_graph
|> redirect_graph axioms tainted bot
- |> isar_proof_of_direct_proof true no_label []
+ |> isar_proof_of_direct_proof
|> (if not preplay andalso isar_compress <= 1.0 then
rpair (false, (true, seconds 0.0))
else
@@ -818,9 +852,11 @@
else
[]) @
(if verbose then
- let val num_steps = metis_steps_total isar_proof in
- [string_of_int num_steps ^ " step" ^ plural_s num_steps]
- end
+ let
+ val num_steps = add_metis_steps (steps_of_proof isar_proof) 0
+ in
+ [string_of_int num_steps ^ " step" ^ plural_s num_steps]
+ end
else
[])
in