author  berghofe 
Thu, 25 Apr 1996 13:03:57 +0200  
changeset 1686  c67d543bc395 
parent 1064  5d6fb2c938e0 
child 1721  445654b6cb95 
permissions  rwrr 
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 casesplitter, 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 

1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

22 

c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

23 
(************************************************************ 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

24 
Create lifttheorem "trlift" : 
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 
[ !! 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

27 

c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

28 
*************************************************************) 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

29 

943  30 
val lift = 
31 
let val ct = read_cterm (#sign(rep_thm iffD)) 

32 
("[ !!x::'b::logic. Q(x) == R(x) ] ==> \ 

33 
\P(%x.Q(x)) == P(%x.R(x))::'a::logic",propT) 

34 
in prove_goalw_cterm [] ct 

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

36 
end; 

4  37 

0  38 
val trlift = lift RS transitive_thm; 
39 
val _ $ (Var(P,PT)$_) $ _ = concl_of trlift; 

40 

41 

1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

42 
(************************************************************************ 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

43 
Set up term for instantiation of P in the lifttheorem 
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 
Ts : types of parameters (i.e. variables bound by metaquantifiers) 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

46 
t : lefthand side of metaequality in subgoal 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

47 
the lift theorem is applied to (see select) 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

48 
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

49 
T : type of body of P(...) 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

50 
maxi : maximum index of Vars 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

51 
*************************************************************************) 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

52 

1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset

53 
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

54 
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

55 
fun down [] t i = Bound 0 
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset

56 
 down (p::ps) t i = 
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset

57 
let val (h,ts) = strip_comb t 
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset

58 
val v1 = map var (take(p,ts) ~~ (i upto (i+p1))) 
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset

59 
val u::us = drop(p,ts) 
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset

60 
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

61 
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

62 
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

63 

1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

64 

c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

65 
(************************************************************************ 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

66 
Set up term for instantiation of P in the splittheorem 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

67 
P(...) == rhs 
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 
Ts : types of parameters (i.e. variables bound by metaquantifiers) 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

70 
t : lefthand side of metaequality in subgoal 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

71 
the split theorem is applied to (see select) 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

72 
pos : "path" leading to body of P(...), coded as a list 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

73 
T : type of body of P(...) 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

74 
maxi : maximum index of Vars 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

75 

c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

76 
bvars : type of variables bound by other than metaquantifiers 
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 

c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

79 
fun mk_cntxt_splitthm Ts t pos T maxi = 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

80 
let fun down [] t i bvars = Bound (length bvars) 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

81 
 down (p::ps) (Abs(v,T2,t)) i bvars = Abs(v,T2,down ps t i (T2::bvars)) 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

82 
 down (p::ps) t i bvars = 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

83 
let val vars = map Bound (0 upto ((length bvars)1)) 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

84 
val (h,ts) = strip_comb t 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

85 
fun var (t,i) = list_comb(Var(("X",i),bvars > (type_of1(bvars @ Ts,t))),vars); 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

86 
val v1 = map var (take(p,ts) ~~ (i upto (i+p1))) 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

87 
val u::us = drop(p,ts) 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

88 
val v2 = map var (us ~~ ((i+p) upto (i+length(ts)2))) 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

89 
in list_comb(h,v1@[down ps u (i+length ts) bvars]@v2) end; 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

90 
in Abs("",T,down (rev pos) t maxi []) end; 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

91 

c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

92 

c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

93 
(* 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

94 
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

95 

1064  96 
(* check if the innermost quantifier that needs to be removed 
97 
has a body of type T; otherwise the expansion thm will fail later on 

98 
*) 

99 
fun type_test(T,lbnos,apsns) = 

100 
let val (_,U,_) = nth_elem(min lbnos,apsns) 

101 
in T=U end; 

0  102 

1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

103 
(************************************************************************* 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

104 
Create a "split_pack". 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

105 

c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

106 
thm : the relevant splittheorem, i.e. P(...) == rhs , where P(...) 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

107 
is of the form 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

108 
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

109 
T : type of P(...) 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

110 
n : number of arguments expected by Const(key,...) 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

111 
ts : list of arguments actually found 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

112 
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

113 
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

114 
Const(key, ...) $ ... occurs, where 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

115 
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

116 
U : type of the abstraction's body 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

117 
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

118 
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

119 
TB : type of Const(key,...) $ t_1 $ ... $ t_n 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

120 

c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

121 
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

122 
(thm, apsns, pos, TB) 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

123 
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

124 
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

125 
by other than metaquantifiers, apsns is empty, because no further 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

126 
lifting is required before applying the splittheorem. 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

127 
******************************************************************************) 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

128 

c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

129 
fun mk_split_pack(thm,T,n,ts,apsns,pos,TB) = 
1064  130 
if n > length ts then [] 
131 
else let val lev = length apsns 

1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset

132 
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

133 
val flbnos = filter (fn i => i < lev) lbnos 
1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

134 
in if null flbnos then [(thm,[],pos,TB)] 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

135 
else if type_test(T,flbnos,apsns) then [(thm, rev apsns,pos,TB)] 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 "splitpacks" (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 splittheorems 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 
1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

163 
Some(thm,T,n) => mk_split_pack(thm,T,n,ts,apsns,pos,type_of1(Ts,t)) 
1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset

164 
 None => []) 
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset

165 
 _ => [] 
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset

166 
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

167 
in posns Ts [] [] t end; 
0  168 

1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

169 

0  170 
fun nth_subgoal i thm = nth_elem(i1,prems_of thm); 
171 

1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

172 
fun shorter((_,ps,pos,_),(_,qs,qos,_)) = 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

173 
let val ms = length ps and ns = length qs 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

174 
in ms < ns orelse (ms = ns andalso length pos >= length qos) end; 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

175 

c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

176 

c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

177 
(************************************************************ 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

178 
call split_posns with appropriate parameters 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

179 
*************************************************************) 
0  180 

1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset

181 
fun select cmap state i = 
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset

182 
let val goali = nth_subgoal i state 
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset

183 
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

184 
val _ $ t $ _ = Logic.strip_assums_concl goali; 
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset

185 
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

186 

1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

187 

c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

188 
(************************************************************* 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

189 
instantiate lift theorem 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

190 

c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

191 
if t is of the form 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

192 
... ( Const(...,...) $ Abs( .... ) ) ... 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

193 
then 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

194 
P = %a. ... ( Const(...,...) $ a ) ... 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

195 
where a has type T > U 
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 
Ts : types of parameters 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

198 
t : lefthand side of metaequality in subgoal 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

199 
the split theorem is applied to (see cmap) 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

200 
T,U,pos : see mk_split_pack 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

201 
state : current proof state 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

202 
lift : the lift theorem 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

203 
i : no. of subgoal 
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 

1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset

206 
fun inst_lift Ts t (T,U,pos) state lift i = 
0  207 
let val sg = #sign(rep_thm state) 
208 
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

209 
val cntxt = mk_cntxt Ts t pos (T>U) (#maxidx(rep_thm lift)) 
231  210 
val cu = cterm_of sg cntxt 
211 
val uT = #T(rep_cterm cu) 

212 
val cP' = cterm_of sg (Var(P,uT)) 

0  213 
val ixnTs = Type.typ_match tsig ([],(PT,uT)); 
231  214 
val ixncTs = map (fn (x,y) => (x,ctyp_of sg y)) ixnTs; 
0  215 
in instantiate (ixncTs, [(cP',cu)]) lift end; 
216 

217 

1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

218 
(************************************************************* 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

219 
instantiate split theorem 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

220 

c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

221 
Ts : types of parameters 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

222 
t : lefthand side of metaequality in subgoal 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

223 
the split theorem is applied to (see cmap) 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

224 
pos : "path" to the body of P(...) 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

225 
thm : the split theorem 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

226 
TB : type of body of P(...) 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

227 
state : current proof state 
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 

c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

230 
fun inst_split Ts t pos thm TB state = 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

231 
let val _$((Var(P2,PT2))$_)$_ = concl_of thm 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

232 
val sg = #sign(rep_thm state) 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

233 
val tsig = #tsig(Sign.rep_sg sg) 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

234 
val cntxt = mk_cntxt_splitthm Ts t pos TB (#maxidx(rep_thm thm)) 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

235 
val cu = cterm_of sg cntxt 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

236 
val uT = #T(rep_cterm cu) 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

237 
val cP' = cterm_of sg (Var(P2,uT)) 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

238 
val ixnTs = Type.typ_match tsig ([],(PT2,uT)); 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

239 
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

240 
in instantiate (ixncTs, [(cP',cu)]) thm end; 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

241 

c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

242 

c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

243 
(***************************************************************************** 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

244 
The splittactic 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

245 

c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

246 
splits : list of splittheorems to be tried 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

247 
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

248 
*****************************************************************************) 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

249 

0  250 
fun split_tac [] i = no_tac 
251 
 split_tac splits i = 

1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset

252 
let fun const(thm) = let val _$(t as _$lhs)$_ = concl_of thm 
0  253 
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

254 
in (a,(thm,fastype_of t,length args)) end 
0  255 
val cmap = map const splits; 
1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset

256 
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

257 
fun lift_split state = 
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset

258 
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

259 
in case splits of 
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset

260 
[] => no_tac 
1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

261 
 (thm,apsns,pos,TB)::_ => 
1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset

262 
(case apsns of 
1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

263 
[] => STATE(fn state => rtac (inst_split Ts t pos thm TB state) i) 
1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset

264 
 p::_ => EVERY[STATE(lift Ts t p), 
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset

265 
rtac reflexive_thm (i+1), 
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset

266 
STATE lift_split]) 
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset

267 
end 
0  268 
in STATE(fn thm => 
1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset

269 
if i <= nprems_of thm then rtac iffD i THEN STATE lift_split 
0  270 
else no_tac) 
271 
end; 

272 

273 
in split_tac end; 