discontinued old-style goal cases;
authorwenzelm
Sun Sep 23 21:49:31 2018 +0200 (13 months ago ago)
changeset 690458c240fdeffcb
parent 69044 364c989edb49
child 69046 5840724b1d71
child 69048 587d0b8a7609
child 69109 697789794af1
discontinued old-style goal cases;
NEWS
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_context.ML
     1.1 --- a/NEWS	Sun Sep 23 21:38:30 2018 +0200
     1.2 +++ b/NEWS	Sun Sep 23 21:49:31 2018 +0200
     1.3 @@ -18,6 +18,10 @@
     1.4  * More robust treatment of structural errors: begin/end blocks take
     1.5  precedence over goal/proof.
     1.6  
     1.7 +* Implicit cases goal1, goal2, goal3, etc. have been discontinued
     1.8 +(legacy feature since Isabelle2016).
     1.9 +
    1.10 +
    1.11  
    1.12  *** HOL ***
    1.13  
     2.1 --- a/src/Pure/Isar/proof.ML	Sun Sep 23 21:38:30 2018 +0200
     2.2 +++ b/src/Pure/Isar/proof.ML	Sun Sep 23 21:49:31 2018 +0200
     2.3 @@ -415,24 +415,11 @@
     2.4  
     2.5  local
     2.6  
     2.7 -fun goalN i = "goal" ^ string_of_int i;
     2.8 -fun goals st = map goalN (1 upto Thm.nprems_of st);
     2.9 -
    2.10 -fun no_goal_cases st = map (rpair NONE) (goals st);
    2.11 -
    2.12 -fun goal_cases ctxt st =
    2.13 -  Rule_Cases.make_common ctxt (Thm.prop_of st) (map (rpair [] o rpair []) (goals st));
    2.14 -
    2.15  fun apply_method text ctxt state =
    2.16    find_goal state |> (fn (goal_ctxt, {statement, using, goal, before_qed, after_qed}) =>
    2.17      Method.evaluate text ctxt using (goal_ctxt, goal)
    2.18      |> Seq.map_result (fn (goal_ctxt', goal') =>
    2.19 -      let
    2.20 -        val goal_ctxt'' = goal_ctxt'
    2.21 -          |> Proof_Context.update_cases_legacy (no_goal_cases goal @ goal_cases ctxt goal');
    2.22 -        val state' = state
    2.23 -          |> map_goal (K (goal_ctxt'', statement, using, goal', before_qed, after_qed));
    2.24 -      in state' end));
    2.25 +        state |> map_goal (K (goal_ctxt', statement, using, goal', before_qed, after_qed))));
    2.26  
    2.27  in
    2.28  
     3.1 --- a/src/Pure/Isar/proof_context.ML	Sun Sep 23 21:38:30 2018 +0200
     3.2 +++ b/src/Pure/Isar/proof_context.ML	Sun Sep 23 21:49:31 2018 +0200
     3.3 @@ -151,9 +151,8 @@
     3.4    val add_assms_cmd: Assumption.export ->
     3.5      (Thm.binding * (string * string list) list) list ->
     3.6      Proof.context -> (string * thm list) list * Proof.context
     3.7 -  val dest_cases: Proof.context option -> Proof.context -> (string * (Rule_Cases.T * {legacy: bool})) list
     3.8 +  val dest_cases: Proof.context option -> Proof.context -> (string * Rule_Cases.T) list
     3.9    val update_cases: (string * Rule_Cases.T option) list -> Proof.context -> Proof.context
    3.10 -  val update_cases_legacy: (string * Rule_Cases.T option) list -> Proof.context -> Proof.context
    3.11    val apply_case: Rule_Cases.T -> Proof.context -> (string * term list) list * Proof.context
    3.12    val check_case: Proof.context -> bool ->
    3.13      string * Position.T -> binding option list -> Rule_Cases.T
    3.14 @@ -228,7 +227,7 @@
    3.15  
    3.16  (** Isar proof context information **)
    3.17  
    3.18 -type cases = (Rule_Cases.T * {legacy: bool}) Name_Space.table;
    3.19 +type cases = Rule_Cases.T Name_Space.table;
    3.20  val empty_cases: cases = Name_Space.empty_table Markup.caseN;
    3.21  
    3.22  datatype data =
    3.23 @@ -238,7 +237,7 @@
    3.24      tsig: Type.tsig * Type.tsig, (*local/global type signature -- local name space / defsort only*)
    3.25      consts: Consts.T * Consts.T, (*local/global consts -- local name space / abbrevs only*)
    3.26      facts: Facts.T,              (*local facts, based on initial global facts*)
    3.27 -    cases: cases};               (*named case contexts: case, legacy, running index*)
    3.28 +    cases: cases};               (*named case contexts*)
    3.29  
    3.30  fun make_data (mode, syntax, tsig, consts, facts, cases) =
    3.31    Data {mode = mode, syntax = syntax, tsig = tsig, consts = consts, facts = facts, cases = cases};
    3.32 @@ -1319,17 +1318,10 @@
    3.33  fun drop_schematic (b as (xi, SOME t)) = if Term.exists_subterm is_Var t then (xi, NONE) else b
    3.34    | drop_schematic b = b;
    3.35  
    3.36 -fun update_case _ _ ("", _) cases = cases
    3.37 -  | update_case _ _ (name, NONE) cases = Name_Space.del_table name cases
    3.38 -  | update_case context legacy (name, SOME c) cases =
    3.39 -      let
    3.40 -        val binding = Binding.name name |> legacy ? Binding.concealed;
    3.41 -        val (_, cases') = Name_Space.define context false (binding, (c, {legacy = legacy})) cases;
    3.42 -      in cases' end;
    3.43 -
    3.44 -fun update_cases' legacy args ctxt =
    3.45 -  let val context = Context.Proof ctxt |> Name_Space.map_naming (K Name_Space.global_naming);
    3.46 -  in map_cases (fold (update_case context legacy) args) ctxt end;
    3.47 +fun update_case _ ("", _) cases = cases
    3.48 +  | update_case _ (name, NONE) cases = Name_Space.del_table name cases
    3.49 +  | update_case context (name, SOME c) cases =
    3.50 +      #2 (Name_Space.define context false (Binding.name name, c) cases);
    3.51  
    3.52  fun fix (b, T) ctxt =
    3.53    let val ([x], ctxt') = add_fixes [(b, SOME T, NoSyn)] ctxt
    3.54 @@ -1337,8 +1329,9 @@
    3.55  
    3.56  in
    3.57  
    3.58 -val update_cases = update_cases' false;
    3.59 -val update_cases_legacy = update_cases' true;
    3.60 +fun update_cases args ctxt =
    3.61 +  let val context = Context.Proof ctxt |> Name_Space.map_naming (K Name_Space.global_naming);
    3.62 +  in map_cases (fold (update_case context) args) ctxt end;
    3.63  
    3.64  fun case_result c ctxt =
    3.65    let
    3.66 @@ -1356,13 +1349,8 @@
    3.67  
    3.68  fun check_case ctxt internal (name, pos) param_specs =
    3.69    let
    3.70 -    val (_, (Rule_Cases.Case {fixes, assumes, binds, cases}, {legacy})) =
    3.71 +    val (_, Rule_Cases.Case {fixes, assumes, binds, cases}) =
    3.72        Name_Space.check (Context.Proof ctxt) (cases_of ctxt) (name, pos);
    3.73 -    val _ =
    3.74 -      if legacy then
    3.75 -        legacy_feature ("Bad case " ^ quote name ^ Position.here pos ^
    3.76 -          " -- use proof method \"goal_cases\" instead")
    3.77 -      else ();
    3.78  
    3.79      val _ = List.app (fn NONE => () | SOME b => ignore (check_var internal b)) param_specs;
    3.80      fun replace (opt_x :: xs) ((y, T) :: ys) = (the_default y opt_x, T) :: replace xs ys
    3.81 @@ -1537,10 +1525,9 @@
    3.82  
    3.83  fun pretty_cases ctxt =
    3.84    let
    3.85 -    fun mk_case (_, (_, {legacy = true})) = NONE
    3.86 -      | mk_case (name, (c as Rule_Cases.Case {fixes, ...}, {legacy = false})) =
    3.87 -          SOME (name, (fixes, case_result c ctxt));
    3.88 -    val cases = dest_cases NONE ctxt |> map_filter mk_case;
    3.89 +    val cases =
    3.90 +      dest_cases NONE ctxt |> map (fn (name, c as Rule_Cases.Case {fixes, ...}) =>
    3.91 +        (name, (fixes, case_result c ctxt)));
    3.92    in
    3.93      if null cases then []
    3.94      else [Pretty.big_list "cases:" (map pretty_case cases)]
    3.95 @@ -1563,20 +1550,18 @@
    3.96      fun is_case x t =
    3.97        x = Rule_Cases.case_conclN andalso not (Term.exists_subterm Term.is_Var t);
    3.98  
    3.99 -    fun print_proof (name, (Rule_Cases.Case {fixes, binds, ...}, {legacy})) =
   3.100 -      if legacy then NONE
   3.101 -      else
   3.102 -        let
   3.103 -          val concl =
   3.104 -            if exists (fn ((x, _), SOME t) => is_case x t | _ => false) binds
   3.105 -            then Rule_Cases.case_conclN else Auto_Bind.thesisN;
   3.106 -        in
   3.107 -          SOME (cat_lines
   3.108 -            ["  case " ^ print_case name (map (Binding.name_of o #1) fixes),
   3.109 -             "  then show ?" ^ concl ^ " sorry"])
   3.110 -        end;
   3.111 +    fun print_proof (name, Rule_Cases.Case {fixes, binds, ...}) =
   3.112 +      let
   3.113 +        val concl =
   3.114 +          if exists (fn ((x, _), SOME t) => is_case x t | _ => false) binds
   3.115 +          then Rule_Cases.case_conclN else Auto_Bind.thesisN;
   3.116 +      in
   3.117 +        cat_lines
   3.118 +          ["  case " ^ print_case name (map (Binding.name_of o #1) fixes),
   3.119 +           "  then show ?" ^ concl ^ " sorry"]
   3.120 +      end;
   3.121    in
   3.122 -    (case map_filter print_proof (dest_cases (SOME ctxt0) ctxt) of
   3.123 +    (case map print_proof (dest_cases (SOME ctxt0) ctxt) of
   3.124        [] => ""
   3.125      | proofs =>
   3.126          "Proof outline with cases:\n" ^