155 |> strip_abs_body |
155 |> strip_abs_body |
156 |
156 |
157 (** building proof obligations *) |
157 (** building proof obligations *) |
158 fun mk_compat_proof_obligations domT ranT fvar f RCss inv glrs = |
158 fun mk_compat_proof_obligations domT ranT fvar f RCss inv glrs = |
159 let |
159 let |
160 fun mk_impl (((qs, gs, lhs, rhs), RCs), ((qs', gs', lhs', rhs'), _)) = |
160 fun mk_impl (((qs, gs, lhs, rhs), RCs_lhs), ((qs', gs', lhs', rhs'), RCs_rhs)) = |
161 let |
161 let |
162 val shift = incr_boundvars (length qs') |
162 val shift = incr_boundvars (length qs') |
163 val eqvts_proof_obligations = map (shift o mk_eqvt_proof_obligation qs fvar) RCs |
163 val eqvts_obligations_lhs = map (shift o mk_eqvt_proof_obligation qs fvar) RCs_lhs |
164 val invs_proof_obligations = map (shift o mk_inv_proof_obligation inv qs fvar) RCs |
164 val eqvts_obligations_rhs = map (mk_eqvt_proof_obligation qs' fvar) RCs_rhs |
|
165 val invs_obligations_lhs = map (shift o mk_inv_proof_obligation inv qs fvar) RCs_lhs |
|
166 val invs_obligations_rhs = map (mk_inv_proof_obligation inv qs' fvar) RCs_rhs |
165 in |
167 in |
166 Logic.mk_implies |
168 Logic.mk_implies |
167 (HOLogic.mk_Trueprop (HOLogic.eq_const domT $ shift lhs $ lhs'), |
169 (HOLogic.mk_Trueprop (HOLogic.eq_const domT $ shift lhs $ lhs'), |
168 HOLogic.mk_Trueprop (HOLogic.eq_const ranT $ shift rhs $ rhs')) |
170 HOLogic.mk_Trueprop (HOLogic.eq_const ranT $ shift rhs $ rhs')) |
169 |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs') |
171 |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs') |
170 |> fold_rev (curry Logic.mk_implies) invs_proof_obligations (* nominal *) |
172 |> fold_rev (curry Logic.mk_implies) invs_obligations_rhs (* nominal *) |
171 |> fold_rev (curry Logic.mk_implies) eqvts_proof_obligations (* nominal *) |
173 |> fold_rev (curry Logic.mk_implies) invs_obligations_lhs (* nominal *) |
|
174 |> fold_rev (curry Logic.mk_implies) eqvts_obligations_rhs (* nominal *) |
|
175 |> fold_rev (curry Logic.mk_implies) eqvts_obligations_lhs (* nominal *) |
172 |> fold_rev (fn (n,T) => fn b => Term.all T $ Abs(n,T,b)) (qs @ qs') |
176 |> fold_rev (fn (n,T) => fn b => Term.all T $ Abs(n,T,b)) (qs @ qs') |
173 |> curry abstract_over fvar |
177 |> curry abstract_over fvar |
174 |> curry subst_bound f |
178 |> curry subst_bound f |
175 end |
179 end |
176 in |
180 in |
296 val compat = lookup_compat_thm j i cts |
300 val compat = lookup_compat_thm j i cts |
297 in |
301 in |
298 compat (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) |
302 compat (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) |
299 |> fold Thm.forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) |
303 |> fold Thm.forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) |
300 |> fold Thm.elim_implies eqvtsj (* nominal *) |
304 |> fold Thm.elim_implies eqvtsj (* nominal *) |
|
305 |> fold Thm.elim_implies eqvtsi (* nominal *) |
301 |> fold Thm.elim_implies invsj (* nominal *) |
306 |> fold Thm.elim_implies invsj (* nominal *) |
|
307 |> fold Thm.elim_implies invsi (* nominal *) |
302 |> fold Thm.elim_implies agsj |
308 |> fold Thm.elim_implies agsj |
303 |> fold Thm.elim_implies agsi |
309 |> fold Thm.elim_implies agsi |
304 |> Thm.elim_implies ((Thm.assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *) |
310 |> Thm.elim_implies ((Thm.assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *) |
305 end |
311 end |
306 else |
312 else |
308 val compat = lookup_compat_thm i j cts |
314 val compat = lookup_compat_thm i j cts |
309 in |
315 in |
310 compat (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) |
316 compat (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) |
311 |> fold Thm.forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) |
317 |> fold Thm.forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) |
312 |> fold Thm.elim_implies eqvtsi (* nominal *) |
318 |> fold Thm.elim_implies eqvtsi (* nominal *) |
|
319 |> fold Thm.elim_implies eqvtsj (* nominal *) |
313 |> fold Thm.elim_implies invsi (* nominal *) |
320 |> fold Thm.elim_implies invsi (* nominal *) |
|
321 |> fold Thm.elim_implies invsj (* nominal *) |
314 |> fold Thm.elim_implies agsi |
322 |> fold Thm.elim_implies agsi |
315 |> fold Thm.elim_implies agsj |
323 |> fold Thm.elim_implies agsj |
316 |> Thm.elim_implies (Thm.assume lhsi_eq_lhsj) |
324 |> Thm.elim_implies (Thm.assume lhsi_eq_lhsj) |
317 |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *) |
325 |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *) |
318 end |
326 end |