author  wenzelm 
Fri, 08 Jan 2021 22:30:32 +0100  
changeset 73110  c87ca43ebd3b 
parent 71007  15129c2f4a33 
child 74295  9a9326a072bb 
permissions  rwrr 
32174  1 
(* Title: Provers/splitter.ML 
4  2 
Author: Tobias Nipkow 
1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset

3 
Copyright 1995 TU Munich 
4  4 

5 
Generic casesplitter, suitable for most logics. 

13157
4a4599f78f18
allowed more general split rules to cope with div/mod 2
nipkow
parents:
10821
diff
changeset

6 
Deals with equalities of the form ?P(f args) = ... 
4a4599f78f18
allowed more general split rules to cope with div/mod 2
nipkow
parents:
10821
diff
changeset

7 
where "f args" must be a firstorder term without duplicate variables. 
0  8 
*) 
9 

5304  10 
signature SPLITTER_DATA = 
11 
sig 

59970  12 
val context : Proof.context 
5553  13 
val mk_eq : thm > thm 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
18988
diff
changeset

14 
val meta_eq_to_iff: thm (* "x == y ==> x = y" *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
18988
diff
changeset

15 
val iffD : thm (* "[ P = Q; Q ] ==> P" *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
18988
diff
changeset

16 
val disjE : thm (* "[ P  Q; P ==> R; Q ==> R ] ==> R" *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
18988
diff
changeset

17 
val conjE : thm (* "[ P & Q; [ P; Q ] ==> R ] ==> R" *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
18988
diff
changeset

18 
val exE : thm (* "[ EX x. P x; !!x. P x ==> Q ] ==> Q" *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
18988
diff
changeset

19 
val contrapos : thm (* "[ ~ Q; P ==> Q ] ==> ~ P" *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
18988
diff
changeset

20 
val contrapos2 : thm (* "[ Q; ~ P ==> ~ Q ] ==> P" *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
18988
diff
changeset

21 
val notnotD : thm (* "~ ~ P ==> P" *) 
63636  22 
val safe_tac : Proof.context > tactic 
5304  23 
end 
24 

25 
signature SPLITTER = 

26 
sig 

20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
18988
diff
changeset

27 
(* somewhat more internal functions *) 
33242  28 
val cmap_of_split_thms: thm list > (string * (typ * term * thm * typ * int) list) list 
29 
val split_posns: (string * (typ * term * thm * typ * int) list) list > 

30 
theory > typ list > term > (thm * (typ * typ * int list) list * int list * typ * term) list 

31 
(* first argument is a "cmap", returns a list of "split packs" *) 

20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
18988
diff
changeset

32 
(* the "real" interface, providing a number of tactics *) 
58956
a816aa3ff391
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents:
58838
diff
changeset

33 
val split_tac : Proof.context > thm list > int > tactic 
a816aa3ff391
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents:
58838
diff
changeset

34 
val split_inside_tac: Proof.context > thm list > int > tactic 
a816aa3ff391
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents:
58838
diff
changeset

35 
val split_asm_tac : Proof.context > thm list > int > tactic 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45620
diff
changeset

36 
val add_split: thm > Proof.context > Proof.context 
63636  37 
val add_split_bang: thm > Proof.context > Proof.context 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45620
diff
changeset

38 
val del_split: thm > Proof.context > Proof.context 
30513  39 
val split_modifiers : Method.modifier parser list 
5304  40 
end; 
41 

32177
bc02c5bfcb5b
renamed functor SplitterFun to Splitter, require explicit theory;
wenzelm
parents:
32174
diff
changeset

42 
functor Splitter(Data: SPLITTER_DATA): SPLITTER = 
17881  43 
struct 
5304  44 

18545  45 
val Const (const_not, _) $ _ = 
59970  46 
Object_Logic.drop_judgment Data.context 
18545  47 
(#1 (Logic.dest_implies (Thm.prop_of Data.notnotD))); 
5304  48 

18545  49 
val Const (const_or , _) $ _ $ _ = 
59970  50 
Object_Logic.drop_judgment Data.context 
18545  51 
(#1 (Logic.dest_implies (Thm.prop_of Data.disjE))); 
52 

59970  53 
val const_Trueprop = Object_Logic.judgment_name Data.context; 
18545  54 

1721
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset

55 

20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
18988
diff
changeset

56 
fun split_format_err () = error "Wrong format for split rule"; 
4668
131989b78417
Little reorganization. Loop tactics have names now.
nipkow
parents:
4519
diff
changeset

57 

59582  58 
fun split_thm_info thm = 
59 
(case Thm.concl_of (Data.mk_eq thm) of 

69593  60 
Const(\<^const_name>\<open>Pure.eq\<close>, _) $ (Var _ $ t) $ c => 
59582  61 
(case strip_comb t of 
62 
(Const p, _) => (p, case c of (Const (s, _) $ _) => s = const_not  _ => false) 

63 
 _ => split_format_err ()) 

64 
 _ => split_format_err ()); 

5304  65 

20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
18988
diff
changeset

66 
fun cmap_of_split_thms thms = 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
18988
diff
changeset

67 
let 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
18988
diff
changeset

68 
val splits = map Data.mk_eq thms 
33242  69 
fun add_thm thm cmap = 
59582  70 
(case Thm.concl_of thm of _ $ (t as _ $ lhs) $ _ => 
33242  71 
(case strip_comb lhs of (Const(a,aT),args) => 
72 
let val info = (aT,lhs,thm,fastype_of t,length args) 

73 
in case AList.lookup (op =) cmap a of 

74 
SOME infos => AList.update (op =) (a, info::infos) cmap 

75 
 NONE => (a,[info])::cmap 

76 
end 

77 
 _ => split_format_err()) 

78 
 _ => split_format_err()) 

20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
18988
diff
changeset

79 
in 
33242  80 
fold add_thm splits [] 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
18988
diff
changeset

81 
end; 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
18988
diff
changeset

82 

54216
c0c453ce70a7
inst_lift now fully instantiates context to avoid problems with loose bound variables
berghofe
parents:
52131
diff
changeset

83 
val abss = fold (Term.abs o pair ""); 
c0c453ce70a7
inst_lift now fully instantiates context to avoid problems with loose bound variables
berghofe
parents:
52131
diff
changeset

84 

20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
18988
diff
changeset

85 
(*  *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
18988
diff
changeset

86 
(* mk_case_split_tac *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
18988
diff
changeset

87 
(*  *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
18988
diff
changeset

88 

5304  89 
fun mk_case_split_tac order = 
0  90 
let 
91 

1686
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 
Create lifttheorem "trlift" : 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

94 

7672
c092e67d12f8
 Fixed bug in mk_split_pack which caused application of expansion theorem
berghofe
parents:
6130
diff
changeset

95 
[ !!x. Q x == R x; P(%x. R x) == C ] ==> P (%x. Q x) == C 
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 
*************************************************************) 
5304  98 

20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
18988
diff
changeset

99 
val meta_iffD = Data.meta_eq_to_iff RS Data.iffD; (* (P == Q) ==> Q ==> P *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
18988
diff
changeset

100 

71007  101 
val lift = Goal.prove_global \<^theory> ["P", "Q", "R"] 
69593  102 
[Syntax.read_prop_global \<^theory>\<open>Pure\<close> "!!x :: 'b. Q(x) == R(x) :: 'c"] 
103 
(Syntax.read_prop_global \<^theory>\<open>Pure\<close> "P(%x. Q(x)) == P(%x. R(x))") 

59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

104 
(fn {context = ctxt, prems} => 
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

105 
rewrite_goals_tac ctxt prems THEN resolve_tac ctxt [reflexive_thm] 1) 
4  106 

59582  107 
val _ $ _ $ (_ $ (_ $ abs_lift) $ _) = Thm.prop_of lift; 
54216
c0c453ce70a7
inst_lift now fully instantiates context to avoid problems with loose bound variables
berghofe
parents:
52131
diff
changeset

108 

0  109 
val trlift = lift RS transitive_thm; 
110 

111 

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

113 
Set up term for instantiation of P in the lifttheorem 
17881  114 

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

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

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

117 
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

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

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

120 

54216
c0c453ce70a7
inst_lift now fully instantiates context to avoid problems with loose bound variables
berghofe
parents:
52131
diff
changeset

121 
fun mk_cntxt t pos T = 
c0c453ce70a7
inst_lift now fully instantiates context to avoid problems with loose bound variables
berghofe
parents:
52131
diff
changeset

122 
let 
c0c453ce70a7
inst_lift now fully instantiates context to avoid problems with loose bound variables
berghofe
parents:
52131
diff
changeset

123 
fun down [] t = (Bound 0, t) 
c0c453ce70a7
inst_lift now fully instantiates context to avoid problems with loose bound variables
berghofe
parents:
52131
diff
changeset

124 
 down (p :: ps) t = 
c0c453ce70a7
inst_lift now fully instantiates context to avoid problems with loose bound variables
berghofe
parents:
52131
diff
changeset

125 
let 
c0c453ce70a7
inst_lift now fully instantiates context to avoid problems with loose bound variables
berghofe
parents:
52131
diff
changeset

126 
val (h, ts) = strip_comb t 
c0c453ce70a7
inst_lift now fully instantiates context to avoid problems with loose bound variables
berghofe
parents:
52131
diff
changeset

127 
val (ts1, u :: ts2) = chop p ts 
c0c453ce70a7
inst_lift now fully instantiates context to avoid problems with loose bound variables
berghofe
parents:
52131
diff
changeset

128 
val (u1, u2) = down ps u 
c0c453ce70a7
inst_lift now fully instantiates context to avoid problems with loose bound variables
berghofe
parents:
52131
diff
changeset

129 
in 
c0c453ce70a7
inst_lift now fully instantiates context to avoid problems with loose bound variables
berghofe
parents:
52131
diff
changeset

130 
(list_comb (incr_boundvars 1 h, 
c0c453ce70a7
inst_lift now fully instantiates context to avoid problems with loose bound variables
berghofe
parents:
52131
diff
changeset

131 
map (incr_boundvars 1) ts1 @ u1 :: 
c0c453ce70a7
inst_lift now fully instantiates context to avoid problems with loose bound variables
berghofe
parents:
52131
diff
changeset

132 
map (incr_boundvars 1) ts2), 
c0c453ce70a7
inst_lift now fully instantiates context to avoid problems with loose bound variables
berghofe
parents:
52131
diff
changeset

133 
u2) 
c0c453ce70a7
inst_lift now fully instantiates context to avoid problems with loose bound variables
berghofe
parents:
52131
diff
changeset

134 
end; 
c0c453ce70a7
inst_lift now fully instantiates context to avoid problems with loose bound variables
berghofe
parents:
52131
diff
changeset

135 
val (u1, u2) = down (rev pos) t 
c0c453ce70a7
inst_lift now fully instantiates context to avoid problems with loose bound variables
berghofe
parents:
52131
diff
changeset

136 
in (Abs ("", T, u1), u2) end; 
1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset

137 

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

138 

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

140 
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

141 
P(...) == rhs 
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 
t : lefthand side of metaequality in subgoal 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

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

145 
T : type of body of P(...) 
4232  146 
tt : the term Const(key,..) $ ... 
1686
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 

4232  149 
fun mk_cntxt_splitthm t tt T = 
150 
let fun repl lev t = 

52131  151 
if Envir.aeconv(incr_boundvars lev tt, t) then Bound lev 
4232  152 
else case t of 
153 
(Abs (v, T2, t)) => Abs (v, T2, repl (lev+1) t) 

154 
 (Bound i) => Bound (if i>=lev then i+1 else i) 

155 
 (t1 $ t2) => (repl lev t1) $ (repl lev t2) 

156 
 t => t 

157 
in Abs("", T, repl 0 t) end; 

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

158 

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 
(* add all loose bound variables in t to list is *) 
33245  161 
fun add_lbnos t is = add_loose_bnos (t, 0, is); 
1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset

162 

7672
c092e67d12f8
 Fixed bug in mk_split_pack which caused application of expansion theorem
berghofe
parents:
6130
diff
changeset

163 
(* check if the innermost abstraction that needs to be removed 
1064  164 
has a body of type T; otherwise the expansion thm will fail later on 
165 
*) 

33029  166 
fun type_test (T, lbnos, apsns) = 
42364  167 
let val (_, U: typ, _) = nth apsns (foldl1 Int.min lbnos) 
33029  168 
in T = U end; 
0  169 

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

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

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

172 

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

173 
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

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

175 
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

176 
T : type of P(...) 
7672
c092e67d12f8
 Fixed bug in mk_split_pack which caused application of expansion theorem
berghofe
parents:
6130
diff
changeset

177 
T' : type of term to be scanned 
1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

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

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

180 
apsns : list of tuples of the form (T,U,pos), one tuple for each 
17881  181 
abstraction that is encountered on the way to the position where 
1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

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

183 
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

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

185 
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

186 
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

187 
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

188 
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

189 

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

190 
A split pack is a tuple of the form 
7672
c092e67d12f8
 Fixed bug in mk_split_pack which caused application of expansion theorem
berghofe
parents:
6130
diff
changeset

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

192 
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

193 
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

194 
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

195 
lifting is required before applying the splittheorem. 
17881  196 
******************************************************************************) 
1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

197 

20664  198 
fun mk_split_pack (thm, T: typ, T', n, ts, apsns, pos, TB, t) = 
1064  199 
if n > length ts then [] 
200 
else let val lev = length apsns 

33955  201 
val lbnos = fold add_lbnos (take n ts) [] 
33317  202 
val flbnos = filter (fn i => i < lev) lbnos 
4232  203 
val tt = incr_boundvars (~lev) t 
7672
c092e67d12f8
 Fixed bug in mk_split_pack which caused application of expansion theorem
berghofe
parents:
6130
diff
changeset

204 
in if null flbnos then 
c092e67d12f8
 Fixed bug in mk_split_pack which caused application of expansion theorem
berghofe
parents:
6130
diff
changeset

205 
if T = T' then [(thm,[],pos,TB,tt)] else [] 
c092e67d12f8
 Fixed bug in mk_split_pack which caused application of expansion theorem
berghofe
parents:
6130
diff
changeset

206 
else if type_test(T,flbnos,apsns) then [(thm, rev apsns,pos,TB,tt)] 
2143  207 
else [] 
1064  208 
end; 
0  209 

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

210 

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

211 
(**************************************************************************** 
58318  212 
Recursively scans term for occurrences of Const(key,...) $ ... 
213 
Returns a list of "splitpacks" (one for each occurrence of Const(key,...) ) 

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

214 

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

215 
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

216 
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

217 
key : the theorem's key constant ( Const(key,...) $ ... ) 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

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

219 
T : type of P( Const(key,...) $ ... ) 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

220 
n : number of arguments expected by Const(key,...) 
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 : the term to be scanned 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

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

224 

13157
4a4599f78f18
allowed more general split rules to cope with div/mod 2
nipkow
parents:
10821
diff
changeset

225 
(* Simplified firstorder matching; 
4a4599f78f18
allowed more general split rules to cope with div/mod 2
nipkow
parents:
10821
diff
changeset

226 
assumes that all Vars in the pattern are distinct; 
4a4599f78f18
allowed more general split rules to cope with div/mod 2
nipkow
parents:
10821
diff
changeset

227 
see Pure/pattern.ML for the full version; 
4a4599f78f18
allowed more general split rules to cope with div/mod 2
nipkow
parents:
10821
diff
changeset

228 
*) 
4a4599f78f18
allowed more general split rules to cope with div/mod 2
nipkow
parents:
10821
diff
changeset

229 
local 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
18988
diff
changeset

230 
exception MATCH 
13157
4a4599f78f18
allowed more general split rules to cope with div/mod 2
nipkow
parents:
10821
diff
changeset

231 
in 
42367
577d85fb5862
more direct Thm.cprem_of (with exception THM instead of Subscript);
wenzelm
parents:
42364
diff
changeset

232 
fun typ_match thy (tyenv, TU) = Sign.typ_match thy TU tyenv 
577d85fb5862
more direct Thm.cprem_of (with exception THM instead of Subscript);
wenzelm
parents:
42364
diff
changeset

233 
handle Type.TYPE_MATCH => raise MATCH; 
33242  234 

42367
577d85fb5862
more direct Thm.cprem_of (with exception THM instead of Subscript);
wenzelm
parents:
42364
diff
changeset

235 
fun fomatch thy args = 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
18988
diff
changeset

236 
let 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
18988
diff
changeset

237 
fun mtch tyinsts = fn 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
18988
diff
changeset

238 
(Ts, Var(_,T), t) => 
42367
577d85fb5862
more direct Thm.cprem_of (with exception THM instead of Subscript);
wenzelm
parents:
42364
diff
changeset

239 
typ_match thy (tyinsts, (T, fastype_of1(Ts,t))) 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
18988
diff
changeset

240 
 (_, Free (a,T), Free (b,U)) => 
42367
577d85fb5862
more direct Thm.cprem_of (with exception THM instead of Subscript);
wenzelm
parents:
42364
diff
changeset

241 
if a=b then typ_match thy (tyinsts,(T,U)) else raise MATCH 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
18988
diff
changeset

242 
 (_, Const (a,T), Const (b,U)) => 
42367
577d85fb5862
more direct Thm.cprem_of (with exception THM instead of Subscript);
wenzelm
parents:
42364
diff
changeset

243 
if a=b then typ_match thy (tyinsts,(T,U)) else raise MATCH 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
18988
diff
changeset

244 
 (_, Bound i, Bound j) => 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
18988
diff
changeset

245 
if i=j then tyinsts else raise MATCH 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
18988
diff
changeset

246 
 (Ts, Abs(_,T,t), Abs(_,U,u)) => 
42367
577d85fb5862
more direct Thm.cprem_of (with exception THM instead of Subscript);
wenzelm
parents:
42364
diff
changeset

247 
mtch (typ_match thy (tyinsts,(T,U))) (U::Ts,t,u) 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
18988
diff
changeset

248 
 (Ts, f$t, g$u) => 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
18988
diff
changeset

249 
mtch (mtch tyinsts (Ts,f,g)) (Ts, t, u) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
18988
diff
changeset

250 
 _ => raise MATCH 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
18988
diff
changeset

251 
in (mtch Vartab.empty args; true) handle MATCH => false end; 
33242  252 
end; 
13157
4a4599f78f18
allowed more general split rules to cope with div/mod 2
nipkow
parents:
10821
diff
changeset

253 

42367
577d85fb5862
more direct Thm.cprem_of (with exception THM instead of Subscript);
wenzelm
parents:
42364
diff
changeset

254 
fun split_posns (cmap : (string * (typ * term * thm * typ * int) list) list) thy Ts t = 
6130
30b84ad2131d
Fixed old bug: selection of constant to be split should depend not just on
nipkow
parents:
5553
diff
changeset

255 
let 
7672
c092e67d12f8
 Fixed bug in mk_split_pack which caused application of expansion theorem
berghofe
parents:
6130
diff
changeset

256 
val T' = fastype_of1 (Ts, t); 
c092e67d12f8
 Fixed bug in mk_split_pack which caused application of expansion theorem
berghofe
parents:
6130
diff
changeset

257 
fun posns Ts pos apsns (Abs (_, T, t)) = 
c092e67d12f8
 Fixed bug in mk_split_pack which caused application of expansion theorem
berghofe
parents:
6130
diff
changeset

258 
let val U = fastype_of1 (T::Ts,t) 
c092e67d12f8
 Fixed bug in mk_split_pack which caused application of expansion theorem
berghofe
parents:
6130
diff
changeset

259 
in posns (T::Ts) (0::pos) ((T, U, pos)::apsns) t end 
6130
30b84ad2131d
Fixed old bug: selection of constant to be split should depend not just on
nipkow
parents:
5553
diff
changeset

260 
 posns Ts pos apsns t = 
30b84ad2131d
Fixed old bug: selection of constant to be split should depend not just on
nipkow
parents:
5553
diff
changeset

261 
let 
7672
c092e67d12f8
 Fixed bug in mk_split_pack which caused application of expansion theorem
berghofe
parents:
6130
diff
changeset

262 
val (h, ts) = strip_comb t 
33245  263 
fun iter t (i, a) = (i+1, (posns Ts (i::pos) apsns t) @ a); 
264 
val a = 

265 
case h of 

266 
Const(c, cT) => 

267 
let fun find [] = [] 

268 
 find ((gcT, pat, thm, T, n)::tups) = 

42367
577d85fb5862
more direct Thm.cprem_of (with exception THM instead of Subscript);
wenzelm
parents:
42364
diff
changeset

269 
let val t2 = list_comb (h, take n ts) in 
577d85fb5862
more direct Thm.cprem_of (with exception THM instead of Subscript);
wenzelm
parents:
42364
diff
changeset

270 
if Sign.typ_instance thy (cT, gcT) andalso fomatch thy (Ts, pat, t2) 
577d85fb5862
more direct Thm.cprem_of (with exception THM instead of Subscript);
wenzelm
parents:
42364
diff
changeset

271 
then mk_split_pack(thm,T,T',n,ts,apsns,pos,type_of1(Ts,t2),t2) 
577d85fb5862
more direct Thm.cprem_of (with exception THM instead of Subscript);
wenzelm
parents:
42364
diff
changeset

272 
else find tups 
33245  273 
end 
274 
in find (these (AList.lookup (op =) cmap c)) end 

275 
 _ => [] 

276 
in snd (fold iter ts (0, a)) end 

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

277 
in posns Ts [] [] t end; 
0  278 

20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
18988
diff
changeset

279 
fun shorter ((_,ps,pos,_,_), (_,qs,qos,_,_)) = 
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58956
diff
changeset

280 
prod_ord (int_ord o apply2 length) (order o apply2 length) 
4519  281 
((ps, pos), (qs, qos)); 
282 

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

283 

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

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

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

286 
*************************************************************) 
0  287 

60362  288 
fun select thy cmap state i = 
42367
577d85fb5862
more direct Thm.cprem_of (with exception THM instead of Subscript);
wenzelm
parents:
42364
diff
changeset

289 
let 
59582  290 
val goal = Thm.term_of (Thm.cprem_of state i); 
42367
577d85fb5862
more direct Thm.cprem_of (with exception THM instead of Subscript);
wenzelm
parents:
42364
diff
changeset

291 
val Ts = rev (map #2 (Logic.strip_params goal)); 
577d85fb5862
more direct Thm.cprem_of (with exception THM instead of Subscript);
wenzelm
parents:
42364
diff
changeset

292 
val _ $ t $ _ = Logic.strip_assums_concl goal; 
577d85fb5862
more direct Thm.cprem_of (with exception THM instead of Subscript);
wenzelm
parents:
42364
diff
changeset

293 
in (Ts, t, sort shorter (split_posns cmap thy Ts t)) end; 
1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset

294 

42367
577d85fb5862
more direct Thm.cprem_of (with exception THM instead of Subscript);
wenzelm
parents:
42364
diff
changeset

295 
fun exported_split_posns cmap thy Ts t = 
577d85fb5862
more direct Thm.cprem_of (with exception THM instead of Subscript);
wenzelm
parents:
42364
diff
changeset

296 
sort shorter (split_posns cmap thy Ts t); 
1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

297 

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

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

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

300 

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

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

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

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

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

305 
where a has type T > U 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

306 

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

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

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

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

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

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

312 
i : no. of subgoal 
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

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

314 

60362  315 
fun inst_lift ctxt Ts t (T, U, pos) state i = 
7672
c092e67d12f8
 Fixed bug in mk_split_pack which caused application of expansion theorem
berghofe
parents:
6130
diff
changeset

316 
let 
54216
c0c453ce70a7
inst_lift now fully instantiates context to avoid problems with loose bound variables
berghofe
parents:
52131
diff
changeset

317 
val (cntxt, u) = mk_cntxt t pos (T > U); 
c0c453ce70a7
inst_lift now fully instantiates context to avoid problems with loose bound variables
berghofe
parents:
52131
diff
changeset

318 
val trlift' = Thm.lift_rule (Thm.cprem_of state i) 
c0c453ce70a7
inst_lift now fully instantiates context to avoid problems with loose bound variables
berghofe
parents:
52131
diff
changeset

319 
(Thm.rename_boundvars abs_lift u trlift); 
60781  320 
val (Var (P, _), _) = 
321 
strip_comb (fst (Logic.dest_equals 

322 
(Logic.strip_assums_concl (Thm.prop_of trlift')))); 

323 
in infer_instantiate ctxt [(P, Thm.cterm_of ctxt (abss Ts cntxt))] trlift' end; 

0  324 

325 

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

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

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

328 

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

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

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

331 
the split theorem is applied to (see cmap) 
4232  332 
tt : the term Const(key,..) $ ... 
1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

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

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

335 
state : current proof state 
4232  336 
i : number of subgoal 
1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

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

338 

60362  339 
fun inst_split ctxt Ts t tt thm TB state i = 
17881  340 
let 
18145  341 
val thm' = Thm.lift_rule (Thm.cprem_of state i) thm; 
60781  342 
val (Var (P, _), _) = 
343 
strip_comb (fst (Logic.dest_equals 

344 
(Logic.strip_assums_concl (Thm.prop_of thm')))); 

7672
c092e67d12f8
 Fixed bug in mk_split_pack which caused application of expansion theorem
berghofe
parents:
6130
diff
changeset

345 
val cntxt = mk_cntxt_splitthm t tt TB; 
60781  346 
in infer_instantiate ctxt [(P, Thm.cterm_of ctxt (abss Ts cntxt))] thm' end; 
1686
c67d543bc395
Added functions mk_cntxt_splitthm and inst_split which instantiate
berghofe
parents:
1064
diff
changeset

347 

7672
c092e67d12f8
 Fixed bug in mk_split_pack which caused application of expansion theorem
berghofe
parents:
6130
diff
changeset

348 

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

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

350 
The splittactic 
17881  351 

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

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

353 
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

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

355 

58956
a816aa3ff391
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents:
58838
diff
changeset

356 
fun split_tac _ [] i = no_tac 
a816aa3ff391
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents:
58838
diff
changeset

357 
 split_tac ctxt splits i = 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
18988
diff
changeset

358 
let val cmap = cmap_of_split_thms splits 
60362  359 
fun lift_tac Ts t p st = compose_tac ctxt (false, inst_lift ctxt Ts t p st i, 2) i st 
7672
c092e67d12f8
 Fixed bug in mk_split_pack which caused application of expansion theorem
berghofe
parents:
6130
diff
changeset

360 
fun lift_split_tac state = 
60362  361 
let val (Ts, t, splits) = select (Proof_Context.theory_of ctxt) cmap state i 
1030
1d8fa2fc4b9c
Completely rewrote split_tac. The old one failed in strange circumstances.
nipkow
parents:
943
diff
changeset

362 
in case splits of 
7672
c092e67d12f8
 Fixed bug in mk_split_pack which caused application of expansion theorem
berghofe
parents:
6130
diff
changeset

363 
[] => no_tac state 
c092e67d12f8
 Fixed bug in mk_split_pack which caused application of expansion theorem
berghofe
parents:
6130
diff
changeset

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

365 
(case apsns of 
60362  366 
[] => 
367 
compose_tac ctxt (false, inst_split ctxt Ts t tt thm TB state i, 0) i state 

7672
c092e67d12f8
 Fixed bug in mk_split_pack which caused application of expansion theorem
berghofe
parents:
6130
diff
changeset

368 
 p::_ => EVERY [lift_tac Ts t p, 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

369 
resolve_tac ctxt [reflexive_thm] (i+1), 
7672
c092e67d12f8
 Fixed bug in mk_split_pack which caused application of expansion theorem
berghofe
parents:
6130
diff
changeset

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

371 
end 
17881  372 
in COND (has_fewer_prems i) no_tac 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

373 
(resolve_tac ctxt [meta_iffD] i THEN lift_split_tac) 
0  374 
end; 
375 

20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
18988
diff
changeset

376 
in (split_tac, exported_split_posns) end; (* mk_case_split_tac *) 
1721
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset

377 

5304  378 

33242  379 
val (split_tac, split_posns) = mk_case_split_tac int_ord; 
4189  380 

33242  381 
val (split_inside_tac, _) = mk_case_split_tac (rev_order o int_ord); 
5304  382 

4189  383 

384 
(***************************************************************************** 

385 
The splittactic for premises 

17881  386 

4189  387 
splits : list of splittheorems to be tried 
5304  388 
****************************************************************************) 
58956
a816aa3ff391
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents:
58838
diff
changeset

389 
fun split_asm_tac _ [] = K no_tac 
a816aa3ff391
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents:
58838
diff
changeset

390 
 split_asm_tac ctxt splits = 
5304  391 

13855
644692eca537
addsplits / delsplits no longer ignore type of constant.
berghofe
parents:
13157
diff
changeset

392 
let val cname_list = map (fst o fst o split_thm_info) splits; 
17881  393 
fun tac (t,i) = 
20664  394 
let val n = find_index (exists_Const (member (op =) cname_list o #1)) 
17881  395 
(Logic.strip_assums_hyp t); 
69593  396 
fun first_prem_is_disj (Const (\<^const_name>\<open>Pure.imp\<close>, _) $ (Const (c, _) 
18545  397 
$ (Const (s, _) $ _ $ _ )) $ _ ) = c = const_Trueprop andalso s = const_or 
69593  398 
 first_prem_is_disj (Const(\<^const_name>\<open>Pure.all\<close>,_)$Abs(_,_,t)) = 
17881  399 
first_prem_is_disj t 
400 
 first_prem_is_disj _ = false; 

20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
18988
diff
changeset

401 
(* does not work properly if the split variable is bound by a quantifier *) 
17881  402 
fun flat_prems_tac i = SUBGOAL (fn (t,i) => 
403 
(if first_prem_is_disj t 

59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

404 
then EVERY[eresolve_tac ctxt [Data.disjE] i, rotate_tac ~1 i, 
17881  405 
rotate_tac ~1 (i+1), 
406 
flat_prems_tac (i+1)] 

407 
else all_tac) 

59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

408 
THEN REPEAT (eresolve_tac ctxt [Data.conjE,Data.exE] i) 
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

409 
THEN REPEAT (dresolve_tac ctxt [Data.notnotD] i)) i; 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
18988
diff
changeset

410 
in if n<0 then no_tac else (DETERM (EVERY' 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

411 
[rotate_tac n, eresolve_tac ctxt [Data.contrapos2], 
58956
a816aa3ff391
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents:
58838
diff
changeset

412 
split_tac ctxt splits, 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

413 
rotate_tac ~1, eresolve_tac ctxt [Data.contrapos], rotate_tac ~1, 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
18988
diff
changeset

414 
flat_prems_tac] i)) 
17881  415 
end; 
4189  416 
in SUBGOAL tac 
417 
end; 

418 

58956
a816aa3ff391
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents:
58838
diff
changeset

419 
fun gen_split_tac _ [] = K no_tac 
a816aa3ff391
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents:
58838
diff
changeset

420 
 gen_split_tac ctxt (split::splits) = 
10652  421 
let val (_,asm) = split_thm_info split 
58956
a816aa3ff391
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents:
58838
diff
changeset

422 
in (if asm then split_asm_tac else split_tac) ctxt [split] ORELSE' 
a816aa3ff391
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents:
58838
diff
changeset

423 
gen_split_tac ctxt splits 
10652  424 
end; 
8468  425 

18688  426 

8468  427 
(** declare split rules **) 
428 

45620
f2a587696afb
modernized some oldstyle infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
42367
diff
changeset

429 
(* add_split / del_split *) 
8468  430 

33242  431 
fun string_of_typ (Type (s, Ts)) = 
432 
(if null Ts then "" else enclose "(" ")" (commas (map string_of_typ Ts))) ^ s 

13859
adf68d9e5dec
split_name no longer uses Sign.string_of_typ to encode types, since
berghofe
parents:
13855
diff
changeset

433 
 string_of_typ _ = "_"; 
adf68d9e5dec
split_name no longer uses Sign.string_of_typ to encode types, since
berghofe
parents:
13855
diff
changeset

434 

17881  435 
fun split_name (name, T) asm = "split " ^ 
13859
adf68d9e5dec
split_name no longer uses Sign.string_of_typ to encode types, since
berghofe
parents:
13855
diff
changeset

436 
(if asm then "asm " else "") ^ name ^ " :: " ^ string_of_typ T; 
4189  437 

63636  438 
fun gen_add_split bang split ctxt = 
33242  439 
let 
45620
f2a587696afb
modernized some oldstyle infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
42367
diff
changeset

440 
val (name, asm) = split_thm_info split 
67644  441 
val split0 = Thm.trim_context split 
63636  442 
fun tac ctxt' = 
67649  443 
let val split' = Thm.transfer' ctxt' split0 in 
67644  444 
(if asm then split_asm_tac ctxt' [split'] 
445 
else if bang 

446 
then split_tac ctxt' [split'] THEN_ALL_NEW 

447 
TRY o (SELECT_GOAL (Data.safe_tac ctxt')) 

448 
else split_tac ctxt' [split']) 

449 
end 

58956
a816aa3ff391
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents:
58838
diff
changeset

450 
in Simplifier.addloop (ctxt, (split_name name asm, tac)) end; 
1721
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset

451 

63636  452 
val add_split = gen_add_split false; 
453 
val add_split_bang = gen_add_split true; 

454 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45620
diff
changeset

455 
fun del_split split ctxt = 
45620
f2a587696afb
modernized some oldstyle infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
42367
diff
changeset

456 
let val (name, asm) = split_thm_info split 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45620
diff
changeset

457 
in Simplifier.delloop (ctxt, split_name name asm) end; 
1721
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset

458 

8468  459 

460 
(* attributes *) 

461 

462 
val splitN = "split"; 

463 

63636  464 
fun split_add bang = Simplifier.attrib (gen_add_split bang); 
45620
f2a587696afb
modernized some oldstyle infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
42367
diff
changeset

465 
val split_del = Simplifier.attrib del_split; 
8634  466 

63650  467 
val add_del = Scan.lift 
468 
(Args.bang >> K (split_add true) 

469 
 Args.del >> K split_del 

470 
 Scan.succeed (split_add false)); 

63636  471 

472 
val _ = Theory.setup 

69593  473 
(Attrib.setup \<^binding>\<open>split\<close> add_del "declare case split rule"); 
58826  474 

8634  475 

9703  476 
(* methods *) 
8468  477 

478 
val split_modifiers = 

64556  479 
[Args.$$$ splitN  Args.colon >> K (Method.modifier (split_add false) \<^here>), 
480 
Args.$$$ splitN  Args.bang_colon >> K (Method.modifier (split_add true) \<^here>), 

481 
Args.$$$ splitN  Args.del  Args.colon >> K (Method.modifier split_del \<^here>)]; 

8468  482 

58826  483 
val _ = 
484 
Theory.setup 

69593  485 
(Method.setup \<^binding>\<open>split\<close> 
58956
a816aa3ff391
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents:
58838
diff
changeset

486 
(Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (CHANGED_PROP o gen_split_tac ctxt ths))) 
58826  487 
"apply case split rule"); 
4189  488 

1721
445654b6cb95
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
berghofe
parents:
1686
diff
changeset

489 
end; 