src/Pure/Isar/calculation.ML
author wenzelm
Fri Nov 09 00:19:20 2001 +0100 (2001-11-09)
changeset 12123 739eba13e2cd
parent 12055 a9c44895cc8c
child 12311 ce5f9e61c037
permissions -rw-r--r--
theory data: finish method;
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@12055
    17
  val also: thm list option -> (Proof.context -> thm list -> unit)
wenzelm@12055
    18
    -> Proof.state -> Proof.state Seq.seq
wenzelm@12055
    19
  val finally: thm list option -> (Proof.context -> thm list -> unit)
wenzelm@12055
    20
    -> Proof.state -> Proof.state Seq.seq
wenzelm@12055
    21
  val moreover: (Proof.context -> thm list -> unit) -> Proof.state -> Proof.state
wenzelm@12055
    22
  val ultimately: (Proof.context -> thm list -> unit) -> Proof.state -> Proof.state
wenzelm@6778
    23
  val setup: (theory -> theory) list
wenzelm@6778
    24
end;
wenzelm@6778
    25
wenzelm@6778
    26
structure Calculation: CALCULATION =
wenzelm@6778
    27
struct
wenzelm@6778
    28
wenzelm@6778
    29
(** global and local calculation data **)
wenzelm@6778
    30
wenzelm@8300
    31
(* theory data kind 'Isar/calculation' *)
wenzelm@6778
    32
wenzelm@12055
    33
fun print_rules prt x rs =
wenzelm@12055
    34
  Pretty.writeln (Pretty.big_list "transitivity rules:" (map (prt x) (NetRules.rules rs)));
wenzelm@6778
    35
wenzelm@6778
    36
structure GlobalCalculationArgs =
wenzelm@6778
    37
struct
wenzelm@6778
    38
  val name = "Isar/calculation";
wenzelm@8300
    39
  type T = thm NetRules.T
wenzelm@6778
    40
wenzelm@11784
    41
  val empty = NetRules.elim;
wenzelm@6778
    42
  val copy = I;
wenzelm@12123
    43
  val finish = I;
wenzelm@6778
    44
  val prep_ext = I;
wenzelm@8300
    45
  val merge = NetRules.merge;
wenzelm@12055
    46
  val print = print_rules Display.pretty_thm_sg;
wenzelm@6778
    47
end;
wenzelm@6778
    48
wenzelm@6778
    49
structure GlobalCalculation = TheoryDataFun(GlobalCalculationArgs);
wenzelm@6778
    50
val print_global_rules = GlobalCalculation.print;
wenzelm@6778
    51
wenzelm@6778
    52
wenzelm@6778
    53
(* proof data kind 'Isar/calculation' *)
wenzelm@6778
    54
wenzelm@6778
    55
structure LocalCalculationArgs =
wenzelm@6778
    56
struct
wenzelm@6778
    57
  val name = "Isar/calculation";
wenzelm@8300
    58
  type T = thm NetRules.T * (thm list * int) option;
wenzelm@6778
    59
wenzelm@6778
    60
  fun init thy = (GlobalCalculation.get thy, None);
wenzelm@12055
    61
  fun print ctxt (rs, _) = print_rules ProofContext.pretty_thm ctxt rs;
wenzelm@6778
    62
end;
wenzelm@6778
    63
wenzelm@6778
    64
structure LocalCalculation = ProofDataFun(LocalCalculationArgs);
wenzelm@6787
    65
val get_local_rules = #1 o LocalCalculation.get_st;
wenzelm@6778
    66
val print_local_rules = LocalCalculation.print;
wenzelm@6778
    67
wenzelm@6778
    68
wenzelm@6778
    69
(* access calculation *)
wenzelm@6778
    70
wenzelm@6778
    71
fun get_calculation state =
wenzelm@6787
    72
  (case #2 (LocalCalculation.get_st state) of
wenzelm@6778
    73
    None => None
wenzelm@7414
    74
  | Some (thms, lev) => if lev = Proof.level state then Some thms else None);
wenzelm@6778
    75
wenzelm@7414
    76
fun put_calculation thms state =
wenzelm@7414
    77
  LocalCalculation.put_st (get_local_rules state, Some (thms, Proof.level state)) state;
wenzelm@6778
    78
wenzelm@6787
    79
fun reset_calculation state =
wenzelm@6787
    80
  LocalCalculation.put_st (get_local_rules state, None) state;
wenzelm@6787
    81
wenzelm@6778
    82
wenzelm@6778
    83
wenzelm@6778
    84
(** attributes **)
wenzelm@6778
    85
wenzelm@6778
    86
(* trans add/del *)
wenzelm@6778
    87
wenzelm@6778
    88
fun mk_att f g (x, thm) = (f (g thm) x, thm);
wenzelm@6778
    89
wenzelm@8300
    90
val trans_add_global = mk_att GlobalCalculation.map NetRules.insert;
wenzelm@8300
    91
val trans_del_global = mk_att GlobalCalculation.map NetRules.delete;
wenzelm@8300
    92
val trans_add_local = mk_att LocalCalculation.map (Library.apfst o NetRules.insert);
wenzelm@8300
    93
val trans_del_local = mk_att LocalCalculation.map (Library.apfst o NetRules.delete);
wenzelm@6778
    94
wenzelm@6778
    95
wenzelm@6778
    96
(* concrete syntax *)
wenzelm@6778
    97
