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