# HG changeset patch # User wenzelm # Date 968172612 -7200 # Node ID 5c5efed691b9d44770522dc335d817f9c1426310 # Parent 2cd338998b531f81b8c682087c22e3268bb7568c added 'iff' declarations; diff -r 2cd338998b53 -r 5c5efed691b9 src/Provers/clasimp.ML --- a/src/Provers/clasimp.ML Tue Sep 05 18:49:26 2000 +0200 +++ b/src/Provers/clasimp.ML Tue Sep 05 18:50:12 2000 +0200 @@ -6,8 +6,8 @@ simplifier.ML, splitter.ML classical.ML, blast.ML). *) -infix 4 addSIs2 addSEs2 addSDs2 addIs2 addEs2 addDs2 addsimps2 delsimps2; -infix 4 addSss addss; +infix 4 addSIs2 addSEs2 addSDs2 addIs2 addEs2 addDs2 addsimps2 delsimps2 + addSss addss addIffs delIffs; signature CLASIMP_DATA = sig @@ -16,6 +16,13 @@ structure Classical: CLASSICAL structure Blast: BLAST sharing type Classical.claset = Blast.claset + val dest_Trueprop: term -> term + val not_const: term + val iff_const: term + val notE: thm + val iffD1: thm + val iffD2: thm + val cla_make_elim: thm -> thm end signature CLASIMP = @@ -24,35 +31,44 @@ type claset type simpset type clasimpset - val addSIs2 : clasimpset * thm list -> clasimpset - val addSEs2 : clasimpset * thm list -> clasimpset - val addSDs2 : clasimpset * thm list -> clasimpset - val addIs2 : clasimpset * thm list -> clasimpset - val addEs2 : clasimpset * thm list -> clasimpset - val addDs2 : clasimpset * thm list -> clasimpset - val addsimps2 : clasimpset * thm list -> clasimpset - val delsimps2 : clasimpset * thm list -> clasimpset - val addSss : claset * simpset -> claset - val addss : claset * simpset -> claset - val CLASIMPSET :(clasimpset -> tactic) -> tactic - val CLASIMPSET' :(clasimpset -> 'a -> tactic) -> 'a -> tactic + val addSIs2: clasimpset * thm list -> clasimpset + val addSEs2: clasimpset * thm list -> clasimpset + val addSDs2: clasimpset * thm list -> clasimpset + val addIs2: clasimpset * thm list -> clasimpset + val addEs2: clasimpset * thm list -> clasimpset + val addDs2: clasimpset * thm list -> clasimpset + val addsimps2: clasimpset * thm list -> clasimpset + val delsimps2: clasimpset * thm list -> clasimpset + val addSss: claset * simpset -> claset + val addss: claset * simpset -> claset + val addIffs: clasimpset * thm list -> clasimpset + val delIffs: clasimpset * thm list -> clasimpset + val AddIffs: thm list -> unit + val DelIffs: thm list -> unit + val CLASIMPSET: (clasimpset -> tactic) -> tactic + val CLASIMPSET': (clasimpset -> 'a -> tactic) -> 'a -> tactic val clarsimp_tac: clasimpset -> int -> tactic - val Clarsimp_tac: int -> tactic - val mk_auto_tac : clasimpset -> int -> int -> tactic - val auto_tac : clasimpset -> tactic - val Auto_tac : tactic - val auto : unit -> unit - val force_tac : clasimpset -> int -> tactic - val Force_tac : int -> tactic - val force : int -> unit - val fast_simp_tac : clasimpset -> int -> tactic - val slow_simp_tac : clasimpset -> int -> tactic - val best_simp_tac : clasimpset -> int -> tactic + val Clarsimp_tac: int -> tactic + val mk_auto_tac: clasimpset -> int -> int -> tactic + val auto_tac: clasimpset -> tactic + val Auto_tac: tactic + val auto: unit -> unit + val force_tac: clasimpset -> int -> tactic + val Force_tac: int -> tactic + val force: int -> unit + val fast_simp_tac: clasimpset -> int -> tactic + val slow_simp_tac: clasimpset -> int -> tactic + val best_simp_tac: clasimpset -> int -> tactic val change_global_css: (clasimpset * thm list -> clasimpset) -> theory attribute val change_local_css: (clasimpset * thm list -> clasimpset) -> Proof.context attribute val get_local_clasimpset: Proof.context -> clasimpset + val iff_add_global: theory attribute + val iff_del_global: theory attribute + val iff_add_local: Proof.context attribute + val iff_del_local: Proof.context attribute + val iff_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list val clasimp_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list - val setup : (theory -> theory) list + val setup: (theory -> theory) list end; functor ClasimpFun(Data: CLASIMP_DATA): CLASIMP = @@ -92,6 +108,56 @@ fun cs addss ss = Classical.addbefore (cs, ("asm_full_simp_tac", CHANGED o Simplifier.asm_full_simp_tac ss)); + +(* iffs: addition of rules to simpsets and clasets simultaneously *) + +(*Takes UNCONDITIONAL theorems of the form A<->B to + the Safe Intr rule B==>A and + the Safe Destruct rule A==>B. + Also ~A goes to the Safe Elim rule A ==> ?R + Failing other cases, A is added as a Safe Intr rule*) +local + +fun addIff ((cla, simp), th) = + (case dest_Trueprop (#prop (rep_thm th)) of + con $ _ $ _ => + if con = Data.iff_const then + Classical.addSDs (Classical.addSIs (cla, [zero_var_indexes (th RS Data.iffD2)]), + [zero_var_indexes (th RS Data.iffD1)]) + else Classical.addSIs (cla, [th]) + | con $ A => + if con = Data.not_const then Classical.addSEs (cla, [zero_var_indexes (th RS Data.notE)]) + else Classical.addSIs (cla, [th]) + | _ => Classical.addSIs (cla, [th]), Simplifier.addsimps (simp, [th])) + handle TERM _ => error ("iff add: theorem must be unconditional\n" ^ Display.string_of_thm th); + +fun delIff ((cla, simp), th) = + (case dest_Trueprop (#prop (rep_thm th)) of + con $ _ $ _ => + if con = Data.iff_const then + Classical.delrules (cla, [zero_var_indexes (th RS Data.iffD2), + Data.cla_make_elim (zero_var_indexes (th RS Data.iffD1))]) + else Classical.delrules (cla, [th]) + | con $ A => + if con = Data.not_const then Classical.delrules (cla, [zero_var_indexes (th RS Data.notE)]) + else Classical.delrules (cla, [th]) + | _ => Classical.delrules (cla, [th]), Simplifier.delsimps (simp, [th])) + handle TERM _ => + (warning ("iff del: ignoring conditional theorem\n" ^ string_of_thm th); (cla, simp)); + +fun store_clasimp (cla, simp) = + (Classical.claset_ref () := cla; Simplifier.simpset_ref () := simp); + +in + +val op addIffs = foldl addIff; +val op delIffs = foldl delIff; +fun AddIffs thms = store_clasimp ((Classical.claset (), Simplifier.simpset ()) addIffs thms); +fun DelIffs thms = store_clasimp ((Classical.claset (), Simplifier.simpset ()) delIffs thms); + +end; + + (* tacticals *) fun CLASIMPSET tacf state = @@ -167,7 +233,7 @@ val best_simp_tac = ADDSS Classical.best_tac; -(* change clasimpset *) +(* access clasimpset *) fun change_global_css f (thy, th) = let @@ -187,14 +253,39 @@ |> Simplifier.put_local_simpset ss'; in (ctxt', th) end; - -(* methods *) - fun get_local_clasimpset ctxt = (Classical.get_local_claset ctxt, Simplifier.get_local_simpset ctxt); + +(* attributes *) + +val iff_add_global = change_global_css (op addIffs); +val iff_del_global = change_global_css (op delIffs); +val iff_add_local = change_local_css (op addIffs); +val iff_del_local = change_local_css (op delIffs); + +val iff_attr = + (Attrib.add_del_args iff_add_global iff_del_global, + Attrib.add_del_args iff_add_local iff_del_local); + + +(* method modifiers *) + +val iffN = "iff"; +val addN = "add"; +val delN = "del"; + +val iff_modifiers = + [Args.$$$ iffN -- Args.colon >> K ((I, iff_add_local): Method.modifier), + Args.$$$ iffN -- Args.$$$ addN -- Args.colon >> K (I, iff_add_local), + Args.$$$ iffN -- Args.$$$ delN -- Args.colon >> K (I, iff_del_local)]; + val clasimp_modifiers = - Simplifier.simp_modifiers @ Splitter.split_modifiers @ Classical.cla_modifiers; + Simplifier.simp_modifiers @ Splitter.split_modifiers @ + Classical.cla_modifiers @ iff_modifiers; + + +(* methods *) fun clasimp_meth tac prems ctxt = Method.METHOD (fn facts => ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (get_local_clasimpset ctxt)); @@ -216,7 +307,9 @@ (* theory setup *) val setup = - [Method.add_methods + [Attrib.add_attributes + [("iff", iff_attr, "declare simplifier / classical rules")], + Method.add_methods [("fastsimp", clasimp_method' fast_simp_tac, "combined fast and simp"), ("slowsimp", clasimp_method' slow_simp_tac, "combined slow and simp"), ("bestsimp", clasimp_method' best_simp_tac, "combined best and simp"), @@ -224,5 +317,4 @@ ("auto", auto_args auto_meth, "auto"), ("clarsimp", clasimp_method' (CHANGED oo clarsimp_tac), "clarify simplified goal")]]; - end;