# HG changeset patch # User wenzelm # Date 1468622313 -7200 # Node ID 9f8d06f23c09828e4317c83a04a58580836118d2 # Parent 1c7b1e294fb5fd47494b99aac6efef8366b65a6f information about proof outline with cases (sendback); diff -r 1c7b1e294fb5 -r 9f8d06f23c09 NEWS --- a/NEWS Sat Jul 16 00:11:03 2016 +0200 +++ b/NEWS Sat Jul 16 00:38:33 2016 +0200 @@ -100,6 +100,9 @@ established at the end of a proof are properly identified in the theorem statement. +* Command 'proof' provides information about proof outline with cases, +e.g. for proof methods "cases", "induct", "goal_cases". + *** Isar *** diff -r 1c7b1e294fb5 -r 9f8d06f23c09 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Sat Jul 16 00:11:03 2016 +0200 +++ b/src/Pure/Isar/proof_context.ML Sat Jul 16 00:38:33 2016 +0200 @@ -144,7 +144,7 @@ val add_assms_cmd: Assumption.export -> (Thm.binding * (string * string list) list) list -> Proof.context -> (string * thm list) list * Proof.context - val dest_cases: Proof.context -> (string * (Rule_Cases.T * {legacy: bool})) list + val dest_cases: Proof.context option -> Proof.context -> (string * (Rule_Cases.T * {legacy: bool})) list val update_cases: (string * Rule_Cases.T option) list -> Proof.context -> Proof.context val update_cases_legacy: (string * Rule_Cases.T option) list -> Proof.context -> Proof.context val apply_case: Rule_Cases.T -> Proof.context -> (string * term list) list * Proof.context @@ -188,6 +188,7 @@ val pretty_local_facts: bool -> Proof.context -> Pretty.T list val print_local_facts: bool -> Proof.context -> unit val pretty_cases: Proof.context -> Pretty.T list + val print_cases_proof: Proof.context -> Proof.context -> string val debug: bool Config.T val verbose: bool Config.T val pretty_ctxt: Proof.context -> Pretty.T list @@ -1272,9 +1273,18 @@ (** cases **) -fun dest_cases ctxt = - Name_Space.fold_table (fn (a, (c, i)) => cons (i, (a, c))) (cases_of ctxt) [] - |> sort (int_ord o apply2 #1) |> map #2; +fun dest_cases prev_ctxt ctxt = + let + val ignored = + (case prev_ctxt of + NONE => Inttab.empty + | SOME ctxt0 => + Name_Space.fold_table (Inttab.insert_set o #2 o #2) (cases_of ctxt0) Inttab.empty); + in + Name_Space.fold_table (fn (a, (c, i)) => + not (Inttab.defined ignored i) ? cons (i, (a, c))) (cases_of ctxt) [] + |> sort (int_ord o apply2 #1) |> map #2 + end; local @@ -1469,7 +1479,7 @@ Pretty.writeln_chunks (pretty_local_facts verbose ctxt); -(* local contexts *) +(* named local contexts *) local @@ -1508,7 +1518,7 @@ fun mk_case (_, (_, {legacy = true})) = NONE | mk_case (name, (c as Rule_Cases.Case {fixes, ...}, {legacy = false})) = SOME (name, (fixes, case_result c ctxt)); - val cases = dest_cases ctxt |> map_filter mk_case; + val cases = dest_cases NONE ctxt |> map_filter mk_case; in if null cases then [] else [Pretty.big_list "cases:" (map pretty_case cases)] @@ -1516,6 +1526,34 @@ end; +fun print_cases_proof ctxt0 ctxt = + let + fun print_case name [] = name + | print_case name xs = enclose "(" ")" (space_implode " " (name :: map Name.clean xs)); + + fun print_proof (name, (Rule_Cases.Case {fixes, binds, ...}, {legacy})) = + if legacy then NONE + else + let + val concl = + if exists (fn ((x, _), SOME t) => + x = Rule_Cases.case_conclN andalso Term.maxidx_of_term t = ~1 | _ => false) binds + then Rule_Cases.case_conclN + else Auto_Bind.thesisN; + in + SOME (cat_lines + [" case " ^ print_case name (map (Name.clean o Binding.name_of o #1) fixes), + " then show ?" ^ concl ^ " sorry"]) + end; + in + (case map_filter print_proof (dest_cases (SOME ctxt0) ctxt) of + [] => "" + | proofs => + "Proof outline with cases:\n" ^ + Active.sendback_markup [Markup.padding_command] + (space_implode "\nnext\n" proofs ^ "\nqed")) + end; + (* core context *) diff -r 1c7b1e294fb5 -r 9f8d06f23c09 src/Pure/Pure.thy --- a/src/Pure/Pure.thy Sat Jul 16 00:11:03 2016 +0200 +++ b/src/Pure/Pure.thy Sat Jul 16 00:38:33 2016 +0200 @@ -902,7 +902,14 @@ val _ = Outer_Syntax.command @{command_keyword proof} "backward proof step" (Scan.option Method.parse >> (fn m => - (Option.map Method.report m; Toplevel.proof (Proof.proof m #> Seq.the_result "")))); + (Option.map Method.report m; + Toplevel.proof (fn state => + let + val state' = state |> Proof.proof m |> Seq.the_result ""; + val _ = + Output.information + (Proof_Context.print_cases_proof (Proof.context_of state) (Proof.context_of state')); + in state' end)))) in end\