added 'swapped' attribute;
authorwenzelm
Thu Dec 06 00:41:37 2001 +0100 (2001-12-06 ago)
changeset 124014363432ef0cd
parent 12400 f12f95e216e0
child 12402 cef751fff6b0
added 'swapped' attribute;
tuned xtra_netpair;
tuned;
src/Provers/classical.ML
     1.1 --- a/src/Provers/classical.ML	Thu Dec 06 00:40:56 2001 +0100
     1.2 +++ b/src/Provers/classical.ML	Thu Dec 06 00:41:37 2001 +0100
     1.3 @@ -47,7 +47,8 @@
     1.4                   swrappers: (string * wrapper) list,
     1.5                   uwrappers: (string * wrapper) list,
     1.6                   safe0_netpair: netpair, safep_netpair: netpair,
     1.7 -                 haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: netpair}
     1.8 +                 haz_netpair: netpair, dup_netpair: netpair,
     1.9 +                 xtra_netpair: ContextRules.netpair}
    1.10    val merge_cs          : claset * claset -> claset
    1.11    val addDs             : claset * thm list -> claset
    1.12    val addEs             : claset * thm list -> claset
    1.13 @@ -189,6 +190,7 @@
    1.14  
    1.15  (*Creates rules to eliminate ~A, from rules to introduce A*)
    1.16  fun swapify intrs = intrs RLN (2, [swap]);
    1.17 +fun swapped x = Attrib.no_args (fn (x, th) => (x, th RSN (2, swap))) x;
    1.18  
    1.19  (*Uses introduction rules in the normal way, or on negated assumptions,
    1.20    trying rules in order. *)
    1.21 @@ -213,17 +215,17 @@
    1.22  (**** Classical rule sets ****)
    1.23  
    1.24  datatype claset =
    1.25 -  CS of {safeIs         : thm list,             (*safe introduction rules*)
    1.26 -         safeEs         : thm list,             (*safe elimination rules*)
    1.27 -         hazIs          : thm list,             (*unsafe introduction rules*)
    1.28 -         hazEs          : thm list,             (*unsafe elimination rules*)
    1.29 -         swrappers      : (string * wrapper) list, (*for transf. safe_step_tac*)
    1.30 +  CS of {safeIs         : thm list,                (*safe introduction rules*)
    1.31 +         safeEs         : thm list,                (*safe elimination rules*)
    1.32 +         hazIs          : thm list,                (*unsafe introduction rules*)
    1.33 +         hazEs          : thm list,                (*unsafe elimination rules*)
    1.34 +         swrappers      : (string * wrapper) list, (*for transforming safe_step_tac*)
    1.35           uwrappers      : (string * wrapper) list, (*for transforming step_tac*)
    1.36 -         safe0_netpair  : netpair,              (*nets for trivial cases*)
    1.37 -         safep_netpair  : netpair,              (*nets for >0 subgoals*)
    1.38 -         haz_netpair    : netpair,              (*nets for unsafe rules*)
    1.39 -         dup_netpair    : netpair,              (*nets for duplication*)
    1.40 -         xtra_netpair   : netpair};             (*nets for extra rules*)
    1.41 +         safe0_netpair  : netpair,                 (*nets for trivial cases*)
    1.42 +         safep_netpair  : netpair,                 (*nets for >0 subgoals*)
    1.43 +         haz_netpair    : netpair,                 (*nets for unsafe rules*)
    1.44 +         dup_netpair    : netpair,                 (*nets for duplication*)
    1.45 +         xtra_netpair   : ContextRules.netpair};   (*nets for extra rules*)
    1.46  
    1.47  (*Desired invariants are
    1.48          safe0_netpair = build safe0_brls,
    1.49 @@ -283,7 +285,7 @@
    1.50  fun joinrules (intrs, elims) =
    1.51    (map (pair true) (elims @ swapify intrs) @ map (pair false) intrs);
    1.52  
    1.53 -fun joinrules_simple (intrs, elims) =
    1.54 +fun joinrules' (intrs, elims) =
    1.55    (map (pair true) elims @ map (pair false) intrs);
    1.56  
    1.57  (*Priority: prefer rules with fewest subgoals,
    1.58 @@ -293,8 +295,8 @@
    1.59        (1000000*subgoals_of_brl brl + k, brl) ::
    1.60        tag_brls (k+1) brls;
    1.61  
    1.62 -fun tag_brls_simple k [] = []
    1.63 -  | tag_brls_simple k (brl::brls) = (k, brl) :: tag_brls_simple (k+1) brls;
    1.64 +fun tag_brls' _ _ [] = []
    1.65 +  | tag_brls' w k (brl::brls) = ((w, k), brl) :: tag_brls' w (k + 1) brls;
    1.66  
    1.67  fun insert_tagged_list kbrls netpr = foldr Tactic.insert_tagged_brl (kbrls, netpr);
    1.68  
    1.69 @@ -302,11 +304,11 @@
    1.70    Count the intr rules double (to account for swapify).  Negate to give the
    1.71    new insertions the lowest priority.*)
    1.72  fun insert (nI, nE) = insert_tagged_list o (tag_brls (~(2*nI+nE))) o joinrules;
    1.73 -fun insert_simple (nI, nE) = insert_tagged_list o tag_brls_simple (~(nI + nE)) o joinrules_simple;
    1.74 +fun insert' w (nI, nE) = insert_tagged_list o tag_brls' w (~(nI + nE)) o joinrules';
    1.75  
    1.76  fun delete_tagged_list brls netpr = foldr Tactic.delete_tagged_brl (brls, netpr);
    1.77  fun delete x = delete_tagged_list (joinrules x);
    1.78 -fun delete_simple x = delete_tagged_list (joinrules_simple x);
    1.79 +fun delete' x = delete_tagged_list (joinrules' x);
    1.80  
    1.81  val mem_thm = gen_mem eq_thm
    1.82  and rem_thm = gen_rem eq_thm;
    1.83 @@ -349,7 +351,7 @@
    1.84          uwrappers    = uwrappers,
    1.85          haz_netpair  = haz_netpair,
    1.86          dup_netpair  = dup_netpair,
    1.87 -        xtra_netpair = insert_simple (nI,nE) ([th], []) xtra_netpair}
    1.88 +        xtra_netpair = insert' 0 (nI,nE) ([th], []) xtra_netpair}
    1.89    end;
    1.90  
    1.91  fun addSE (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
    1.92 @@ -374,7 +376,7 @@
    1.93          uwrappers    = uwrappers,
    1.94          haz_netpair  = haz_netpair,
    1.95          dup_netpair  = dup_netpair,
    1.96 -        xtra_netpair = insert_simple (nI,nE) ([], [th]) xtra_netpair}
    1.97 +        xtra_netpair = insert' 0 (nI,nE) ([], [th]) xtra_netpair}
    1.98    end;
    1.99  
   1.100  fun rev_foldl f (e, l) = foldl f (e, rev l);
   1.101 @@ -407,7 +409,7 @@
   1.102          uwrappers     = uwrappers,
   1.103          safe0_netpair = safe0_netpair,
   1.104          safep_netpair = safep_netpair,
   1.105 -        xtra_netpair = insert_simple (nI,nE) ([th], []) xtra_netpair}
   1.106 +        xtra_netpair = insert' 1 (nI,nE) ([th], []) xtra_netpair}
   1.107    end;
   1.108  
   1.109  fun addE (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   1.110 @@ -430,7 +432,7 @@
   1.111          uwrappers     = uwrappers,
   1.112          safe0_netpair = safe0_netpair,
   1.113          safep_netpair = safep_netpair,
   1.114 -        xtra_netpair = insert_simple (nI,nE) ([], [th]) xtra_netpair}
   1.115 +        xtra_netpair = insert' 1 (nI,nE) ([], [th]) xtra_netpair}
   1.116    end;
   1.117  
   1.118  val op addIs = rev_foldl addI;
   1.119 @@ -461,7 +463,7 @@
   1.120           uwrappers    = uwrappers,
   1.121           haz_netpair  = haz_netpair,
   1.122           dup_netpair  = dup_netpair,
   1.123 -         xtra_netpair = delete_simple ([th], []) xtra_netpair}
   1.124 +         xtra_netpair = delete' ([th], []) xtra_netpair}
   1.125     end
   1.126   else cs;
   1.127  
   1.128 @@ -480,7 +482,7 @@
   1.129           uwrappers    = uwrappers,
   1.130           haz_netpair  = haz_netpair,
   1.131           dup_netpair  = dup_netpair,
   1.132 -         xtra_netpair = delete_simple ([], [th]) xtra_netpair}
   1.133 +         xtra_netpair = delete' ([], [th]) xtra_netpair}
   1.134     end
   1.135   else cs;
   1.136  
   1.137 @@ -499,7 +501,7 @@
   1.138          uwrappers     = uwrappers,
   1.139          safe0_netpair = safe0_netpair,
   1.140          safep_netpair = safep_netpair,
   1.141 -        xtra_netpair = delete_simple ([th], []) xtra_netpair}
   1.142 +        xtra_netpair = delete' ([th], []) xtra_netpair}
   1.143   else cs;
   1.144  
   1.145  fun delE th
   1.146 @@ -516,7 +518,7 @@
   1.147          uwrappers     = uwrappers,
   1.148          safe0_netpair = safe0_netpair,
   1.149          safep_netpair = safep_netpair,
   1.150 -        xtra_netpair = delete_simple ([], [th]) xtra_netpair}
   1.151 +        xtra_netpair = delete' ([], [th]) xtra_netpair}
   1.152   else cs;
   1.153  
   1.154  
   1.155 @@ -902,6 +904,7 @@
   1.156  val setup_attrs = Attrib.add_attributes
   1.157   [("elim_format", (elim_format, elim_format),
   1.158      "destruct rule turned into elimination rule format (classical)"),
   1.159 +  ("swapped", (swapped, swapped), "classical swap of introduction rule"),
   1.160    (destN,
   1.161     (add_rule ContextRules.dest_query_global haz_dest_global safe_dest_global,
   1.162      add_rule ContextRules.dest_query_local haz_dest_local safe_dest_local),
   1.163 @@ -929,17 +932,10 @@
   1.164  
   1.165  local
   1.166  
   1.167 -fun may_unify t net = map snd (Tactic.orderlist (Net.unify_term net t));
   1.168 -
   1.169 -fun find_erules [] = K []
   1.170 -  | find_erules (fact :: _) = may_unify (Logic.strip_assums_concl (#prop (Thm.rep_thm fact)));
   1.171 -fun find_irules goal = may_unify (Logic.strip_assums_concl goal);
   1.172 -fun find_rules (inet, enet) facts goal = find_erules facts enet @ find_irules goal inet;
   1.173 -
   1.174  fun some_rule_tac ctxt (CS {xtra_netpair, ...}) facts = SUBGOAL (fn (goal, i) =>
   1.175    let
   1.176 -    val [rules1, rules2, rules4] = ContextRules.find_rules ctxt facts goal;
   1.177 -    val rules3 = find_rules xtra_netpair facts goal;
   1.178 +    val [rules1, rules2, rules4] = ContextRules.find_rules false facts goal ctxt;
   1.179 +    val rules3 = ContextRules.find_rules_netpair true facts goal xtra_netpair;
   1.180      val rules = rules1 @ rules2 @ rules3 @ rules4;
   1.181      val ruleq = Method.multi_resolves facts rules;
   1.182    in