author | wenzelm |
Wed, 10 Jun 1998 11:55:30 +0200 | |
changeset 5018 | ce8e87fad843 |
parent 4930 | 89271bc4e7ed |
child 5304 | c133f16febc7 |
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 |
||
4189 | 12 |
by(split_tac splits i); |
0 | 13 |
|
14 |
where splits = [P(elim(...)) == rhs, ...] |
|
15 |
iffD = [| P <-> Q; Q |] ==> P (* is called iffD2 in HOL *) |
|
16 |
||
17 |
*) |
|
18 |
||
1721
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
19 |
local |
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
20 |
|
4668
131989b78417
Little reorganization. Loop tactics have names now.
nipkow
parents:
4519
diff
changeset
|
21 |
fun split_format_err() = error("Wrong format for split rule"); |
131989b78417
Little reorganization. Loop tactics have names now.
nipkow
parents:
4519
diff
changeset
|
22 |
|
1721
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
23 |
fun mk_case_split_tac_2 iffD order = |
0 | 24 |
let |
25 |
||
1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
26 |
|
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
27 |
(************************************************************ |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
28 |
Create lift-theorem "trlift" : |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
29 |
|
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
30 |
[| !! x. Q(x)==R(x) ; P(R) == C |] ==> P(Q)==C |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
31 |
|
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
32 |
*************************************************************) |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
33 |
|
943 | 34 |
val lift = |
35 |
let val ct = read_cterm (#sign(rep_thm iffD)) |
|
36 |
("[| !!x::'b::logic. Q(x) == R(x) |] ==> \ |
|
3835 | 37 |
\P(%x. Q(x)) == P(%x. R(x))::'a::logic",propT) |
943 | 38 |
in prove_goalw_cterm [] ct |
39 |
(fn [prem] => [rewtac prem, rtac reflexive_thm 1]) |
|
40 |
end; |
|
4 | 41 |
|
0 | 42 |
val trlift = lift RS transitive_thm; |
43 |
val _ $ (Var(P,PT)$_) $ _ = concl_of trlift; |
|
44 |
||
45 |
||
1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
46 |
(************************************************************************ |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
47 |
Set up term for instantiation of P in the lift-theorem |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
48 |
|
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
49 |
Ts : types of parameters (i.e. variables bound by meta-quantifiers) |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
50 |
t : lefthand side of meta-equality in subgoal |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
51 |
the lift theorem is applied to (see select) |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
52 |
pos : "path" leading to abstraction, coded as a list |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
53 |
T : type of body of P(...) |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
54 |
maxi : maximum index of Vars |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
55 |
*************************************************************************) |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
56 |
|
1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
57 |
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
|
58 |
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
|
59 |
fun down [] t i = Bound 0 |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
60 |
| down (p::ps) t i = |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
61 |
let val (h,ts) = strip_comb t |
2266 | 62 |
val v1 = ListPair.map var (take(p,ts), i upto (i+p-1)) |
1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
63 |
val u::us = drop(p,ts) |
2266 | 64 |
val v2 = ListPair.map var (us, (i+p) upto (i+length(ts)-2)) |
1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
65 |
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
|
66 |
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
|
67 |
|
1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
68 |
|
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
69 |
(************************************************************************ |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
70 |
Set up term for instantiation of P in the split-theorem |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
71 |
P(...) == rhs |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
72 |
|
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
73 |
t : lefthand side of meta-equality in subgoal |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
74 |
the split theorem is applied to (see select) |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
75 |
T : type of body of P(...) |
4232 | 76 |
tt : the term Const(key,..) $ ... |
1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
77 |
*************************************************************************) |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
78 |
|
4232 | 79 |
fun mk_cntxt_splitthm t tt T = |
80 |
let fun repl lev t = |
|
81 |
if incr_boundvars lev tt = t then Bound lev |
|
82 |
else case t of |
|
83 |
(Abs (v, T2, t)) => Abs (v, T2, repl (lev+1) t) |
|
84 |
| (Bound i) => Bound (if i>=lev then i+1 else i) |
|
85 |
| (t1 $ t2) => (repl lev t1) $ (repl lev t2) |
|
86 |
| t => t |
|
87 |
in Abs("", T, repl 0 t) end; |
|
1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
88 |
|
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
89 |
|
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
90 |
(* add all loose bound variables in t to list is *) |
1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
91 |
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
|
92 |
|
1064 | 93 |
(* check if the innermost quantifier that needs to be removed |
94 |
has a body of type T; otherwise the expansion thm will fail later on |
|
95 |
*) |
|
96 |
fun type_test(T,lbnos,apsns) = |
|
2143 | 97 |
let val (_,U,_) = nth_elem(foldl Int.min (hd lbnos, tl lbnos), apsns) |
1064 | 98 |
in T=U end; |
0 | 99 |
|
1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
100 |
(************************************************************************* |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
101 |
Create a "split_pack". |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
102 |
|
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
103 |
thm : the relevant split-theorem, i.e. P(...) == rhs , where P(...) |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
104 |
is of the form |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
105 |
P( Const(key,...) $ t_1 $ ... $ t_n ) (e.g. key = "if") |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
106 |
T : type of P(...) |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
107 |
n : number of arguments expected by Const(key,...) |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
108 |
ts : list of arguments actually found |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
109 |
apsns : list of tuples of the form (T,U,pos), one tuple for each |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
110 |
abstraction that is encountered on the way to the position where |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
111 |
Const(key, ...) $ ... occurs, where |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
112 |
T : type of the variable bound by the abstraction |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
113 |
U : type of the abstraction's body |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
114 |
pos : "path" leading to the body of the abstraction |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
115 |
pos : "path" leading to the position where Const(key, ...) $ ... occurs. |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
116 |
TB : type of Const(key,...) $ t_1 $ ... $ t_n |
1721
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
117 |
t : the term Const(key,...) $ t_1 $ ... $ t_n |
1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
118 |
|
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
119 |
A split pack is a tuple of the form |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
120 |
(thm, apsns, pos, TB) |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
121 |
Note : apsns is reversed, so that the outermost quantifier's position |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
122 |
comes first ! If the terms in ts don't contain variables bound |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
123 |
by other than meta-quantifiers, apsns is empty, because no further |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
124 |
lifting is required before applying the split-theorem. |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
125 |
******************************************************************************) |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
126 |
|
1721
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
127 |
fun mk_split_pack(thm,T,n,ts,apsns,pos,TB,t) = |
1064 | 128 |
if n > length ts then [] |
129 |
else let val lev = length apsns |
|
1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
130 |
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
|
131 |
val flbnos = filter (fn i => i < lev) lbnos |
4232 | 132 |
val tt = incr_boundvars (~lev) t |
1721
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
133 |
in if null flbnos then [(thm,[],pos,TB,tt)] |
2143 | 134 |
else if type_test(T,flbnos,apsns) then [(thm, rev apsns,pos,TB,tt)] |
135 |
else [] |
|
1064 | 136 |
end; |
0 | 137 |
|
1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
138 |
|
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
139 |
(**************************************************************************** |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
140 |
Recursively scans term for occurences of Const(key,...) $ ... |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
141 |
Returns a list of "split-packs" (one for each occurence of Const(key,...) ) |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
142 |
|
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
143 |
cmap : association list of split-theorems that should be tried. |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
144 |
The elements have the format (key,(thm,T,n)) , where |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
145 |
key : the theorem's key constant ( Const(key,...) $ ... ) |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
146 |
thm : the theorem itself |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
147 |
T : type of P( Const(key,...) $ ... ) |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
148 |
n : number of arguments expected by Const(key,...) |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
149 |
Ts : types of parameters |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
150 |
t : the term to be scanned |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
151 |
******************************************************************************) |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
152 |
|
1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
153 |
fun split_posns cmap Ts t = |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
154 |
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
|
155 |
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
|
156 |
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
|
157 |
| posns Ts pos apsns t = |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
158 |
let val (h,ts) = strip_comb t |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
159 |
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
|
160 |
val a = case h of |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
161 |
Const(c,_) => |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
162 |
(case assoc(cmap,c) of |
4232 | 163 |
Some(thm, T, n) => |
164 |
let val t2 = list_comb (h, take (n, ts)) in |
|
165 |
mk_split_pack(thm,T,n,ts,apsns,pos,type_of1(Ts, t2),t2) |
|
166 |
end |
|
1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
167 |
| None => []) |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
168 |
| _ => [] |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
169 |
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
|
170 |
in posns Ts [] [] t end; |
0 | 171 |
|
1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
172 |
|
0 | 173 |
fun nth_subgoal i thm = nth_elem(i-1,prems_of thm); |
174 |
||
1721
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
175 |
fun shorter((_,ps,pos,_,_),(_,qs,qos,_,_)) = |
4519 | 176 |
prod_ord (int_ord o pairself length) (order o pairself length) |
177 |
((ps, pos), (qs, qos)); |
|
178 |
||
1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
179 |
|
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
180 |
|
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
181 |
(************************************************************ |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
182 |
call split_posns with appropriate parameters |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
183 |
*************************************************************) |
0 | 184 |
|
1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
185 |
fun select cmap state i = |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
186 |
let val goali = nth_subgoal i state |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
187 |
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
|
188 |
val _ $ t $ _ = Logic.strip_assums_concl goali; |
4519 | 189 |
in (Ts,t, sort shorter (split_posns cmap Ts t)) end; |
1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
190 |
|
1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
191 |
|
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
192 |
(************************************************************* |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
193 |
instantiate lift theorem |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
194 |
|
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
195 |
if t is of the form |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
196 |
... ( Const(...,...) $ Abs( .... ) ) ... |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
197 |
then |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
198 |
P = %a. ... ( Const(...,...) $ a ) ... |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
199 |
where a has type T --> U |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
200 |
|
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
201 |
Ts : types of parameters |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
202 |
t : lefthand side of meta-equality in subgoal |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
203 |
the split theorem is applied to (see cmap) |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
204 |
T,U,pos : see mk_split_pack |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
205 |
state : current proof state |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
206 |
lift : the lift theorem |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
207 |
i : no. of subgoal |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
208 |
**************************************************************) |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
209 |
|
1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
210 |
fun inst_lift Ts t (T,U,pos) state lift i = |
0 | 211 |
let val sg = #sign(rep_thm state) |
212 |
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
|
213 |
val cntxt = mk_cntxt Ts t pos (T-->U) (#maxidx(rep_thm lift)) |
231 | 214 |
val cu = cterm_of sg cntxt |
215 |
val uT = #T(rep_cterm cu) |
|
216 |
val cP' = cterm_of sg (Var(P,uT)) |
|
0 | 217 |
val ixnTs = Type.typ_match tsig ([],(PT,uT)); |
231 | 218 |
val ixncTs = map (fn (x,y) => (x,ctyp_of sg y)) ixnTs; |
0 | 219 |
in instantiate (ixncTs, [(cP',cu)]) lift end; |
220 |
||
221 |
||
1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
222 |
(************************************************************* |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
223 |
instantiate split theorem |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
224 |
|
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
225 |
Ts : types of parameters |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
226 |
t : lefthand side of meta-equality in subgoal |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
227 |
the split theorem is applied to (see cmap) |
4232 | 228 |
tt : the term Const(key,..) $ ... |
1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
229 |
thm : the split theorem |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
230 |
TB : type of body of P(...) |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
231 |
state : current proof state |
4232 | 232 |
i : number of subgoal |
1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
233 |
**************************************************************) |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
234 |
|
4232 | 235 |
fun inst_split Ts t tt thm TB state i = |
236 |
let val _ $ ((Var (P2, PT2)) $ _) $ _ = concl_of thm; |
|
1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
237 |
val sg = #sign(rep_thm state) |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
238 |
val tsig = #tsig(Sign.rep_sg sg) |
4232 | 239 |
val cntxt = mk_cntxt_splitthm t tt TB; |
4236 | 240 |
val T = fastype_of1 (Ts, cntxt); |
4232 | 241 |
val ixnTs = Type.typ_match tsig ([],(PT2, T)) |
242 |
val abss = foldl (fn (t, T) => Abs ("", T, t)) |
|
243 |
in |
|
244 |
term_lift_inst_rule (state, i, ixnTs, [((P2, T), abss (cntxt, Ts))], thm) |
|
245 |
end; |
|
1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
246 |
|
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
247 |
(***************************************************************************** |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
248 |
The split-tactic |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
249 |
|
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
250 |
splits : list of split-theorems to be tried |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
251 |
i : number of subgoal the tactic should be applied to |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
252 |
*****************************************************************************) |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
253 |
|
0 | 254 |
fun split_tac [] i = no_tac |
255 |
| split_tac splits i = |
|
3918 | 256 |
let fun const(thm) = |
257 |
(case concl_of thm of _$(t as _$lhs)$_ => |
|
258 |
(case strip_comb lhs of (Const(a,_),args) => |
|
259 |
(a,(thm,fastype_of t,length args)) |
|
4668
131989b78417
Little reorganization. Loop tactics have names now.
nipkow
parents:
4519
diff
changeset
|
260 |
| _ => split_format_err()) |
131989b78417
Little reorganization. Loop tactics have names now.
nipkow
parents:
4519
diff
changeset
|
261 |
| _ => split_format_err()) |
0 | 262 |
val cmap = map const splits; |
3537 | 263 |
fun lift_tac Ts t p st = (rtac (inst_lift Ts t p st trlift i) i) st |
264 |
fun lift_split_tac st = st |> |
|
265 |
let val (Ts,t,splits) = select cmap st i |
|
1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
266 |
in case splits of |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
267 |
[] => no_tac |
1721
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
268 |
| (thm,apsns,pos,TB,tt)::_ => |
1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
269 |
(case apsns of |
3537 | 270 |
[] => (fn state => state |> |
4232 | 271 |
compose_tac (false, inst_split Ts t tt thm TB state i, 0) i) |
3537 | 272 |
| p::_ => EVERY[lift_tac Ts t p, |
1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
273 |
rtac reflexive_thm (i+1), |
3537 | 274 |
lift_split_tac]) |
1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
275 |
end |
3537 | 276 |
in COND (has_fewer_prems i) no_tac |
277 |
(rtac iffD i THEN lift_split_tac) |
|
0 | 278 |
end; |
279 |
||
280 |
in split_tac end; |
|
1721
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
281 |
|
4930
89271bc4e7ed
extended addsplits and delsplits to handle also split rules for assumptions
oheimb
parents:
4668
diff
changeset
|
282 |
(* FIXME: this junk is only FOL/HOL specific and should therefore not go here!*) |
89271bc4e7ed
extended addsplits and delsplits to handle also split rules for assumptions
oheimb
parents:
4668
diff
changeset
|
283 |
(* split_thm_info is used in FOL/simpdata.ML and HOL/simpdata.ML *) |
89271bc4e7ed
extended addsplits and delsplits to handle also split rules for assumptions
oheimb
parents:
4668
diff
changeset
|
284 |
fun split_thm_info thm = |
4668
131989b78417
Little reorganization. Loop tactics have names now.
nipkow
parents:
4519
diff
changeset
|
285 |
(case concl_of thm of |
4930
89271bc4e7ed
extended addsplits and delsplits to handle also split rules for assumptions
oheimb
parents:
4668
diff
changeset
|
286 |
Const("Trueprop",_) $ (Const("op =", _)$(Var _$t)$c) => |
4668
131989b78417
Little reorganization. Loop tactics have names now.
nipkow
parents:
4519
diff
changeset
|
287 |
(case strip_comb t of |
4930
89271bc4e7ed
extended addsplits and delsplits to handle also split rules for assumptions
oheimb
parents:
4668
diff
changeset
|
288 |
(Const(a,_),_) => (a,case c of (Const("Not",_)$_)=> true |_=> false) |
4668
131989b78417
Little reorganization. Loop tactics have names now.
nipkow
parents:
4519
diff
changeset
|
289 |
| _ => split_format_err()) |
131989b78417
Little reorganization. Loop tactics have names now.
nipkow
parents:
4519
diff
changeset
|
290 |
| _ => split_format_err()); |
4189 | 291 |
|
4202 | 292 |
fun mk_case_split_asm_tac split_tac |
293 |
(disjE,conjE,exE,contrapos,contrapos2,notnotD) = |
|
4189 | 294 |
let |
295 |
||
296 |
(***************************************************************************** |
|
297 |
The split-tactic for premises |
|
298 |
||
299 |
splits : list of split-theorems to be tried |
|
300 |
i : number of subgoal the tactic should be applied to |
|
301 |
*****************************************************************************) |
|
302 |
||
4202 | 303 |
fun split_asm_tac [] = K no_tac |
304 |
| split_asm_tac splits = |
|
4930
89271bc4e7ed
extended addsplits and delsplits to handle also split rules for assumptions
oheimb
parents:
4668
diff
changeset
|
305 |
let val cname_list = map (fst o split_thm_info) splits; |
4189 | 306 |
fun is_case (a,_) = a mem cname_list; |
307 |
fun tac (t,i) = |
|
308 |
let val n = find_index (exists_Const is_case) |
|
309 |
(Logic.strip_assums_hyp t); |
|
310 |
fun first_prem_is_disj (Const ("==>", _) $ (Const ("Trueprop", _) |
|
311 |
$ (Const ("op |", _) $ _ $ _ )) $ _ ) = true |
|
4202 | 312 |
| first_prem_is_disj (Const("all",_)$Abs(_,_,t)) = |
313 |
first_prem_is_disj t |
|
4189 | 314 |
| first_prem_is_disj _ = false; |
4202 | 315 |
fun flat_prems_tac i = SUBGOAL (fn (t,i) => |
4189 | 316 |
(if first_prem_is_disj t |
317 |
then EVERY[etac disjE i, rotate_tac ~1 i, |
|
318 |
rotate_tac ~1 (i+1), |
|
319 |
flat_prems_tac (i+1)] |
|
320 |
else all_tac) |
|
321 |
THEN REPEAT (eresolve_tac [conjE,exE] i) |
|
4202 | 322 |
THEN REPEAT (dresolve_tac [notnotD] i)) i; |
4189 | 323 |
in if n<0 then no_tac else DETERM (EVERY' |
324 |
[rotate_tac n, etac contrapos2, |
|
325 |
split_tac splits, |
|
326 |
rotate_tac ~1, etac contrapos, rotate_tac ~1, |
|
4202 | 327 |
flat_prems_tac] i) |
4189 | 328 |
end; |
329 |
in SUBGOAL tac |
|
330 |
end; |
|
331 |
||
4202 | 332 |
in split_asm_tac end; |
4189 | 333 |
|
334 |
||
1721
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
335 |
in |
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
336 |
|
4930
89271bc4e7ed
extended addsplits and delsplits to handle also split rules for assumptions
oheimb
parents:
4668
diff
changeset
|
337 |
val split_thm_info = split_thm_info; |
4668
131989b78417
Little reorganization. Loop tactics have names now.
nipkow
parents:
4519
diff
changeset
|
338 |
|
4519 | 339 |
fun mk_case_split_tac iffD = mk_case_split_tac_2 iffD int_ord; |
1721
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
340 |
|
4519 | 341 |
fun mk_case_split_inside_tac iffD = mk_case_split_tac_2 iffD (rev_order o int_ord); |
1721
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
342 |
|
4202 | 343 |
val mk_case_split_asm_tac = mk_case_split_asm_tac; |
4189 | 344 |
|
1721
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
345 |
end; |