4
|
1 |
(* Title: Provers/splitter
|
|
2 |
ID: $Id$
|
|
3 |
Author: Tobias Nipkow
|
|
4 |
Copyright 1993 TU Munich
|
|
5 |
|
|
6 |
Generic case-splitter, 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 |
|
|
22 |
val lift = prove_goal Pure.thy
|
|
23 |
"[| !!x::'b::logic. Q(x) == R(x) |] ==> P(%x.Q(x)) == P(%x.R(x))::'a::logic"
|
|
24 |
(fn [prem] => [rewtac prem, rtac reflexive_thm 1]);
|
4
|
25 |
|
0
|
26 |
val trlift = lift RS transitive_thm;
|
|
27 |
val _ $ (Var(P,PT)$_) $ _ = concl_of trlift;
|
|
28 |
|
|
29 |
fun contains cmap =
|
|
30 |
let fun isin i (Abs(_,_,b)) = isin 0 b
|
|
31 |
| isin i (s$t) = isin (i+1) s orelse isin 0 t
|
|
32 |
| isin i (Const(c,_)) = (case assoc(cmap,c) of
|
|
33 |
Some(n,_) => n <= i
|
|
34 |
| None => false)
|
|
35 |
| isin _ _ = false
|
|
36 |
in isin 0 end;
|
|
37 |
|
|
38 |
fun mk_context cmap Ts maxi t =
|
|
39 |
let fun var (t,i) = Var(("X",i),type_of1(Ts,t))
|
|
40 |
|
|
41 |
fun mka((None,i,ts),t) = if contains cmap t
|
|
42 |
then let val (u,T,j) = mk(t,i) in (Some(T),j,ts@[u]) end
|
|
43 |
else (None,i+1,ts@[var(t,i)])
|
|
44 |
| mka((some,i,ts),t) = (some,i+1,ts@[var(t,i)])
|
|
45 |
and mk(t as Abs _, i) = (Bound 0,type_of1(Ts,t),i)
|
|
46 |
| mk(t,i) =
|
|
47 |
let val (f,ts) = strip_comb t
|
|
48 |
val (Some(T),j,us) = foldl mka ((None,i,[]),ts)
|
|
49 |
in (list_comb(f,us),T,j) end
|
|
50 |
|
|
51 |
val (u,T,_) = mk(t,maxi+1)
|
|
52 |
in Abs("",T,u) end;
|
|
53 |
|
|
54 |
fun nth_subgoal i thm = nth_elem(i-1,prems_of thm);
|
|
55 |
|
|
56 |
fun goal_concl i thm = Logic.strip_assums_concl(nth_subgoal i thm);
|
|
57 |
|
|
58 |
fun inst_lift cmap state lift i =
|
|
59 |
let val sg = #sign(rep_thm state)
|
|
60 |
val tsig = #tsig(Sign.rep_sg sg)
|
|
61 |
val goali = nth_subgoal i state
|
|
62 |
val Ts = map #2 (Logic.strip_params goali)
|
|
63 |
val _ $ t $ _ = Logic.strip_assums_concl goali;
|
|
64 |
val cntxt = mk_context cmap (rev Ts) (#maxidx(rep_thm lift)) t
|
231
|
65 |
val cu = cterm_of sg cntxt
|
|
66 |
val uT = #T(rep_cterm cu)
|
|
67 |
val cP' = cterm_of sg (Var(P,uT))
|
0
|
68 |
val ixnTs = Type.typ_match tsig ([],(PT,uT));
|
231
|
69 |
val ixncTs = map (fn (x,y) => (x,ctyp_of sg y)) ixnTs;
|
0
|
70 |
in instantiate (ixncTs, [(cP',cu)]) lift end;
|
|
71 |
|
|
72 |
fun splittable al i thm =
|
|
73 |
let val tm = goal_concl i thm
|
|
74 |
fun nobound j k (Abs(_,_,t)) = nobound j (k+1) t
|
|
75 |
| nobound j k (s$t) = nobound j k s andalso nobound j k t
|
|
76 |
| nobound j k (Bound n) = n < k orelse k+j <= n
|
|
77 |
| nobound _ _ _ = true;
|
|
78 |
fun find j (None,t) = (case t of
|
|
79 |
Abs(_,_,t) => find (j+1) (None,t)
|
|
80 |
| _ => let val (h,args) = strip_comb t
|
|
81 |
fun no() = foldl (find j) (None,args)
|
|
82 |
in case h of
|
|
83 |
Const(c,_) =>
|
|
84 |
(case assoc(al,c) of
|
|
85 |
Some(n,thm) =>
|
|
86 |
if length args < n then no()
|
|
87 |
else if forall (nobound j 0) (take(n,args))
|
|
88 |
then Some(thm)
|
|
89 |
else no()
|
|
90 |
| None => no())
|
|
91 |
| _ => no()
|
|
92 |
end)
|
|
93 |
| find _ (some,_) = some
|
|
94 |
in find 0 (None,tm) end;
|
|
95 |
|
|
96 |
fun split_tac [] i = no_tac
|
|
97 |
| split_tac splits i =
|
|
98 |
let fun const(thm) = let val _$(_$lhs)$_ = concl_of thm
|
|
99 |
val (Const(a,_),args) = strip_comb lhs
|
|
100 |
in (a,(length args,thm)) end
|
|
101 |
val cmap = map const splits;
|
|
102 |
fun lift thm = rtac (inst_lift cmap thm trlift i) i
|
|
103 |
fun lift_split thm =
|
|
104 |
case splittable cmap i thm of
|
|
105 |
Some(split) => rtac split i
|
|
106 |
| None => EVERY[STATE lift, rtac reflexive_thm (i+1),
|
|
107 |
STATE lift_split]
|
|
108 |
in STATE(fn thm =>
|
|
109 |
if (i <= nprems_of thm) andalso contains cmap (goal_concl i thm)
|
|
110 |
then EVERY[rtac iffD i, STATE lift_split]
|
|
111 |
else no_tac)
|
|
112 |
end;
|
|
113 |
|
|
114 |
in split_tac end;
|