# HG changeset patch # User wenzelm # Date 1305287120 -7200 # Node ID a2dca9a3d0dae8995398b127217105f8f3781f0e # Parent 226962b6a6d14c27c6cd7101aac3d5799149e84c simplified clasimpset declarations -- prefer attributes; diff -r 226962b6a6d1 -r a2dca9a3d0da src/Provers/clasimp.ML --- a/src/Provers/clasimp.ML Fri May 13 10:10:44 2011 +0200 +++ b/src/Provers/clasimp.ML Fri May 13 13:45:20 2011 +0200 @@ -5,8 +5,7 @@ splitter.ML, classical.ML, blast.ML). *) -infix 4 addSIs2 addSEs2 addSDs2 addIs2 addEs2 addDs2 addsimps2 delsimps2 - addSss addss addss' addIffs delIffs; +infix 4 addSss addss addss'; signature CLASIMP_DATA = sig @@ -17,28 +16,16 @@ val notE: thm val iffD1: thm val iffD2: thm -end +end; signature CLASIMP = sig type claset type clasimpset - val get_css: Context.generic -> clasimpset - val map_css: (clasimpset -> clasimpset) -> Context.generic -> Context.generic val clasimpset_of: Proof.context -> 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 addss': claset * simpset -> claset - val addIffs: clasimpset * thm list -> clasimpset - val delIffs: clasimpset * thm list -> clasimpset val clarsimp_tac: clasimpset -> int -> tactic val mk_auto_tac: clasimpset -> int -> int -> tactic val auto_tac: clasimpset -> tactic @@ -46,7 +33,6 @@ val fast_simp_tac: clasimpset -> int -> tactic val slow_simp_tac: clasimpset -> int -> tactic val best_simp_tac: clasimpset -> int -> tactic - val attrib: (clasimpset * thm list -> clasimpset) -> attribute val iff_add: attribute val iff_add': attribute val iff_del: attribute @@ -68,40 +54,13 @@ type claset = Classical.claset; type clasimpset = claset * simpset; -fun get_css context = (Classical.get_cs context, Simplifier.get_ss context); - -fun map_css f context = - let - val (cs, ss) = get_css context; - val (cs', ss') = f (cs, Simplifier.context (Context.proof_of context) ss); - in - context - |> Classical.map_cs (K cs') - |> Simplifier.map_ss (K (Simplifier.inherit_context ss ss')) - end; - fun clasimpset_of ctxt = (Classical.claset_of ctxt, Simplifier.simpset_of ctxt); -(* clasimpset operations *) - -(*this interface for updating a clasimpset is rudimentary and just for - convenience for the most common cases*) - -fun pair_upd1 f ((a, b), x) = (f (a, x), b); -fun pair_upd2 f ((a, b), x) = (a, f (b, x)); - -fun op addSIs2 arg = pair_upd1 Classical.addSIs arg; -fun op addSEs2 arg = pair_upd1 Classical.addSEs arg; -fun op addSDs2 arg = pair_upd1 Classical.addSDs arg; -fun op addIs2 arg = pair_upd1 Classical.addIs arg; -fun op addEs2 arg = pair_upd1 Classical.addEs arg; -fun op addDs2 arg = pair_upd1 Classical.addDs arg; -fun op addsimps2 arg = pair_upd2 Simplifier.addsimps arg; -fun op delsimps2 arg = pair_upd2 Simplifier.delsimps arg; +(* simp as classical wrapper *) (*not totally safe: may instantiate unknowns that appear also in other subgoals*) -val safe_asm_full_simp_tac = Simplifier.generic_simp_tac true (true,true,true); +val safe_asm_full_simp_tac = Simplifier.generic_simp_tac true (true, true, true); (*Add a simpset to a classical set!*) (*Caution: only one simpset added can be added by each of addSss and addss*) @@ -114,58 +73,55 @@ fun cs addss' ss = Classical.addbefore (cs, ("asm_full_simp_tac", CHANGED o Simplifier.asm_lr_simp_tac ss)); + (* iffs: addition of rules to simpsets and clasets simultaneously *) +local + (*Takes (possibly conditional) 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 decls1 decls2 simp ((cs, ss), th) = - let - val n = nprems_of th; - val (elim, intro) = if n = 0 then decls1 else decls2; - val zero_rotate = zero_var_indexes o rotate_prems n; - in - (elim (intro (cs, [zero_rotate (th RS Data.iffD2)]), - [Tactic.make_elim (zero_rotate (th RS Data.iffD1))]) - handle THM _ => (elim (cs, [zero_rotate (th RS Data.notE)]) - handle THM _ => intro (cs, [th])), - simp (ss, [th])) - end; +fun app (att: attribute) th context = #1 (att (context, th)); -fun delIff delcs delss ((cs, ss), th) = +fun add_iff safe unsafe = + Thm.declaration_attribute (fn th => + let + val n = nprems_of th; + val (elim, intro) = if n = 0 then safe else unsafe; + val zero_rotate = zero_var_indexes o rotate_prems n; + in + app intro (zero_rotate (th RS Data.iffD2)) #> + app elim (Tactic.make_elim (zero_rotate (th RS Data.iffD1))) + handle THM _ => (app elim (zero_rotate (th RS Data.notE)) handle THM _ => app intro th) + end); + +fun del_iff del = Thm.declaration_attribute (fn th => let val zero_rotate = zero_var_indexes o rotate_prems (nprems_of th) in - (delcs (cs, [zero_rotate (th RS Data.iffD2), - Tactic.make_elim (zero_rotate (th RS Data.iffD1))]) - handle THM _ => (delcs (cs, [zero_rotate (th RS Data.notE)]) - handle THM _ => delcs (cs, [th])), - delss (ss, [th])) - end; - -fun modifier att (x, ths) = - fst (Library.foldl_map (Library.apply [att]) (x, rev ths)); - -val addXIs = modifier (Context_Rules.intro_query NONE); -val addXEs = modifier (Context_Rules.elim_query NONE); -val delXs = modifier Context_Rules.rule_del; + app del (zero_rotate (th RS Data.iffD2)) #> + app del (Tactic.make_elim (zero_rotate (th RS Data.iffD1))) + handle THM _ => (app del (zero_rotate (th RS Data.notE)) handle THM _ => app del th) + end); in -val op addIffs = - Library.foldl - (addIff (Classical.addSEs, Classical.addSIs) - (Classical.addEs, Classical.addIs) - Simplifier.addsimps); -val op delIffs = Library.foldl (delIff Classical.delrules Simplifier.delsimps); +val iff_add = + add_iff + (Classical.safe_elim NONE, Classical.safe_intro NONE) + (Classical.haz_elim NONE, Classical.haz_intro NONE) + #> Simplifier.simp_add; -fun addIffs_generic (x, ths) = - Library.foldl (addIff (addXEs, addXIs) (addXEs, addXIs) #1) ((x, ()), ths) |> #1; +val iff_add' = + add_iff + (Context_Rules.elim_query NONE, Context_Rules.intro_query NONE) + (Context_Rules.elim_query NONE, Context_Rules.intro_query NONE); -fun delIffs_generic (x, ths) = - Library.foldl (delIff delXs #1) ((x, ()), ths) |> #1; +val iff_del = + del_iff Classical.rule_del #> + del_iff Context_Rules.rule_del #> + Simplifier.simp_del; end; @@ -244,17 +200,10 @@ -(** access clasimpset **) +(** concrete syntax **) (* attributes *) -fun attrib f = Thm.declaration_attribute (fn th => map_css (fn css => f (css, [th]))); -fun attrib' f (x, th) = (f (x, [th]), th); - -val iff_add = attrib (op addIffs); -val iff_add' = attrib' addIffs_generic; -val iff_del = attrib (op delIffs) o attrib' delIffs_generic; - fun iff_att x = (Scan.lift (Args.del >> K iff_del || Scan.option Args.add -- Args.query >> K iff_add' ||