src/Provers/classical.ML
changeset 18691 a2dc15d9d6c8
parent 18688 abf0f018b5ec
child 18708 4b3dadb4fe33
     1.1 --- a/src/Provers/classical.ML	Sun Jan 15 19:58:53 2006 +0100
     1.2 +++ b/src/Provers/classical.ML	Sun Jan 15 19:58:54 2006 +0100
     1.3 @@ -143,12 +143,12 @@
     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: Context.generic attribute
     1.8 -  val safe_elim: Context.generic attribute
     1.9 -  val safe_intro: Context.generic attribute
    1.10 -  val haz_dest: Context.generic attribute
    1.11 -  val haz_elim: Context.generic attribute
    1.12 -  val haz_intro: Context.generic attribute
    1.13 +  val safe_dest: int option -> Context.generic attribute
    1.14 +  val safe_elim: int option -> Context.generic attribute
    1.15 +  val safe_intro: int option -> Context.generic attribute
    1.16 +  val haz_dest: int option -> Context.generic attribute
    1.17 +  val haz_elim: int option -> Context.generic attribute
    1.18 +  val haz_intro: int option -> Context.generic attribute
    1.19    val rule_del: Context.generic attribute
    1.20    val cla_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
    1.21    val cla_meth: (claset -> tactic) -> thm list -> Proof.context -> Proof.method
    1.22 @@ -197,7 +197,6 @@
    1.23  fun classical_rule rule =
    1.24    if is_elim rule then
    1.25      let
    1.26 -      val ntags = Thm.get_name_tags rule;
    1.27        val rule' = rule RS classical;
    1.28        val concl' = Thm.concl_of rule';
    1.29        fun redundant_hyp goal =
    1.30 @@ -212,7 +211,7 @@
    1.31            else all_tac))
    1.32          |> Seq.hd
    1.33          |> Drule.zero_var_indexes
    1.34 -        |> Thm.put_name_tags ntags;
    1.35 +        |> Thm.put_name_tags (Thm.get_name_tags rule);
    1.36      in if Drule.weak_eq_thm (rule, rule'') then rule else rule'' end
    1.37    else rule;
    1.38  
    1.39 @@ -361,29 +360,29 @@
    1.40  fun delete x = delete_tagged_list (joinrules x);
    1.41  fun delete' x = delete_tagged_list (joinrules' x);
    1.42  
    1.43 -val mem_thm = gen_mem Drule.eq_thm_prop
    1.44 -and rem_thm = gen_rem Drule.eq_thm_prop;
    1.45 +val mem_thm = member Drule.eq_thm_prop
    1.46 +and rem_thm = remove Drule.eq_thm_prop;
    1.47  
    1.48  (*Warn if the rule is already present ELSEWHERE in the claset.  The addition
    1.49    is still allowed.*)
    1.50  fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, ...}) =
    1.51 -       if mem_thm (th, safeIs) then
    1.52 +       if mem_thm safeIs th then
    1.53           warning ("Rule already declared as safe introduction (intro!)\n" ^ string_of_thm th)
    1.54 -  else if mem_thm (th, safeEs) then
    1.55 +  else if mem_thm safeEs th then
    1.56           warning ("Rule already declared as safe elimination (elim!)\n" ^ string_of_thm th)
    1.57 -  else if mem_thm (th, hazIs) then
    1.58 +  else if mem_thm hazIs th then
    1.59           warning ("Rule already declared as introduction (intro)\n" ^ string_of_thm th)
    1.60 -  else if mem_thm (th, hazEs) then
    1.61 +  else if mem_thm hazEs th then
    1.62           warning ("Rule already declared as elimination (elim)\n" ^ string_of_thm th)
    1.63    else ();
    1.64  
    1.65  
    1.66  (*** Safe rules ***)
    1.67  
    1.68 -fun addSI th
    1.69 +fun addSI w th
    1.70    (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
    1.71               safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
    1.72 -  if mem_thm (th, safeIs) then
    1.73 +  if mem_thm safeIs th then
    1.74           (warning ("Ignoring duplicate safe introduction (intro!)\n" ^ string_of_thm th);
    1.75            cs)
    1.76    else
    1.77 @@ -402,13 +401,13 @@
    1.78          uwrappers    = uwrappers,
    1.79          haz_netpair  = haz_netpair,
    1.80          dup_netpair  = dup_netpair,
    1.81 -        xtra_netpair = insert' 0 (nI,nE) ([th], []) xtra_netpair}
    1.82 +        xtra_netpair = insert' (the_default 0 w) (nI,nE) ([th], []) xtra_netpair}
    1.83    end;
    1.84  
    1.85 -fun addSE th
    1.86 +fun addSE w th
    1.87    (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
    1.88               safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
    1.89 -  if mem_thm (th, safeEs) then
    1.90 +  if mem_thm safeEs th then
    1.91           (warning ("Ignoring duplicate safe elimination (elim!)\n" ^ string_of_thm th);
    1.92            cs)
    1.93    else if has_fewer_prems 1 th then
    1.94 @@ -431,11 +430,11 @@
    1.95          uwrappers    = uwrappers,
    1.96          haz_netpair  = haz_netpair,
    1.97          dup_netpair  = dup_netpair,
    1.98 -        xtra_netpair = insert' 0 (nI,nE) ([], [th]) xtra_netpair}
    1.99 +        xtra_netpair = insert' (the_default 0 w) (nI,nE) ([], [th]) xtra_netpair}
   1.100    end;
   1.101  
   1.102 -fun cs addSIs ths = fold_rev addSI ths cs;
   1.103 -fun cs addSEs ths = fold_rev addSE ths cs;
   1.104 +fun cs addSIs ths = fold_rev (addSI NONE) ths cs;
   1.105 +fun cs addSEs ths = fold_rev (addSE NONE) ths cs;
   1.106  
   1.107  (*Give new theorem a name, if it has one already.*)
   1.108  fun name_make_elim th =
   1.109 @@ -451,10 +450,10 @@
   1.110  
   1.111  (*** Hazardous (unsafe) rules ***)
   1.112  
   1.113 -fun addI th
   1.114 +fun addI w th
   1.115    (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   1.116               safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   1.117 -  if mem_thm (th, hazIs) then
   1.118 +  if mem_thm hazIs th then
   1.119           (warning ("Ignoring duplicate introduction (intro)\n" ^ string_of_thm th);
   1.120            cs)
   1.121    else
   1.122 @@ -471,15 +470,15 @@
   1.123          uwrappers     = uwrappers,
   1.124          safe0_netpair = safe0_netpair,
   1.125          safep_netpair = safep_netpair,
   1.126 -        xtra_netpair = insert' 1 (nI,nE) ([th], []) xtra_netpair}
   1.127 +        xtra_netpair = insert' (the_default 1 w) (nI,nE) ([th], []) xtra_netpair}
   1.128    end
   1.129    handle THM("RSN: no unifiers",_,_) => (*from dup_intr*)
   1.130           error ("Ill-formed introduction rule\n" ^ string_of_thm th);
   1.131  
   1.132 -fun addE th
   1.133 +fun addE w th
   1.134    (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   1.135              safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   1.136 -  if mem_thm (th, hazEs) then
   1.137 +  if mem_thm hazEs th then
   1.138           (warning ("Ignoring duplicate elimination (elim)\n" ^ string_of_thm th);
   1.139            cs)
   1.140    else if has_fewer_prems 1 th then
   1.141 @@ -500,11 +499,11 @@
   1.142          uwrappers     = uwrappers,
   1.143          safe0_netpair = safe0_netpair,
   1.144          safep_netpair = safep_netpair,
   1.145 -        xtra_netpair = insert' 1 (nI,nE) ([], [th]) xtra_netpair}
   1.146 +        xtra_netpair = insert' (the_default 1 w) (nI,nE) ([], [th]) xtra_netpair}
   1.147    end;
   1.148  
   1.149 -fun cs addIs ths = fold_rev addI ths cs;
   1.150 -fun cs addEs ths = fold_rev addE ths cs;
   1.151 +fun cs addIs ths = fold_rev (addI NONE) ths cs;
   1.152 +fun cs addEs ths = fold_rev (addE NONE) ths cs;
   1.153  
   1.154  fun cs addDs ths = cs addEs (map name_make_elim ths);
   1.155  
   1.156 @@ -512,18 +511,16 @@
   1.157  (*** Deletion of rules
   1.158       Working out what to delete, requires repeating much of the code used
   1.159          to insert.
   1.160 -     Separate functions delSI, etc., are not exported; instead delrules
   1.161 -        searches in all the lists and chooses the relevant delXX functions.
   1.162  ***)
   1.163  
   1.164  fun delSI th
   1.165            (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   1.166                      safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   1.167 - if mem_thm (th, safeIs) then
   1.168 + if mem_thm safeIs th then
   1.169     let val (safe0_rls, safep_rls) = List.partition Thm.no_prems [th]
   1.170     in CS{safe0_netpair = delete (safe0_rls, []) safe0_netpair,
   1.171           safep_netpair = delete (safep_rls, []) safep_netpair,
   1.172 -         safeIs = rem_thm (safeIs,th),
   1.173 +         safeIs = rem_thm th safeIs,
   1.174           safeEs = safeEs,
   1.175           hazIs  = hazIs,
   1.176           hazEs  = hazEs,
   1.177 @@ -538,14 +535,14 @@
   1.178  fun delSE th
   1.179            (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   1.180                      safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   1.181 -  if mem_thm (th, safeEs) then
   1.182 +  if mem_thm safeEs th then
   1.183      let
   1.184        val th' = classical_rule th
   1.185        val (safe0_rls, safep_rls) = List.partition (fn rl => nprems_of rl=1) [th']
   1.186      in CS{safe0_netpair = delete ([], safe0_rls) safe0_netpair,
   1.187           safep_netpair = delete ([], safep_rls) safep_netpair,
   1.188           safeIs = safeIs,
   1.189 -         safeEs = rem_thm (safeEs,th),
   1.190 +         safeEs = rem_thm th safeEs,
   1.191           hazIs  = hazIs,
   1.192           hazEs  = hazEs,
   1.193           swrappers    = swrappers,
   1.194 @@ -560,12 +557,12 @@
   1.195  fun delI th
   1.196           (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   1.197                     safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   1.198 - if mem_thm (th, hazIs) then
   1.199 + if mem_thm hazIs th then
   1.200       CS{haz_netpair = delete ([th], []) haz_netpair,
   1.201          dup_netpair = delete ([dup_intr th], []) dup_netpair,
   1.202          safeIs  = safeIs,
   1.203          safeEs  = safeEs,
   1.204 -        hazIs   = rem_thm (hazIs,th),
   1.205 +        hazIs   = rem_thm th hazIs,
   1.206          hazEs   = hazEs,
   1.207          swrappers     = swrappers,
   1.208          uwrappers     = uwrappers,
   1.209 @@ -581,13 +578,13 @@
   1.210           (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   1.211                     safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   1.212    let val th' = classical_rule th in
   1.213 -    if mem_thm (th, hazEs) then
   1.214 +    if mem_thm hazEs th then
   1.215       CS{haz_netpair = delete ([], [th']) haz_netpair,
   1.216          dup_netpair = delete ([], [dup_elim th']) dup_netpair,
   1.217          safeIs  = safeIs,
   1.218          safeEs  = safeEs,
   1.219          hazIs   = hazIs,
   1.220 -        hazEs   = rem_thm (hazEs,th),
   1.221 +        hazEs   = rem_thm th hazEs,
   1.222          swrappers     = swrappers,
   1.223          uwrappers     = uwrappers,
   1.224          safe0_netpair = safe0_netpair,
   1.225 @@ -600,9 +597,9 @@
   1.226  (*Delete ALL occurrences of "th" in the claset (perhaps from several lists)*)
   1.227  fun delrule th (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}) =
   1.228    let val th' = Tactic.make_elim th in
   1.229 -    if mem_thm (th, safeIs) orelse mem_thm (th, safeEs) orelse
   1.230 -      mem_thm (th, hazIs)  orelse mem_thm (th, hazEs) orelse
   1.231 -      mem_thm (th', safeEs) orelse mem_thm (th', hazEs)
   1.232 +    if mem_thm safeIs th orelse mem_thm safeEs th orelse
   1.233 +      mem_thm hazIs th orelse mem_thm hazEs th orelse
   1.234 +      mem_thm safeEs th' orelse mem_thm hazEs th'
   1.235      then delSI th (delSE th (delI th (delE th (delSE th' (delE th' cs)))))
   1.236      else (warning ("Undeclared classical rule\n" ^ string_of_thm th); cs)
   1.237    end;
   1.238 @@ -881,7 +878,7 @@
   1.239  
   1.240  (** claset data **)
   1.241  
   1.242 -(* global clasets *)
   1.243 +(* global claset *)
   1.244  
   1.245  structure GlobalClaset = TheoryDataFun
   1.246  (struct
   1.247 @@ -932,7 +929,7 @@
   1.248  fun del_context_unsafe_wrapper name = map_context_cs (apsnd (filter_out (equal name o #1)));
   1.249  
   1.250  
   1.251 -(* proof data kind 'Provers/claset' *)
   1.252 +(* local claset *)
   1.253  
   1.254  structure LocalClaset = ProofDataFun
   1.255  (struct
   1.256 @@ -953,16 +950,16 @@
   1.257  (* attributes *)
   1.258  
   1.259  fun attrib f = Attrib.declaration (fn th =>
   1.260 -   fn Context.Theory thy => (change_claset_of thy (fn cs => f (cs, [th])); Context.Theory thy)
   1.261 -    | Context.Proof ctxt => Context.Proof (LocalClaset.map (fn cs => f (cs, [th])) ctxt));
   1.262 +   fn Context.Theory thy => (change_claset_of thy (f th); Context.Theory thy)
   1.263 +    | Context.Proof ctxt => Context.Proof (LocalClaset.map (f th) ctxt));
   1.264  
   1.265 -val safe_dest = attrib (op addSDs);
   1.266 -val safe_elim = attrib (op addSEs);
   1.267 -val safe_intro = attrib (op addSIs);
   1.268 -val haz_dest = attrib (op addDs);
   1.269 -val haz_elim = attrib (op addEs);
   1.270 -val haz_intro = attrib (op addIs);
   1.271 -val rule_del = attrib (op delrules) o ContextRules.rule_del;
   1.272 +fun safe_dest w = attrib (addSE w o name_make_elim);
   1.273 +val safe_elim = attrib o addSE;
   1.274 +val safe_intro = attrib o addSI;
   1.275 +fun haz_dest w = attrib (addE w o name_make_elim);
   1.276 +val haz_elim = attrib o addE;
   1.277 +val haz_intro = attrib o addI;
   1.278 +val rule_del = attrib delrule o ContextRules.rule_del;
   1.279  
   1.280  
   1.281  (* tactics referring to the implicit claset *)
   1.282 @@ -986,31 +983,20 @@
   1.283  
   1.284  (** concrete syntax of attributes **)
   1.285  
   1.286 -(* add / del rules *)
   1.287 -
   1.288  val introN = "intro";
   1.289  val elimN = "elim";
   1.290  val destN = "dest";
   1.291  val ruleN = "rule";
   1.292  
   1.293 -fun add_rule xtra haz safe = Attrib.syntax
   1.294 - (Scan.lift (Args.query |-- Scan.option Args.nat >> xtra || Args.bang >> K safe ||
   1.295 -  Scan.succeed haz));
   1.296 -
   1.297 -fun del_rule att = Attrib.syntax (Scan.lift Args.del >> K att);
   1.298 -
   1.299 -
   1.300 -(* setup_attrs *)
   1.301 -
   1.302  val setup_attrs = Attrib.add_attributes
   1.303 - [("swapped", (swapped, swapped), "classical swap of introduction rule"),
   1.304 -  (destN, Attrib.common (add_rule ContextRules.dest_query haz_dest safe_dest),
   1.305 + [("swapped", Attrib.common swapped, "classical swap of introduction rule"),
   1.306 +  (destN, Attrib.common (ContextRules.add_args safe_dest haz_dest ContextRules.dest_query),
   1.307      "declaration of Classical destruction rule"),
   1.308 -  (elimN, Attrib.common (add_rule ContextRules.elim_query haz_elim safe_elim),
   1.309 +  (elimN, Attrib.common (ContextRules.add_args safe_elim haz_elim ContextRules.elim_query),
   1.310      "declaration of Classical elimination rule"),
   1.311 -  (introN, Attrib.common (add_rule ContextRules.intro_query haz_intro safe_intro),
   1.312 +  (introN, Attrib.common (ContextRules.add_args safe_intro haz_intro ContextRules.intro_query),
   1.313      "declaration of Classical introduction rule"),
   1.314 -  (ruleN, Attrib.common (del_rule rule_del),
   1.315 +  (ruleN, Attrib.common (Attrib.syntax (Scan.lift Args.del >> K rule_del)),
   1.316      "remove declaration of intro/elim/dest rule")];
   1.317  
   1.318  
   1.319 @@ -1058,12 +1044,12 @@
   1.320  (* automatic methods *)
   1.321  
   1.322  val cla_modifiers =
   1.323 - [Args.$$$ destN -- Args.bang_colon >> K ((I, Attrib.context safe_dest): Method.modifier),
   1.324 -  Args.$$$ destN -- Args.colon >> K (I, Attrib.context haz_dest),
   1.325 -  Args.$$$ elimN -- Args.bang_colon >> K (I, Attrib.context safe_elim),
   1.326 -  Args.$$$ elimN -- Args.colon >> K (I, Attrib.context haz_elim),
   1.327 -  Args.$$$ introN -- Args.bang_colon >> K (I, Attrib.context safe_intro),
   1.328 -  Args.$$$ introN -- Args.colon >> K (I, Attrib.context haz_intro),
   1.329 + [Args.$$$ destN -- Args.bang_colon >> K ((I, Attrib.context (safe_dest NONE)): Method.modifier),
   1.330 +  Args.$$$ destN -- Args.colon >> K (I, Attrib.context (haz_dest NONE)),
   1.331 +  Args.$$$ elimN -- Args.bang_colon >> K (I, Attrib.context (safe_elim NONE)),
   1.332 +  Args.$$$ elimN -- Args.colon >> K (I, Attrib.context (haz_elim NONE)),
   1.333 +  Args.$$$ introN -- Args.bang_colon >> K (I, Attrib.context (safe_intro NONE)),
   1.334 +  Args.$$$ introN -- Args.colon >> K (I, Attrib.context (haz_intro NONE)),
   1.335    Args.del -- Args.colon >> K (I, Attrib.context rule_del)];
   1.336  
   1.337  fun cla_meth tac prems ctxt = Method.METHOD (fn facts =>