73 in prove_goalw_cterm [] ct |
73 in prove_goalw_cterm [] ct |
74 (fn [prem] => [rewtac prem, rtac reflexive_thm 1]) |
74 (fn [prem] => [rewtac prem, rtac reflexive_thm 1]) |
75 end; |
75 end; |
76 |
76 |
77 val trlift = lift RS transitive_thm; |
77 val trlift = lift RS transitive_thm; |
78 val _ $ (Var(P,PT)$_) $ _ = concl_of trlift; |
78 val _ $ (P $ _) $ _ = concl_of trlift; |
79 |
79 |
80 |
80 |
81 (************************************************************************ |
81 (************************************************************************ |
82 Set up term for instantiation of P in the lift-theorem |
82 Set up term for instantiation of P in the lift-theorem |
83 |
83 |
111 tt : the term Const(key,..) $ ... |
111 tt : the term Const(key,..) $ ... |
112 *************************************************************************) |
112 *************************************************************************) |
113 |
113 |
114 fun mk_cntxt_splitthm t tt T = |
114 fun mk_cntxt_splitthm t tt T = |
115 let fun repl lev t = |
115 let fun repl lev t = |
116 if incr_boundvars lev tt = t then Bound lev |
116 if incr_boundvars lev tt aconv t then Bound lev |
117 else case t of |
117 else case t of |
118 (Abs (v, T2, t)) => Abs (v, T2, repl (lev+1) t) |
118 (Abs (v, T2, t)) => Abs (v, T2, repl (lev+1) t) |
119 | (Bound i) => Bound (if i>=lev then i+1 else i) |
119 | (Bound i) => Bound (if i>=lev then i+1 else i) |
120 | (t1 $ t2) => (repl lev t1) $ (repl lev t2) |
120 | (t1 $ t2) => (repl lev t1) $ (repl lev t2) |
121 | t => t |
121 | t => t |
123 |
123 |
124 |
124 |
125 (* add all loose bound variables in t to list is *) |
125 (* add all loose bound variables in t to list is *) |
126 fun add_lbnos(is,t) = add_loose_bnos(t,0,is); |
126 fun add_lbnos(is,t) = add_loose_bnos(t,0,is); |
127 |
127 |
128 (* check if the innermost quantifier that needs to be removed |
128 (* check if the innermost abstraction that needs to be removed |
129 has a body of type T; otherwise the expansion thm will fail later on |
129 has a body of type T; otherwise the expansion thm will fail later on |
130 *) |
130 *) |
131 fun type_test(T,lbnos,apsns) = |
131 fun type_test(T,lbnos,apsns) = |
132 let val (_,U,_) = nth_elem(foldl Int.min (hd lbnos, tl lbnos), apsns) |
132 let val (_,U,_) = nth_elem(foldl Int.min (hd lbnos, tl lbnos), apsns) |
133 in T=U end; |
133 in T=U end; |
137 |
137 |
138 thm : the relevant split-theorem, i.e. P(...) == rhs , where P(...) |
138 thm : the relevant split-theorem, i.e. P(...) == rhs , where P(...) |
139 is of the form |
139 is of the form |
140 P( Const(key,...) $ t_1 $ ... $ t_n ) (e.g. key = "if") |
140 P( Const(key,...) $ t_1 $ ... $ t_n ) (e.g. key = "if") |
141 T : type of P(...) |
141 T : type of P(...) |
|
142 T' : type of term to be scanned |
142 n : number of arguments expected by Const(key,...) |
143 n : number of arguments expected by Const(key,...) |
143 ts : list of arguments actually found |
144 ts : list of arguments actually found |
144 apsns : list of tuples of the form (T,U,pos), one tuple for each |
145 apsns : list of tuples of the form (T,U,pos), one tuple for each |
145 abstraction that is encountered on the way to the position where |
146 abstraction that is encountered on the way to the position where |
146 Const(key, ...) $ ... occurs, where |
147 Const(key, ...) $ ... occurs, where |
150 pos : "path" leading to the position where Const(key, ...) $ ... occurs. |
151 pos : "path" leading to the position where Const(key, ...) $ ... occurs. |
151 TB : type of Const(key,...) $ t_1 $ ... $ t_n |
152 TB : type of Const(key,...) $ t_1 $ ... $ t_n |
152 t : the term Const(key,...) $ t_1 $ ... $ t_n |
153 t : the term Const(key,...) $ t_1 $ ... $ t_n |
153 |
154 |
154 A split pack is a tuple of the form |
155 A split pack is a tuple of the form |
155 (thm, apsns, pos, TB) |
156 (thm, apsns, pos, TB, tt) |
156 Note : apsns is reversed, so that the outermost quantifier's position |
157 Note : apsns is reversed, so that the outermost quantifier's position |
157 comes first ! If the terms in ts don't contain variables bound |
158 comes first ! If the terms in ts don't contain variables bound |
158 by other than meta-quantifiers, apsns is empty, because no further |
159 by other than meta-quantifiers, apsns is empty, because no further |
159 lifting is required before applying the split-theorem. |
160 lifting is required before applying the split-theorem. |
160 ******************************************************************************) |
161 ******************************************************************************) |
161 |
162 |
162 fun mk_split_pack(thm,T,n,ts,apsns,pos,TB,t) = |
163 fun mk_split_pack(thm, T, T', n, ts, apsns, pos, TB, t) = |
163 if n > length ts then [] |
164 if n > length ts then [] |
164 else let val lev = length apsns |
165 else let val lev = length apsns |
165 val lbnos = foldl add_lbnos ([],take(n,ts)) |
166 val lbnos = foldl add_lbnos ([],take(n,ts)) |
166 val flbnos = filter (fn i => i < lev) lbnos |
167 val flbnos = filter (fn i => i < lev) lbnos |
167 val tt = incr_boundvars (~lev) t |
168 val tt = incr_boundvars (~lev) t |
168 in if null flbnos then [(thm,[],pos,TB,tt)] |
169 in if null flbnos then |
169 else if type_test(T,flbnos,apsns) then [(thm, rev apsns,pos,TB,tt)] |
170 if T = T' then [(thm,[],pos,TB,tt)] else [] |
|
171 else if type_test(T,flbnos,apsns) then [(thm, rev apsns,pos,TB,tt)] |
170 else [] |
172 else [] |
171 end; |
173 end; |
172 |
174 |
173 |
175 |
174 (**************************************************************************** |
176 (**************************************************************************** |
185 t : the term to be scanned |
187 t : the term to be scanned |
186 ******************************************************************************) |
188 ******************************************************************************) |
187 |
189 |
188 fun split_posns cmap sg Ts t = |
190 fun split_posns cmap sg Ts t = |
189 let |
191 let |
190 fun posns Ts pos apsns (Abs(_,T,t)) = |
192 val T' = fastype_of1 (Ts, t); |
191 let val U = fastype_of1(T::Ts,t) |
193 fun posns Ts pos apsns (Abs (_, T, t)) = |
192 in posns (T::Ts) (0::pos) ((T,U,pos)::apsns) t end |
194 let val U = fastype_of1 (T::Ts,t) |
|
195 in posns (T::Ts) (0::pos) ((T, U, pos)::apsns) t end |
193 | posns Ts pos apsns t = |
196 | posns Ts pos apsns t = |
194 let |
197 let |
195 val (h,ts) = strip_comb t |
198 val (h, ts) = strip_comb t |
196 fun iter((i,a),t) = (i+1, (posns Ts (i::pos) apsns t) @ a); |
199 fun iter((i, a), t) = (i+1, (posns Ts (i::pos) apsns t) @ a); |
197 val a = case h of |
200 val a = case h of |
198 Const(c,cT) => |
201 Const(c, cT) => |
199 (case assoc(cmap,c) of |
202 (case assoc(cmap, c) of |
200 Some(gcT, thm, T, n) => |
203 Some(gcT, thm, T, n) => |
201 if Type.typ_instance(Sign.tsig_of sg, cT, gcT) |
204 if Type.typ_instance(Sign.tsig_of sg, cT, gcT) |
202 then |
205 then |
203 let val t2 = list_comb (h, take (n, ts)) |
206 let val t2 = list_comb (h, take (n, ts)) |
204 in mk_split_pack(thm,T,n,ts,apsns,pos,type_of1(Ts, t2),t2) |
207 in mk_split_pack (thm, T, T', n, ts, apsns, pos, type_of1 (Ts, t2), t2) |
205 end |
208 end |
206 else [] |
209 else [] |
207 | None => []) |
210 | None => []) |
208 | _ => [] |
211 | _ => [] |
209 in snd(foldl iter ((0,a),ts)) end |
212 in snd(foldl iter ((0, a), ts)) end |
210 in posns Ts [] [] t end; |
213 in posns Ts [] [] t end; |
211 |
214 |
212 |
215 |
213 fun nth_subgoal i thm = nth_elem(i-1,prems_of thm); |
216 fun nth_subgoal i thm = nth_elem(i-1,prems_of thm); |
214 |
217 |
246 state : current proof state |
249 state : current proof state |
247 lift : the lift theorem |
250 lift : the lift theorem |
248 i : no. of subgoal |
251 i : no. of subgoal |
249 **************************************************************) |
252 **************************************************************) |
250 |
253 |
251 fun inst_lift Ts t (T,U,pos) state lift i = |
254 fun inst_lift Ts t (T, U, pos) state i = |
252 let val sg = #sign(rep_thm state) |
255 let |
253 val tsig = #tsig(Sign.rep_sg sg) |
256 val cert = cterm_of (sign_of_thm state); |
254 val cntxt = mk_cntxt Ts t pos (T-->U) (#maxidx(rep_thm lift)) |
257 val cntxt = mk_cntxt Ts t pos (T --> U) (#maxidx(rep_thm trlift)); |
255 val cu = cterm_of sg cntxt |
258 in cterm_instantiate [(cert P, cert cntxt)] trlift |
256 val uT = #T(rep_cterm cu) |
259 end; |
257 val cP' = cterm_of sg (Var(P,uT)) |
|
258 val ixnTs = Type.typ_match tsig ([],(PT,uT)); |
|
259 val ixncTs = map (fn (x,y) => (x,ctyp_of sg y)) ixnTs; |
|
260 in instantiate (ixncTs, [(cP',cu)]) lift end; |
|
261 |
260 |
262 |
261 |
263 (************************************************************* |
262 (************************************************************* |
264 instantiate split theorem |
263 instantiate split theorem |
265 |
264 |
272 state : current proof state |
271 state : current proof state |
273 i : number of subgoal |
272 i : number of subgoal |
274 **************************************************************) |
273 **************************************************************) |
275 |
274 |
276 fun inst_split Ts t tt thm TB state i = |
275 fun inst_split Ts t tt thm TB state i = |
277 let val _ $ ((Var (P2, PT2)) $ _) $ _ = concl_of thm; |
276 let |
278 val sg = #sign(rep_thm state) |
277 val thm' = Thm.lift_rule (state, i) thm; |
279 val tsig = #tsig(Sign.rep_sg sg) |
278 val (P, _) = strip_comb (fst (Logic.dest_equals |
280 val cntxt = mk_cntxt_splitthm t tt TB; |
279 (Logic.strip_assums_concl (#prop (rep_thm thm'))))); |
281 val T = fastype_of1 (Ts, cntxt); |
280 val cert = cterm_of (sign_of_thm state); |
282 val ixnTs = Type.typ_match tsig ([],(PT2, T)) |
281 val cntxt = mk_cntxt_splitthm t tt TB; |
283 val abss = foldl (fn (t, T) => Abs ("", T, t)) |
282 val abss = foldl (fn (t, T) => Abs ("", T, t)); |
284 in |
283 in cterm_instantiate [(cert P, cert (abss (cntxt, Ts)))] thm' |
285 term_lift_inst_rule (state, i, ixnTs, [((P2, T), abss (cntxt, Ts))], thm) |
284 end; |
286 end; |
285 |
287 |
286 |
288 (***************************************************************************** |
287 (***************************************************************************** |
289 The split-tactic |
288 The split-tactic |
290 |
289 |
291 splits : list of split-theorems to be tried |
290 splits : list of split-theorems to be tried |
300 (case strip_comb lhs of (Const(a,aT),args) => |
299 (case strip_comb lhs of (Const(a,aT),args) => |
301 (a,(aT,thm,fastype_of t,length args)) |
300 (a,(aT,thm,fastype_of t,length args)) |
302 | _ => split_format_err()) |
301 | _ => split_format_err()) |
303 | _ => split_format_err()) |
302 | _ => split_format_err()) |
304 val cmap = map const splits; |
303 val cmap = map const splits; |
305 fun lift_tac Ts t p st = (rtac (inst_lift Ts t p st trlift i) i) st |
304 fun lift_tac Ts t p st = rtac (inst_lift Ts t p st i) i st |
306 fun lift_split_tac st = st |> |
305 fun lift_split_tac state = |
307 let val (Ts,t,splits) = select cmap st i |
306 let val (Ts, t, splits) = select cmap state i |
308 in case splits of |
307 in case splits of |
309 [] => no_tac |
308 [] => no_tac state |
310 | (thm,apsns,pos,TB,tt)::_ => |
309 | (thm, apsns, pos, TB, tt)::_ => |
311 (case apsns of |
310 (case apsns of |
312 [] => (fn state => state |> |
311 [] => compose_tac (false, inst_split Ts t tt thm TB state i, 0) i state |
313 compose_tac (false, inst_split Ts t tt thm TB state i, 0) i) |
312 | p::_ => EVERY [lift_tac Ts t p, |
314 | p::_ => EVERY[lift_tac Ts t p, |
313 rtac reflexive_thm (i+1), |
315 rtac reflexive_thm (i+1), |
314 lift_split_tac] state) |
316 lift_split_tac]) |
|
317 end |
315 end |
318 in COND (has_fewer_prems i) no_tac |
316 in COND (has_fewer_prems i) no_tac |
319 (rtac meta_iffD i THEN lift_split_tac) |
317 (rtac meta_iffD i THEN lift_split_tac) |
320 end; |
318 end; |
321 |
319 |