src/Pure/Isar/calculation.ML
author wenzelm
Thu, 07 Aug 2008 19:21:41 +0200
changeset 27779 4569003b8813
parent 26463 9283b4185fdf
child 28210 c164d1892553
permissions -rw-r--r--
simplified Antiq: regular SymbolPos.text with position; renamed read_arguments to read_antiq; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6778
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Isar/calculation.ML
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
     4
17350
26cd3756377a more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents: 16571
diff changeset
     5
Generic calculational proofs.
6778
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
     6
*)
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
     7
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
     8
signature CALCULATION =
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
     9
sig
21506
b2a673894ce5 prefer Proof.context over Context.generic;
wenzelm
parents: 21445
diff changeset
    10
  val print_rules: Proof.context -> unit
16571
c1f41c98fd3c export get_calculation;
wenzelm
parents: 16424
diff changeset
    11
  val get_calculation: Proof.state -> thm list option
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    12
  val trans_add: attribute
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    13
  val trans_del: attribute
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    14
  val sym_add: attribute
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    15
  val sym_del: attribute
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    16
  val symmetric: attribute
26336
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26252
diff changeset
    17
  val also: (Facts.ref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq
17350
26cd3756377a more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents: 16571
diff changeset
    18
  val also_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
26336
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26252
diff changeset
    19
  val finally_: (Facts.ref * Attrib.src list) list option -> bool ->
22573
2ac646ab2f6c avoid clash with Alice keywords;
wenzelm
parents: 21506
diff changeset
    20
    Proof.state -> Proof.state Seq.seq
17350
26cd3756377a more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents: 16571
diff changeset
    21
  val finally_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
26cd3756377a more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents: 16571
diff changeset
    22
  val moreover: bool -> Proof.state -> Proof.state
26cd3756377a more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents: 16571
diff changeset
    23
  val ultimately: bool -> Proof.state -> Proof.state
6778
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    24
end;
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    25
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    26
structure Calculation: CALCULATION =
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    27
struct
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    28
18637
33a6f6caa617 generic data and attributes;
wenzelm
parents: 18377
diff changeset
    29
(** calculation data **)
6778
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    30
18637
33a6f6caa617 generic data and attributes;
wenzelm
parents: 18377
diff changeset
    31
structure CalculationData = GenericDataFun
33a6f6caa617 generic data and attributes;
wenzelm
parents: 18377
diff changeset
    32
(
12379
c74d160ff0c5 added 'sym' and 'symmetric' atts;
wenzelm
parents: 12311
diff changeset
    33
  type T = (thm NetRules.T * thm list) * (thm list * int) option;
18637
33a6f6caa617 generic data and attributes;
wenzelm
parents: 18377
diff changeset
    34
  val empty = ((NetRules.elim, []), NONE);
33a6f6caa617 generic data and attributes;
wenzelm
parents: 18377
diff changeset
    35
  val extend = I;
6778
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    36
18637
33a6f6caa617 generic data and attributes;
wenzelm
parents: 18377
diff changeset
    37
  fun merge _ (((trans1, sym1), _), ((trans2, sym2), _)) =
24039
273698405054 renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents: 22846
diff changeset
    38
    ((NetRules.merge (trans1, trans2), Thm.merge_thms (sym1, sym2)), NONE);
18637
33a6f6caa617 generic data and attributes;
wenzelm
parents: 18377
diff changeset
    39
);
33a6f6caa617 generic data and attributes;
wenzelm
parents: 18377
diff changeset
    40
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22573
diff changeset
    41
fun print_rules ctxt =
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22573
diff changeset
    42
  let val ((trans, sym), _) = CalculationData.get (Context.Proof ctxt) in
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22573
diff changeset
    43
    [Pretty.big_list "transitivity rules:"
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22573
diff changeset
    44
        (map (ProofContext.pretty_thm ctxt) (NetRules.rules trans)),
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22573
diff changeset
    45
      Pretty.big_list "symmetry rules:" (map (ProofContext.pretty_thm ctxt) sym)]
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22573
diff changeset
    46
    |> Pretty.chunks |> Pretty.writeln
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22573
diff changeset
    47
  end;
6778
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    48
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    49
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    50
(* access calculation *)
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    51
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    52
fun get_calculation state =
18637
33a6f6caa617 generic data and attributes;
wenzelm
parents: 18377
diff changeset
    53
  (case #2 (CalculationData.get (Context.Proof (Proof.context_of state))) of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
    54
    NONE => NONE
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
    55
  | SOME (thms, lev) => if lev = Proof.level state then SOME thms else NONE);
6778
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    56
17350
26cd3756377a more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents: 16571
diff changeset
    57
val calculationN = "calculation";
6778
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    58
17350
26cd3756377a more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents: 16571
diff changeset
    59
fun put_calculation calc =
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    60
  `Proof.level #-> (fn lev => Proof.map_context (Context.proof_map
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    61
     (CalculationData.map (apsnd (K (Option.map (rpair lev) calc))))))
26252
d8145f7c97b2 Proof.put_thms false;
wenzelm
parents: 24039
diff changeset
    62
  #> Proof.put_thms false (calculationN, calc);
6778
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    63
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    64
18637
33a6f6caa617 generic data and attributes;
wenzelm
parents: 18377
diff changeset
    65
6778
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    66
(** attributes **)
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    67
12379
c74d160ff0c5 added 'sym' and 'symmetric' atts;
wenzelm
parents: 12311
diff changeset
    68
(* add/del rules *)
c74d160ff0c5 added 'sym' and 'symmetric' atts;
wenzelm
parents: 12311
diff changeset
    69
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    70
val trans_add = Thm.declaration_attribute (CalculationData.map o apfst o apfst o NetRules.insert);
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    71
val trans_del = Thm.declaration_attribute (CalculationData.map o apfst o apfst o NetRules.delete);
6778
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    72
18637
33a6f6caa617 generic data and attributes;
wenzelm
parents: 18377
diff changeset
    73
val sym_add =
24039
273698405054 renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents: 22846
diff changeset
    74
  Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Thm.add_thm)
18637
33a6f6caa617 generic data and attributes;
wenzelm
parents: 18377
diff changeset
    75
  #> ContextRules.elim_query NONE;
33a6f6caa617 generic data and attributes;
wenzelm
parents: 18377
diff changeset
    76
val sym_del =
24039
273698405054 renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents: 22846
diff changeset
    77
  Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Thm.del_thm)
18637
33a6f6caa617 generic data and attributes;
wenzelm
parents: 18377
diff changeset
    78
  #> ContextRules.rule_del;
12379
c74d160ff0c5 added 'sym' and 'symmetric' atts;
wenzelm
parents: 12311
diff changeset
    79
c74d160ff0c5 added 'sym' and 'symmetric' atts;
wenzelm
parents: 12311
diff changeset
    80
18637
33a6f6caa617 generic data and attributes;
wenzelm
parents: 18377
diff changeset
    81
(* symmetric *)
12379
c74d160ff0c5 added 'sym' and 'symmetric' atts;
wenzelm
parents: 12311
diff changeset
    82
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    83
val symmetric = Thm.rule_attribute (fn x => fn th =>
19861
620d90091788 tuned Seq/Envir/Unify interfaces;
wenzelm
parents: 19074
diff changeset
    84
  (case Seq.chop 2 (Drule.multi_resolves [th] (#2 (#1 (CalculationData.get x)))) of
20898
113c9516a2d7 attribute symmetric: zero_var_indexes;
wenzelm
parents: 19861
diff changeset
    85
    ([th'], _) => Drule.zero_var_indexes th'
12379
c74d160ff0c5 added 'sym' and 'symmetric' atts;
wenzelm
parents: 12311
diff changeset
    86
  | ([], _) => raise THM ("symmetric: no unifiers", 1, [th])
c74d160ff0c5 added 'sym' and 'symmetric' atts;
wenzelm
parents: 12311
diff changeset
    87
  | _ => raise THM ("symmetric: multiple unifiers", 1, [th])));
c74d160ff0c5 added 'sym' and 'symmetric' atts;
wenzelm
parents: 12311
diff changeset
    88
6778
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    89
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    90
(* concrete syntax *)
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    91
18637
33a6f6caa617 generic data and attributes;
wenzelm
parents: 18377
diff changeset
    92
val trans_att = Attrib.add_del_args trans_add trans_del;
33a6f6caa617 generic data and attributes;
wenzelm
parents: 18377
diff changeset
    93
val sym_att = Attrib.add_del_args sym_add sym_del;
12379
c74d160ff0c5 added 'sym' and 'symmetric' atts;
wenzelm
parents: 12311
diff changeset
    94
26463
9283b4185fdf Context.>> : operate on Context.generic;
wenzelm
parents: 26435
diff changeset
    95
val _ = Context.>> (Context.map_theory
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18678
diff changeset
    96
 (Attrib.add_attributes
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    97
   [("trans", trans_att, "declaration of transitivity rule"),
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    98
    ("sym", sym_att, "declaration of symmetry rule"),
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    99
    ("symmetric", Attrib.no_args symmetric, "resolution with symmetry rule")] #>
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18678
diff changeset
   100
  PureThy.add_thms
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   101
   [(("", transitive_thm), [trans_add]),
26463
9283b4185fdf Context.>> : operate on Context.generic;
wenzelm
parents: 26435
diff changeset
   102
    (("", symmetric_thm), [sym_add])] #> snd));
15801
d2f5ca3c048d superceded by Pure.thy and CPure.thy;
wenzelm
parents: 15570
diff changeset
   103
6778
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   104
6787
wenzelm
parents: 6782
diff changeset
   105
6778
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   106
(** proof commands **)
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   107
18678
dd0c569fa43d sane ERROR handling;
wenzelm
parents: 18637
diff changeset
   108
fun err_if b msg = if b then error msg else ();
17350
26cd3756377a more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents: 16571
diff changeset
   109
14555
341908d6c792 'also'/'moreover': do not interfere with current facts, allow in chain mode;
wenzelm
parents: 14549
diff changeset
   110
fun assert_sane final =
341908d6c792 'also'/'moreover': do not interfere with current facts, allow in chain mode;
wenzelm
parents: 14549
diff changeset
   111
  if final then Proof.assert_forward else Proof.assert_forward_or_chain;
341908d6c792 'also'/'moreover': do not interfere with current facts, allow in chain mode;
wenzelm
parents: 14549
diff changeset
   112
17350
26cd3756377a more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents: 16571
diff changeset
   113
fun maintain_calculation false calc = put_calculation (SOME calc)
26cd3756377a more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents: 16571
diff changeset
   114
  | maintain_calculation true calc = put_calculation NONE #> Proof.chain_facts calc;
6778
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   115
17350
26cd3756377a more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents: 16571
diff changeset
   116
fun print_calculation false _ _ = ()
26cd3756377a more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents: 16571
diff changeset
   117
  | print_calculation true ctxt calc =
26cd3756377a more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents: 16571
diff changeset
   118
      Pretty.writeln (ProofContext.pretty_fact ctxt (calculationN, calc));
8562
ce0e2b8e8844 added 'moreover' command;
wenzelm
parents: 8461
diff changeset
   119
ce0e2b8e8844 added 'moreover' command;
wenzelm
parents: 8461
diff changeset
   120
17350
26cd3756377a more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents: 16571
diff changeset
   121
(* also and finally *)
8562
ce0e2b8e8844 added 'moreover' command;
wenzelm
parents: 8461
diff changeset
   122
18637
33a6f6caa617 generic data and attributes;
wenzelm
parents: 18377
diff changeset
   123
val get_rules = #1 o CalculationData.get o Context.Proof o Proof.context_of;
33a6f6caa617 generic data and attributes;
wenzelm
parents: 18377
diff changeset
   124
17350
26cd3756377a more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents: 16571
diff changeset
   125
fun calculate prep_rules final raw_rules int state =
6778
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   126
  let
12805
3be853cf19cf Thm.prop_of;
wenzelm
parents: 12402
diff changeset
   127
    val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of;
18947
de38ee3654d4 eq_prop: Envir.beta_eta_contract;
wenzelm
parents: 18728
diff changeset
   128
    val eq_prop = op aconv o pairself (Envir.beta_eta_contract o strip_assums_concl);
11097
c1be9f2dff4c more robust selection of calculational rules;
wenzelm
parents: 10478
diff changeset
   129
    fun projection ths th = Library.exists (Library.curry eq_prop th) ths;
8300
4c3f83414de3 use NetRules;
wenzelm
parents: 8150
diff changeset
   130
17350
26cd3756377a more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents: 16571
diff changeset
   131
    val opt_rules = Option.map (prep_rules state) raw_rules;
11097
c1be9f2dff4c more robust selection of calculational rules;
wenzelm
parents: 10478
diff changeset
   132
    fun combine ths =
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   133
      (case opt_rules of SOME rules => rules
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   134
      | NONE =>
18637
33a6f6caa617 generic data and attributes;
wenzelm
parents: 18377
diff changeset
   135
          (case ths of [] => NetRules.rules (#1 (get_rules state))
33a6f6caa617 generic data and attributes;
wenzelm
parents: 18377
diff changeset
   136
          | th :: _ => NetRules.retrieve (#1 (get_rules state)) (strip_assums_concl th)))
18223
20830cb4428c Drule.multi_resolves;
wenzelm
parents: 17384
diff changeset
   137
      |> Seq.of_list |> Seq.maps (Drule.multi_resolve ths)
11097
c1be9f2dff4c more robust selection of calculational rules;
wenzelm
parents: 10478
diff changeset
   138
      |> Seq.filter (not o projection ths);
7414
9bc7797d1249 calculation: thm list;
wenzelm
parents: 7197
diff changeset
   139
14555
341908d6c792 'also'/'moreover': do not interfere with current facts, allow in chain mode;
wenzelm
parents: 14549
diff changeset
   140
    val facts = Proof.the_facts (assert_sane final state);
6903
682f8a9ec75d improved errors;
wenzelm
parents: 6877
diff changeset
   141
    val (initial, calculations) =
6778
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   142
      (case get_calculation state of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   143
        NONE => (true, Seq.single facts)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   144
      | SOME calc => (false, Seq.map single (combine (calc @ facts))));
6778
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   145
  in
18678
dd0c569fa43d sane ERROR handling;
wenzelm
parents: 18637
diff changeset
   146
    err_if (initial andalso final) "No calculation yet";
dd0c569fa43d sane ERROR handling;
wenzelm
parents: 18637
diff changeset
   147
    err_if (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given";
17350
26cd3756377a more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents: 16571
diff changeset
   148
    calculations |> Seq.map (fn calc => (print_calculation int (Proof.context_of state) calc;
12055
a9c44895cc8c pretty/print functions with context;
wenzelm
parents: 12021
diff changeset
   149
        state |> maintain_calculation final calc))
6778
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   150
  end;
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   151
17350
26cd3756377a more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents: 16571
diff changeset
   152
val also = calculate Proof.get_thmss false;
26cd3756377a more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents: 16571
diff changeset
   153
val also_i = calculate (K I) false;
22573
2ac646ab2f6c avoid clash with Alice keywords;
wenzelm
parents: 21506
diff changeset
   154
val finally_ = calculate Proof.get_thmss true;
17350
26cd3756377a more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents: 16571
diff changeset
   155
val finally_i = calculate (K I) true;
6778
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   156
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   157
17350
26cd3756377a more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents: 16571
diff changeset
   158
(* moreover and ultimately *)
8562
ce0e2b8e8844 added 'moreover' command;
wenzelm
parents: 8461
diff changeset
   159
17350
26cd3756377a more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents: 16571
diff changeset
   160
fun collect final int state =
8588
b7c3f264f8ac added 'ultimately';
wenzelm
parents: 8562
diff changeset
   161
  let
14555
341908d6c792 'also'/'moreover': do not interfere with current facts, allow in chain mode;
wenzelm
parents: 14549
diff changeset
   162
    val facts = Proof.the_facts (assert_sane final state);
8588
b7c3f264f8ac added 'ultimately';
wenzelm
parents: 8562
diff changeset
   163
    val (initial, thms) =
b7c3f264f8ac added 'ultimately';
wenzelm
parents: 8562
diff changeset
   164
      (case get_calculation state of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   165
        NONE => (true, [])
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   166
      | SOME thms => (false, thms));
8588
b7c3f264f8ac added 'ultimately';
wenzelm
parents: 8562
diff changeset
   167
    val calc = thms @ facts;
b7c3f264f8ac added 'ultimately';
wenzelm
parents: 8562
diff changeset
   168
  in
18678
dd0c569fa43d sane ERROR handling;
wenzelm
parents: 18637
diff changeset
   169
    err_if (initial andalso final) "No calculation yet";
17350
26cd3756377a more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents: 16571
diff changeset
   170
    print_calculation int (Proof.context_of state) calc;
8588
b7c3f264f8ac added 'ultimately';
wenzelm
parents: 8562
diff changeset
   171
    state |> maintain_calculation final calc
b7c3f264f8ac added 'ultimately';
wenzelm
parents: 8562
diff changeset
   172
  end;
b7c3f264f8ac added 'ultimately';
wenzelm
parents: 8562
diff changeset
   173
17350
26cd3756377a more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents: 16571
diff changeset
   174
val moreover = collect false;
26cd3756377a more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents: 16571
diff changeset
   175
val ultimately = collect true;
8562
ce0e2b8e8844 added 'moreover' command;
wenzelm
parents: 8461
diff changeset
   176
6778
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   177
end;