src/Pure/Isar/calculation.ML
author wenzelm
Sat Jun 05 20:32:10 1999 +0200 (1999-06-05)
changeset 6787 25265c6807c3
parent 6782 adf099e851ed
child 6877 3d5e5e6f9e20
permissions -rw-r--r--
tuned;
wenzelm@6778
     1
(*  Title:      Pure/Isar/calculation.ML
wenzelm@6778
     2
    ID:         $Id$
wenzelm@6778
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@6778
     4
wenzelm@6778
     5
Support for calculational proofs.
wenzelm@6778
     6
*)
wenzelm@6778
     7
wenzelm@6778
     8
signature CALCULATION =
wenzelm@6778
     9
sig
wenzelm@6778
    10
  val print_global_rules: theory -> unit
wenzelm@6778
    11
  val print_local_rules: Proof.context -> unit
wenzelm@6778
    12
  val trans_add_global: theory attribute
wenzelm@6778
    13
  val trans_del_global: theory attribute
wenzelm@6778
    14
  val trans_add_local: Proof.context attribute
wenzelm@6778
    15
  val trans_del_local: Proof.context attribute
wenzelm@6778
    16
  val also: (thm -> unit) -> Proof.state -> Proof.state Seq.seq
wenzelm@6778
    17
  val finally: (thm -> unit) -> Proof.state -> Proof.state Seq.seq
wenzelm@6778
    18
  val setup: (theory -> theory) list
wenzelm@6778
    19
end;
wenzelm@6778
    20
wenzelm@6778
    21
structure Calculation: CALCULATION =
wenzelm@6778
    22
struct
wenzelm@6778
    23
wenzelm@6778
    24
wenzelm@6778
    25
(** global and local calculation data **)
wenzelm@6778
    26
wenzelm@6778
    27
fun print_rules ths =
wenzelm@6778
    28
  Pretty.writeln (Pretty.big_list "calculation rules:" (map Display.pretty_thm ths));
wenzelm@6778
    29
wenzelm@6778
    30
wenzelm@6778
    31
(* theory data kind 'Isar/calculation' *)
wenzelm@6778
    32
wenzelm@6778
    33
structure GlobalCalculationArgs =
wenzelm@6778
    34
struct
wenzelm@6778
    35
  val name = "Isar/calculation";
wenzelm@6778
    36
  type T = thm list;
wenzelm@6778
    37
wenzelm@6778
    38
  val empty = [];
wenzelm@6778
    39
  val copy = I;
wenzelm@6778
    40
  val prep_ext = I;
wenzelm@6778
    41
  fun merge (ths1, ths2) = Library.generic_merge Thm.eq_thm I I ths1 ths2;
wenzelm@6778
    42
  fun print _ = print_rules;
wenzelm@6778
    43
end;
wenzelm@6778
    44
wenzelm@6778
    45
structure GlobalCalculation = TheoryDataFun(GlobalCalculationArgs);
wenzelm@6778
    46
val print_global_rules = GlobalCalculation.print;
wenzelm@6778
    47
wenzelm@6778
    48
wenzelm@6778
    49
(* proof data kind 'Isar/calculation' *)
wenzelm@6778
    50
wenzelm@6778
    51
structure LocalCalculationArgs =
wenzelm@6778
    52
struct
wenzelm@6778
    53
  val name = "Isar/calculation";
wenzelm@6778
    54
  type T = thm list * (thm * int) option;
wenzelm@6778
    55
wenzelm@6778
    56
  fun init thy = (GlobalCalculation.get thy, None);
wenzelm@6778
    57
  fun print _ (ths, _) = print_rules ths;
wenzelm@6778
    58
end;
wenzelm@6778
    59
wenzelm@6778
    60
structure LocalCalculation = ProofDataFun(LocalCalculationArgs);
wenzelm@6787
    61
val get_local_rules = #1 o LocalCalculation.get_st;
wenzelm@6778
    62
val print_local_rules = LocalCalculation.print;
wenzelm@6778
    63
wenzelm@6778
    64
wenzelm@6778
    65
(* access calculation *)
wenzelm@6778
    66
wenzelm@6778
    67
fun get_calculation state =
wenzelm@6787
    68
  (case #2 (LocalCalculation.get_st state) of
wenzelm@6778
    69
    None => None
wenzelm@6778
    70
  | Some (thm, lev) => if lev = Proof.level state then Some thm else None);
wenzelm@6778
    71
wenzelm@6778
    72
fun put_calculation thm state =
wenzelm@6778
    73
  LocalCalculation.put_st (get_local_rules state, Some (thm, Proof.level state)) state;
wenzelm@6778
    74
wenzelm@6787
    75
fun reset_calculation state =
wenzelm@6787
    76
  LocalCalculation.put_st (get_local_rules state, None) state;
