src/Pure/goal.ML
author wenzelm
Mon, 10 Apr 2017 21:05:31 +0200
changeset 65458 cf504b7a7aa7
parent 64567 7141a3a4dc83
child 67721 5348bea4accd
permissions -rw-r--r--
tuned signature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17980
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/goal.ML
29345
5904873d8f11 tuned protect, conclude: Drule.comp_no_flatten;
wenzelm
parents: 29343
diff changeset
     2
    Author:     Makarius
17980
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
     3
49061
7449b804073b central management of forked goals wrt. transaction id;
wenzelm
parents: 49041
diff changeset
     4
Goals in tactical theorem proving, with support for forked proofs.
17980
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
     5
*)
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
     6
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
     7
signature BASIC_GOAL =
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
     8
sig
61527
d05f3d86a758 tuned signature -- clarified modules;
wenzelm
parents: 61508
diff changeset
     9
  val quick_and_dirty: bool Config.T
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32365
diff changeset
    10
  val parallel_proofs: int Unsynchronized.ref
17980
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
    11
  val SELECT_GOAL: tactic -> int -> tactic
52458
210bca64b894 less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
wenzelm
parents: 52456
diff changeset
    12
  val PREFER_GOAL: tactic -> int -> tactic
23418
c195f6f13769 balanced conjunctions;
wenzelm
parents: 23414
diff changeset
    13
  val CONJUNCTS: tactic -> int -> tactic
23414
927203ad4b3a tuned conjunction tactics: slightly smaller proof terms;
wenzelm
parents: 23356
diff changeset
    14
  val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
17980
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
    15
end;
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
    16
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
    17
signature GOAL =
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
    18
sig
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
    19
  include BASIC_GOAL
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
    20
  val init: cterm -> thm
52456
960202346d0c tuned signature;
wenzelm
parents: 52223
diff changeset
    21
  val protect: int -> thm -> thm
17980
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
    22
  val conclude: thm -> thm
49845
9b19c0e81166 tuned signature;
wenzelm
parents: 49830
diff changeset
    23
  val check_finished: Proof.context -> thm -> thm
32197
bc341bbe4417 Goal.finish: explicit context for printing;
wenzelm
parents: 32187
diff changeset
    24
  val finish: Proof.context -> thm -> thm
54883
dd04a8b654fc proper context for norm_hhf and derived operations;
wenzelm
parents: 54742
diff changeset
    25
  val norm_result: Proof.context -> thm -> thm
52499
812215680f6d clarified Proofterm.proofs vs. Goal.skip_proofs;
wenzelm
parents: 52461
diff changeset
    26
  val skip_proofs_enabled: unit -> bool
53189
ee8b8dafef0e discontinued parallel_subproofs_saturation and related internal counters (superseded by parallel_subproofs_threshold and timing information);
wenzelm
parents: 52811
diff changeset
    27
  val future_enabled: int -> bool
51423
e5f9a6d9ca82 clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents: 51276
diff changeset
    28
  val future_enabled_timing: Time.time -> bool
28973
c549650d1442 future proofs: pass actual futures to facilitate composite computations;
wenzelm
parents: 28619
diff changeset
    29
  val future_result: Proof.context -> thm future -> term -> thm
54883
dd04a8b654fc proper context for norm_hhf and derived operations;
wenzelm
parents: 54742
diff changeset
    30
  val prove_internal: Proof.context -> cterm list -> cterm -> (thm list -> tactic) -> thm
51553
63327f679cff more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
wenzelm
parents: 51552
diff changeset
    31
  val is_schematic: term -> bool
59564
fdc03c8daacc Goal.prove_multi is superseded by the fully general Goal.prove_common;
wenzelm
parents: 59498
diff changeset
    32
  val prove_common: Proof.context -> int option -> string list -> term list -> term list ->
20290
3f886c176c9b normalized Proof.context/method type aliases;
wenzelm
parents: 20260
diff changeset
    33
    ({prems: thm list, context: Proof.context} -> tactic) -> thm list
28446
a01de3b3fa2e renamed promise to future, tuned related interfaces;
wenzelm
parents: 28363
diff changeset
    34
  val prove_future: Proof.context -> string list -> term list -> term ->
28340
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
    35
    ({prems: thm list, context: Proof.context} -> tactic) -> thm
20290
3f886c176c9b normalized Proof.context/method type aliases;
wenzelm
parents: 20260
diff changeset
    36
  val prove: Proof.context -> string list -> term list -> term ->
3f886c176c9b normalized Proof.context/method type aliases;
wenzelm
parents: 20260
diff changeset
    37
    ({prems: thm list, context: Proof.context} -> tactic) -> thm
51118
32a5994dd205 tuned signature -- legacy packages might want to fork proofs as well;
wenzelm
parents: 51110
diff changeset
    38
  val prove_global_future: theory -> string list -> term list -> term ->
32a5994dd205 tuned signature -- legacy packages might want to fork proofs as well;
wenzelm
parents: 51110
diff changeset
    39
    ({prems: thm list, context: Proof.context} -> tactic) -> thm
26713
1c6181def1d0 prove_global: Variable.set_body true, pass context;
wenzelm
parents: 26628
diff changeset
    40
  val prove_global: theory -> string list -> term list -> term ->
1c6181def1d0 prove_global: Variable.set_body true, pass context;
wenzelm
parents: 26628
diff changeset
    41
    ({prems: thm list, context: Proof.context} -> tactic) -> thm
61527
d05f3d86a758 tuned signature -- clarified modules;
wenzelm
parents: 61508
diff changeset
    42
  val quick_and_dirty_raw: Config.raw
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51423
diff changeset
    43
  val prove_sorry: Proof.context -> string list -> term list -> term ->
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51423
diff changeset
    44
    ({prems: thm list, context: Proof.context} -> tactic) -> thm
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51423
diff changeset
    45
  val prove_sorry_global: theory -> string list -> term list -> term ->
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51423
diff changeset
    46
    ({prems: thm list, context: Proof.context} -> tactic) -> thm
