information about proof outline with cases (sendback);
authorwenzelm
Sat Jul 16 00:38:33 2016 +0200 (2016-07-16)
changeset 635139f8d06f23c09
parent 63512 1c7b1e294fb5
child 63514 d4d3df24f536
information about proof outline with cases (sendback);
NEWS
src/Pure/Isar/proof_context.ML
src/Pure/Pure.thy
     1.1 --- a/NEWS	Sat Jul 16 00:11:03 2016 +0200
     1.2 +++ b/NEWS	Sat Jul 16 00:38:33 2016 +0200
     1.3 @@ -100,6 +100,9 @@
     1.4  established at the end of a proof are properly identified in the theorem
     1.5  statement.
     1.6  
     1.7 +* Command 'proof' provides information about proof outline with cases,
     1.8 +e.g. for proof methods "cases", "induct", "goal_cases".
     1.9 +
    1.10  
    1.11  *** Isar ***
    1.12  
     2.1 --- a/src/Pure/Isar/proof_context.ML	Sat Jul 16 00:11:03 2016 +0200
     2.2 +++ b/src/Pure/Isar/proof_context.ML	Sat Jul 16 00:38:33 2016 +0200
     2.3 @@ -144,7 +144,7 @@
     2.4    val add_assms_cmd: Assumption.export ->
     2.5      (Thm.binding * (string * string list) list) list ->
     2.6      Proof.context -> (string * thm list) list * Proof.context
     2.7 -  val dest_cases: Proof.context -> (string * (Rule_Cases.T * {legacy: bool})) list
     2.8 +  val dest_cases: Proof.context option -> Proof.context -> (string * (Rule_Cases.T * {legacy: bool})) list
     2.9    val update_cases: (string * Rule_Cases.T option) list -> Proof.context -> Proof.context
    2.10    val update_cases_legacy: (string * Rule_Cases.T option) list -> Proof.context -> Proof.context
    2.11    val apply_case: Rule_Cases.T -> Proof.context -> (string * term list) list * Proof.context
    2.12 @@ -188,6 +188,7 @@
    2.13    val pretty_local_facts: bool -> Proof.context -> Pretty.T list
    2.14    val print_local_facts: bool -> Proof.context -> unit
    2.15    val pretty_cases: Proof.context -> Pretty.T list
    2.16 +  val print_cases_proof: Proof.context -> Proof.context -> string
    2.17    val debug: bool Config.T
    2.18    val verbose: bool Config.T
    2.19    val pretty_ctxt: Proof.context -> Pretty.T list
    2.20 @@ -1272,9 +1273,18 @@
    2.21  
    2.22  (** cases **)
    2.23  
    2.24 -fun dest_cases ctxt =
    2.25 -  Name_Space.fold_table (fn (a, (c, i)) => cons (i, (a, c))) (cases_of ctxt) []
    2.26 -  |> sort (int_ord o apply2 #1) |> map #2;
    2.27 +fun dest_cases prev_ctxt ctxt =
    2.28 +  let
    2.29 +    val ignored =
    2.30 +      (case prev_ctxt of
    2.31 +        NONE => Inttab.empty
    2.32 +      | SOME ctxt0 =>
    2.33 +          Name_Space.fold_table (Inttab.insert_set o #2 o #2) (cases_of ctxt0) Inttab.empty);
    2.34 +  in
    2.35 +    Name_Space.fold_table (fn (a, (c, i)) =>
    2.36 +      not (Inttab.defined ignored i) ? cons (i, (a, c))) (cases_of ctxt) []
    2.37 +    |> sort (int_ord o apply2 #1) |> map #2
    2.38 +  end;
    2.39  
    2.40  local
    2.41  
    2.42 @@ -1469,7 +1479,7 @@
    2.43    Pretty.writeln_chunks (pretty_local_facts verbose ctxt);
    2.44  
    2.45  
    2.46 -(* local contexts *)
    2.47 +(* named local contexts *)
    2.48  
    2.49  local
    2.50  
    2.51 @@ -1508,7 +1518,7 @@
    2.52      fun mk_case (_, (_, {legacy = true})) = NONE
    2.53        | mk_case (name, (c as Rule_Cases.Case {fixes, ...}, {legacy = false})) =
    2.54            SOME (name, (fixes, case_result c ctxt));
    2.55 -    val cases = dest_cases ctxt |> map_filter mk_case;
    2.56 +    val cases = dest_cases NONE ctxt |> map_filter mk_case;
    2.57    in
    2.58      if null cases then []
    2.59      else [Pretty.big_list "cases:" (map pretty_case cases)]
    2.60 @@ -1516,6 +1526,34 @@
    2.61  
    2.62  end;
    2.63  
    2.64 +fun print_cases_proof ctxt0 ctxt =
    2.65 +  let
    2.66 +    fun print_case name [] = name
    2.67 +      | print_case name xs = enclose "(" ")" (space_implode " " (name :: map Name.clean xs));
    2.68 +
    2.69 +    fun print_proof (name, (Rule_Cases.Case {fixes, binds, ...}, {legacy})) =
    2.70 +      if legacy then NONE
    2.71 +      else
    2.72 +        let
    2.73 +          val concl =
    2.74 +            if exists (fn ((x, _), SOME t) =>
    2.75 +              x = Rule_Cases.case_conclN andalso Term.maxidx_of_term t = ~1 | _ => false) binds
    2.76 +            then Rule_Cases.case_conclN
    2.77 +            else Auto_Bind.thesisN;
    2.78 +        in
    2.79 +          SOME (cat_lines
    2.80 +            ["  case " ^ print_case name (map (Name.clean o Binding.name_of o #1) fixes),
    2.81 +             "  then show ?" ^ concl ^ " sorry"])
    2.82 +        end;
    2.83 +  in
    2.84 +    (case map_filter print_proof (dest_cases (SOME ctxt0) ctxt) of
    2.85 +      [] => ""
    2.86 +    | proofs =>
    2.87 +        "Proof outline with cases:\n" ^
    2.88 +        Active.sendback_markup [Markup.padding_command]
    2.89 +          (space_implode "\nnext\n" proofs ^ "\nqed"))
    2.90 +  end;
    2.91 +
    2.92  
    2.93  (* core context *)
    2.94  
     3.1 --- a/src/Pure/Pure.thy	Sat Jul 16 00:11:03 2016 +0200
     3.2 +++ b/src/Pure/Pure.thy	Sat Jul 16 00:38:33 2016 +0200
     3.3 @@ -902,7 +902,14 @@
     3.4  val _ =
     3.5    Outer_Syntax.command @{command_keyword proof} "backward proof step"
     3.6      (Scan.option Method.parse >> (fn m =>
     3.7 -      (Option.map Method.report m; Toplevel.proof (Proof.proof m #> Seq.the_result ""))));
     3.8 +      (Option.map Method.report m;
     3.9 +       Toplevel.proof (fn state =>
    3.10 +         let
    3.11 +          val state' = state |> Proof.proof m |> Seq.the_result "";
    3.12 +          val _ =
    3.13 +            Output.information
    3.14 +              (Proof_Context.print_cases_proof (Proof.context_of state) (Proof.context_of state'));
    3.15 +        in state' end))))
    3.16  
    3.17  in end\<close>
    3.18