src/FOL/simpdata.ML
changeset 5304 c133f16febc7
parent 5220 07f80f447b27
child 5307 6a699d5cdef4
     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