2665
|
1 |
(* Nominal Function Core
|
|
2 |
Author: Christian Urban
|
|
3 |
|
|
4 |
heavily based on the code of Alexander Krauss
|
|
5 |
(code forked on 14 January 2011)
|
|
6 |
|
|
7 |
Core of the nominal function package.
|
|
8 |
*)
|
|
9 |
|
|
10 |
signature NOMINAL_FUNCTION_CORE =
|
|
11 |
sig
|
|
12 |
val trace: bool Unsynchronized.ref
|
|
13 |
|
|
14 |
val prepare_nominal_function : Function_Common.function_config
|
|
15 |
-> string (* defname *)
|
|
16 |
-> ((bstring * typ) * mixfix) list (* defined symbol *)
|
|
17 |
-> ((bstring * typ) list * term list * term * term) list (* specification *)
|
|
18 |
-> local_theory
|
|
19 |
-> (term (* f *)
|
|
20 |
* thm (* goalstate *)
|
|
21 |
* (thm -> Function_Common.function_result) (* continuation *)
|
|
22 |
) * local_theory
|
|
23 |
|
|
24 |
end
|
|
25 |
|
|
26 |
structure Nominal_Function_Core : NOMINAL_FUNCTION_CORE =
|
|
27 |
struct
|
|
28 |
|
|
29 |
val trace = Unsynchronized.ref false
|
|
30 |
fun trace_msg msg = if ! trace then tracing (msg ()) else ()
|
|
31 |
|
|
32 |
val boolT = HOLogic.boolT
|
|
33 |
val mk_eq = HOLogic.mk_eq
|
|
34 |
|
|
35 |
open Function_Lib
|
|
36 |
open Function_Common
|
|
37 |
|
|
38 |
datatype globals = Globals of
|
|
39 |
{fvar: term,
|
|
40 |
domT: typ,
|
|
41 |
ranT: typ,
|
|
42 |
h: term,
|
|
43 |
y: term,
|
|
44 |
x: term,
|
|
45 |
z: term,
|
|
46 |
a: term,
|
|
47 |
P: term,
|
|
48 |
D: term,
|
|
49 |
Pbool:term}
|
|
50 |
|
|
51 |
datatype rec_call_info = RCInfo of
|
|
52 |
{RIvs: (string * typ) list, (* Call context: fixes and assumes *)
|
|
53 |
CCas: thm list,
|
|
54 |
rcarg: term, (* The recursive argument *)
|
|
55 |
llRI: thm,
|
|
56 |
h_assum: term}
|
|
57 |
|
|
58 |
|
|
59 |
datatype clause_context = ClauseContext of
|
|
60 |
{ctxt : Proof.context,
|
|
61 |
qs : term list,
|
|
62 |
gs : term list,
|
|
63 |
lhs: term,
|
|
64 |
rhs: term,
|
|
65 |
cqs: cterm list,
|
|
66 |
ags: thm list,
|
|
67 |
case_hyp : thm}
|
|
68 |
|
|
69 |
|
|
70 |
fun transfer_clause_ctx thy (ClauseContext { ctxt, qs, gs, lhs, rhs, cqs, ags, case_hyp }) =
|
|
71 |
ClauseContext { ctxt = ProofContext.transfer thy ctxt,
|
|
72 |
qs = qs, gs = gs, lhs = lhs, rhs = rhs, cqs = cqs, ags = ags, case_hyp = case_hyp }
|
|
73 |
|
|
74 |
|
|
75 |
datatype clause_info = ClauseInfo of
|
|
76 |
{no: int,
|
|
77 |
qglr : ((string * typ) list * term list * term * term),
|
|
78 |
cdata : clause_context,
|
|
79 |
tree: Function_Ctx_Tree.ctx_tree,
|
|
80 |
lGI: thm,
|
|
81 |
RCs: rec_call_info list}
|
|
82 |
|
|
83 |
|
|
84 |
(* Theory dependencies. *)
|
|
85 |
val acc_induct_rule = @{thm accp_induct_rule}
|
|
86 |
|
|
87 |
val ex1_implies_ex = @{thm FunDef.fundef_ex1_existence}
|
|
88 |
val ex1_implies_un = @{thm FunDef.fundef_ex1_uniqueness}
|
|
89 |
val ex1_implies_iff = @{thm FunDef.fundef_ex1_iff}
|
|
90 |
|
|
91 |
val acc_downward = @{thm accp_downward}
|
|
92 |
val accI = @{thm accp.accI}
|
|
93 |
val case_split = @{thm HOL.case_split}
|
|
94 |
val fundef_default_value = @{thm FunDef.fundef_default_value}
|
|
95 |
val not_acc_down = @{thm not_accp_down}
|
|
96 |
|
|
97 |
|
|
98 |
|
|
99 |
fun find_calls tree =
|
|
100 |
let
|
|
101 |
fun add_Ri (fixes,assumes) (_ $ arg) _ (_, xs) =
|
|
102 |
([], (fixes, assumes, arg) :: xs)
|
|
103 |
| add_Ri _ _ _ _ = raise Match
|
|
104 |
in
|
|
105 |
rev (Function_Ctx_Tree.traverse_tree add_Ri tree [])
|
|
106 |
end
|
|
107 |
|
|
108 |
(* nominal *)
|
|
109 |
fun mk_eqvt_at (f_trm, arg_trm) =
|
|
110 |
let
|
|
111 |
val f_ty = fastype_of f_trm
|
|
112 |
val arg_ty = domain_type f_ty
|
|
113 |
in
|
|
114 |
Const (@{const_name eqvt_at}, [f_ty, arg_ty] ---> @{typ bool}) $ f_trm $ arg_trm
|
|
115 |
|> HOLogic.mk_Trueprop
|
|
116 |
end
|
|
117 |
|
2707
|
118 |
fun mk_eqvt trm =
|
|
119 |
let
|
|
120 |
val ty = fastype_of trm
|
|
121 |
in
|
|
122 |
Const (@{const_name eqvt}, ty --> @{typ bool}) $ trm
|
|
123 |
|> HOLogic.mk_Trueprop
|
|
124 |
end
|
|
125 |
|
2665
|
126 |
(* nominal *)
|
|
127 |
fun find_calls2 f t =
|
|
128 |
let
|
|
129 |
fun aux (g $ arg) = aux g #> aux arg #> (if f = g then cons ((g, arg)) else I)
|
|
130 |
| aux (Abs (_, _, t)) = aux t
|
|
131 |
| aux _ = I
|
|
132 |
in
|
|
133 |
aux t []
|
|
134 |
end
|
|
135 |
|
|
136 |
|
|
137 |
|
|
138 |
(** building proof obligations *)
|
|
139 |
|
|
140 |
fun mk_compat_proof_obligations domT ranT fvar f glrs =
|
|
141 |
let
|
|
142 |
fun mk_impl ((qs, gs, lhs, rhs), (qs', gs', lhs', rhs')) =
|
|
143 |
let
|
|
144 |
val shift = incr_boundvars (length qs')
|
|
145 |
|
|
146 |
val RCs_rhs = find_calls2 fvar rhs (* nominal : FIXME : recursive calls should be passed here *)
|
|
147 |
in
|
|
148 |
Logic.mk_implies
|
|
149 |
(HOLogic.mk_Trueprop (HOLogic.eq_const domT $ shift lhs $ lhs'),
|
|
150 |
HOLogic.mk_Trueprop (HOLogic.eq_const ranT $ shift rhs $ rhs'))
|
|
151 |
|> fold_rev (curry Logic.mk_implies) (map shift gs @ gs')
|
|
152 |
|> fold_rev (curry Logic.mk_implies) (map (shift o mk_eqvt_at) RCs_rhs) (* nominal *)
|
|
153 |
|> fold_rev (fn (n,T) => fn b => Term.all T $ Abs(n,T,b)) (qs @ qs')
|
|
154 |
|> curry abstract_over fvar
|
|
155 |
|> curry subst_bound f
|
|
156 |
end
|
|
157 |
in
|
|
158 |
map mk_impl (unordered_pairs glrs)
|
|
159 |
end
|
|
160 |
|
|
161 |
|
|
162 |
fun mk_completeness (Globals {x, Pbool, ...}) clauses qglrs =
|
|
163 |
let
|
|
164 |
fun mk_case (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) =
|
|
165 |
HOLogic.mk_Trueprop Pbool
|
|
166 |
|> curry Logic.mk_implies (HOLogic.mk_Trueprop (mk_eq (x, lhs)))
|
|
167 |
|> fold_rev (curry Logic.mk_implies) gs
|
|
168 |
|> fold_rev mk_forall_rename (map fst oqs ~~ qs)
|
|
169 |
in
|
|
170 |
HOLogic.mk_Trueprop Pbool
|
|
171 |
|> fold_rev (curry Logic.mk_implies o mk_case) (clauses ~~ qglrs)
|
|
172 |
|> mk_forall_rename ("x", x)
|
|
173 |
|> mk_forall_rename ("P", Pbool)
|
|
174 |
end
|
|
175 |
|
|
176 |
(** making a context with it's own local bindings **)
|
|
177 |
|
|
178 |
fun mk_clause_context x ctxt (pre_qs,pre_gs,pre_lhs,pre_rhs) =
|
|
179 |
let
|
|
180 |
val (qs, ctxt') = Variable.variant_fixes (map fst pre_qs) ctxt
|
|
181 |
|>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
|
|
182 |
|
|
183 |
val thy = ProofContext.theory_of ctxt'
|
|
184 |
|
|
185 |
fun inst t = subst_bounds (rev qs, t)
|
|
186 |
val gs = map inst pre_gs
|
|
187 |
val lhs = inst pre_lhs
|
|
188 |
val rhs = inst pre_rhs
|
|
189 |
|
|
190 |
val cqs = map (cterm_of thy) qs
|
|
191 |
val ags = map (Thm.assume o cterm_of thy) gs
|
|
192 |
|
|
193 |
val case_hyp = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs))))
|
|
194 |
in
|
|
195 |
ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs,
|
|
196 |
cqs = cqs, ags = ags, case_hyp = case_hyp }
|
|
197 |
end
|
|
198 |
|
|
199 |
|
|
200 |
(* lowlevel term function. FIXME: remove *)
|
|
201 |
fun abstract_over_list vs body =
|
|
202 |
let
|
|
203 |
fun abs lev v tm =
|
|
204 |
if v aconv tm then Bound lev
|
|
205 |
else
|
|
206 |
(case tm of
|
|
207 |
Abs (a, T, t) => Abs (a, T, abs (lev + 1) v t)
|
|
208 |
| t $ u => abs lev v t $ abs lev v u
|
|
209 |
| t => t)
|
|
210 |
in
|
|
211 |
fold_index (fn (i, v) => fn t => abs i v t) vs body
|
|
212 |
end
|
|
213 |
|
|
214 |
|
|
215 |
|
|
216 |
fun mk_clause_info globals G f no cdata qglr tree RCs GIntro_thm RIntro_thms =
|
|
217 |
let
|
|
218 |
val Globals {h, ...} = globals
|
|
219 |
|
|
220 |
val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata
|
|
221 |
val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
|
|
222 |
|
|
223 |
(* Instantiate the GIntro thm with "f" and import into the clause context. *)
|
|
224 |
val lGI = GIntro_thm
|
|
225 |
|> Thm.forall_elim (cert f)
|
|
226 |
|> fold Thm.forall_elim cqs
|
|
227 |
|> fold Thm.elim_implies ags
|
|
228 |
|
|
229 |
fun mk_call_info (rcfix, rcassm, rcarg) RI =
|
|
230 |
let
|
|
231 |
val llRI = RI
|
|
232 |
|> fold Thm.forall_elim cqs
|
|
233 |
|> fold (Thm.forall_elim o cert o Free) rcfix
|
|
234 |
|> fold Thm.elim_implies ags
|
|
235 |
|> fold Thm.elim_implies rcassm
|
|
236 |
|
|
237 |
val h_assum =
|
|
238 |
HOLogic.mk_Trueprop (G $ rcarg $ (h $ rcarg))
|
|
239 |
|> fold_rev (curry Logic.mk_implies o prop_of) rcassm
|
|
240 |
|> fold_rev (Logic.all o Free) rcfix
|
|
241 |
|> Pattern.rewrite_term (ProofContext.theory_of ctxt) [(f, h)] []
|
|
242 |
|> abstract_over_list (rev qs)
|
|
243 |
in
|
|
244 |
RCInfo {RIvs=rcfix, rcarg=rcarg, CCas=rcassm, llRI=llRI, h_assum=h_assum}
|
|
245 |
end
|
|
246 |
|
|
247 |
val RC_infos = map2 mk_call_info RCs RIntro_thms
|
|
248 |
in
|
|
249 |
ClauseInfo {no=no, cdata=cdata, qglr=qglr, lGI=lGI, RCs=RC_infos,
|
|
250 |
tree=tree}
|
|
251 |
end
|
|
252 |
|
|
253 |
|
|
254 |
fun store_compat_thms 0 thms = []
|
|
255 |
| store_compat_thms n thms =
|
|
256 |
let
|
|
257 |
val (thms1, thms2) = chop n thms
|
|
258 |
in
|
|
259 |
(thms1 :: store_compat_thms (n - 1) thms2)
|
|
260 |
end
|
|
261 |
|
|
262 |
(* expects i <= j *)
|
|
263 |
fun lookup_compat_thm i j cts =
|
|
264 |
nth (nth cts (i - 1)) (j - i)
|
|
265 |
|
|
266 |
(* nominal *)
|
|
267 |
(* Returns "Gsi, Gsj, lhs_i = lhs_j |-- rhs_j_f = rhs_i_f" *)
|
|
268 |
(* if j < i, then turn around *)
|
|
269 |
fun get_compat_thm thy cts eqvtsi eqvtsj i j ctxi ctxj =
|
|
270 |
let
|
|
271 |
val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi
|
|
272 |
val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj
|
|
273 |
|
|
274 |
val lhsi_eq_lhsj = cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj)))
|
|
275 |
in if j < i then
|
|
276 |
let
|
|
277 |
val compat = lookup_compat_thm j i cts
|
|
278 |
in
|
|
279 |
compat (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
|
|
280 |
|> fold Thm.forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
|
|
281 |
|> fold Thm.elim_implies (rev eqvtsj) (* nominal *)
|
|
282 |
|> fold Thm.elim_implies agsj
|
|
283 |
|> fold Thm.elim_implies agsi
|
|
284 |
|> Thm.elim_implies ((Thm.assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *)
|
|
285 |
end
|
|
286 |
else
|
|
287 |
let
|
|
288 |
val compat = lookup_compat_thm i j cts
|
|
289 |
in
|
|
290 |
compat (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
|
|
291 |
|> fold Thm.forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
|
|
292 |
|> fold Thm.elim_implies (rev eqvtsi) (* nominal *)
|
|
293 |
|> fold Thm.elim_implies agsi
|
|
294 |
|> fold Thm.elim_implies agsj
|
|
295 |
|> Thm.elim_implies (Thm.assume lhsi_eq_lhsj)
|
|
296 |
|> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *)
|
|
297 |
end
|
|
298 |
end
|
|
299 |
|
|
300 |
|
|
301 |
(* Generates the replacement lemma in fully quantified form. *)
|
|
302 |
fun mk_replacement_lemma thy h ih_elim clause =
|
|
303 |
let
|
|
304 |
val ClauseInfo {cdata=ClauseContext {qs, lhs, cqs, ags, case_hyp, ...},
|
|
305 |
RCs, tree, ...} = clause
|
|
306 |
local open Conv in
|
|
307 |
val ih_conv = arg1_conv o arg_conv o arg_conv
|
|
308 |
end
|
|
309 |
|
|
310 |
val ih_elim_case =
|
|
311 |
Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_elim
|
|
312 |
|
|
313 |
val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs
|
|
314 |
val h_assums = map (fn RCInfo {h_assum, ...} =>
|
|
315 |
Thm.assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs
|
|
316 |
|
|
317 |
val (eql, _) =
|
|
318 |
Function_Ctx_Tree.rewrite_by_tree thy h ih_elim_case (Ris ~~ h_assums) tree
|
|
319 |
|
|
320 |
val replace_lemma = (eql RS meta_eq_to_obj_eq)
|
|
321 |
|> Thm.implies_intr (cprop_of case_hyp)
|
|
322 |
|> fold_rev (Thm.implies_intr o cprop_of) h_assums
|
|
323 |
|> fold_rev (Thm.implies_intr o cprop_of) ags
|
|
324 |
|> fold_rev Thm.forall_intr cqs
|
|
325 |
|> Thm.close_derivation
|
|
326 |
in
|
|
327 |
replace_lemma
|
|
328 |
end
|
|
329 |
|
|
330 |
(* nominal *)
|
|
331 |
(* Generates the eqvt lemmas for each clause *)
|
|
332 |
fun mk_eqvt_lemma thy ih_eqvt clause =
|
|
333 |
let
|
|
334 |
val ClauseInfo {cdata=ClauseContext {cqs, ags, case_hyp, ...}, RCs, ...} = clause
|
|
335 |
|
|
336 |
local open Conv in
|
|
337 |
val ih_conv = arg1_conv o arg_conv o arg_conv
|
|
338 |
end
|
|
339 |
|
|
340 |
val ih_eqvt_case =
|
|
341 |
Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_eqvt
|
|
342 |
|
|
343 |
fun prep_eqvt (RCInfo {llRI, RIvs, CCas, ...}) =
|
|
344 |
(llRI RS ih_eqvt_case)
|
|
345 |
|> fold_rev (Thm.implies_intr o cprop_of) CCas
|
|
346 |
|> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs
|
|
347 |
in
|
|
348 |
map prep_eqvt RCs
|
|
349 |
|> map (fold_rev (Thm.implies_intr o cprop_of) ags)
|
|
350 |
|> map (Thm.implies_intr (cprop_of case_hyp))
|
|
351 |
|> map (fold_rev Thm.forall_intr cqs)
|
|
352 |
|> map (Thm.close_derivation)
|
|
353 |
end
|
|
354 |
|
|
355 |
(* nominal *)
|
|
356 |
fun mk_uniqueness_clause thy globals compat_store eqvts clausei clausej RLj =
|
|
357 |
let
|
|
358 |
val Globals {h, y, x, fvar, ...} = globals
|
|
359 |
val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, cqs = cqsi,
|
|
360 |
ags = agsi, ...}, ...} = clausei
|
|
361 |
val ClauseInfo {no=j, qglr=cdescj, RCs=RCsj, ...} = clausej
|
|
362 |
|
|
363 |
val cctxj as ClauseContext {ags = agsj', lhs = lhsj', rhs = rhsj', qs = qsj', cqs = cqsj', ...} =
|
|
364 |
mk_clause_context x ctxti cdescj
|
|
365 |
|
|
366 |
val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj'
|
|
367 |
|
|
368 |
val Ghsj' = map
|
|
369 |
(fn RCInfo {h_assum, ...} => Thm.assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj
|
|
370 |
|
|
371 |
val y_eq_rhsj'h = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h))))
|
|
372 |
val lhsi_eq_lhsj' = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj'))))
|
|
373 |
(* lhs_i = lhs_j' |-- lhs_i = lhs_j' *)
|
|
374 |
|
|
375 |
val case_hypj' = trans OF [case_hyp, lhsi_eq_lhsj']
|
|
376 |
|
|
377 |
val RLj_import = RLj
|
|
378 |
|> fold Thm.forall_elim cqsj'
|
|
379 |
|> fold Thm.elim_implies agsj'
|
|
380 |
|> fold Thm.elim_implies Ghsj'
|
|
381 |
|
|
382 |
val eqvtsi = nth eqvts (i - 1)
|
|
383 |
|> map (fold Thm.forall_elim cqsi)
|
|
384 |
|> map (fold Thm.elim_implies [case_hyp])
|
|
385 |
|> map (fold Thm.elim_implies agsi)
|
|
386 |
|
|
387 |
val eqvtsj = nth eqvts (j - 1)
|
|
388 |
|> map (fold Thm.forall_elim cqsj')
|
|
389 |
|> map (fold Thm.elim_implies [case_hypj'])
|
|
390 |
|> map (fold Thm.elim_implies agsj')
|
|
391 |
|
|
392 |
val compat = get_compat_thm thy compat_store eqvtsi eqvtsj i j cctxi cctxj
|
|
393 |
|
|
394 |
in
|
|
395 |
(trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
|
|
396 |
|> Thm.implies_elim RLj_import
|
|
397 |
(* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *)
|
|
398 |
|> (fn it => trans OF [it, compat])
|
|
399 |
(* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)
|
|
400 |
|> (fn it => trans OF [y_eq_rhsj'h, it])
|
|
401 |
(* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *)
|
|
402 |
|> fold_rev (Thm.implies_intr o cprop_of) Ghsj'
|
|
403 |
|> fold_rev (Thm.implies_intr o cprop_of) agsj'
|
|
404 |
(* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *)
|
|
405 |
|> Thm.implies_intr (cprop_of y_eq_rhsj'h)
|
|
406 |
|> Thm.implies_intr (cprop_of lhsi_eq_lhsj')
|
|
407 |
|> fold_rev Thm.forall_intr (cterm_of thy h :: cqsj')
|
|
408 |
end
|
|
409 |
|
|
410 |
(* nominal *)
|
|
411 |
fun mk_uniqueness_case thy globals G f ihyp ih_intro G_cases compat_store clauses replems eqvtlems clausei =
|
|
412 |
let
|
|
413 |
val Globals {x, y, ranT, fvar, ...} = globals
|
|
414 |
val ClauseInfo {cdata = ClauseContext {lhs, rhs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei
|
|
415 |
val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs
|
|
416 |
|
|
417 |
val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro
|
|
418 |
|
|
419 |
fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) =
|
|
420 |
(llRI RS ih_intro_case)
|
|
421 |
|> fold_rev (Thm.implies_intr o cprop_of) CCas
|
|
422 |
|> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs
|
|
423 |
|
|
424 |
val existence = fold (curry op COMP o prep_RC) RCs lGI
|
|
425 |
|
|
426 |
val P = cterm_of thy (mk_eq (y, rhsC))
|
|
427 |
val G_lhs_y = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (G $ lhs $ y)))
|
|
428 |
|
|
429 |
val unique_clauses =
|
|
430 |
map2 (mk_uniqueness_clause thy globals compat_store eqvtlems clausei) clauses replems
|
|
431 |
|
|
432 |
fun elim_implies_eta A AB =
|
|
433 |
Thm.compose_no_flatten true (A, 0) 1 AB |> Seq.list_of |> the_single
|
|
434 |
|
|
435 |
val uniqueness = G_cases
|
|
436 |
|> Thm.forall_elim (cterm_of thy lhs)
|
|
437 |
|> Thm.forall_elim (cterm_of thy y)
|
|
438 |
|> Thm.forall_elim P
|
|
439 |
|> Thm.elim_implies G_lhs_y
|
|
440 |
|> fold elim_implies_eta unique_clauses
|
|
441 |
|> Thm.implies_intr (cprop_of G_lhs_y)
|
|
442 |
|> Thm.forall_intr (cterm_of thy y)
|
|
443 |
|
|
444 |
val P2 = cterm_of thy (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *)
|
|
445 |
|
|
446 |
val exactly_one =
|
|
447 |
ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)]
|
|
448 |
|> curry (op COMP) existence
|
|
449 |
|> curry (op COMP) uniqueness
|
|
450 |
|> simplify (HOL_basic_ss addsimps [case_hyp RS sym])
|
|
451 |
|> Thm.implies_intr (cprop_of case_hyp)
|
|
452 |
|> fold_rev (Thm.implies_intr o cprop_of) ags
|
|
453 |
|> fold_rev Thm.forall_intr cqs
|
|
454 |
|
|
455 |
val function_value =
|
|
456 |
existence
|
|
457 |
|> Thm.implies_intr ihyp
|
|
458 |
|> Thm.implies_intr (cprop_of case_hyp)
|
|
459 |
|> Thm.forall_intr (cterm_of thy x)
|
|
460 |
|> Thm.forall_elim (cterm_of thy lhs)
|
|
461 |
|> curry (op RS) refl
|
|
462 |
in
|
|
463 |
(exactly_one, function_value)
|
|
464 |
end
|
|
465 |
|
|
466 |
|
|
467 |
(* nominal *)
|
|
468 |
fun prove_stuff ctxt globals G f R clauses complete compat compat_store G_elim G_eqvt f_def =
|
|
469 |
let
|
|
470 |
val Globals {h, domT, ranT, x, ...} = globals
|
|
471 |
val thy = ProofContext.theory_of ctxt
|
|
472 |
|
|
473 |
(* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
|
|
474 |
val ihyp = Term.all domT $ Abs ("z", domT,
|
|
475 |
Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
|
|
476 |
HOLogic.mk_Trueprop (Const (@{const_name Ex1}, (ranT --> boolT) --> boolT) $
|
|
477 |
Abs ("y", ranT, G $ Bound 1 $ Bound 0))))
|
|
478 |
|> cterm_of thy
|
|
479 |
|
|
480 |
val ihyp_thm = Thm.assume ihyp |> Thm.forall_elim_vars 0
|
|
481 |
val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex)
|
|
482 |
val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un)
|
|
483 |
|> instantiate' [] [NONE, SOME (cterm_of thy h)]
|
|
484 |
val ih_eqvt = ihyp_thm RS (G_eqvt RS (f_def RS @{thm fundef_ex1_eqvt_at}))
|
2709
|
485 |
|
2665
|
486 |
val _ = trace_msg (K "Proving Replacement lemmas...")
|
|
487 |
val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses
|
|
488 |
|
|
489 |
val _ = trace_msg (K "Proving Equivariance lemmas...")
|
|
490 |
val eqvtLemmas = map (mk_eqvt_lemma thy ih_eqvt) clauses
|
|
491 |
|
|
492 |
val _ = trace_msg (K "Proving cases for unique existence...")
|
|
493 |
val (ex1s, values) =
|
|
494 |
split_list (map (mk_uniqueness_case thy globals G f
|
|
495 |
ihyp ih_intro G_elim compat_store clauses repLemmas eqvtLemmas) clauses)
|
|
496 |
|
|
497 |
val _ = trace_msg (K "Proving: Graph is a function")
|
|
498 |
val graph_is_function = complete
|
|
499 |
|> Thm.forall_elim_vars 0
|
|
500 |
|> fold (curry op COMP) ex1s
|
|
501 |
|> Thm.implies_intr (ihyp)
|
|
502 |
|> Thm.implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x)))
|
|
503 |
|> Thm.forall_intr (cterm_of thy x)
|
|
504 |
|> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
|
|
505 |
|> (fn it => fold (Thm.forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of it) []) it)
|
|
506 |
|
2707
|
507 |
val goalstate =
|
|
508 |
Conjunction.intr (Conjunction.intr graph_is_function complete) G_eqvt
|
2665
|
509 |
|> Thm.close_derivation
|
|
510 |
|> Goal.protect
|
|
511 |
|> fold_rev (Thm.implies_intr o cprop_of) compat
|
|
512 |
|> Thm.implies_intr (cprop_of complete)
|
2707
|
513 |
|> Thm.implies_intr (cprop_of G_eqvt)
|
2665
|
514 |
in
|
|
515 |
(goalstate, values)
|
|
516 |
end
|
|
517 |
|
|
518 |
(* wrapper -- restores quantifiers in rule specifications *)
|
2707
|
519 |
fun inductive_def (binding as ((R, T), _)) intrs lthy =
|
2665
|
520 |
let
|
|
521 |
val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, raw_induct, ...}, lthy) =
|
|
522 |
lthy
|
|
523 |
|> Local_Theory.conceal
|
|
524 |
|> Inductive.add_inductive_i
|
|
525 |
{quiet_mode = true,
|
|
526 |
verbose = ! trace,
|
|
527 |
alt_name = Binding.empty,
|
|
528 |
coind = false,
|
|
529 |
no_elim = false,
|
|
530 |
no_ind = false,
|
|
531 |
skip_mono = true,
|
|
532 |
fork_mono = false}
|
|
533 |
[binding] (* relation *)
|
|
534 |
[] (* no parameters *)
|
|
535 |
(map (fn t => (Attrib.empty_binding, t)) intrs) (* intro rules *)
|
|
536 |
[] (* no special monos *)
|
|
537 |
||> Local_Theory.restore_naming lthy
|
|
538 |
|
|
539 |
val cert = cterm_of (ProofContext.theory_of lthy)
|
|
540 |
fun requantify orig_intro thm =
|
|
541 |
let
|
|
542 |
val (qs, t) = dest_all_all orig_intro
|
|
543 |
val frees = frees_in_term lthy t |> remove (op =) (Binding.name_of R, T)
|
|
544 |
val vars = Term.add_vars (prop_of thm) [] |> rev
|
|
545 |
val varmap = AList.lookup (op =) (frees ~~ map fst vars)
|
|
546 |
#> the_default ("",0)
|
|
547 |
in
|
|
548 |
fold_rev (fn Free (n, T) =>
|
|
549 |
forall_intr_rename (n, cert (Var (varmap (n, T), T)))) qs thm
|
|
550 |
end
|
|
551 |
in
|
2707
|
552 |
((Rdef, map2 requantify intrs intrs_gen, forall_intr_vars elim_gen, induct), lthy)
|
2665
|
553 |
end
|
|
554 |
|
|
555 |
(* nominal *)
|
|
556 |
fun define_graph Gname fvar domT ranT clauses RCss lthy =
|
|
557 |
let
|
|
558 |
val GT = domT --> ranT --> boolT
|
|
559 |
val (Gvar as (n, T)) = singleton (Variable.variant_frees lthy []) (Gname, GT)
|
|
560 |
|
|
561 |
fun mk_GIntro (ClauseContext {qs, gs, lhs, rhs, ...}) RCs =
|
|
562 |
let
|
|
563 |
fun mk_h_assm (rcfix, rcassm, rcarg) =
|
|
564 |
HOLogic.mk_Trueprop (Free Gvar $ rcarg $ (fvar $ rcarg))
|
|
565 |
|> fold_rev (curry Logic.mk_implies o prop_of) rcassm
|
|
566 |
|> fold_rev (Logic.all o Free) rcfix
|
|
567 |
in
|
|
568 |
HOLogic.mk_Trueprop (Free Gvar $ lhs $ rhs)
|
|
569 |
|> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs
|
|
570 |
|> fold_rev (curry Logic.mk_implies) gs
|
|
571 |
|> fold_rev Logic.all (fvar :: qs)
|
|
572 |
end
|
|
573 |
|
|
574 |
val G_intros = map2 mk_GIntro clauses RCss
|
|
575 |
in
|
2707
|
576 |
inductive_def ((Binding.name n, T), NoSyn) G_intros lthy
|
2665
|
577 |
end
|
|
578 |
|
|
579 |
fun define_function fdefname (fname, mixfix) domT ranT G default lthy =
|
|
580 |
let
|
|
581 |
val f_def =
|
|
582 |
Abs ("x", domT, Const (@{const_name FunDef.THE_default}, ranT --> (ranT --> boolT) --> ranT)
|
|
583 |
$ (default $ Bound 0) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0))
|
|
584 |
|> Syntax.check_term lthy
|
|
585 |
in
|
|
586 |
Local_Theory.define
|
|
587 |
((Binding.name (function_name fname), mixfix),
|
|
588 |
((Binding.conceal (Binding.name fdefname), []), f_def)) lthy
|
|
589 |
end
|
|
590 |
|
|
591 |
(* nominal *)
|
|
592 |
fun define_recursion_relation Rname domT qglrs clauses RCss lthy =
|
|
593 |
let
|
|
594 |
val RT = domT --> domT --> boolT
|
|
595 |
val (Rvar as (n, T)) = singleton (Variable.variant_frees lthy []) (Rname, RT)
|
|
596 |
|
|
597 |
fun mk_RIntro (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) (rcfix, rcassm, rcarg) =
|
|
598 |
HOLogic.mk_Trueprop (Free Rvar $ rcarg $ lhs)
|
|
599 |
|> fold_rev (curry Logic.mk_implies o prop_of) rcassm
|
|
600 |
|> fold_rev (curry Logic.mk_implies) gs
|
|
601 |
|> fold_rev (Logic.all o Free) rcfix
|
|
602 |
|> fold_rev mk_forall_rename (map fst oqs ~~ qs)
|
|
603 |
(* "!!qs xs. CS ==> G => (r, lhs) : R" *)
|
|
604 |
|
|
605 |
val R_intross = map2 (map o mk_RIntro) (clauses ~~ qglrs) RCss
|
|
606 |
|
2707
|
607 |
val ((R, RIntro_thms, R_elim, _), lthy) =
|
|
608 |
inductive_def ((Binding.name n, T), NoSyn) (flat R_intross) lthy
|
2665
|
609 |
in
|
|
610 |
((R, Library.unflat R_intross RIntro_thms, R_elim), lthy)
|
|
611 |
end
|
|
612 |
|
|
613 |
|
|
614 |
fun fix_globals domT ranT fvar ctxt =
|
|
615 |
let
|
|
616 |
val ([h, y, x, z, a, D, P, Pbool],ctxt') = Variable.variant_fixes
|
|
617 |
["h_fd", "y_fd", "x_fd", "z_fd", "a_fd", "D_fd", "P_fd", "Pb_fd"] ctxt
|
|
618 |
in
|
|
619 |
(Globals {h = Free (h, domT --> ranT),
|
|
620 |
y = Free (y, ranT),
|
|
621 |
x = Free (x, domT),
|
|
622 |
z = Free (z, domT),
|
|
623 |
a = Free (a, domT),
|
|
624 |
D = Free (D, domT --> boolT),
|
|
625 |
P = Free (P, domT --> boolT),
|
|
626 |
Pbool = Free (Pbool, boolT),
|
|
627 |
fvar = fvar,
|
|
628 |
domT = domT,
|
|
629 |
ranT = ranT},
|
|
630 |
ctxt')
|
|
631 |
end
|
|
632 |
|
|
633 |
fun inst_RC thy fvar f (rcfix, rcassm, rcarg) =
|
|
634 |
let
|
|
635 |
fun inst_term t = subst_bound(f, abstract_over (fvar, t))
|
|
636 |
in
|
|
637 |
(rcfix, map (Thm.assume o cterm_of thy o inst_term o prop_of) rcassm, inst_term rcarg)
|
|
638 |
end
|
|
639 |
|
|
640 |
|
|
641 |
|
|
642 |
(**********************************************************
|
|
643 |
* PROVING THE RULES
|
|
644 |
**********************************************************)
|
|
645 |
|
|
646 |
fun mk_psimps thy globals R clauses valthms f_iff graph_is_function =
|
|
647 |
let
|
|
648 |
val Globals {domT, z, ...} = globals
|
|
649 |
|
|
650 |
fun mk_psimp (ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {cqs, lhs, ags, ...}, ...}) valthm =
|
|
651 |
let
|
|
652 |
val lhs_acc = cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
|
|
653 |
val z_smaller = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ lhs)) (* "R z lhs" *)
|
|
654 |
in
|
|
655 |
((Thm.assume z_smaller) RS ((Thm.assume lhs_acc) RS acc_downward))
|
|
656 |
|> (fn it => it COMP graph_is_function)
|
|
657 |
|> Thm.implies_intr z_smaller
|
|
658 |
|> Thm.forall_intr (cterm_of thy z)
|
|
659 |
|> (fn it => it COMP valthm)
|
|
660 |
|> Thm.implies_intr lhs_acc
|
|
661 |
|> asm_simplify (HOL_basic_ss addsimps [f_iff])
|
|
662 |
|> fold_rev (Thm.implies_intr o cprop_of) ags
|
|
663 |
|> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
|
|
664 |
end
|
|
665 |
in
|
|
666 |
map2 mk_psimp clauses valthms
|
|
667 |
end
|
|
668 |
|
|
669 |
|
|
670 |
(** Induction rule **)
|
|
671 |
|
|
672 |
|
|
673 |
val acc_subset_induct = @{thm predicate1I} RS @{thm accp_subset_induct}
|
|
674 |
|
|
675 |
|
|
676 |
fun mk_partial_induct_rule thy globals R complete_thm clauses =
|
|
677 |
let
|
|
678 |
val Globals {domT, x, z, a, P, D, ...} = globals
|
|
679 |
val acc_R = mk_acc domT R
|
|
680 |
|
|
681 |
val x_D = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (D $ x)))
|
|
682 |
val a_D = cterm_of thy (HOLogic.mk_Trueprop (D $ a))
|
|
683 |
|
|
684 |
val D_subset = cterm_of thy (Logic.all x
|
|
685 |
(Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), HOLogic.mk_Trueprop (acc_R $ x))))
|
|
686 |
|
|
687 |
val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
|
|
688 |
Logic.all x (Logic.all z (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x),
|
|
689 |
Logic.mk_implies (HOLogic.mk_Trueprop (R $ z $ x),
|
|
690 |
HOLogic.mk_Trueprop (D $ z)))))
|
|
691 |
|> cterm_of thy
|
|
692 |
|
|
693 |
(* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
|
|
694 |
val ihyp = Term.all domT $ Abs ("z", domT,
|
|
695 |
Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
|
|
696 |
HOLogic.mk_Trueprop (P $ Bound 0)))
|
|
697 |
|> cterm_of thy
|
|
698 |
|
|
699 |
val aihyp = Thm.assume ihyp
|
|
700 |
|
|
701 |
fun prove_case clause =
|
|
702 |
let
|
|
703 |
val ClauseInfo {cdata = ClauseContext {ctxt, qs, cqs, ags, gs, lhs, case_hyp, ...},
|
|
704 |
RCs, qglr = (oqs, _, _, _), ...} = clause
|
|
705 |
|
|
706 |
val case_hyp_conv = K (case_hyp RS eq_reflection)
|
|
707 |
local open Conv in
|
|
708 |
val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D
|
|
709 |
val sih =
|
|
710 |
fconv_rule (Conv.binder_conv
|
|
711 |
(K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt) aihyp
|
|
712 |
end
|
|
713 |
|
|
714 |
fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) = sih
|
|
715 |
|> Thm.forall_elim (cterm_of thy rcarg)
|
|
716 |
|> Thm.elim_implies llRI
|
|
717 |
|> fold_rev (Thm.implies_intr o cprop_of) CCas
|
|
718 |
|> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs
|
|
719 |
|
|
720 |
val P_recs = map mk_Prec RCs (* [P rec1, P rec2, ... ] *)
|
|
721 |
|
|
722 |
val step = HOLogic.mk_Trueprop (P $ lhs)
|
|
723 |
|> fold_rev (curry Logic.mk_implies o prop_of) P_recs
|
|
724 |
|> fold_rev (curry Logic.mk_implies) gs
|
|
725 |
|> curry Logic.mk_implies (HOLogic.mk_Trueprop (D $ lhs))
|
|
726 |
|> fold_rev mk_forall_rename (map fst oqs ~~ qs)
|
|
727 |
|> cterm_of thy
|
|
728 |
|
|
729 |
val P_lhs = Thm.assume step
|
|
730 |
|> fold Thm.forall_elim cqs
|
|
731 |
|> Thm.elim_implies lhs_D
|
|
732 |
|> fold Thm.elim_implies ags
|
|
733 |
|> fold Thm.elim_implies P_recs
|
|
734 |
|
|
735 |
val res = cterm_of thy (HOLogic.mk_Trueprop (P $ x))
|
|
736 |
|> Conv.arg_conv (Conv.arg_conv case_hyp_conv)
|
|
737 |
|> Thm.symmetric (* P lhs == P x *)
|
|
738 |
|> (fn eql => Thm.equal_elim eql P_lhs) (* "P x" *)
|
|
739 |
|> Thm.implies_intr (cprop_of case_hyp)
|
|
740 |
|> fold_rev (Thm.implies_intr o cprop_of) ags
|
|
741 |
|> fold_rev Thm.forall_intr cqs
|
|
742 |
in
|
|
743 |
(res, step)
|
|
744 |
end
|
|
745 |
|
|
746 |
val (cases, steps) = split_list (map prove_case clauses)
|
|
747 |
|
|
748 |
val istep = complete_thm
|
|
749 |
|> Thm.forall_elim_vars 0
|
|
750 |
|> fold (curry op COMP) cases (* P x *)
|
|
751 |
|> Thm.implies_intr ihyp
|
|
752 |
|> Thm.implies_intr (cprop_of x_D)
|
|
753 |
|> Thm.forall_intr (cterm_of thy x)
|
|
754 |
|
|
755 |
val subset_induct_rule =
|
|
756 |
acc_subset_induct
|
|
757 |
|> (curry op COMP) (Thm.assume D_subset)
|
|
758 |
|> (curry op COMP) (Thm.assume D_dcl)
|
|
759 |
|> (curry op COMP) (Thm.assume a_D)
|
|
760 |
|> (curry op COMP) istep
|
|
761 |
|> fold_rev Thm.implies_intr steps
|
|
762 |
|> Thm.implies_intr a_D
|
|
763 |
|> Thm.implies_intr D_dcl
|
|
764 |
|> Thm.implies_intr D_subset
|
|
765 |
|
|
766 |
val simple_induct_rule =
|
|
767 |
subset_induct_rule
|
|
768 |
|> Thm.forall_intr (cterm_of thy D)
|
|
769 |
|> Thm.forall_elim (cterm_of thy acc_R)
|
|
770 |
|> assume_tac 1 |> Seq.hd
|
|
771 |
|> (curry op COMP) (acc_downward
|
|
772 |
|> (instantiate' [SOME (ctyp_of thy domT)]
|
|
773 |
(map (SOME o cterm_of thy) [R, x, z]))
|
|
774 |
|> Thm.forall_intr (cterm_of thy z)
|
|
775 |
|> Thm.forall_intr (cterm_of thy x))
|
|
776 |
|> Thm.forall_intr (cterm_of thy a)
|
|
777 |
|> Thm.forall_intr (cterm_of thy P)
|
|
778 |
in
|
|
779 |
simple_induct_rule
|
|
780 |
end
|
|
781 |
|
|
782 |
|
|
783 |
(* FIXME: broken by design *)
|
|
784 |
fun mk_domain_intro ctxt (Globals {domT, ...}) R R_cases clause =
|
|
785 |
let
|
|
786 |
val thy = ProofContext.theory_of ctxt
|
|
787 |
val ClauseInfo {cdata = ClauseContext {gs, lhs, cqs, ...},
|
|
788 |
qglr = (oqs, _, _, _), ...} = clause
|
|
789 |
val goal = HOLogic.mk_Trueprop (mk_acc domT R $ lhs)
|
|
790 |
|> fold_rev (curry Logic.mk_implies) gs
|
|
791 |
|> cterm_of thy
|
|
792 |
in
|
|
793 |
Goal.init goal
|
|
794 |
|> (SINGLE (resolve_tac [accI] 1)) |> the
|
|
795 |
|> (SINGLE (eresolve_tac [Thm.forall_elim_vars 0 R_cases] 1)) |> the
|
|
796 |
|> (SINGLE (auto_tac (clasimpset_of ctxt))) |> the
|
|
797 |
|> Goal.conclude
|
|
798 |
|> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
|
|
799 |
end
|
|
800 |
|
|
801 |
|
|
802 |
|
|
803 |
(** Termination rule **)
|
|
804 |
|
|
805 |
val wf_induct_rule = @{thm Wellfounded.wfP_induct_rule}
|
|
806 |
val wf_in_rel = @{thm FunDef.wf_in_rel}
|
|
807 |
val in_rel_def = @{thm FunDef.in_rel_def}
|
|
808 |
|
|
809 |
fun mk_nest_term_case thy globals R' ihyp clause =
|
|
810 |
let
|
|
811 |
val Globals {z, ...} = globals
|
|
812 |
val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, lhs, case_hyp, ...}, tree,
|
|
813 |
qglr=(oqs, _, _, _), ...} = clause
|
|
814 |
|
|
815 |
val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp
|
|
816 |
|
|
817 |
fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) =
|
|
818 |
let
|
|
819 |
val used = (u @ sub)
|
|
820 |
|> map (fn (ctx,thm) => Function_Ctx_Tree.export_thm thy ctx thm)
|
|
821 |
|
|
822 |
val hyp = HOLogic.mk_Trueprop (R' $ arg $ lhs)
|
|
823 |
|> fold_rev (curry Logic.mk_implies o prop_of) used (* additional hyps *)
|
|
824 |
|> Function_Ctx_Tree.export_term (fixes, assumes)
|
|
825 |
|> fold_rev (curry Logic.mk_implies o prop_of) ags
|
|
826 |
|> fold_rev mk_forall_rename (map fst oqs ~~ qs)
|
|
827 |
|> cterm_of thy
|
|
828 |
|
|
829 |
val thm = Thm.assume hyp
|
|
830 |
|> fold Thm.forall_elim cqs
|
|
831 |
|> fold Thm.elim_implies ags
|
|
832 |
|> Function_Ctx_Tree.import_thm thy (fixes, assumes)
|
|
833 |
|> fold Thm.elim_implies used (* "(arg, lhs) : R'" *)
|
|
834 |
|
|
835 |
val z_eq_arg = HOLogic.mk_Trueprop (mk_eq (z, arg))
|
|
836 |
|> cterm_of thy |> Thm.assume
|
|
837 |
|
|
838 |
val acc = thm COMP ih_case
|
|
839 |
val z_acc_local = acc
|
|
840 |
|> Conv.fconv_rule
|
|
841 |
(Conv.arg_conv (Conv.arg_conv (K (Thm.symmetric (z_eq_arg RS eq_reflection)))))
|
|
842 |
|
|
843 |
val ethm = z_acc_local
|
|
844 |
|> Function_Ctx_Tree.export_thm thy (fixes,
|
|
845 |
z_eq_arg :: case_hyp :: ags @ assumes)
|
|
846 |
|> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
|
|
847 |
|
|
848 |
val sub' = sub @ [(([],[]), acc)]
|
|
849 |
in
|
|
850 |
(sub', (hyp :: hyps, ethm :: thms))
|
|
851 |
end
|
|
852 |
| step _ _ _ _ = raise Match
|
|
853 |
in
|
|
854 |
Function_Ctx_Tree.traverse_tree step tree
|
|
855 |
end
|
|
856 |
|
|
857 |
|
|
858 |
fun mk_nest_term_rule thy globals R R_cases clauses =
|
|
859 |
let
|
|
860 |
val Globals { domT, x, z, ... } = globals
|
|
861 |
val acc_R = mk_acc domT R
|
|
862 |
|
|
863 |
val R' = Free ("R", fastype_of R)
|
|
864 |
|
|
865 |
val Rrel = Free ("R", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)))
|
|
866 |
val inrel_R = Const (@{const_name FunDef.in_rel},
|
|
867 |
HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel
|
|
868 |
|
|
869 |
val wfR' = HOLogic.mk_Trueprop (Const (@{const_name Wellfounded.wfP},
|
|
870 |
(domT --> domT --> boolT) --> boolT) $ R')
|
|
871 |
|> cterm_of thy (* "wf R'" *)
|
|
872 |
|
|
873 |
(* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
|
|
874 |
val ihyp = Term.all domT $ Abs ("z", domT,
|
|
875 |
Logic.mk_implies (HOLogic.mk_Trueprop (R' $ Bound 0 $ x),
|
|
876 |
HOLogic.mk_Trueprop (acc_R $ Bound 0)))
|
|
877 |
|> cterm_of thy
|
|
878 |
|
|
879 |
val ihyp_a = Thm.assume ihyp |> Thm.forall_elim_vars 0
|
|
880 |
|
|
881 |
val R_z_x = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ x))
|
|
882 |
|
|
883 |
val (hyps, cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([], [])
|
|
884 |
in
|
|
885 |
R_cases
|
|
886 |
|> Thm.forall_elim (cterm_of thy z)
|
|
887 |
|> Thm.forall_elim (cterm_of thy x)
|
|
888 |
|> Thm.forall_elim (cterm_of thy (acc_R $ z))
|
|
889 |
|> curry op COMP (Thm.assume R_z_x)
|
|
890 |
|> fold_rev (curry op COMP) cases
|
|
891 |
|> Thm.implies_intr R_z_x
|
|
892 |
|> Thm.forall_intr (cterm_of thy z)
|
|
893 |
|> (fn it => it COMP accI)
|
|
894 |
|> Thm.implies_intr ihyp
|
|
895 |
|> Thm.forall_intr (cterm_of thy x)
|
|
896 |
|> (fn it => Drule.compose_single(it,2,wf_induct_rule))
|
|
897 |
|> curry op RS (Thm.assume wfR')
|
|
898 |
|> forall_intr_vars
|
|
899 |
|> (fn it => it COMP allI)
|
|
900 |
|> fold Thm.implies_intr hyps
|
|
901 |
|> Thm.implies_intr wfR'
|
|
902 |
|> Thm.forall_intr (cterm_of thy R')
|
|
903 |
|> Thm.forall_elim (cterm_of thy (inrel_R))
|
|
904 |
|> curry op RS wf_in_rel
|
|
905 |
|> full_simplify (HOL_basic_ss addsimps [in_rel_def])
|
|
906 |
|> Thm.forall_intr (cterm_of thy Rrel)
|
|
907 |
end
|
|
908 |
|
|
909 |
|
|
910 |
|
|
911 |
(* Tail recursion (probably very fragile)
|
|
912 |
*
|
|
913 |
* FIXME:
|
|
914 |
* - Need to do forall_elim_vars on psimps: Unneccesary, if psimps would be taken from the same context.
|
|
915 |
* - Must we really replace the fvar by f here?
|
|
916 |
* - Splitting is not configured automatically: Problems with case?
|
|
917 |
*)
|
|
918 |
fun mk_trsimps octxt globals f G R f_def R_cases G_induct clauses psimps =
|
|
919 |
let
|
|
920 |
val Globals {domT, ranT, fvar, ...} = globals
|
|
921 |
|
|
922 |
val R_cases = Thm.forall_elim_vars 0 R_cases (* FIXME: Should be already in standard form. *)
|
|
923 |
|
|
924 |
val graph_implies_dom = (* "G ?x ?y ==> dom ?x" *)
|
|
925 |
Goal.prove octxt ["x", "y"] [HOLogic.mk_Trueprop (G $ Free ("x", domT) $ Free ("y", ranT))]
|
|
926 |
(HOLogic.mk_Trueprop (mk_acc domT R $ Free ("x", domT)))
|
|
927 |
(fn {prems=[a], ...} =>
|
|
928 |
((rtac (G_induct OF [a]))
|
|
929 |
THEN_ALL_NEW rtac accI
|
|
930 |
THEN_ALL_NEW etac R_cases
|
|
931 |
THEN_ALL_NEW asm_full_simp_tac (simpset_of octxt)) 1)
|
|
932 |
|
|
933 |
val default_thm =
|
|
934 |
forall_intr_vars graph_implies_dom COMP (f_def COMP fundef_default_value)
|
|
935 |
|
|
936 |
fun mk_trsimp clause psimp =
|
|
937 |
let
|
|
938 |
val ClauseInfo {qglr = (oqs, _, _, _), cdata =
|
|
939 |
ClauseContext {ctxt, cqs, gs, lhs, rhs, ...}, ...} = clause
|
|
940 |
val thy = ProofContext.theory_of ctxt
|
|
941 |
val rhs_f = Pattern.rewrite_term thy [(fvar, f)] [] rhs
|
|
942 |
|
|
943 |
val trsimp = Logic.list_implies(gs,
|
|
944 |
HOLogic.mk_Trueprop (HOLogic.mk_eq(f $ lhs, rhs_f))) (* "f lhs = rhs" *)
|
|
945 |
val lhs_acc = (mk_acc domT R $ lhs) (* "acc R lhs" *)
|
|
946 |
fun simp_default_tac ss =
|
|
947 |
asm_full_simp_tac (ss addsimps [default_thm, Let_def])
|
|
948 |
in
|
|
949 |
Goal.prove ctxt [] [] trsimp (fn _ =>
|
|
950 |
rtac (instantiate' [] [SOME (cterm_of thy lhs_acc)] case_split) 1
|
|
951 |
THEN (rtac (Thm.forall_elim_vars 0 psimp) THEN_ALL_NEW assume_tac) 1
|
|
952 |
THEN (simp_default_tac (simpset_of ctxt) 1)
|
|
953 |
THEN TRY ((etac not_acc_down 1)
|
|
954 |
THEN ((etac R_cases)
|
|
955 |
THEN_ALL_NEW (simp_default_tac (simpset_of ctxt))) 1))
|
|
956 |
|> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
|
|
957 |
end
|
|
958 |
in
|
|
959 |
map2 mk_trsimp clauses psimps
|
|
960 |
end
|
|
961 |
|
|
962 |
|
|
963 |
(* nominal *)
|
|
964 |
fun prepare_nominal_function config defname [((fname, fT), mixfix)] abstract_qglrs lthy =
|
|
965 |
let
|
|
966 |
val FunctionConfig {domintros, tailrec, default=default_opt, ...} = config
|
|
967 |
|
|
968 |
val default_str = the_default "%x. undefined" default_opt (*FIXME dynamic scoping*)
|
|
969 |
val fvar = Free (fname, fT)
|
|
970 |
val domT = domain_type fT
|
|
971 |
val ranT = range_type fT
|
|
972 |
|
|
973 |
val default = Syntax.parse_term lthy default_str
|
|
974 |
|> Type.constraint fT |> Syntax.check_term lthy
|
|
975 |
|
|
976 |
val (globals, ctxt') = fix_globals domT ranT fvar lthy
|
|
977 |
|
|
978 |
val Globals { x, h, ... } = globals
|
|
979 |
|
|
980 |
val clauses = map (mk_clause_context x ctxt') abstract_qglrs
|
|
981 |
|
|
982 |
val n = length abstract_qglrs
|
|
983 |
|
|
984 |
fun build_tree (ClauseContext { ctxt, rhs, ...}) =
|
|
985 |
Function_Ctx_Tree.mk_tree (fname, fT) h ctxt rhs
|
|
986 |
|
|
987 |
val trees = map build_tree clauses
|
|
988 |
val RCss = map find_calls trees
|
|
989 |
|
2707
|
990 |
val ((G, GIntro_thms, G_elim, G_induct), lthy) =
|
2665
|
991 |
PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy
|
|
992 |
|
|
993 |
val ((f, (_, f_defthm)), lthy) =
|
|
994 |
PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy
|
|
995 |
|
|
996 |
val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss
|
|
997 |
val trees = map (Function_Ctx_Tree.inst_tree (ProofContext.theory_of lthy) fvar f) trees
|
|
998 |
|
|
999 |
val ((R, RIntro_thmss, R_elim), lthy) =
|
|
1000 |
PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT abstract_qglrs clauses RCss) lthy
|
|
1001 |
|
|
1002 |
val (_, lthy) =
|
|
1003 |
Local_Theory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy
|
|
1004 |
|
|
1005 |
val newthy = ProofContext.theory_of lthy
|
|
1006 |
val clauses = map (transfer_clause_ctx newthy) clauses
|
|
1007 |
|
|
1008 |
val cert = cterm_of (ProofContext.theory_of lthy)
|
|
1009 |
|
|
1010 |
val xclauses = PROFILE "xclauses"
|
|
1011 |
(map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees
|
|
1012 |
RCss GIntro_thms) RIntro_thmss
|
|
1013 |
|
|
1014 |
val complete =
|
|
1015 |
mk_completeness globals clauses abstract_qglrs |> cert |> Thm.assume
|
|
1016 |
|
|
1017 |
val compat =
|
|
1018 |
mk_compat_proof_obligations domT ranT fvar f abstract_qglrs
|
|
1019 |
|> map (cert #> Thm.assume)
|
|
1020 |
|
2707
|
1021 |
val G_eqvt = mk_eqvt G |> cert |> Thm.assume
|
|
1022 |
|
2665
|
1023 |
val compat_store = store_compat_thms n compat
|
|
1024 |
|
|
1025 |
val (goalstate, values) = PROFILE "prove_stuff"
|
|
1026 |
(prove_stuff lthy globals G f R xclauses complete compat
|
|
1027 |
compat_store G_elim G_eqvt) f_defthm
|
|
1028 |
|
|
1029 |
val mk_trsimps =
|
|
1030 |
mk_trsimps lthy globals f G R f_defthm R_elim G_induct xclauses
|
|
1031 |
|
|
1032 |
fun mk_partial_rules provedgoal =
|
|
1033 |
let
|
|
1034 |
val newthy = theory_of_thm provedgoal (*FIXME*)
|
|
1035 |
|
2707
|
1036 |
val ((graph_is_function, complete_thm), _) =
|
2665
|
1037 |
provedgoal
|
|
1038 |
|> Conjunction.elim
|
2707
|
1039 |
|>> Conjunction.elim
|
|
1040 |
|>> apfst (Thm.forall_elim_vars 0)
|
2665
|
1041 |
|
|
1042 |
val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff)
|
|
1043 |
|
|
1044 |
val psimps = PROFILE "Proving simplification rules"
|
|
1045 |
(mk_psimps newthy globals R xclauses values f_iff) graph_is_function
|
|
1046 |
|
|
1047 |
val simple_pinduct = PROFILE "Proving partial induction rule"
|
|
1048 |
(mk_partial_induct_rule newthy globals R complete_thm) xclauses
|
|
1049 |
|
|
1050 |
val total_intro = PROFILE "Proving nested termination rule"
|
|
1051 |
(mk_nest_term_rule newthy globals R R_elim) xclauses
|
|
1052 |
|
|
1053 |
val dom_intros =
|
|
1054 |
if domintros then SOME (PROFILE "Proving domain introduction rules"
|
|
1055 |
(map (mk_domain_intro lthy globals R R_elim)) xclauses)
|
|
1056 |
else NONE
|
|
1057 |
val trsimps = if tailrec then SOME (mk_trsimps psimps) else NONE
|
|
1058 |
|
|
1059 |
in
|
|
1060 |
FunctionResult {fs=[f], G=G, R=R, cases=complete_thm,
|
|
1061 |
psimps=psimps, simple_pinducts=[simple_pinduct],
|
|
1062 |
termination=total_intro, trsimps=trsimps,
|
|
1063 |
domintros=dom_intros}
|
|
1064 |
end
|
|
1065 |
in
|
|
1066 |
((f, goalstate, mk_partial_rules), lthy)
|
|
1067 |
end
|
|
1068 |
|
|
1069 |
|
|
1070 |
end
|