4

1 
(* Title: Provers/splitter


2 
ID: $Id$


3 
Author: Tobias Nipkow


4 
Copyright 1993 TU Munich


5 


6 
Generic casesplitter, suitable for most logics.


7 

0

8 
Use:


9 


10 
val split_tac = mk_case_split_tac iffD;


11 


12 
by(case_split_tac splits i);


13 


14 
where splits = [P(elim(...)) == rhs, ...]


15 
iffD = [ P <> Q; Q ] ==> P (* is called iffD2 in HOL *)


16 


17 
*)


18 


19 
fun mk_case_split_tac iffD =


20 
let


21 

927

22 
val lift = prove_goalw_cterm [] (cterm_of (sign_of (theory_of_thm iffD))


23 
(read "[ !!x::'b::logic. Q(x) == R(x) ] ==> \


24 
\P(%x.Q(x)) == P(%x.R(x))::'a::logic"))


25 
(fn [prem] => [rewtac prem, rtac reflexive_thm 1]);

4

26 

0

27 
val trlift = lift RS transitive_thm;


28 
val _ $ (Var(P,PT)$_) $ _ = concl_of trlift;


29 


30 
fun contains cmap =


31 
let fun isin i (Abs(_,_,b)) = isin 0 b


32 
 isin i (s$t) = isin (i+1) s orelse isin 0 t


33 
 isin i (Const(c,_)) = (case assoc(cmap,c) of


34 
Some(n,_) => n <= i


35 
 None => false)


36 
 isin _ _ = false


37 
in isin 0 end;


38 


39 
fun mk_context cmap Ts maxi t =


40 
let fun var (t,i) = Var(("X",i),type_of1(Ts,t))


41 


42 
fun mka((None,i,ts),t) = if contains cmap t


43 
then let val (u,T,j) = mk(t,i) in (Some(T),j,ts@[u]) end


44 
else (None,i+1,ts@[var(t,i)])


45 
 mka((some,i,ts),t) = (some,i+1,ts@[var(t,i)])


46 
and mk(t as Abs _, i) = (Bound 0,type_of1(Ts,t),i)


47 
 mk(t,i) =


48 
let val (f,ts) = strip_comb t


49 
val (Some(T),j,us) = foldl mka ((None,i,[]),ts)


50 
in (list_comb(f,us),T,j) end


51 


52 
val (u,T,_) = mk(t,maxi+1)


53 
in Abs("",T,u) end;


54 


55 
fun nth_subgoal i thm = nth_elem(i1,prems_of thm);


56 


57 
fun goal_concl i thm = Logic.strip_assums_concl(nth_subgoal i thm);


58 


59 
fun inst_lift cmap state lift i =


60 
let val sg = #sign(rep_thm state)


61 
val tsig = #tsig(Sign.rep_sg sg)


62 
val goali = nth_subgoal i state


63 
val Ts = map #2 (Logic.strip_params goali)


64 
val _ $ t $ _ = Logic.strip_assums_concl goali;


65 
val cntxt = mk_context cmap (rev Ts) (#maxidx(rep_thm lift)) t

231

66 
val cu = cterm_of sg cntxt


67 
val uT = #T(rep_cterm cu)


68 
val cP' = cterm_of sg (Var(P,uT))

0

69 
val ixnTs = Type.typ_match tsig ([],(PT,uT));

231

70 
val ixncTs = map (fn (x,y) => (x,ctyp_of sg y)) ixnTs;

0

71 
in instantiate (ixncTs, [(cP',cu)]) lift end;


72 


73 
fun splittable al i thm =


74 
let val tm = goal_concl i thm


75 
fun nobound j k (Abs(_,_,t)) = nobound j (k+1) t


76 
 nobound j k (s$t) = nobound j k s andalso nobound j k t


77 
 nobound j k (Bound n) = n < k orelse k+j <= n


78 
 nobound _ _ _ = true;


79 
fun find j (None,t) = (case t of


80 
Abs(_,_,t) => find (j+1) (None,t)


81 
 _ => let val (h,args) = strip_comb t


82 
fun no() = foldl (find j) (None,args)


83 
in case h of


84 
Const(c,_) =>


85 
(case assoc(al,c) of


86 
Some(n,thm) =>


87 
if length args < n then no()


88 
else if forall (nobound j 0) (take(n,args))


89 
then Some(thm)


90 
else no()


91 
 None => no())


92 
 _ => no()


93 
end)


94 
 find _ (some,_) = some


95 
in find 0 (None,tm) end;


96 


97 
fun split_tac [] i = no_tac


98 
 split_tac splits i =


99 
let fun const(thm) = let val _$(_$lhs)$_ = concl_of thm


100 
val (Const(a,_),args) = strip_comb lhs


101 
in (a,(length args,thm)) end


102 
val cmap = map const splits;


103 
fun lift thm = rtac (inst_lift cmap thm trlift i) i


104 
fun lift_split thm =


105 
case splittable cmap i thm of


106 
Some(split) => rtac split i


107 
 None => EVERY[STATE lift, rtac reflexive_thm (i+1),


108 
STATE lift_split]


109 
in STATE(fn thm =>


110 
if (i <= nprems_of thm) andalso contains cmap (goal_concl i thm)


111 
then EVERY[rtac iffD i, STATE lift_split]


112 
else no_tac)


113 
end;


114 


115 
in split_tac end;
