src/Pure/Isar/calculation.ML
author wenzelm
Tue Jul 16 18:38:36 2002 +0200 (2002-07-16)
changeset 13371 82a057cf4413
parent 12805 3be853cf19cf
child 14282 b23f028c1651
permissions -rw-r--r--
avoid "_st" versions of proof data;
     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 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: thm list option -> (Proof.context -> thm list -> unit)
    24     -> Proof.state -> Proof.state Seq.seq
    25   val finally: thm list option -> (Proof.context -> thm list -> unit)
    26     -> Proof.state -> Proof.state Seq.seq
    27   val moreover: (Proof.context -> thm list -> unit) -> Proof.state -> Proof.state
    28   val ultimately: (Proof.context -> thm list -> unit) -> Proof.state -> Proof.state
    29   val setup: (theory -> theory) list
    30 end;
    31 
    32 structure Calculation: CALCULATION =
    33 struct
    34 
    35 (** global and local calculation data **)
    36 
    37 (* theory data kind 'Isar/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 GlobalCalculationArgs =
    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 prep_ext = 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 structure GlobalCalculation = TheoryDataFun(GlobalCalculationArgs);
    58 val print_global_rules = GlobalCalculation.print;
    59 
    60 
    61 (* proof data kind 'Isar/calculation' *)
    62 
    63 structure LocalCalculationArgs =
    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 structure LocalCalculation = ProofDataFun(LocalCalculationArgs);
    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 fun put_calculation thms state =
    85   Proof.map_context
    86     (LocalCalculation.put (get_local_rules state, Some (thms, Proof.level state))) state;
    87 
    88 fun reset_calculation state =
    89   Proof.map_context (LocalCalculation.put (get_local_rules state, None)) state;
    90 
    91 
    92 
    93 (** attributes **)
    94 
    95 (* add/del rules *)
    96 
    97 fun global_att f (x, thm) = (GlobalCalculation.map (f thm) x, thm);
    98 fun local_att f (x, thm) = (LocalCalculation.map (apfst (f thm)) x, thm);
    99 
   100 val trans_add_global = global_att (apfst o NetRules.insert);
   101 val trans_del_global = global_att (apfst o NetRules.delete);
   102 val trans_add_local = local_att (apfst o NetRules.insert);
   103 val trans_del_local = local_att (apfst o NetRules.delete);
   104 
   105 val sym_add_global = global_att (apsnd o Drule.add_rule) o ContextRules.elim_query_global None;
   106 val sym_del_global = global_att (apsnd o Drule.del_rule) o ContextRules.rule_del_global;
   107 val sym_add_local = local_att (apsnd o Drule.add_rule) o ContextRules.elim_query_local None;
   108 val sym_del_local = local_att (apsnd o Drule.del_rule) o ContextRules.rule_del_local;
   109 
   110 
   111 (* symmetry *)
   112 
   113 fun gen_symmetric get_sym = Drule.rule_attribute (fn x => fn th =>
   114   (case Seq.chop (2, Method.multi_resolves [th] (get_sym x)) of
   115     ([th'], _) => th'
   116   | ([], _) => raise THM ("symmetric: no unifiers", 1, [th])
   117   | _ => raise THM ("symmetric: multiple unifiers", 1, [th])));
   118 
   119 val symmetric_global = gen_symmetric (#2 o GlobalCalculation.get);
   120 val symmetric_local = gen_symmetric (#2 o #1 o LocalCalculation.get);
   121 
   122 
   123 (* concrete syntax *)
   124 
   125 val trans_attr =
   126  (Attrib.add_del_args trans_add_global trans_del_global,
   127   Attrib.add_del_args trans_add_local trans_del_local);
   128 
   129 val sym_attr =
   130  (Attrib.add_del_args sym_add_global sym_del_global,
   131   Attrib.add_del_args sym_add_local sym_del_local);
   132 
   133 
   134 
   135 (** proof commands **)
   136 
   137 (* maintain calculation register *)
   138 
   139 val calculationN = "calculation";
   140 
   141 fun maintain_calculation false calc state =
   142       state
   143       |> put_calculation calc
   144       |> Proof.simple_have_thms calculationN calc
   145       |> Proof.reset_facts
   146   | maintain_calculation true calc state =
   147       state
   148       |> reset_calculation
   149       |> Proof.reset_thms calculationN
   150       |> Proof.simple_have_thms "" calc
   151       |> Proof.chain;
   152 
   153 
   154 (* 'also' and 'finally' *)
   155 
   156 fun err_if state b msg = if b then raise Proof.STATE (msg, state) else ();
   157 
   158 fun calculate final opt_rules print state =
   159   let
   160     val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of;
   161     val eq_prop = op aconv o pairself (Pattern.eta_contract o strip_assums_concl);
   162     fun projection ths th = Library.exists (Library.curry eq_prop th) ths;
   163 
   164     fun combine ths =
   165       (case opt_rules of Some rules => rules
   166       | None =>
   167           (case ths of [] => NetRules.rules (#1 (get_local_rules state))
   168           | th :: _ => NetRules.retrieve (#1 (get_local_rules state)) (strip_assums_concl th)))
   169       |> Seq.of_list |> Seq.map (Method.multi_resolve ths) |> Seq.flat
   170       |> Seq.filter (not o projection ths);
   171 
   172     val facts = Proof.the_facts (Proof.assert_forward state);
   173     val (initial, calculations) =
   174       (case get_calculation state of
   175         None => (true, Seq.single facts)
   176       | Some calc => (false, Seq.map single (combine (calc @ facts))));
   177   in
   178     err_if state (initial andalso final) "No calculation yet";
   179     err_if state (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given";
   180     calculations |> Seq.map (fn calc => (print (Proof.context_of state) calc;
   181         state |> maintain_calculation final calc))
   182   end;
   183 
   184 fun also print = calculate false print;
   185 fun finally print = calculate true print;
   186 
   187 
   188 (* 'moreover' and 'ultimately' *)
   189 
   190 fun collect final print state =
   191   let
   192     val facts = Proof.the_facts (Proof.assert_forward state);
   193     val (initial, thms) =
   194       (case get_calculation state of
   195         None => (true, [])
   196       | Some thms => (false, thms));
   197     val calc = thms @ facts;
   198   in
   199     err_if state (initial andalso final) "No calculation yet";
   200     print (Proof.context_of state) calc;
   201     state |> maintain_calculation final calc
   202   end;
   203 
   204 fun moreover print = collect false print;
   205 fun ultimately print = collect true print;
   206 
   207 
   208 
   209 (** theory setup **)
   210 
   211 val setup =
   212  [GlobalCalculation.init, LocalCalculation.init,
   213   Attrib.add_attributes
   214    [("trans", trans_attr, "declaration of transitivity rule"),
   215     ("sym", sym_attr, "declaration of symmetry rule"),
   216     ("symmetric", (Attrib.no_args symmetric_global, Attrib.no_args symmetric_local),
   217       "resolution with symmetry rule")],
   218   #1 o PureThy.add_thms
   219    [(("", transitive_thm), [trans_add_global]),
   220     (("", symmetric_thm), [sym_add_global])]];
   221 
   222 end;