wenzelm@6787
    77
wenzelm@6778
    78
wenzelm@6778
    79
wenzelm@6778
    80
(** attributes **)
wenzelm@6778
    81
wenzelm@6778
    82
(* trans add/del *)
wenzelm@6778
    83
wenzelm@6778
    84
local
wenzelm@6778
    85
wenzelm@6778
    86
fun map_rules_global f thy = GlobalCalculation.put (f (GlobalCalculation.get thy)) thy;
wenzelm@6778
    87
fun map_rules_local f ctxt = LocalCalculation.put (f (LocalCalculation.get ctxt)) ctxt;
wenzelm@6778
    88
wenzelm@6778
    89
fun add_trans thm rules = Library.gen_ins Thm.eq_thm (thm, rules);
wenzelm@6778
    90
fun del_trans thm rules = Library.gen_rem Thm.eq_thm (rules, thm);
wenzelm@6778
    91
wenzelm@6778
    92
fun mk_att f g (x, thm) = (f (g thm) x, thm);
wenzelm@6778
    93
wenzelm@6778
    94
in
wenzelm@6778
    95
wenzelm@6778
    96
val trans_add_global = mk_att map_rules_global add_trans;
wenzelm@6778
    97
val trans_del_global = mk_att map_rules_global del_trans;
wenzelm@6778
    98
val trans_add_local = mk_att map_rules_local (Library.apfst o add_trans);
wenzelm@6778
    99
val trans_del_local = mk_att map_rules_local (Library.apfst o del_trans);
wenzelm@6778
   100
wenzelm@6778
   101
end;
wenzelm@6778
   102
wenzelm@6778
   103
wenzelm@6778
   104
(* concrete syntax *)
wenzelm@6778
   105
wenzelm@6778
   106
val transN = "trans";
wenzelm@6778
   107
val addN = "add";
wenzelm@6778
   108
val delN = "del";
wenzelm@6778
   109
wenzelm@6778
   110
fun trans_att add del =
wenzelm@6778
   111
  Attrib.syntax (Scan.lift (Args.$$$ addN >> K add || Args.$$$ delN >> K del || Scan.succeed add));
wenzelm@6778
   112
wenzelm@6778
   113
val trans_attr =
wenzelm@6778
   114
  (trans_att trans_add_global trans_del_global, trans_att trans_add_local trans_del_local);
wenzelm@6778
   115
wenzelm@6778
   116
wenzelm@6787
   117
wenzelm@6778
   118
(** proof commands **)
wenzelm@6778
   119
wenzelm@6787
   120
fun have_thms name thms = Proof.have_thmss name [] [(thms, [])];
wenzelm@6782
   121
wenzelm@6778
   122
val calculationN = "calculation";
wenzelm@6778
   123
wenzelm@6782
   124
fun calculate final print state =
wenzelm@6778
   125
  let
wenzelm@6778
   126
    val fact = Proof.the_fact state;
wenzelm@6778
   127
    val rules = Seq.of_list (get_local_rules state);
wenzelm@6778
   128
    val calculations =
wenzelm@6778
   129
      (case get_calculation state of
wenzelm@6778
   130
        None => Seq.single fact
wenzelm@6778
   131
      | Some thm => Seq.flat (Seq.map (Method.multi_resolve [thm, fact]) rules));
wenzelm@6778
   132
  in
wenzelm@6782
   133
    calculations |> Seq.map (fn calc =>
wenzelm@6782
   134
      (print calc;
wenzelm@6787
   135
        (if final then
wenzelm@6787
   136
          state
wenzelm@6787
   137
          |> reset_calculation
wenzelm@6787
   138
          |> have_thms calculationN []
wenzelm@6787
   139
          |> have_thms "" [calc]
wenzelm@6787
   140
          |> Proof.chain
wenzelm@6787
   141
        else
wenzelm@6787
   142
          state
wenzelm@6787
   143
          |> put_calculation calc
wenzelm@6787
   144
          |> have_thms calculationN [calc]
wenzelm@6787
   145
          |> Proof.reset_facts)))
wenzelm@6778
   146
  end;
wenzelm@6778
   147
wenzelm@6782
   148
fun also print = calculate false print;
wenzelm@6782
   149
fun finally print = calculate true print;
wenzelm@6778
   150
wenzelm@6778
   151
wenzelm@6778
   152
wenzelm@6778
   153
(** theory setup **)
wenzelm@6778
   154
wenzelm@6778
   155
val setup = [GlobalCalculation.init, LocalCalculation.init,
wenzelm@6778
   156
  Attrib.add_attributes [(transN, trans_attr, "transitivity rule")]];
wenzelm@6778
   157
wenzelm@6778
   158
wenzelm@6778
   159
end;