0

1 
(*** case splitting ***)


2 
(*


3 
Use:


4 


5 
val split_tac = mk_case_split_tac iffD;


6 


7 
by(case_split_tac splits i);


8 


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


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


11 


12 
*)


13 


14 
fun mk_case_split_tac iffD =


15 
let


16 


17 
val lift = prove_goal Pure.thy


18 
"[ !!x::'b::logic. Q(x) == R(x) ] ==> P(%x.Q(x)) == P(%x.R(x))::'a::logic"


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


20 
(*


21 
val iffD = prove_goal Pure.thy "[ PROP P == PROP Q; PROP Q ] ==> PROP P"


22 
(fn [p1,p2] => [rtac (equal_elim (symmetric p1) p2) 1]);


23 
*)


24 
val trlift = lift RS transitive_thm;


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


26 


27 
fun contains cmap =


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


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


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


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


32 
 None => false)


33 
 isin _ _ = false


34 
in isin 0 end;


35 


36 
fun mk_context cmap Ts maxi t =


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


38 


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


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


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


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


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


44 
 mk(t,i) =


45 
let val (f,ts) = strip_comb t


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


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


48 


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


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


51 


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


53 


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


55 


56 
fun inst_lift cmap state lift i =


57 
let val sg = #sign(rep_thm state)


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


59 
val goali = nth_subgoal i state


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


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


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


63 
val cu = Sign.cterm_of sg cntxt


64 
val uT = #T(Sign.rep_cterm cu)


65 
val cP' = Sign.cterm_of sg (Var(P,uT))


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


67 
val ixncTs = map (fn (x,y) => (x,Sign.ctyp_of sg y)) ixnTs;


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


69 


70 
fun splittable al i thm =


71 
let val tm = goal_concl i thm


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


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


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


75 
 nobound _ _ _ = true;


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


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


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


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


80 
in case h of


81 
Const(c,_) =>


82 
(case assoc(al,c) of


83 
Some(n,thm) =>


84 
if length args < n then no()


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


86 
then Some(thm)


87 
else no()


88 
 None => no())


89 
 _ => no()


90 
end)


91 
 find _ (some,_) = some


92 
in find 0 (None,tm) end;


93 


94 
fun split_tac [] i = no_tac


95 
 split_tac splits i =


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


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


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


99 
val cmap = map const splits;


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


101 
fun lift_split thm =


102 
case splittable cmap i thm of


103 
Some(split) => rtac split i


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


105 
STATE lift_split]


106 
in STATE(fn thm =>


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


108 
then EVERY[rtac iffD i, STATE lift_split]


109 
else no_tac)


110 
end;


111 


112 
in split_tac end;
