the splitter is now defined as a functor
authoroheimb
Wed Aug 12 16:21:18 1998 +0200 (1998-08-12)
changeset 5304c133f16febc7
parent 5303 22029546d109
child 5305 513925de8962
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
src/FOL/simpdata.ML
src/FOLP/simpdata.ML
src/HOL/simpdata.ML
src/Provers/splitter.ML
     1.1 --- a/src/FOL/simpdata.ML	Wed Aug 12 16:20:49 1998 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Wed Aug 12 16:21:18 1998 +0200
     1.3 @@ -60,21 +60,6 @@
     1.4  
     1.5  fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
     1.6  
     1.7 -(*Make atomic rewrite rules*)
     1.8 -fun atomize r =
     1.9 -  case concl_of r of
    1.10 -    Const("Trueprop",_) $ p =>
    1.11 -      (case p of
    1.12 -         Const("op -->",_)$_$_ => atomize(r RS mp)
    1.13 -       | Const("op &",_)$_$_   => atomize(r RS conjunct1) @
    1.14 -                                  atomize(r RS conjunct2)
    1.15 -       | Const("All",_)$_      => atomize(r RS spec)
    1.16 -       | Const("True",_)       => []    (*True is DELETED*)
    1.17 -       | Const("False",_)      => []    (*should False do something?*)
    1.18 -       | _                     => [r])
    1.19 -  | _ => [r];
    1.20 -
    1.21 -
    1.22  val P_iff_F = int_prove_fun "~P ==> (P <-> False)";
    1.23  val iff_reflection_F = P_iff_F RS iff_reflection;
    1.24  
    1.25 @@ -89,6 +74,28 @@
    1.26    | _ $ (Const("Not",_)$_)      => th RS iff_reflection_F
    1.27    | _                           => th RS iff_reflection_T;
    1.28  
    1.29 +val mksimps_pairs =
    1.30 +  [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
    1.31 +   ("All", [spec]), ("True", []), ("False", [])];
    1.32 +
    1.33 +(* FIXME: move to Provers/simplifier.ML
    1.34 +val mk_atomize:      (string * thm list) list -> thm -> thm list
    1.35 +*)
    1.36 +(* FIXME: move to Provers/simplifier.ML*)
    1.37 +fun mk_atomize pairs =
    1.38 +  let fun atoms th =
    1.39 +        (case concl_of th of
    1.40 +           Const("Trueprop",_) $ p =>
    1.41 +             (case head_of p of
    1.42 +                Const(a,_) =>
    1.43 +                  (case assoc(pairs,a) of
    1.44 +                     Some(rls) => flat (map atoms ([th] RL rls))
    1.45 +                   | None => [th])
    1.46 +              | _ => [th])
    1.47 +         | _ => [th])
    1.48 +  in atoms end;
    1.49 +
    1.50 +fun mksimps pairs = (map mk_meta_eq o mk_atomize pairs o gen_all);
    1.51  
    1.52  (*** Classical laws ***)
    1.53  
    1.54 @@ -230,22 +237,32 @@
    1.55  
    1.56  (*** Case splitting ***)
    1.57  
    1.58 -qed_goal "meta_iffD" IFOL.thy "[| P==Q; Q |] ==> P"
    1.59 -        (fn [prem1,prem2] => [rewtac prem1, rtac prem2 1]);
    1.60 -
    1.61 -local val mktac = mk_case_split_tac meta_iffD
    1.62 -in
    1.63 -fun split_tac splits = mktac (map mk_meta_eq splits)
    1.64 -end;
    1.65 +val meta_eq_to_iff = prove_goal IFOL.thy "x==y ==> x<->y"
    1.66 +  (fn [prem] => [rewtac prem, rtac iffI 1, atac 1, atac 1]);
    1.67  
    1.68 -local val mktac = mk_case_split_inside_tac meta_iffD
    1.69 -in
    1.70 -fun split_inside_tac splits = mktac (map mk_meta_eq splits)
    1.71 -end;
    1.72 +structure SplitterData =
    1.73 +  struct
    1.74 +  structure Simplifier = Simplifier
    1.75 +  val mk_meta_eq     = mk_meta_eq
    1.76 +  val meta_eq_to_iff = meta_eq_to_iff
    1.77 +  val iffD           = iffD2
    1.78 +  val disjE          = disjE
    1.79 +  val conjE          = conjE
    1.80 +  val exE            = exE
    1.81 +  val contrapos      = contrapos
    1.82 +  val contrapos2     = contrapos2
    1.83 +  val notnotD        = notnotD
    1.84 +  end;
    1.85  
    1.86 -val split_asm_tac = mk_case_split_asm_tac split_tac 
    1.87 -			(disjE,conjE,exE,contrapos,contrapos2,notnotD);
    1.88 +structure Splitter = SplitterFun(SplitterData);
    1.89  
    1.90 +val split_tac        = Splitter.split_tac;
    1.91 +val split_inside_tac = Splitter.split_inside_tac;
    1.92 +val split_asm_tac    = Splitter.split_asm_tac;
    1.93 +val addsplits        = Splitter.addsplits;
    1.94 +val delsplits        = Splitter.delsplits;
    1.95 +val Addsplits        = Splitter.Addsplits;
    1.96 +val Delsplits        = Splitter.Delsplits;
    1.97  
    1.98  
    1.99  (*** Standard simpsets ***)
   1.100 @@ -264,35 +281,6 @@
   1.101  fun Addcongs congs = (simpset_ref() := simpset() addcongs congs);
   1.102  fun Delcongs congs = (simpset_ref() := simpset() delcongs congs);
   1.103  
   1.104 -(** FIXME: this is a PATCH until similar code in Provers/splitter is
   1.105 -    generalized **)
   1.106 -
   1.107 -fun split_format_err() = error("Wrong format for split rule");
   1.108 -
   1.109 -fun split_thm_info thm =
   1.110 -  (case concl_of thm of
   1.111 -     Const("Trueprop",_) $ (Const("op <->", _)$(Var _$t)$c) =>
   1.112 -        (case strip_comb t of
   1.113 -           (Const(a,_),_) => (a,case c of (Const("Not",_)$_)=> true |_=> false)
   1.114 -         | _              => split_format_err())
   1.115 -   | _ => split_format_err());
   1.116 -
   1.117 -infix 4 addsplits delsplits;
   1.118 -fun ss addsplits splits =
   1.119 -  let fun addsplit (ss,split) =
   1.120 -        let val (name,asm) = split_thm_info split 
   1.121 -        in ss addloop ("split "^ name ^ (if asm then " asm" else ""),
   1.122 -		       (if asm then split_asm_tac else split_tac) [split]) end
   1.123 -  in foldl addsplit (ss,splits) end;
   1.124 -
   1.125 -fun ss delsplits splits =
   1.126 -  let fun delsplit(ss,split) =
   1.127 -        let val (name,asm) = split_thm_info split 
   1.128 -        in ss delloop ("split "^ name ^ (if asm then " asm" else "")) end
   1.129 -  in foldl delsplit (ss,splits) end;
   1.130 -
   1.131 -fun Addsplits splits = (simpset_ref() := simpset() addsplits splits);
   1.132 -fun Delsplits splits = (simpset_ref() := simpset() delsplits splits);
   1.133  
   1.134  val IFOL_simps =
   1.135     [refl RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @ 
   1.136 @@ -312,7 +300,9 @@
   1.137                              addsimprocs [defALL_regroup,defEX_regroup]
   1.138  			    setSSolver   safe_solver
   1.139  			    setSolver  unsafe_solver
   1.140 -			    setmksimps (map mk_meta_eq o atomize o gen_all);
   1.141 +			    setmksimps (mksimps mksimps_pairs);
   1.142 +
   1.143 +
   1.144  
   1.145  (*intuitionistic simprules only*)
   1.146  val IFOL_ss = FOL_basic_ss addsimps (IFOL_simps @ int_ex_simps @ int_all_simps)
   1.147 @@ -336,20 +326,6 @@
   1.148  
   1.149  (*** integration of simplifier with classical reasoner ***)
   1.150  
   1.151 -(* rot_eq_tac rotates the first equality premise of subgoal i to the front,
   1.152 -   fails if there is no equaliy or if an equality is already at the front *)
   1.153 -local
   1.154 -  fun is_eq (Const ("Trueprop", _) $ (Const("op ="  ,_) $ _ $ _)) = true
   1.155 -    | is_eq (Const ("Trueprop", _) $ (Const("op <->",_) $ _ $ _)) = true
   1.156 -    | is_eq _ = false;
   1.157 -  val find_eq = find_index is_eq;
   1.158 -in
   1.159 -val rot_eq_tac = 
   1.160 -     SUBGOAL (fn (Bi,i) => let val n = find_eq (Logic.strip_assums_hyp Bi) in
   1.161 -		if n>0 then rotate_tac n i else no_tac end)
   1.162 -end;
   1.163 -
   1.164 -
   1.165  structure Clasimp = ClasimpFun
   1.166   (structure Simplifier = Simplifier and Classical = Cla and Blast = Blast
   1.167    val op addcongs = op addcongs and op delcongs = op delcongs
     2.1 --- a/src/FOLP/simpdata.ML	Wed Aug 12 16:20:49 1998 +0200
     2.2 +++ b/src/FOLP/simpdata.ML	Wed Aug 12 16:21:18 1998 +0200
     2.3 @@ -73,16 +73,25 @@
     2.4      | _ $ (Const("Not",_)$_) $ _ => th RS not_P_imp_P_iff_F 
     2.5      | _ => make_iff_T th;
     2.6  
     2.7 -fun atomize th = case concl_of th of (*The operator below is "Proof $ P $ p"*)
     2.8 -      _ $ (Const("op -->",_) $ _ $ _) $ _ => atomize(th RS mp)
     2.9 -    | _ $ (Const("op &",_) $ _ $ _) $ _ => atomize(th RS conjunct1) @
    2.10 -                                       atomize(th RS conjunct2)
    2.11 -    | _ $ (Const("All",_) $ _) $ _ => atomize(th RS spec)
    2.12 -    | _ $ (Const("True",_)) $ _ => []
    2.13 -    | _ $ (Const("False",_)) $ _ => []
    2.14 -    | _ => [th];
    2.15 +
    2.16 +val mksimps_pairs =
    2.17 +  [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
    2.18 +   ("All", [spec]), ("True", []), ("False", [])];
    2.19  
    2.20 -fun mk_rew_rules th = map mk_eq (atomize th);
    2.21 +fun mk_atomize pairs =
    2.22 +  let fun atoms th =
    2.23 +        (case concl_of th of
    2.24 +           Const("Trueprop",_) $ p =>
    2.25 +             (case head_of p of
    2.26 +                Const(a,_) =>
    2.27 +                  (case assoc(pairs,a) of
    2.28 +                     Some(rls) => flat (map atoms ([th] RL rls))
    2.29 +                   | None => [th])
    2.30 +              | _ => [th])
    2.31 +         | _ => [th])
    2.32 +  in atoms end;
    2.33 +
    2.34 +fun mk_rew_rules th = map mk_eq (mk_atomize mksimps_pairs th);
    2.35  
    2.36  (*destruct function for analysing equations*)
    2.37  fun dest_red(_ $ (red $ lhs $ rhs) $ _) = (red,lhs,rhs)
     3.1 --- a/src/HOL/simpdata.ML	Wed Aug 12 16:20:49 1998 +0200
     3.2 +++ b/src/HOL/simpdata.ML	Wed Aug 12 16:21:18 1998 +0200
     3.3 @@ -3,7 +3,7 @@
     3.4      Author:     Tobias Nipkow
     3.5      Copyright   1991  University of Cambridge
     3.6  
     3.7 -Instantiation of the generic simplifier.
     3.8 +Instantiation of the generic simplifier for HOL.
     3.9  *)
    3.10  
    3.11  section "Simplifier";
    3.12 @@ -56,6 +56,7 @@
    3.13  fun DelIffs thms = store_clasimp ((claset (), simpset ()) delIffs thms);
    3.14  end;
    3.15  
    3.16 +
    3.17  qed_goal "meta_eq_to_obj_eq" HOL.thy "x==y ==> x=y"
    3.18    (fn [prem] => [rewtac prem, rtac refl 1]);
    3.19  
    3.20 @@ -69,32 +70,19 @@
    3.21    val not_P_imp_P_iff_F = prover "~P --> (P = False)" RS mp;
    3.22    val not_P_imp_P_eq_False = not_P_imp_P_iff_F RS eq_reflection;
    3.23  
    3.24 -  fun atomize pairs =
    3.25 -    let fun atoms th =
    3.26 -          (case concl_of th of
    3.27 -             Const("Trueprop",_) $ p =>
    3.28 -               (case head_of p of
    3.29 -                  Const(a,_) =>
    3.30 -                    (case assoc(pairs,a) of
    3.31 -                       Some(rls) => flat (map atoms ([th] RL rls))
    3.32 -                     | None => [th])
    3.33 -                | _ => [th])
    3.34 -           | _ => [th])
    3.35 -    in atoms end;
    3.36 -
    3.37 -  fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
    3.38 -
    3.39  in
    3.40  
    3.41 -  fun mk_meta_eq r = r RS eq_reflection;
    3.42 +  fun meta_eq r = r RS eq_reflection;
    3.43 +
    3.44 +  fun mk_meta_eq th = case concl_of th of
    3.45 +          Const("==",_)$_$_       => th
    3.46 +      |   _$(Const("op =",_)$_$_) => meta_eq th
    3.47 +      |   _$(Const("Not",_)$_)    => th RS not_P_imp_P_eq_False
    3.48 +      |   _                       => th RS P_imp_P_eq_True;
    3.49 +  (* last 2 lines requires all formulae to be of the from Trueprop(.) *)
    3.50 +
    3.51    fun mk_meta_eq_True r = Some(r RS meta_eq_to_obj_eq RS P_imp_P_eq_True);
    3.52  
    3.53 -  fun mk_meta_eq_simp r = case concl_of r of
    3.54 -          Const("==",_)$_$_ => r
    3.55 -      |   _$(Const("op =",_)$lhs$rhs) => mk_meta_eq r
    3.56 -      |   _$(Const("Not",_)$_) => r RS not_P_imp_P_eq_False
    3.57 -      |   _ => r RS P_imp_P_eq_True;
    3.58 -  (* last 2 lines requires all formulae to be of the from Trueprop(.) *)
    3.59  
    3.60  val simp_thms = map prover
    3.61   [ "(x=x) = True",
    3.62 @@ -122,7 +110,7 @@
    3.63  infix 4 addcongs delcongs;
    3.64  
    3.65  fun mk_meta_cong rl =
    3.66 -  standard(mk_meta_eq(replicate (nprems_of rl) meta_eq_to_obj_eq MRS rl))
    3.67 +  standard(meta_eq(replicate (nprems_of rl) meta_eq_to_obj_eq MRS rl))
    3.68    handle THM _ =>
    3.69    error("Premises and conclusion of congruence rules must be =-equalities");
    3.70  
    3.71 @@ -133,8 +121,6 @@
    3.72  fun Addcongs congs = (simpset_ref() := simpset() addcongs congs);
    3.73  fun Delcongs congs = (simpset_ref() := simpset() delcongs congs);
    3.74  
    3.75 -fun mksimps pairs = map mk_meta_eq_simp o atomize pairs o gen_all;
    3.76 -
    3.77  val imp_cong = impI RSN
    3.78      (2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
    3.79          (fn _=> [Blast_tac 1]) RS mp RS mp);
    3.80 @@ -249,9 +235,6 @@
    3.81  
    3.82  prove "eq_sym_conv" "(x=y) = (y=x)";
    3.83  
    3.84 -qed_goalw "o_apply" HOL.thy [o_def] "(f o g) x = f (g x)"
    3.85 - (K [rtac refl 1]);
    3.86 -
    3.87  
    3.88  (** if-then-else rules **)
    3.89  
    3.90 @@ -261,12 +244,9 @@
    3.91  qed_goalw "if_False" HOL.thy [if_def] "(if False then x else y) = y"
    3.92   (K [Blast_tac 1]);
    3.93  
    3.94 -qed_goal "if_P" HOL.thy "P ==> (if P then x else y) = x"
    3.95 - (fn [prem] => [ stac (prem RS eqTrueI) 1, rtac if_True 1 ]);
    3.96 -(*
    3.97 -qed_goal "if_not_P" HOL.thy "~P ==> (if P then x else y) = y"
    3.98 - (fn [prem] => [ stac (prem RS not_P_imp_P_iff_F) 1, rtac if_False 1 ]);
    3.99 -*)
   3.100 +qed_goalw "if_P" HOL.thy [if_def] "!!P. P ==> (if P then x else y) = x"
   3.101 + (K [Blast_tac 1]);
   3.102 +
   3.103  qed_goalw "if_not_P" HOL.thy [if_def] "!!P. ~P ==> (if P then x else y) = y"
   3.104   (K [Blast_tac 1]);
   3.105  
   3.106 @@ -284,6 +264,12 @@
   3.107      (K [stac split_if 1,
   3.108  	Blast_tac 1]);
   3.109  
   3.110 +qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"
   3.111 +  (K [stac split_if 1, Blast_tac 1]);
   3.112 +
   3.113 +qed_goal "if_eq_cancel" HOL.thy "(if x = y then y else x) = x"
   3.114 +  (K [stac split_if 1, Blast_tac 1]);
   3.115 +
   3.116  (*This form is useful for expanding IFs on the RIGHT of the ==> symbol*)
   3.117  qed_goal "if_bool_eq_conj" HOL.thy
   3.118      "(if P then Q else R) = ((P-->Q) & (~P-->R))"
   3.119 @@ -339,42 +325,29 @@
   3.120  
   3.121  (*** Case splitting ***)
   3.122  
   3.123 -local val mktac = mk_case_split_tac (meta_eq_to_obj_eq RS iffD2)
   3.124 -in
   3.125 -fun split_tac splits = mktac (map mk_meta_eq splits)
   3.126 -end;
   3.127 -
   3.128 -local val mktac = mk_case_split_inside_tac (meta_eq_to_obj_eq RS iffD2)
   3.129 -in
   3.130 -fun split_inside_tac splits = mktac (map mk_meta_eq splits)
   3.131 -end;
   3.132 -
   3.133 -val split_asm_tac = mk_case_split_asm_tac split_tac 
   3.134 -			(disjE,conjE,exE,contrapos,contrapos2,notnotD);
   3.135 -
   3.136 -infix 4 addsplits delsplits;
   3.137 +structure SplitterData =
   3.138 +  struct
   3.139 +  structure Simplifier = Simplifier
   3.140 +  val mk_meta_eq     = mk_meta_eq
   3.141 +  val meta_eq_to_iff = meta_eq_to_obj_eq
   3.142 +  val iffD           = iffD2
   3.143 +  val disjE          = disjE
   3.144 +  val conjE          = conjE
   3.145 +  val exE            = exE
   3.146 +  val contrapos      = contrapos
   3.147 +  val contrapos2     = contrapos2
   3.148 +  val notnotD        = notnotD
   3.149 +  end;
   3.150  
   3.151 -fun ss addsplits splits =
   3.152 -  let fun addsplit (ss,split) =
   3.153 -        let val (name,asm) = split_thm_info split 
   3.154 -        in ss addloop ("split "^ name ^ (if asm then " asm" else ""),
   3.155 -		       (if asm then split_asm_tac else split_tac) [split]) end
   3.156 -  in foldl addsplit (ss,splits) end;
   3.157 +structure Splitter = SplitterFun(SplitterData);
   3.158  
   3.159 -fun ss delsplits splits =
   3.160 -  let fun delsplit(ss,split) =
   3.161 -        let val (name,asm) = split_thm_info split 
   3.162 -        in ss delloop ("split "^ name ^ (if asm then " asm" else "")) end
   3.163 -  in foldl delsplit (ss,splits) end;
   3.164 -
   3.165 -fun Addsplits splits = (simpset_ref() := simpset() addsplits splits);
   3.166 -fun Delsplits splits = (simpset_ref() := simpset() delsplits splits);
   3.167 -
   3.168 -qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"
   3.169 -  (K [split_tac [split_if] 1, Blast_tac 1]);
   3.170 -
   3.171 -qed_goal "if_eq_cancel" HOL.thy "(if x = y then y else x) = x"
   3.172 -  (K [split_tac [split_if] 1, Blast_tac 1]);
   3.173 +val split_tac        = Splitter.split_tac;
   3.174 +val split_inside_tac = Splitter.split_inside_tac;
   3.175 +val split_asm_tac    = Splitter.split_asm_tac;
   3.176 +val addsplits        = Splitter.addsplits;
   3.177 +val delsplits        = Splitter.delsplits;
   3.178 +val Addsplits        = Splitter.Addsplits;
   3.179 +val Delsplits        = Splitter.Delsplits;
   3.180  
   3.181  (** 'if' congruence rules: neither included by default! *)
   3.182  
   3.183 @@ -402,11 +375,32 @@
   3.184    rewriting by "(P|Q --> R) = ((P-->R)&(Q-->R))" might be justified on the
   3.185    grounds that it allows simplification of R in the two cases.*)
   3.186  
   3.187 +fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
   3.188 +
   3.189  val mksimps_pairs =
   3.190    [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
   3.191     ("All", [spec]), ("True", []), ("False", []),
   3.192     ("If", [if_bool_eq_conj RS iffD1])];
   3.193  
   3.194 +(* FIXME: move to Provers/simplifier.ML
   3.195 +val mk_atomize:      (string * thm list) list -> thm -> thm list
   3.196 +*)
   3.197 +(* FIXME: move to Provers/simplifier.ML*)
   3.198 +fun mk_atomize pairs =
   3.199 +  let fun atoms th =
   3.200 +        (case concl_of th of
   3.201 +           Const("Trueprop",_) $ p =>
   3.202 +             (case head_of p of
   3.203 +                Const(a,_) =>
   3.204 +                  (case assoc(pairs,a) of
   3.205 +                     Some(rls) => flat (map atoms ([th] RL rls))
   3.206 +                   | None => [th])
   3.207 +              | _ => [th])
   3.208 +         | _ => [th])
   3.209 +  in atoms end;
   3.210 +
   3.211 +fun mksimps pairs = (map mk_meta_eq o mk_atomize pairs o gen_all);
   3.212 +
   3.213  fun unsafe_solver prems = FIRST'[resolve_tac (reflexive_thm::TrueI::refl::prems),
   3.214  				 atac, etac FalseE];
   3.215  (*No premature instantiation of variables during simplification*)
   3.216 @@ -424,9 +418,9 @@
   3.217       ([triv_forall_equality, (* prunes params *)
   3.218         True_implies_equals, (* prune asms `True' *)
   3.219         if_True, if_False, if_cancel, if_eq_cancel,
   3.220 -       o_apply, imp_disjL, conj_assoc, disj_assoc,
   3.221 +       imp_disjL, conj_assoc, disj_assoc,
   3.222         de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_imp,
   3.223 -       disj_not1, not_all, not_ex, cases_simp]
   3.224 +       disj_not1, not_all, not_ex, cases_simp, Eps_eq]
   3.225       @ ex_simps @ all_simps @ simp_thms)
   3.226       addsimprocs [defALL_regroup,defEX_regroup]
   3.227       addcongs [imp_cong]
   3.228 @@ -436,9 +430,6 @@
   3.229    "f(if c then x else y) = (if c then f x else f y)" 
   3.230    (K [simp_tac (HOL_ss setloop (split_tac [split_if])) 1]);
   3.231  
   3.232 -qed_goalw "o_assoc" HOL.thy [o_def] "f o (g o h) = f o g o h"
   3.233 -  (K [rtac ext 1, rtac refl 1]);
   3.234 -
   3.235  
   3.236  (*For expand_case_tac*)
   3.237  val prems = goal HOL.thy "[| P ==> Q(True); ~P ==> Q(False) |] ==> Q(P)";
   3.238 @@ -462,19 +453,6 @@
   3.239  
   3.240  (*** integration of simplifier with classical reasoner ***)
   3.241  
   3.242 -(* rot_eq_tac rotates the first equality premise of subgoal i to the front,
   3.243 -   fails if there is no equaliy or if an equality is already at the front *)
   3.244 -local
   3.245 -  fun is_eq (Const ("Trueprop", _) $ (Const("op ="  ,_) $ _ $ _)) = true
   3.246 -    | is_eq _ = false;
   3.247 -  val find_eq = find_index is_eq;
   3.248 -in
   3.249 -val rot_eq_tac = 
   3.250 -     SUBGOAL (fn (Bi,i) => let val n = find_eq (Logic.strip_assums_hyp Bi) in
   3.251 -		if n>0 then rotate_tac n i else no_tac end)
   3.252 -end;
   3.253 -
   3.254 -
   3.255  structure Clasimp = ClasimpFun
   3.256   (structure Simplifier = Simplifier and Classical = Classical and Blast = Blast
   3.257    val op addcongs = op addcongs and op delcongs = op delcongs
     4.1 --- a/src/Provers/splitter.ML	Wed Aug 12 16:20:49 1998 +0200
     4.2 +++ b/src/Provers/splitter.ML	Wed Aug 12 16:21:18 1998 +0200
     4.3 @@ -4,23 +4,57 @@
     4.4      Copyright   1995  TU Munich
     4.5  
     4.6  Generic case-splitter, suitable for most logics.
     4.7 -
     4.8 -Use:
     4.9 -
    4.10 -val split_tac = mk_case_split_tac iffD;
    4.11 -
    4.12 -by(split_tac splits i);
    4.13 -
    4.14 -where splits = [P(elim(...)) == rhs, ...]
    4.15 -      iffD  = [| P <-> Q; Q |] ==> P (* is called iffD2 in HOL *)
    4.16 -
    4.17  *)
    4.18  
    4.19 -local
    4.20 +infix 4 addsplits delsplits;
    4.21 +
    4.22 +signature SPLITTER_DATA =
    4.23 +sig
    4.24 +  structure Simplifier: SIMPLIFIER
    4.25 +  val mk_meta_eq    : thm -> thm
    4.26 +  val meta_eq_to_iff: thm (* "x == y ==> x = y"                    *)
    4.27 +  val iffD          : thm (* "[| P = Q; Q |] ==> P"                *)
    4.28 +  val disjE         : thm (* "[| P | Q; P ==> R; Q ==> R |] ==> R" *)
    4.29 +  val conjE         : thm (* "[| P & Q; [| P; Q |] ==> R |] ==> R" *)
    4.30 +  val exE           : thm (* "[|  x. P x; !!x. P x ==> Q |] ==> Q" *)
    4.31 +  val contrapos     : thm (* "[| ~ Q; P ==> Q |] ==> ~ P"          *)
    4.32 +  val contrapos2    : thm (* "[| Q; ~ P ==> ~ Q |] ==> P"          *)
    4.33 +  val notnotD       : thm (* "~ ~ P ==> P"                         *)
    4.34 +end
    4.35 +
    4.36 +signature SPLITTER =
    4.37 +sig
    4.38 +  type simpset
    4.39 +  val split_tac       : thm list -> int -> tactic
    4.40 +  val split_inside_tac: thm list -> int -> tactic
    4.41 +  val split_asm_tac   : thm list -> int -> tactic
    4.42 +  val addsplits       : simpset * thm list -> simpset
    4.43 +  val delsplits       : simpset * thm list -> simpset
    4.44 +  val Addsplits       : thm list -> unit
    4.45 +  val Delsplits       : thm list -> unit
    4.46 +end;
    4.47 +
    4.48 +functor SplitterFun(Data: SPLITTER_DATA): SPLITTER =
    4.49 +struct 
    4.50 +
    4.51 +type simpset = Data.Simplifier.simpset;
    4.52 +
    4.53 +val Const ("==>", _) $ (Const ("Trueprop", _) $
    4.54 +         (Const (const_not, _) $ _    )) $ _ = #prop (rep_thm(Data.notnotD));
    4.55 +
    4.56 +val Const ("==>", _) $ (Const ("Trueprop", _) $
    4.57 +         (Const (const_or , _) $ _ $ _)) $ _ = #prop (rep_thm(Data.disjE));
    4.58  
    4.59  fun split_format_err() = error("Wrong format for split rule");
    4.60  
    4.61 -fun mk_case_split_tac_2 iffD order =
    4.62 +fun split_thm_info thm = case concl_of (Data.mk_meta_eq thm) of
    4.63 +     Const("==", _)$(Var _$t)$c =>
    4.64 +        (case strip_comb t of
    4.65 +           (Const(a,_),_) => (a,case c of (Const(s,_)$_)=>s=const_not|_=> false)
    4.66 +         | _              => split_format_err())
    4.67 +   | _ => split_format_err();
    4.68 +
    4.69 +fun mk_case_split_tac order =
    4.70  let
    4.71  
    4.72  
    4.73 @@ -30,9 +64,10 @@
    4.74     [| !! x. Q(x)==R(x) ; P(R) == C |] ==> P(Q)==C
    4.75  
    4.76  *************************************************************)
    4.77 - 
    4.78 +
    4.79 +val meta_iffD = Data.meta_eq_to_iff RS Data.iffD;
    4.80  val lift =
    4.81 -  let val ct = read_cterm (#sign(rep_thm iffD))
    4.82 +  let val ct = read_cterm (#sign(rep_thm Data.iffD))
    4.83             ("[| !!x::'b::logic. Q(x) == R(x) |] ==> \
    4.84              \P(%x. Q(x)) == P(%x. R(x))::'a::logic",propT)
    4.85    in prove_goalw_cterm [] ct
    4.86 @@ -253,7 +288,8 @@
    4.87  
    4.88  fun split_tac [] i = no_tac
    4.89    | split_tac splits i =
    4.90 -  let fun const(thm) =
    4.91 +  let val splits = map Data.mk_meta_eq splits;
    4.92 +      fun const(thm) =
    4.93              (case concl_of thm of _$(t as _$lhs)$_ =>
    4.94                 (case strip_comb lhs of (Const(a,_),args) =>
    4.95                    (a,(thm,fastype_of t,length args))
    4.96 @@ -274,72 +310,70 @@
    4.97                                      lift_split_tac])
    4.98              end
    4.99    in COND (has_fewer_prems i) no_tac 
   4.100 -          (rtac iffD i THEN lift_split_tac)
   4.101 +          (rtac meta_iffD i THEN lift_split_tac)
   4.102    end;
   4.103  
   4.104  in split_tac end;
   4.105  
   4.106 -(* FIXME: this junk is only FOL/HOL specific and should therefore not go here!*)
   4.107 -(* split_thm_info is used in FOL/simpdata.ML and HOL/simpdata.ML *)
   4.108 -fun split_thm_info thm =
   4.109 -  (case concl_of thm of
   4.110 -     Const("Trueprop",_) $ (Const("op =", _)$(Var _$t)$c) =>
   4.111 -        (case strip_comb t of
   4.112 -           (Const(a,_),_) => (a,case c of (Const("Not",_)$_)=> true |_=> false)
   4.113 -         | _              => split_format_err())
   4.114 -   | _ => split_format_err());
   4.115 +
   4.116 +val split_tac        = mk_case_split_tac              int_ord;
   4.117  
   4.118 -fun mk_case_split_asm_tac split_tac 
   4.119 -			  (disjE,conjE,exE,contrapos,contrapos2,notnotD) = 
   4.120 -let
   4.121 +val split_inside_tac = mk_case_split_tac (rev_order o int_ord);
   4.122 +
   4.123  
   4.124  (*****************************************************************************
   4.125     The split-tactic for premises
   4.126     
   4.127     splits : list of split-theorems to be tried
   4.128 -   i      : number of subgoal the tactic should be applied to
   4.129 -*****************************************************************************)
   4.130 -
   4.131 +****************************************************************************)
   4.132  fun split_asm_tac []     = K no_tac
   4.133    | split_asm_tac splits = 
   4.134 +
   4.135    let val cname_list = map (fst o split_thm_info) splits;
   4.136        fun is_case (a,_) = a mem cname_list;
   4.137        fun tac (t,i) = 
   4.138  	  let val n = find_index (exists_Const is_case) 
   4.139  				 (Logic.strip_assums_hyp t);
   4.140  	      fun first_prem_is_disj (Const ("==>", _) $ (Const ("Trueprop", _)
   4.141 -				 $ (Const ("op |", _) $ _ $ _ )) $ _ ) = true
   4.142 +				 $ (Const (s, _) $ _ $ _ )) $ _ ) = (s=const_or)
   4.143  	      |   first_prem_is_disj (Const("all",_)$Abs(_,_,t)) = 
   4.144  					first_prem_is_disj t
   4.145  	      |   first_prem_is_disj _ = false;
   4.146  	      fun flat_prems_tac i = SUBGOAL (fn (t,i) => 
   4.147 -				   (if first_prem_is_disj t
   4.148 -				    then EVERY[etac disjE i, rotate_tac ~1 i,
   4.149 -					       rotate_tac ~1  (i+1),
   4.150 -					       flat_prems_tac (i+1)]
   4.151 -				    else all_tac) 
   4.152 -				   THEN REPEAT (eresolve_tac [conjE,exE] i)
   4.153 -				   THEN REPEAT (dresolve_tac [notnotD]   i)) i;
   4.154 +			   (if first_prem_is_disj t
   4.155 +			    then EVERY[etac Data.disjE i,rotate_tac ~1 i,
   4.156 +				       rotate_tac ~1  (i+1),
   4.157 +				       flat_prems_tac (i+1)]
   4.158 +			    else all_tac) 
   4.159 +			   THEN REPEAT (eresolve_tac [Data.conjE,Data.exE] i)
   4.160 +			   THEN REPEAT (dresolve_tac [Data.notnotD]   i)) i;
   4.161  	  in if n<0 then no_tac else DETERM (EVERY'
   4.162 -		[rotate_tac n, etac contrapos2,
   4.163 +		[rotate_tac n, etac Data.contrapos2,
   4.164  		 split_tac splits, 
   4.165 -		 rotate_tac ~1, etac contrapos, rotate_tac ~1, 
   4.166 +		 rotate_tac ~1, etac Data.contrapos, rotate_tac ~1, 
   4.167  		 flat_prems_tac] i)
   4.168  	  end;
   4.169    in SUBGOAL tac
   4.170    end;
   4.171  
   4.172 -in split_asm_tac end;
   4.173 +fun split_name name asm = "split " ^ name ^ (if asm then " asm" else "");
   4.174  
   4.175 -
   4.176 -in
   4.177 +fun ss addsplits splits =
   4.178 +  let fun addsplit (ss,split) =
   4.179 +        let val (name,asm) = split_thm_info split
   4.180 +        in Data.Simplifier.addloop(ss,(split_name name asm,
   4.181 +		       (if asm then split_asm_tac else split_tac) [split])) end
   4.182 +  in foldl addsplit (ss,splits) end;
   4.183  
   4.184 -val split_thm_info = split_thm_info;
   4.185 -
   4.186 -fun mk_case_split_tac iffD = mk_case_split_tac_2 iffD int_ord;
   4.187 +fun ss delsplits splits =
   4.188 +  let fun delsplit(ss,split) =
   4.189 +        let val (name,asm) = split_thm_info split
   4.190 +        in Data.Simplifier.delloop(ss,split_name name asm)
   4.191 +  end in foldl delsplit (ss,splits) end;
   4.192  
   4.193 -fun mk_case_split_inside_tac iffD = mk_case_split_tac_2 iffD (rev_order o int_ord);
   4.194 -
   4.195 -val mk_case_split_asm_tac = mk_case_split_asm_tac;
   4.196 +fun Addsplits splits = (Data.Simplifier.simpset_ref() := 
   4.197 +			Data.Simplifier.simpset() addsplits splits);
   4.198 +fun Delsplits splits = (Data.Simplifier.simpset_ref() := 
   4.199 +			Data.Simplifier.simpset() delsplits splits);
   4.200  
   4.201  end;