src/Pure/Isar/calculation.ML
author wenzelm
Wed Apr 14 13:28:46 2004 +0200 (2004-04-14)
changeset 14564 3667b4616e9a
parent 14555 341908d6c792
child 14981 e73f8140af78
permissions -rw-r--r--
renamed have_thms to note_thms;
wenzelm@6778
     1
(*  Title:      Pure/Isar/calculation.ML
wenzelm@6778
     2
    ID:         $Id$
wenzelm@6778
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@8807
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@6778
     5
wenzelm@6778
     6
Support for calculational proofs.
wenzelm@6778
     7
*)
wenzelm@6778
     8
wenzelm@6778
     9
signature CALCULATION =
wenzelm@6778
    10
sig
wenzelm@6778
    11
  val print_global_rules: theory -> unit
wenzelm@6778
    12
  val print_local_rules: Proof.context -> unit
wenzelm@6778
    13
  val trans_add_global: theory attribute
wenzelm@6778
    14
  val trans_del_global: theory attribute
wenzelm@6778
    15
  val trans_add_local: Proof.context attribute
wenzelm@6778
    16
  val trans_del_local: Proof.context attribute
wenzelm@12379
    17
  val sym_add_global: theory attribute
wenzelm@12379
    18
  val sym_del_global: theory attribute
wenzelm@12379
    19
  val sym_add_local: Proof.context attribute
wenzelm@12379
    20
  val sym_del_local: Proof.context attribute
wenzelm@12379
    21
  val symmetric_global: theory attribute
wenzelm@12379
    22
  val symmetric_local: Proof.context attribute
wenzelm@12055
    23
  val also: thm list option -> (Proof.context -> thm list -> unit)
wenzelm@12055
    24
    -> Proof.state -> Proof.state Seq.seq
wenzelm@12055
    25
  val finally: thm list option -> (Proof.context -> thm list -> unit)
wenzelm@12055
    26
    -> Proof.state -> Proof.state Seq.seq
wenzelm@12055
    27
  val moreover: (Proof.context -> thm list -> unit) -> Proof.state -> Proof.state
wenzelm@12055
    28
  val ultimately: (Proof.context -> thm list -> unit) -> Proof.state -> Proof.state
wenzelm@6778
    29
  val setup: (theory -> theory) list
wenzelm@6778
    30
end;
wenzelm@6778
    31
wenzelm@6778
    32
structure Calculation: CALCULATION =
wenzelm@6778
    33
struct
wenzelm@6778
    34
wenzelm@6778
    35
(** global and local calculation data **)
wenzelm@6778
    36
wenzelm@8300
    37
(* theory data kind 'Isar/calculation' *)
wenzelm@6778
    38
wenzelm@12379
    39
fun print_rules prt x (trans, sym) =
wenzelm@12379
    40
  [Pretty.big_list "transitivity rules:" (map (prt x) (NetRules.rules trans)),
wenzelm@12379
    41
    Pretty.big_list "symmetry rules:" (map (prt x) sym)]
wenzelm@12379
    42
  |> Pretty.chunks |> Pretty.writeln;
wenzelm@6778
    43
wenzelm@6778
    44
structure GlobalCalculationArgs =
wenzelm@6778
    45
struct
wenzelm@6778
    46
  val name = "Isar/calculation";
wenzelm@12379
    47
  type T = thm NetRules.T * thm list
wenzelm@6778
    48
wenzelm@12379
    49
  val empty = (NetRules.elim, []);
wenzelm@6778
    50
  val copy = I;
wenzelm@6778
    51
  val prep_ext = I;
wenzelm@12379
    52
  fun merge ((trans1, sym1), (trans2, sym2)) =
wenzelm@12379
    53
    (NetRules.merge (trans1, trans2), Drule.merge_rules (sym1, sym2));
wenzelm@12055
    54
  val print = print_rules Display.pretty_thm_sg;
wenzelm@6778
    55
end;
wenzelm@6778
    56
wenzelm@6778
    57
structure GlobalCalculation = TheoryDataFun(GlobalCalculationArgs);
wenzelm@6778
    58
val print_global_rules = GlobalCalculation.print;
wenzelm@6778
    59
wenzelm@6778
    60
wenzelm@6778
    61
(* proof data kind 'Isar/calculation' *)
wenzelm@6778
    62
wenzelm@6778
    63
structure LocalCalculationArgs =
wenzelm@6778
    64
struct
wenzelm@6778
    65
  val name = "Isar/calculation";
wenzelm@12379
    66
  type T = (thm NetRules.T * thm list) * (thm list * int) option;
wenzelm@6778
    67
wenzelm@6778
    68
  fun init thy = (GlobalCalculation.get thy, None);
wenzelm@12055
    69
  fun print ctxt (rs, _) = print_rules ProofContext.pretty_thm ctxt rs;
wenzelm@6778
    70
end;
wenzelm@6778
    71
wenzelm@6778
    72