wenzelm@6778
    98
val trans_attr =
wenzelm@8634
    99
 (Attrib.add_del_args trans_add_global trans_del_global,
wenzelm@8634
   100
  Attrib.add_del_args trans_add_local trans_del_local);
wenzelm@6778
   101
wenzelm@6778
   102
wenzelm@6787
   103
wenzelm@6778
   104
(** proof commands **)
wenzelm@6778
   105
wenzelm@8588
   106
(* maintain calculation register *)
wenzelm@8562
   107
wenzelm@6778
   108
val calculationN = "calculation";
wenzelm@6778
   109
wenzelm@8588
   110
fun maintain_calculation false calc state =
wenzelm@8588
   111
      state
wenzelm@8588
   112
      |> put_calculation calc
wenzelm@8588
   113
      |> Proof.simple_have_thms calculationN calc
wenzelm@8588
   114
      |> Proof.reset_facts
wenzelm@8588
   115
  | maintain_calculation true calc state =
wenzelm@8588
   116
      state
wenzelm@8588
   117
      |> reset_calculation
wenzelm@8588
   118
      |> Proof.reset_thms calculationN
wenzelm@8588
   119
      |> Proof.simple_have_thms "" calc
wenzelm@8588
   120
      |> Proof.chain;
wenzelm@8562
   121
wenzelm@8562
   122
wenzelm@8562
   123
(* 'also' and 'finally' *)
wenzelm@8562
   124
wenzelm@8588
   125
fun err_if state b msg = if b then raise Proof.STATE (msg, state) else ();
wenzelm@8588
   126
wenzelm@6877
   127
fun calculate final opt_rules print state =
wenzelm@6778
   128
  let
wenzelm@9322
   129
    val strip_assums_concl = Logic.strip_assums_concl o #prop o Thm.rep_thm;
wenzelm@9322
   130
    val eq_prop = op aconv o pairself (Pattern.eta_contract o strip_assums_concl);
wenzelm@11097
   131
    fun projection ths th = Library.exists (Library.curry eq_prop th) ths;
wenzelm@8300
   132
wenzelm@11097
   133
    fun combine ths =
wenzelm@11097
   134
      (case opt_rules of Some rules => rules
wenzelm@11097
   135
      | None =>
wenzelm@11097
   136
          (case ths of [] => NetRules.rules (get_local_rules state)
wenzelm@11784
   137
          | th :: _ => NetRules.retrieve (get_local_rules state) (strip_assums_concl th)))
wenzelm@11097
   138
      |> Seq.of_list |> Seq.map (Method.multi_resolve ths) |> Seq.flat
wenzelm@11097
   139
      |> Seq.filter (not o projection ths);
wenzelm@7414
   140
wenzelm@11097
   141
    val facts = Proof.the_facts (Proof.assert_forward state);
wenzelm@6903
   142
    val (initial, calculations) =
wenzelm@6778
   143
      (case get_calculation state of
wenzelm@7414
   144
        None => (true, Seq.single facts)
wenzelm@11097
   145
      | Some calc => (false, Seq.map single (combine (calc @ facts))));
wenzelm@6778
   146
  in
wenzelm@8588
   147
    err_if state (initial andalso final) "No calculation yet";
wenzelm@8588
   148
    err_if state (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given";
wenzelm@12055
   149
    calculations |> Seq.map (fn calc => (print (Proof.context_of state) calc;
wenzelm@12055
   150
        state |> maintain_calculation final calc))
wenzelm@6778
   151
  end;
wenzelm@6778
   152
wenzelm@6782
   153
fun also print = calculate false print;
wenzelm@6782
   154
fun finally print = calculate true print;
wenzelm@6778
   155
wenzelm@6778
   156
wenzelm@8588
   157
(* 'moreover' and 'ultimately' *)
wenzelm@8562
   158
wenzelm@8588
   159
fun collect final print state =
wenzelm@8588
   160
  let
wenzelm@10478
   161
    val facts = Proof.the_facts (Proof.assert_forward state);
wenzelm@8588
   162
    val (initial, thms) =
wenzelm@8588
   163
      (case get_calculation state of
wenzelm@8588
   164
        None => (true, [])
wenzelm@8588
   165
      | Some thms => (false, thms));
wenzelm@8588
   166
    val calc = thms @ facts;
wenzelm@8588
   167
  in
wenzelm@8588
   168
    err_if state (initial andalso final) "No calculation yet";
wenzelm@12055
   169
    print (Proof.context_of state) calc;
wenzelm@8588
   170
    state |> maintain_calculation final calc
wenzelm@8588
   171
  end;
wenzelm@8588
   172
wenzelm@8588
   173
fun moreover print = collect false print;
wenzelm@8588
   174
fun ultimately print = collect true print;
wenzelm@8562
   175
wenzelm@8562
   176
wenzelm@6778
   177
wenzelm@6778
   178
(** theory setup **)
wenzelm@6778
   179
wenzelm@6778
   180
val setup = [GlobalCalculation.init, LocalCalculation.init,
wenzelm@12021
   181
  Attrib.add_attributes [("trans", trans_attr, "declaration of transitivity rule")],
wenzelm@12021
   182
  #1 o PureThy.add_thms [(("", transitive_thm), [trans_add_global])]];
wenzelm@6778
   183
wenzelm@6778
   184
wenzelm@6778
   185
end;