oheimb@4652: (* Title: Provers/clasimp.ML oheimb@4652: ID: $Id$ oheimb@4652: Author: David von Oheimb, TU Muenchen oheimb@4652: wenzelm@5219: Combination of classical reasoner and simplifier (depends on wenzelm@5219: simplifier.ML, classical.ML, blast.ML). oheimb@4652: *) oheimb@4652: oheimb@5554: infix 4 addSIs2 addSEs2 addSDs2 addIs2 addEs2 addDs2 addsimps2 delsimps2; oheimb@4652: infix 4 addSss addss; oheimb@4652: wenzelm@5219: signature CLASIMP_DATA = wenzelm@5219: sig wenzelm@5219: structure Simplifier: SIMPLIFIER wenzelm@5219: structure Classical: CLASSICAL wenzelm@5219: structure Blast: BLAST wenzelm@5219: sharing type Classical.claset = Blast.claset wenzelm@5219: end wenzelm@5219: oheimb@4652: signature CLASIMP = oheimb@4652: sig wenzelm@5219: include CLASIMP_DATA wenzelm@5219: type claset wenzelm@5219: type simpset wenzelm@5219: type clasimpset oheimb@4652: val addSIs2 : clasimpset * thm list -> clasimpset oheimb@4652: val addSEs2 : clasimpset * thm list -> clasimpset oheimb@4652: val addSDs2 : clasimpset * thm list -> clasimpset oheimb@4652: val addIs2 : clasimpset * thm list -> clasimpset oheimb@4652: val addEs2 : clasimpset * thm list -> clasimpset oheimb@4652: val addDs2 : clasimpset * thm list -> clasimpset oheimb@4652: val addsimps2 : clasimpset * thm list -> clasimpset oheimb@4652: val delsimps2 : clasimpset * thm list -> clasimpset oheimb@4652: val addSss : claset * simpset -> claset oheimb@4652: val addss : claset * simpset -> claset oheimb@5483: val CLASIMPSET :(clasimpset -> tactic) -> tactic oheimb@5483: val CLASIMPSET' :(clasimpset -> 'a -> tactic) -> 'a -> tactic oheimb@5483: val clarsimp_tac: clasimpset -> int -> tactic oheimb@5483: val Clarsimp_tac: int -> tactic oheimb@5483: val mk_auto_tac : clasimpset -> int -> int -> tactic oheimb@5483: val auto_tac : clasimpset -> tactic oheimb@5483: val Auto_tac : tactic oheimb@5483: val auto : unit -> unit oheimb@5483: val force_tac : clasimpset -> int -> tactic oheimb@5483: val Force_tac : int -> tactic oheimb@5483: val force : int -> unit oheimb@4652: end; oheimb@4652: wenzelm@5219: functor ClasimpFun(Data: CLASIMP_DATA): CLASIMP = oheimb@4652: struct oheimb@4652: wenzelm@5219: open Data; wenzelm@5219: wenzelm@5219: type claset = Classical.claset; wenzelm@5219: type simpset = Simplifier.simpset; wenzelm@5219: type clasimpset = claset * simpset; wenzelm@5219: wenzelm@5219: wenzelm@5219: (* clasimpset operations *) wenzelm@5219: wenzelm@5219: (*this interface for updating a clasimpset is rudimentary and just for wenzelm@5219: convenience for the most common cases*) wenzelm@5219: wenzelm@5219: fun pair_upd1 f ((a,b),x) = (f(a,x), b); wenzelm@5219: fun pair_upd2 f ((a,b),x) = (a, f(b,x)); wenzelm@5219: wenzelm@5219: fun op addSIs2 arg = pair_upd1 Classical.addSIs arg; wenzelm@5219: fun op addSEs2 arg = pair_upd1 Classical.addSEs arg; wenzelm@5219: fun op addSDs2 arg = pair_upd1 Classical.addSDs arg; wenzelm@5219: fun op addIs2 arg = pair_upd1 Classical.addIs arg; wenzelm@5219: fun op addEs2 arg = pair_upd1 Classical.addEs arg; wenzelm@5219: fun op addDs2 arg = pair_upd1 Classical.addDs arg; wenzelm@5219: fun op addsimps2 arg = pair_upd2 Simplifier.addsimps arg; wenzelm@5219: fun op delsimps2 arg = pair_upd2 Simplifier.delsimps arg; oheimb@4652: oheimb@4652: (*Add a simpset to a classical set!*) oheimb@4652: (*Caution: only one simpset added can be added by each of addSss and addss*) paulson@5567: fun cs addSss ss = Classical.addSaltern (cs, ("safe_asm_full_simp_tac", oheimb@5554: CHANGED o Simplifier.safe_asm_full_simp_tac ss)); paulson@5567: fun cs addss ss = Classical.addbefore (cs, ("asm_full_simp_tac", oheimb@5554: CHANGED o Simplifier.asm_full_simp_tac ss)); oheimb@4652: wenzelm@5219: (* tacticals *) wenzelm@5219: wenzelm@5219: fun CLASIMPSET tacf state = wenzelm@5219: Classical.CLASET (fn cs => Simplifier.SIMPSET (fn ss => tacf (cs, ss))) state; wenzelm@5219: wenzelm@5219: fun CLASIMPSET' tacf i state = wenzelm@5219: Classical.CLASET (fn cs => Simplifier.SIMPSET (fn ss => tacf (cs, ss) i)) state; wenzelm@4888: wenzelm@4888: oheimb@5483: fun clarsimp_tac (cs, ss) = Simplifier.safe_asm_full_simp_tac ss THEN_MAYBE' oheimb@5483: Classical.clarify_tac (cs addSss ss); oheimb@5483: fun Clarsimp_tac i = clarsimp_tac (Classical.claset(), Simplifier.simpset()) i; oheimb@5483: oheimb@5483: wenzelm@5219: (* auto_tac *) oheimb@4652: wenzelm@5219: fun blast_depth_tac cs m i thm = oheimb@5554: Blast.depth_tac cs m i thm oheimb@5554: handle Blast.TRANS s => (warning ("Blast_tac: " ^ s); Seq.empty); oheimb@5756: wenzelm@5219: (* a variant of depth_tac that avoids interference of the simplifier wenzelm@5219: with dup_step_tac when they are combined by auto_tac *) oheimb@5756: local oheimb@5756: fun slow_step_tac' cs = Classical.appWrappers cs oheimb@5756: (Classical.instp_step_tac cs APPEND' Classical.haz_step_tac cs); oheimb@5756: in fun nodup_depth_tac cs m i state = SELECT_GOAL oheimb@5756: (Classical.safe_steps_tac cs 1 THEN_ELSE oheimb@5756: (DEPTH_SOLVE (nodup_depth_tac cs m 1), oheimb@5756: Classical.inst0_step_tac cs 1 APPEND COND (K (m=0)) no_tac oheimb@5756: (slow_step_tac' cs 1 THEN DEPTH_SOLVE (nodup_depth_tac cs (m-1) 1)) oheimb@5756: )) i state; oheimb@5756: end; oheimb@4652: oheimb@4652: (*Designed to be idempotent, except if best_tac instantiates variables oheimb@4652: in some of the subgoals*) oheimb@4652: fun mk_auto_tac (cs, ss) m n = wenzelm@5219: let val cs' = cs addss ss oheimb@4652: val maintac = oheimb@5756: blast_depth_tac cs m (* fast but can't use wrappers *) oheimb@4652: ORELSE' oheimb@5756: (CHANGED o nodup_depth_tac cs' n); (* slower but more general *) wenzelm@5219: in EVERY [ALLGOALS (Simplifier.asm_full_simp_tac ss), oheimb@5525: TRY (Classical.safe_tac cs), oheimb@4652: REPEAT (FIRSTGOAL maintac), wenzelm@5219: TRY (Classical.safe_tac (cs addSss ss)), oheimb@4652: prune_params_tac] oheimb@4652: end; oheimb@4652: oheimb@4652: fun auto_tac (cs,ss) = mk_auto_tac (cs,ss) 4 2; oheimb@4652: wenzelm@5219: fun Auto_tac st = auto_tac (Classical.claset(), Simplifier.simpset()) st; oheimb@4652: oheimb@4652: fun auto () = by Auto_tac; oheimb@4652: wenzelm@5219: wenzelm@5219: (* force_tac *) wenzelm@5219: oheimb@4659: (* aimed to solve the given subgoal totally, using whatever tools possible *) oheimb@4717: fun force_tac (cs,ss) = let val cs' = cs addss ss in SELECT_GOAL (EVERY [ wenzelm@5219: Classical.clarify_tac cs' 1, wenzelm@5219: IF_UNSOLVED (Simplifier.asm_full_simp_tac ss 1), wenzelm@5219: ALLGOALS (Classical.best_tac cs')]) end; wenzelm@5219: fun Force_tac i = force_tac (Classical.claset(), Simplifier.simpset()) i; oheimb@4717: fun force i = by (Force_tac i); oheimb@4659: wenzelm@5219: oheimb@4652: end;