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 

943

22 
val lift =


23 
let val ct = read_cterm (#sign(rep_thm iffD))


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


25 
\P(%x.Q(x)) == P(%x.R(x))::'a::logic",propT)


26 
in prove_goalw_cterm [] ct


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


28 
end;

4

29 

0

30 
val trlift = lift RS transitive_thm;


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


32 


33 
fun contains cmap =


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


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


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


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


38 
 None => false)


39 
 isin _ _ = false


40 
in isin 0 end;


41 


42 
fun mk_context cmap Ts maxi t =


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


44 


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


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


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


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


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


50 
 mk(t,i) =


51 
let val (f,ts) = strip_comb t


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


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


54 


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


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


57 


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


59 


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


61 


62 
fun inst_lift cmap state lift i =


63 
let val sg = #sign(rep_thm state)


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


65 
val goali = nth_subgoal i state


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


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


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

231

69 
val cu = cterm_of sg cntxt


70 
val uT = #T(rep_cterm cu)


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

0

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

231

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

0

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


75 


76 
fun splittable al i thm =


77 
let val tm = goal_concl i thm


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


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


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


81 
 nobound _ _ _ = true;


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


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


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


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


86 
in case h of


87 
Const(c,_) =>


88 
(case assoc(al,c) of


89 
Some(n,thm) =>


90 
if length args < n then no()


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


92 
then Some(thm)


93 
else no()


94 
 None => no())


95 
 _ => no()


96 
end)


97 
 find _ (some,_) = some


98 
in find 0 (None,tm) end;


99 


100 
fun split_tac [] i = no_tac


101 
 split_tac splits i =


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


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


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


105 
val cmap = map const splits;


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


107 
fun lift_split thm =


108 
case splittable cmap i thm of


109 
Some(split) => rtac split i


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


111 
STATE lift_split]


112 
in STATE(fn thm =>


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


114 
then EVERY[rtac iffD i, STATE lift_split]


115 
else no_tac)


116 
end;


117 


118 
in split_tac end;
