# HG changeset patch # User wenzelm # Date 1007595697 -3600 # Node ID 4363432ef0cddf251b2e7d40595dc0574c961d83 # Parent f12f95e216e05fb13475704ea1f64d17e62a9cff added 'swapped' attribute; tuned xtra_netpair; tuned; diff -r f12f95e216e0 -r 4363432ef0cd src/Provers/classical.ML --- a/src/Provers/classical.ML Thu Dec 06 00:40:56 2001 +0100 +++ b/src/Provers/classical.ML Thu Dec 06 00:41:37 2001 +0100 @@ -47,7 +47,8 @@ swrappers: (string * wrapper) list, uwrappers: (string * wrapper) list, safe0_netpair: netpair, safep_netpair: netpair, - haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: netpair} + haz_netpair: netpair, dup_netpair: netpair, + xtra_netpair: ContextRules.netpair} val merge_cs : claset * claset -> claset val addDs : claset * thm list -> claset val addEs : claset * thm list -> claset @@ -189,6 +190,7 @@ (*Creates rules to eliminate ~A, from rules to introduce A*) fun swapify intrs = intrs RLN (2, [swap]); +fun swapped x = Attrib.no_args (fn (x, th) => (x, th RSN (2, swap))) x; (*Uses introduction rules in the normal way, or on negated assumptions, trying rules in order. *) @@ -213,17 +215,17 @@ (**** Classical rule sets ****) datatype claset = - CS of {safeIs : thm list, (*safe introduction rules*) - safeEs : thm list, (*safe elimination rules*) - hazIs : thm list, (*unsafe introduction rules*) - hazEs : thm list, (*unsafe elimination rules*) - swrappers : (string * wrapper) list, (*for transf. safe_step_tac*) + CS of {safeIs : thm list, (*safe introduction rules*) + safeEs : thm list, (*safe elimination rules*) + hazIs : thm list, (*unsafe introduction rules*) + hazEs : thm list, (*unsafe elimination rules*) + swrappers : (string * wrapper) list, (*for transforming safe_step_tac*) uwrappers : (string * wrapper) list, (*for transforming step_tac*) - safe0_netpair : netpair, (*nets for trivial cases*) - safep_netpair : netpair, (*nets for >0 subgoals*) - haz_netpair : netpair, (*nets for unsafe rules*) - dup_netpair : netpair, (*nets for duplication*) - xtra_netpair : netpair}; (*nets for extra rules*) + safe0_netpair : netpair, (*nets for trivial cases*) + safep_netpair : netpair, (*nets for >0 subgoals*) + haz_netpair : netpair, (*nets for unsafe rules*) + dup_netpair : netpair, (*nets for duplication*) + xtra_netpair : ContextRules.netpair}; (*nets for extra rules*) (*Desired invariants are safe0_netpair = build safe0_brls, @@ -283,7 +285,7 @@ fun joinrules (intrs, elims) = (map (pair true) (elims @ swapify intrs) @ map (pair false) intrs); -fun joinrules_simple (intrs, elims) = +fun joinrules' (intrs, elims) = (map (pair true) elims @ map (pair false) intrs); (*Priority: prefer rules with fewest subgoals, @@ -293,8 +295,8 @@ (1000000*subgoals_of_brl brl + k, brl) :: tag_brls (k+1) brls; -fun tag_brls_simple k [] = [] - | tag_brls_simple k (brl::brls) = (k, brl) :: tag_brls_simple (k+1) brls; +fun tag_brls' _ _ [] = [] + | tag_brls' w k (brl::brls) = ((w, k), brl) :: tag_brls' w (k + 1) brls; fun insert_tagged_list kbrls netpr = foldr Tactic.insert_tagged_brl (kbrls, netpr); @@ -302,11 +304,11 @@ Count the intr rules double (to account for swapify). Negate to give the new insertions the lowest priority.*) fun insert (nI, nE) = insert_tagged_list o (tag_brls (~(2*nI+nE))) o joinrules; -fun insert_simple (nI, nE) = insert_tagged_list o tag_brls_simple (~(nI + nE)) o joinrules_simple; +fun insert' w (nI, nE) = insert_tagged_list o tag_brls' w (~(nI + nE)) o joinrules'; fun delete_tagged_list brls netpr = foldr Tactic.delete_tagged_brl (brls, netpr); fun delete x = delete_tagged_list (joinrules x); -fun delete_simple x = delete_tagged_list (joinrules_simple x); +fun delete' x = delete_tagged_list (joinrules' x); val mem_thm = gen_mem eq_thm and rem_thm = gen_rem eq_thm; @@ -349,7 +351,7 @@ uwrappers = uwrappers, haz_netpair = haz_netpair, dup_netpair = dup_netpair, - xtra_netpair = insert_simple (nI,nE) ([th], []) xtra_netpair} + xtra_netpair = insert' 0 (nI,nE) ([th], []) xtra_netpair} end; fun addSE (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, @@ -374,7 +376,7 @@ uwrappers = uwrappers, haz_netpair = haz_netpair, dup_netpair = dup_netpair, - xtra_netpair = insert_simple (nI,nE) ([], [th]) xtra_netpair} + xtra_netpair = insert' 0 (nI,nE) ([], [th]) xtra_netpair} end; fun rev_foldl f (e, l) = foldl f (e, rev l); @@ -407,7 +409,7 @@ uwrappers = uwrappers, safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, - xtra_netpair = insert_simple (nI,nE) ([th], []) xtra_netpair} + xtra_netpair = insert' 1 (nI,nE) ([th], []) xtra_netpair} end; fun addE (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, @@ -430,7 +432,7 @@ uwrappers = uwrappers, safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, - xtra_netpair = insert_simple (nI,nE) ([], [th]) xtra_netpair} + xtra_netpair = insert' 1 (nI,nE) ([], [th]) xtra_netpair} end; val op addIs = rev_foldl addI; @@ -461,7 +463,7 @@ uwrappers = uwrappers, haz_netpair = haz_netpair, dup_netpair = dup_netpair, - xtra_netpair = delete_simple ([th], []) xtra_netpair} + xtra_netpair = delete' ([th], []) xtra_netpair} end else cs; @@ -480,7 +482,7 @@ uwrappers = uwrappers, haz_netpair = haz_netpair, dup_netpair = dup_netpair, - xtra_netpair = delete_simple ([], [th]) xtra_netpair} + xtra_netpair = delete' ([], [th]) xtra_netpair} end else cs; @@ -499,7 +501,7 @@ uwrappers = uwrappers, safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, - xtra_netpair = delete_simple ([th], []) xtra_netpair} + xtra_netpair = delete' ([th], []) xtra_netpair} else cs; fun delE th @@ -516,7 +518,7 @@ uwrappers = uwrappers, safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, - xtra_netpair = delete_simple ([], [th]) xtra_netpair} + xtra_netpair = delete' ([], [th]) xtra_netpair} else cs; @@ -902,6 +904,7 @@ val setup_attrs = Attrib.add_attributes [("elim_format", (elim_format, elim_format), "destruct rule turned into elimination rule format (classical)"), + ("swapped", (swapped, swapped), "classical swap of introduction rule"), (destN, (add_rule ContextRules.dest_query_global haz_dest_global safe_dest_global, add_rule ContextRules.dest_query_local haz_dest_local safe_dest_local), @@ -929,17 +932,10 @@ local -fun may_unify t net = map snd (Tactic.orderlist (Net.unify_term net t)); - -fun find_erules [] = K [] - | find_erules (fact :: _) = may_unify (Logic.strip_assums_concl (#prop (Thm.rep_thm fact))); -fun find_irules goal = may_unify (Logic.strip_assums_concl goal); -fun find_rules (inet, enet) facts goal = find_erules facts enet @ find_irules goal inet; - fun some_rule_tac ctxt (CS {xtra_netpair, ...}) facts = SUBGOAL (fn (goal, i) => let - val [rules1, rules2, rules4] = ContextRules.find_rules ctxt facts goal; - val rules3 = find_rules xtra_netpair facts goal; + val [rules1, rules2, rules4] = ContextRules.find_rules false facts goal ctxt; + val rules3 = ContextRules.find_rules_netpair true facts goal xtra_netpair; val rules = rules1 @ rules2 @ rules3 @ rules4; val ruleq = Method.multi_resolves facts rules; in