# HG changeset patch # User wenzelm # Date 1137351534 -3600 # Node ID a2dc15d9d6c8139f7e7a559524e69504453af491 # Parent 16a64bdc548592b67e6b19672e6099381afaf13d attributes: optional weight; tuned; diff -r 16a64bdc5485 -r a2dc15d9d6c8 src/Provers/classical.ML --- a/src/Provers/classical.ML Sun Jan 15 19:58:53 2006 +0100 +++ b/src/Provers/classical.ML Sun Jan 15 19:58:54 2006 +0100 @@ -143,12 +143,12 @@ val print_local_claset: Proof.context -> unit val get_local_claset: Proof.context -> claset val put_local_claset: claset -> Proof.context -> Proof.context - val safe_dest: Context.generic attribute - val safe_elim: Context.generic attribute - val safe_intro: Context.generic attribute - val haz_dest: Context.generic attribute - val haz_elim: Context.generic attribute - val haz_intro: Context.generic attribute + val safe_dest: int option -> Context.generic attribute + val safe_elim: int option -> Context.generic attribute + val safe_intro: int option -> Context.generic attribute + val haz_dest: int option -> Context.generic attribute + val haz_elim: int option -> Context.generic attribute + val haz_intro: int option -> Context.generic attribute val rule_del: Context.generic attribute val cla_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list val cla_meth: (claset -> tactic) -> thm list -> Proof.context -> Proof.method @@ -197,7 +197,6 @@ fun classical_rule rule = if is_elim rule then let - val ntags = Thm.get_name_tags rule; val rule' = rule RS classical; val concl' = Thm.concl_of rule'; fun redundant_hyp goal = @@ -212,7 +211,7 @@ else all_tac)) |> Seq.hd |> Drule.zero_var_indexes - |> Thm.put_name_tags ntags; + |> Thm.put_name_tags (Thm.get_name_tags rule); in if Drule.weak_eq_thm (rule, rule'') then rule else rule'' end else rule; @@ -361,29 +360,29 @@ fun delete x = delete_tagged_list (joinrules x); fun delete' x = delete_tagged_list (joinrules' x); -val mem_thm = gen_mem Drule.eq_thm_prop -and rem_thm = gen_rem Drule.eq_thm_prop; +val mem_thm = member Drule.eq_thm_prop +and rem_thm = remove Drule.eq_thm_prop; (*Warn if the rule is already present ELSEWHERE in the claset. The addition is still allowed.*) fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, ...}) = - if mem_thm (th, safeIs) then + if mem_thm safeIs th then warning ("Rule already declared as safe introduction (intro!)\n" ^ string_of_thm th) - else if mem_thm (th, safeEs) then + else if mem_thm safeEs th then warning ("Rule already declared as safe elimination (elim!)\n" ^ string_of_thm th) - else if mem_thm (th, hazIs) then + else if mem_thm hazIs th then warning ("Rule already declared as introduction (intro)\n" ^ string_of_thm th) - else if mem_thm (th, hazEs) then + else if mem_thm hazEs th then warning ("Rule already declared as elimination (elim)\n" ^ string_of_thm th) else (); (*** Safe rules ***) -fun addSI th +fun addSI w th (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = - if mem_thm (th, safeIs) then + if mem_thm safeIs th then (warning ("Ignoring duplicate safe introduction (intro!)\n" ^ string_of_thm th); cs) else @@ -402,13 +401,13 @@ uwrappers = uwrappers, haz_netpair = haz_netpair, dup_netpair = dup_netpair, - xtra_netpair = insert' 0 (nI,nE) ([th], []) xtra_netpair} + xtra_netpair = insert' (the_default 0 w) (nI,nE) ([th], []) xtra_netpair} end; -fun addSE th +fun addSE w th (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = - if mem_thm (th, safeEs) then + if mem_thm safeEs th then (warning ("Ignoring duplicate safe elimination (elim!)\n" ^ string_of_thm th); cs) else if has_fewer_prems 1 th then @@ -431,11 +430,11 @@ uwrappers = uwrappers, haz_netpair = haz_netpair, dup_netpair = dup_netpair, - xtra_netpair = insert' 0 (nI,nE) ([], [th]) xtra_netpair} + xtra_netpair = insert' (the_default 0 w) (nI,nE) ([], [th]) xtra_netpair} end; -fun cs addSIs ths = fold_rev addSI ths cs; -fun cs addSEs ths = fold_rev addSE ths cs; +fun cs addSIs ths = fold_rev (addSI NONE) ths cs; +fun cs addSEs ths = fold_rev (addSE NONE) ths cs; (*Give new theorem a name, if it has one already.*) fun name_make_elim th = @@ -451,10 +450,10 @@ (*** Hazardous (unsafe) rules ***) -fun addI th +fun addI w th (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = - if mem_thm (th, hazIs) then + if mem_thm hazIs th then (warning ("Ignoring duplicate introduction (intro)\n" ^ string_of_thm th); cs) else @@ -471,15 +470,15 @@ uwrappers = uwrappers, safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, - xtra_netpair = insert' 1 (nI,nE) ([th], []) xtra_netpair} + xtra_netpair = insert' (the_default 1 w) (nI,nE) ([th], []) xtra_netpair} end handle THM("RSN: no unifiers",_,_) => (*from dup_intr*) error ("Ill-formed introduction rule\n" ^ string_of_thm th); -fun addE th +fun addE w th (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = - if mem_thm (th, hazEs) then + if mem_thm hazEs th then (warning ("Ignoring duplicate elimination (elim)\n" ^ string_of_thm th); cs) else if has_fewer_prems 1 th then @@ -500,11 +499,11 @@ uwrappers = uwrappers, safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, - xtra_netpair = insert' 1 (nI,nE) ([], [th]) xtra_netpair} + xtra_netpair = insert' (the_default 1 w) (nI,nE) ([], [th]) xtra_netpair} end; -fun cs addIs ths = fold_rev addI ths cs; -fun cs addEs ths = fold_rev addE ths cs; +fun cs addIs ths = fold_rev (addI NONE) ths cs; +fun cs addEs ths = fold_rev (addE NONE) ths cs; fun cs addDs ths = cs addEs (map name_make_elim ths); @@ -512,18 +511,16 @@ (*** Deletion of rules Working out what to delete, requires repeating much of the code used to insert. - Separate functions delSI, etc., are not exported; instead delrules - searches in all the lists and chooses the relevant delXX functions. ***) fun delSI th (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = - if mem_thm (th, safeIs) then + if mem_thm safeIs th then let val (safe0_rls, safep_rls) = List.partition Thm.no_prems [th] in CS{safe0_netpair = delete (safe0_rls, []) safe0_netpair, safep_netpair = delete (safep_rls, []) safep_netpair, - safeIs = rem_thm (safeIs,th), + safeIs = rem_thm th safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs, @@ -538,14 +535,14 @@ fun delSE th (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = - if mem_thm (th, safeEs) then + if mem_thm safeEs th then let val th' = classical_rule th val (safe0_rls, safep_rls) = List.partition (fn rl => nprems_of rl=1) [th'] in CS{safe0_netpair = delete ([], safe0_rls) safe0_netpair, safep_netpair = delete ([], safep_rls) safep_netpair, safeIs = safeIs, - safeEs = rem_thm (safeEs,th), + safeEs = rem_thm th safeEs, hazIs = hazIs, hazEs = hazEs, swrappers = swrappers, @@ -560,12 +557,12 @@ fun delI th (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = - if mem_thm (th, hazIs) then + if mem_thm hazIs th then CS{haz_netpair = delete ([th], []) haz_netpair, dup_netpair = delete ([dup_intr th], []) dup_netpair, safeIs = safeIs, safeEs = safeEs, - hazIs = rem_thm (hazIs,th), + hazIs = rem_thm th hazIs, hazEs = hazEs, swrappers = swrappers, uwrappers = uwrappers, @@ -581,13 +578,13 @@ (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = let val th' = classical_rule th in - if mem_thm (th, hazEs) then + if mem_thm hazEs th then CS{haz_netpair = delete ([], [th']) haz_netpair, dup_netpair = delete ([], [dup_elim th']) dup_netpair, safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, - hazEs = rem_thm (hazEs,th), + hazEs = rem_thm th hazEs, swrappers = swrappers, uwrappers = uwrappers, safe0_netpair = safe0_netpair, @@ -600,9 +597,9 @@ (*Delete ALL occurrences of "th" in the claset (perhaps from several lists)*) fun delrule th (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}) = let val th' = Tactic.make_elim th in - if mem_thm (th, safeIs) orelse mem_thm (th, safeEs) orelse - mem_thm (th, hazIs) orelse mem_thm (th, hazEs) orelse - mem_thm (th', safeEs) orelse mem_thm (th', hazEs) + if mem_thm safeIs th orelse mem_thm safeEs th orelse + mem_thm hazIs th orelse mem_thm hazEs th orelse + mem_thm safeEs th' orelse mem_thm hazEs th' then delSI th (delSE th (delI th (delE th (delSE th' (delE th' cs))))) else (warning ("Undeclared classical rule\n" ^ string_of_thm th); cs) end; @@ -881,7 +878,7 @@ (** claset data **) -(* global clasets *) +(* global claset *) structure GlobalClaset = TheoryDataFun (struct @@ -932,7 +929,7 @@ fun del_context_unsafe_wrapper name = map_context_cs (apsnd (filter_out (equal name o #1))); -(* proof data kind 'Provers/claset' *) +(* local claset *) structure LocalClaset = ProofDataFun (struct @@ -953,16 +950,16 @@ (* attributes *) fun attrib f = Attrib.declaration (fn th => - fn Context.Theory thy => (change_claset_of thy (fn cs => f (cs, [th])); Context.Theory thy) - | Context.Proof ctxt => Context.Proof (LocalClaset.map (fn cs => f (cs, [th])) ctxt)); + fn Context.Theory thy => (change_claset_of thy (f th); Context.Theory thy) + | Context.Proof ctxt => Context.Proof (LocalClaset.map (f th) ctxt)); -val safe_dest = attrib (op addSDs); -val safe_elim = attrib (op addSEs); -val safe_intro = attrib (op addSIs); -val haz_dest = attrib (op addDs); -val haz_elim = attrib (op addEs); -val haz_intro = attrib (op addIs); -val rule_del = attrib (op delrules) o ContextRules.rule_del; +fun safe_dest w = attrib (addSE w o name_make_elim); +val safe_elim = attrib o addSE; +val safe_intro = attrib o addSI; +fun haz_dest w = attrib (addE w o name_make_elim); +val haz_elim = attrib o addE; +val haz_intro = attrib o addI; +val rule_del = attrib delrule o ContextRules.rule_del; (* tactics referring to the implicit claset *) @@ -986,31 +983,20 @@ (** concrete syntax of attributes **) -(* add / del rules *) - val introN = "intro"; val elimN = "elim"; val destN = "dest"; val ruleN = "rule"; -fun add_rule xtra haz safe = Attrib.syntax - (Scan.lift (Args.query |-- Scan.option Args.nat >> xtra || Args.bang >> K safe || - Scan.succeed haz)); - -fun del_rule att = Attrib.syntax (Scan.lift Args.del >> K att); - - -(* setup_attrs *) - val setup_attrs = Attrib.add_attributes - [("swapped", (swapped, swapped), "classical swap of introduction rule"), - (destN, Attrib.common (add_rule ContextRules.dest_query haz_dest safe_dest), + [("swapped", Attrib.common swapped, "classical swap of introduction rule"), + (destN, Attrib.common (ContextRules.add_args safe_dest haz_dest ContextRules.dest_query), "declaration of Classical destruction rule"), - (elimN, Attrib.common (add_rule ContextRules.elim_query haz_elim safe_elim), + (elimN, Attrib.common (ContextRules.add_args safe_elim haz_elim ContextRules.elim_query), "declaration of Classical elimination rule"), - (introN, Attrib.common (add_rule ContextRules.intro_query haz_intro safe_intro), + (introN, Attrib.common (ContextRules.add_args safe_intro haz_intro ContextRules.intro_query), "declaration of Classical introduction rule"), - (ruleN, Attrib.common (del_rule rule_del), + (ruleN, Attrib.common (Attrib.syntax (Scan.lift Args.del >> K rule_del)), "remove declaration of intro/elim/dest rule")]; @@ -1058,12 +1044,12 @@ (* automatic methods *) val cla_modifiers = - [Args.$$$ destN -- Args.bang_colon >> K ((I, Attrib.context safe_dest): Method.modifier), - Args.$$$ destN -- Args.colon >> K (I, Attrib.context haz_dest), - Args.$$$ elimN -- Args.bang_colon >> K (I, Attrib.context safe_elim), - Args.$$$ elimN -- Args.colon >> K (I, Attrib.context haz_elim), - Args.$$$ introN -- Args.bang_colon >> K (I, Attrib.context safe_intro), - Args.$$$ introN -- Args.colon >> K (I, Attrib.context haz_intro), + [Args.$$$ destN -- Args.bang_colon >> K ((I, Attrib.context (safe_dest NONE)): Method.modifier), + Args.$$$ destN -- Args.colon >> K (I, Attrib.context (haz_dest NONE)), + Args.$$$ elimN -- Args.bang_colon >> K (I, Attrib.context (safe_elim NONE)), + Args.$$$ elimN -- Args.colon >> K (I, Attrib.context (haz_elim NONE)), + Args.$$$ introN -- Args.bang_colon >> K (I, Attrib.context (safe_intro NONE)), + Args.$$$ introN -- Args.colon >> K (I, Attrib.context (haz_intro NONE)), Args.del -- Args.colon >> K (I, Attrib.context rule_del)]; fun cla_meth tac prems ctxt = Method.METHOD (fn facts =>