src/Pure/Isar/calculation.ML
author wenzelm
Wed Sep 14 22:04:35 2005 +0200 (2005-09-14)
changeset 17384 c01de5939f5b
parent 17350 26cd3756377a
child 18223 20830cb4428c
permissions -rw-r--r--
tuned;
     1 (*  Title:      Pure/Isar/calculation.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Generic calculational proofs.
     6 *)
     7 
     8 signature CALCULATION =
     9 sig
    10   val get_calculation: Proof.state -> thm list option
    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 sym_add_global: theory attribute
    18   val sym_del_global: theory attribute
    19   val sym_add_local: Proof.context attribute
    20   val sym_del_local: Proof.context attribute
    21   val symmetric_global: theory attribute
    22   val symmetric_local: Proof.context attribute
    23   val also: (thmref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq
    24   val also_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
    25   val finally: (thmref * Attrib.src list) list option -> bool ->
    26     Proof.state -> Proof.state Seq.seq
    27   val finally_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
    28   val moreover: bool -> Proof.state -> Proof.state
    29   val ultimately: bool -> Proof.state -> Proof.state
    30 end;
    31 
    32 structure Calculation: CALCULATION =
    33 struct
    34 
    35 (** global and local calculation data **)
    36 
    37 (* global calculation *)
    38 
    39 fun print_rules prt x (trans, sym) =
    40   [Pretty.big_list "transitivity rules:" (map (prt x) (NetRules.rules trans)),
    41     Pretty.big_list "symmetry rules:" (map (prt x) sym)]
    42   |> Pretty.chunks |> Pretty.writeln;
    43 
    44 structure GlobalCalculation = TheoryDataFun
    45 (struct
    46   val name = "Isar/calculation";
    47   type T = thm NetRules.T * thm list
    48 
    49   val empty = (NetRules.elim, []);
    50   val copy = I;
    51   val extend = I;
    52   fun merge _ ((trans1, sym1), (trans2, sym2)) =
    53     (NetRules.merge (trans1, trans2), Drule.merge_rules (sym1, sym2));
    54   val print = print_rules Display.pretty_thm_sg;
    55 end);
    56 
    57 val _ = Context.add_setup [GlobalCalculation.init];
    58 val print_global_rules = GlobalCalculation.print;
    59 
    60 
    61 (* local calculation *)
    62 
    63 structure LocalCalculation = ProofDataFun
    64 (struct
    65   val name = "Isar/calculation";
    66   type T = (thm NetRules.T * thm list) * (thm list * int) option;
    67 
    68   fun init thy = (GlobalCalculation.get thy, NONE);
    69   fun print ctxt (rs, _) = print_rules ProofContext.pretty_thm ctxt rs;
    70 end);
    71 
    72 val _ = Context.add_setup [LocalCalculation.init];
    73 val get_local_rules = #1 o LocalCalculation.get o Proof.context_of;
    74 val print_local_rules = LocalCalculation.print;
    75 
    76 
    77 (* access calculation *)
    78 
    79 fun get_calculation state =
    80   (case #2 (LocalCalculation.get (Proof.context_of state)) of
    81     NONE => NONE
    82   | SOME (thms, lev) => if lev = Proof.level state then SOME thms else NONE);
    83 
    84 val calculationN = "calculation";
    85 
    86 fun put_calculation calc =
    87   `Proof.level #-> (fn lev => Proof.map_context
    88     (LocalCalculation.map (apsnd (K (Option.map (rpair lev) calc)))))
    89   #> Proof.put_thms (calculationN, calc);
    90 
    91 
    92 (** attributes **)
    93 
    94 (* add/del rules *)
    95 
    96 fun global_att f (x, thm) = (GlobalCalculation.map (f thm) x, thm);
    97 fun local_att f (x, thm) = (LocalCalculation.map (apfst (f thm)) x, thm);
    98 
    99 val trans_add_global = global_att (apfst o NetRules.insert);
   100 val trans_del_global = global_att (apfst o NetRules.delete);
   101 val trans_add_local = local_att (apfst o NetRules.insert);
   102 val trans_del_local = local_att (apfst o NetRules.delete);
   103 
   104 val sym_add_global = global_att (apsnd o Drule.add_rule) o ContextRules.elim_query_global NONE;
   105 val sym_del_global = global_att (apsnd o Drule.del_rule) o ContextRules.rule_del_global;
   106 val sym_add_local = local_att (apsnd o Drule.add_rule) o ContextRules.elim_query_local NONE;
   107 val sym_del_local = local_att (apsnd o Drule.del_rule) o ContextRules.rule_del_local;
   108 
   109 
   110 (* symmetry *)
   111 
   112 fun gen_symmetric get_sym = Drule.rule_attribute (fn x => fn th =>
   113   (case Seq.chop (2, Method.multi_resolves [th] (get_sym x)) of
   114     ([th'], _) => th'
   115   | ([], _) => raise THM ("symmetric: no unifiers", 1, [th])
   116   | _ => raise THM ("symmetric: multiple unifiers", 1, [th])));
   117 
   118 val symmetric_global = gen_symmetric (#2 o GlobalCalculation.get);
   119 val symmetric_local = gen_symmetric (#2 o #1 o LocalCalculation.get);
   120 
   121 
   122 (* concrete syntax *)
   123 
   124 val trans_attr =
   125  (Attrib.add_del_args trans_add_global trans_del_global,
   126   Attrib.add_del_args trans_add_local trans_del_local);
   127 
   128 val sym_attr =
   129  (Attrib.add_del_args sym_add_global sym_del_global,
   130   Attrib.add_del_args sym_add_local sym_del_local);
   131 
   132 val _ = Context.add_setup
   133  [Attrib.add_attributes
   134    [("trans", trans_attr, "declaration of transitivity rule"),
   135     ("sym", sym_attr, "declaration of symmetry rule"),
   136     ("symmetric", (Attrib.no_args symmetric_global, Attrib.no_args symmetric_local),
   137       "resolution with symmetry rule")],
   138   #1 o PureThy.add_thms
   139    [(("", transitive_thm), [trans_add_global]),
   140     (("", symmetric_thm), [sym_add_global])]];
   141 
   142 
   143 
   144 (** proof commands **)
   145 
   146 fun err_if state b msg = if b then raise Proof.STATE (msg, state) else ();
   147 
   148 fun assert_sane final =
   149   if final then Proof.assert_forward else Proof.assert_forward_or_chain;
   150 
   151 fun maintain_calculation false calc = put_calculation (SOME calc)
   152   | maintain_calculation true calc = put_calculation NONE #> Proof.chain_facts calc;
   153 
   154 fun print_calculation false _ _ = ()
   155   | print_calculation true ctxt calc =
   156       Pretty.writeln (ProofContext.pretty_fact ctxt (calculationN, calc));
   157 
   158 
   159 (* also and finally *)
   160 
   161 fun calculate prep_rules final raw_rules int state =
   162   let
   163     val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of;
   164     val eq_prop = op aconv o pairself (Pattern.eta_contract o strip_assums_concl);
   165     fun projection ths th = Library.exists (Library.curry eq_prop th) ths;
   166 
   167     val opt_rules = Option.map (prep_rules state) raw_rules;
   168     fun combine ths =
   169       (case opt_rules of SOME rules => rules
   170       | NONE =>
   171           (case ths of [] => NetRules.rules (#1 (get_local_rules state))
   172           | th :: _ => NetRules.retrieve (#1 (get_local_rules state)) (strip_assums_concl th)))
   173       |> Seq.of_list |> Seq.maps (Method.multi_resolve ths)
   174       |> Seq.filter (not o projection ths);
   175 
   176     val facts = Proof.the_facts (assert_sane final state);
   177     val (initial, calculations) =
   178       (case get_calculation state of
   179         NONE => (true, Seq.single facts)
   180       | SOME calc => (false, Seq.map single (combine (calc @ facts))));
   181   in
   182     err_if state (initial andalso final) "No calculation yet";
   183     err_if state (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given";
   184     calculations |> Seq.map (fn calc => (print_calculation int (Proof.context_of state) calc;
   185         state |> maintain_calculation final calc))
   186   end;
   187 
   188 val also = calculate Proof.get_thmss false;
   189 val also_i = calculate (K I) false;
   190 val finally = calculate Proof.get_thmss true;
   191 val finally_i = calculate (K I) true;
   192 
   193 
   194 (* moreover and ultimately *)
   195 
   196 fun collect final int state =
   197   let
   198     val facts = Proof.the_facts (assert_sane final state);
   199     val (initial, thms) =
   200       (case get_calculation state of
   201         NONE => (true, [])
   202       | SOME thms => (false, thms));
   203     val calc = thms @ facts;
   204   in
   205     err_if state (initial andalso final) "No calculation yet";
   206     print_calculation int (Proof.context_of state) calc;
   207     state |> maintain_calculation final calc
   208   end;
   209 
   210 val moreover = collect false;
   211 val ultimately = collect true;
   212 
   213 end;