src/Pure/Isar/calculation.ML
author wenzelm
Fri Mar 31 21:55:27 2000 +0200 (2000-03-31)
changeset 8634 3f34637cb9c0
parent 8588 b7c3f264f8ac
child 8649 dc496bb0638f
permissions -rw-r--r--
use Attrib.add_del_args;
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@7414
    16
  val also: thm list option -> (thm list -> unit) -> Proof.state -> Proof.state Seq.seq
wenzelm@7414
    17
  val finally: thm list option -> (thm list -> unit) -> Proof.state -> Proof.state Seq.seq
wenzelm@8562
    18
  val moreover: (thm list -> unit) -> Proof.state -> Proof.state
wenzelm@8588
    19
  val ultimately: (thm list -> unit) -> Proof.state -> Proof.state
wenzelm@6778
    20
  val setup: (theory -> theory) list
wenzelm@6778
    21
end;
wenzelm@6778
    22
wenzelm@6778
    23
structure Calculation: CALCULATION =
wenzelm@6778
    24
struct
wenzelm@6778
    25
wenzelm@6778
    26
(** global and local calculation data **)
wenzelm@6778
    27
wenzelm@8300
    28
(* theory data kind 'Isar/calculation' *)
wenzelm@6778
    29
wenzelm@8300
    30
fun print_rules rs = Pretty.writeln (Pretty.big_list "calculation rules:"
wenzelm@8300
    31
  (map Display.pretty_thm (NetRules.rules rs)));
wenzelm@6778
    32
wenzelm@6778
    33
structure GlobalCalculationArgs =
wenzelm@6778
    34
struct
wenzelm@6778
    35
  val name = "Isar/calculation";
wenzelm@8300
    36
  type T = thm NetRules.T
wenzelm@6778
    37
wenzelm@8300
    38
  val empty = NetRules.init_elim;
wenzelm@6778
    39
  val copy = I;
wenzelm@6778
    40
  val prep_ext = I;
wenzelm@8300
    41
  val merge = NetRules.merge;
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@8300
    54
  type T = thm NetRules.T * (thm list * int) option;
wenzelm@6778
    55
wenzelm@6778
    56
  fun init thy = (GlobalCalculation.get thy, None);
wenzelm@8300
    57
  fun print _ (rs, _) = print_rules rs;
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@7414
    70
  | Some (thms, lev) => if lev = Proof.level state then Some thms else None);
wenzelm@6778
    71
wenzelm@7414
    72
