src/Pure/Isar/subgoal.ML
author wenzelm
Sat, 04 Apr 2020 22:39:42 +0200
changeset 71945 8ed68b2aeba1
parent 67721 5348bea4accd
child 74501 c49134ee16c1
permissions -rw-r--r--
more robust: notably for sledgehammer with 'using' and prover=cvc4;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
60630
fc7625ec7427 clarified module;
wenzelm
parents: 60629
diff changeset
     1
(*  Title:      Pure/Isar/subgoal.ML
20210
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
60623
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
     3
    Author:     Daniel Matichuk, NICTA/UNSW
20210
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
     4
32281
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
     5
Tactical operations with explicit subgoal focus, based on canonical
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
     6
proof decomposition.  The "visible" part of the text within the
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
     7
context is fixed, the remaining goal may be schematic.
60623
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
     8
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
     9
Isar subgoal command for proof structure within unstructured proof
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
    10
scripts.
20210
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    11
*)
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    12
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    13
signature SUBGOAL =
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    14
sig
60642
48dd1cefb4ae simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents: 60630
diff changeset
    15
  type focus =
48dd1cefb4ae simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents: 60630
diff changeset
    16
   {context: Proof.context, params: (string * cterm) list, prems: thm list, asms: cterm list,
48dd1cefb4ae simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents: 60630
diff changeset
    17
    concl: cterm, schematics: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list}
60697
757549b4bbe6 Variable.focus etc.: optional bindings provided by user;
wenzelm
parents: 60642
diff changeset
    18
  val focus_params: Proof.context -> int -> binding list option -> thm -> focus * thm
757549b4bbe6 Variable.focus etc.: optional bindings provided by user;
wenzelm
parents: 60642
diff changeset
    19
  val focus_params_fixed: Proof.context -> int -> binding list option -> thm -> focus * thm
757549b4bbe6 Variable.focus etc.: optional bindings provided by user;
wenzelm
parents: 60642
diff changeset
    20
  val focus_prems: Proof.context -> int -> binding list option -> thm -> focus * thm
757549b4bbe6 Variable.focus etc.: optional bindings provided by user;
wenzelm
parents: 60642
diff changeset
    21
  val focus: Proof.context -> int -> binding list option -> thm -> focus * thm
32210
a5e9d9f3e5e1 retrofit: actually handle schematic variables -- need to export into original context;
wenzelm
parents: 32200
diff changeset
    22
  val retrofit: Proof.context -> Proof.context -> (string * cterm) list -> cterm list ->
32200
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    23
    int -> thm -> thm -> thm Seq.seq
32281
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    24
  val FOCUS_PARAMS: (focus -> tactic) -> Proof.context -> int -> tactic
60626
9eefb9f39021 clarified prems: full subgoal is imported in any case, to avoid remaining schematic variables;
wenzelm
parents: 60625
diff changeset
    25
  val FOCUS_PARAMS_FIXED: (focus -> tactic) -> Proof.context -> int -> tactic
32281
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    26
  val FOCUS_PREMS: (focus -> tactic) -> Proof.context -> int -> tactic
32200
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    27
  val FOCUS: (focus -> tactic) -> Proof.context -> int -> tactic
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    28
  val SUBPROOF: (focus -> tactic) -> Proof.context -> int -> tactic
60629
d4e97fcdf83e allow to specify suffix of goal parameters;
wenzelm
parents: 60628
diff changeset
    29
  val subgoal: Attrib.binding -> Attrib.binding option ->
d4e97fcdf83e allow to specify suffix of goal parameters;
wenzelm
parents: 60628
diff changeset
    30
    bool * (string option * Position.T) list -> Proof.state -> focus * Proof.state
d4e97fcdf83e allow to specify suffix of goal parameters;
wenzelm
parents: 60628
diff changeset
    31
  val subgoal_cmd: Attrib.binding -> Attrib.binding option ->
d4e97fcdf83e allow to specify suffix of goal parameters;
wenzelm
parents: 60628
diff changeset
    32
    bool * (string option * Position.T) list -> Proof.state -> focus * Proof.state
20210
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    33
end;
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    34
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    35
structure Subgoal: SUBGOAL =
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    36
struct
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    37
32200
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    38
(* focus *)
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    39
60642
48dd1cefb4ae simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents: 60630
diff changeset
    40
