src/Provers/classical.ML
changeset 42810 2425068fe13a
parent 42807 e639d91d9073
child 42812 dda4aef7cba4
     1.1 --- a/src/Provers/classical.ML	Sat May 14 18:29:06 2011 +0200
     1.2 +++ b/src/Provers/classical.ML	Sat May 14 21:42:17 2011 +0200
     1.3 @@ -37,11 +37,12 @@
     1.4  sig
     1.5    type claset
     1.6    val empty_cs: claset
     1.7 +  val merge_cs: claset * claset -> claset
     1.8    val rep_cs: claset ->
     1.9 -   {safeIs: thm list,
    1.10 -    safeEs: thm list,
    1.11 -    hazIs: thm list,
    1.12 -    hazEs: thm list,
    1.13 +   {safeIs: thm Item_Net.T,
    1.14 +    safeEs: thm Item_Net.T,
    1.15 +    hazIs: thm Item_Net.T,
    1.16 +    hazEs: thm Item_Net.T,
    1.17      swrappers: (string * (Proof.context -> wrapper)) list,
    1.18      uwrappers: (string * (Proof.context -> wrapper)) list,
    1.19      safe0_netpair: netpair,
    1.20 @@ -214,10 +215,10 @@
    1.21  
    1.22  datatype claset =
    1.23    CS of
    1.24 -   {safeIs         : thm list,                (*safe introduction rules*)
    1.25 -    safeEs         : thm list,                (*safe elimination rules*)
    1.26 -    hazIs          : thm list,                (*unsafe introduction rules*)
    1.27 -    hazEs          : thm list,                (*unsafe elimination rules*)
    1.28 +   {safeIs         : thm Item_Net.T,          (*safe introduction rules*)
    1.29 +    safeEs         : thm Item_Net.T,          (*safe elimination rules*)
    1.30 +    hazIs          : thm Item_Net.T,          (*unsafe introduction rules*)
    1.31 +    hazEs          : thm Item_Net.T,          (*unsafe elimination rules*)
    1.32      swrappers      : (string * (Proof.context -> wrapper)) list, (*for transforming safe_step_tac*)
    1.33      uwrappers      : (string * (Proof.context -> wrapper)) list, (*for transforming step_tac*)
    1.34      safe0_netpair  : netpair,                 (*nets for trivial cases*)
    1.35 @@ -244,10 +245,10 @@
    1.36  
    1.37  val empty_cs =
    1.38    CS
    1.39 -   {safeIs = [],
    1.40 -    safeEs = [],
    1.41 -    hazIs = [],
    1.42 -    hazEs = [],
    1.43 +   {safeIs = Thm.full_rules,
    1.44 +    safeEs = Thm.full_rules,
    1.45 +    hazIs = Thm.full_rules,
    1.46 +    hazEs = Thm.full_rules,
    1.47      swrappers = [],
    1.48      uwrappers = [],
    1.49      safe0_netpair = empty_netpair,
    1.50 @@ -294,9 +295,6 @@
    1.51  fun delete x = delete_tagged_list (joinrules x);
    1.52  fun delete' x = delete_tagged_list (joinrules' x);
    1.53  
    1.54 -val mem_thm = member Thm.eq_thm_prop
    1.55 -and rem_thm = remove Thm.eq_thm_prop;
    1.56 -
    1.57  fun string_of_thm NONE = Display.string_of_thm_without_context
    1.58    | string_of_thm (SOME context) =
    1.59        Display.string_of_thm (Context.cases Syntax.init_pretty_global I context);
    1.60 @@ -312,7 +310,7 @@
    1.61    else ();
    1.62  
    1.63  fun warn_rules context msg rules th =
    1.64 -  mem_thm rules th andalso (warn_thm context msg th; true);
    1.65 +  Item_Net.member rules th andalso (warn_thm context msg th; true);
    1.66  
    1.67  fun warn_claset context th (CS {safeIs, safeEs, hazIs, hazEs, ...}) =
    1.68    warn_rules context "Rule already declared as safe introduction (intro!)\n" safeIs th orelse
    1.69 @@ -332,12 +330,12 @@
    1.70        val th' = flat_rule th;
    1.71        val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
    1.72          List.partition Thm.no_prems [th'];
    1.73 -      val nI = length safeIs + 1;
    1.74 -      val nE = length safeEs;
    1.75 +      val nI = Item_Net.length safeIs + 1;
    1.76 +      val nE = Item_Net.length safeEs;
    1.77        val _ = warn_claset context th cs;
    1.78      in
    1.79        CS
    1.80 -       {safeIs  = th::safeIs,
    1.81 +       {safeIs = Item_Net.update th safeIs,
    1.82          safe0_netpair = insert (nI,nE) (safe0_rls, []) safe0_netpair,
    1.83          safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair,
    1.84          safeEs = safeEs,
    1.85 @@ -361,12 +359,12 @@
    1.86        val th' = classical_rule (flat_rule th);
    1.87        val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
    1.88          List.partition (fn rl => nprems_of rl=1) [th'];
    1.89 -      val nI = length safeIs;
    1.90 -      val nE = length safeEs + 1;
    1.91 +      val nI = Item_Net.length safeIs;
    1.92 +      val nE = Item_Net.length safeEs + 1;
    1.93        val _ = warn_claset context th cs;
    1.94      in
    1.95        CS
    1.96 -       {safeEs  = th::safeEs,
    1.97 +       {safeEs = Item_Net.update th safeEs,
    1.98          safe0_netpair = insert (nI,nE) ([], safe0_rls) safe0_netpair,
    1.99          safep_netpair = insert (nI,nE) ([], safep_rls) safep_netpair,
   1.100          safeIs = safeIs,
   1.101 @@ -391,12 +389,12 @@
   1.102    else
   1.103      let
   1.104        val th' = flat_rule th;
   1.105 -      val nI = length hazIs + 1;
   1.106 -      val nE = length hazEs;
   1.107 +      val nI = Item_Net.length hazIs + 1;
   1.108 +      val nE = Item_Net.length hazEs;
   1.109        val _ = warn_claset context th cs;
   1.110      in
   1.111        CS
   1.112 -       {hazIs = th :: hazIs,
   1.113 +       {hazIs = Item_Net.update th hazIs,
   1.114          haz_netpair = insert (nI, nE) ([th'], []) haz_netpair,
   1.115          dup_netpair = insert (nI, nE) ([dup_intr th'], []) dup_netpair,
   1.116          safeIs = safeIs,
   1.117 @@ -420,12 +418,12 @@
   1.118    else
   1.119      let
   1.120        val th' = classical_rule (flat_rule th);
   1.121 -      val nI = length hazIs;
   1.122 -      val nE = length hazEs + 1;
   1.123 +      val nI = Item_Net.length hazIs;
   1.124 +      val nE = Item_Net.length hazEs + 1;
   1.125        val _ = warn_claset context th cs;
   1.126      in
   1.127        CS
   1.128 -       {hazEs = th :: hazEs,
   1.129 +       {hazEs = Item_Net.update th hazEs,
   1.130          haz_netpair = insert (nI, nE) ([], [th']) haz_netpair,
   1.131          dup_netpair = insert (nI, nE) ([], [dup_elim th']) dup_netpair,
   1.132          safeIs = safeIs,
   1.133 @@ -450,7 +448,7 @@
   1.134  fun delSI th
   1.135      (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   1.136        safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   1.137 -  if mem_thm safeIs th then
   1.138 +  if Item_Net.member safeIs th then
   1.139      let
   1.140        val th' = flat_rule th;
   1.141        val (safe0_rls, safep_rls) = List.partition Thm.no_prems [th'];
   1.142 @@ -458,7 +456,7 @@
   1.143        CS
   1.144         {safe0_netpair = delete (safe0_rls, []) safe0_netpair,
   1.145          safep_netpair = delete (safep_rls, []) safep_netpair,
   1.146 -        safeIs = rem_thm th safeIs,
   1.147 +        safeIs = Item_Net.remove th safeIs,
   1.148          safeEs = safeEs,
   1.149          hazIs = hazIs,
   1.150          hazEs = hazEs,
   1.151 @@ -473,7 +471,7 @@
   1.152  fun delSE th
   1.153      (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   1.154        safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   1.155 -  if mem_thm safeEs th then
   1.156 +  if Item_Net.member safeEs th then
   1.157      let
   1.158        val th' = classical_rule (flat_rule th);
   1.159        val (safe0_rls, safep_rls) = List.partition (fn rl => nprems_of rl = 1) [th'];
   1.160 @@ -482,7 +480,7 @@
   1.161         {safe0_netpair = delete ([], safe0_rls) safe0_netpair,
   1.162          safep_netpair = delete ([], safep_rls) safep_netpair,
   1.163          safeIs = safeIs,
   1.164 -        safeEs = rem_thm th safeEs,
   1.165 +        safeEs = Item_Net.remove th safeEs,
   1.166          hazIs = hazIs,
   1.167          hazEs = hazEs,
   1.168          swrappers = swrappers,
   1.169 @@ -496,14 +494,14 @@
   1.170  fun delI context th
   1.171      (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   1.172        safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   1.173 -  if mem_thm hazIs th then
   1.174 +  if Item_Net.member hazIs th then
   1.175      let val th' = flat_rule th in
   1.176        CS
   1.177         {haz_netpair = delete ([th'], []) haz_netpair,
   1.178          dup_netpair = delete ([dup_intr th'], []) dup_netpair,
   1.179          safeIs = safeIs,
   1.180          safeEs = safeEs,
   1.181 -        hazIs = rem_thm th hazIs,
   1.182 +        hazIs = Item_Net.remove th hazIs,
   1.183          hazEs = hazEs,
   1.184          swrappers = swrappers,
   1.185          uwrappers = uwrappers,
   1.186 @@ -518,7 +516,7 @@
   1.187  fun delE th
   1.188      (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   1.189        safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   1.190 -  if mem_thm hazEs th then
   1.191 +  if Item_Net.member hazEs th then
   1.192      let val th' = classical_rule (flat_rule th) in
   1.193        CS
   1.194         {haz_netpair = delete ([], [th']) haz_netpair,
   1.195 @@ -526,7 +524,7 @@
   1.196          safeIs = safeIs,
   1.197          safeEs = safeEs,
   1.198          hazIs = hazIs,
   1.199 -        hazEs = rem_thm th hazEs,
   1.200 +        hazEs = Item_Net.remove th hazEs,
   1.201          swrappers = swrappers,
   1.202          uwrappers = uwrappers,
   1.203          safe0_netpair = safe0_netpair,
   1.204 @@ -538,9 +536,9 @@
   1.205  (*Delete ALL occurrences of "th" in the claset (perhaps from several lists)*)
   1.206  fun delrule context th (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}) =
   1.207    let val th' = Tactic.make_elim th in
   1.208 -    if mem_thm safeIs th orelse mem_thm safeEs th orelse
   1.209 -      mem_thm hazIs th orelse mem_thm hazEs th orelse
   1.210 -      mem_thm safeEs th' orelse mem_thm hazEs th'
   1.211 +    if Item_Net.member safeIs th orelse Item_Net.member safeEs th orelse
   1.212 +      Item_Net.member hazIs th orelse Item_Net.member hazEs th orelse
   1.213 +      Item_Net.member safeEs th' orelse Item_Net.member hazEs th'
   1.214      then delSI th (delSE th (delI context th (delE th (delSE th' (delE th' cs)))))
   1.215      else (warn_thm context "Undeclared classical rule\n" th; cs)
   1.216    end;
   1.217 @@ -570,28 +568,24 @@
   1.218  
   1.219  (* merge_cs *)
   1.220  
   1.221 -(*Merge works by adding all new rules of the 2nd claset into the 1st claset.
   1.222 -  Merging the term nets may look more efficient, but the rather delicate
   1.223 -  treatment of priority might get muddled up.*)
   1.224 +(*Merge works by adding all new rules of the 2nd claset into the 1st claset,
   1.225 +  in order to preserve priorities reliably.*)
   1.226 +
   1.227 +fun merge_thms add thms1 thms2 =
   1.228 +  fold_rev (fn thm => if Item_Net.member thms1 thm then I else add thm) (Item_Net.content thms2);
   1.229 +
   1.230  fun merge_cs (cs as CS {safeIs, safeEs, hazIs, hazEs, ...},
   1.231      cs' as CS {safeIs = safeIs2, safeEs = safeEs2, hazIs = hazIs2, hazEs = hazEs2,
   1.232        swrappers, uwrappers, ...}) =
   1.233    if pointer_eq (cs, cs') then cs
   1.234    else
   1.235 -    let
   1.236 -      val safeIs' = fold rem_thm safeIs safeIs2;
   1.237 -      val safeEs' = fold rem_thm safeEs safeEs2;
   1.238 -      val hazIs' = fold rem_thm hazIs hazIs2;
   1.239 -      val hazEs' = fold rem_thm hazEs hazEs2;
   1.240 -    in
   1.241 -      cs
   1.242 -      |> fold_rev (addSI NONE NONE) safeIs'
   1.243 -      |> fold_rev (addSE NONE NONE) safeEs'
   1.244 -      |> fold_rev (addI NONE NONE) hazIs'
   1.245 -      |> fold_rev (addE NONE NONE) hazEs'
   1.246 -      |> map_swrappers (fn ws => AList.merge (op =) (K true) (ws, swrappers))
   1.247 -      |> map_uwrappers (fn ws => AList.merge (op =) (K true) (ws, uwrappers))
   1.248 -    end;
   1.249 +    cs
   1.250 +    |> merge_thms (addSI NONE NONE) safeIs safeIs2
   1.251 +    |> merge_thms (addSE NONE NONE) safeEs safeEs2
   1.252 +    |> merge_thms (addI NONE NONE) hazIs hazIs2
   1.253 +    |> merge_thms (addE NONE NONE) hazEs hazEs2
   1.254 +    |> map_swrappers (fn ws => AList.merge (op =) (K true) (ws, swrappers))
   1.255 +    |> map_uwrappers (fn ws => AList.merge (op =) (K true) (ws, uwrappers));
   1.256  
   1.257  
   1.258  (* data *)
   1.259 @@ -617,7 +611,7 @@
   1.260  fun print_claset ctxt =
   1.261    let
   1.262      val {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...} = rep_claset_of ctxt;
   1.263 -    val pretty_thms = map (Display.pretty_thm ctxt);
   1.264 +    val pretty_thms = map (Display.pretty_thm ctxt) o Item_Net.content;
   1.265    in
   1.266      [Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs),
   1.267        Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs),