src/Pure/Isar/calculation.ML
author wenzelm
Mon, 09 Aug 1999 22:21:08 +0200
changeset 7197 3ddf4a55d765
parent 6903 682f8a9ec75d
child 7414 9bc7797d1249
permissions -rw-r--r--
append user rules;
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
6877
3d5e5e6f9e20 also, finally: opt_rules;
wenzelm
parents: 6787
diff changeset
    16
  val also: thm list option -> (thm -> unit) -> Proof.state -> Proof.state Seq.seq
3d5e5e6f9e20 also, finally: opt_rules;
wenzelm
parents: 6787
diff changeset
    17
  val finally: thm list option -> (thm -> unit) -> Proof.state -> Proof.state Seq.seq
6778
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
(* theory data kind 'Isar/calculation' *)
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    31
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    32
structure GlobalCalculationArgs =
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    33
struct
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    34
  val name = "Isar/calculation";
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    35
  type T = thm list;
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    36
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    37
  val empty = [];
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    38
  val copy = I;
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    39
  val prep_ext = I;
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    40
  fun merge (ths1, ths2) = Library.generic_merge Thm.eq_thm I I ths1 ths2;
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    41
  fun print _ = print_rules;
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    42
end;
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    43
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    44
structure GlobalCalculation = TheoryDataFun(GlobalCalculationArgs);
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    45
val print_global_rules = GlobalCalculation.print;
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    46
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    47
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    48
(* proof data kind 'Isar/calculation' *)
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    49
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    50
structure LocalCalculationArgs =
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    51
struct
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    52
  val name = "Isar/calculation";
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    53
  type T = thm list * (thm * int) option;
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    54
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    55
  fun init thy = (GlobalCalculation.get thy, None);
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    56
  fun print _ (ths, _) = print_rules ths;
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    57
end;
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    58
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    59
structure LocalCalculation = ProofDataFun(LocalCalculationArgs);
6787
wenzelm
parents: 6782
diff changeset
    60
val get_local_rules = #1 o LocalCalculation.get_st;
6778
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    61
val print_local_rules = LocalCalculation.print;
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    62
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    63
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    64
(* access calculation *)
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    65
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    66
fun get_calculation state =
6787
wenzelm
parents: 6782
diff changeset
    67
  (case #2 (LocalCalculation.get_st state) of
6778
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    68
    None => None
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    69
  | Some (thm, lev) => if lev = Proof.level state then Some thm else None);
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    70
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    71
fun put_calculation thm state =
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    72
  LocalCalculation.put_st (get_local_rules state, Some (thm, Proof.level state)) state;
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    73
6787
wenzelm
parents: 6782
diff changeset
    74
fun reset_calculation state =
wenzelm
parents: 6782
diff changeset
    75
  LocalCalculation.put_st (get_local_rules state, None) state;
wenzelm
parents: 6782
diff changeset
    76
6778
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    77
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    78
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    79
(** attributes **)
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    80
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    81
(* trans add/del *)
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    82
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    83
local
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    84
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    85
fun map_rules_global f thy = GlobalCalculation.put (f (GlobalCalculation.get thy)) thy;
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    86
fun map_rules_local f ctxt = LocalCalculation.put (f (LocalCalculation.get ctxt)) ctxt;
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    87
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    88
fun add_trans thm rules = Library.gen_ins Thm.eq_thm (thm, rules);
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    89
fun del_trans thm rules = Library.gen_rem Thm.eq_thm (rules, thm);
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    90
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    91
fun mk_att f g (x, thm) = (f (g thm) x, thm);
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    92
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    93
in
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    94
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    95
val trans_add_global = mk_att map_rules_global add_trans;
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    96
val trans_del_global = mk_att map_rules_global del_trans;
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    97
val trans_add_local = mk_att map_rules_local (Library.apfst o add_trans);
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    98
val trans_del_local = mk_att map_rules_local (Library.apfst o del_trans);
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    99
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   100
end;
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   101
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   102
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   103
(* concrete syntax *)
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   104
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   105
val transN = "trans";
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   106
val addN = "add";
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   107
val delN = "del";
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   108
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   109
fun trans_att add del =
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   110
  Attrib.syntax (Scan.lift (Args.$$$ addN >> K add || Args.$$$ delN >> K del || Scan.succeed add));
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   111
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   112
val trans_attr =
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   113
  (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
   114
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   115
6787
wenzelm
parents: 6782
diff changeset
   116
6778
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   117
(** proof commands **)
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   118
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   119
val calculationN = "calculation";
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   120
6877
3d5e5e6f9e20 also, finally: opt_rules;
wenzelm
parents: 6787
diff changeset
   121
fun calculate final opt_rules print state =
6778
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   122
  let
6903
682f8a9ec75d improved errors;
wenzelm
parents: 6877
diff changeset
   123
    fun err_if b msg = if b then raise Proof.STATE (msg, state) else ();
6778
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   124
    val fact = Proof.the_fact state;
7197
3ddf4a55d765 append user rules;
wenzelm
parents: 6903
diff changeset
   125
    val rules = Seq.of_list (if_none opt_rules [] @ get_local_rules state);
6903
682f8a9ec75d improved errors;
wenzelm
parents: 6877
diff changeset
   126
    val (initial, calculations) =
6778
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   127
      (case get_calculation state of
6903
682f8a9ec75d improved errors;
wenzelm
parents: 6877
diff changeset
   128
        None => (true, Seq.single fact)
682f8a9ec75d improved errors;
wenzelm
parents: 6877
diff changeset
   129
      | Some thm => (false, Seq.flat (Seq.map (Method.multi_resolve [thm, fact]) rules)));
6778
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   130
  in
6903
682f8a9ec75d improved errors;
wenzelm
parents: 6877
diff changeset
   131
    err_if (initial andalso final) "No calculation yet";
682f8a9ec75d improved errors;
wenzelm
parents: 6877
diff changeset
   132
    err_if (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given";
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
6877
3d5e5e6f9e20 also, finally: opt_rules;
wenzelm
parents: 6787
diff changeset
   138
          |> Proof.simple_have_thms calculationN []
3d5e5e6f9e20 also, finally: opt_rules;
wenzelm
parents: 6787
diff changeset
   139
          |> Proof.simple_have_thms "" [calc]
6787
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
6877
3d5e5e6f9e20 also, finally: opt_rules;
wenzelm
parents: 6787
diff changeset
   144
          |> Proof.simple_have_thms calculationN [calc]
6787
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;