author | wenzelm |
Mon, 22 Sep 1997 17:37:48 +0200 | |
changeset 3696 | e2af92a3281b |
parent 3537 | 79ac9b475621 |
child 3835 | 9a5a4e123859 |
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 |
||
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 |
|
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
21 |
fun mk_case_split_tac_2 iffD order = |
0 | 22 |
let |
23 |
||
1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
24 |
|
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
25 |
(************************************************************ |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
26 |
Create lift-theorem "trlift" : |
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 |
[| !! 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
|
29 |
|
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
30 |
*************************************************************) |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
31 |
|
943 | 32 |
val lift = |
33 |
let val ct = read_cterm (#sign(rep_thm iffD)) |
|
34 |
("[| !!x::'b::logic. Q(x) == R(x) |] ==> \ |
|
35 |
\P(%x.Q(x)) == P(%x.R(x))::'a::logic",propT) |
|
36 |
in prove_goalw_cterm [] ct |
|
37 |
(fn [prem] => [rewtac prem, rtac reflexive_thm 1]) |
|
38 |
end; |
|
4 | 39 |
|
0 | 40 |
val trlift = lift RS transitive_thm; |
41 |
val _ $ (Var(P,PT)$_) $ _ = concl_of trlift; |
|
42 |
||
43 |
||
1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
44 |
(************************************************************************ |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
45 |
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
|
46 |
|
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
47 |
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
|
48 |
t : lefthand side of meta-equality in subgoal |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
49 |
the lift theorem is applied to (see select) |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
50 |
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
|
51 |
T : type of body of P(...) |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
52 |
maxi : maximum index of Vars |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
53 |
*************************************************************************) |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
54 |
|
1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
55 |
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
|
56 |
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
|
57 |
fun down [] t i = Bound 0 |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
58 |
| down (p::ps) t i = |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
59 |
let val (h,ts) = strip_comb t |
2266 | 60 |
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
|
61 |
val u::us = drop(p,ts) |
2266 | 62 |
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
|
63 |
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
|
64 |
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
|
65 |
|
1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
66 |
|
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
67 |
(************************************************************************ |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
68 |
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
|
69 |
P(...) == rhs |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
70 |
|
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
71 |
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
|
72 |
t : lefthand side of meta-equality in subgoal |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
73 |
the split theorem is applied to (see select) |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
74 |
T : type of body of P(...) |
1721
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
75 |
tt : the term Const(..,..) $ ... |
1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
76 |
maxi : maximum index of Vars |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
77 |
|
1721
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
78 |
lev : abstraction level |
1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
79 |
*************************************************************************) |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
80 |
|
1721
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
81 |
fun mk_cntxt_splitthm Ts t tt T maxi = |
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
82 |
let fun down lev (Abs(v,T2,t)) = Abs(v,T2,down (lev+1) t) |
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
83 |
| down lev (Bound i) = if i >= lev |
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
84 |
then Var(("X",maxi+i-lev),nth_elem(i-lev,Ts)) |
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
85 |
else Bound i |
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
86 |
| down lev t = |
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
87 |
let val (h,ts) = strip_comb t |
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
88 |
val h2 = (case h of Bound _ => down lev h | _ => h) |
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
89 |
in if incr_bv(lev,0,tt)=t |
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
90 |
then |
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
91 |
Bound (lev) |
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
92 |
else |
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
93 |
list_comb(h2,map (down lev) ts) |
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
94 |
end; |
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
95 |
in Abs("",T,down 0 t) end; |
1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
96 |
|
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
97 |
|
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
98 |
(* 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
|
99 |
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
|
100 |
|
1064 | 101 |
(* check if the innermost quantifier that needs to be removed |
102 |
has a body of type T; otherwise the expansion thm will fail later on |
|
103 |
*) |
|
104 |
fun type_test(T,lbnos,apsns) = |
|
2143 | 105 |
let val (_,U,_) = nth_elem(foldl Int.min (hd lbnos, tl lbnos), apsns) |
1064 | 106 |
in T=U end; |
0 | 107 |
|
1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
108 |
(************************************************************************* |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
109 |
Create a "split_pack". |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
110 |
|
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
111 |
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
|
112 |
is of the form |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
113 |
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
|
114 |
T : type of P(...) |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
115 |
n : number of arguments expected by Const(key,...) |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
116 |
ts : list of arguments actually found |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
117 |
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
|
118 |
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
|
119 |
Const(key, ...) $ ... occurs, where |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
120 |
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
|
121 |
U : type of the abstraction's body |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
122 |
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
|
123 |
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
|
124 |
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
|
125 |
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
|
126 |
|
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
127 |
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
|
128 |
(thm, apsns, pos, TB) |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
129 |
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
|
130 |
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
|
131 |
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
|
132 |
lifting is required before applying the split-theorem. |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
133 |
******************************************************************************) |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
134 |
|
1721
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
135 |
fun mk_split_pack(thm,T,n,ts,apsns,pos,TB,t) = |
1064 | 136 |
if n > length ts then [] |
137 |
else let val lev = length apsns |
|
1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
138 |
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
|
139 |
val flbnos = filter (fn i => i < lev) lbnos |
1721
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
140 |
val tt = incr_bv(~lev,0,t) |
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
141 |
in if null flbnos then [(thm,[],pos,TB,tt)] |
2143 | 142 |
else if type_test(T,flbnos,apsns) then [(thm, rev apsns,pos,TB,tt)] |
143 |
else [] |
|
1064 | 144 |
end; |
0 | 145 |
|
1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
146 |
|
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
147 |
(**************************************************************************** |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
148 |
Recursively scans term for occurences of Const(key,...) $ ... |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
149 |
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
|
150 |
|
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
151 |
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
|
152 |
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
|
153 |
key : the theorem's key constant ( Const(key,...) $ ... ) |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
154 |
thm : the theorem itself |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
155 |
T : type of P( Const(key,...) $ ... ) |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
156 |
n : number of arguments expected by Const(key,...) |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
157 |
Ts : types of parameters |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
158 |
t : the term to be scanned |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
159 |
******************************************************************************) |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
160 |
|
1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
161 |
fun split_posns cmap Ts t = |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
162 |
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
|
163 |
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
|
164 |
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
|
165 |
| posns Ts pos apsns t = |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
166 |
let val (h,ts) = strip_comb t |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
167 |
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
|
168 |
val a = case h of |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
169 |
Const(c,_) => |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
170 |
(case assoc(cmap,c) of |
1721
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
171 |
Some(thm,T,n) => mk_split_pack(thm,T,n,ts,apsns,pos,type_of1(Ts,t),t) |
1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
172 |
| None => []) |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
173 |
| _ => [] |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
174 |
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
|
175 |
in posns Ts [] [] t end; |
0 | 176 |
|
1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
177 |
|
0 | 178 |
fun nth_subgoal i thm = nth_elem(i-1,prems_of thm); |
179 |
||
1721
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
180 |
fun shorter((_,ps,pos,_,_),(_,qs,qos,_,_)) = |
1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
181 |
let val ms = length ps and ns = length qs |
1721
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
182 |
in ms < ns orelse (ms = ns andalso order(length pos,length qos)) end; |
1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
183 |
|
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
184 |
|
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
185 |
(************************************************************ |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
186 |
call split_posns with appropriate parameters |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
187 |
*************************************************************) |
0 | 188 |
|
1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
189 |
fun select cmap state i = |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
190 |
let val goali = nth_subgoal i state |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
191 |
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
|
192 |
val _ $ t $ _ = Logic.strip_assums_concl goali; |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
193 |
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
|
194 |
|
1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
195 |
|
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
196 |
(************************************************************* |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
197 |
instantiate lift theorem |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
198 |
|
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
199 |
if t is of the form |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
200 |
... ( Const(...,...) $ Abs( .... ) ) ... |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
201 |
then |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
202 |
P = %a. ... ( Const(...,...) $ a ) ... |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
203 |
where a has type T --> U |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
204 |
|
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
205 |
Ts : types of parameters |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
206 |
t : lefthand side of meta-equality in subgoal |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
207 |
the split theorem is applied to (see cmap) |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
208 |
T,U,pos : see mk_split_pack |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
209 |
state : current proof state |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
210 |
lift : the lift theorem |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
211 |
i : no. of subgoal |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
212 |
**************************************************************) |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
213 |
|
1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
214 |
fun inst_lift Ts t (T,U,pos) state lift i = |
0 | 215 |
let val sg = #sign(rep_thm state) |
216 |
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
|
217 |
val cntxt = mk_cntxt Ts t pos (T-->U) (#maxidx(rep_thm lift)) |
231 | 218 |
val cu = cterm_of sg cntxt |
219 |
val uT = #T(rep_cterm cu) |
|
220 |
val cP' = cterm_of sg (Var(P,uT)) |
|
0 | 221 |
val ixnTs = Type.typ_match tsig ([],(PT,uT)); |
231 | 222 |
val ixncTs = map (fn (x,y) => (x,ctyp_of sg y)) ixnTs; |
0 | 223 |
in instantiate (ixncTs, [(cP',cu)]) lift end; |
224 |
||
225 |
||
1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
226 |
(************************************************************* |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
227 |
instantiate split theorem |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
228 |
|
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
229 |
Ts : types of parameters |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
230 |
t : lefthand side of meta-equality in subgoal |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
231 |
the split theorem is applied to (see cmap) |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
232 |
pos : "path" to the body of P(...) |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
233 |
thm : the split theorem |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
234 |
TB : type of body of P(...) |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
235 |
state : current proof state |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
236 |
**************************************************************) |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
237 |
|
1721
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
238 |
fun inst_split Ts t tt thm TB state = |
1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
239 |
let val _$((Var(P2,PT2))$_)$_ = concl_of thm |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
240 |
val sg = #sign(rep_thm state) |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
241 |
val tsig = #tsig(Sign.rep_sg sg) |
1721
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
242 |
val cntxt = mk_cntxt_splitthm Ts t tt TB (#maxidx(rep_thm thm)) |
1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
243 |
val cu = cterm_of sg cntxt |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
244 |
val uT = #T(rep_cterm cu) |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
245 |
val cP' = cterm_of sg (Var(P2,uT)) |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
246 |
val ixnTs = Type.typ_match tsig ([],(PT2,uT)); |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
247 |
val ixncTs = map (fn (x,y) => (x,ctyp_of sg y)) ixnTs; |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
248 |
in instantiate (ixncTs, [(cP',cu)]) thm end; |
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 |
|
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
251 |
(***************************************************************************** |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
252 |
The split-tactic |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
253 |
|
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
254 |
splits : list of split-theorems to be tried |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
255 |
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
|
256 |
*****************************************************************************) |
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset
|
257 |
|
0 | 258 |
fun split_tac [] i = no_tac |
259 |
| split_tac splits i = |
|
1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
260 |
let fun const(thm) = let val _$(t as _$lhs)$_ = concl_of thm |
0 | 261 |
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
|
262 |
in (a,(thm,fastype_of t,length args)) end |
0 | 263 |
val cmap = map const splits; |
3537 | 264 |
fun lift_tac Ts t p st = (rtac (inst_lift Ts t p st trlift i) i) st |
265 |
fun lift_split_tac st = st |> |
|
266 |
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
|
267 |
in case splits of |
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
268 |
[] => no_tac |
1721
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
269 |
| (thm,apsns,pos,TB,tt)::_ => |
1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
270 |
(case apsns of |
3537 | 271 |
[] => (fn state => state |> |
272 |
rtac (inst_split Ts t tt thm TB state) i) |
|
273 |
| 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
|
274 |
rtac reflexive_thm (i+1), |
3537 | 275 |
lift_split_tac]) |
1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset
|
276 |
end |
3537 | 277 |
in COND (has_fewer_prems i) no_tac |
278 |
(rtac iffD i THEN lift_split_tac) |
|
0 | 279 |
end; |
280 |
||
281 |
in split_tac end; |
|
1721
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
282 |
|
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
283 |
in |
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
284 |
|
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
285 |
fun mk_case_split_tac iffD = mk_case_split_tac_2 iffD (op <=) ; |
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
286 |
|
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
287 |
fun mk_case_split_inside_tac iffD = mk_case_split_tac_2 iffD (op >=) ; |
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
288 |
|
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset
|
289 |
end; |