the splitter is now defined as a functor
moved addsplits, delsplits, Addsplits, Delsplits to Provers/splitter.ML
moved split_thm_info to Provers/splitter.ML
definined atomize via general mk_atomize
removed superfluous rot_eq_tac from simplifier.ML
HOL/simpdata.ML: renamed mk_meta_eq to meta_eq,
re-renamed mk_meta_eq_simp to mk_meta_eq
added Eps_eq to simpset
--- a/src/FOL/simpdata.ML Wed Aug 12 16:20:49 1998 +0200
+++ b/src/FOL/simpdata.ML Wed Aug 12 16:21:18 1998 +0200
@@ -60,21 +60,6 @@
fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
-(*Make atomic rewrite rules*)
-fun atomize r =
- case concl_of r of
- Const("Trueprop",_) $ p =>
- (case p of
- Const("op -->",_)$_$_ => atomize(r RS mp)
- | Const("op &",_)$_$_ => atomize(r RS conjunct1) @
- atomize(r RS conjunct2)
- | Const("All",_)$_ => atomize(r RS spec)
- | Const("True",_) => [] (*True is DELETED*)
- | Const("False",_) => [] (*should False do something?*)
- | _ => [r])
- | _ => [r];
-
-
val P_iff_F = int_prove_fun "~P ==> (P <-> False)";
val iff_reflection_F = P_iff_F RS iff_reflection;
@@ -89,6 +74,28 @@
| _ $ (Const("Not",_)$_) => th RS iff_reflection_F
| _ => th RS iff_reflection_T;
+val mksimps_pairs =
+ [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
+ ("All", [spec]), ("True", []), ("False", [])];
+
+(* FIXME: move to Provers/simplifier.ML
+val mk_atomize: (string * thm list) list -> thm -> thm list
+*)
+(* FIXME: move to Provers/simplifier.ML*)
+fun mk_atomize pairs =
+ let fun atoms th =
+ (case concl_of th of
+ Const("Trueprop",_) $ p =>
+ (case head_of p of
+ Const(a,_) =>
+ (case assoc(pairs,a) of
+ Some(rls) => flat (map atoms ([th] RL rls))
+ | None => [th])
+ | _ => [th])
+ | _ => [th])
+ in atoms end;
+
+fun mksimps pairs = (map mk_meta_eq o mk_atomize pairs o gen_all);
(*** Classical laws ***)
@@ -230,22 +237,32 @@
(*** Case splitting ***)
-qed_goal "meta_iffD" IFOL.thy "[| P==Q; Q |] ==> P"
- (fn [prem1,prem2] => [rewtac prem1, rtac prem2 1]);
-
-local val mktac = mk_case_split_tac meta_iffD
-in
-fun split_tac splits = mktac (map mk_meta_eq splits)
-end;
+val meta_eq_to_iff = prove_goal IFOL.thy "x==y ==> x<->y"
+ (fn [prem] => [rewtac prem, rtac iffI 1, atac 1, atac 1]);
-local val mktac = mk_case_split_inside_tac meta_iffD
-in
-fun split_inside_tac splits = mktac (map mk_meta_eq splits)
-end;
+structure SplitterData =
+ struct
+ structure Simplifier = Simplifier
+ val mk_meta_eq = mk_meta_eq
+ val meta_eq_to_iff = meta_eq_to_iff
+ val iffD = iffD2
+ val disjE = disjE
+ val conjE = conjE
+ val exE = exE
+ val contrapos = contrapos
+ val contrapos2 = contrapos2
+ val notnotD = notnotD
+ end;
-val split_asm_tac = mk_case_split_asm_tac split_tac
- (disjE,conjE,exE,contrapos,contrapos2,notnotD);
+structure Splitter = SplitterFun(SplitterData);
+val split_tac = Splitter.split_tac;
+val split_inside_tac = Splitter.split_inside_tac;
+val split_asm_tac = Splitter.split_asm_tac;
+val addsplits = Splitter.addsplits;
+val delsplits = Splitter.delsplits;
+val Addsplits = Splitter.Addsplits;
+val Delsplits = Splitter.Delsplits;
(*** Standard simpsets ***)
@@ -264,35 +281,6 @@
fun Addcongs congs = (simpset_ref() := simpset() addcongs congs);
fun Delcongs congs = (simpset_ref() := simpset() delcongs congs);
-(** FIXME: this is a PATCH until similar code in Provers/splitter is
- generalized **)
-
-fun split_format_err() = error("Wrong format for split rule");
-
-fun split_thm_info thm =
- (case concl_of thm of
- Const("Trueprop",_) $ (Const("op <->", _)$(Var _$t)$c) =>
- (case strip_comb t of
- (Const(a,_),_) => (a,case c of (Const("Not",_)$_)=> true |_=> false)
- | _ => split_format_err())
- | _ => split_format_err());
-
-infix 4 addsplits delsplits;
-fun ss addsplits splits =
- let fun addsplit (ss,split) =
- let val (name,asm) = split_thm_info split
- in ss addloop ("split "^ name ^ (if asm then " asm" else ""),
- (if asm then split_asm_tac else split_tac) [split]) end
- in foldl addsplit (ss,splits) end;
-
-fun ss delsplits splits =
- let fun delsplit(ss,split) =
- let val (name,asm) = split_thm_info split
- in ss delloop ("split "^ name ^ (if asm then " asm" else "")) end
- in foldl delsplit (ss,splits) end;
-
-fun Addsplits splits = (simpset_ref() := simpset() addsplits splits);
-fun Delsplits splits = (simpset_ref() := simpset() delsplits splits);
val IFOL_simps =
[refl RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @
@@ -312,7 +300,9 @@
addsimprocs [defALL_regroup,defEX_regroup]
setSSolver safe_solver
setSolver unsafe_solver
- setmksimps (map mk_meta_eq o atomize o gen_all);
+ setmksimps (mksimps mksimps_pairs);
+
+
(*intuitionistic simprules only*)
val IFOL_ss = FOL_basic_ss addsimps (IFOL_simps @ int_ex_simps @ int_all_simps)
@@ -336,20 +326,6 @@
(*** integration of simplifier with classical reasoner ***)
-(* rot_eq_tac rotates the first equality premise of subgoal i to the front,
- fails if there is no equaliy or if an equality is already at the front *)
-local
- fun is_eq (Const ("Trueprop", _) $ (Const("op =" ,_) $ _ $ _)) = true
- | is_eq (Const ("Trueprop", _) $ (Const("op <->",_) $ _ $ _)) = true
- | is_eq _ = false;
- val find_eq = find_index is_eq;
-in
-val rot_eq_tac =
- SUBGOAL (fn (Bi,i) => let val n = find_eq (Logic.strip_assums_hyp Bi) in
- if n>0 then rotate_tac n i else no_tac end)
-end;
-
-
structure Clasimp = ClasimpFun
(structure Simplifier = Simplifier and Classical = Cla and Blast = Blast
val op addcongs = op addcongs and op delcongs = op delcongs
--- a/src/FOLP/simpdata.ML Wed Aug 12 16:20:49 1998 +0200
+++ b/src/FOLP/simpdata.ML Wed Aug 12 16:21:18 1998 +0200
@@ -73,16 +73,25 @@
| _ $ (Const("Not",_)$_) $ _ => th RS not_P_imp_P_iff_F
| _ => make_iff_T th;
-fun atomize th = case concl_of th of (*The operator below is "Proof $ P $ p"*)
- _ $ (Const("op -->",_) $ _ $ _) $ _ => atomize(th RS mp)
- | _ $ (Const("op &",_) $ _ $ _) $ _ => atomize(th RS conjunct1) @
- atomize(th RS conjunct2)
- | _ $ (Const("All",_) $ _) $ _ => atomize(th RS spec)
- | _ $ (Const("True",_)) $ _ => []
- | _ $ (Const("False",_)) $ _ => []
- | _ => [th];
+
+val mksimps_pairs =
+ [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
+ ("All", [spec]), ("True", []), ("False", [])];
-fun mk_rew_rules th = map mk_eq (atomize th);
+fun mk_atomize pairs =
+ let fun atoms th =
+ (case concl_of th of
+ Const("Trueprop",_) $ p =>
+ (case head_of p of
+ Const(a,_) =>
+ (case assoc(pairs,a) of
+ Some(rls) => flat (map atoms ([th] RL rls))
+ | None => [th])
+ | _ => [th])
+ | _ => [th])
+ in atoms end;
+
+fun mk_rew_rules th = map mk_eq (mk_atomize mksimps_pairs th);
(*destruct function for analysing equations*)
fun dest_red(_ $ (red $ lhs $ rhs) $ _) = (red,lhs,rhs)
--- a/src/HOL/simpdata.ML Wed Aug 12 16:20:49 1998 +0200
+++ b/src/HOL/simpdata.ML Wed Aug 12 16:21:18 1998 +0200
@@ -3,7 +3,7 @@
Author: Tobias Nipkow
Copyright 1991 University of Cambridge
-Instantiation of the generic simplifier.
+Instantiation of the generic simplifier for HOL.
*)
section "Simplifier";
@@ -56,6 +56,7 @@
fun DelIffs thms = store_clasimp ((claset (), simpset ()) delIffs thms);
end;
+
qed_goal "meta_eq_to_obj_eq" HOL.thy "x==y ==> x=y"
(fn [prem] => [rewtac prem, rtac refl 1]);
@@ -69,32 +70,19 @@
val not_P_imp_P_iff_F = prover "~P --> (P = False)" RS mp;
val not_P_imp_P_eq_False = not_P_imp_P_iff_F RS eq_reflection;
- fun atomize pairs =
- let fun atoms th =
- (case concl_of th of
- Const("Trueprop",_) $ p =>
- (case head_of p of
- Const(a,_) =>
- (case assoc(pairs,a) of
- Some(rls) => flat (map atoms ([th] RL rls))
- | None => [th])
- | _ => [th])
- | _ => [th])
- in atoms end;
-
- fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
-
in
- fun mk_meta_eq r = r RS eq_reflection;
+ fun meta_eq r = r RS eq_reflection;
+
+ fun mk_meta_eq th = case concl_of th of
+ Const("==",_)$_$_ => th
+ | _$(Const("op =",_)$_$_) => meta_eq th
+ | _$(Const("Not",_)$_) => th RS not_P_imp_P_eq_False
+ | _ => th RS P_imp_P_eq_True;
+ (* last 2 lines requires all formulae to be of the from Trueprop(.) *)
+
fun mk_meta_eq_True r = Some(r RS meta_eq_to_obj_eq RS P_imp_P_eq_True);
- fun mk_meta_eq_simp r = case concl_of r of
- Const("==",_)$_$_ => r
- | _$(Const("op =",_)$lhs$rhs) => mk_meta_eq r
- | _$(Const("Not",_)$_) => r RS not_P_imp_P_eq_False
- | _ => r RS P_imp_P_eq_True;
- (* last 2 lines requires all formulae to be of the from Trueprop(.) *)
val simp_thms = map prover
[ "(x=x) = True",
@@ -122,7 +110,7 @@
infix 4 addcongs delcongs;
fun mk_meta_cong rl =
- standard(mk_meta_eq(replicate (nprems_of rl) meta_eq_to_obj_eq MRS rl))
+ standard(meta_eq(replicate (nprems_of rl) meta_eq_to_obj_eq MRS rl))
handle THM _ =>
error("Premises and conclusion of congruence rules must be =-equalities");
@@ -133,8 +121,6 @@
fun Addcongs congs = (simpset_ref() := simpset() addcongs congs);
fun Delcongs congs = (simpset_ref() := simpset() delcongs congs);
-fun mksimps pairs = map mk_meta_eq_simp o atomize pairs o gen_all;
-
val imp_cong = impI RSN
(2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
(fn _=> [Blast_tac 1]) RS mp RS mp);
@@ -249,9 +235,6 @@
prove "eq_sym_conv" "(x=y) = (y=x)";
-qed_goalw "o_apply" HOL.thy [o_def] "(f o g) x = f (g x)"
- (K [rtac refl 1]);
-
(** if-then-else rules **)
@@ -261,12 +244,9 @@
qed_goalw "if_False" HOL.thy [if_def] "(if False then x else y) = y"
(K [Blast_tac 1]);
-qed_goal "if_P" HOL.thy "P ==> (if P then x else y) = x"
- (fn [prem] => [ stac (prem RS eqTrueI) 1, rtac if_True 1 ]);
-(*
-qed_goal "if_not_P" HOL.thy "~P ==> (if P then x else y) = y"
- (fn [prem] => [ stac (prem RS not_P_imp_P_iff_F) 1, rtac if_False 1 ]);
-*)
+qed_goalw "if_P" HOL.thy [if_def] "!!P. P ==> (if P then x else y) = x"
+ (K [Blast_tac 1]);
+
qed_goalw "if_not_P" HOL.thy [if_def] "!!P. ~P ==> (if P then x else y) = y"
(K [Blast_tac 1]);
@@ -284,6 +264,12 @@
(K [stac split_if 1,
Blast_tac 1]);
+qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"
+ (K [stac split_if 1, Blast_tac 1]);
+
+qed_goal "if_eq_cancel" HOL.thy "(if x = y then y else x) = x"
+ (K [stac split_if 1, Blast_tac 1]);
+
(*This form is useful for expanding IFs on the RIGHT of the ==> symbol*)
qed_goal "if_bool_eq_conj" HOL.thy
"(if P then Q else R) = ((P-->Q) & (~P-->R))"
@@ -339,42 +325,29 @@
(*** Case splitting ***)
-local val mktac = mk_case_split_tac (meta_eq_to_obj_eq RS iffD2)
-in
-fun split_tac splits = mktac (map mk_meta_eq splits)
-end;
-
-local val mktac = mk_case_split_inside_tac (meta_eq_to_obj_eq RS iffD2)
-in
-fun split_inside_tac splits = mktac (map mk_meta_eq splits)
-end;
-
-val split_asm_tac = mk_case_split_asm_tac split_tac
- (disjE,conjE,exE,contrapos,contrapos2,notnotD);
-
-infix 4 addsplits delsplits;
+structure SplitterData =
+ struct
+ structure Simplifier = Simplifier
+ val mk_meta_eq = mk_meta_eq
+ val meta_eq_to_iff = meta_eq_to_obj_eq
+ val iffD = iffD2
+ val disjE = disjE
+ val conjE = conjE
+ val exE = exE
+ val contrapos = contrapos
+ val contrapos2 = contrapos2
+ val notnotD = notnotD
+ end;
-fun ss addsplits splits =
- let fun addsplit (ss,split) =
- let val (name,asm) = split_thm_info split
- in ss addloop ("split "^ name ^ (if asm then " asm" else ""),
- (if asm then split_asm_tac else split_tac) [split]) end
- in foldl addsplit (ss,splits) end;
+structure Splitter = SplitterFun(SplitterData);
-fun ss delsplits splits =
- let fun delsplit(ss,split) =
- let val (name,asm) = split_thm_info split
- in ss delloop ("split "^ name ^ (if asm then " asm" else "")) end
- in foldl delsplit (ss,splits) end;
-
-fun Addsplits splits = (simpset_ref() := simpset() addsplits splits);
-fun Delsplits splits = (simpset_ref() := simpset() delsplits splits);
-
-qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"
- (K [split_tac [split_if] 1, Blast_tac 1]);
-
-qed_goal "if_eq_cancel" HOL.thy "(if x = y then y else x) = x"
- (K [split_tac [split_if] 1, Blast_tac 1]);
+val split_tac = Splitter.split_tac;
+val split_inside_tac = Splitter.split_inside_tac;
+val split_asm_tac = Splitter.split_asm_tac;
+val addsplits = Splitter.addsplits;
+val delsplits = Splitter.delsplits;
+val Addsplits = Splitter.Addsplits;
+val Delsplits = Splitter.Delsplits;
(** 'if' congruence rules: neither included by default! *)
@@ -402,11 +375,32 @@
rewriting by "(P|Q --> R) = ((P-->R)&(Q-->R))" might be justified on the
grounds that it allows simplification of R in the two cases.*)
+fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
+
val mksimps_pairs =
[("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
("All", [spec]), ("True", []), ("False", []),
("If", [if_bool_eq_conj RS iffD1])];
+(* FIXME: move to Provers/simplifier.ML
+val mk_atomize: (string * thm list) list -> thm -> thm list
+*)
+(* FIXME: move to Provers/simplifier.ML*)
+fun mk_atomize pairs =
+ let fun atoms th =
+ (case concl_of th of
+ Const("Trueprop",_) $ p =>
+ (case head_of p of
+ Const(a,_) =>
+ (case assoc(pairs,a) of
+ Some(rls) => flat (map atoms ([th] RL rls))
+ | None => [th])
+ | _ => [th])
+ | _ => [th])
+ in atoms end;
+
+fun mksimps pairs = (map mk_meta_eq o mk_atomize pairs o gen_all);
+
fun unsafe_solver prems = FIRST'[resolve_tac (reflexive_thm::TrueI::refl::prems),
atac, etac FalseE];
(*No premature instantiation of variables during simplification*)
@@ -424,9 +418,9 @@
([triv_forall_equality, (* prunes params *)
True_implies_equals, (* prune asms `True' *)
if_True, if_False, if_cancel, if_eq_cancel,
- o_apply, imp_disjL, conj_assoc, disj_assoc,
+ imp_disjL, conj_assoc, disj_assoc,
de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_imp,
- disj_not1, not_all, not_ex, cases_simp]
+ disj_not1, not_all, not_ex, cases_simp, Eps_eq]
@ ex_simps @ all_simps @ simp_thms)
addsimprocs [defALL_regroup,defEX_regroup]
addcongs [imp_cong]
@@ -436,9 +430,6 @@
"f(if c then x else y) = (if c then f x else f y)"
(K [simp_tac (HOL_ss setloop (split_tac [split_if])) 1]);
-qed_goalw "o_assoc" HOL.thy [o_def] "f o (g o h) = f o g o h"
- (K [rtac ext 1, rtac refl 1]);
-
(*For expand_case_tac*)
val prems = goal HOL.thy "[| P ==> Q(True); ~P ==> Q(False) |] ==> Q(P)";
@@ -462,19 +453,6 @@
(*** integration of simplifier with classical reasoner ***)
-(* rot_eq_tac rotates the first equality premise of subgoal i to the front,
- fails if there is no equaliy or if an equality is already at the front *)
-local
- fun is_eq (Const ("Trueprop", _) $ (Const("op =" ,_) $ _ $ _)) = true
- | is_eq _ = false;
- val find_eq = find_index is_eq;
-in
-val rot_eq_tac =
- SUBGOAL (fn (Bi,i) => let val n = find_eq (Logic.strip_assums_hyp Bi) in
- if n>0 then rotate_tac n i else no_tac end)
-end;
-
-
structure Clasimp = ClasimpFun
(structure Simplifier = Simplifier and Classical = Classical and Blast = Blast
val op addcongs = op addcongs and op delcongs = op delcongs
--- a/src/Provers/splitter.ML Wed Aug 12 16:20:49 1998 +0200
+++ b/src/Provers/splitter.ML Wed Aug 12 16:21:18 1998 +0200
@@ -4,23 +4,57 @@
Copyright 1995 TU Munich
Generic case-splitter, suitable for most logics.
-
-Use:
-
-val split_tac = mk_case_split_tac iffD;
-
-by(split_tac splits i);
-
-where splits = [P(elim(...)) == rhs, ...]
- iffD = [| P <-> Q; Q |] ==> P (* is called iffD2 in HOL *)
-
*)
-local
+infix 4 addsplits delsplits;
+
+signature SPLITTER_DATA =
+sig
+ structure Simplifier: SIMPLIFIER
+ val mk_meta_eq : thm -> thm
+ val meta_eq_to_iff: thm (* "x == y ==> x = y" *)
+ val iffD : thm (* "[| P = Q; Q |] ==> P" *)
+ val disjE : thm (* "[| P | Q; P ==> R; Q ==> R |] ==> R" *)
+ val conjE : thm (* "[| P & Q; [| P; Q |] ==> R |] ==> R" *)
+ val exE : thm (* "[| x. P x; !!x. P x ==> Q |] ==> Q" *)
+ val contrapos : thm (* "[| ~ Q; P ==> Q |] ==> ~ P" *)
+ val contrapos2 : thm (* "[| Q; ~ P ==> ~ Q |] ==> P" *)
+ val notnotD : thm (* "~ ~ P ==> P" *)
+end
+
+signature SPLITTER =
+sig
+ type simpset
+ val split_tac : thm list -> int -> tactic
+ val split_inside_tac: thm list -> int -> tactic
+ val split_asm_tac : thm list -> int -> tactic
+ val addsplits : simpset * thm list -> simpset
+ val delsplits : simpset * thm list -> simpset
+ val Addsplits : thm list -> unit
+ val Delsplits : thm list -> unit
+end;
+
+functor SplitterFun(Data: SPLITTER_DATA): SPLITTER =
+struct
+
+type simpset = Data.Simplifier.simpset;
+
+val Const ("==>", _) $ (Const ("Trueprop", _) $
+ (Const (const_not, _) $ _ )) $ _ = #prop (rep_thm(Data.notnotD));
+
+val Const ("==>", _) $ (Const ("Trueprop", _) $
+ (Const (const_or , _) $ _ $ _)) $ _ = #prop (rep_thm(Data.disjE));
fun split_format_err() = error("Wrong format for split rule");
-fun mk_case_split_tac_2 iffD order =
+fun split_thm_info thm = case concl_of (Data.mk_meta_eq thm) of
+ Const("==", _)$(Var _$t)$c =>
+ (case strip_comb t of
+ (Const(a,_),_) => (a,case c of (Const(s,_)$_)=>s=const_not|_=> false)
+ | _ => split_format_err())
+ | _ => split_format_err();
+
+fun mk_case_split_tac order =
let
@@ -30,9 +64,10 @@
[| !! x. Q(x)==R(x) ; P(R) == C |] ==> P(Q)==C
*************************************************************)
-
+
+val meta_iffD = Data.meta_eq_to_iff RS Data.iffD;
val lift =
- let val ct = read_cterm (#sign(rep_thm iffD))
+ let val ct = read_cterm (#sign(rep_thm Data.iffD))
("[| !!x::'b::logic. Q(x) == R(x) |] ==> \
\P(%x. Q(x)) == P(%x. R(x))::'a::logic",propT)
in prove_goalw_cterm [] ct
@@ -253,7 +288,8 @@
fun split_tac [] i = no_tac
| split_tac splits i =
- let fun const(thm) =
+ let val splits = map Data.mk_meta_eq splits;
+ fun const(thm) =
(case concl_of thm of _$(t as _$lhs)$_ =>
(case strip_comb lhs of (Const(a,_),args) =>
(a,(thm,fastype_of t,length args))
@@ -274,72 +310,70 @@
lift_split_tac])
end
in COND (has_fewer_prems i) no_tac
- (rtac iffD i THEN lift_split_tac)
+ (rtac meta_iffD i THEN lift_split_tac)
end;
in split_tac end;
-(* FIXME: this junk is only FOL/HOL specific and should therefore not go here!*)
-(* split_thm_info is used in FOL/simpdata.ML and HOL/simpdata.ML *)
-fun split_thm_info thm =
- (case concl_of thm of
- Const("Trueprop",_) $ (Const("op =", _)$(Var _$t)$c) =>
- (case strip_comb t of
- (Const(a,_),_) => (a,case c of (Const("Not",_)$_)=> true |_=> false)
- | _ => split_format_err())
- | _ => split_format_err());
+
+val split_tac = mk_case_split_tac int_ord;
-fun mk_case_split_asm_tac split_tac
- (disjE,conjE,exE,contrapos,contrapos2,notnotD) =
-let
+val split_inside_tac = mk_case_split_tac (rev_order o int_ord);
+
(*****************************************************************************
The split-tactic for premises
splits : list of split-theorems to be tried
- i : number of subgoal the tactic should be applied to
-*****************************************************************************)
-
+****************************************************************************)
fun split_asm_tac [] = K no_tac
| split_asm_tac splits =
+
let val cname_list = map (fst o split_thm_info) splits;
fun is_case (a,_) = a mem cname_list;
fun tac (t,i) =
let val n = find_index (exists_Const is_case)
(Logic.strip_assums_hyp t);
fun first_prem_is_disj (Const ("==>", _) $ (Const ("Trueprop", _)
- $ (Const ("op |", _) $ _ $ _ )) $ _ ) = true
+ $ (Const (s, _) $ _ $ _ )) $ _ ) = (s=const_or)
| first_prem_is_disj (Const("all",_)$Abs(_,_,t)) =
first_prem_is_disj t
| first_prem_is_disj _ = false;
fun flat_prems_tac i = SUBGOAL (fn (t,i) =>
- (if first_prem_is_disj t
- then EVERY[etac disjE i, rotate_tac ~1 i,
- rotate_tac ~1 (i+1),
- flat_prems_tac (i+1)]
- else all_tac)
- THEN REPEAT (eresolve_tac [conjE,exE] i)
- THEN REPEAT (dresolve_tac [notnotD] i)) i;
+ (if first_prem_is_disj t
+ then EVERY[etac Data.disjE i,rotate_tac ~1 i,
+ rotate_tac ~1 (i+1),
+ flat_prems_tac (i+1)]
+ else all_tac)
+ THEN REPEAT (eresolve_tac [Data.conjE,Data.exE] i)
+ THEN REPEAT (dresolve_tac [Data.notnotD] i)) i;
in if n<0 then no_tac else DETERM (EVERY'
- [rotate_tac n, etac contrapos2,
+ [rotate_tac n, etac Data.contrapos2,
split_tac splits,
- rotate_tac ~1, etac contrapos, rotate_tac ~1,
+ rotate_tac ~1, etac Data.contrapos, rotate_tac ~1,
flat_prems_tac] i)
end;
in SUBGOAL tac
end;
-in split_asm_tac end;
+fun split_name name asm = "split " ^ name ^ (if asm then " asm" else "");
-
-in
+fun ss addsplits splits =
+ let fun addsplit (ss,split) =
+ let val (name,asm) = split_thm_info split
+ in Data.Simplifier.addloop(ss,(split_name name asm,
+ (if asm then split_asm_tac else split_tac) [split])) end
+ in foldl addsplit (ss,splits) end;
-val split_thm_info = split_thm_info;
-
-fun mk_case_split_tac iffD = mk_case_split_tac_2 iffD int_ord;
+fun ss delsplits splits =
+ let fun delsplit(ss,split) =
+ let val (name,asm) = split_thm_info split
+ in Data.Simplifier.delloop(ss,split_name name asm)
+ end in foldl delsplit (ss,splits) end;
-fun mk_case_split_inside_tac iffD = mk_case_split_tac_2 iffD (rev_order o int_ord);
-
-val mk_case_split_asm_tac = mk_case_split_asm_tac;
+fun Addsplits splits = (Data.Simplifier.simpset_ref() :=
+ Data.Simplifier.simpset() addsplits splits);
+fun Delsplits splits = (Data.Simplifier.simpset_ref() :=
+ Data.Simplifier.simpset() delsplits splits);
end;