52458
210bca64b894 less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
wenzelm
parents: 52456
diff changeset
    47
  val restrict: int -> int -> thm -> thm
210bca64b894 less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
wenzelm
parents: 52456
diff changeset
    48
  val unrestrict: int -> thm -> thm
23418
c195f6f13769 balanced conjunctions;
wenzelm
parents: 23414
diff changeset
    49
  val conjunction_tac: int -> tactic
23414
927203ad4b3a tuned conjunction tactics: slightly smaller proof terms;
wenzelm
parents: 23356
diff changeset
    50
  val precise_conjunction_tac: int -> int -> tactic
23418
c195f6f13769 balanced conjunctions;
wenzelm
parents: 23414
diff changeset
    51
  val recover_conjunction_tac: tactic
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 54567
diff changeset
    52
  val norm_hhf_tac: Proof.context -> int -> tactic
23237
ac9d126456e1 added assume_rule_tac;
wenzelm
parents: 22902
diff changeset
    53
  val assume_rule_tac: Proof.context -> int -> tactic
17980
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
    54
end;
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
    55
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
    56
structure Goal: GOAL =
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
    57
struct
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
    58
18027
09ab79d4e8e1 renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents: 17986
diff changeset
    59
(** goals **)
09ab79d4e8e1 renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents: 17986
diff changeset
    60
09ab79d4e8e1 renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents: 17986
diff changeset
    61
(*
09ab79d4e8e1 renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents: 17986
diff changeset
    62
  -------- (init)
09ab79d4e8e1 renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents: 17986
diff changeset
    63
  C ==> #C
09ab79d4e8e1 renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents: 17986
diff changeset
    64
*)
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: 59623
diff changeset
    65
fun init C = Thm.instantiate ([], [((("A", 0), propT), C)]) Drule.protectI;
17980
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
    66
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
    67
(*
52456
960202346d0c tuned signature;
wenzelm
parents: 52223
diff changeset
    68
  A1 ==> ... ==> An ==> C
960202346d0c tuned signature;
wenzelm
parents: 52223
diff changeset
    69
  ------------------------ (protect n)
960202346d0c tuned signature;
wenzelm
parents: 52223
diff changeset
    70
  A1 ==> ... ==> An ==> #C
17980
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
    71
*)
52456
960202346d0c tuned signature;
wenzelm
parents: 52223
diff changeset
    72
fun protect n th = Drule.comp_no_flatten (th, n) 1 Drule.protectI;
17980
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
    73
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
    74
(*
18027
09ab79d4e8e1 renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents: 17986
diff changeset
    75
  A ==> ... ==> #C
09ab79d4e8e1 renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents: 17986
diff changeset
    76
  ---------------- (conclude)
17980
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
    77
  A ==> ... ==> C
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
    78
*)
29345
5904873d8f11 tuned protect, conclude: Drule.comp_no_flatten;
wenzelm
parents: 29343
diff changeset
    79
fun conclude th = Drule.comp_no_flatten (th, Thm.nprems_of th) 1 Drule.protectD;
17980
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
    80
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
    81
(*
18027
09ab79d4e8e1 renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents: 17986
diff changeset
    82
  #C
09ab79d4e8e1 renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents: 17986
diff changeset
    83
  --- (finish)
09ab79d4e8e1 renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents: 17986
diff changeset
    84
   C
17983
wenzelm
parents: 17980
diff changeset
    85
*)
32197
bc341bbe4417 Goal.finish: explicit context for printing;
wenzelm
parents: 32187
diff changeset
    86
fun check_finished ctxt th =
51608
wenzelm
parents: 51607
diff changeset
    87
  if Thm.no_prems th then th
wenzelm
parents: 51607
diff changeset
    88
  else
51958
bca32217b304 retain goal display options when printing error messages, to avoid breakdown for huge goals;
wenzelm
parents: 51608
diff changeset
    89
    raise THM ("Proof failed.\n" ^ Pretty.string_of (Goal_Display.pretty_goal ctxt th), 0, [th]);
32197
bc341bbe4417 Goal.finish: explicit context for printing;
wenzelm
parents: 32187
diff changeset
    90
49845
9b19c0e81166 tuned signature;
wenzelm
parents: 49830
diff changeset
    91
fun finish ctxt = check_finished ctxt #> conclude;
17980
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
    92
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
    93
18027
09ab79d4e8e1 renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents: 17986
diff changeset
    94
09ab79d4e8e1 renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents: 17986
diff changeset
    95
(** results **)
09ab79d4e8e1 renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents: 17986
diff changeset
    96
28340
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
    97
(* normal form *)
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
    98
54883
dd04a8b654fc proper context for norm_hhf and derived operations;
wenzelm
parents: 54742
diff changeset
    99
fun norm_result ctxt =
58950
d07464875dd4 optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents: 58837
diff changeset
   100
  Drule.flexflex_unique (SOME ctxt)
54883
dd04a8b654fc proper context for norm_hhf and derived operations;
wenzelm
parents: 54742
diff changeset
   101
  #> Raw_Simplifier.norm_hhf_protect ctxt
21604
1af327306c8e added norm/close_result (supercede local_standard etc.);
wenzelm
parents: 21579
diff changeset
   102
  #> Thm.strip_shyps
1af327306c8e added norm/close_result (supercede local_standard etc.);
wenzelm
parents: 21579
diff changeset
   103
  #> Drule.zero_var_indexes;
1af327306c8e added norm/close_result (supercede local_standard etc.);
wenzelm
parents: 21579
diff changeset
   104
