Support for calculational proofs.
authorwenzelm
Fri Jun 04 19:55:41 1999 +0200 (1999-06-04)
changeset 67782f66eea8a025
parent 6777 175ff298ac0e
child 6779 2912aff958bd
Support for calculational proofs.
src/Pure/Isar/calculation.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Isar/calculation.ML	Fri Jun 04 19:55:41 1999 +0200
     1.3 @@ -0,0 +1,153 @@
     1.4 +(*  Title:      Pure/Isar/calculation.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Markus Wenzel, TU Muenchen
     1.7 +
     1.8 +Support for calculational proofs.
     1.9 +*)
    1.10 +
    1.11 +signature CALCULATION =
    1.12 +sig
    1.13 +  val print_global_rules: theory -> unit
    1.14 +  val print_local_rules: Proof.context -> unit
    1.15 +  val trans_add_global: theory attribute
    1.16 +  val trans_del_global: theory attribute
    1.17 +  val trans_add_local: Proof.context attribute
    1.18 +  val trans_del_local: Proof.context attribute
    1.19 +  val also: (thm -> unit) -> Proof.state -> Proof.state Seq.seq
    1.20 +  val finally: (thm -> unit) -> Proof.state -> Proof.state Seq.seq
    1.21 +  val setup: (theory -> theory) list
    1.22 +end;
    1.23 +
    1.24 +structure Calculation: CALCULATION =
    1.25 +struct
    1.26 +
    1.27 +
    1.28 +(** global and local calculation data **)
    1.29 +
    1.30 +fun print_rules ths =
    1.31 +  Pretty.writeln (Pretty.big_list "calculation rules:" (map Display.pretty_thm ths));
    1.32 +
    1.33 +
    1.34 +(* theory data kind 'Isar/calculation' *)
    1.35 +
    1.36 +structure GlobalCalculationArgs =
    1.37 +struct
    1.38 +  val name = "Isar/calculation";
    1.39 +  type T = thm list;
    1.40 +
    1.41 +  val empty = [];
    1.42 +  val copy = I;
    1.43 +  val prep_ext = I;
    1.44 +  fun merge (ths1, ths2) = Library.generic_merge Thm.eq_thm I I ths1 ths2;
    1.45 +  fun print _ = print_rules;
    1.46 +end;
    1.47 +
    1.48 +structure GlobalCalculation = TheoryDataFun(GlobalCalculationArgs);
    1.49 +val print_global_rules = GlobalCalculation.print;
    1.50 +
    1.51 +
    1.52 +(* proof data kind 'Isar/calculation' *)
    1.53 +
    1.54 +structure LocalCalculationArgs =
    1.55 +struct
    1.56 +  val name = "Isar/calculation";
    1.57 +  type T = thm list * (thm * int) option;
    1.58 +
    1.59 +  fun init thy = (GlobalCalculation.get thy, None);
    1.60 +  fun print _ (ths, _) = print_rules ths;
    1.61 +end;
    1.62 +
    1.63 +structure LocalCalculation = ProofDataFun(LocalCalculationArgs);
    1.64 +val get_local_rules = #1 o LocalCalculation.get o Proof.context_of;
    1.65 +val print_local_rules = LocalCalculation.print;
    1.66 +
    1.67 +
    1.68 +(* access calculation *)
    1.69 +
    1.70 +fun get_calculation state =
    1.71 +  (case #2 (LocalCalculation.get (Proof.context_of state)) of
    1.72 +    None => None
    1.73 +  | Some (thm, lev) => if lev = Proof.level state then Some thm else None);
    1.74 +
    1.75 +fun put_calculation thm state =
    1.76 +  LocalCalculation.put_st (get_local_rules state, Some (thm, Proof.level state)) state;
    1.77 +
    1.78 +
    1.79 +
    1.80 +(** attributes **)
    1.81 +
    1.82 +(* trans add/del *)
    1.83 +
    1.84 +local
    1.85 +
    1.86 +fun map_rules_global f thy = GlobalCalculation.put (f (GlobalCalculation.get thy)) thy;
    1.87 +fun map_rules_local f ctxt = LocalCalculation.put (f (LocalCalculation.get ctxt)) ctxt;
    1.88 +
    1.89 +fun add_trans thm rules = Library.gen_ins Thm.eq_thm (thm, rules);
    1.90 +fun del_trans thm rules = Library.gen_rem Thm.eq_thm (rules, thm);
    1.91 +
    1.92 +fun mk_att f g (x, thm) = (f (g thm) x, thm);
    1.93 +
    1.94 +in
    1.95 +
    1.96 +val trans_add_global = mk_att map_rules_global add_trans;
    1.97 +val trans_del_global = mk_att map_rules_global del_trans;
    1.98 +val trans_add_local = mk_att map_rules_local (Library.apfst o add_trans);
    1.99 +val trans_del_local = mk_att map_rules_local (Library.apfst o del_trans);
   1.100 +
   1.101 +end;
   1.102 +
   1.103 +
   1.104 +(* concrete syntax *)
   1.105 +
   1.106 +val transN = "trans";
   1.107 +val addN = "add";
   1.108 +val delN = "del";
   1.109 +
   1.110 +fun trans_att add del =
   1.111 +  Attrib.syntax (Scan.lift (Args.$$$ addN >> K add || Args.$$$ delN >> K del || Scan.succeed add));
   1.112 +
   1.113 +val trans_attr =
   1.114 +  (trans_att trans_add_global trans_del_global, trans_att trans_add_local trans_del_local);
   1.115 +
   1.116 +
   1.117 +(** proof commands **)
   1.118 +
   1.119 +val calculationN = "calculation";
   1.120 +
   1.121 +fun calculate final prt state =
   1.122 +  let
   1.123 +    val fact = Proof.the_fact state;
   1.124 +    val dddot = ObjectLogic.dest_main_statement (#prop (Thm.rep_thm fact)) handle TERM _ =>
   1.125 +      raise Proof.STATE ("Unable to bind '...' pattern from current fact", state);
   1.126 +
   1.127 +    val name = if final then "" else calculationN;
   1.128 +    fun have_thm thm = Proof.have_thmss name [] [([thm], [])];
   1.129 +
   1.130 +    val rules = Seq.of_list (get_local_rules state);
   1.131 +    val calculations =
   1.132 +      (case get_calculation state of
   1.133 +        None => Seq.single fact
   1.134 +      | Some thm => Seq.flat (Seq.map (Method.multi_resolve [thm, fact]) rules));
   1.135 +  in
   1.136 +    calculations
   1.137 +    |> Seq.map (fn calc =>
   1.138 +      (prt calc;
   1.139 +        state
   1.140 +        |> Proof.bind_i [(Syntax.dddot_indexname, dddot)]
   1.141 +        |> have_thm calc
   1.142 +        |> (if final then I else Proof.reset_facts)))
   1.143 +  end;
   1.144 +
   1.145 +val also = calculate false;
   1.146 +val finally = calculate true;
   1.147 +
   1.148 +
   1.149 +
   1.150 +(** theory setup **)
   1.151 +
   1.152 +val setup = [GlobalCalculation.init, LocalCalculation.init,
   1.153 +  Attrib.add_attributes [(transN, trans_attr, "transitivity rule")]];
   1.154 +
   1.155 +
   1.156 +end;