--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Oct 21 17:46:51 2020 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Oct 22 15:18:08 2020 +0200
@@ -83,7 +83,15 @@
| try_methss ress (meths :: methss) =
let
fun mk_step fact_names meths =
- Prove ([], [], ("", 0), goal_t, [], ([], fact_names), meths, "")
+ Prove {
+ qualifiers = [],
+ obtains = [],
+ label = ("", 0),
+ goal = goal_t,
+ subproofs = [],
+ facts = ([], fact_names),
+ proof_methods = meths,
+ comment = ""}
in
(case preplay_isar_step ctxt [] timeout [] (mk_step fact_names meths) of
(res as (meth, Played time)) :: _ =>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Oct 21 17:46:51 2020 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Oct 22 15:18:08 2020 +0200
@@ -198,16 +198,24 @@
atp_proof
val assms = map_filter (Option.map fst o get_role (curry (op =) Hypothesis)) atp_proof
- fun add_lemma ((l, t), rule) ctxt =
+ fun add_lemma ((label, goal), rule) ctxt =
let
- val (skos, meths) =
- (if is_skolemize_rule rule then (skolems_of ctxt t, skolem_methods)
+ val (skos, proof_methods) =
+ (if is_skolemize_rule rule then (skolems_of ctxt goal, skolem_methods)
else if is_arith_rule rule then ([], arith_methods)
else ([], rewrite_methods))
||> massage_methods
+ val prove = Prove {
+ qualifiers = [],
+ obtains = skos,
+ label = label,
+ goal = goal,
+ subproofs = [],
+ facts = ([], []),
+ proof_methods = proof_methods,
+ comment = ""}
in
- (Prove ([], skos, l, t, [], ([], []), meths, ""),
- ctxt |> not (null skos) ? (Variable.add_fixes (map fst skos) #> snd))
+ (prove, ctxt |> not (null skos) ? (Variable.add_fixes (map fst skos) #> snd))
end
val (lems, _) =
@@ -239,25 +247,30 @@
atp_proof
fun is_referenced_in_step _ (Let _) = false
- | is_referenced_in_step l (Prove (_, _, _, _, subs, (ls, _), _, _)) =
- member (op =) ls l orelse exists (is_referenced_in_proof l) subs
+ | is_referenced_in_step l (Prove {subproofs, facts = (ls, _), ...}) =
+ member (op =) ls l orelse exists (is_referenced_in_proof l) subproofs
and is_referenced_in_proof l (Proof {steps, ...}) =
exists (is_referenced_in_step l) steps
fun insert_lemma_in_step lem
- (step as Prove (qs, fix, l, t, subs, (ls, gs), meths, comment)) =
+ (step as Prove {qualifiers, obtains, label, goal, subproofs, facts = (ls, gs),
+ proof_methods, comment}) =
let val l' = the (label_of_isar_step lem) in
if member (op =) ls l' then
[lem, step]
else
- let val refs = map (is_referenced_in_proof l') subs in
+ let val refs = map (is_referenced_in_proof l') subproofs in
if length (filter I refs) = 1 then
- let
- val subs' = map2 (fn false => I | true => insert_lemma_in_proof lem) refs
- subs
- in
- [Prove (qs, fix, l, t, subs', (ls, gs), meths, comment)]
- end
+ [Prove {
+ qualifiers = qualifiers,
+ obtains = obtains,
+ label = label,
+ goal = goal,
+ subproofs =
+ map2 (fn false => I | true => insert_lemma_in_proof lem) refs subproofs,
+ facts = (ls, gs),
+ proof_methods = proof_methods,
+ comment = comment}]
else
[lem, step]
end
@@ -295,9 +308,15 @@
accum
|> (if tainted = [] then
(* e.g., trivial, empty proof by Z3 *)
- cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [],
- sort_facts (the_list predecessor, []), massage_methods systematic_methods',
- ""))
+ cons (Prove {
+ qualifiers = if outer then [Show] else [],
+ obtains = [],
+ label = no_label,
+ goal = concl_t,
+ subproofs = [],
+ facts = sort_facts (the_list predecessor, []),
+ proof_methods = massage_methods systematic_methods',
+ comment = ""})
else
I)
|> rev
@@ -318,7 +337,15 @@
else systematic_methods')
|> massage_methods
- fun prove sub facts = Prove (maybe_show outer c, [], l, t, sub, facts, meths, "")
+ fun prove subproofs facts = Prove {
+ qualifiers = maybe_show outer c,
+ obtains = [],
+ label = l,
+ goal = t,
+ subproofs = subproofs,
+ facts = facts,
+ proof_methods = meths,
+ comment = ""}
fun steps_of_rest step = isar_steps outer (SOME l) (step :: accum) infs
in
if is_clause_tainted c then
@@ -339,7 +366,15 @@
(if skolem then
(case skolems_of ctxt t of
[] => prove [] deps
- | skos => Prove ([], skos, l, t, [], deps, meths, ""))
+ | skos => Prove {
+ qualifiers = [],
+ obtains = skos,
+ label = l,
+ goal = t,
+ subproofs = [],
+ facts = deps,
+ proof_methods = meths,
+ comment = ""})
else
prove [] deps)
end
@@ -351,10 +386,15 @@
val l = label_of_clause c
val t = prop_of_clause c
val step =
- Prove (maybe_show outer c, [], l, t,
- map isar_case (filter_out (null o snd) cases),
- sort_facts (the_list predecessor, []), massage_methods systematic_methods',
- "")
+ Prove {
+ qualifiers = maybe_show outer c,
+ obtains = [],
+ label = l,
+ goal = t,
+ subproofs = map isar_case (filter_out (null o snd) cases),
+ facts = sort_facts (the_list predecessor, []),
+ proof_methods = massage_methods systematic_methods',
+ comment = ""}
in
isar_steps outer (SOME l) (step :: accum) infs
end
@@ -424,7 +464,8 @@
one_line_proof_text ctxt 0
(if is_less (play_outcome_ord (play_outcome, one_line_play)) then
(case isar_proof of
- Proof {steps = [Prove (_, _, _, _, _, (_, gfs), meth :: _, _)], ...} =>
+ Proof {steps = [Prove {facts = (_, gfs), proof_methods = meth :: _, ...}],
+ ...} =>
let
val used_facts' =
map_filter (fn s =>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Wed Oct 21 17:46:51 2020 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Thu Oct 22 15:18:08 2020 +0200
@@ -28,10 +28,10 @@
fun collect_steps _ (accum as ([], _)) = accum
| collect_steps [] accum = accum
| collect_steps (step :: steps) accum = collect_steps steps (collect_step step accum)
- and collect_step (step as Prove (_, _, l, _, subproofs, _, _, _)) x =
+ and collect_step (step as Prove {label, subproofs, ...}) x =
(case collect_subproofs subproofs x of
- (accum as ([], _)) => accum
- | accum as (l' :: lbls', accu) => if l = l' then (lbls', step :: accu) else accum)
+ accum as ([], _) => accum
+ | accum as (l' :: lbls', accu) => if label = l' then (lbls', step :: accu) else accum)
| collect_step _ accum = accum
and collect_subproofs [] accum = accum
| collect_subproofs (proof :: subproofs) accum =
@@ -48,15 +48,32 @@
| update_steps steps [] = (steps, [])
| update_steps (step :: steps) updates = update_step step (update_steps steps updates)
and update_step step (steps, []) = (step :: steps, [])
- | update_step (Prove (qs, xs, l, t, subproofs, facts, meths, comment))
- (steps,
- updates as Prove (qs', xs', l', t', subproofs', facts', meths', comment') :: updates') =
+ | update_step (Prove {qualifiers = qs, obtains = xs, label = l, goal = t, subproofs, facts,
+ proof_methods = meths, comment}) (steps, updates as Prove {qualifiers = qs',
+ obtains = xs', label = l', goal = t', subproofs = subproofs', facts = facts',
+ proof_methods = meths', comment = comment'} :: updates') =
(if l = l' then
update_subproofs subproofs' updates'
- |>> (fn subproofs'' => Prove (qs', xs', l', t', subproofs'', facts', meths', comment'))
+ |>> (fn subproofs'' => Prove {
+ qualifiers = qs',
+ obtains = xs',
+ label = l',
+ goal = t',
+ subproofs = subproofs'',
+ facts = facts',
+ proof_methods = meths',
+ comment = comment'})
else
update_subproofs subproofs updates
- |>> (fn subproofs' => Prove (qs, xs, l, t, subproofs', facts, meths, comment)))
+ |>> (fn subproofs' => Prove {
+ qualifiers = qs,
+ obtains = xs,
+ label = l,
+ goal = t,
+ subproofs = subproofs',
+ facts = facts,
+ proof_methods = meths,
+ comment = comment}))
|>> (fn step => step :: steps)
| update_step step (steps, updates) = (step :: steps, updates)
and update_subproofs [] updates = ([], updates)
@@ -87,16 +104,25 @@
(hopeful @ hopeless, hopeless)
end
-fun merge_steps preplay_data (Prove ([], xs1, l1, _, subproofs1, (lfs1, gfs1), meths1, comment1))
- (Prove (qs2, xs2, l2, t, subproofs2, (lfs2, gfs2), meths2, comment2)) =
+fun merge_steps preplay_data
+ (Prove (p1 as {qualifiers = [], label = l1, goal = _, facts = (lfs1, gfs1), ...}))
+ (Prove (p2 as {qualifiers = qs2, label = l2, goal = t, facts = (lfs2, gfs2), ...})) =
let
- val (meths, hopeless) = merge_methods preplay_data (l1, meths1) (l2, meths2)
+ val (meths, hopeless) =
+ merge_methods preplay_data (l1, #proof_methods p1) (l2, #proof_methods p2)
val lfs = union (op =) lfs1 (remove (op =) l1 lfs2)
val gfs = union (op =) gfs1 gfs2
+ val prove = Prove {
+ qualifiers = qs2,
+ obtains = inter (op =) (Term.add_frees t []) (#obtains p1 @ #obtains p2),
+ label = l2,
+ goal = t,
+ subproofs = #subproofs p1 @ #subproofs p2,
+ facts = sort_facts (lfs, gfs),
+ proof_methods = meths,
+ comment = #comment p1 ^ #comment p2}
in
- (Prove (qs2, inter (op =) (Term.add_frees t []) (xs1 @ xs2), l2, t,
- subproofs1 @ subproofs2, sort_facts (lfs, gfs), meths, comment1 ^ comment2),
- hopeless)
+ (prove, hopeless)
end
val merge_slack_time = seconds 0.01
@@ -126,8 +152,8 @@
val (get_successors, replace_successor) =
let
- fun add_refs (Prove (_, _, l, _, _, (lfs, _), _, _)) =
- fold (fn key => Canonical_Label_Tab.cons_list (key, l)) lfs
+ fun add_refs (Prove {label, facts = (lfs, _), ...}) =
+ fold (fn key => Canonical_Label_Tab.cons_list (key, label)) lfs
| add_refs _ = I
val tab =
@@ -154,40 +180,58 @@
| _ => preplay_timeout)
(* elimination of trivial, one-step subproofs *)
- fun elim_one_subproof time (step as Prove (qs, xs, l, t, _, (lfs, gfs), meths, comment)) subs
+ fun elim_one_subproof time (step as Prove {qualifiers, obtains, label, goal,
+ facts = (lfs, gfs), proof_methods, comment, ...}) subs
nontriv_subs =
if null subs orelse not (compress_further ()) then
- Prove (qs, xs, l, t, List.revAppend (nontriv_subs, subs), (lfs, gfs), meths, comment)
+ Prove {
+ qualifiers = qualifiers,
+ obtains = obtains,
+ label = label,
+ goal = goal,
+ subproofs = List.revAppend (nontriv_subs, subs),
+ facts = (lfs, gfs),
+ proof_methods = proof_methods,
+ comment = comment}
else
(case subs of
(sub as Proof {assumptions,
- steps = [Prove (_, _, l', _, [], (lfs', gfs'), meths', _)], ...}) :: subs =>
+ steps = [Prove {label = label', subproofs = [], facts = (lfs', gfs'),
+ proof_methods = proof_methods', ...}], ...}) :: subs =>
let
(* merge steps *)
val subs'' = subs @ nontriv_subs
val lfs'' = union (op =) lfs (subtract (op =) (map fst assumptions) lfs')
val gfs'' = union (op =) gfs' gfs
- val (meths'' as _ :: _, hopeless) =
- merge_methods (!preplay_data) (l', meths') (l, meths)
- val step'' = Prove (qs, xs, l, t, subs'', (lfs'', gfs''), meths'', comment)
+ val (proof_methods'' as _ :: _, hopeless) =
+ merge_methods (!preplay_data) (label', proof_methods') (label, proof_methods)
+ val step'' = Prove {
+ qualifiers = qualifiers,
+ obtains = obtains,
+ label = label,
+ goal = goal,
+ subproofs = subs'',
+ facts = (lfs'', gfs''),
+ proof_methods = proof_methods'',
+ comment = comment}
(* check if the modified step can be preplayed fast enough *)
- val timeout = adjust_merge_timeout preplay_timeout (time + reference_time l')
+ val timeout = adjust_merge_timeout preplay_timeout (time + reference_time label')
in
(case preplay_isar_step ctxt [] timeout hopeless step'' of
meths_outcomes as (_, Played time'') :: _ =>
(* "l'" successfully eliminated *)
(decrement_step_count ();
set_preplay_outcomes_of_isar_step ctxt time'' preplay_data step'' meths_outcomes;
- map (replace_successor l' [l]) lfs';
+ map (replace_successor label' [label]) lfs';
elim_one_subproof time'' step'' subs nontriv_subs)
| _ => elim_one_subproof time step subs (sub :: nontriv_subs))
end
| sub :: subs => elim_one_subproof time step subs (sub :: nontriv_subs))
- fun elim_subproofs (step as Prove (_, _, l, _, subproofs, _, _, _)) =
+ fun elim_subproofs (step as Prove {label, subproofs, ...}) =
if exists (null o tl o steps_of_isar_proof) subproofs then
- elim_one_subproof (reference_time l) step subproofs []
+ elim_one_subproof (reference_time label) step subproofs []
else
step
| elim_subproofs step = step
@@ -205,7 +249,7 @@
fun try_eliminate i l labels steps =
let
- val (steps_before, (cand as Prove (_, _, _, _, _, (lfs, _), _, _)) :: steps_after) =
+ val (steps_before, (cand as Prove {facts = (lfs, _), ...}) :: steps_after) =
chop i steps
val succs = collect_successors steps_after labels
val (succs', hopelesses) = split_list (map (merge_steps (!preplay_data) cand) succs)
@@ -258,7 +302,8 @@
|> compression_loop candidates'
end))
- fun add_cand (Prove (_, xs, l, t, _, _, _, _)) = cons (l, (length xs, size_of_term t))
+ fun add_cand (Prove {obtains, label, goal, ...}) =
+ cons (label, (length obtains, size_of_term goal))
| add_cand _ = I
(* the very last step is not a candidate *)
@@ -283,9 +328,18 @@
steps
|> map (fn step => step |> compress_further () ? compress_sub_levels)
|> compress_further () ? compress_top_level
- and compress_sub_levels (Prove (qs, xs, l, t, subproofs, facts, meths, comment)) =
+ and compress_sub_levels (Prove {qualifiers, obtains, label, goal, subproofs, facts,
+ proof_methods, comment}) =
(* compress subproofs *)
- Prove (qs, xs, l, t, map compress_proof subproofs, facts, meths, comment)
+ Prove {
+ qualifiers = qualifiers,
+ obtains = obtains,
+ label = label,
+ goal = goal,
+ subproofs = map compress_proof subproofs,
+ facts = facts,
+ proof_methods = proof_methods,
+ comment = comment}
(* eliminate trivial subproofs *)
|> compress_further () ? elim_subproofs
| compress_sub_levels step = step
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Wed Oct 21 17:46:51 2020 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Thu Oct 22 15:18:08 2020 +0200
@@ -30,19 +30,36 @@
open Sledgehammer_Isar_Preplay
fun keep_fastest_method_of_isar_step preplay_data
- (Prove (qs, xs, l, t, subproofs, facts, meths, comment)) =
- Prove (qs, xs, l, t, subproofs, facts,
- meths |> List.partition (curry (op =) (fastest_method_of_isar_step preplay_data l)) |> op @,
- comment)
+ (Prove {qualifiers, obtains, label, goal, subproofs, facts, proof_methods, comment}) =
+ Prove {
+ qualifiers = qualifiers,
+ obtains = obtains,
+ label = label,
+ goal = goal,
+ subproofs = subproofs,
+ facts = facts,
+ proof_methods = proof_methods
+ |> List.partition (curry (op =) (fastest_method_of_isar_step preplay_data label))
+ |> op @,
+ comment = comment}
| keep_fastest_method_of_isar_step _ step = step
val slack = seconds 0.025
fun minimized_isar_step ctxt chained time
- (Prove (qs, xs, l, t, subproofs, (lfs0, gfs0), meths as meth :: _, comment)) =
+ (Prove {qualifiers, obtains, label, goal, subproofs, facts = (lfs0, gfs0),
+ proof_methods as meth :: _, comment}) =
let
fun mk_step_lfs_gfs lfs gfs =
- Prove (qs, xs, l, t, subproofs, sort_facts (lfs, gfs), meths, comment)
+ Prove {
+ qualifiers = qualifiers,
+ obtains = obtains,
+ label = label,
+ goal = goal,
+ subproofs = subproofs,
+ facts = sort_facts (lfs, gfs),
+ proof_methods = proof_methods,
+ comment = comment}
fun minimize_half _ min_facts [] time = (min_facts, time)
| minimize_half mk_step min_facts (fact :: facts) time =
@@ -58,7 +75,7 @@
end
fun minimize_isar_step_dependencies ctxt preplay_data
- (step as Prove (_, _, l, _, _, _, meth :: meths, _)) =
+ (step as Prove {label = l, proof_methods = meth :: meths, ...}) =
(case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of
Played time =>
let
@@ -77,9 +94,19 @@
fun postprocess_isar_proof_remove_show_stuttering (proof as Proof {steps, ...}) =
let
fun process_steps [] = []
- | process_steps (steps as [Prove ([], [], _, t1, subs1, facts1, meths1, comment1),
- Prove ([Show], [], l2, t2, _, _, _, comment2)]) =
- if t1 aconv t2 then [Prove ([Show], [], l2, t2, subs1, facts1, meths1, comment1 ^ comment2)]
+ | process_steps (steps as [
+ Prove (p1 as {qualifiers = [], obtains = [], goal = t1, ...}),
+ Prove (p2 as {qualifiers = [Show], obtains = [], goal = t2, ...})]) =
+ if t1 aconv t2 then
+ [Prove {
+ qualifiers = [Show],
+ obtains = [],
+ label = #label p2,
+ goal = t2,
+ subproofs = #subproofs p1,
+ facts = #facts p1,
+ proof_methods = #proof_methods p1,
+ comment = #comment p1 ^ #comment p2}]
else steps
| process_steps (step :: steps) = step :: process_steps steps
in
@@ -105,15 +132,25 @@
else
(used, accu))
and process_used_step step = process_used_step_subproofs (postproc_step step)
- and process_used_step_subproofs (Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths, comment)) =
+ and process_used_step_subproofs (Prove {qualifiers, obtains, label, goal, subproofs,
+ facts = (lfs, gfs), proof_methods, comment}) =
let
- val (used, subproofs) =
+ val (used, subproofs') =
map process_proof subproofs
|> split_list
|>> Ord_List.unions label_ord
|>> fold (Ord_List.insert label_ord) lfs
+ val prove = Prove {
+ qualifiers = qualifiers,
+ obtains = obtains,
+ label = label,
+ goal = goal,
+ subproofs = subproofs',
+ facts = (lfs, gfs),
+ proof_methods = proof_methods,
+ comment = comment}
in
- (used, Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths, comment))
+ (used, prove)
end
in
snd o process_proof
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Wed Oct 21 17:46:51 2020 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Thu Oct 22 15:18:08 2020 +0200
@@ -79,8 +79,8 @@
fun enrich_with_proof (Proof {assumptions, steps = isar_steps, ...}) =
enrich_with_assms assumptions #> fold enrich_with_step isar_steps
- and enrich_with_step (Prove (_, _, l, t, subproofs, _, _, _)) =
- enrich_with_fact l t #> fold enrich_with_proof subproofs
+ and enrich_with_step (Prove {label, goal, subproofs, ...}) =
+ enrich_with_fact label goal #> fold enrich_with_proof subproofs
| enrich_with_step _ = I
in
enrich_with_proof proof ctxt
@@ -115,7 +115,7 @@
val concl =
(case try List.last steps of
- SOME (Prove (_, [], _, t, _, _, _, _)) => t
+ SOME (Prove {obtains = [], goal, ...}) => goal
| _ => raise Fail "preplay error: malformed subproof")
val var_idx = maxidx_of_term concl + 1
@@ -129,11 +129,11 @@
(* may throw exceptions *)
fun raw_preplay_step_for_method ctxt chained timeout meth
- (Prove (_, xs, _, t, subproofs, facts, _, _)) =
+ (Prove {obtains = xs, goal, subproofs, facts, ...}) =
let
val goal =
(case xs of
- [] => t
+ [] => goal
| _ =>
(* proof obligation: !!thesis. (!!x1...xn. t ==> thesis) ==> thesis
(cf. "~~/src/Pure/Isar/obtain.ML") *)
@@ -144,7 +144,7 @@
val thesis_prop = HOLogic.mk_Trueprop thesis
(* !!x1...xn. t ==> thesis *)
- val inner_prop = fold_rev Logic.all frees (Logic.mk_implies (t, thesis_prop))
+ val inner_prop = fold_rev Logic.all frees (Logic.mk_implies (goal, thesis_prop))
in
(* !!thesis. (!!x1...xn. t ==> thesis) ==> thesis *)
Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop))
@@ -195,13 +195,13 @@
Play_Timed_Out (Time.+ (apply2 time_of_play (play1, play2)))
fun set_preplay_outcomes_of_isar_step ctxt timeout preplay_data
- (step as Prove (_, _, l, _, _, _, meths, _)) meths_outcomes0 =
+ (step as Prove {label = l, proof_methods, ...}) meths_outcomes0 =
let
fun lazy_preplay meth =
Lazy.lazy (fn () => preplay_isar_step_for_method ctxt [] timeout meth step)
val meths_outcomes = meths_outcomes0
|> map (apsnd Lazy.value)
- |> fold (fn meth => AList.default (op =) (meth, lazy_preplay meth)) meths
+ |> fold (fn meth => AList.default (op =) (meth, lazy_preplay meth)) proof_methods
in
preplay_data := Canonical_Label_Tab.update (l, fold (AList.update (op =)) meths_outcomes [])
(!preplay_data)
@@ -240,8 +240,8 @@
#> get_best_method_outcome Lazy.force
#> fst
-fun forced_outcome_of_step preplay_data (Prove (_, _, l, _, _, _, meths, _)) =
- Lazy.force (preplay_outcome_of_isar_step_for_method preplay_data l (hd meths))
+fun forced_outcome_of_step preplay_data (Prove {label, proof_methods, ...}) =
+ Lazy.force (preplay_outcome_of_isar_step_for_method preplay_data label (hd proof_methods))
| forced_outcome_of_step _ _ = Played Time.zeroTime
fun preplay_outcome_of_isar_proof preplay_data (Proof {steps, ...}) =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Wed Oct 21 17:46:51 2020 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Thu Oct 22 15:18:08 2020 +0200
@@ -22,9 +22,20 @@
steps : isar_step list
}
and isar_step =
- Let of term * term |
- Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list
- * facts * proof_method list * string
+ Let of {
+ lhs : term,
+ rhs : term
+ } |
+ Prove of {
+ qualifiers : isar_qualifier list,
+ obtains : (string * typ) list,
+ label : label,
+ goal : term,
+ subproofs : isar_proof list,
+ facts : facts,
+ proof_methods : proof_method list,
+ comment : string
+ }
val no_label : label
@@ -34,6 +45,7 @@
val steps_of_isar_proof : isar_proof -> isar_step list
val isar_proof_with_steps : isar_proof -> isar_step list -> isar_proof
+
val label_of_isar_step : isar_step -> label option
val facts_of_isar_step : isar_step -> facts
val proof_methods_of_isar_step : isar_step -> proof_method list
@@ -79,9 +91,20 @@
steps : isar_step list
}
and isar_step =
- Let of term * term |
- Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list
- * facts * proof_method list * string
+ Let of {
+ lhs : term,
+ rhs : term
+ } |
+ Prove of {
+ qualifiers : isar_qualifier list,
+ obtains : (string * typ) list,
+ label : label,
+ goal : term,
+ subproofs : isar_proof list,
+ facts : facts,
+ proof_methods : proof_method list,
+ comment : string
+ }
val no_label = ("", ~1)
@@ -107,16 +130,16 @@
fun isar_proof_with_steps (Proof {fixes, assumptions, ...}) steps =
Proof {fixes = fixes, assumptions = assumptions, steps = steps}
-fun label_of_isar_step (Prove (_, _, l, _, _, _, _, _)) = SOME l
+fun label_of_isar_step (Prove {label, ...}) = SOME label
| label_of_isar_step _ = NONE
-fun subproofs_of_isar_step (Prove (_, _, _, _, subs, _, _, _)) = subs
+fun subproofs_of_isar_step (Prove {subproofs, ...}) = subproofs
| subproofs_of_isar_step _ = []
-fun facts_of_isar_step (Prove (_, _, _, _, _, facts, _, _)) = facts
+fun facts_of_isar_step (Prove {facts, ...}) = facts
| facts_of_isar_step _ = ([], [])
-fun proof_methods_of_isar_step (Prove (_, _, _, _, _, _, meths, _)) = meths
+fun proof_methods_of_isar_step (Prove {proof_methods, ...}) = proof_methods
| proof_methods_of_isar_step _ = []
fun fold_isar_step f step =
@@ -127,8 +150,17 @@
let
fun map_proof (proof as Proof {steps, ...}) = isar_proof_with_steps proof (map map_step steps)
and map_step (step as Let _) = f step
- | map_step (Prove (qs, xs, l, t, subs, facts, meths, comment)) =
- f (Prove (qs, xs, l, t, map map_proof subs, facts, meths, comment))
+ | map_step (Prove {qualifiers, obtains, label, goal, subproofs, facts, proof_methods,
+ comment}) =
+ f (Prove {
+ qualifiers = qualifiers,
+ obtains = obtains,
+ label = label,
+ goal = goal,
+ subproofs = map map_proof subproofs,
+ facts = facts,
+ proof_methods = proof_methods,
+ comment = comment})
in map_proof end
val add_isar_steps = fold_isar_steps (fn Prove _ => Integer.add 1 | _ => I)
@@ -140,8 +172,17 @@
type key = label
val ord = canonical_label_ord)
-fun comment_isar_step comment_of (Prove (qs, xs, l, t, subs, facts, meths, _)) =
- Prove (qs, xs, l, t, subs, facts, meths, comment_of l meths)
+fun comment_isar_step comment_of (Prove {qualifiers, obtains, label, goal, subproofs, facts,
+ proof_methods, ...}) =
+ Prove {
+ qualifiers = qualifiers,
+ obtains = obtains,
+ label = label,
+ goal = goal,
+ subproofs = subproofs,
+ facts = facts,
+ proof_methods = proof_methods,
+ comment = comment_of label proof_methods}
| comment_isar_step _ step = step
fun comment_isar_proof comment_of = map_isar_steps (comment_isar_step comment_of)
@@ -149,9 +190,18 @@
| chain_qs_lfs (SOME l0) lfs =
if member (op =) lfs l0 then ([Then], remove (op =) l0 lfs) else ([], lfs)
-fun chain_isar_step lbl (Prove (qs, xs, l, t, subs, (lfs, gfs), meths, comment)) =
+fun chain_isar_step lbl (Prove {qualifiers, obtains, label, goal, subproofs,
+ facts = (lfs, gfs), proof_methods, comment}) =
let val (qs', lfs) = chain_qs_lfs lbl lfs in
- Prove (qs' @ qs, xs, l, t, map chain_isar_proof subs, (lfs, gfs), meths, comment)
+ Prove {
+ qualifiers = qs' @ qualifiers,
+ obtains = obtains,
+ label = label,
+ goal = goal,
+ subproofs = map chain_isar_proof subproofs,
+ facts = (lfs, gfs),
+ proof_methods = proof_methods,
+ comment = comment}
end
| chain_isar_step _ step = step
and chain_isar_steps _ [] = []
@@ -167,8 +217,17 @@
fun kill_label l = if member (op =) used_ls l then l else no_label
- fun kill_step (Prove (qs, xs, l, t, subs, facts, meths, comment)) =
- Prove (qs, xs, kill_label l, t, map kill_proof subs, facts, meths, comment)
+ fun kill_step (Prove {qualifiers, obtains, label, goal, subproofs, facts, proof_methods,
+ comment}) =
+ Prove {
+ qualifiers = qualifiers,
+ obtains = obtains,
+ label = kill_label label,
+ goal = goal,
+ subproofs = map kill_proof subproofs,
+ facts = facts,
+ proof_methods = proof_methods,
+ comment = comment}
| kill_step step = step
and kill_proof (Proof {fixes, assumptions, steps}) =
let
@@ -186,15 +245,24 @@
fun next_label l (next, subst) =
let val l' = ("", next) in (l', (next + 1, (l, l') :: subst)) end
- fun relabel_step (Prove (qs, fix, l, t, subs, (lfs, gfs), meths, comment))
- (accum as (_, subst)) =
+ fun relabel_step (Prove {qualifiers, obtains, label, goal, subproofs, facts = (lfs, gfs),
+ proof_methods, comment}) (accum as (_, subst)) =
let
val lfs' = maps (the_list o AList.lookup (op =) subst) lfs
val ((subs', l'), accum') = accum
- |> fold_map relabel_proof subs
- ||>> next_label l
+ |> fold_map relabel_proof subproofs
+ ||>> next_label label
+ val prove = Prove {
+ qualifiers = qualifiers,
+ obtains = obtains,
+ label = l',
+ goal = goal,
+ subproofs = subs',
+ facts = (lfs', gfs),
+ proof_methods = proof_methods,
+ comment = comment}
in
- (Prove (qs, fix, l', t, subs', (lfs', gfs), meths, comment), accum')
+ (prove, accum')
end
| relabel_step step accum = (step, accum)
and relabel_proof (Proof {fixes, assumptions, steps}) =
@@ -216,14 +284,21 @@
(l', (next + 1, (l, l') :: subst))
end
- fun relabel_step depth (Prove (qs, xs, l, t, subs, (lfs, gfs), meths, comment))
- (accum as (_, subst)) =
+ fun relabel_step depth (Prove {qualifiers, obtains, label, goal,
+ subproofs, facts = (lfs, gfs), proof_methods, comment}) (accum as (_, subst)) =
let
- val lfs' = maps (the_list o AList.lookup (op =) subst) lfs
- val (l', accum' as (_, subst')) = next_label depth have_prefix l accum
- val subs' = map (relabel_proof subst' (depth + 1)) subs
+ val (l', accum' as (_, subst')) = next_label depth have_prefix label accum
+ val prove = Prove {
+ qualifiers = qualifiers,
+ obtains = obtains,
+ label = l',
+ goal = goal,
+ subproofs = map (relabel_proof subst' (depth + 1)) subproofs,
+ facts = (maps (the_list o AList.lookup (op =) subst) lfs, gfs),
+ proof_methods = proof_methods,
+ comment = comment}
in
- (Prove (qs, xs, l', t, subs', (lfs', gfs), meths, comment), accum')
+ (prove, accum')
end
| relabel_step _ step accum = (step, accum)
and relabel_proof subst depth (Proof {fixes, assumptions, steps}) =
@@ -250,13 +325,21 @@
(ys, ((map Free xs ~~ map Free ys) @ subst, ctxt'))
end
- fun rationalize_step (Prove (qs, xs, l, t, subs, facts, meths, comment)) subst_ctxt =
+ fun rationalize_step (Prove {qualifiers, obtains, label, goal, subproofs, facts, proof_methods,
+ comment}) subst_ctxt =
let
- val (xs', subst_ctxt' as (subst', _)) = rename_obtains xs subst_ctxt
- val t' = subst_atomic subst' t
- val subs' = map (rationalize_proof false subst_ctxt') subs
+ val (obtains', subst_ctxt' as (subst', _)) = rename_obtains obtains subst_ctxt
+ val prove = Prove {
+ qualifiers = qualifiers,
+ obtains = obtains',
+ label = label,
+ goal = subst_atomic subst' goal,
+ subproofs = map (rationalize_proof false subst_ctxt') subproofs,
+ facts = facts,
+ proof_methods = proof_methods,
+ comment = comment}
in
- (Prove (qs, xs', l, t', subs', facts, meths, comment), subst_ctxt')
+ (prove, subst_ctxt')
end
and rationalize_proof outer (subst_ctxt as (subst, ctxt)) (Proof {fixes, assumptions, steps}) =
let
@@ -367,21 +450,24 @@
space_implode (of_moreover ind) (map (of_subproof ind ctxt) subs)
and add_step_pre ind qs subs (s, ctxt) =
(s ^ of_subproofs ind ctxt qs subs ^ of_indent ind, ctxt)
- and add_step ind (Let (t1, t2)) =
+ and add_step ind (Let {lhs = t1, rhs = t2}) =
add_str (of_indent ind ^ "let ") #> add_term t1 #> add_str " = " #> add_term t2
#> add_str "\n"
- | add_step ind (Prove (qs, xs, l, t, subs, (ls, ss), meth :: _, comment)) =
- add_step_pre ind qs subs
- #> (case xs of
- [] => add_str (of_have qs (length subs) ^ " ")
- | _ =>
- add_str (of_obtain qs (length subs) ^ " ")
- #> add_frees xs
- #> add_str (" where\n" ^ of_indent (ind + 1)))
- #> add_str (of_label l)
- #> add_term (if is_thesis ctxt t then HOLogic.mk_Trueprop (Var thesis_var) else t)
- #> add_str ("\n" ^ of_indent (ind + 1) ^ of_method ls ss meth ^
- (if comment = "" then "" else " (* " ^ comment ^ " *)") ^ "\n")
+ | add_step ind (Prove {qualifiers, obtains, label, goal, subproofs, facts = (ls, ss),
+ proof_methods = meth :: _, comment}) =
+ let val num_subproofs = length subproofs in
+ add_step_pre ind qualifiers subproofs
+ #> (case obtains of
+ [] => add_str (of_have qualifiers num_subproofs ^ " ")
+ | _ =>
+ add_str (of_obtain qualifiers num_subproofs ^ " ")
+ #> add_frees obtains
+ #> add_str (" where\n" ^ of_indent (ind + 1)))
+ #> add_str (of_label label)
+ #> add_term (if is_thesis ctxt goal then HOLogic.mk_Trueprop (Var thesis_var) else goal)
+ #> add_str ("\n" ^ of_indent (ind + 1) ^ of_method ls ss meth ^
+ (if comment = "" then "" else " (* " ^ comment ^ " *)") ^ "\n")
+ end
and add_steps ind = fold (add_step ind)
and of_proof ind ctxt (Proof {fixes, assumptions, steps}) =
("", ctxt)