--- a/src/Provers/splitter.ML Mon Oct 17 23:10:18 2005 +0200
+++ b/src/Provers/splitter.ML Mon Oct 17 23:10:19 2005 +0200
@@ -12,7 +12,6 @@
signature SPLITTER_DATA =
sig
- structure Simplifier: SIMPLIFIER
val mk_eq : thm -> thm
val meta_eq_to_iff: thm (* "x == y ==> x = y" *)
val iffD : thm (* "[| P = Q; Q |] ==> P" *)
@@ -26,7 +25,6 @@
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
@@ -43,10 +41,7 @@
end;
functor SplitterFun(Data: SPLITTER_DATA): SPLITTER =
-struct
-
-structure Simplifier = Data.Simplifier;
-type simpset = Simplifier.simpset;
+struct
val Const ("==>", _) $ (Const ("Trueprop", _) $
(Const (const_not, _) $ _ )) $ _ = #prop (rep_thm(Data.notnotD));
@@ -86,9 +81,9 @@
val _ $ (P $ _) $ _ = concl_of trlift;
-(************************************************************************
+(************************************************************************
Set up term for instantiation of P in the lift-theorem
-
+
Ts : types of parameters (i.e. variables bound by meta-quantifiers)
t : lefthand side of meta-equality in subgoal
the lift theorem is applied to (see select)
@@ -109,7 +104,7 @@
in Abs("", T, down (rev pos) t maxi) end;
-(************************************************************************
+(************************************************************************
Set up term for instantiation of P in the split-theorem
P(...) == rhs
@@ -151,7 +146,7 @@
n : number of arguments expected by Const(key,...)
ts : list of arguments actually found
apsns : list of tuples of the form (T,U,pos), one tuple for each
- abstraction that is encountered on the way to the position where
+ abstraction that is encountered on the way to the position where
Const(key, ...) $ ... occurs, where
T : type of the variable bound by the abstraction
U : type of the abstraction's body
@@ -166,7 +161,7 @@
comes first ! If the terms in ts don't contain variables bound
by other than meta-quantifiers, apsns is empty, because no further
lifting is required before applying the split-theorem.
-******************************************************************************)
+******************************************************************************)
fun mk_split_pack(thm, T, T', n, ts, apsns, pos, TB, t) =
if n > length ts then []
@@ -287,7 +282,7 @@
fun inst_lift Ts t (T, U, pos) state i =
let
val cert = cterm_of (sign_of_thm state);
- val cntxt = mk_cntxt Ts t pos (T --> U) (#maxidx(rep_thm trlift));
+ val cntxt = mk_cntxt Ts t pos (T --> U) (#maxidx(rep_thm trlift));
in cterm_instantiate [(cert P, cert cntxt)] trlift
end;
@@ -306,7 +301,7 @@
**************************************************************)
fun inst_split Ts t tt thm TB state i =
- let
+ let
val thm' = Thm.lift_rule (state, i) thm;
val (P, _) = strip_comb (fst (Logic.dest_equals
(Logic.strip_assums_concl (#prop (rep_thm thm')))));
@@ -319,7 +314,7 @@
(*****************************************************************************
The split-tactic
-
+
splits : list of split-theorems to be tried
i : number of subgoal the tactic should be applied to
*****************************************************************************)
@@ -350,7 +345,7 @@
rtac reflexive_thm (i+1),
lift_split_tac] state)
end
- in COND (has_fewer_prems i) no_tac
+ in COND (has_fewer_prems i) no_tac
(rtac meta_iffD i THEN lift_split_tac)
end;
@@ -364,37 +359,37 @@
(*****************************************************************************
The split-tactic for premises
-
+
splits : list of split-theorems to be tried
****************************************************************************)
fun split_asm_tac [] = K no_tac
- | split_asm_tac splits =
+ | split_asm_tac splits =
let val cname_list = map (fst o 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 (s, _) $ _ $ _ )) $ _ ) = (s=const_or)
- | first_prem_is_disj (Const("all",_)$Abs(_,_,t)) =
- first_prem_is_disj t
- | first_prem_is_disj _ = false;
+ 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 (s, _) $ _ $ _ )) $ _ ) = (s=const_or)
+ | first_prem_is_disj (Const("all",_)$Abs(_,_,t)) =
+ first_prem_is_disj t
+ | first_prem_is_disj _ = false;
(* does not work properly if the split variable is bound by a quantfier *)
- fun flat_prems_tac i = SUBGOAL (fn (t,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 Data.contrapos2,
- split_tac splits,
- rotate_tac ~1, etac Data.contrapos, rotate_tac ~1,
- flat_prems_tac] i)
- end;
+ fun flat_prems_tac i = SUBGOAL (fn (t,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 Data.contrapos2,
+ split_tac splits,
+ rotate_tac ~1, etac Data.contrapos, rotate_tac ~1,
+ flat_prems_tac] i)
+ end;
in SUBGOAL tac
end;
@@ -413,14 +408,14 @@
else enclose "(" ")" (commas (map string_of_typ Ts))) ^ s
| string_of_typ _ = "_";
-fun split_name (name, T) asm = "split " ^
+fun split_name (name, T) asm = "split " ^
(if asm then "asm " else "") ^ name ^ " :: " ^ string_of_typ T;
fun ss addsplits splits =
let fun addsplit (ss,split) =
let val (name,asm) = split_thm_info split
in Simplifier.addloop (ss, (split_name name asm,
- (if asm then split_asm_tac else split_tac) [split])) end
+ (if asm then split_asm_tac else split_tac) [split])) end
in Library.foldl addsplit (ss,splits) end;
fun ss delsplits splits =
@@ -429,10 +424,8 @@
in Simplifier.delloop (ss, split_name name asm)
end in Library.foldl delsplit (ss,splits) end;
-fun Addsplits splits = (Simplifier.simpset_ref() :=
- Simplifier.simpset() addsplits splits);
-fun Delsplits splits = (Simplifier.simpset_ref() :=
- Simplifier.simpset() delsplits splits);
+fun Addsplits splits = (change_simpset (fn ss => ss addsplits splits));
+fun Delsplits splits = (change_simpset (fn ss => ss delsplits splits));
(* attributes *)