src/Pure/Isar/calculation.ML
author skalberg
Thu Mar 03 12:43:01 2005 +0100 (2005-03-03)
changeset 15570 8d8c70b41bab
parent 15531 08c8dad8e399
child 15801 d2f5ca3c048d
permissions -rw-r--r--
Move towards standard functions.
     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 sym_add_global: theory attribute
    17   val sym_del_global: theory attribute
    18   val sym_add_local: Proof.context attribute
    19   val sym_del_local: Proof.context attribute
    20   val symmetric_global: theory attribute
    21   val symmetric_local: Proof.context attribute
    22   val also: thm list option -> (Proof.context -> thm list -> unit)
    23     -> Proof.state -> Proof.state Seq.seq
    24   val finally: thm list option -> (Proof.context -> thm list -> unit)
    25     -> Proof.state -> Proof.state Seq.seq
    26   val moreover: (Proof.context -> thm list -> unit) -> Proof.state -> Proof.state
    27   val ultimately: (Proof.context -> thm list -> unit) -> Proof.state -> Proof.state
    28   val setup: (theory -> theory) list
    29 end;
    30 
    31 structure Calculation: CALCULATION =
    32 struct
    33 
    34 (** global and local calculation data **)
    35 
    36 (* theory data kind 'Isar/calculation' *)
    37 
    38 fun print_rules prt x (trans, sym) =
    39   [Pretty.big_list "transitivity rules:" (map (prt x) (NetRules.rules trans)),
    40     Pretty.big_list "symmetry rules:" (map (prt x) sym)]
    41   |> Pretty.chunks |> Pretty.writeln;
    42 
    43 structure GlobalCalculationArgs =
    44 struct
    45   val name = "Isar/calculation";
    46   type T = thm NetRules.T * thm list
    47 
    48   val empty = (NetRules.elim, []);
    49   val copy = I;
    50   val prep_ext = I;
    51   fun merge ((trans1, sym1), (trans2, sym2)) =
    52     (NetRules.merge (trans1, trans2), Drule.merge_rules (sym1, sym2));
    53   val print = print_rules Display.pretty_thm_sg;
    54 end;
    55 
    56 structure GlobalCalculation = TheoryDataFun(GlobalCalculationArgs);
    57 val print_global_rules = GlobalCalculation.print;
    58 
    59 
    60 (* proof data kind 'Isar/calculation' *)
    61 
    62 structure LocalCalculationArgs =
    63 struct
    64   val name = "Isar/calculation";
    65   type T = (thm NetRules.T * thm list) * (thm list * int) option;
    66 
    67   fun init thy = (GlobalCalculation.get thy, NONE);
    68   fun print ctxt (rs, _) = print_rules ProofContext.pretty_thm ctxt rs;
    69 end;
    70 
    71 structure LocalCalculation = ProofDataFun(LocalCalculationArgs);
    72 val get_local_rules = #1 o LocalCalculation.get o Proof.context_of;
    73 val print_local_rules = LocalCalculation.print;
    74 
    75 
    76 (* access calculation *)
    77 
    78 fun get_calculation state =
    79   (case #2 (LocalCalculation.get (Proof.context_of state)) of
    80     NONE => NONE
    81   | SOME (thms, lev) => if lev = Proof.level state then SOME thms else NONE);
    82 
    83 fun put_calculation thms state =
    84   Proof.map_context
    85     (LocalCalculation.put (get_local_rules state, SOME (thms, Proof.level state))) state;
    86 
    87 fun reset_calculation state =
    88   Proof.map_context (LocalCalculation.put (get_local_rules state, NONE)) state;
    89 
    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 
   133 
   134 (** proof commands **)
   135 
   136 fun assert_sane final =
   137   if final then Proof.assert_forward else Proof.assert_forward_or_chain;
   138 
   139 
   140 (* maintain calculation register *)
   141 
   142 val calculationN = "calculation";
   143 
   144 fun maintain_calculation false calc state =
   145       state
   146       |> put_calculation calc
   147       |> Proof.put_thms (calculationN, calc)
   148   | maintain_calculation true calc state =
   149       state
   150       |> reset_calculation
   151       |> Proof.reset_thms calculationN
   152       |> Proof.simple_note_thms "" calc
   153       |> Proof.chain;
   154 
   155 
   156 (* 'also' and 'finally' *)
   157 
   158 fun err_if state b msg = if b then raise Proof.STATE (msg, state) else ();
   159 
   160 fun calculate final opt_rules print state =
   161   let
   162     val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of;
   163     val eq_prop = op aconv o pairself (Pattern.eta_contract o strip_assums_concl);
   164     fun projection ths th = Library.exists (Library.curry eq_prop th) ths;
   165 
   166     fun combine ths =
   167       (case opt_rules of SOME rules => rules
   168       | NONE =>
   169           (case ths of [] => NetRules.rules (#1 (get_local_rules state))
   170           | th :: _ => NetRules.retrieve (#1 (get_local_rules state)) (strip_assums_concl th)))
   171       |> Seq.of_list |> Seq.map (Method.multi_resolve ths) |> Seq.flat
   172       |> Seq.filter (not o projection ths);
   173 
   174     val facts = Proof.the_facts (assert_sane final state);
   175     val (initial, calculations) =
   176       (case get_calculation state of
   177         NONE => (true, Seq.single facts)
   178       | SOME calc => (false, Seq.map single (combine (calc @ facts))));
   179   in
   180     err_if state (initial andalso final) "No calculation yet";
   181     err_if state (initial andalso isSome opt_rules) "Initial calculation -- no rules to be given";
   182     calculations |> Seq.map (fn calc => (print (Proof.context_of state) calc;
   183         state |> maintain_calculation final calc))
   184   end;
   185 
   186 fun also print = calculate false print;
   187 fun finally print = calculate true print;
   188 
   189 
   190 (* 'moreover' and 'ultimately' *)
   191 
   192 fun collect final print state =
   193   let
   194     val facts = Proof.the_facts (assert_sane final state);
   195     val (initial, thms) =
   196       (case get_calculation state of
   197         NONE => (true, [])
   198       | SOME thms => (false, thms));
   199     val calc = thms @ facts;
   200   in
   201     err_if state (initial andalso final) "No calculation yet";
   202     print (Proof.context_of state) calc;
   203     state |> maintain_calculation final calc
   204   end;
   205 
   206 fun moreover print = collect false print;
   207 fun ultimately print = collect true print;
   208 
   209 
   210 
   211 (** theory setup **)
   212 
   213 val setup =
   214  [GlobalCalculation.init, LocalCalculation.init,
   215   Attrib.add_attributes
   216    [("trans", trans_attr, "declaration of transitivity rule"),
   217     ("sym", sym_attr, "declaration of symmetry rule"),
   218     ("symmetric", (Attrib.no_args symmetric_global, Attrib.no_args symmetric_local),
   219       "resolution with symmetry rule")],
   220   #1 o PureThy.add_thms
   221    [(("", transitive_thm), [trans_add_global]),
   222     (("", symmetric_thm), [sym_add_global])]];
   223 
   224 end;