1af327306c8e added norm/close_result (supercede local_standard etc.);
wenzelm
parents: 21579
diff changeset
   105
41703
d27950860514 parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents: 41683
diff changeset
   106
(* scheduling parameters *)
d27950860514 parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents: 41683
diff changeset
   107
52499
812215680f6d clarified Proofterm.proofs vs. Goal.skip_proofs;
wenzelm
parents: 52461
diff changeset
   108
fun skip_proofs_enabled () =
52710
52790e3961fe just one option "skip_proofs", without direct access within the editor (it makes document processing stateful without strong reasons -- monotonic updates already handle goal forks smoothly);
wenzelm
parents: 52696
diff changeset
   109
  let val skip = Options.default_bool "skip_proofs" in
52499
812215680f6d clarified Proofterm.proofs vs. Goal.skip_proofs;
wenzelm
parents: 52461
diff changeset
   110
    if Proofterm.proofs_enabled () andalso skip then
812215680f6d clarified Proofterm.proofs vs. Goal.skip_proofs;
wenzelm
parents: 52461
diff changeset
   111
      (warning "Proof terms enabled -- cannot skip proofs"; false)
812215680f6d clarified Proofterm.proofs vs. Goal.skip_proofs;
wenzelm
parents: 52461
diff changeset
   112
    else skip
812215680f6d clarified Proofterm.proofs vs. Goal.skip_proofs;
wenzelm
parents: 52461
diff changeset
   113
  end;
812215680f6d clarified Proofterm.proofs vs. Goal.skip_proofs;
wenzelm
parents: 52461
diff changeset
   114
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32365
diff changeset
   115
val parallel_proofs = Unsynchronized.ref 1;
29448
34b9652b2f45 added Goal.future_enabled abstraction -- now also checks that this is already
wenzelm
parents: 29435
diff changeset
   116
53189
ee8b8dafef0e discontinued parallel_subproofs_saturation and related internal counters (superseded by parallel_subproofs_threshold and timing information);
wenzelm
parents: 52811
diff changeset
   117
fun future_enabled n =
49012
8686c36fa27d refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
wenzelm
parents: 49009
diff changeset
   118
  Multithreading.enabled () andalso ! parallel_proofs >= n andalso
41703
d27950860514 parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents: 41683
diff changeset
   119
  is_some (Future.worker_task ());
32061
11f8ee55662d parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
wenzelm
parents: 32058
diff changeset
   120
51423
e5f9a6d9ca82 clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents: 51276
diff changeset
   121
fun future_enabled_timing t =
53189
ee8b8dafef0e discontinued parallel_subproofs_saturation and related internal counters (superseded by parallel_subproofs_threshold and timing information);
wenzelm
parents: 52811
diff changeset
   122
  future_enabled 1 andalso
52104
250cd2a9308d proper options;
wenzelm
parents: 52059
diff changeset
   123
    Time.toReal t >= Options.default_real "parallel_subproofs_threshold";
29448
34b9652b2f45 added Goal.future_enabled abstraction -- now also checks that this is already
wenzelm
parents: 29435
diff changeset
   124
34b9652b2f45 added Goal.future_enabled abstraction -- now also checks that this is already
wenzelm
parents: 29435
diff changeset
   125
28446
a01de3b3fa2e renamed promise to future, tuned related interfaces;
wenzelm
parents: 28363
diff changeset
   126
(* future_result *)
28340
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
   127
28446
a01de3b3fa2e renamed promise to future, tuned related interfaces;
wenzelm
parents: 28363
diff changeset
   128
fun future_result ctxt result prop =
28340
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
   129
  let
30473
e0b66c11e7e4 Assumption.all_prems_of, Assumption.all_assms_of;
wenzelm
parents: 29448
diff changeset
   130
    val assms = Assumption.all_assms_of ctxt;
28340
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
   131
    val As = map Thm.term_of assms;
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
   132
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
   133
    val xs = map Free (fold Term.add_frees (prop :: As) []);
59623
920889b0788e clarified context;
wenzelm
parents: 59621
diff changeset
   134
    val fixes = map (Thm.cterm_of ctxt) xs;
28340
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
   135
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
   136
    val tfrees = fold Term.add_tfrees (prop :: As) [];
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: 59623
diff changeset
   137
    val instT = map (fn (a, S) => (((a, 0), S), Thm.ctyp_of ctxt (TFree (a, S)))) tfrees;
28340
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
   138
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
   139
    val global_prop =
59616
eb59c6968219 tuned -- more explicit use of context;
wenzelm
parents: 59582
diff changeset
   140
      Logic.varify_types_global (fold_rev Logic.all xs (Logic.list_implies (As, prop)))
59623
920889b0788e clarified context;
wenzelm
parents: 59621
diff changeset
   141
      |> Thm.cterm_of ctxt
61508
2c7e2ae6173d clarified modules;
wenzelm
parents: 60948
diff changeset
   142
      |> Thm.weaken_sorts' ctxt;
28973
c549650d1442 future proofs: pass actual futures to facilitate composite computations;
wenzelm
parents: 28619
diff changeset
   143
    val global_result = result |> Future.map
