author | nipkow |
Thu, 13 Apr 1995 10:20:55 +0200 | |
changeset 1030 | 1d8fa2fc4b9c |
parent 943 | 8477483f663f |
child 1064 | 5d6fb2c938e0 |
permissions | -rw-r--r-- |
4 | 1 |
(* Title: Provers/splitter |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow |
|
1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
4 |
Copyright 1995 TU Munich |
4 | 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 |
||
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 |
||
1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
34 |
fun mk_cntxt Ts t pos T maxi = |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
35 |
let fun var (t,i) = Var(("X",i),type_of1(Ts,t)); |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
36 |
fun down [] t i = Bound 0 |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
37 |
| down (p::ps) t i = |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
38 |
let val (h,ts) = strip_comb t |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
39 |
val v1 = map var (take(p,ts) ~~ (i upto (i+p-1))) |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
40 |
val u::us = drop(p,ts) |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
41 |
val v2 = map var (us ~~ ((i+p) upto (i+length(ts)-2))) |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
42 |
in list_comb(h,v1@[down ps u (i+length ts)]@v2) end; |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
43 |
in Abs("", T, down (rev pos) t maxi) end; |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
44 |
|
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
45 |
fun add_lbnos(is,t) = add_loose_bnos(t,0,is); |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
46 |
|
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
47 |
fun typ_test _ [] = true |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
48 |
| typ_test T ((_,U,_)::_) = (T=U); |
0 | 49 |
|
1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
50 |
fun mk_split_pack(thm,T,n,ts,apsns) = |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
51 |
if n <= length ts andalso typ_test T apsns |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
52 |
then let val lev = length apsns |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
53 |
val lbnos = foldl add_lbnos ([],take(n,ts)) |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
54 |
val flbnos = filter (fn i => i < lev) lbnos |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
55 |
in [(thm, if null flbnos then [] else rev apsns)] end |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
56 |
else []; |
0 | 57 |
|
1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
58 |
fun split_posns cmap Ts t = |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
59 |
let fun posns Ts pos apsns (Abs(_,T,t)) = |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
60 |
let val U = fastype_of1(T::Ts,t) |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
61 |
in posns (T::Ts) (0::pos) ((T,U,pos)::apsns) t end |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
62 |
| posns Ts pos apsns t = |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
63 |
let val (h,ts) = strip_comb t |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
64 |
fun iter((i,a),t) = (i+1, (posns Ts (i::pos) apsns t) @ a); |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
65 |
val a = case h of |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
66 |
Const(c,_) => |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
67 |
(case assoc(cmap,c) of |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
68 |
Some(thm,T,n) => mk_split_pack(thm,T,n,ts,apsns) |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
69 |
| None => []) |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
70 |
| _ => [] |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
71 |
in snd(foldl iter ((0,a),ts)) end |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
72 |
in posns Ts [] [] t end; |
0 | 73 |
|
74 |
fun nth_subgoal i thm = nth_elem(i-1,prems_of thm); |
|
75 |
||
1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
76 |
fun shorter((_,ps),(_,qs)) = length ps <= length qs; |
0 | 77 |
|
1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
78 |
fun select cmap state i = |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
79 |
let val goali = nth_subgoal i state |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
80 |
val Ts = rev(map #2 (Logic.strip_params goali)) |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
81 |
val _ $ t $ _ = Logic.strip_assums_concl goali; |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
82 |
in (Ts,t,sort shorter (split_posns cmap Ts t)) end; |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
83 |
|
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
84 |
fun inst_lift Ts t (T,U,pos) state lift i = |
0 | 85 |
let val sg = #sign(rep_thm state) |
86 |
val tsig = #tsig(Sign.rep_sg sg) |
|
1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
87 |
val cntxt = mk_cntxt Ts t pos (T-->U) (#maxidx(rep_thm lift)) |
231 | 88 |
val cu = cterm_of sg cntxt |
89 |
val uT = #T(rep_cterm cu) |
|
90 |
val cP' = cterm_of sg (Var(P,uT)) |
|
0 | 91 |
val ixnTs = Type.typ_match tsig ([],(PT,uT)); |
231 | 92 |
val ixncTs = map (fn (x,y) => (x,ctyp_of sg y)) ixnTs; |
0 | 93 |
in instantiate (ixncTs, [(cP',cu)]) lift end; |
94 |
||
95 |
||
96 |
fun split_tac [] i = no_tac |
|
97 |
| split_tac splits i = |
|
1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
98 |
let fun const(thm) = let val _$(t as _$lhs)$_ = concl_of thm |
0 | 99 |
val (Const(a,_),args) = strip_comb lhs |
1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
100 |
in (a,(thm,fastype_of t,length args)) end |
0 | 101 |
val cmap = map const splits; |
1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
102 |
fun lift Ts t p state = rtac (inst_lift Ts t p state trlift i) i |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
103 |
fun lift_split state = |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
104 |
let val (Ts,t,splits) = select cmap state i |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
105 |
in case splits of |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
106 |
[] => no_tac |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
107 |
| (thm,apsns)::_ => |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
108 |
(case apsns of |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
109 |
[] => rtac thm i |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
110 |
| p::_ => EVERY[STATE(lift Ts t p), |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
111 |
rtac reflexive_thm (i+1), |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
112 |
STATE lift_split]) |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
113 |
end |
0 | 114 |
in STATE(fn thm => |
1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
115 |
if i <= nprems_of thm then rtac iffD i THEN STATE lift_split |
0 | 116 |
else no_tac) |
117 |
end; |
|
118 |
||
119 |
in split_tac end; |