src/Pure/Isar/calculation.ML
author wenzelm
Fri Nov 09 00:19:20 2001 +0100 (2001-11-09)
changeset 12123 739eba13e2cd
parent 12055 a9c44895cc8c
child 12311 ce5f9e61c037
permissions -rw-r--r--
theory data: finish method;
     1 (*  Title:      Pure/Isar/calculation.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 Support for calculational proofs.
     7 *)
     8 
     9 signature CALCULATION =
    10 sig
    11   val print_global_rules: theory -> unit
    12   val print_local_rules: Proof.context -> unit
    13   val trans_add_global: theory attribute
    14   val trans_del_global: theory attribute
    15   val trans_add_local: Proof.context attribute
    16   val trans_del_local: Proof.context attribute
    17   val also: thm list option -> (Proof.context -> thm list -> unit)
    18     -> Proof.state -> Proof.state Seq.seq
    19   val finally: thm list option -> (Proof.context -> thm list -> unit)
    20     -> Proof.state -> Proof.state Seq.seq
    21   val moreover: (Proof.context -> thm list -> unit) -> Proof.state -> Proof.state
    22   val ultimately: (Proof.context -> thm list -> unit) -> Proof.state -> Proof.state
    23   val setup: (theory -> theory) list
    24 end;
    25 
    26 structure Calculation: CALCULATION =
    27 struct
    28 
    29 (** global and local calculation data **)
    30 
    31 (* theory data kind 'Isar/calculation' *)
    32 
    33 fun print_rules prt x rs =
    34   Pretty.writeln (Pretty.big_list "transitivity rules:" (map (prt x) (NetRules.rules rs)));
    35 
    36 structure GlobalCalculationArgs =
    37 struct
    38   val name = "Isar/calculation";
    39   type T = thm NetRules.T
    40 
    41   val empty = NetRules.elim;
    42   val copy = I;
    43   val finish = I;
    44   val prep_ext = I;
    45   val merge = NetRules.merge;
    46   val print = print_rules Display.pretty_thm_sg;
    47 end;
    48 
    49 structure GlobalCalculation = TheoryDataFun(GlobalCalculationArgs);
    50 val print_global_rules = GlobalCalculation.print;
    51 
    52 
    53 (* proof data kind 'Isar/calculation' *)
    54 
    55 structure LocalCalculationArgs =
    56 struct
    57   val name = "Isar/calculation";
    58   type T = thm NetRules.T * (thm list * int) option;
    59 
    60   fun init thy = (GlobalCalculation.get thy, None);
    61   fun print ctxt (rs, _) = print_rules ProofContext.pretty_thm ctxt rs;
    62 end;
    63 
    64 structure LocalCalculation = ProofDataFun(LocalCalculationArgs);
    65 val get_local_rules = #1 o LocalCalculation.get_st;
    66 val print_local_rules = LocalCalculation.print;
    67 
    68 
    69 (* access calculation *)
    70 
    71 fun get_calculation state =
    72   (case #2 (LocalCalculation.get_st state) of
    73     None => None
    74   | Some (thms, lev) => if lev = Proof.level state then Some thms else None);
    75 
    76 fun put_calculation thms state =
    77   LocalCalculation.put_st (get_local_rules state, Some (thms, Proof.level state)) state;
    78 
    79 fun reset_calculation state =
    80   LocalCalculation.put_st (get_local_rules state, None) state;
    81 
    82 
    83 
    84 (** attributes **)
    85 
    86 (* trans add/del *)
    87 
    88 fun mk_att f g (x, thm) = (f (g thm) x, thm);
    89 
    90 val trans_add_global = mk_att GlobalCalculation.map NetRules.insert;
    91 val trans_del_global = mk_att GlobalCalculation.map NetRules.delete;
    92 val trans_add_local = mk_att LocalCalculation.map (Library.apfst o NetRules.insert);
    93 val trans_del_local = mk_att LocalCalculation.map (Library.apfst o NetRules.delete);
    94 
    95 
    96 (* concrete syntax *)
    97 
    98 val trans_attr =
    99  (Attrib.add_del_args trans_add_global trans_del_global,
   100   Attrib.add_del_args trans_add_local trans_del_local);
   101 
   102 
   103 
   104 (** proof commands **)
   105 
   106 (* maintain calculation register *)
   107 
   108 val calculationN = "calculation";
   109 
   110 fun maintain_calculation false calc state =
   111       state
   112       |> put_calculation calc
   113       |> Proof.simple_have_thms calculationN calc
   114       |> Proof.reset_facts
   115   | maintain_calculation true calc state =
   116       state
   117       |> reset_calculation
   118       |> Proof.reset_thms calculationN
   119       |> Proof.simple_have_thms "" calc
   120       |> Proof.chain;
   121 
   122 
   123 (* 'also' and 'finally' *)
   124 
   125 fun err_if state b msg = if b then raise Proof.STATE (msg, state) else ();
   126 
   127 fun calculate final opt_rules print state =
   128   let
   129     val strip_assums_concl = Logic.strip_assums_concl o #prop o Thm.rep_thm;
   130     val eq_prop = op aconv o pairself (Pattern.eta_contract o strip_assums_concl);
   131     fun projection ths th = Library.exists (Library.curry eq_prop th) ths;
   132 
   133     fun combine ths =
   134       (case opt_rules of Some rules => rules
   135       | None =>
   136           (case ths of [] => NetRules.rules (get_local_rules state)
   137           | th :: _ => NetRules.retrieve (get_local_rules state) (strip_assums_concl th)))
   138       |> Seq.of_list |> Seq.map (Method.multi_resolve ths) |> Seq.flat
   139       |> Seq.filter (not o projection ths);
   140 
   141     val facts = Proof.the_facts (Proof.assert_forward state);
   142     val (initial, calculations) =
   143       (case get_calculation state of
   144         None => (true, Seq.single facts)
   145       | Some calc => (false, Seq.map single (combine (calc @ facts))));
   146   in
   147     err_if state (initial andalso final) "No calculation yet";
   148     err_if state (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given";
   149     calculations |> Seq.map (fn calc => (print (Proof.context_of state) calc;
   150         state |> maintain_calculation final calc))
   151   end;
   152 
   153 fun also print = calculate false print;
   154 fun finally print = calculate true print;
   155 
   156 
   157 (* 'moreover' and 'ultimately' *)
   158 
   159 fun collect final print state =
   160   let
   161     val facts = Proof.the_facts (Proof.assert_forward state);
   162     val (initial, thms) =
   163       (case get_calculation state of
   164         None => (true, [])
   165       | Some thms => (false, thms));
   166     val calc = thms @ facts;
   167   in
   168     err_if state (initial andalso final) "No calculation yet";
   169     print (Proof.context_of state) calc;
   170     state |> maintain_calculation final calc
   171   end;
   172 
   173 fun moreover print = collect false print;
   174 fun ultimately print = collect true print;
   175 
   176 
   177 
   178 (** theory setup **)
   179 
   180 val setup = [GlobalCalculation.init, LocalCalculation.init,
   181   Attrib.add_attributes [("trans", trans_attr, "declaration of transitivity rule")],
   182   #1 o PureThy.add_thms [(("", transitive_thm), [trans_add_global])]];
   183 
   184 
   185 end;