src/Provers/splitter.ML
changeset 5304 c133f16febc7
parent 4930 89271bc4e7ed
child 5437 f68b9d225942
     1.1 --- a/src/Provers/splitter.ML	Wed Aug 12 16:20:49 1998 +0200
     1.2 +++ b/src/Provers/splitter.ML	Wed Aug 12 16:21:18 1998 +0200
     1.3 @@ -4,23 +4,57 @@
     1.4      Copyright   1995  TU Munich
     1.5  
     1.6  Generic case-splitter, suitable for most logics.
     1.7 -
     1.8 -Use:
     1.9 -
    1.10 -val split_tac = mk_case_split_tac iffD;
    1.11 -
    1.12 -by(split_tac splits i);
    1.13 -
    1.14 -where splits = [P(elim(...)) == rhs, ...]
    1.15 -      iffD  = [| P <-> Q; Q |] ==> P (* is called iffD2 in HOL *)
    1.16 -
    1.17  *)
    1.18  
    1.19 -local
    1.20 +infix 4 addsplits delsplits;
    1.21 +
    1.22 +signature SPLITTER_DATA =
    1.23 +sig
    1.24 +  structure Simplifier: SIMPLIFIER
    1.25 +  val mk_meta_eq    : thm -> thm
    1.26 +  val meta_eq_to_iff: thm (* "x == y ==> x = y"                    *)
    1.27 +  val iffD          : thm (* "[| P = Q; Q |] ==> P"                *)
    1.28 +  val disjE         : thm (* "[| P | Q; P ==> R; Q ==> R |] ==> R" *)
    1.29 +  val conjE         : thm (* "[| P & Q; [| P; Q |] ==> R |] ==> R" *)
    1.30 +  val exE           : thm (* "[|  x. P x; !!x. P x ==> Q |] ==> Q" *)
    1.31 +  val contrapos     : thm (* "[| ~ Q; P ==> Q |] ==> ~ P"          *)
    1.32 +  val contrapos2    : thm (* "[| Q; ~ P ==> ~ Q |] ==> P"          *)
    1.33 +  val notnotD       : thm (* "~ ~ P ==> P"                         *)
    1.34 +end
    1.35 +
    1.36 +signature SPLITTER =
    1.37 +sig
    1.38 +  type simpset
    1.39 +  val split_tac       : thm list -> int -> tactic
    1.40 +  val split_inside_tac: thm list -> int -> tactic
    1.41 +  val split_asm_tac   : thm list -> int -> tactic
    1.42 +  val addsplits       : simpset * thm list -> simpset
    1.43 +  val delsplits       : simpset * thm list -> simpset
    1.44 +  val Addsplits       : thm list -> unit
    1.45 +  val Delsplits       : thm list -> unit
    1.46 +end;
    1.47 +
    1.48 +functor SplitterFun(Data: SPLITTER_DATA): SPLITTER =
    1.49 +struct 
    1.50 +
    1.51 +type simpset = Data.Simplifier.simpset;
    1.52 +
    1.53 +val Const ("==>", _) $ (Const ("Trueprop", _) $
    1.54 +         (Const (const_not, _) $ _    )) $ _ = #prop (rep_thm(Data.notnotD));
    1.55 +
    1.56 +val Const ("==>", _) $ (Const ("Trueprop", _) $
    1.57 +         (Const (const_or , _) $ _ $ _)) $ _ = #prop (rep_thm(Data.disjE));
    1.58  
    1.59  fun split_format_err() = error("Wrong format for split rule");
    1.60  
    1.61 -fun mk_case_split_tac_2 iffD order =
    1.62 +fun split_thm_info thm = case concl_of (Data.mk_meta_eq thm) of
    1.63 +     Const("==", _)$(Var _$t)$c =>
    1.64 +        (case strip_comb t of
    1.65 +           (Const(a,_),_) => (a,case c of (Const(s,_)$_)=>s=const_not|_=> false)
    1.66 +         | _              => split_format_err())
    1.67 +   | _ => split_format_err();
    1.68 +
    1.69 +fun mk_case_split_tac order =
    1.70  let
    1.71  
    1.72  
    1.73 @@ -30,9 +64,10 @@
    1.74     [| !! x. Q(x)==R(x) ; P(R) == C |] ==> P(Q)==C
    1.75  
    1.76  *************************************************************)
    1.77 - 
    1.78 +
    1.79 +val meta_iffD = Data.meta_eq_to_iff RS Data.iffD;
    1.80  val lift =
    1.81 -  let val ct = read_cterm (#sign(rep_thm iffD))
    1.82 +  let val ct = read_cterm (#sign(rep_thm Data.iffD))
    1.83             ("[| !!x::'b::logic. Q(x) == R(x) |] ==> \
    1.84              \P(%x. Q(x)) == P(%x. R(x))::'a::logic",propT)
    1.85    in prove_goalw_cterm [] ct
    1.86 @@ -253,7 +288,8 @@
    1.87  
    1.88  fun split_tac [] i = no_tac
    1.89    | split_tac splits i =
    1.90 -  let fun const(thm) =
    1.91 +  let val splits = map Data.mk_meta_eq splits;
    1.92 +      fun const(thm) =
    1.93              (case concl_of thm of _$(t as _$lhs)$_ =>
    1.94                 (case strip_comb lhs of (Const(a,_),args) =>
    1.95                    (a,(thm,fastype_of t,length args))
    1.96 @@ -274,72 +310,70 @@
    1.97                                      lift_split_tac])
    1.98              end
    1.99    in COND (has_fewer_prems i) no_tac 
   1.100 -          (rtac iffD i THEN lift_split_tac)
   1.101 +          (rtac meta_iffD i THEN lift_split_tac)
   1.102    end;
   1.103  
   1.104  in split_tac end;
   1.105  
   1.106 -(* FIXME: this junk is only FOL/HOL specific and should therefore not go here!*)
   1.107 -(* split_thm_info is used in FOL/simpdata.ML and HOL/simpdata.ML *)
   1.108 -fun split_thm_info thm =
   1.109 -  (case concl_of thm of
   1.110 -     Const("Trueprop",_) $ (Const("op =", _)$(Var _$t)$c) =>
   1.111 -        (case strip_comb t of
   1.112 -           (Const(a,_),_) => (a,case c of (Const("Not",_)$_)=> true |_=> false)
   1.113 -         | _              => split_format_err())
   1.114 -   | _ => split_format_err());
   1.115 +
   1.116 +val split_tac        = mk_case_split_tac              int_ord;
   1.117  
   1.118 -fun mk_case_split_asm_tac split_tac 
   1.119 -			  (disjE,conjE,exE,contrapos,contrapos2,notnotD) = 
   1.120 -let
   1.121 +val split_inside_tac = mk_case_split_tac (rev_order o int_ord);
   1.122 +
   1.123  
   1.124  (*****************************************************************************
   1.125     The split-tactic for premises
   1.126     
   1.127     splits : list of split-theorems to be tried
   1.128 -   i      : number of subgoal the tactic should be applied to
   1.129 -*****************************************************************************)
   1.130 -
   1.131 +****************************************************************************)
   1.132  fun split_asm_tac []     = K no_tac
   1.133    | split_asm_tac splits = 
   1.134 +
   1.135    let val cname_list = map (fst o split_thm_info) splits;
   1.136        fun is_case (a,_) = a mem cname_list;
   1.137        fun tac (t,i) = 
   1.138  	  let val n = find_index (exists_Const is_case) 
   1.139  				 (Logic.strip_assums_hyp t);
   1.140  	      fun first_prem_is_disj (Const ("==>", _) $ (Const ("Trueprop", _)
   1.141 -				 $ (Const ("op |", _) $ _ $ _ )) $ _ ) = true
   1.142 +				 $ (Const (s, _) $ _ $ _ )) $ _ ) = (s=const_or)
   1.143  	      |   first_prem_is_disj (Const("all",_)$Abs(_,_,t)) = 
   1.144  					first_prem_is_disj t
   1.145  	      |   first_prem_is_disj _ = false;
   1.146  	      fun flat_prems_tac i = SUBGOAL (fn (t,i) => 
   1.147 -				   (if first_prem_is_disj t
   1.148 -				    then EVERY[etac disjE i, rotate_tac ~1 i,
   1.149 -					       rotate_tac ~1  (i+1),
   1.150 -					       flat_prems_tac (i+1)]
   1.151 -				    else all_tac) 
   1.152 -				   THEN REPEAT (eresolve_tac [conjE,exE] i)
   1.153 -				   THEN REPEAT (dresolve_tac [notnotD]   i)) i;
   1.154 +			   (if first_prem_is_disj t
   1.155 +			    then EVERY[etac Data.disjE i,rotate_tac ~1 i,
   1.156 +				       rotate_tac ~1  (i+1),
   1.157 +				       flat_prems_tac (i+1)]
   1.158 +			    else all_tac) 
   1.159 +			   THEN REPEAT (eresolve_tac [Data.conjE,Data.exE] i)
   1.160 +			   THEN REPEAT (dresolve_tac [Data.notnotD]   i)) i;
   1.161  	  in if n<0 then no_tac else DETERM (EVERY'
   1.162 -		[rotate_tac n, etac contrapos2,
   1.163 +		[rotate_tac n, etac Data.contrapos2,
   1.164  		 split_tac splits, 
   1.165 -		 rotate_tac ~1, etac contrapos, rotate_tac ~1, 
   1.166 +		 rotate_tac ~1, etac Data.contrapos, rotate_tac ~1, 
   1.167  		 flat_prems_tac] i)
   1.168  	  end;
   1.169    in SUBGOAL tac
   1.170    end;
   1.171  
   1.172 -in split_asm_tac end;
   1.173 +fun split_name name asm = "split " ^ name ^ (if asm then " asm" else "");
   1.174  
   1.175 -
   1.176 -in
   1.177 +fun ss addsplits splits =
   1.178 +  let fun addsplit (ss,split) =
   1.179 +        let val (name,asm) = split_thm_info split
   1.180 +        in Data.Simplifier.addloop(ss,(split_name name asm,
   1.181 +		       (if asm then split_asm_tac else split_tac) [split])) end
   1.182 +  in foldl addsplit (ss,splits) end;
   1.183  
   1.184 -val split_thm_info = split_thm_info;
   1.185 -
   1.186 -fun mk_case_split_tac iffD = mk_case_split_tac_2 iffD int_ord;
   1.187 +fun ss delsplits splits =
   1.188 +  let fun delsplit(ss,split) =
   1.189 +        let val (name,asm) = split_thm_info split
   1.190 +        in Data.Simplifier.delloop(ss,split_name name asm)
   1.191 +  end in foldl delsplit (ss,splits) end;
   1.192  
   1.193 -fun mk_case_split_inside_tac iffD = mk_case_split_tac_2 iffD (rev_order o int_ord);
   1.194 -
   1.195 -val mk_case_split_asm_tac = mk_case_split_asm_tac;
   1.196 +fun Addsplits splits = (Data.Simplifier.simpset_ref() := 
   1.197 +			Data.Simplifier.simpset() addsplits splits);
   1.198 +fun Delsplits splits = (Data.Simplifier.simpset_ref() := 
   1.199 +			Data.Simplifier.simpset() delsplits splits);
   1.200  
   1.201  end;