58950
d07464875dd4 optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents: 58837
diff changeset
   144
      (Drule.flexflex_unique (SOME ctxt) #>
33768
bba9eac8aa25 future_result: purge flexflex pairs, which should normally be trivial anyway -- prevent Thm.future_result from complaining about tpairs;
wenzelm
parents: 32788
diff changeset
   145
        Thm.adjust_maxidx_thm ~1 #>
28973
c549650d1442 future proofs: pass actual futures to facilitate composite computations;
wenzelm
parents: 28619
diff changeset
   146
        Drule.implies_intr_list assms #>
c549650d1442 future proofs: pass actual futures to facilitate composite computations;
wenzelm
parents: 28619
diff changeset
   147
        Drule.forall_intr_list fixes #>
36613
f3157c288aca simplified primitive Thm.future: more direct theory check, do not hardwire strip_shyps here;
wenzelm
parents: 36610
diff changeset
   148
        Thm.generalize (map #1 tfrees, []) 0 #>
f3157c288aca simplified primitive Thm.future: more direct theory check, do not hardwire strip_shyps here;
wenzelm
parents: 36610
diff changeset
   149
        Thm.strip_shyps);
28340
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
   150
    val local_result =
32056
f4b74cbecdaf future_result: explicitly impose Variable.sorts_of again;
wenzelm
parents: 30473
diff changeset
   151
      Thm.future global_result global_prop
50987
616789281413 always close derivation at the bottom of forked proofs (despite increased non-determinism of proof terms) -- improve parallel performance by avoiding dynamic dependency within large Isar proofs, e.g. Slicing/JinjaVM/SemanticsWF.thy in AFP/bf9b14cbc707;
wenzelm
parents: 50974
diff changeset
   152
      |> Thm.close_derivation
28340
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
   153
      |> Thm.instantiate (instT, [])
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
   154
      |> Drule.forall_elim_list fixes
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
   155
      |> fold (Thm.elim_implies o Thm.assume) assms;
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
   156
  in local_result end;
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
   157
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
   158
18027
09ab79d4e8e1 renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents: 17986
diff changeset
   159
09ab79d4e8e1 renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents: 17986
diff changeset
   160
(** tactical theorem proving **)
09ab79d4e8e1 renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents: 17986
diff changeset
   161
23356
dbe3731241c3 renamed prove_raw to prove_internal;
wenzelm
parents: 23237
diff changeset
   162
(* prove_internal -- minimal checks, no normalization of result! *)
20250
c3f209752749 prove: proper assumption context, more tactic arguments;
wenzelm
parents: 20228
diff changeset
   163
54883
dd04a8b654fc proper context for norm_hhf and derived operations;
wenzelm
parents: 54742
diff changeset
   164
fun prove_internal ctxt casms cprop tac =
dd04a8b654fc proper context for norm_hhf and derived operations;
wenzelm
parents: 54742
diff changeset
   165
  (case SINGLE (tac (map (Assumption.assume ctxt) casms)) (init cprop) of
54992
e5f4075d4c5e clarified context;
wenzelm
parents: 54985
diff changeset
   166
    SOME th => Drule.implies_intr_list casms (finish ctxt th)
38875
c7a66b584147 tuned messages: discontinued spurious full-stops (messages are occasionally composed unexpectedly);
wenzelm
parents: 38236
diff changeset
   167
  | NONE => error "Tactic failed");
20250
c3f209752749 prove: proper assumption context, more tactic arguments;
wenzelm
parents: 20228
diff changeset
   168
c3f209752749 prove: proper assumption context, more tactic arguments;
wenzelm
parents: 20228
diff changeset
   169
51553
63327f679cff more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
wenzelm
parents: 51552
diff changeset
   170
(* prove variations *)
63327f679cff more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
wenzelm
parents: 51552
diff changeset
   171
63327f679cff more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
wenzelm
parents: 51552
diff changeset
   172
fun is_schematic t =
63327f679cff more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
wenzelm
parents: 51552
diff changeset
   173
  Term.exists_subterm Term.is_Var t orelse
63327f679cff more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
wenzelm
parents: 51552
diff changeset
   174
  Term.exists_type (Term.exists_subtype Term.is_TVar) t;
17986
0450847646c3 prove_raw: cterms, explicit asms;
wenzelm
parents: 17983
diff changeset
   175
59564
fdc03c8daacc Goal.prove_multi is superseded by the fully general Goal.prove_common;
wenzelm
parents: 59498
diff changeset
   176
fun prove_common ctxt fork_pri xs asms props tac =
17980
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
   177
  let
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 41819
diff changeset
   178
    val thy = Proof_Context.theory_of ctxt;
20056
0698a403a066 prove/prove_multi: context;
wenzelm
parents: 19862
diff changeset
   179
51553
63327f679cff more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
wenzelm
parents: 51552
diff changeset
   180
    val schematic = exists is_schematic props;
59564
fdc03c8daacc Goal.prove_multi is superseded by the fully general Goal.prove_common;
wenzelm
parents: 59498
diff changeset
   181
    val immediate = is_none fork_pri;
53189
ee8b8dafef0e discontinued parallel_subproofs_saturation and related internal counters (superseded by parallel_subproofs_threshold and timing information);
wenzelm
parents: 52811
diff changeset
   182
    val future = future_enabled 1;
52499
812215680f6d clarified Proofterm.proofs vs. Goal.skip_proofs;
wenzelm
parents: 52461
diff changeset
   183
    val skip = not immediate andalso not schematic andalso future andalso skip_proofs_enabled ();
51553
63327f679cff more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
wenzelm
parents: 51552
diff changeset
   184
28355
b9d9360e2440 prove: error with original thread position;
wenzelm
parents: 28341
diff changeset
   185
    val pos = Position.thread_data ();
55559
d4aea4bbe87f tuned message;
wenzelm
parents: 54994
diff changeset
   186
    fun err msg =
d4aea4bbe87f tuned message;
wenzelm
parents: 54994
diff changeset
   187
      cat_error msg
d4aea4bbe87f tuned message;
wenzelm
parents: 54994
diff changeset
   188
        ("The error(s) above occurred for the goal statement" ^ Position.here pos ^ ":\n" ^
d4aea4bbe87f tuned message;
wenzelm
parents: 54994
diff changeset
   189
          Syntax.string_of_term ctxt (Logic.list_implies (asms, Logic.mk_conjunction_list props)));
17980
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
   190
59623
920889b0788e clarified context;
wenzelm
parents: 59621
diff changeset
   191
    fun cert_safe t = Thm.cterm_of ctxt (Envir.beta_norm (Term.no_dummy_patterns t))
17980
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
   192
      handle TERM (msg, _) => err msg | TYPE (msg, _, _) => err msg;
20250
c3f209752749 prove: proper assumption context, more tactic arguments;
wenzelm
parents: 20228
diff changeset
   193
    val casms = map cert_safe asms;
c3f209752749 prove: proper assumption context, more tactic arguments;
wenzelm
parents: 20228
diff changeset
   194
    val cprops = map cert_safe props;
17980
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
   195
20250
c3f209752749 prove: proper assumption context, more tactic arguments;
wenzelm
parents: 20228
diff changeset
   196
    val (prems, ctxt') = ctxt
c3f209752749 prove: proper assumption context, more tactic arguments;
wenzelm
parents: 20228
diff changeset
   197
      |> Variable.add_fixes_direct xs
27218
4548c83cd508 prove: full Variable.declare_term, including constraints;
wenzelm
parents: 26939
diff changeset
   198
      |> fold Variable.declare_term (asms @ props)
26713
1c6181def1d0 prove_global: Variable.set_body true, pass context;
wenzelm
parents: 26628
diff changeset
   199
      |> Assumption.add_assumes casms
1c6181def1d0 prove_global: Variable.set_body true, pass context;
wenzelm
parents: 26628
diff changeset
   200
      ||> Variable.set_body true;
17980
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
   201
61508
2c7e2ae6173d clarified modules;
wenzelm
parents: 60948
diff changeset
   202
    val stmt = Thm.weaken_sorts' ctxt' (Conjunction.mk_conjunction_balanced cprops);
28340
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
   203
51553
63327f679cff more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
wenzelm
parents: 51552
diff changeset
   204
    fun tac' args st =
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58963
diff changeset
   205
      if skip then ALLGOALS (Skip_Proof.cheat_tac ctxt) st before Skip_Proof.report ctxt
51553
63327f679cff more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
wenzelm
parents: 51552
diff changeset
   206
      else tac args st;
28340
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
   207
    fun result () =
51553
63327f679cff more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
wenzelm
parents: 51552
diff changeset
   208
      (case SINGLE (tac' {prems = prems, context = ctxt'}) (init stmt) of
38875
c7a66b584147 tuned messages: discontinued spurious full-stops (messages are occasionally composed unexpectedly);
wenzelm
parents: 38236
diff changeset
   209
        NONE => err "Tactic failed"
28340
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
   210
      | SOME st =>
54567
cfe53047dc16 more uniform / rigid checking of Goal.prove_common vs. Proof.conclude_goal -- NB: Goal.prove_common cannot check hyps right now, e.g. due to undeclared Simplifier prems;
wenzelm
parents: 53192
diff changeset
   211
          let
54981
a128df2f670e explicit check of background theory;
wenzelm
parents: 54883
diff changeset
   212
            val _ =
65458
cf504b7a7aa7 tuned signature;
wenzelm
parents: 64567
diff changeset
   213
              Context.subthy_id (Thm.theory_id st, Context.theory_id thy) orelse
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59564
diff changeset
   214
                err "Bad background theory of goal state";
54567
cfe53047dc16 more uniform / rigid checking of Goal.prove_common vs. Proof.conclude_goal -- NB: Goal.prove_common cannot check hyps right now, e.g. due to undeclared Simplifier prems;
wenzelm
parents: 53192
diff changeset
   215
            val res =
cfe53047dc16 more uniform / rigid checking of Goal.prove_common vs. Proof.conclude_goal -- NB: Goal.prove_common cannot check hyps right now, e.g. due to undeclared Simplifier prems;
wenzelm
parents: 53192
diff changeset
   216
              (finish ctxt' st
58950
d07464875dd4 optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents: 58837
diff changeset
   217
                |> Drule.flexflex_unique (SOME ctxt')
61508
2c7e2ae6173d clarified modules;
wenzelm
parents: 60948
diff changeset
   218
                |> Thm.check_shyps ctxt'
54994
8e98d67325b1 reactivate Thm.check_hyps, after adapting AFP/Datatype_Order_Generator (see AFP/b7e389b5765c);
wenzelm
parents: 54993
diff changeset
   219
                |> Thm.check_hyps (Context.Proof ctxt'))
54567
cfe53047dc16 more uniform / rigid checking of Goal.prove_common vs. Proof.conclude_goal -- NB: Goal.prove_common cannot check hyps right now, e.g. due to undeclared Simplifier prems;
wenzelm
parents: 53192
diff changeset
   220
              handle THM (msg, _, _) => err msg | ERROR msg => err msg;
cfe53047dc16 more uniform / rigid checking of Goal.prove_common vs. Proof.conclude_goal -- NB: Goal.prove_common cannot check hyps right now, e.g. due to undeclared Simplifier prems;
wenzelm
parents: 53192
diff changeset
   221
          in
58950
d07464875dd4 optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents: 58837
diff changeset
   222
            if Unify.matches_list (Context.Proof ctxt') [Thm.term_of stmt] [Thm.prop_of res]
d07464875dd4 optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents: 58837
diff changeset
   223
            then res
54567
cfe53047dc16 more uniform / rigid checking of Goal.prove_common vs. Proof.conclude_goal -- NB: Goal.prove_common cannot check hyps right now, e.g. due to undeclared Simplifier prems;
wenzelm
parents: 53192
diff changeset
   224
            else err ("Proved a different theorem: " ^ Syntax.string_of_term ctxt' (Thm.prop_of res))
28340
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
   225
          end);
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
   226
    val res =
53192
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 53190
diff changeset
   227
      if immediate orelse schematic orelse not future orelse skip then result ()
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 53190
diff changeset
   228
      else
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 53190
diff changeset
   229
        future_result ctxt'
59564
fdc03c8daacc Goal.prove_multi is superseded by the fully general Goal.prove_common;
wenzelm
parents: 59498
diff changeset
   230
          (Execution.fork {name = "Goal.prove", pos = Position.thread_data (), pri = the fork_pri}
fdc03c8daacc Goal.prove_multi is superseded by the fully general Goal.prove_common;
wenzelm
parents: 59498
diff changeset
   231
            result)
53192
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 53190
diff changeset
   232
          (Thm.term_of stmt);
17980
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
   233
  in
60722
a8babbb6d5ea normalize proof before splitting conjunctions, according to Proof.conclude_goal (see also 4dd0ba632e40) -- may reduce general resource usage;
wenzelm
parents: 60695
diff changeset
   234
    res
64567
7141a3a4dc83 always close derivation, for significantly improved performance without parallel proofs;
wenzelm
parents: 64556
diff changeset
   235
    |> Thm.close_derivation
60722
a8babbb6d5ea normalize proof before splitting conjunctions, according to Proof.conclude_goal (see also 4dd0ba632e40) -- may reduce general resource usage;
wenzelm
parents: 60695
diff changeset
   236
    |> Conjunction.elim_balanced (length props)
20290
3f886c176c9b normalized Proof.context/method type aliases;
wenzelm
parents: 20260
diff changeset
   237
    |> map (Assumption.export false ctxt' ctxt)
20056
0698a403a066 prove/prove_multi: context;
wenzelm
parents: 19862
diff changeset
   238
    |> Variable.export ctxt' ctxt
20250
c3f209752749 prove: proper assumption context, more tactic arguments;
wenzelm
parents: 20228
diff changeset
   239
    |> map Drule.zero_var_indexes
17980
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
   240
  end;
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
   241
59564
fdc03c8daacc Goal.prove_multi is superseded by the fully general Goal.prove_common;
wenzelm
parents: 59498
diff changeset
   242
fun prove_future_pri ctxt pri xs asms prop tac =
fdc03c8daacc Goal.prove_multi is superseded by the fully general Goal.prove_common;
wenzelm
parents: 59498
diff changeset
   243
  hd (prove_common ctxt (SOME pri) xs asms [prop] tac);
17980
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
   244
59564
fdc03c8daacc Goal.prove_multi is superseded by the fully general Goal.prove_common;
wenzelm
parents: 59498
diff changeset
   245
fun prove_future ctxt = prove_future_pri ctxt ~1;
51118
32a5994dd205 tuned signature -- legacy packages might want to fork proofs as well;
wenzelm
parents: 51110
diff changeset
   246
59564
fdc03c8daacc Goal.prove_multi is superseded by the fully general Goal.prove_common;
wenzelm
parents: 59498
diff changeset
   247
fun prove ctxt xs asms prop tac = hd (prove_common ctxt NONE xs asms [prop] tac);
20056
0698a403a066 prove/prove_multi: context;
wenzelm
parents: 19862
diff changeset
   248
51118
32a5994dd205 tuned signature -- legacy packages might want to fork proofs as well;
wenzelm
parents: 51110
diff changeset
   249
fun prove_global_future thy xs asms prop tac =
32a5994dd205 tuned signature -- legacy packages might want to fork proofs as well;
wenzelm
parents: 51110
diff changeset
   250
  Drule.export_without_context (prove_future (Proof_Context.init_global thy) xs asms prop tac);
32a5994dd205 tuned signature -- legacy packages might want to fork proofs as well;
wenzelm
parents: 51110
diff changeset
   251
20056
0698a403a066 prove/prove_multi: context;
wenzelm
parents: 19862
diff changeset
   252
fun prove_global thy xs asms prop tac =
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 41819
diff changeset
   253
  Drule.export_without_context (prove (Proof_Context.init_global thy) xs asms prop tac);
18027
09ab79d4e8e1 renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents: 17986
diff changeset
   254
61527
d05f3d86a758 tuned signature -- clarified modules;
wenzelm
parents: 61508
diff changeset
   255
d05f3d86a758 tuned signature -- clarified modules;
wenzelm
parents: 61508
diff changeset
   256
(* skip proofs *)
d05f3d86a758 tuned signature -- clarified modules;
wenzelm
parents: 61508
diff changeset
   257
64556
851ae0e7b09c more symbols;
wenzelm
parents: 61527
diff changeset
   258
val quick_and_dirty_raw = Config.declare_option ("quick_and_dirty", \<^here>);
61527
d05f3d86a758 tuned signature -- clarified modules;
wenzelm
parents: 61508
diff changeset
   259
val quick_and_dirty = Config.bool quick_and_dirty_raw;
d05f3d86a758 tuned signature -- clarified modules;
wenzelm
parents: 61508
diff changeset
   260
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51423
diff changeset
   261
fun prove_sorry ctxt xs asms prop tac =
52059
2f970c7f722b proper option quick_and_dirty;
wenzelm
parents: 51958
diff changeset
   262
  if Config.get ctxt quick_and_dirty then
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58963
diff changeset
   263
    prove ctxt xs asms prop (fn _ => ALLGOALS (Skip_Proof.cheat_tac ctxt))
59564
fdc03c8daacc Goal.prove_multi is superseded by the fully general Goal.prove_common;
wenzelm
parents: 59498
diff changeset
   264
  else (if future_enabled 1 then prove_future_pri ctxt ~2 else prove ctxt) xs asms prop tac;
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51423
diff changeset
   265
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51423
diff changeset
   266
fun prove_sorry_global thy xs asms prop tac =
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51423
diff changeset
   267
  Drule.export_without_context
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51423
diff changeset
   268
    (prove_sorry (Proof_Context.init_global thy) xs asms prop tac);
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51423
diff changeset
   269
18027
09ab79d4e8e1 renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents: 17986
diff changeset
   270
17980
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
   271
21687
f689f729afab reorganized structure Goal vs. Tactic;
wenzelm
parents: 21604
diff changeset
   272
(** goal structure **)
f689f729afab reorganized structure Goal vs. Tactic;
wenzelm
parents: 21604
diff changeset
   273
52458
210bca64b894 less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
wenzelm
parents: 52456
diff changeset
   274
(* rearrange subgoals *)
210bca64b894 less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
wenzelm
parents: 52456
diff changeset
   275
210bca64b894 less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
wenzelm
parents: 52456
diff changeset
   276
fun restrict i n st =
210bca64b894 less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
wenzelm
parents: 52456
diff changeset
   277
  if i < 1 orelse n < 1 orelse i + n - 1 > Thm.nprems_of st
210bca64b894 less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
wenzelm
parents: 52456
diff changeset
   278
  then raise THM ("Goal.restrict", i, [st])
210bca64b894 less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
wenzelm
parents: 52456
diff changeset
   279
  else rotate_prems (i - 1) st |> protect n;
210bca64b894 less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
wenzelm
parents: 52456
diff changeset
   280
210bca64b894 less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
wenzelm
parents: 52456
diff changeset
   281
fun unrestrict i = conclude #> rotate_prems (1 - i);
210bca64b894 less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
wenzelm
parents: 52456
diff changeset
   282
210bca64b894 less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
wenzelm
parents: 52456
diff changeset
   283
(*with structural marker*)
17980
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
   284
fun SELECT_GOAL tac i st =
19191
56cda3ec2ef8 SELECT_GOAL: fixed trivial case;
wenzelm
parents: 19184
diff changeset
   285
  if Thm.nprems_of st = 1 andalso i = 1 then tac st
52458
210bca64b894 less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
wenzelm
parents: 52456
diff changeset
   286
  else (PRIMITIVE (restrict i 1) THEN tac THEN PRIMITIVE (unrestrict i)) st;
210bca64b894 less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
wenzelm
parents: 52456
diff changeset
   287
210bca64b894 less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
wenzelm
parents: 52456
diff changeset
   288
(*without structural marker*)
210bca64b894 less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
wenzelm
parents: 52456
diff changeset
   289
fun PREFER_GOAL tac i st =
210bca64b894 less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
wenzelm
parents: 52456
diff changeset
   290
  if i < 1 orelse i > Thm.nprems_of st then Seq.empty
210bca64b894 less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
wenzelm
parents: 52456
diff changeset
   291
  else (PRIMITIVE (rotate_prems (i - 1)) THEN tac THEN PRIMITIVE (rotate_prems (1 - i))) st;
17980
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
   292
21687
f689f729afab reorganized structure Goal vs. Tactic;
wenzelm
parents: 21604
diff changeset
   293
f689f729afab reorganized structure Goal vs. Tactic;
wenzelm
parents: 21604
diff changeset
   294
(* multiple goals *)
f689f729afab reorganized structure Goal vs. Tactic;
wenzelm
parents: 21604
diff changeset
   295
23418
c195f6f13769 balanced conjunctions;
wenzelm
parents: 23414
diff changeset
   296
fun precise_conjunction_tac 0 i = eq_assume_tac i
c195f6f13769 balanced conjunctions;
wenzelm
parents: 23414
diff changeset
   297
  | precise_conjunction_tac 1 i = SUBGOAL (K all_tac) i
c195f6f13769 balanced conjunctions;
wenzelm
parents: 23414
diff changeset
   298
  | precise_conjunction_tac n i = PRIMITIVE (Drule.with_subgoal i (Conjunction.curry_balanced n));
23414
927203ad4b3a tuned conjunction tactics: slightly smaller proof terms;
wenzelm
parents: 23356
diff changeset
   299
23418
c195f6f13769 balanced conjunctions;
wenzelm
parents: 23414
diff changeset
   300
val adhoc_conjunction_tac = REPEAT_ALL_NEW
c195f6f13769 balanced conjunctions;
wenzelm
parents: 23414
diff changeset
   301
  (SUBGOAL (fn (goal, i) =>
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58963
diff changeset
   302
    if can Logic.dest_conjunction goal then resolve0_tac [Conjunction.conjunctionI] i
23418
c195f6f13769 balanced conjunctions;
wenzelm
parents: 23414
diff changeset
   303
    else no_tac));
21687
f689f729afab reorganized structure Goal vs. Tactic;
wenzelm
parents: 21604
diff changeset
   304
23418
c195f6f13769 balanced conjunctions;
wenzelm
parents: 23414
diff changeset
   305
val conjunction_tac = SUBGOAL (fn (goal, i) =>
c195f6f13769 balanced conjunctions;
wenzelm
parents: 23414
diff changeset
   306
  precise_conjunction_tac (length (Logic.dest_conjunctions goal)) i ORELSE
c195f6f13769 balanced conjunctions;
wenzelm
parents: 23414
diff changeset
   307
  TRY (adhoc_conjunction_tac i));
21687
f689f729afab reorganized structure Goal vs. Tactic;
wenzelm
parents: 21604
diff changeset
   308
23418
c195f6f13769 balanced conjunctions;
wenzelm
parents: 23414
diff changeset
   309
val recover_conjunction_tac = PRIMITIVE (fn th =>
c195f6f13769 balanced conjunctions;
wenzelm
parents: 23414
diff changeset
   310
  Conjunction.uncurry_balanced (Thm.nprems_of th) th);
23414
927203ad4b3a tuned conjunction tactics: slightly smaller proof terms;
wenzelm
parents: 23356
diff changeset
   311
927203ad4b3a tuned conjunction tactics: slightly smaller proof terms;
wenzelm
parents: 23356
diff changeset
   312
fun PRECISE_CONJUNCTS n tac =
927203ad4b3a tuned conjunction tactics: slightly smaller proof terms;
wenzelm
parents: 23356
diff changeset
   313
  SELECT_GOAL (precise_conjunction_tac n 1
927203ad4b3a tuned conjunction tactics: slightly smaller proof terms;
wenzelm
parents: 23356
diff changeset
   314
    THEN tac
23418
c195f6f13769 balanced conjunctions;
wenzelm
parents: 23414
diff changeset
   315
    THEN recover_conjunction_tac);
23414
927203ad4b3a tuned conjunction tactics: slightly smaller proof terms;
wenzelm
parents: 23356
diff changeset
   316
21687
f689f729afab reorganized structure Goal vs. Tactic;
wenzelm
parents: 21604
diff changeset
   317
fun CONJUNCTS tac =
f689f729afab reorganized structure Goal vs. Tactic;
wenzelm
parents: 21604
diff changeset
   318
  SELECT_GOAL (conjunction_tac 1
f689f729afab reorganized structure Goal vs. Tactic;
wenzelm
parents: 21604
diff changeset
   319
    THEN tac
23418
c195f6f13769 balanced conjunctions;
wenzelm
parents: 23414
diff changeset
   320
    THEN recover_conjunction_tac);
21687
f689f729afab reorganized structure Goal vs. Tactic;
wenzelm
parents: 21604
diff changeset
   321
f689f729afab reorganized structure Goal vs. Tactic;
wenzelm
parents: 21604
diff changeset
   322
f689f729afab reorganized structure Goal vs. Tactic;
wenzelm
parents: 21604
diff changeset
   323
(* hhf normal form *)
f689f729afab reorganized structure Goal vs. Tactic;
wenzelm
parents: 21604
diff changeset
   324
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 54567
diff changeset
   325
fun norm_hhf_tac ctxt =
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58963
diff changeset
   326
  resolve_tac ctxt [Drule.asm_rl]  (*cheap approximation -- thanks to builtin Logic.flatten_params*)
21687
f689f729afab reorganized structure Goal vs. Tactic;
wenzelm
parents: 21604
diff changeset
   327
  THEN' SUBGOAL (fn (t, i) =>
f689f729afab reorganized structure Goal vs. Tactic;
wenzelm
parents: 21604
diff changeset
   328
    if Drule.is_norm_hhf t then all_tac
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 54567
diff changeset
   329
    else rewrite_goal_tac ctxt Drule.norm_hhf_eqs i);
21687
f689f729afab reorganized structure Goal vs. Tactic;
wenzelm
parents: 21604
diff changeset
   330
23237
ac9d126456e1 added assume_rule_tac;
wenzelm
parents: 22902
diff changeset
   331
ac9d126456e1 added assume_rule_tac;
wenzelm
parents: 22902
diff changeset
   332
(* non-atomic goal assumptions *)
ac9d126456e1 added assume_rule_tac;
wenzelm
parents: 22902
diff changeset
   333
56245
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 55559
diff changeset
   334
fun non_atomic (Const ("Pure.imp", _) $ _ $ _) = true
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 55559
diff changeset
   335
  | non_atomic (Const ("Pure.all", _) $ _) = true
23356
dbe3731241c3 renamed prove_raw to prove_internal;
wenzelm
parents: 23237
diff changeset
   336
  | non_atomic _ = false;
dbe3731241c3 renamed prove_raw to prove_internal;
wenzelm
parents: 23237
diff changeset
   337
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 54567
diff changeset
   338
fun assume_rule_tac ctxt = norm_hhf_tac ctxt THEN' CSUBGOAL (fn (goal, i) =>
23237
ac9d126456e1 added assume_rule_tac;
wenzelm
parents: 22902
diff changeset
   339
  let
60695
757549b4bbe6 Variable.focus etc.: optional bindings provided by user;
wenzelm
parents: 60642
diff changeset
   340
    val ((_, goal'), ctxt') = Variable.focus_cterm NONE goal ctxt;
23237
ac9d126456e1 added assume_rule_tac;
wenzelm
parents: 22902
diff changeset
   341
    val goal'' = Drule.cterm_rule (singleton (Variable.export ctxt' ctxt)) goal';
23356
dbe3731241c3 renamed prove_raw to prove_internal;
wenzelm
parents: 23237
diff changeset
   342
    val Rs = filter (non_atomic o Thm.term_of) (Drule.strip_imp_prems goal'');
23237
ac9d126456e1 added assume_rule_tac;
wenzelm
parents: 22902
diff changeset
   343
    val tacs = Rs |> map (fn R =>
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58963
diff changeset
   344
      eresolve_tac ctxt [Raw_Simplifier.norm_hhf ctxt (Thm.trivial R)] THEN_ALL_NEW assume_tac ctxt);
23237
ac9d126456e1 added assume_rule_tac;
wenzelm
parents: 22902
diff changeset
   345
  in fold_rev (curry op APPEND') tacs (K no_tac) i end);
ac9d126456e1 added assume_rule_tac;
wenzelm
parents: 22902
diff changeset
   346
52461
ef4c16887f83 more scalable PARALLEL_GOALS, using more elementary retrofit;
wenzelm
parents: 52458
diff changeset
   347
end;
ef4c16887f83 more scalable PARALLEL_GOALS, using more elementary retrofit;
wenzelm
parents: 52458
diff changeset
   348
32365
9b74d0339c44 added PARALLEL_CHOICE, PARALLEL_GOALS;
wenzelm
parents: 32255
diff changeset
   349
structure Basic_Goal: BASIC_GOAL = Goal;
9b74d0339c44 added PARALLEL_CHOICE, PARALLEL_GOALS;
wenzelm
parents: 32255
diff changeset
   350
open Basic_Goal;