src/Provers/classical.ML
changeset 18688 abf0f018b5ec
parent 18643 89a7978f90e1
child 18691 a2dc15d9d6c8
     1.1 --- a/src/Provers/classical.ML	Sat Jan 14 17:20:51 2006 +0100
     1.2 +++ b/src/Provers/classical.ML	Sat Jan 14 22:25:34 2006 +0100
     1.3 @@ -143,20 +143,13 @@
     1.4    val print_local_claset: Proof.context -> unit
     1.5    val get_local_claset: Proof.context -> claset
     1.6    val put_local_claset: claset -> Proof.context -> Proof.context
     1.7 -  val safe_dest_global: theory attribute
     1.8 -  val safe_elim_global: theory attribute
     1.9 -  val safe_intro_global: theory attribute
    1.10 -  val haz_dest_global: theory attribute
    1.11 -  val haz_elim_global: theory attribute
    1.12 -  val haz_intro_global: theory attribute
    1.13 -  val rule_del_global: theory attribute
    1.14 -  val safe_dest_local: Proof.context attribute
    1.15 -  val safe_elim_local: Proof.context attribute
    1.16 -  val safe_intro_local: Proof.context attribute
    1.17 -  val haz_dest_local: Proof.context attribute
    1.18 -  val haz_elim_local: Proof.context attribute
    1.19 -  val haz_intro_local: Proof.context attribute
    1.20 -  val rule_del_local: Proof.context attribute
    1.21 +  val safe_dest: Context.generic attribute
    1.22 +  val safe_elim: Context.generic attribute
    1.23 +  val safe_intro: Context.generic attribute
    1.24 +  val haz_dest: Context.generic attribute
    1.25 +  val haz_elim: Context.generic attribute
    1.26 +  val haz_intro: Context.generic attribute
    1.27 +  val rule_del: Context.generic attribute
    1.28    val cla_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
    1.29    val cla_meth: (claset -> tactic) -> thm list -> Proof.context -> Proof.method
    1.30    val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
    1.31 @@ -959,24 +952,17 @@
    1.32  
    1.33  (* attributes *)
    1.34  
    1.35 -fun change_global_cs f (thy, th) = (change_claset_of thy (fn cs => f (cs, [th])); (thy, th));
    1.36 -fun change_local_cs f (ctxt, th) = (LocalClaset.map (fn cs => f (cs, [th])) ctxt, th);
    1.37 +fun attrib f = Attrib.declaration (fn th =>
    1.38 +   fn Context.Theory thy => (change_claset_of thy (fn cs => f (cs, [th])); Context.Theory thy)
    1.39 +    | Context.Proof ctxt => Context.Proof (LocalClaset.map (fn cs => f (cs, [th])) ctxt));
    1.40  
    1.41 -val safe_dest_global = change_global_cs (op addSDs);
    1.42 -val safe_elim_global = change_global_cs (op addSEs);
    1.43 -val safe_intro_global = change_global_cs (op addSIs);
    1.44 -val haz_dest_global = change_global_cs (op addDs);
    1.45 -val haz_elim_global = change_global_cs (op addEs);
    1.46 -val haz_intro_global = change_global_cs (op addIs);
    1.47 -val rule_del_global = change_global_cs (op delrules) o Attrib.theory ContextRules.rule_del;
    1.48 -
    1.49 -val safe_dest_local = change_local_cs (op addSDs);
    1.50 -val safe_elim_local = change_local_cs (op addSEs);
    1.51 -val safe_intro_local = change_local_cs (op addSIs);
    1.52 -val haz_dest_local = change_local_cs (op addDs);
    1.53 -val haz_elim_local = change_local_cs (op addEs);
    1.54 -val haz_intro_local = change_local_cs (op addIs);
    1.55 -val rule_del_local = change_local_cs (op delrules) o Attrib.context ContextRules.rule_del;
    1.56 +val safe_dest = attrib (op addSDs);
    1.57 +val safe_elim = attrib (op addSEs);
    1.58 +val safe_intro = attrib (op addSIs);
    1.59 +val haz_dest = attrib (op addDs);
    1.60 +val haz_elim = attrib (op addEs);
    1.61 +val haz_intro = attrib (op addIs);
    1.62 +val rule_del = attrib (op delrules) o ContextRules.rule_del;
    1.63  
    1.64  
    1.65  (* tactics referring to the implicit claset *)
    1.66 @@ -1018,19 +1004,13 @@
    1.67  
    1.68  val setup_attrs = Attrib.add_attributes
    1.69   [("swapped", (swapped, swapped), "classical swap of introduction rule"),
    1.70 -  (destN,
    1.71 -   (add_rule (Attrib.theory o ContextRules.dest_query) haz_dest_global safe_dest_global,
    1.72 -    add_rule (Attrib.context o ContextRules.dest_query) haz_dest_local safe_dest_local),
    1.73 -    "declaration of destruction rule"),
    1.74 -  (elimN,
    1.75 -   (add_rule (Attrib.theory o ContextRules.elim_query) haz_elim_global safe_elim_global,
    1.76 -    add_rule (Attrib.context o ContextRules.elim_query) haz_elim_local safe_elim_local),
    1.77 -    "declaration of elimination rule"),
    1.78 -  (introN,
    1.79 -   (add_rule (Attrib.theory o ContextRules.intro_query) haz_intro_global safe_intro_global,
    1.80 -    add_rule (Attrib.context o ContextRules.intro_query) haz_intro_local safe_intro_local),
    1.81 -    "declaration of introduction rule"),
    1.82 -  (ruleN, (del_rule rule_del_global, del_rule rule_del_local),
    1.83 +  (destN, Attrib.common (add_rule ContextRules.dest_query haz_dest safe_dest),
    1.84 +    "declaration of Classical destruction rule"),
    1.85 +  (elimN, Attrib.common (add_rule ContextRules.elim_query haz_elim safe_elim),
    1.86 +    "declaration of Classical elimination rule"),
    1.87 +  (introN, Attrib.common (add_rule ContextRules.intro_query haz_intro safe_intro),
    1.88 +    "declaration of Classical introduction rule"),
    1.89 +  (ruleN, Attrib.common (del_rule rule_del),
    1.90      "remove declaration of intro/elim/dest rule")];
    1.91  
    1.92  
    1.93 @@ -1078,13 +1058,13 @@
    1.94  (* automatic methods *)
    1.95  
    1.96  val cla_modifiers =
    1.97 - [Args.$$$ destN -- Args.bang_colon >> K ((I, safe_dest_local): Method.modifier),
    1.98 -  Args.$$$ destN -- Args.colon >> K (I, haz_dest_local),
    1.99 -  Args.$$$ elimN -- Args.bang_colon >> K (I, safe_elim_local),
   1.100 -  Args.$$$ elimN -- Args.colon >> K (I, haz_elim_local),
   1.101 -  Args.$$$ introN -- Args.bang_colon >> K (I, safe_intro_local),
   1.102 -  Args.$$$ introN -- Args.colon >> K (I, haz_intro_local),
   1.103 -  Args.del -- Args.colon >> K (I, rule_del_local)];
   1.104 + [Args.$$$ destN -- Args.bang_colon >> K ((I, Attrib.context safe_dest): Method.modifier),
   1.105 +  Args.$$$ destN -- Args.colon >> K (I, Attrib.context haz_dest),
   1.106 +  Args.$$$ elimN -- Args.bang_colon >> K (I, Attrib.context safe_elim),
   1.107 +  Args.$$$ elimN -- Args.colon >> K (I, Attrib.context haz_elim),
   1.108 +  Args.$$$ introN -- Args.bang_colon >> K (I, Attrib.context safe_intro),
   1.109 +  Args.$$$ introN -- Args.colon >> K (I, Attrib.context haz_intro),
   1.110 +  Args.del -- Args.colon >> K (I, Attrib.context rule_del)];
   1.111  
   1.112  fun cla_meth tac prems ctxt = Method.METHOD (fn facts =>
   1.113    ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (local_claset_of ctxt));