src/Pure/Isar/calculation.ML
changeset 8300 4c3f83414de3
parent 8150 7021549ef32d
child 8461 2693a3a9fcc1
     1.1 --- a/src/Pure/Isar/calculation.ML	Sun Feb 27 15:13:44 2000 +0100
     1.2 +++ b/src/Pure/Isar/calculation.ML	Sun Feb 27 15:15:52 2000 +0100
     1.3 @@ -21,24 +21,22 @@
     1.4  structure Calculation: CALCULATION =
     1.5  struct
     1.6  
     1.7 -
     1.8  (** global and local calculation data **)
     1.9  
    1.10 -fun print_rules ths =
    1.11 -  Pretty.writeln (Pretty.big_list "calculation rules:" (map Display.pretty_thm ths));
    1.12 +(* theory data kind 'Isar/calculation' *)
    1.13  
    1.14 -
    1.15 -(* theory data kind 'Isar/calculation' *)
    1.16 +fun print_rules rs = Pretty.writeln (Pretty.big_list "calculation rules:"
    1.17 +  (map Display.pretty_thm (NetRules.rules rs)));
    1.18  
    1.19  structure GlobalCalculationArgs =
    1.20  struct
    1.21    val name = "Isar/calculation";
    1.22 -  type T = thm list;
    1.23 +  type T = thm NetRules.T
    1.24  
    1.25 -  val empty = [];
    1.26 +  val empty = NetRules.init_elim;
    1.27    val copy = I;
    1.28    val prep_ext = I;
    1.29 -  fun merge (ths1, ths2) = Library.generic_merge Thm.eq_thm I I ths1 ths2;
    1.30 +  val merge = NetRules.merge;
    1.31    fun print _ = print_rules;
    1.32  end;
    1.33  
    1.34 @@ -51,10 +49,10 @@
    1.35  structure LocalCalculationArgs =
    1.36  struct
    1.37    val name = "Isar/calculation";
    1.38 -  type T = thm list * (thm list * int) option;
    1.39 +  type T = thm NetRules.T * (thm list * int) option;
    1.40  
    1.41    fun init thy = (GlobalCalculation.get thy, None);
    1.42 -  fun print _ (ths, _) = print_rules ths;
    1.43 +  fun print _ (rs, _) = print_rules rs;
    1.44  end;
    1.45  
    1.46  structure LocalCalculation = ProofDataFun(LocalCalculationArgs);
    1.47 @@ -81,21 +79,12 @@
    1.48  
    1.49  (* trans add/del *)
    1.50  
    1.51 -local
    1.52 -
    1.53 -fun add_trans thm rules = Library.gen_ins Thm.eq_thm (thm, rules);
    1.54 -fun del_trans thm rules = Library.gen_rem Thm.eq_thm (rules, thm);
    1.55 -
    1.56  fun mk_att f g (x, thm) = (f (g thm) x, thm);
    1.57  
    1.58 -in
    1.59 -
    1.60 -val trans_add_global = mk_att GlobalCalculation.map add_trans;
    1.61 -val trans_del_global = mk_att GlobalCalculation.map del_trans;
    1.62 -val trans_add_local = mk_att LocalCalculation.map (Library.apfst o add_trans);
    1.63 -val trans_del_local = mk_att LocalCalculation.map (Library.apfst o del_trans);
    1.64 -
    1.65 -end;
    1.66 +val trans_add_global = mk_att GlobalCalculation.map NetRules.insert;
    1.67 +val trans_del_global = mk_att GlobalCalculation.map NetRules.delete;
    1.68 +val trans_add_local = mk_att LocalCalculation.map (Library.apfst o NetRules.insert);
    1.69 +val trans_del_local = mk_att LocalCalculation.map (Library.apfst o NetRules.delete);
    1.70  
    1.71  
    1.72  (* concrete syntax *)
    1.73 @@ -120,12 +109,19 @@
    1.74    let
    1.75      fun err_if b msg = if b then raise Proof.STATE (msg, state) else ();
    1.76      val facts = Proof.the_facts state;
    1.77 -    val rules = Seq.of_list (if_none opt_rules [] @ get_local_rules state);
    1.78  
    1.79      val eq_prop = op aconv o pairself (#prop o Thm.rep_thm);
    1.80      fun differ thms thms' = not (Library.equal_lists eq_prop (thms, thms'));
    1.81 +
    1.82      fun combine thms =
    1.83 -      Seq.map Library.single (Seq.flat (Seq.map (Method.multi_resolve (thms @ facts)) rules));
    1.84 +      let
    1.85 +        val ths = thms @ facts;
    1.86 +        val rs = NetRules.inserts (if_none opt_rules []) (get_local_rules state);
    1.87 +        val rules =
    1.88 +          (case ths of [] => NetRules.rules rs
    1.89 +          | th :: _ => NetRules.may_unify rs (Logic.strip_assums_concl (#prop (Thm.rep_thm th))));
    1.90 +        val ruleq = Seq.of_list rules;
    1.91 +      in Seq.map Library.single (Seq.flat (Seq.map (Method.multi_resolve ths) ruleq)) end;
    1.92  
    1.93      val (initial, calculations) =
    1.94        (case get_calculation state of