src/Pure/Isar/calculation.ML
author wenzelm
Fri Apr 07 17:36:25 2000 +0200 (2000-04-07 ago)
changeset 8681 957a5fe9b212
parent 8649 dc496bb0638f
child 8807 0046be1769f9
permissions -rw-r--r--
apply etc.: comments;
     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 moreover: (thm list -> unit) -> Proof.state -> Proof.state
    19   val ultimately: (thm list -> unit) -> Proof.state -> Proof.state
    20   val setup: (theory -> theory) list
    21 end;
    22 
    23 structure Calculation: CALCULATION =
    24 struct
    25 
    26 (** global and local calculation data **)
    27 
    28 (* theory data kind 'Isar/calculation' *)
    29 
    30 fun print_rules rs = Pretty.writeln (Pretty.big_list "calculation rules:"
    31   (map Display.pretty_thm (NetRules.rules rs)));
    32 
    33 structure GlobalCalculationArgs =
    34 struct
    35   val name = "Isar/calculation";
    36   type T = thm NetRules.T
    37 
    38   val empty = NetRules.init_elim;
    39   val copy = I;
    40   val prep_ext = I;
    41   val merge = NetRules.merge;
    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 NetRules.T * (thm list * int) option;
    55 
    56   fun init thy = (GlobalCalculation.get thy, None);
    57   fun print _ (rs, _) = print_rules rs;
    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 fun mk_att f g (x, thm) = (f (g thm) x, thm);
    85 
    86 val trans_add_global = mk_att GlobalCalculation.map NetRules.insert;
    87 val trans_del_global = mk_att GlobalCalculation.map NetRules.delete;
    88 val trans_add_local = mk_att LocalCalculation.map (Library.apfst o NetRules.insert);
    89 val trans_del_local = mk_att LocalCalculation.map (Library.apfst o NetRules.delete);
    90 
    91 
    92 (* concrete syntax *)
    93 
    94 val trans_attr =
    95  (Attrib.add_del_args trans_add_global trans_del_global,
    96   Attrib.add_del_args trans_add_local trans_del_local);
    97 
    98 
    99 
   100 (** proof commands **)
   101 
   102 (* maintain calculation register *)
   103 
   104 val calculationN = "calculation";
   105 
   106 fun maintain_calculation false calc state =
   107       state
   108       |> put_calculation calc
   109       |> Proof.simple_have_thms calculationN calc
   110       |> Proof.reset_facts
   111   | maintain_calculation true calc state =
   112       state
   113       |> reset_calculation
   114       |> Proof.reset_thms calculationN
   115       |> Proof.simple_have_thms "" calc
   116       |> Proof.chain;
   117 
   118 
   119 (* 'also' and 'finally' *)
   120 
   121 fun err_if state b msg = if b then raise Proof.STATE (msg, state) else ();
   122 
   123 fun calculate final opt_rules print state =
   124   let
   125     val facts = Proof.the_facts state;
   126 
   127     val eq_prop = op aconv o pairself (#prop o Thm.rep_thm);
   128     fun differ thms thms' = not (Library.equal_lists eq_prop (thms, thms'));
   129 
   130     fun combine thms =
   131       let
   132         val ths = thms @ facts;
   133         val rs = get_local_rules state;
   134         val rules =
   135           (case ths of [] => NetRules.rules rs
   136           | th :: _ => NetRules.may_unify rs (Logic.strip_assums_concl (#prop (Thm.rep_thm th))));
   137         val ruleq = Seq.of_list (if_none opt_rules [] @ rules);
   138       in Seq.map Library.single (Seq.flat (Seq.map (Method.multi_resolve ths) ruleq)) end;
   139 
   140     val (initial, calculations) =
   141       (case get_calculation state of
   142         None => (true, Seq.single facts)
   143       | Some thms => (false, Seq.filter (differ thms) (combine thms)))
   144   in
   145     err_if state (initial andalso final) "No calculation yet";
   146     err_if state (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given";
   147     calculations |> Seq.map (fn calc => (print calc; state |> maintain_calculation final calc))
   148   end;
   149 
   150 fun also print = calculate false print;
   151 fun finally print = calculate true print;
   152 
   153 
   154 (* 'moreover' and 'ultimately' *)
   155 
   156 fun collect final print state =
   157   let
   158     val facts = Proof.the_facts state;
   159     val (initial, thms) =
   160       (case get_calculation state of
   161         None => (true, [])
   162       | Some thms => (false, thms));
   163     val calc = thms @ facts;
   164   in
   165     err_if state (initial andalso final) "No calculation yet";
   166     print calc;
   167     state |> maintain_calculation final calc
   168   end;
   169 
   170 fun moreover print = collect false print;
   171 fun ultimately print = collect true print;
   172 
   173 
   174 
   175 (** theory setup **)
   176 
   177 val setup = [GlobalCalculation.init, LocalCalculation.init,
   178   Attrib.add_attributes [("trans", trans_attr, "declare transitivity rule")]];
   179 
   180 
   181 end;