src/Pure/Isar/calculation.ML
author wenzelm
Wed Mar 15 18:25:42 2000 +0100 (2000-03-15)
changeset 8461 2693a3a9fcc1
parent 8300 4c3f83414de3
child 8562 ce0e2b8e8844
permissions -rw-r--r--
tuned comment;
     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 also: thm list option -> (thm list -> unit) -> Proof.state -> Proof.state Seq.seq
    17   val finally: thm list option -> (thm list -> unit) -> Proof.state -> Proof.state Seq.seq
    18   val setup: (theory -> theory) list
    19 end;
    20 
    21 structure Calculation: CALCULATION =
    22 struct
    23 
    24 (** global and local calculation data **)
    25 
    26 (* theory data kind 'Isar/calculation' *)
    27 
    28 fun print_rules rs = Pretty.writeln (Pretty.big_list "calculation rules:"
    29   (map Display.pretty_thm (NetRules.rules rs)));
    30 
    31 structure GlobalCalculationArgs =
    32 struct
    33   val name = "Isar/calculation";
    34   type T = thm NetRules.T
    35 
    36   val empty = NetRules.init_elim;
    37   val copy = I;
    38   val prep_ext = I;
    39   val merge = NetRules.merge;
    40   fun print _ = print_rules;
    41 end;
    42 
    43 structure GlobalCalculation = TheoryDataFun(GlobalCalculationArgs);
    44 val print_global_rules = GlobalCalculation.print;
    45 
    46 
    47 (* proof data kind 'Isar/calculation' *)
    48 
    49 structure LocalCalculationArgs =
    50 struct
    51   val name = "Isar/calculation";
    52   type T = thm NetRules.T * (thm list * int) option;
    53 
    54   fun init thy = (GlobalCalculation.get thy, None);
    55   fun print _ (rs, _) = print_rules rs;
    56 end;
    57 
    58 structure LocalCalculation = ProofDataFun(LocalCalculationArgs);
    59 val get_local_rules = #1 o LocalCalculation.get_st;
    60 val print_local_rules = LocalCalculation.print;
    61 
    62 
    63 (* access calculation *)
    64 
    65 fun get_calculation state =
    66   (case #2 (LocalCalculation.get_st state) of
    67     None => None
    68   | Some (thms, lev) => if lev = Proof.level state then Some thms else None);
    69 
    70 fun put_calculation thms state =
    71   LocalCalculation.put_st (get_local_rules state, Some (thms, Proof.level state)) state;
    72 
    73 fun reset_calculation state =
    74   LocalCalculation.put_st (get_local_rules state, None) state;
    75 
    76 
    77 
    78 (** attributes **)
    79 
    80 (* trans add/del *)
    81 
    82 fun mk_att f g (x, thm) = (f (g thm) x, thm);
    83 
    84 val trans_add_global = mk_att GlobalCalculation.map NetRules.insert;
    85 val trans_del_global = mk_att GlobalCalculation.map NetRules.delete;
    86 val trans_add_local = mk_att LocalCalculation.map (Library.apfst o NetRules.insert);
    87 val trans_del_local = mk_att LocalCalculation.map (Library.apfst o NetRules.delete);
    88 
    89 
    90 (* concrete syntax *)
    91 
    92 val transN = "trans";
    93 val addN = "add";
    94 val delN = "del";
    95 
    96 fun trans_att add del =
    97   Attrib.syntax (Scan.lift (Args.$$$ addN >> K add || Args.$$$ delN >> K del || Scan.succeed add));
    98 
    99 val trans_attr =
   100   (trans_att trans_add_global trans_del_global, trans_att trans_add_local trans_del_local);
   101 
   102 
   103 
   104 (** proof commands **)
   105 
   106 val calculationN = "calculation";
   107 
   108 fun calculate final opt_rules print state =
   109   let
   110     fun err_if b msg = if b then raise Proof.STATE (msg, state) else ();
   111     val facts = Proof.the_facts state;
   112 
   113     val eq_prop = op aconv o pairself (#prop o Thm.rep_thm);
   114     fun differ thms thms' = not (Library.equal_lists eq_prop (thms, thms'));
   115 
   116     fun combine thms =
   117       let
   118         val ths = thms @ facts;
   119         val rs = NetRules.inserts (if_none opt_rules []) (get_local_rules state);
   120         val rules =
   121           (case ths of [] => NetRules.rules rs
   122           | th :: _ => NetRules.may_unify rs (Logic.strip_assums_concl (#prop (Thm.rep_thm th))));
   123         val ruleq = Seq.of_list rules;
   124       in Seq.map Library.single (Seq.flat (Seq.map (Method.multi_resolve ths) ruleq)) end;
   125 
   126     val (initial, calculations) =
   127       (case get_calculation state of
   128         None => (true, Seq.single facts)
   129       | Some thms => (false, Seq.filter (differ thms) (combine thms)))
   130   in
   131     err_if (initial andalso final) "No calculation yet";
   132     err_if (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given";
   133     calculations |> Seq.map (fn calc =>
   134       (print calc;
   135         (if final then
   136           state
   137           |> reset_calculation
   138           |> Proof.reset_thms calculationN
   139           |> Proof.simple_have_thms "" calc
   140           |> Proof.chain
   141         else
   142           state
   143           |> put_calculation calc
   144           |> Proof.simple_have_thms calculationN calc
   145           |> Proof.reset_facts)))
   146   end;
   147 
   148 fun also print = calculate false print;
   149 fun finally print = calculate true print;
   150 
   151 
   152 
   153 (** theory setup **)
   154 
   155 val setup = [GlobalCalculation.init, LocalCalculation.init,
   156   Attrib.add_attributes [(transN, trans_attr, "declare transitivity rule")]];
   157 
   158 
   159 end;