type focus =
48dd1cefb4ae simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents: 60630
diff changeset
    41
 {context: Proof.context, params: (string * cterm) list, prems: thm list, asms: cterm list,
48dd1cefb4ae simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents: 60630
diff changeset
    42
  concl: cterm, schematics: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list};
20210
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    43
60697
757549b4bbe6 Variable.focus etc.: optional bindings provided by user;
wenzelm
parents: 60642
diff changeset
    44
fun gen_focus (do_prems, do_concl) ctxt i bindings raw_st =
20210
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    45
  let
60367
e201bd8973db clarified context;
wenzelm
parents: 59621
diff changeset
    46
    val st = raw_st
71945
8ed68b2aeba1 more robust: notably for sledgehammer with 'using' and prover=cvc4;
wenzelm
parents: 67721
diff changeset
    47
      |> Thm.solve_constraints
67649
1e1782c1aedf tuned signature;
wenzelm
parents: 63352
diff changeset
    48
      |> Thm.transfer' ctxt
60630
fc7625ec7427 clarified module;
wenzelm
parents: 60629
diff changeset
    49
      |> Raw_Simplifier.norm_hhf_protect ctxt;
32281
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    50
    val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt;
60697
757549b4bbe6 Variable.focus etc.: optional bindings provided by user;
wenzelm
parents: 60642
diff changeset
    51
    val ((params, goal), ctxt2) = Variable.focus_cterm bindings (Thm.cprem_of st' i) ctxt1;
32281
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    52
32213
f1b166317ae2 added focus_params/FOCUS_PARAMS, which focus on the parameter prefix only;
wenzelm
parents: 32210
diff changeset
    53
    val (asms, concl) =
32281
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    54
      if do_prems then (Drule.strip_imp_prems goal, Drule.strip_imp_concl goal)
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    55
      else ([], goal);
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    56
    val text = asms @ (if do_concl then [concl] else []);
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    57
60367
e201bd8973db clarified context;
wenzelm
parents: 59621
diff changeset
    58
    val (inst, ctxt3) = Variable.import_inst true (map Thm.term_of text) ctxt2;
60805
4cc49ead6e75 tuned signature;
wenzelm
parents: 60707
diff changeset
    59
    val schematic_terms = map (apsnd (Thm.cterm_of ctxt3)) (#2 inst);
32281
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    60
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    61
    val schematics = (schematic_types, schematic_terms);
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    62
    val asms' = map (Thm.instantiate_cterm schematics) asms;
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    63
    val concl' = Thm.instantiate_cterm schematics concl;
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    64
    val (prems, context) = Assumption.add_assumes asms' ctxt3;
20210
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    65
  in
32200
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    66
    ({context = context, params = params, prems = prems,
32281
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    67
      asms = asms', concl = concl', schematics = schematics}, Goal.init concl')
20210
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    68
  end;
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    69
32281
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    70
val focus_params = gen_focus (false, false);
60626
9eefb9f39021 clarified prems: full subgoal is imported in any case, to avoid remaining schematic variables;
wenzelm
parents: 60625
diff changeset
    71
val focus_params_fixed = gen_focus (false, true);
32281
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    72
val focus_prems = gen_focus (true, false);
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    73
val focus = gen_focus (true, true);
32213
f1b166317ae2 added focus_params/FOCUS_PARAMS, which focus on the parameter prefix only;
wenzelm
parents: 32210
diff changeset
    74
32200
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    75
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    76
(* lift and retrofit *)
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    77
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    78
(*
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    79
     B [?'b, ?y]
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    80
  ----------------
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    81
  B ['b, y params]
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    82
*)
32284
d8ee8a956f19 retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents: 32283
diff changeset
    83
fun lift_import idx params th ctxt =
32200
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    84
  let
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    85
    val ((_, [th']), ctxt') = Variable.importT [th] ctxt;
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    86
59586
ddf6deaadfe8 clarified signature;
wenzelm
parents: 59573
diff changeset
    87
    val Ts = map Thm.typ_of_cterm params;
32200
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    88
    val ts = map Thm.term_of params;
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    89
32281
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    90
    val prop = Thm.full_prop_of th';
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    91
    val concl_vars = Term.add_vars (Logic.strip_imp_concl prop) [];
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    92
    val vars = rev (Term.add_vars prop []);
32200
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    93
    val (ys, ctxt'') = Variable.variant_fixes (map (Name.clean o #1 o #1) vars) ctxt';
32284
d8ee8a956f19 retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents: 32283
diff changeset
    94
d8ee8a956f19 retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents: 32283
diff changeset
    95
    fun var_inst v y =
d8ee8a956f19 retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents: 32283
diff changeset
    96
      let
d8ee8a956f19 retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents: 32283
diff changeset
    97
        val ((x, i), T) = v;
d8ee8a956f19 retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents: 32283
diff changeset
    98
        val (U, args) =
d8ee8a956f19 retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents: 32283
diff changeset
    99
          if member (op =) concl_vars v then (T, [])
d8ee8a956f19 retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents: 32283
diff changeset
   100
          else (Ts ---> T, ts);
d8ee8a956f19 retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents: 32283
diff changeset
   101
        val u = Free (y, U);
d8ee8a956f19 retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents: 32283
diff changeset
   102
        in ((Var v, list_comb (u, args)), (u, Var ((x, i + idx), U))) end;
59616
eb59c6968219 tuned -- more explicit use of context;
wenzelm
parents: 59586
diff changeset
   103
    val (inst1, inst2) =
59621
291934bac95e Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents: 59616
diff changeset
   104
      split_list (map (apply2 (apply2 (Thm.cterm_of ctxt))) (map2 var_inst vars ys));
32284
d8ee8a956f19 retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents: 32283
diff changeset
   105
60642
48dd1cefb4ae simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents: 60630
diff changeset
   106
    val th'' = Thm.instantiate ([], map (apfst (Term.dest_Var o Thm.term_of)) inst1) th';
32284
d8ee8a956f19 retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents: 32283
diff changeset
   107
  in ((inst2, th''), ctxt'') end;
32200
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
   108
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
   109
(*
32281
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
   110
       [x, A x]
32200
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
   111
          :
67721
5348bea4accd eliminated ASCII syntax from Pure bootstrap;
wenzelm
parents: 67649
diff changeset
   112
       B x \<Longrightarrow> C
32200
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
   113
  ------------------
67721
5348bea4accd eliminated ASCII syntax from Pure bootstrap;
wenzelm
parents: 67649
diff changeset
   114
  [\<And>x. A x \<Longrightarrow> B x]
32281
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
   115
          :
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
   116
          C
32200
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
   117
*)
60938
b316f218ef34 clarified context;
wenzelm
parents: 60805
diff changeset
   118
fun lift_subgoals ctxt params asms th =
32200
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
   119
  let
60938
b316f218ef34 clarified context;
wenzelm
parents: 60805
diff changeset
   120
    fun lift ct = fold_rev (Thm.all_name ctxt) params (Drule.list_implies (asms, ct));
32200
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
   121
    val unlift =
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
   122
      fold (Thm.elim_implies o Thm.assume) asms o
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
   123
      Drule.forall_elim_list (map #2 params) o Thm.assume;
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
   124
    val subgoals = map lift (Drule.strip_imp_prems (Thm.cprop_of th));
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
   125
    val th' = fold (Thm.elim_implies o unlift) subgoals th;
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
   126
  in (subgoals, th') end;
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
   127
32213
f1b166317ae2 added focus_params/FOCUS_PARAMS, which focus on the parameter prefix only;
wenzelm
parents: 32210
diff changeset
   128
fun retrofit ctxt1 ctxt0 params asms i st1 st0 =
32200
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
   129
  let
32284
d8ee8a956f19 retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents: 32283
diff changeset
   130
    val idx = Thm.maxidx_of st0 + 1;
32200
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
   131
    val ps = map #2 params;
32284
d8ee8a956f19 retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents: 32283
diff changeset
   132
    val ((subgoal_inst, st2), ctxt2) = lift_import idx ps st1 ctxt1;
60938
b316f218ef34 clarified context;
wenzelm
parents: 60805
diff changeset
   133
    val (subgoals, st3) = lift_subgoals ctxt2 params asms st2;
32213
f1b166317ae2 added focus_params/FOCUS_PARAMS, which focus on the parameter prefix only;
wenzelm
parents: 32210
diff changeset
   134
    val result = st3
f1b166317ae2 added focus_params/FOCUS_PARAMS, which focus on the parameter prefix only;
wenzelm
parents: 32210
diff changeset
   135
      |> Goal.conclude
32200
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
   136
      |> Drule.implies_intr_list asms
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
   137
      |> Drule.forall_intr_list ps
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
   138
      |> Drule.implies_intr_list subgoals
32284
d8ee8a956f19 retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents: 32283
diff changeset
   139
      |> fold_rev (Thm.forall_intr o #1) subgoal_inst
d8ee8a956f19 retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents: 32283
diff changeset
   140
      |> fold (Thm.forall_elim o #2) subgoal_inst
d8ee8a956f19 retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents: 32283
diff changeset
   141
      |> Thm.adjust_maxidx_thm idx
d8ee8a956f19 retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents: 32283
diff changeset
   142
      |> singleton (Variable.export ctxt2 ctxt0);
52223
5bb6ae8acb87 tuned signature -- more explicit flags for low-level Thm.bicompose;
wenzelm
parents: 49845
diff changeset
   143
  in
58950
d07464875dd4 optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents: 54883
diff changeset
   144
    Thm.bicompose (SOME ctxt0) {flatten = true, match = false, incremented = false}
52223
5bb6ae8acb87 tuned signature -- more explicit flags for low-level Thm.bicompose;
wenzelm
parents: 49845
diff changeset
   145
      (false, result, Thm.nprems_of st1) i st0
5bb6ae8acb87 tuned signature -- more explicit flags for low-level Thm.bicompose;
wenzelm
parents: 49845
diff changeset
   146
  end;
32200
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
   147
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
   148
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
   149
(* tacticals *)
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
   150
32281
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
   151
fun GEN_FOCUS flags tac ctxt i st =
20210
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
   152
  if Thm.nprems_of st < i then Seq.empty
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
   153
  else
60707
e96b7be56d44 SUBPROOF and Subgoal.FOCUS combinators use anonymous quasi-bound variables (like the Simplifier);
wenzelm
parents: 60697
diff changeset
   154
    let val (args as {context = ctxt', params, asms, ...}, st') =
e96b7be56d44 SUBPROOF and Subgoal.FOCUS combinators use anonymous quasi-bound variables (like the Simplifier);
wenzelm
parents: 60697
diff changeset
   155
      gen_focus flags (ctxt |> Variable.set_bound_focus true) i NONE st;
32329
1527ff8c2dfb SUBPROOF: recovered Goal.check_finished;
wenzelm
parents: 32284
diff changeset
   156
    in Seq.lifts (retrofit ctxt' ctxt params asms i) (tac args st') st end;
32200
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
   157
32281
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
   158
val FOCUS_PARAMS = GEN_FOCUS (false, false);
60626
9eefb9f39021 clarified prems: full subgoal is imported in any case, to avoid remaining schematic variables;
wenzelm
parents: 60625
diff changeset
   159
val FOCUS_PARAMS_FIXED = GEN_FOCUS (false, true);
32281
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
   160
val FOCUS_PREMS = GEN_FOCUS (true, false);
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
   161
val FOCUS = GEN_FOCUS (true, true);
32213
f1b166317ae2 added focus_params/FOCUS_PARAMS, which focus on the parameter prefix only;
wenzelm
parents: 32210
diff changeset
   162
49845
9b19c0e81166 tuned signature;
wenzelm
parents: 42495
diff changeset
   163
fun SUBPROOF tac ctxt = FOCUS (Seq.map (Goal.check_finished ctxt) oo tac) ctxt;
20210
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
   164
60623
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
   165
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
   166
(* Isar subgoal command *)
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
   167
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
   168
local
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
   169
60697
757549b4bbe6 Variable.focus etc.: optional bindings provided by user;
wenzelm
parents: 60642
diff changeset
   170
fun param_bindings ctxt (param_suffix, raw_param_specs) st =
60628
5ff15d0dd7fa subgoal parameters are internal by default and named by user;
wenzelm
parents: 60627
diff changeset
   171
  let
5ff15d0dd7fa subgoal parameters are internal by default and named by user;
wenzelm
parents: 60627
diff changeset
   172
    val _ = if Thm.no_prems st then error "No subgoals!" else ();
60697
757549b4bbe6 Variable.focus etc.: optional bindings provided by user;
wenzelm
parents: 60642
diff changeset
   173
    val subgoal = #1 (Logic.dest_implies (Thm.prop_of st));
60629
d4e97fcdf83e allow to specify suffix of goal parameters;
wenzelm
parents: 60628
diff changeset
   174
    val subgoal_params =
d4e97fcdf83e allow to specify suffix of goal parameters;
wenzelm
parents: 60628
diff changeset
   175
      map (apfst (Name.internal o Name.clean)) (Term.strip_all_vars subgoal)
d4e97fcdf83e allow to specify suffix of goal parameters;
wenzelm
parents: 60628
diff changeset
   176
      |> Term.variant_frees subgoal |> map #1;
60628
5ff15d0dd7fa subgoal parameters are internal by default and named by user;
wenzelm
parents: 60627
diff changeset
   177
60629
d4e97fcdf83e allow to specify suffix of goal parameters;
wenzelm
parents: 60628
diff changeset
   178
    val n = length subgoal_params;
d4e97fcdf83e allow to specify suffix of goal parameters;
wenzelm
parents: 60628
diff changeset
   179
    val m = length raw_param_specs;
60628
5ff15d0dd7fa subgoal parameters are internal by default and named by user;
wenzelm
parents: 60627
diff changeset
   180
    val _ =
60629
d4e97fcdf83e allow to specify suffix of goal parameters;
wenzelm
parents: 60628
diff changeset
   181
      m <= n orelse
d4e97fcdf83e allow to specify suffix of goal parameters;
wenzelm
parents: 60628
diff changeset
   182
        error ("Excessive subgoal parameter specification" ^
d4e97fcdf83e allow to specify suffix of goal parameters;
wenzelm
parents: 60628
diff changeset
   183
          Position.here_list (map snd (drop n raw_param_specs)));
60628
5ff15d0dd7fa subgoal parameters are internal by default and named by user;
wenzelm
parents: 60627
diff changeset
   184
60629
d4e97fcdf83e allow to specify suffix of goal parameters;
wenzelm
parents: 60628
diff changeset
   185
    val param_specs =
d4e97fcdf83e allow to specify suffix of goal parameters;
wenzelm
parents: 60628
diff changeset
   186
      raw_param_specs |> map
d4e97fcdf83e allow to specify suffix of goal parameters;
wenzelm
parents: 60628
diff changeset
   187
        (fn (NONE, _) => NONE
d4e97fcdf83e allow to specify suffix of goal parameters;
wenzelm
parents: 60628
diff changeset
   188
          | (SOME x, pos) =>
60697
757549b4bbe6 Variable.focus etc.: optional bindings provided by user;
wenzelm
parents: 60642
diff changeset
   189
              let
757549b4bbe6 Variable.focus etc.: optional bindings provided by user;
wenzelm
parents: 60642
diff changeset
   190
                val b = #1 (#1 (Proof_Context.cert_var (Binding.make (x, pos), NONE, NoSyn) ctxt));
757549b4bbe6 Variable.focus etc.: optional bindings provided by user;
wenzelm
parents: 60642
diff changeset
   191
                val _ = Variable.check_name b;
757549b4bbe6 Variable.focus etc.: optional bindings provided by user;
wenzelm
parents: 60642
diff changeset
   192
              in SOME b end)
60629
d4e97fcdf83e allow to specify suffix of goal parameters;
wenzelm
parents: 60628
diff changeset
   193
      |> param_suffix ? append (replicate (n - m) NONE);
d4e97fcdf83e allow to specify suffix of goal parameters;
wenzelm
parents: 60628
diff changeset
   194
60697
757549b4bbe6 Variable.focus etc.: optional bindings provided by user;
wenzelm
parents: 60642
diff changeset
   195
    fun bindings (SOME x :: xs) (_ :: ys) = x :: bindings xs ys
757549b4bbe6 Variable.focus etc.: optional bindings provided by user;
wenzelm
parents: 60642
diff changeset
   196
      | bindings (NONE :: xs) (y :: ys) = Binding.name y :: bindings xs ys
757549b4bbe6 Variable.focus etc.: optional bindings provided by user;
wenzelm
parents: 60642
diff changeset
   197
      | bindings _ ys = map Binding.name ys;
757549b4bbe6 Variable.focus etc.: optional bindings provided by user;
wenzelm
parents: 60642
diff changeset
   198
  in bindings param_specs subgoal_params end;
60628
5ff15d0dd7fa subgoal parameters are internal by default and named by user;
wenzelm
parents: 60627
diff changeset
   199
5ff15d0dd7fa subgoal parameters are internal by default and named by user;
wenzelm
parents: 60627
diff changeset
   200
fun gen_subgoal prep_atts raw_result_binding raw_prems_binding param_specs state =
60623
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
   201
  let
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
   202
    val _ = Proof.assert_backward state;
60627
5d13babbb3f6 split multi-goals as usual (outermost Pure.conjunction only);
wenzelm
parents: 60626
diff changeset
   203
5d13babbb3f6 split multi-goals as usual (outermost Pure.conjunction only);
wenzelm
parents: 60626
diff changeset
   204
    val state1 = state |> Proof.refine_insert [];
5d13babbb3f6 split multi-goals as usual (outermost Pure.conjunction only);
wenzelm
parents: 60626
diff changeset
   205
    val {context = ctxt, facts = facts, goal = st} = Proof.raw_goal state1;
60623
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
   206
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
   207
    val result_binding = apsnd (map (prep_atts ctxt)) raw_result_binding;
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
   208
    val (prems_binding, do_prems) =
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
   209
      (case raw_prems_binding of
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
   210
        SOME (b, raw_atts) => ((b, map (prep_atts ctxt) raw_atts), true)
63352
4eaf35781b23 tuned signature;
wenzelm
parents: 60938
diff changeset
   211
      | NONE => (Binding.empty_atts, false));
60623
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
   212
60628
5ff15d0dd7fa subgoal parameters are internal by default and named by user;
wenzelm
parents: 60627
diff changeset
   213
    val (subgoal_focus, _) =
60697
757549b4bbe6 Variable.focus etc.: optional bindings provided by user;
wenzelm
parents: 60642
diff changeset
   214
      (if do_prems then focus else focus_params_fixed) ctxt
757549b4bbe6 Variable.focus etc.: optional bindings provided by user;
wenzelm
parents: 60642
diff changeset
   215
        1 (SOME (param_bindings ctxt param_specs st)) st;
60623
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
   216
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
   217
    fun after_qed (ctxt'', [[result]]) =
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
   218
      Proof.end_block #> (fn state' =>
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
   219
        let
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
   220
          val ctxt' = Proof.context_of state';
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
   221
          val results' =
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
   222
            Proof_Context.export ctxt'' ctxt' (Conjunction.elim_conjunctions result);
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
   223
        in
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
   224
          state'
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
   225
          |> Proof.refine_primitive (fn _ => fn _ =>
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
   226
            retrofit ctxt'' ctxt' (#params subgoal_focus) (#asms subgoal_focus) 1
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
   227
              (Goal.protect 0 result) st
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
   228
            |> Seq.hd)
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
   229
          |> Proof.map_context
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
   230
            (#2 o Proof_Context.note_thmss "" [(result_binding, [(results', [])])])
60625
f64658887a05 proper state after qed;
wenzelm
parents: 60623
diff changeset
   231
        end)
f64658887a05 proper state after qed;
wenzelm
parents: 60623
diff changeset
   232
      #> Proof.reset_facts
f64658887a05 proper state after qed;
wenzelm
parents: 60623
diff changeset
   233
      #> Proof.enter_backward;
60623
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
   234
  in
60627
5d13babbb3f6 split multi-goals as usual (outermost Pure.conjunction only);
wenzelm
parents: 60626
diff changeset
   235
    state1
60623
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
   236
    |> Proof.enter_forward
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
   237
    |> Proof.using_facts []
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
   238
    |> Proof.begin_block
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
   239
    |> Proof.map_context (fn _ =>
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
   240
      #context subgoal_focus
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
   241
      |> Proof_Context.note_thmss "" [(prems_binding, [(#prems subgoal_focus, [])])] |> #2)
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
   242
    |> Proof.internal_goal (K (K ())) (Proof_Context.get_mode ctxt) true "subgoal"
63352
4eaf35781b23 tuned signature;
wenzelm
parents: 60938
diff changeset
   243
        NONE after_qed [] [] [(Binding.empty_atts, [(Thm.term_of (#concl subgoal_focus), [])])] |> #2
60623
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
   244
    |> Proof.using_facts facts
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
   245
    |> pair subgoal_focus
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
   246
  end;
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
   247
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
   248
in
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
   249
60626
9eefb9f39021 clarified prems: full subgoal is imported in any case, to avoid remaining schematic variables;
wenzelm
parents: 60625
diff changeset
   250
val subgoal = gen_subgoal Attrib.attribute;
9eefb9f39021 clarified prems: full subgoal is imported in any case, to avoid remaining schematic variables;
wenzelm
parents: 60625
diff changeset
   251
val subgoal_cmd = gen_subgoal Attrib.attribute_cmd;
60623
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
   252
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
   253
end;
be39fe6c5620 support for subgoal focus command;
wenzelm
parents: 60367
diff changeset
   254
20210
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
   255
end;
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
   256
32200
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
   257
val SUBPROOF = Subgoal.SUBPROOF;