added 'sym' and 'symmetric' atts;
authorwenzelm
Wed Dec 05 03:14:22 2001 +0100 (2001-12-05)
changeset 12379c74d160ff0c5
parent 12378 86c58273f8c0
child 12380 3402d300f5ef
added 'sym' and 'symmetric' atts;
src/Pure/Isar/calculation.ML
     1.1 --- a/src/Pure/Isar/calculation.ML	Wed Dec 05 03:13:57 2001 +0100
     1.2 +++ b/src/Pure/Isar/calculation.ML	Wed Dec 05 03:14:22 2001 +0100
     1.3 @@ -14,6 +14,12 @@
     1.4    val trans_del_global: theory attribute
     1.5    val trans_add_local: Proof.context attribute
     1.6    val trans_del_local: Proof.context attribute
     1.7 +  val sym_add_global: theory attribute
     1.8 +  val sym_del_global: theory attribute
     1.9 +  val sym_add_local: Proof.context attribute
    1.10 +  val sym_del_local: Proof.context attribute
    1.11 +  val symmetric_global: theory attribute
    1.12 +  val symmetric_local: Proof.context attribute
    1.13    val also: thm list option -> (Proof.context -> thm list -> unit)
    1.14      -> Proof.state -> Proof.state Seq.seq
    1.15    val finally: thm list option -> (Proof.context -> thm list -> unit)
    1.16 @@ -30,18 +36,21 @@
    1.17  
    1.18  (* theory data kind 'Isar/calculation' *)
    1.19  
    1.20 -fun print_rules prt x rs =
    1.21 -  Pretty.writeln (Pretty.big_list "transitivity rules:" (map (prt x) (NetRules.rules rs)));
    1.22 +fun print_rules prt x (trans, sym) =
    1.23 +  [Pretty.big_list "transitivity rules:" (map (prt x) (NetRules.rules trans)),
    1.24 +    Pretty.big_list "symmetry rules:" (map (prt x) sym)]
    1.25 +  |> Pretty.chunks |> Pretty.writeln;
    1.26  
    1.27  structure GlobalCalculationArgs =
    1.28  struct
    1.29    val name = "Isar/calculation";
    1.30 -  type T = thm NetRules.T
    1.31 +  type T = thm NetRules.T * thm list
    1.32  
    1.33 -  val empty = NetRules.elim;
    1.34 +  val empty = (NetRules.elim, []);
    1.35    val copy = I;
    1.36    val prep_ext = I;
    1.37 -  val merge = NetRules.merge;
    1.38 +  fun merge ((trans1, sym1), (trans2, sym2)) =
    1.39 +    (NetRules.merge (trans1, trans2), Drule.merge_rules (sym1, sym2));
    1.40    val print = print_rules Display.pretty_thm_sg;
    1.41  end;
    1.42  
    1.43 @@ -54,7 +63,7 @@
    1.44  structure LocalCalculationArgs =
    1.45  struct
    1.46    val name = "Isar/calculation";
    1.47 -  type T = thm NetRules.T * (thm list * int) option;
    1.48 +  type T = (thm NetRules.T * thm list) * (thm list * int) option;
    1.49  
    1.50    fun init thy = (GlobalCalculation.get thy, None);
    1.51    fun print ctxt (rs, _) = print_rules ProofContext.pretty_thm ctxt rs;
    1.52 @@ -82,14 +91,32 @@
    1.53  
    1.54  (** attributes **)
    1.55  
    1.56 -(* trans add/del *)
    1.57 +(* add/del rules *)
    1.58 +
    1.59 +fun global_att f (x, thm) = (GlobalCalculation.map (f thm) x, thm);
    1.60 +fun local_att f (x, thm) = (LocalCalculation.map (apfst (f thm)) x, thm);
    1.61  
    1.62 -fun mk_att f g (x, thm) = (f (g thm) x, thm);
    1.63 +val trans_add_global = global_att (apfst o NetRules.insert);
    1.64 +val trans_del_global = global_att (apfst o NetRules.delete);
    1.65 +val trans_add_local = local_att (apfst o NetRules.insert);
    1.66 +val trans_del_local = local_att (apfst o NetRules.delete);
    1.67  
    1.68 -val trans_add_global = mk_att GlobalCalculation.map NetRules.insert;
    1.69 -val trans_del_global = mk_att GlobalCalculation.map NetRules.delete;
    1.70 -val trans_add_local = mk_att LocalCalculation.map (Library.apfst o NetRules.insert);
    1.71 -val trans_del_local = mk_att LocalCalculation.map (Library.apfst o NetRules.delete);
    1.72 +val sym_add_global = global_att (apsnd o Drule.add_rule) o ContextRules.elim_query_global None;
    1.73 +val sym_del_global = global_att (apsnd o Drule.del_rule);
    1.74 +val sym_add_local = local_att (apsnd o Drule.add_rule) o ContextRules.elim_query_local None;
    1.75 +val sym_del_local = local_att (apsnd o Drule.del_rule);
    1.76 +
    1.77 +
    1.78 +(* symmetry *)
    1.79 +
    1.80 +fun gen_symmetric get_sym = Drule.rule_attribute (fn x => fn th =>
    1.81 +  (case Seq.chop (2, Method.multi_resolves [th] (get_sym x)) of
    1.82 +    ([th'], _) => th'
    1.83 +  | ([], _) => raise THM ("symmetric: no unifiers", 1, [th])
    1.84 +  | _ => raise THM ("symmetric: multiple unifiers", 1, [th])));
    1.85 +
    1.86 +val symmetric_global = gen_symmetric (#2 o GlobalCalculation.get);
    1.87 +val symmetric_local = gen_symmetric (#2 o #1 o LocalCalculation.get);
    1.88  
    1.89  
    1.90  (* concrete syntax *)
    1.91 @@ -98,6 +125,10 @@
    1.92   (Attrib.add_del_args trans_add_global trans_del_global,
    1.93    Attrib.add_del_args trans_add_local trans_del_local);
    1.94  
    1.95 +val sym_attr =
    1.96 + (Attrib.add_del_args sym_add_global sym_del_global,
    1.97 +  Attrib.add_del_args sym_add_local sym_del_local);
    1.98 +
    1.99  
   1.100  
   1.101  (** proof commands **)
   1.102 @@ -132,8 +163,8 @@
   1.103      fun combine ths =
   1.104        (case opt_rules of Some rules => rules
   1.105        | None =>
   1.106 -          (case ths of [] => NetRules.rules (get_local_rules state)
   1.107 -          | th :: _ => NetRules.retrieve (get_local_rules state) (strip_assums_concl th)))
   1.108 +          (case ths of [] => NetRules.rules (#1 (get_local_rules state))
   1.109 +          | th :: _ => NetRules.retrieve (#1 (get_local_rules state)) (strip_assums_concl th)))
   1.110        |> Seq.of_list |> Seq.map (Method.multi_resolve ths) |> Seq.flat
   1.111        |> Seq.filter (not o projection ths);
   1.112  
   1.113 @@ -176,9 +207,15 @@
   1.114  
   1.115  (** theory setup **)
   1.116  
   1.117 -val setup = [GlobalCalculation.init, LocalCalculation.init,
   1.118 -  Attrib.add_attributes [("trans", trans_attr, "declaration of transitivity rule")],
   1.119 -  #1 o PureThy.add_thms [(("", transitive_thm), [trans_add_global])]];
   1.120 -
   1.121 +val setup =
   1.122 + [GlobalCalculation.init, LocalCalculation.init,
   1.123 +  Attrib.add_attributes
   1.124 +   [("trans", trans_attr, "declaration of transitivity rule"),
   1.125 +    ("sym", sym_attr, "declaration of symmetry rule"),
   1.126 +    ("symmetric", (Attrib.no_args symmetric_global, Attrib.no_args symmetric_local),
   1.127 +      "resolution with symmetry rule")],
   1.128 +  #1 o PureThy.add_thms
   1.129 +   [(("", transitive_thm), [trans_add_global]),
   1.130 +    (("", symmetric_thm), [sym_add_global])]];
   1.131  
   1.132  end;