# HG changeset patch # User wenzelm # Date 931539295 -7200 # Node ID 9e2d97ef55d2bf1fb2ec963c62af0c62a96a2e57 # Parent dbeafc269f4ffbf1c2b8e3ea280f99b5dc8e5b44 type claset: added extra I/E rules; diff -r dbeafc269f4f -r 9e2d97ef55d2 src/Provers/blast.ML --- a/src/Provers/blast.ML Fri Jul 09 18:48:54 1999 +0200 +++ b/src/Provers/blast.ML Fri Jul 09 18:54:55 1999 +0200 @@ -62,10 +62,11 @@ val rep_cs : (* dependent on classical.ML *) claset -> {safeIs: thm list, safeEs: thm list, hazIs: thm list, hazEs: thm list, + xtraIs: thm list, xtraEs: thm list, swrappers: (string * wrapper) list, uwrappers: (string * wrapper) list, safe0_netpair: netpair, safep_netpair: netpair, - haz_netpair: netpair, dup_netpair: netpair} + haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: netpair} val cla_method': (claset -> int -> tactic) -> Args.src -> Proof.context -> Proof.method end; diff -r dbeafc269f4f -r 9e2d97ef55d2 src/Provers/classical.ML --- a/src/Provers/classical.ML Fri Jul 09 18:48:54 1999 +0200 +++ b/src/Provers/classical.ML Fri Jul 09 18:54:55 1999 +0200 @@ -53,10 +53,11 @@ val rep_cs: (* BLAST_DATA in blast.ML dependent on this *) claset -> {safeIs: thm list, safeEs: thm list, hazIs: thm list, hazEs: thm list, + xtraIs: thm list, xtraEs: thm list, swrappers: (string * wrapper) list, uwrappers: (string * wrapper) list, safe0_netpair: netpair, safep_netpair: netpair, - haz_netpair: netpair, dup_netpair: netpair} + haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: netpair} val merge_cs : claset * claset -> claset val addDs : claset * thm list -> claset val addEs : claset * thm list -> claset @@ -128,6 +129,9 @@ val AddSDs : thm list -> unit val AddSEs : thm list -> unit val AddSIs : thm list -> unit + val AddXDs : thm list -> unit + val AddXEs : thm list -> unit + val AddXIs : thm list -> unit val Delrules : thm list -> unit val Safe_tac : tactic val Safe_step_tac : int -> tactic @@ -147,19 +151,25 @@ val print_local_claset: Proof.context -> unit val get_local_claset: Proof.context -> claset val put_local_claset: claset -> Proof.context -> Proof.context - val haz_dest_global: theory attribute - val haz_elim_global: theory attribute - val haz_intro_global: theory attribute val safe_dest_global: theory attribute val safe_elim_global: theory attribute val safe_intro_global: theory attribute + val haz_dest_global: theory attribute + val haz_elim_global: theory attribute + val haz_intro_global: theory attribute + val xtra_dest_global: theory attribute + val xtra_elim_global: theory attribute + val xtra_intro_global: theory attribute val delrule_global: theory attribute + val safe_dest_local: Proof.context attribute + val safe_elim_local: Proof.context attribute + val safe_intro_local: Proof.context attribute val haz_dest_local: Proof.context attribute val haz_elim_local: Proof.context attribute val haz_intro_local: Proof.context attribute - val safe_dest_local: Proof.context attribute - val safe_elim_local: Proof.context attribute - val safe_intro_local: Proof.context attribute + val xtra_dest_local: Proof.context attribute + val xtra_elim_local: Proof.context attribute + val xtra_intro_local: Proof.context attribute val delrule_local: Proof.context attribute val cla_modifiers: (Args.T list -> (Proof.context attribute * Args.T list)) list val cla_method: (claset -> tactic) -> Args.src -> Proof.context -> Proof.method @@ -255,19 +265,23 @@ safeEs : thm list, (*safe elimination rules*) hazIs : thm list, (*unsafe introduction rules*) hazEs : thm list, (*unsafe elimination rules*) + xtraIs : thm list, (*extra introduction rules*) + xtraEs : thm list, (*extra elimination rules*) swrappers : (string * wrapper) list, (*for transf. 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*) + dup_netpair : netpair, (*nets for duplication*) + xtra_netpair : netpair}; (*nets for extra rules*) (*Desired invariants are safe0_netpair = build safe0_brls, safep_netpair = build safep_brls, haz_netpair = build (joinrules(hazIs, hazEs)), dup_netpair = build (joinrules(map dup_intr hazIs, - map dup_elim hazEs))} + map dup_elim hazEs)), + xtra_netpair = build (joinrules(xtraIs, xtraEs))} where build = build_netpair(Net.empty,Net.empty), safe0_brls contains all brules that solve the subgoal, and @@ -283,19 +297,24 @@ safeEs = [], hazIs = [], hazEs = [], + xtraIs = [], + xtraEs = [], swrappers = [], uwrappers = [], safe0_netpair = empty_netpair, safep_netpair = empty_netpair, haz_netpair = empty_netpair, - dup_netpair = empty_netpair}; + dup_netpair = empty_netpair, + xtra_netpair = empty_netpair}; -fun print_cs (CS {safeIs, safeEs, hazIs, hazEs, ...}) = +fun print_cs (CS {safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, ...}) = let val pretty_thms = map Display.pretty_thm in Pretty.writeln (Pretty.big_list "safe introduction rules:" (pretty_thms safeIs)); Pretty.writeln (Pretty.big_list "unsafe introduction rules:" (pretty_thms hazIs)); + Pretty.writeln (Pretty.big_list "extra introduction rules:" (pretty_thms xtraIs)); Pretty.writeln (Pretty.big_list "safe elimination rules:" (pretty_thms safeEs)); - Pretty.writeln (Pretty.big_list "unsafe elimination rules:" (pretty_thms hazEs)) + Pretty.writeln (Pretty.big_list "unsafe elimination rules:" (pretty_thms hazEs)); + Pretty.writeln (Pretty.big_list "extra elimination rules:" (pretty_thms xtraEs)) end; fun rep_cs (CS args) = args; @@ -342,7 +361,7 @@ (*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, ...}) = +fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, ...}) = if mem_thm (th, safeIs) then warning ("Rule already in claset as Safe Intr\n" ^ string_of_thm th) else if mem_thm (th, safeEs) then @@ -351,12 +370,16 @@ warning ("Rule already in claset as unsafe Intr\n" ^ string_of_thm th) else if mem_thm (th, hazEs) then warning ("Rule already in claset as unsafe Elim\n" ^ string_of_thm th) + else if mem_thm (th, xtraIs) then + warning ("Rule already in claset as extra Intr\n" ^ string_of_thm th) + else if mem_thm (th, xtraEs) then + warning ("Rule already in claset as extra Elim\n" ^ string_of_thm th) else (); (*** Safe rules ***) -fun addSI (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair}, +fun addSI (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, th) = if mem_thm (th, safeIs) then (warning ("Ignoring duplicate Safe Intr\n" ^ string_of_thm th); @@ -373,14 +396,17 @@ safeEs = safeEs, hazIs = hazIs, hazEs = hazEs, + xtraIs = xtraIs, + xtraEs = xtraEs, swrappers = swrappers, uwrappers = uwrappers, haz_netpair = haz_netpair, - dup_netpair = dup_netpair} + dup_netpair = dup_netpair, + xtra_netpair = xtra_netpair} end; -fun addSE (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair}, +fun addSE (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, th) = if mem_thm (th, safeEs) then (warning ("Ignoring duplicate Safe Elim\n" ^ string_of_thm th); @@ -397,10 +423,13 @@ safeIs = safeIs, hazIs = hazIs, hazEs = hazEs, + xtraIs = xtraIs, + xtraEs = xtraEs, swrappers = swrappers, uwrappers = uwrappers, haz_netpair = haz_netpair, - dup_netpair = dup_netpair} + dup_netpair = dup_netpair, + xtra_netpair = xtra_netpair} end; fun rev_foldl f (e, l) = foldl f (e, rev l); @@ -413,8 +442,8 @@ (*** Hazardous (unsafe) rules ***) -fun addI (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair}, +fun addI (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, th)= if mem_thm (th, hazIs) then (warning ("Ignoring duplicate unsafe Intr\n" ^ string_of_thm th); @@ -429,14 +458,17 @@ safeIs = safeIs, safeEs = safeEs, hazEs = hazEs, + xtraIs = xtraIs, + xtraEs = xtraEs, swrappers = swrappers, uwrappers = uwrappers, safe0_netpair = safe0_netpair, - safep_netpair = safep_netpair} + safep_netpair = safep_netpair, + xtra_netpair = xtra_netpair} end; -fun addE (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair}, +fun addE (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, th) = if mem_thm (th, hazEs) then (warning ("Ignoring duplicate unsafe Elim\n" ^ string_of_thm th); @@ -451,10 +483,13 @@ safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, + xtraIs = xtraIs, + xtraEs = xtraEs, swrappers = swrappers, uwrappers = uwrappers, safe0_netpair = safe0_netpair, - safep_netpair = safep_netpair} + safep_netpair = safep_netpair, + xtra_netpair = xtra_netpair} end; val op addIs = rev_foldl addI; @@ -463,6 +498,66 @@ fun cs addDs ths = cs addEs (map make_elim ths); +(*** Extra (single step) rules ***) + +fun addXI (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, + th)= + if mem_thm (th, xtraIs) then + (warning ("Ignoring duplicate extra Intr\n" ^ string_of_thm th); + cs) + else + let val nI = length xtraIs + 1 + and nE = length xtraEs + in warn_dup th cs; + CS{xtraIs = th::xtraIs, + xtra_netpair = insert (nI,nE) ([th], []) xtra_netpair, + safeIs = safeIs, + safeEs = safeEs, + hazIs = hazIs, + hazEs = hazEs, + xtraEs = xtraEs, + swrappers = swrappers, + uwrappers = uwrappers, + safe0_netpair = safe0_netpair, + safep_netpair = safep_netpair, + haz_netpair = haz_netpair, + dup_netpair = dup_netpair} + end; + +fun addXE (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, + th) = + if mem_thm (th, xtraEs) then + (warning ("Ignoring duplicate extra Elim\n" ^ string_of_thm th); + cs) + else + let val nI = length xtraIs + and nE = length xtraEs + 1 + in warn_dup th cs; + CS{xtraEs = th::xtraEs, + xtra_netpair = insert (nI,nE) ([], [th]) xtra_netpair, + safeIs = safeIs, + safeEs = safeEs, + hazIs = hazIs, + hazEs = hazEs, + xtraIs = xtraIs, + swrappers = swrappers, + uwrappers = uwrappers, + safe0_netpair = safe0_netpair, + safep_netpair = safep_netpair, + haz_netpair = haz_netpair, + dup_netpair = dup_netpair} + end; + +infix 4 addXIs addXEs addXDs; + +val op addXIs = rev_foldl addXI; +val op addXEs = rev_foldl addXE; + +fun cs addXDs ths = cs addXEs (map make_elim ths); + + (*** Deletion of rules Working out what to delete, requires repeating much of the code used to insert. @@ -471,8 +566,8 @@ ***) fun delSI th - (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) = + (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = if mem_thm (th, safeIs) then let val (safe0_rls, safep_rls) = partition (fn rl => nprems_of rl=0) [th] in CS{safe0_netpair = delete (safe0_rls, []) safe0_netpair, @@ -481,16 +576,19 @@ safeEs = safeEs, hazIs = hazIs, hazEs = hazEs, + xtraIs = xtraIs, + xtraEs = xtraEs, swrappers = swrappers, uwrappers = uwrappers, haz_netpair = haz_netpair, - dup_netpair = dup_netpair} + dup_netpair = dup_netpair, + xtra_netpair = xtra_netpair} end else cs; fun delSE th - (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) = + (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = if mem_thm (th, safeEs) then let val (safe0_rls, safep_rls) = partition (fn rl => nprems_of rl=1) [th] in CS{safe0_netpair = delete ([], safe0_rls) safe0_netpair, @@ -499,17 +597,20 @@ safeEs = rem_thm (safeEs,th), hazIs = hazIs, hazEs = hazEs, + xtraIs = xtraIs, + xtraEs = xtraEs, swrappers = swrappers, uwrappers = uwrappers, haz_netpair = haz_netpair, - dup_netpair = dup_netpair} + dup_netpair = dup_netpair, + xtra_netpair = xtra_netpair} end else cs; fun delI th - (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) = + (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = if mem_thm (th, hazIs) then CS{haz_netpair = delete ([th], []) haz_netpair, dup_netpair = delete ([dup_intr th], []) dup_netpair, @@ -517,15 +618,18 @@ safeEs = safeEs, hazIs = rem_thm (hazIs,th), hazEs = hazEs, + xtraIs = xtraIs, + xtraEs = xtraEs, swrappers = swrappers, uwrappers = uwrappers, safe0_netpair = safe0_netpair, - safep_netpair = safep_netpair} + safep_netpair = safep_netpair, + xtra_netpair = xtra_netpair} else cs; fun delE th - (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) = + (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = if mem_thm (th, hazEs) then CS{haz_netpair = delete ([], [th]) haz_netpair, dup_netpair = delete ([], [dup_elim th]) dup_netpair, @@ -533,17 +637,60 @@ safeEs = safeEs, hazIs = hazIs, hazEs = rem_thm (hazEs,th), + xtraIs = xtraIs, + xtraEs = xtraEs, + swrappers = swrappers, + uwrappers = uwrappers, + safe0_netpair = safe0_netpair, + safep_netpair = safep_netpair, + xtra_netpair = xtra_netpair} + else cs; + + +fun delXI th + (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = + if mem_thm (th, xtraIs) then + CS{xtra_netpair = delete ([th], []) xtra_netpair, + safeIs = safeIs, + safeEs = safeEs, + hazIs = hazIs, + hazEs = hazEs, + xtraIs = rem_thm (xtraIs,th), + xtraEs = xtraEs, swrappers = swrappers, uwrappers = uwrappers, safe0_netpair = safe0_netpair, - safep_netpair = safep_netpair} + safep_netpair = safep_netpair, + haz_netpair = haz_netpair, + dup_netpair = dup_netpair} + else cs; + +fun delXE th + (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = + if mem_thm (th, xtraEs) then + CS{xtra_netpair = delete ([], [th]) xtra_netpair, + safeIs = safeIs, + safeEs = safeEs, + hazIs = hazIs, + hazEs = hazEs, + xtraIs = xtraIs, + xtraEs = rem_thm (xtraEs,th), + swrappers = swrappers, + uwrappers = uwrappers, + safe0_netpair = safe0_netpair, + safep_netpair = safep_netpair, + haz_netpair = haz_netpair, + dup_netpair = dup_netpair} else cs; (*Delete ALL occurrences of "th" in the claset (perhaps from several lists)*) -fun delrule (cs as CS{safeIs, safeEs, hazIs, hazEs, ...}, th) = +fun delrule (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, ...}, th) = if mem_thm (th, safeIs) orelse mem_thm (th, safeEs) orelse - mem_thm (th, hazIs) orelse mem_thm (th, hazEs) - then delSI th (delSE th (delI th (delE th cs))) + mem_thm (th, hazIs) orelse mem_thm (th, hazEs) orelse + mem_thm (th, xtraIs) orelse mem_thm (th, xtraEs) + then delSI th (delSE th (delI th (delE th (delXI th (delXE th cs))))) else (warning ("Rule not in claset\n" ^ (string_of_thm th)); cs); @@ -552,20 +699,22 @@ (*** Modifying the wrapper tacticals ***) fun update_swrappers -(CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) f = +(CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) f = CS{safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs, + xtraIs = xtraIs, xtraEs = xtraEs, swrappers = f swrappers, uwrappers = uwrappers, safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, - haz_netpair = haz_netpair, dup_netpair = dup_netpair}; + haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair}; fun update_uwrappers -(CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) f = +(CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) f = CS{safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs, + xtraIs = xtraIs, xtraEs = xtraEs, swrappers = swrappers, uwrappers = f uwrappers, safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, - haz_netpair = haz_netpair, dup_netpair = dup_netpair}; + haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair}; (*Add/replace a safe wrapper*) @@ -617,17 +766,21 @@ Merging the term nets may look more efficient, but the rather delicate treatment of priority might get muddled up.*) fun merge_cs - (cs as CS{safeIs, safeEs, hazIs, hazEs, ...}, + (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, ...}, CS{safeIs=safeIs2, safeEs=safeEs2, hazIs=hazIs2, hazEs=hazEs2, - swrappers, uwrappers, ...}) = + xtraIs=xtraIs2, xtraEs=xtraEs2, swrappers, uwrappers, ...}) = let val safeIs' = gen_rems eq_thm (safeIs2,safeIs) val safeEs' = gen_rems eq_thm (safeEs2,safeEs) val hazIs' = gen_rems eq_thm ( hazIs2, hazIs) val hazEs' = gen_rems eq_thm ( hazEs2, hazEs) + val xtraIs' = gen_rems eq_thm (xtraIs2, xtraIs) + val xtraEs' = gen_rems eq_thm (xtraEs2, xtraEs) val cs1 = cs addSIs safeIs' addSEs safeEs' addIs hazIs' addEs hazEs' + addXIs xtraIs' + addXEs xtraEs' val cs2 = update_swrappers cs1 (fn ws => merge_alists ws swrappers); val cs3 = update_uwrappers cs2 (fn ws => merge_alists ws uwrappers); in cs3 @@ -829,6 +982,9 @@ val AddSDs = change_claset (op addSDs); val AddSEs = change_claset (op addSEs); val AddSIs = change_claset (op addSIs); +val AddXDs = change_claset (op addXDs); +val AddXEs = change_claset (op addXEs); +val AddXIs = change_claset (op addXIs); val Delrules = change_claset (op delrules); @@ -858,20 +1014,26 @@ let val cs = f (get_local_claset ctxt, [th]) in (put_local_claset cs ctxt, th) end; -val haz_dest_global = change_global_cs (op addDs); -val haz_elim_global = change_global_cs (op addEs); -val haz_intro_global = change_global_cs (op addIs); val safe_dest_global = change_global_cs (op addSDs); val safe_elim_global = change_global_cs (op addSEs); val safe_intro_global = change_global_cs (op addSIs); +val haz_dest_global = change_global_cs (op addDs); +val haz_elim_global = change_global_cs (op addEs); +val haz_intro_global = change_global_cs (op addIs); +val xtra_dest_global = change_global_cs (op addXDs); +val xtra_elim_global = change_global_cs (op addXEs); +val xtra_intro_global = change_global_cs (op addXIs); val delrule_global = change_global_cs (op delrules); +val safe_dest_local = change_local_cs (op addSDs); +val safe_elim_local = change_local_cs (op addSEs); +val safe_intro_local = change_local_cs (op addSIs); val haz_dest_local = change_local_cs (op addDs); val haz_elim_local = change_local_cs (op addEs); val haz_intro_local = change_local_cs (op addIs); -val safe_dest_local = change_local_cs (op addSDs); -val safe_elim_local = change_local_cs (op addSEs); -val safe_intro_local = change_local_cs (op addSIs); +val xtra_dest_local = change_local_cs (op addXDs); +val xtra_elim_local = change_local_cs (op addXEs); +val xtra_intro_local = change_local_cs (op addXIs); val delrule_local = change_local_cs (op delrules); @@ -905,20 +1067,21 @@ val delruleN = "delrule"; val bang = Args.$$$ "!"; +val bbang = Args.$$$ "!!"; -fun cla_att change haz safe = - Attrib.syntax (Scan.lift ((bang >> K haz || Scan.succeed safe) >> change)); +fun cla_att change xtra haz safe = Attrib.syntax + (Scan.lift ((bbang >> K xtra || bang >> K haz || Scan.succeed safe) >> change)); -fun cla_attr f g = (cla_att change_global_cs f g, cla_att change_local_cs f g); +fun cla_attr f g h = (cla_att change_global_cs f g h, cla_att change_local_cs f g h); val del_attr = (Attrib.no_args delrule_global, Attrib.no_args delrule_local); (* setup_attrs *) val setup_attrs = Attrib.add_attributes - [(destN, cla_attr (op addDs) (op addSDs), "destruction rule"), - (elimN, cla_attr (op addEs) (op addSEs), "elimination rule"), - (introN, cla_attr (op addIs) (op addSIs), "introduction rule"), + [(destN, cla_attr (op addXDs) (op addDs) (op addSDs), "destruction rule"), + (elimN, cla_attr (op addXEs) (op addEs) (op addSEs), "elimination rule"), + (introN, cla_attr (op addXIs) (op addIs) (op addSIs), "introduction rule"), (delruleN, del_attr, "delete rule")]; @@ -935,10 +1098,10 @@ in flat (map rules_of nets) end; fun find_erules [] _ = [] - | find_erules facts nets = + | find_erules (fact :: _) nets = let fun may_unify net = Net.unify_term net o Logic.strip_assums_concl o #prop o Thm.rep_thm; - fun erules_of (_, enet) = order_rules (flat (map (may_unify enet) facts)); + fun erules_of (_, enet) = order_rules (may_unify enet fact); in flat (map erules_of nets) end; @@ -960,9 +1123,9 @@ fun single_tac cs facts = let - val CS {safe0_netpair, safep_netpair, haz_netpair, dup_netpair, ...} = cs; + val CS {safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair, ...} = cs; val nets = [imp_elim_netpair, safe0_netpair, safep_netpair, - not_elim_netpair, haz_netpair, dup_netpair]; + not_elim_netpair, haz_netpair, dup_netpair, xtra_netpair]; val erules = find_erules facts nets; val tac = SUBGOAL (fn (goal, i) => @@ -994,10 +1157,13 @@ (* automatic methods *) val cla_modifiers = - [Args.$$$ destN -- bang >> K haz_dest_local, + [Args.$$$ destN -- bbang >> K xtra_dest_local, + Args.$$$ destN -- bang >> K haz_dest_local, Args.$$$ destN >> K safe_dest_local, + Args.$$$ elimN -- bbang >> K xtra_elim_local, Args.$$$ elimN -- bang >> K haz_elim_local, Args.$$$ elimN >> K safe_elim_local, + Args.$$$ introN -- bbang >> K xtra_intro_local, Args.$$$ introN -- bang >> K haz_intro_local, Args.$$$ introN >> K safe_intro_local, Args.$$$ delN >> K delrule_local];