src/Pure/Isar/calculation.ML
author wenzelm
Wed Sep 29 13:49:07 1999 +0200 (1999-09-29)
changeset 7632 25a0d2ba3a87
parent 7600 73f91da46230
child 8150 7021549ef32d
permissions -rw-r--r--
removed extra shyps error;
     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 list -> unit) -> Proof.state -> Proof.state Seq.seq
    17   val finally: thm list option -> (thm list -> 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 list * 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_st;
    62 val print_local_rules = LocalCalculation.print;
    63 
    64 
    65 (* access calculation *)
    66 
    67 fun get_calculation state =
    68   (case #2 (LocalCalculation.get_st state) of
    69     None => None
    70   | Some (thms, lev) => if lev = Proof.level state then Some thms else None);
    71 
    72 fun put_calculation thms state =
    73   LocalCalculation.put_st (get_local_rules state, Some (thms, Proof.level state)) state;
    74 
    75 fun reset_calculation state =
    76   LocalCalculation.put_st (get_local_rules state, None) state;
    77 
    78 
    79 
    80 (** attributes **)
    81 
    82 (* trans add/del *)
    83 
    84 local
    85 
    86 fun map_rules_global f thy = GlobalCalculation.put (f (GlobalCalculation.get thy)) thy;
    87 fun map_rules_local f ctxt = LocalCalculation.put (f (LocalCalculation.get ctxt)) ctxt;
    88 
    89 fun add_trans thm rules = Library.gen_ins Thm.eq_thm (thm, rules);
    90 fun del_trans thm rules = Library.gen_rem Thm.eq_thm (rules, thm);
    91 
    92 fun mk_att f g (x, thm) = (f (g thm) x, thm);
    93 
    94 in
    95 
    96 val trans_add_global = mk_att map_rules_global add_trans;
    97 val trans_del_global = mk_att map_rules_global del_trans;
    98 val trans_add_local = mk_att map_rules_local (Library.apfst o add_trans);
    99 val trans_del_local = mk_att map_rules_local (Library.apfst o del_trans);
   100 
   101 end;
   102 
   103 
   104 (* concrete syntax *)
   105 
   106 val transN = "trans";
   107 val addN = "add";
   108 val delN = "del";
   109 
   110 fun trans_att add del =
   111   Attrib.syntax (Scan.lift (Args.$$$ addN >> K add || Args.$$$ delN >> K del || Scan.succeed add));
   112 
   113 val trans_attr =
   114   (trans_att trans_add_global trans_del_global, trans_att trans_add_local trans_del_local);
   115 
   116 
   117 
   118 (** proof commands **)
   119 
   120 val calculationN = "calculation";
   121 
   122 fun calculate final opt_rules print state =
   123   let
   124     fun err_if b msg = if b then raise Proof.STATE (msg, state) else ();
   125     val facts = Proof.the_facts state;
   126     val rules = Seq.of_list (if_none opt_rules [] @ get_local_rules state);
   127 
   128     val eq_prop = op aconv o pairself (#prop o Thm.rep_thm);
   129     fun differ thms thms' = not (Library.equal_lists eq_prop (thms, thms'));
   130     fun combine thms =
   131       Seq.map Library.single (Seq.flat (Seq.map (Method.multi_resolve (thms @ facts)) rules));
   132 
   133     val (initial, calculations) =
   134       (case get_calculation state of
   135         None => (true, Seq.single facts)
   136       | Some thms => (false, Seq.filter (differ thms) (combine thms)))
   137   in
   138     err_if (initial andalso final) "No calculation yet";
   139     err_if (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given";
   140     calculations |> Seq.map (fn calc =>
   141       (print calc;
   142         (if final then
   143           state
   144           |> reset_calculation
   145           |> Proof.reset_thms calculationN
   146           |> Proof.simple_have_thms "" calc
   147           |> Proof.chain
   148         else
   149           state
   150           |> put_calculation calc
   151           |> Proof.simple_have_thms calculationN calc
   152           |> Proof.reset_facts)))
   153   end;
   154 
   155 fun also print = calculate false print;
   156 fun finally print = calculate true print;
   157 
   158 
   159 
   160 (** theory setup **)
   161 
   162 val setup = [GlobalCalculation.init, LocalCalculation.init,
   163   Attrib.add_attributes [(transN, trans_attr, "transitivity rule")]];
   164 
   165 
   166 end;