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