--- 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' ||