src/Pure/Isar/calculation.ML
changeset 6778 2f66eea8a025
child 6781 0db24da2a3c1
equal deleted inserted replaced
6777:175ff298ac0e 6778:2f66eea8a025
       
     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 -> unit) -> Proof.state -> Proof.state Seq.seq
       
    17   val finally: (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 
       
    31 (* theory data kind 'Isar/calculation' *)
       
    32 
       
    33 structure GlobalCalculationArgs =
       
    34 struct
       
    35   val name = "Isar/calculation";
       
    36   type T = thm list;
       
    37 
       
    38   val empty = [];
       
    39   val copy = I;
       
    40   val prep_ext = I;
       
    41   fun merge (ths1, ths2) = Library.generic_merge Thm.eq_thm I I ths1 ths2;
       
    42   fun print _ = print_rules;
       
    43 end;
       
    44 
       
    45 structure GlobalCalculation = TheoryDataFun(GlobalCalculationArgs);
       
    46 val print_global_rules = GlobalCalculation.print;
       
    47 
       
    48 
       
    49 (* proof data kind 'Isar/calculation' *)
       
    50 
       
    51 structure LocalCalculationArgs =
       
    52 struct
       
    53   val name = "Isar/calculation";
       
    54   type T = thm list * (thm * int) option;
       
    55 
       
    56   fun init thy = (GlobalCalculation.get thy, None);
       
    57   fun print _ (ths, _) = print_rules ths;
       
    58 end;
       
    59 
       
    60 structure LocalCalculation = ProofDataFun(LocalCalculationArgs);
       
    61 val get_local_rules = #1 o LocalCalculation.get o Proof.context_of;
       
    62 val print_local_rules = LocalCalculation.print;
       
    63 
       
    64 
       
    65 (* access calculation *)
       
    66 
       
    67 fun get_calculation state =
       
    68   (case #2 (LocalCalculation.get (Proof.context_of state)) of
       
    69     None => None
       
    70   | Some (thm, lev) => if lev = Proof.level state then Some thm else None);
       
    71 
       
    72 fun put_calculation thm state =
       
    73   LocalCalculation.put_st (get_local_rules state, Some (thm, Proof.level state)) state;
       
    74 
       
    75 
       
    76 
       
    77 (** attributes **)
       
    78 
       
    79 (* trans add/del *)
       
    80 
       
    81 local
       
    82 
       
    83 fun map_rules_global f thy = GlobalCalculation.put (f (GlobalCalculation.get thy)) thy;
       
    84 fun map_rules_local f ctxt = LocalCalculation.put (f (LocalCalculation.get ctxt)) ctxt;
       
    85 
       
    86 fun add_trans thm rules = Library.gen_ins Thm.eq_thm (thm, rules);
       
    87 fun del_trans thm rules = Library.gen_rem Thm.eq_thm (rules, thm);
       
    88 
       
    89 fun mk_att f g (x, thm) = (f (g thm) x, thm);
       
    90 
       
    91 in
       
    92 
       
    93 val trans_add_global = mk_att map_rules_global add_trans;
       
    94 val trans_del_global = mk_att map_rules_global del_trans;
       
    95 val trans_add_local = mk_att map_rules_local (Library.apfst o add_trans);
       
    96 val trans_del_local = mk_att map_rules_local (Library.apfst o del_trans);
       
    97 
       
    98 end;
       
    99 
       
   100 
       
   101 (* concrete syntax *)
       
   102 
       
   103 val transN = "trans";
       
   104 val addN = "add";
       
   105 val delN = "del";
       
   106 
       
   107 fun trans_att add del =
       
   108   Attrib.syntax (Scan.lift (Args.$$$ addN >> K add || Args.$$$ delN >> K del || Scan.succeed add));
       
   109 
       
   110 val trans_attr =
       
   111   (trans_att trans_add_global trans_del_global, trans_att trans_add_local trans_del_local);
       
   112 
       
   113 
       
   114 (** proof commands **)
       
   115 
       
   116 val calculationN = "calculation";
       
   117 
       
   118 fun calculate final prt state =
       
   119   let
       
   120     val fact = Proof.the_fact state;
       
   121     val dddot = ObjectLogic.dest_main_statement (#prop (Thm.rep_thm fact)) handle TERM _ =>
       
   122       raise Proof.STATE ("Unable to bind '...' pattern from current fact", state);
       
   123 
       
   124     val name = if final then "" else calculationN;
       
   125     fun have_thm thm = Proof.have_thmss name [] [([thm], [])];
       
   126 
       
   127     val rules = Seq.of_list (get_local_rules state);
       
   128     val calculations =
       
   129       (case get_calculation state of
       
   130         None => Seq.single fact
       
   131       | Some thm => Seq.flat (Seq.map (Method.multi_resolve [thm, fact]) rules));
       
   132   in
       
   133     calculations
       
   134     |> Seq.map (fn calc =>
       
   135       (prt calc;
       
   136         state
       
   137         |> Proof.bind_i [(Syntax.dddot_indexname, dddot)]
       
   138         |> have_thm calc
       
   139         |> (if final then I else Proof.reset_facts)))
       
   140   end;
       
   141 
       
   142 val also = calculate false;
       
   143 val finally = calculate true;
       
   144 
       
   145 
       
   146 
       
   147 (** theory setup **)
       
   148 
       
   149 val setup = [GlobalCalculation.init, LocalCalculation.init,
       
   150   Attrib.add_attributes [(transN, trans_attr, "transitivity rule")]];
       
   151 
       
   152 
       
   153 end;