fun put_calculation thms state =
wenzelm@7414
    73
  LocalCalculation.put_st (get_local_rules state, Some (thms, 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
fun mk_att f g (x, thm) = (f (g thm) x, thm);
wenzelm@6778
    85
wenzelm@8300
    86
val trans_add_global = mk_att GlobalCalculation.map NetRules.insert;
wenzelm@8300
    87
val trans_del_global = mk_att GlobalCalculation.map NetRules.delete;
wenzelm@8300
    88
val trans_add_local = mk_att LocalCalculation.map (Library.apfst o NetRules.insert);
wenzelm@8300
    89
val trans_del_local = mk_att LocalCalculation.map (Library.apfst o NetRules.delete);
wenzelm@6778
    90
wenzelm@6778
    91
wenzelm@6778
    92
(* concrete syntax *)
wenzelm@6778
    93
wenzelm@6778
    94
val trans_attr =
wenzelm@8634
    95
 (Attrib.add_del_args trans_add_global trans_del_global,
wenzelm@8634
    96
  Attrib.add_del_args trans_add_local trans_del_local);
wenzelm@6778
    97
wenzelm@6778
    98
wenzelm@6787
    99
wenzelm@6778
   100
(** proof commands **)
wenzelm@6778
   101
wenzelm@8588
   102
(* maintain calculation register *)
wenzelm@8562
   103
wenzelm@6778
   104
val calculationN = "calculation";
wenzelm@6778
   105
wenzelm@8588
   106
fun maintain_calculation false calc state =
wenzelm@8588
   107
      state
wenzelm@8588
   108
      |> put_calculation calc
wenzelm@8588
   109
      |> Proof.simple_have_thms calculationN calc
wenzelm@8588
   110
      |> Proof.reset_facts
wenzelm@8588
   111
  | maintain_calculation true calc state =
wenzelm@8588
   112
      state
wenzelm@8588
   113
      |> reset_calculation
wenzelm@8588
   114
      |> Proof.reset_thms calculationN
wenzelm@8588
   115
      |> Proof.simple_have_thms "" calc
wenzelm@8588
   116
      |> Proof.chain;
wenzelm@8562
   117
wenzelm@8562
   118
wenzelm@8562
   119
(* 'also' and 'finally' *)
wenzelm@8562
   120
wenzelm@8588
   121
fun err_if state b msg = if b then raise Proof.STATE (msg, state) else ();
wenzelm@8588
   122
wenzelm@6877
   123
fun calculate final opt_rules print state =
wenzelm@6778
   124
  let
wenzelm@7414
   125
    val facts = Proof.the_facts state;
wenzelm@7414
   126
wenzelm@7554
   127
    val eq_prop = op aconv o pairself (#prop o Thm.rep_thm);
wenzelm@7554
   128
    fun differ thms thms' = not (Library.equal_lists eq_prop (thms, thms'));
wenzelm@8300
   129
wenzelm@7414
   130
    fun combine thms =
wenzelm@8300
   131
      let
wenzelm@8300
   132
        val ths = thms @ facts;
wenzelm@8300
   133
        val rs = NetRules.inserts (if_none opt_rules []) (get_local_rules state);
wenzelm@8300
   134
        val rules =
wenzelm@8300
   135
          (case ths of [] => NetRules.rules rs
wenzelm@8300
   136
          | th :: _ => NetRules.may_unify rs (Logic.strip_assums_concl (#prop (Thm.rep_thm th))));
wenzelm@8300
   137
        val ruleq = Seq.of_list rules;
wenzelm@8300
   138
      in Seq.map Library.single (Seq.flat (Seq.map (Method.multi_resolve ths) ruleq)) end;
wenzelm@7414
   139
wenzelm@6903
   140
    val (initial, calculations) =
wenzelm@6778
   141
      (case get_calculation state of
wenzelm@7414
   142
        None => (true, Seq.single facts)
wenzelm@7414
   143
      | Some thms => (false, Seq.filter (differ thms) (combine thms)))
wenzelm@6778
   144
  in
wenzelm@8588
   145
    err_if state (initial andalso final) "No calculation yet";
wenzelm@8588
   146
    err_if state (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given";
wenzelm@8588
   147
    calculations |> Seq.map (fn calc => (print calc; state |> maintain_calculation final calc))
wenzelm@6778
   148
  end;
wenzelm@6778
   149
wenzelm@6782
   150
fun also print = calculate false print;
wenzelm@6782
   151
fun finally print = calculate true print;
wenzelm@6778
   152
wenzelm@6778
   153
wenzelm@8588
   154
(* 'moreover' and 'ultimately' *)
wenzelm@8562
   155
wenzelm@8588
   156
fun collect final print state =
wenzelm@8588
   157
  let
wenzelm@8588
   158
    val facts = Proof.the_facts state;
wenzelm@8588
   159
    val (initial, thms) =
wenzelm@8588
   160
      (case get_calculation state of
wenzelm@8588
   161
        None => (true, [])
wenzelm@8588
   162
      | Some thms => (false, thms));
wenzelm@8588
   163
    val calc = thms @ facts;
wenzelm@8588
   164
  in
wenzelm@8588
   165
    err_if state (initial andalso final) "No calculation yet";
wenzelm@8588
   166
    print calc;
wenzelm@8588
   167
    state |> maintain_calculation final calc
wenzelm@8588
   168
  end;
wenzelm@8588
   169
wenzelm@8588
   170
fun moreover print = collect false print;
wenzelm@8588
   171
fun ultimately print = collect true print;
wenzelm@8562
   172
wenzelm@8562
   173
wenzelm@6778
   174
wenzelm@6778
   175
(** theory setup **)
wenzelm@6778
   176
wenzelm@6778
   177
val setup = [GlobalCalculation.init, LocalCalculation.init,
wenzelm@8634
   178
  Attrib.add_attributes [("trans", trans_attr, "declare transitivity rule")]];
wenzelm@6778
   179
wenzelm@6778
   180
wenzelm@6778
   181
end;