src/Pure/goal.ML
author wenzelm
Fri, 10 Jan 2014 23:42:18 +0100
changeset 54985 9a1710a64412
parent 54984 da70ab8531f4
child 54992 e5f4075d4c5e
permissions -rw-r--r--
disable Thm.check_hyps for now, due to remaining problems with AFP/Datatype_Order_Generator and AFP/Psi_Calculi (because of HOL-Nominal 'equivariance');
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
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32365
diff changeset
     9
  val parallel_proofs: int Unsynchronized.ref
17980
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
    10
  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
    11
  val PREFER_GOAL: tactic -> int -> tactic
23418
c195f6f13769 balanced conjunctions;
wenzelm
parents: 23414
diff changeset
    12
  val CONJUNCTS: tactic -> int -> tactic
23414
927203ad4b3a tuned conjunction tactics: slightly smaller proof terms;
wenzelm
parents: 23356
diff changeset
    13
  val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
32365
9b74d0339c44 added PARALLEL_CHOICE, PARALLEL_GOALS;
wenzelm
parents: 32255
diff changeset
    14
  val PARALLEL_CHOICE: tactic list -> tactic
9b74d0339c44 added PARALLEL_CHOICE, PARALLEL_GOALS;
wenzelm
parents: 32255
diff changeset
    15
  val PARALLEL_GOALS: tactic -> tactic
17980
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
    16
end;
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
    17
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
    18
signature GOAL =
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
    19
sig
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
    20
  include BASIC_GOAL
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
    21
  val init: cterm -> thm
52456
960202346d0c tuned signature;
wenzelm
parents: 52223
diff changeset
    22
  val protect: int -> thm -> thm
17980
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
    23
  val conclude: thm -> thm
49845
9b19c0e81166 tuned signature;
wenzelm
parents: 49830
diff changeset
    24
  val check_finished: Proof.context -> thm -> thm
32197
bc341bbe4417 Goal.finish: explicit context for printing;
wenzelm
parents: 32187
diff changeset
    25
  val finish: Proof.context -> thm -> thm
54883
dd04a8b654fc proper context for norm_hhf and derived operations;
wenzelm
parents: 54742
diff changeset
    26
  val norm_result: Proof.context -> thm -> thm
52499
812215680f6d clarified Proofterm.proofs vs. Goal.skip_proofs;
wenzelm
parents: 52461
diff changeset
    27
  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
    28
  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
    29
  val future_enabled_timing: Time.time -> bool
28973
c549650d1442 future proofs: pass actual futures to facilitate composite computations;
wenzelm
parents: 28619
diff changeset
    30
  val future_result: Proof.context -> thm future -> term -> thm
54883
dd04a8b654fc proper context for norm_hhf and derived operations;
wenzelm
parents: 54742
diff changeset
    31
  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
    32
  val is_schematic: term -> bool
20290
3f886c176c9b normalized Proof.context/method type aliases;
wenzelm
parents: 20260
diff changeset
    33
  val prove_multi: Proof.context -> string list -> term list -> term list ->
3f886c176c9b normalized Proof.context/method type aliases;
wenzelm
parents: 20260
diff changeset
    34
    ({prems: thm list, context: Proof.context} -> tactic) -> thm list
28446
a01de3b3fa2e renamed promise to future, tuned related interfaces;
wenzelm
parents: 28363
diff changeset
    35
  val prove_future: Proof.context -> string list -> term list -> term ->
28340
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
    36
    ({prems: thm list, context: Proof.context} -> tactic) -> thm
20290
3f886c176c9b normalized Proof.context/method type aliases;
wenzelm
parents: 20260
diff changeset
    37
  val prove: Proof.context -> string list -> term list -> term ->