structure LocalCalculation = ProofDataFun(LocalCalculationArgs);
wenzelm@13371
    73
val get_local_rules = #1 o LocalCalculation.get o Proof.context_of;
wenzelm@6778
    74
val print_local_rules = LocalCalculation.print;
wenzelm@6778
    75
wenzelm@6778
    76
wenzelm@6778
    77
(* access calculation *)
wenzelm@6778
    78
wenzelm@6778
    79
fun get_calculation state =
wenzelm@13371
    80
  (case #2 (LocalCalculation.get (Proof.context_of state)) of
wenzelm@6778
    81
    None => None
wenzelm@7414
    82
  | Some (thms, lev) => if lev = Proof.level state then Some thms else None);
wenzelm@6778
    83
wenzelm@7414
    84
fun put_calculation thms state =
wenzelm@13371
    85
  Proof.map_context
wenzelm@13371
    86
    (LocalCalculation.put (get_local_rules state, Some (thms, Proof.level state))) state;
wenzelm@6778
    87
wenzelm@6787
    88
fun reset_calculation state =
wenzelm@13371
    89
  Proof.map_context (LocalCalculation.put (get_local_rules state, None)) state;
wenzelm@6787
    90
wenzelm@6778
    91
wenzelm@6778
    92
wenzelm@6778
    93
(** attributes **)
wenzelm@6778
    94
wenzelm@12379
    95
(* add/del rules *)
wenzelm@12379
    96
wenzelm@12379
    97
fun global_att f (x, thm) = (GlobalCalculation.map (f thm) x, thm);
wenzelm@12379
    98
fun local_att f (x, thm) = (LocalCalculation.map (apfst (f thm)) x, thm);
wenzelm@6778
    99
wenzelm@12379
   100
val trans_add_global = global_att (apfst o NetRules.insert);
wenzelm@12379
   101
val trans_del_global = global_att (apfst o NetRules.delete);
wenzelm@12379
   102
val trans_add_local = local_att (apfst o NetRules.insert);
wenzelm@12379
   103
val trans_del_local = local_att (apfst o NetRules.delete);
wenzelm@6778
   104
wenzelm@12379
   105
val sym_add_global = global_att (apsnd o Drule.add_rule) o ContextRules.elim_query_global None;
wenzelm@12402
   106
val sym_del_global = global_att (apsnd o Drule.del_rule) o ContextRules.rule_del_global;
wenzelm@12379
   107
val sym_add_local = local_att (apsnd o Drule.add_rule) o ContextRules.elim_query_local None;
wenzelm@12402
   108
val sym_del_local = local_att (apsnd o Drule.del_rule) o ContextRules.rule_del_local;
wenzelm@12379
   109
wenzelm@12379
   110
wenzelm@12379
   111
(* symmetry *)
wenzelm@12379
   112
wenzelm@12379
   113
