121 in |
121 in |
122 Const (@{const_name eqvt}, ty --> @{typ bool}) $ trm |
122 Const (@{const_name eqvt}, ty --> @{typ bool}) $ trm |
123 |> HOLogic.mk_Trueprop |
123 |> HOLogic.mk_Trueprop |
124 end |
124 end |
125 |
125 |
126 (* nominal *) |
126 fun mk_eqvt_proof_obligation qs fvar (assms, arg) = |
127 fun find_calls2 f t = |
127 mk_eqvt_at (fvar, arg) |
128 let |
128 |> curry Logic.list_implies assms |
129 fun aux (g $ arg) = aux g #> aux arg #> (if f = g then cons ((g, arg)) else I) |
129 |> curry Term.list_abs_free qs |
130 | aux (Abs (_, _, t)) = aux t |
130 |> strip_abs_body |
131 | aux _ = I |
|
132 in |
|
133 aux t [] |
|
134 end |
|
135 |
|
136 |
|
137 |
131 |
138 (** building proof obligations *) |
132 (** building proof obligations *) |
139 |
133 |
140 fun mk_compat_proof_obligations domT ranT fvar f glrs = |
134 fun mk_compat_proof_obligations lthy domT ranT fvar f RCss glrs = |
141 let |
135 let |
142 fun mk_impl ((qs, gs, lhs, rhs), (qs', gs', lhs', rhs')) = |
136 fun mk_impl (((qs, gs, lhs, rhs), RCs), ((qs', gs', lhs', rhs'), _)) = |
143 let |
137 let |
144 val shift = incr_boundvars (length qs') |
138 val shift = incr_boundvars (length qs') |
145 |
139 |
146 val RCs_rhs = find_calls2 fvar rhs (* nominal : FIXME : recursive calls should be passed here *) |
140 val rc_args = map (fn (_, thms, args) => (map prop_of thms, args)) RCs |
|
141 val tt = map (shift o mk_eqvt_proof_obligation qs fvar) rc_args |
147 in |
142 in |
148 Logic.mk_implies |
143 Logic.mk_implies |
149 (HOLogic.mk_Trueprop (HOLogic.eq_const domT $ shift lhs $ lhs'), |
144 (HOLogic.mk_Trueprop (HOLogic.eq_const domT $ shift lhs $ lhs'), |
150 HOLogic.mk_Trueprop (HOLogic.eq_const ranT $ shift rhs $ rhs')) |
145 HOLogic.mk_Trueprop (HOLogic.eq_const ranT $ shift rhs $ rhs')) |
151 |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs') |
146 |> 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 *) |
147 |> fold_rev (curry Logic.mk_implies) tt (* nominal *) |
153 |> fold_rev (fn (n,T) => fn b => Term.all T $ Abs(n,T,b)) (qs @ qs') |
148 |> fold_rev (fn (n,T) => fn b => Term.all T $ Abs(n,T,b)) (qs @ qs') |
154 |> curry abstract_over fvar |
149 |> curry abstract_over fvar |
155 |> curry subst_bound f |
150 |> curry subst_bound f |
156 end |
151 end |
157 in |
152 in |
158 map mk_impl (unordered_pairs glrs) |
153 map mk_impl (unordered_pairs (glrs ~~ RCss)) |
159 end |
154 end |
160 |
155 |
161 |
156 |
162 fun mk_completeness (Globals {x, Pbool, ...}) clauses qglrs = |
157 fun mk_completeness (Globals {x, Pbool, ...}) clauses qglrs = |
163 let |
158 let |
266 (* nominal *) |
261 (* nominal *) |
267 (* Returns "Gsi, Gsj, lhs_i = lhs_j |-- rhs_j_f = rhs_i_f" *) |
262 (* Returns "Gsi, Gsj, lhs_i = lhs_j |-- rhs_j_f = rhs_i_f" *) |
268 (* if j < i, then turn around *) |
263 (* if j < i, then turn around *) |
269 fun get_compat_thm thy cts eqvtsi eqvtsj i j ctxi ctxj = |
264 fun get_compat_thm thy cts eqvtsi eqvtsj i j ctxi ctxj = |
270 let |
265 let |
271 val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi |
266 val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,case_hyp=case_hypi,...} = ctxi |
272 val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj |
267 val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,case_hyp=case_hypj,...} = ctxj |
273 |
268 |
274 val lhsi_eq_lhsj = cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj))) |
269 val lhsi_eq_lhsj = cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj))) |
275 in if j < i then |
270 in if j < i then |
276 let |
271 let |
277 val compat = lookup_compat_thm j i cts |
272 val compat = lookup_compat_thm j i cts |
278 in |
273 in |
279 compat (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) |
274 compat (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) |
280 |> fold Thm.forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) |
275 |> fold Thm.forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) |
281 |> fold Thm.elim_implies (rev eqvtsj) (* nominal *) |
276 |> fold Thm.elim_implies eqvtsj (* nominal *) |
282 |> fold Thm.elim_implies agsj |
277 |> fold Thm.elim_implies agsj |
283 |> fold Thm.elim_implies agsi |
278 |> fold Thm.elim_implies agsi |
284 |> Thm.elim_implies ((Thm.assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *) |
279 |> Thm.elim_implies ((Thm.assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *) |
285 end |
280 end |
286 else |
281 else |
287 let |
282 let |
288 val compat = lookup_compat_thm i j cts |
283 val compat = lookup_compat_thm i j cts |
289 in |
284 in |
290 compat (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) |
285 compat (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) |
291 |> fold Thm.forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) |
286 |> fold Thm.forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) |
292 |> fold Thm.elim_implies (rev eqvtsi) (* nominal *) |
287 |> fold Thm.elim_implies eqvtsi (* nominal *) |
293 |> fold Thm.elim_implies agsi |
288 |> fold Thm.elim_implies agsi |
294 |> fold Thm.elim_implies agsj |
289 |> fold Thm.elim_implies agsj |
295 |> Thm.elim_implies (Thm.assume lhsi_eq_lhsj) |
290 |> Thm.elim_implies (Thm.assume lhsi_eq_lhsj) |
296 |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *) |
291 |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *) |
297 end |
292 end |
330 (* nominal *) |
325 (* nominal *) |
331 (* Generates the eqvt lemmas for each clause *) |
326 (* Generates the eqvt lemmas for each clause *) |
332 fun mk_eqvt_lemma thy ih_eqvt clause = |
327 fun mk_eqvt_lemma thy ih_eqvt clause = |
333 let |
328 let |
334 val ClauseInfo {cdata=ClauseContext {cqs, ags, case_hyp, ...}, RCs, ...} = clause |
329 val ClauseInfo {cdata=ClauseContext {cqs, ags, case_hyp, ...}, RCs, ...} = clause |
335 |
330 |
336 local open Conv in |
331 local open Conv in |
337 val ih_conv = arg1_conv o arg_conv o arg_conv |
332 val ih_conv = arg1_conv o arg_conv o arg_conv |
338 end |
333 end |
339 |
334 |
340 val ih_eqvt_case = |
335 val ih_eqvt_case = |
418 |
413 |
419 fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = |
414 fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = |
420 (llRI RS ih_intro_case) |
415 (llRI RS ih_intro_case) |
421 |> fold_rev (Thm.implies_intr o cprop_of) CCas |
416 |> fold_rev (Thm.implies_intr o cprop_of) CCas |
422 |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs |
417 |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs |
423 |
418 |
424 val existence = fold (curry op COMP o prep_RC) RCs lGI |
419 val existence = fold (curry op COMP o prep_RC) RCs lGI |
425 |
420 |
426 val P = cterm_of thy (mk_eq (y, rhsC)) |
421 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))) |
422 val G_lhs_y = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (G $ lhs $ y))) |
428 |
423 |
429 val unique_clauses = |
424 val unique_clauses = |
430 map2 (mk_uniqueness_clause thy globals compat_store eqvtlems clausei) clauses replems |
425 map2 (mk_uniqueness_clause thy globals compat_store eqvtlems clausei) clauses replems |
431 |
426 |
432 fun elim_implies_eta A AB = |
427 fun elim_implies_eta A AB = |
433 Thm.compose_no_flatten true (A, 0) 1 AB |> Seq.list_of |> the_single |
428 Thm.compose_no_flatten true (A, 0) 1 AB |> Seq.list_of |> the_single |
434 |
429 |
435 val uniqueness = G_cases |
430 val uniqueness = G_cases |
436 |> Thm.forall_elim (cterm_of thy lhs) |
431 |> Thm.forall_elim (cterm_of thy lhs) |
437 |> Thm.forall_elim (cterm_of thy y) |
432 |> Thm.forall_elim (cterm_of thy y) |
438 |> Thm.forall_elim P |
433 |> Thm.forall_elim P |
439 |> Thm.elim_implies G_lhs_y |
434 |> Thm.elim_implies G_lhs_y |