3f886c176c9b normalized Proof.context/method type aliases;
wenzelm
parents: 20260
diff changeset
    38
    ({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
    39
  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
    40
    ({prems: thm list, context: Proof.context} -> tactic) -> thm
26713
1c6181def1d0 prove_global: Variable.set_body true, pass context;
wenzelm
parents: 26628
diff changeset
    41
  val prove_global: theory -> string list -> term list -> term ->
1c6181def1d0 prove_global: Variable.set_body true, pass context;
wenzelm
parents: 26628
diff changeset
    42
    ({prems: thm list, context: Proof.context} -> tactic) -> thm
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
*)
20290
3f886c176c9b normalized Proof.context/method type aliases;
wenzelm
parents: 20260
diff changeset
    65
val init =
22902
ac833b4bb7ee moved some Drule operations to Thm (see more_thm.ML);
wenzelm
parents: 21687
diff changeset
    66
  let val A = #1 (Thm.dest_implies (Thm.cprop_of Drule.protectI))
20290
3f886c176c9b normalized Proof.context/method type aliases;
wenzelm
parents: 20260
diff changeset
    67
  in fn C => Thm.instantiate ([], [(A, C)]) Drule.protectI end;
17980
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
    68
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
    69
(*
52456
960202346d0c tuned signature;
wenzelm
parents: 52223
diff changeset
    70
  A1 ==> ... ==> An ==> C
960202346d0c tuned signature;
wenzelm
parents: 52223
diff changeset
    71
  ------------------------ (protect n)
960202346d0c tuned signature;
wenzelm
parents: 52223
diff changeset
    72
  A1 ==> ... ==> An ==> #C
17980
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
    73
*)
52456
960202346d0c tuned signature;
wenzelm
parents: 52223
diff changeset
    74
fun protect n th = Drule.comp_no_flatten (th, n) 1 Drule.protectI;
17980
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
    75
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
    76
(*
18027
09ab79d4e8e1 renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents: 17986
diff changeset
    77
  A ==> ... ==> #C
09ab79d4e8e1 renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents: 17986
diff changeset
    78
  ---------------- (conclude)
17980
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
    79
  A ==> ... ==> C
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
    80
*)
29345
5904873d8f11 tuned protect, conclude: Drule.comp_no_flatten;
wenzelm
parents: 29343
diff changeset
    81
fun conclude th = Drule.comp_no_flatten (th, Thm.nprems_of th) 1 Drule.protectD;
17980
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
    82
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
    83
(*
18027
09ab79d4e8e1 renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents: 17986
diff changeset
    84
  #C
09ab79d4e8e1 renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents: 17986
diff changeset
    85
  --- (finish)
09ab79d4e8e1 renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents: 17986
diff changeset
    86
   C
17983
wenzelm
parents: 17980
diff changeset
    87
*)
32197
bc341bbe4417 Goal.finish: explicit context for printing;
wenzelm
parents: 32187
diff changeset
    88
fun check_finished ctxt th =
51608
wenzelm
parents: 51607
diff changeset
    89
  if Thm.no_prems th then th
wenzelm
parents: 51607
diff changeset
    90
  else
51958
bca32217b304 retain goal display options when printing error messages, to avoid breakdown for huge goals;
wenzelm
parents: 51608
diff changeset
    91
    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
    92
49845
9b19c0e81166 tuned signature;
wenzelm
parents: 49830
diff changeset
    93
fun finish ctxt = check_finished ctxt #> conclude;
17980
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
    94
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
    95
18027
09ab79d4e8e1 renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents: 17986
diff changeset
    96
09ab79d4e8e1 renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents: 17986
diff changeset
    97
(** results **)
09ab79d4e8e1 renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents: 17986
diff changeset
    98
28340
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
    99
(* normal form *)
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
   100
54883
dd04a8b654fc proper context for norm_hhf and derived operations;
wenzelm
parents: 54742
diff changeset
   101
fun norm_result ctxt =
21604
1af327306c8e added norm/close_result (supercede local_standard etc.);
wenzelm
parents: 21579
diff changeset
   102
  Drule.flexflex_unique
54883
dd04a8b654fc proper context for norm_hhf and derived operations;
wenzelm
parents: 54742
diff changeset
   103
  #> Raw_Simplifier.norm_hhf_protect ctxt
21604
1af327306c8e added norm/close_result (supercede local_standard etc.);
wenzelm
parents: 21579
diff changeset
   104
  #> Thm.strip_shyps
1af327306c8e added norm/close_result (supercede local_standard etc.);
wenzelm
parents: 21579
diff changeset
   105
  #> Drule.zero_var_indexes;
1af327306c8e added norm/close_result (supercede local_standard etc.);
wenzelm
parents: 21579
diff changeset
   106
1af327306c8e added norm/close_result (supercede local_standard etc.);
wenzelm
parents: 21579
diff changeset
   107
41703
d27950860514 parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents: 41683
diff changeset
   108
(* scheduling parameters *)
d27950860514 parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents: 41683
diff changeset
   109
52499
812215680f6d clarified Proofterm.proofs vs. Goal.skip_proofs;
wenzelm
parents: 52461
diff changeset
   110
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
   111
  let val skip = Options.default_bool "skip_proofs" in
52499
812215680f6d clarified Proofterm.proofs vs. Goal.skip_proofs;
wenzelm
parents: 52461
diff changeset
   112
    if Proofterm.proofs_enabled () andalso skip then
812215680f6d clarified Proofterm.proofs vs. Goal.skip_proofs;
wenzelm
parents: 52461
diff changeset
   113
      (warning "Proof terms enabled -- cannot skip proofs"; false)
812215680f6d clarified Proofterm.proofs vs. Goal.skip_proofs;
wenzelm
parents: 52461
diff changeset
   114
    else skip
812215680f6d clarified Proofterm.proofs vs. Goal.skip_proofs;
wenzelm
parents: 52461
diff changeset
   115
  end;
812215680f6d clarified Proofterm.proofs vs. Goal.skip_proofs;
wenzelm
parents: 52461
diff changeset
   116
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32365
diff changeset
   117
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
   118
53189
ee8b8dafef0e discontinued parallel_subproofs_saturation and related internal counters (superseded by parallel_subproofs_threshold and timing information);
wenzelm
parents: 52811
diff changeset
   119
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
   120
  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
   121
  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
   122
51423
e5f9a6d9ca82 clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents: 51276
diff changeset
   123
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
   124
  future_enabled 1 andalso
52104
250cd2a9308d proper options;
wenzelm
parents: 52059
diff changeset
   125
    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
   126
34b9652b2f45 added Goal.future_enabled abstraction -- now also checks that this is already
wenzelm
parents: 29435
diff changeset
   127
28446
a01de3b3fa2e renamed promise to future, tuned related interfaces;
wenzelm
parents: 28363
diff changeset
   128
(* future_result *)
28340
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
   129
28446
a01de3b3fa2e renamed promise to future, tuned related interfaces;
wenzelm
parents: 28363
diff changeset
   130
fun future_result ctxt result prop =
28340
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
   131
  let
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 41819
diff changeset
   132
    val thy = Proof_Context.theory_of ctxt;
28340
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
   133
    val cert = Thm.cterm_of thy;
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
   134
    val certT = Thm.ctyp_of thy;
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
   135
30473
e0b66c11e7e4 Assumption.all_prems_of, Assumption.all_assms_of;
wenzelm
parents: 29448
diff changeset
   136
    val assms = Assumption.all_assms_of ctxt;
28340
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
   137
    val As = map Thm.term_of assms;
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 xs = map Free (fold Term.add_frees (prop :: As) []);
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
   140
    val fixes = map cert xs;
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
   141
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
   142
    val tfrees = fold Term.add_tfrees (prop :: As) [];
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
   143
    val instT = map (fn (a, S) => (certT (TVar ((a, 0), S)), certT (TFree (a, S)))) tfrees;
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
   144
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
   145
    val global_prop =
45344
e209da839ff4 added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
wenzelm
parents: 44302
diff changeset
   146
      cert (Logic.varify_types_global (fold_rev Logic.all xs (Logic.list_implies (As, prop))))
32056
f4b74cbecdaf future_result: explicitly impose Variable.sorts_of again;
wenzelm
parents: 30473
diff changeset
   147
      |> Thm.weaken_sorts (Variable.sorts_of ctxt);
28973
c549650d1442 future proofs: pass actual futures to facilitate composite computations;
wenzelm
parents: 28619
diff changeset
   148
    val global_result = result |> Future.map
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
   149
      (Drule.flexflex_unique #>
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
   150
        Thm.adjust_maxidx_thm ~1 #>
28973
c549650d1442 future proofs: pass actual futures to facilitate composite computations;
wenzelm
parents: 28619
diff changeset
   151
        Drule.implies_intr_list assms #>
c549650d1442 future proofs: pass actual futures to facilitate composite computations;
wenzelm
parents: 28619
diff changeset
   152
        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
   153
        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
   154
        Thm.strip_shyps);
28340
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
   155
    val local_result =
32056
f4b74cbecdaf future_result: explicitly impose Variable.sorts_of again;
wenzelm
parents: 30473
diff changeset
   156
      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
   157
      |> Thm.close_derivation
28340
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
   158
      |> Thm.instantiate (instT, [])
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
   159
      |> Drule.forall_elim_list fixes
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
   160
      |> fold (Thm.elim_implies o Thm.assume) assms;
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
   161
  in local_result end;
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
   162
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
   163
18027
09ab79d4e8e1 renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents: 17986
diff changeset
   164
09ab79d4e8e1 renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents: 17986
diff changeset
   165
(** tactical theorem proving **)
09ab79d4e8e1 renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents: 17986
diff changeset
   166
23356
dbe3731241c3 renamed prove_raw to prove_internal;
wenzelm
parents: 23237
diff changeset
   167
(* prove_internal -- minimal checks, no normalization of result! *)
20250
c3f209752749 prove: proper assumption context, more tactic arguments;
wenzelm
parents: 20228
diff changeset
   168
54883
dd04a8b654fc proper context for norm_hhf and derived operations;
wenzelm
parents: 54742
diff changeset
   169
fun prove_internal ctxt casms cprop tac =
dd04a8b654fc proper context for norm_hhf and derived operations;
wenzelm
parents: 54742
diff changeset
   170
  (case SINGLE (tac (map (Assumption.assume ctxt) casms)) (init cprop) of
32197
bc341bbe4417 Goal.finish: explicit context for printing;
wenzelm
parents: 32187
diff changeset
   171
    SOME th => Drule.implies_intr_list casms
bc341bbe4417 Goal.finish: explicit context for printing;
wenzelm
parents: 32187
diff changeset
   172
      (finish (Syntax.init_pretty_global (Thm.theory_of_thm th)) th)
38875
c7a66b584147 tuned messages: discontinued spurious full-stops (messages are occasionally composed unexpectedly);
wenzelm
parents: 38236
diff changeset
   173
  | NONE => error "Tactic failed");
20250
c3f209752749 prove: proper assumption context, more tactic arguments;
wenzelm
parents: 20228
diff changeset
   174
c3f209752749 prove: proper assumption context, more tactic arguments;
wenzelm
parents: 20228
diff changeset
   175
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
   176
(* 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
   177
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
   178
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
   179
  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
   180
  Term.exists_type (Term.exists_subtype Term.is_TVar) t;
17986
0450847646c3 prove_raw: cterms, explicit asms;
wenzelm
parents: 17983
diff changeset
   181
52811
dae6c61f991e clarified priority of "skipped" proofs, which might take long but do not produce relevant information (potential conflict of quick interactive feedback vs. performance in batch mode);
wenzelm
parents: 52775
diff changeset
   182
fun prove_common immediate pri ctxt xs asms props tac =
17980
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
   183
  let
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 41819
diff changeset
   184
    val thy = Proof_Context.theory_of ctxt;
20056
0698a403a066 prove/prove_multi: context;
wenzelm
parents: 19862
diff changeset
   185
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
   186
    val schematic = exists is_schematic props;
53189
ee8b8dafef0e discontinued parallel_subproofs_saturation and related internal counters (superseded by parallel_subproofs_threshold and timing information);
wenzelm
parents: 52811
diff changeset
   187
    val future = future_enabled 1;
52499
812215680f6d clarified Proofterm.proofs vs. Goal.skip_proofs;
wenzelm
parents: 52461
diff changeset
   188
    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
   189
28355
b9d9360e2440 prove: error with original thread position;
wenzelm
parents: 28341
diff changeset
   190
    val pos = Position.thread_data ();
20250
c3f209752749 prove: proper assumption context, more tactic arguments;
wenzelm
parents: 20228
diff changeset
   191
    fun err msg = cat_error msg
c3f209752749 prove: proper assumption context, more tactic arguments;
wenzelm
parents: 20228
diff changeset
   192
      ("The error(s) above occurred for the goal statement:\n" ^
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
   193
        Syntax.string_of_term ctxt (Logic.list_implies (asms, Logic.mk_conjunction_list props)) ^
48992
0518bf89c777 renamed Position.str_of to Position.here;
wenzelm
parents: 47415
diff changeset
   194
        (case Position.here pos of "" => "" | s => "\n" ^ s));
17980
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
   195
20250
c3f209752749 prove: proper assumption context, more tactic arguments;
wenzelm
parents: 20228
diff changeset
   196
    fun cert_safe t = Thm.cterm_of thy (Envir.beta_norm (Term.no_dummy_patterns t))
17980
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
   197
      handle TERM (msg, _) => err msg | TYPE (msg, _, _) => err msg;
20250
c3f209752749 prove: proper assumption context, more tactic arguments;
wenzelm
parents: 20228
diff changeset
   198
    val casms = map cert_safe asms;
c3f209752749 prove: proper assumption context, more tactic arguments;
wenzelm
parents: 20228
diff changeset
   199
    val cprops = map cert_safe props;
17980
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
   200
20250
c3f209752749 prove: proper assumption context, more tactic arguments;
wenzelm
parents: 20228
diff changeset
   201
    val (prems, ctxt') = ctxt
c3f209752749 prove: proper assumption context, more tactic arguments;
wenzelm
parents: 20228
diff changeset
   202
      |> Variable.add_fixes_direct xs
27218
4548c83cd508 prove: full Variable.declare_term, including constraints;
wenzelm
parents: 26939
diff changeset
   203
      |> fold Variable.declare_term (asms @ props)
26713
1c6181def1d0 prove_global: Variable.set_body true, pass context;
wenzelm
parents: 26628
diff changeset
   204
      |> Assumption.add_assumes casms
1c6181def1d0 prove_global: Variable.set_body true, pass context;
wenzelm
parents: 26628
diff changeset
   205
      ||> Variable.set_body true;
28619
89f9dd800a22 prove_common: include all sorts from context into statement, check shyps of result;
wenzelm
parents: 28446
diff changeset
   206
    val sorts = Variable.sorts_of ctxt';
17980
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
   207
28619
89f9dd800a22 prove_common: include all sorts from context into statement, check shyps of result;
wenzelm
parents: 28446
diff changeset
   208
    val stmt = Thm.weaken_sorts sorts (Conjunction.mk_conjunction_balanced cprops);
28340
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
   209
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
   210
    fun tac' args st =
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
   211
      if skip then ALLGOALS Skip_Proof.cheat_tac st before Skip_Proof.report ctxt
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
   212
      else tac args st;
28340
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
   213
    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
   214
      (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
   215
        NONE => err "Tactic failed"
28340
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
   216
      | 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
   217
          let
54981
a128df2f670e explicit check of background theory;
wenzelm
parents: 54883
diff changeset
   218
            val _ =
a128df2f670e explicit check of background theory;
wenzelm
parents: 54883
diff changeset
   219
              Theory.subthy (theory_of_thm st, thy) orelse 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
   220
            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
   221
              (finish ctxt' st
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
   222
                |> Drule.flexflex_unique
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
   223
                |> Thm.check_shyps sorts
54985
9a1710a64412 disable Thm.check_hyps for now, due to remaining problems with AFP/Datatype_Order_Generator and AFP/Psi_Calculi (because of HOL-Nominal 'equivariance');
wenzelm
parents: 54984
diff changeset
   224
                (* |> Thm.check_hyps ctxt' *) (* FIXME *))
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
   225
              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
   226
          in
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
   227
            if Unify.matches_list thy [Thm.term_of stmt] [Thm.prop_of res] then 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
   228
            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
   229
          end);
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
   230
    val res =
53192
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 53190
diff changeset
   231
      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
   232
      else
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 53190
diff changeset
   233
        future_result ctxt'
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 53190
diff changeset
   234
          (Execution.fork {name = "Goal.prove", pos = Position.thread_data (), pri = pri} result)
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 53190
diff changeset
   235
          (Thm.term_of stmt);
17980
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
   236
  in
28340
e8597242f649 added promise_result, prove_promise;
wenzelm
parents: 27218
diff changeset
   237
    Conjunction.elim_balanced (length props) res
20290
3f886c176c9b normalized Proof.context/method type aliases;
wenzelm
parents: 20260
diff changeset
   238
    |> map (Assumption.export false ctxt' ctxt)
20056
0698a403a066 prove/prove_multi: context;
wenzelm
parents: 19862
diff changeset
   239
    |> Variable.export ctxt' ctxt
20250
c3f209752749 prove: proper assumption context, more tactic arguments;
wenzelm
parents: 20228
diff changeset
   240
    |> map Drule.zero_var_indexes
17980
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
   241
  end;
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
   242
52811
dae6c61f991e clarified priority of "skipped" proofs, which might take long but do not produce relevant information (potential conflict of quick interactive feedback vs. performance in batch mode);
wenzelm
parents: 52775
diff changeset
   243
val prove_multi = prove_common true 0;
17980
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
   244
52811
dae6c61f991e clarified priority of "skipped" proofs, which might take long but do not produce relevant information (potential conflict of quick interactive feedback vs. performance in batch mode);
wenzelm
parents: 52775
diff changeset
   245
fun prove_future_pri pri ctxt xs asms prop tac =
dae6c61f991e clarified priority of "skipped" proofs, which might take long but do not produce relevant information (potential conflict of quick interactive feedback vs. performance in batch mode);
wenzelm
parents: 52775
diff changeset
   246
  hd (prove_common false pri ctxt xs asms [prop] tac);
51118
32a5994dd205 tuned signature -- legacy packages might want to fork proofs as well;
wenzelm
parents: 51110
diff changeset
   247
52811
dae6c61f991e clarified priority of "skipped" proofs, which might take long but do not produce relevant information (potential conflict of quick interactive feedback vs. performance in batch mode);
wenzelm
parents: 52775
diff changeset
   248
val prove_future = prove_future_pri ~1;
dae6c61f991e clarified priority of "skipped" proofs, which might take long but do not produce relevant information (potential conflict of quick interactive feedback vs. performance in batch mode);
wenzelm
parents: 52775
diff changeset
   249
dae6c61f991e clarified priority of "skipped" proofs, which might take long but do not produce relevant information (potential conflict of quick interactive feedback vs. performance in batch mode);
wenzelm
parents: 52775
diff changeset
   250
fun prove ctxt xs asms prop tac = hd (prove_multi ctxt xs asms [prop] tac);
20056
0698a403a066 prove/prove_multi: context;
wenzelm
parents: 19862
diff changeset
   251
51118
32a5994dd205 tuned signature -- legacy packages might want to fork proofs as well;
wenzelm
parents: 51110
diff changeset
   252
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
   253
  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
   254
20056
0698a403a066 prove/prove_multi: context;
wenzelm
parents: 19862
diff changeset
   255
fun prove_global thy xs asms prop tac =
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 41819
diff changeset
   256
  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
   257
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51423
diff changeset
   258
fun prove_sorry ctxt xs asms prop tac =
52059
2f970c7f722b proper option quick_and_dirty;
wenzelm
parents: 51958
diff changeset
   259
  if Config.get ctxt quick_and_dirty then
51552
c713c9505f68 clarified Skip_Proof.cheat_tac: more standard tactic;
wenzelm
parents: 51551
diff changeset
   260
    prove ctxt xs asms prop (fn _ => ALLGOALS Skip_Proof.cheat_tac)
53189
ee8b8dafef0e discontinued parallel_subproofs_saturation and related internal counters (superseded by parallel_subproofs_threshold and timing information);
wenzelm
parents: 52811
diff changeset
   261
  else (if future_enabled 1 then prove_future_pri ~2 else prove) ctxt xs asms prop tac;
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51423
diff changeset
   262
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51423
diff changeset
   263
fun prove_sorry_global thy xs asms prop tac =
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51423
diff changeset
   264
  Drule.export_without_context
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51423
diff changeset
   265
    (prove_sorry (Proof_Context.init_global thy) xs asms prop tac);
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51423
diff changeset
   266
18027
09ab79d4e8e1 renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents: 17986
diff changeset
   267
17980
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
   268
21687
f689f729afab reorganized structure Goal vs. Tactic;
wenzelm
parents: 21604
diff changeset
   269
(** goal structure **)
f689f729afab reorganized structure Goal vs. Tactic;
wenzelm
parents: 21604
diff changeset
   270
52458
210bca64b894 less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
wenzelm
parents: 52456
diff changeset
   271
(* rearrange subgoals *)
210bca64b894 less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
wenzelm
parents: 52456
diff changeset
   272
210bca64b894 less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
wenzelm
parents: 52456
diff changeset
   273
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
   274
  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
   275
  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
   276
  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
   277
210bca64b894 less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
wenzelm
parents: 52456
diff changeset
   278
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
   279
210bca64b894 less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
wenzelm
parents: 52456
diff changeset
   280
(*with structural marker*)
17980
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
   281
fun SELECT_GOAL tac i st =
19191
56cda3ec2ef8 SELECT_GOAL: fixed trivial case;
wenzelm
parents: 19184
diff changeset
   282
  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
   283
  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
   284
210bca64b894 less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
wenzelm
parents: 52456
diff changeset
   285
(*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
   286
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
   287
  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
   288
  else (PRIMITIVE (rotate_prems (i - 1)) THEN tac THEN PRIMITIVE (rotate_prems (1 - i))) st;
17980
788836292b1a Internal goals.
wenzelm
parents:
diff changeset
   289
21687
f689f729afab reorganized structure Goal vs. Tactic;
wenzelm
parents: 21604
diff changeset
   290
f689f729afab reorganized structure Goal vs. Tactic;
wenzelm
parents: 21604
diff changeset
   291
(* multiple goals *)
f689f729afab reorganized structure Goal vs. Tactic;
wenzelm
parents: 21604
diff changeset
   292
23418
c195f6f13769 balanced conjunctions;
wenzelm
parents: 23414
diff changeset
   293
fun precise_conjunction_tac 0 i = eq_assume_tac i
c195f6f13769 balanced conjunctions;
wenzelm
parents: 23414
diff changeset
   294
  | precise_conjunction_tac 1 i = SUBGOAL (K all_tac) i
c195f6f13769 balanced conjunctions;
wenzelm
parents: 23414
diff changeset
   295
  | 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
   296
23418
c195f6f13769 balanced conjunctions;
wenzelm
parents: 23414
diff changeset
   297
val adhoc_conjunction_tac = REPEAT_ALL_NEW
c195f6f13769 balanced conjunctions;
wenzelm
parents: 23414
diff changeset
   298
  (SUBGOAL (fn (goal, i) =>
c195f6f13769 balanced conjunctions;
wenzelm
parents: 23414
diff changeset
   299
    if can Logic.dest_conjunction goal then rtac Conjunction.conjunctionI i
c195f6f13769 balanced conjunctions;
wenzelm
parents: 23414
diff changeset
   300
    else no_tac));
21687
f689f729afab reorganized structure Goal vs. Tactic;
wenzelm
parents: 21604
diff changeset
   301
23418
c195f6f13769 balanced conjunctions;
wenzelm
parents: 23414
diff changeset
   302
val conjunction_tac = SUBGOAL (fn (goal, i) =>
c195f6f13769 balanced conjunctions;
wenzelm
parents: 23414
diff changeset
   303
  precise_conjunction_tac (length (Logic.dest_conjunctions goal)) i ORELSE
c195f6f13769 balanced conjunctions;
wenzelm
parents: 23414
diff changeset
   304
  TRY (adhoc_conjunction_tac i));
21687
f689f729afab reorganized structure Goal vs. Tactic;
wenzelm
parents: 21604
diff changeset
   305
23418
c195f6f13769 balanced conjunctions;
wenzelm
parents: 23414
diff changeset
   306
val recover_conjunction_tac = PRIMITIVE (fn th =>
c195f6f13769 balanced conjunctions;
wenzelm
parents: 23414
diff changeset
   307
  Conjunction.uncurry_balanced (Thm.nprems_of th) th);
23414
927203ad4b3a tuned conjunction tactics: slightly smaller proof terms;
wenzelm
parents: 23356
diff changeset
   308
927203ad4b3a tuned conjunction tactics: slightly smaller proof terms;
wenzelm
parents: 23356
diff changeset
   309
fun PRECISE_CONJUNCTS n tac =
927203ad4b3a tuned conjunction tactics: slightly smaller proof terms;
wenzelm
parents: 23356
diff changeset
   310
  SELECT_GOAL (precise_conjunction_tac n 1
927203ad4b3a tuned conjunction tactics: slightly smaller proof terms;
wenzelm
parents: 23356
diff changeset
   311
    THEN tac
23418
c195f6f13769 balanced conjunctions;
wenzelm
parents: 23414
diff changeset
   312
    THEN recover_conjunction_tac);
23414
927203ad4b3a tuned conjunction tactics: slightly smaller proof terms;
wenzelm
parents: 23356
diff changeset
   313
21687
f689f729afab reorganized structure Goal vs. Tactic;
wenzelm
parents: 21604
diff changeset
   314
fun CONJUNCTS tac =
f689f729afab reorganized structure Goal vs. Tactic;
wenzelm
parents: 21604
diff changeset
   315
  SELECT_GOAL (conjunction_tac 1
f689f729afab reorganized structure Goal vs. Tactic;
wenzelm
parents: 21604
diff changeset
   316
    THEN tac
23418
c195f6f13769 balanced conjunctions;
wenzelm
parents: 23414
diff changeset
   317
    THEN recover_conjunction_tac);
21687
f689f729afab reorganized structure Goal vs. Tactic;
wenzelm
parents: 21604
diff changeset
   318
f689f729afab reorganized structure Goal vs. Tactic;
wenzelm
parents: 21604
diff changeset
   319
f689f729afab reorganized structure Goal vs. Tactic;
wenzelm
parents: 21604
diff changeset
   320
(* hhf normal form *)
f689f729afab reorganized structure Goal vs. Tactic;
wenzelm
parents: 21604
diff changeset
   321
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 54567
diff changeset
   322
fun norm_hhf_tac ctxt =
21687
f689f729afab reorganized structure Goal vs. Tactic;
wenzelm
parents: 21604
diff changeset
   323
  rtac Drule.asm_rl  (*cheap approximation -- thanks to builtin Logic.flatten_params*)
f689f729afab reorganized structure Goal vs. Tactic;
wenzelm
parents: 21604
diff changeset
   324
  THEN' SUBGOAL (fn (t, i) =>
f689f729afab reorganized structure Goal vs. Tactic;
wenzelm
parents: 21604
diff changeset
   325
    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
   326
    else rewrite_goal_tac ctxt Drule.norm_hhf_eqs i);
21687
f689f729afab reorganized structure Goal vs. Tactic;
wenzelm
parents: 21604
diff changeset
   327
23237
ac9d126456e1 added assume_rule_tac;
wenzelm
parents: 22902
diff changeset
   328
ac9d126456e1 added assume_rule_tac;
wenzelm
parents: 22902
diff changeset
   329
(* non-atomic goal assumptions *)
ac9d126456e1 added assume_rule_tac;
wenzelm
parents: 22902
diff changeset
   330
23356
dbe3731241c3 renamed prove_raw to prove_internal;
wenzelm
parents: 23237
diff changeset
   331
fun non_atomic (Const ("==>", _) $ _ $ _) = true
dbe3731241c3 renamed prove_raw to prove_internal;
wenzelm
parents: 23237
diff changeset
   332
  | non_atomic (Const ("all", _) $ _) = true
dbe3731241c3 renamed prove_raw to prove_internal;
wenzelm
parents: 23237
diff changeset
   333
  | non_atomic _ = false;
dbe3731241c3 renamed prove_raw to prove_internal;
wenzelm
parents: 23237
diff changeset
   334
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 54567
diff changeset
   335
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
   336
  let
42495
1af81b70cf09 clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;
wenzelm
parents: 42371
diff changeset
   337
    val ((_, goal'), ctxt') = Variable.focus_cterm goal ctxt;
23237
ac9d126456e1 added assume_rule_tac;
wenzelm
parents: 22902
diff changeset
   338
    val goal'' = Drule.cterm_rule (singleton (Variable.export ctxt' ctxt)) goal';
23356
dbe3731241c3 renamed prove_raw to prove_internal;
wenzelm
parents: 23237
diff changeset
   339
    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
   340
    val tacs = Rs |> map (fn R =>
54883
dd04a8b654fc proper context for norm_hhf and derived operations;
wenzelm
parents: 54742
diff changeset
   341
      etac (Raw_Simplifier.norm_hhf ctxt (Thm.trivial R)) THEN_ALL_NEW assume_tac);
23237
ac9d126456e1 added assume_rule_tac;
wenzelm
parents: 22902
diff changeset
   342
  in fold_rev (curry op APPEND') tacs (K no_tac) i end);
ac9d126456e1 added assume_rule_tac;
wenzelm
parents: 22902
diff changeset
   343
32365
9b74d0339c44 added PARALLEL_CHOICE, PARALLEL_GOALS;
wenzelm
parents: 32255
diff changeset
   344
52461
ef4c16887f83 more scalable PARALLEL_GOALS, using more elementary retrofit;
wenzelm
parents: 52458
diff changeset
   345
ef4c16887f83 more scalable PARALLEL_GOALS, using more elementary retrofit;
wenzelm
parents: 52458
diff changeset
   346
(** parallel tacticals **)
32365
9b74d0339c44 added PARALLEL_CHOICE, PARALLEL_GOALS;
wenzelm
parents: 32255
diff changeset
   347
52461
ef4c16887f83 more scalable PARALLEL_GOALS, using more elementary retrofit;
wenzelm
parents: 52458
diff changeset
   348
(* parallel choice of single results *)
ef4c16887f83 more scalable PARALLEL_GOALS, using more elementary retrofit;
wenzelm
parents: 52458
diff changeset
   349
32365
9b74d0339c44 added PARALLEL_CHOICE, PARALLEL_GOALS;
wenzelm
parents: 32255
diff changeset
   350
fun PARALLEL_CHOICE tacs st =
9b74d0339c44 added PARALLEL_CHOICE, PARALLEL_GOALS;
wenzelm
parents: 32255
diff changeset
   351
  (case Par_List.get_some (fn tac => SINGLE tac st) tacs of
9b74d0339c44 added PARALLEL_CHOICE, PARALLEL_GOALS;
wenzelm
parents: 32255
diff changeset
   352
    NONE => Seq.empty
9b74d0339c44 added PARALLEL_CHOICE, PARALLEL_GOALS;
wenzelm
parents: 32255
diff changeset
   353
  | SOME st' => Seq.single st');
9b74d0339c44 added PARALLEL_CHOICE, PARALLEL_GOALS;
wenzelm
parents: 32255
diff changeset
   354
52461
ef4c16887f83 more scalable PARALLEL_GOALS, using more elementary retrofit;
wenzelm
parents: 52458
diff changeset
   355
ef4c16887f83 more scalable PARALLEL_GOALS, using more elementary retrofit;
wenzelm
parents: 52458
diff changeset
   356
(* parallel refinement of non-schematic goal by single results *)
ef4c16887f83 more scalable PARALLEL_GOALS, using more elementary retrofit;
wenzelm
parents: 52458
diff changeset
   357
ef4c16887f83 more scalable PARALLEL_GOALS, using more elementary retrofit;
wenzelm
parents: 52458
diff changeset
   358
local
ef4c16887f83 more scalable PARALLEL_GOALS, using more elementary retrofit;
wenzelm
parents: 52458
diff changeset
   359
32788
a65deb8f9434 PARALLEL_GOALS: proper scope for exception FAILED, with dummy argument to prevent its interpretation as variable;
wenzelm
parents: 32738
diff changeset
   360
exception FAILED of unit;
52461
ef4c16887f83 more scalable PARALLEL_GOALS, using more elementary retrofit;
wenzelm
parents: 52458
diff changeset
   361
ef4c16887f83 more scalable PARALLEL_GOALS, using more elementary retrofit;
wenzelm
parents: 52458
diff changeset
   362
fun retrofit st' =
ef4c16887f83 more scalable PARALLEL_GOALS, using more elementary retrofit;
wenzelm
parents: 52458
diff changeset
   363
  rotate_prems ~1 #>
ef4c16887f83 more scalable PARALLEL_GOALS, using more elementary retrofit;
wenzelm
parents: 52458
diff changeset
   364
  Thm.bicompose {flatten = false, match = false, incremented = false}
ef4c16887f83 more scalable PARALLEL_GOALS, using more elementary retrofit;
wenzelm
parents: 52458
diff changeset
   365
      (false, conclude st', Thm.nprems_of st') 1;
ef4c16887f83 more scalable PARALLEL_GOALS, using more elementary retrofit;
wenzelm
parents: 52458
diff changeset
   366
ef4c16887f83 more scalable PARALLEL_GOALS, using more elementary retrofit;
wenzelm
parents: 52458
diff changeset
   367
in
ef4c16887f83 more scalable PARALLEL_GOALS, using more elementary retrofit;
wenzelm
parents: 52458
diff changeset
   368
42370
244911efd275 refined PARALLEL_GOALS;
wenzelm
parents: 42360
diff changeset
   369
fun PARALLEL_GOALS tac =
244911efd275 refined PARALLEL_GOALS;
wenzelm
parents: 42360
diff changeset
   370
  Thm.adjust_maxidx_thm ~1 #>
244911efd275 refined PARALLEL_GOALS;
wenzelm
parents: 42360
diff changeset
   371
  (fn st =>
42371
5900f06b4198 enable PARALLEL_GOALS more liberally, unlike forked proofs (cf. 34b9652b2f45);
wenzelm
parents: 42370
diff changeset
   372
    if not (Multithreading.enabled ()) orelse Thm.maxidx_of st >= 0 orelse Thm.nprems_of st <= 1
42370
244911efd275 refined PARALLEL_GOALS;
wenzelm
parents: 42360
diff changeset
   373
    then DETERM tac st
244911efd275 refined PARALLEL_GOALS;
wenzelm
parents: 42360
diff changeset
   374
    else
244911efd275 refined PARALLEL_GOALS;
wenzelm
parents: 42360
diff changeset
   375
      let
244911efd275 refined PARALLEL_GOALS;
wenzelm
parents: 42360
diff changeset
   376
        fun try_tac g =
244911efd275 refined PARALLEL_GOALS;
wenzelm
parents: 42360
diff changeset
   377
          (case SINGLE tac g of
244911efd275 refined PARALLEL_GOALS;
wenzelm
parents: 42360
diff changeset
   378
            NONE => raise FAILED ()
244911efd275 refined PARALLEL_GOALS;
wenzelm
parents: 42360
diff changeset
   379
          | SOME g' => g');
32365
9b74d0339c44 added PARALLEL_CHOICE, PARALLEL_GOALS;
wenzelm
parents: 32255
diff changeset
   380
42370
244911efd275 refined PARALLEL_GOALS;
wenzelm
parents: 42360
diff changeset
   381
        val goals = Drule.strip_imp_prems (Thm.cprop_of st);
244911efd275 refined PARALLEL_GOALS;
wenzelm
parents: 42360
diff changeset
   382
        val results = Par_List.map (try_tac o init) goals;
52461
ef4c16887f83 more scalable PARALLEL_GOALS, using more elementary retrofit;
wenzelm
parents: 52458
diff changeset
   383
      in EVERY (map retrofit (rev results)) st end
42370
244911efd275 refined PARALLEL_GOALS;
wenzelm
parents: 42360
diff changeset
   384
      handle FAILED () => Seq.empty);
32365
9b74d0339c44 added PARALLEL_CHOICE, PARALLEL_GOALS;
wenzelm
parents: 32255
diff changeset
   385
18207
9edbeda7e39a tuned norm_hhf_protected;
wenzelm
parents: 18180
diff changeset
   386
end;
9edbeda7e39a tuned norm_hhf_protected;
wenzelm
parents: 18180
diff changeset
   387
52461
ef4c16887f83 more scalable PARALLEL_GOALS, using more elementary retrofit;
wenzelm
parents: 52458
diff changeset
   388
end;
ef4c16887f83 more scalable PARALLEL_GOALS, using more elementary retrofit;
wenzelm
parents: 52458
diff changeset
   389
32365
9b74d0339c44 added PARALLEL_CHOICE, PARALLEL_GOALS;
wenzelm
parents: 32255
diff changeset
   390
structure Basic_Goal: BASIC_GOAL = Goal;
9b74d0339c44 added PARALLEL_CHOICE, PARALLEL_GOALS;
wenzelm
parents: 32255
diff changeset
   391
open Basic_Goal;