fun gen_symmetric get_sym = Drule.rule_attribute (fn x => fn th =>
wenzelm@12379
   114
  (case Seq.chop (2, Method.multi_resolves [th] (get_sym x)) of
wenzelm@12379
   115
    ([th'], _) => th'
wenzelm@12379
   116
  | ([], _) => raise THM ("symmetric: no unifiers", 1, [th])
wenzelm@12379
   117
  | _ => raise THM ("symmetric: multiple unifiers", 1, [th])));
wenzelm@12379
   118
wenzelm@12379
   119
val symmetric_global = gen_symmetric (#2 o GlobalCalculation.get);
wenzelm@12379
   120
val symmetric_local = gen_symmetric (#2 o #1 o LocalCalculation.get);
wenzelm@6778
   121
wenzelm@6778
   122
wenzelm@6778
   123
(* concrete syntax *)
wenzelm@6778
   124
wenzelm@6778
   125
val trans_attr =
wenzelm@8634
   126
 (Attrib.add_del_args trans_add_global trans_del_global,
wenzelm@8634
   127
  Attrib.add_del_args trans_add_local trans_del_local);
wenzelm@6778
   128
wenzelm@12379
   129
val sym_attr =
wenzelm@12379
   130
 (Attrib.add_del_args sym_add_global sym_del_global,
wenzelm@12379
   131
  Attrib.add_del_args sym_add_local sym_del_local);
wenzelm@12379
   132
wenzelm@6778
   133
wenzelm@6787
   134
wenzelm@6778
   135
(** proof commands **)
wenzelm@6778
   136
wenzelm@14555
   137
fun assert_sane final =
wenzelm@14555
   138
  if final then Proof.assert_forward else Proof.assert_forward_or_chain;
wenzelm@14555
   139
wenzelm@14555
   140
wenzelm@8588
   141
(* maintain calculation register *)
wenzelm@8562
   142
wenzelm@6778
   143
val calculationN = "calculation";
wenzelm@6778
   144
wenzelm@8588
   145
fun maintain_calculation false calc state =
wenzelm@8588
   146
      state
wenzelm@8588
   147
      |> put_calculation calc
wenzelm@14555
   148
      |> Proof.put_thms (calculationN, calc)
wenzelm@8588
   149
  | maintain_calculation true calc state =
wenzelm@8588
   150
      state
wenzelm@8588
   151
      |> reset_calculation
wenzelm@8588
   152
      |> Proof.reset_thms calculationN
wenzelm@14564
   153
      |> Proof.simple_note_thms "" calc
wenzelm@8588
   154
      |> Proof.chain;
wenzelm@8562
   155
wenzelm@8562
   156
wenzelm@8562
   157
(* 'also' and 'finally' *)
wenzelm@8562
   158
wenzelm@8588
   159
fun err_if state b msg = if b then raise Proof.STATE (msg, state) else ();
wenzelm@8588
   160
wenzelm@6877
   161
fun calculate final opt_rules print state =
wenzelm@6778
   162
  let
wenzelm@12805
   163
    val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of;
wenzelm@9322
   164
    val eq_prop = op aconv o pairself (Pattern.eta_contract o strip_assums_concl);
wenzelm@11097
   165
    fun projection ths th = Library.exists (Library.curry eq_prop th) ths;
wenzelm@8300
   166
wenzelm@11097
   167
    fun combine ths =
wenzelm@11097
   168
      (case opt_rules of Some rules => rules
wenzelm@11097
   169
      | None =>
wenzelm@12379
   170
          (case ths of [] => NetRules.rules (#1 (get_local_rules state))
wenzelm@12379
   171
          | th :: _ => NetRules.retrieve (#1 (get_local_rules state)) (strip_assums_concl th)))
wenzelm@11097
   172
      |> Seq.of_list |> Seq.map (Method.multi_resolve ths) |> Seq.flat
wenzelm@11097
   173
      |> Seq.filter (not o projection ths);
wenzelm@7414
   174
wenzelm@14555
   175
    val facts = Proof.the_facts (assert_sane final state);
wenzelm@6903
   176
    val (initial, calculations) =
wenzelm@6778
   177
      (case get_calculation state of
wenzelm@7414
   178
        None => (true, Seq.single facts)
wenzelm@11097
   179
      | Some calc => (false, Seq.map single (combine (calc @ facts))));
wenzelm@6778
   180
  in
wenzelm@8588
   181
    err_if state (initial andalso final) "No calculation yet";
wenzelm@8588
   182
    err_if state (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given";
wenzelm@12055
   183
    calculations |> Seq.map (fn calc => (print (Proof.context_of state) calc;
wenzelm@12055
   184
        state |> maintain_calculation final calc))
wenzelm@6778
   185
  end;
wenzelm@6778
   186
wenzelm@6782
   187
fun also print = calculate false print;
wenzelm@6782
   188
fun finally print = calculate true print;
wenzelm@6778
   189
wenzelm@6778
   190
wenzelm@8588
   191
(* 'moreover' and 'ultimately' *)
wenzelm@8562
   192
wenzelm@8588
   193
fun collect final print state =
wenzelm@8588
   194
  let
wenzelm@14555
   195
    val facts = Proof.the_facts (assert_sane final state);
wenzelm@8588
   196
    val (initial, thms) =
wenzelm@8588
   197
      (case get_calculation state of
wenzelm@8588
   198
        None => (true, [])
wenzelm@8588
   199
      | Some thms => (false, thms));
wenzelm@8588
   200
    val calc = thms @ facts;
wenzelm@8588
   201
  in
wenzelm@8588
   202
    err_if state (initial andalso final) "No calculation yet";
wenzelm@12055
   203
    print (Proof.context_of state) calc;
wenzelm@8588
   204
    state |> maintain_calculation final calc
wenzelm@8588
   205
  end;
wenzelm@8588
   206
wenzelm@8588
   207
fun moreover print = collect false print;
wenzelm@8588
   208
fun ultimately print = collect true print;
wenzelm@8562
   209
wenzelm@8562
   210
wenzelm@6778
   211
wenzelm@6778
   212
(** theory setup **)
wenzelm@6778
   213
wenzelm@12379
   214
val setup =
wenzelm@12379
   215
 [GlobalCalculation.init, LocalCalculation.init,
wenzelm@12379
   216
  Attrib.add_attributes
wenzelm@12379
   217
   [("trans", trans_attr, "declaration of transitivity rule"),
wenzelm@12379
   218
    ("sym", sym_attr, "declaration of symmetry rule"),
wenzelm@12379
   219
    ("symmetric", (Attrib.no_args symmetric_global, Attrib.no_args symmetric_local),
wenzelm@12379
   220
      "resolution with symmetry rule")],
wenzelm@12379
   221
  #1 o PureThy.add_thms
wenzelm@12379
   222
   [(("", transitive_thm), [trans_add_global]),
wenzelm@12379
   223
    (("", symmetric_thm), [sym_add_global])]];
wenzelm@6778
   224
wenzelm@6778
   225
end;