# HG changeset patch # User desharna # Date 1603372688 -7200 # Node ID 4ea19e5dc67e591c7f310baac8643d24c298434d # Parent e728d3a3d383604e64e6cb1910ba97f4ee79d581 Tuned isar_step datatype diff -r e728d3a3d383 -r 4ea19e5dc67e src/HOL/Tools/Sledgehammer/sledgehammer.ML --- 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)) :: _ => diff -r e728d3a3d383 -r 4ea19e5dc67e src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- 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 => diff -r e728d3a3d383 -r 4ea19e5dc67e src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML --- 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 diff -r e728d3a3d383 -r 4ea19e5dc67e src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML --- 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 diff -r e728d3a3d383 -r 4ea19e5dc67e src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML --- 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, ...}) = diff -r e728d3a3d383 -r 4ea19e5dc67e src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML --- 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)