src/Pure/Isar/calculation.ML
author wenzelm
Fri, 04 Jun 1999 19:55:41 +0200
changeset 6778 2f66eea8a025
child 6781 0db24da2a3c1
permissions -rw-r--r--
Support for calculational proofs.
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);
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    61
val get_local_rules = #1 o LocalCalculation.get o Proof.context_of;
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 =
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    68
  (case #2 (LocalCalculation.get (Proof.context_of state)) of
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
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    75
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    76
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    77
(** attributes **)
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    78
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    79
(* trans add/del *)
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    80
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    81
local
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    82
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    83
fun map_rules_global f thy = GlobalCalculation.put (f (GlobalCalculation.get thy)) thy;
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    84
fun map_rules_local f ctxt = LocalCalculation.put (f (LocalCalculation.get ctxt)) ctxt;
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    85
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    86
fun add_trans thm rules = Library.gen_ins Thm.eq_thm (thm, rules);
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    87
fun del_trans thm rules = Library.gen_rem Thm.eq_thm (rules, thm);
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    88
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    89
fun mk_att f g (x, thm) = (f (g thm) x, thm);
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    90
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    91
in
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    92
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    93
val trans_add_global = mk_att map_rules_global add_trans;
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    94
val trans_del_global = mk_att map_rules_global del_trans;
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    95
val trans_add_local = mk_att map_rules_local (Library.apfst o add_trans);
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    96
val trans_del_local = mk_att map_rules_local (Library.apfst o del_trans);
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    97
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    98
end;
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
    99
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   100
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   101
(* concrete syntax *)
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   102
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   103
val transN = "trans";
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   104
val addN = "add";
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   105
val delN = "del";
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   106
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   107
fun trans_att add del =
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   108
  Attrib.syntax (Scan.lift (Args.$$$ addN >> K add || Args.$$$ delN >> K del || Scan.succeed add));
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   109
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   110
val trans_attr =
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   111
  (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
   112
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   113
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   114
(** proof commands **)
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   115
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   116
val calculationN = "calculation";
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   117
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   118
fun calculate final prt state =
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   119
  let
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   120
    val fact = Proof.the_fact state;
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   121
    val dddot = ObjectLogic.dest_main_statement (#prop (Thm.rep_thm fact)) handle TERM _ =>
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   122
      raise Proof.STATE ("Unable to bind '...' pattern from current fact", state);
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   123
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   124
    val name = if final then "" else calculationN;
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   125
    fun have_thm thm = Proof.have_thmss name [] [([thm], [])];
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   126
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
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   133
    calculations
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   134
    |> Seq.map (fn calc =>
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   135
      (prt calc;
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   136
        state
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   137
        |> Proof.bind_i [(Syntax.dddot_indexname, dddot)]
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   138
        |> have_thm calc
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   139
        |> (if final then I else Proof.reset_facts)))
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   140
  end;
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   141
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   142
val also = calculate false;
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   143
val finally = calculate true;
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   144
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   145
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   146
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   147
(** theory setup **)
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   148
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   149
val setup = [GlobalCalculation.init, LocalCalculation.init,
2f66eea8a025 Support for calculational proofs.
wenzelm
parents:
diff changeset
   150
  Attrib.add_attributes [(transN, trans_attr, "transitivity rule")]];
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
end;