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