124 end |
124 end |
125 |
125 |
126 (** building proof obligations *) |
126 (** building proof obligations *) |
127 fun mk_eqvt_proof_obligation qs fvar (vs, assms, arg) = |
127 fun mk_eqvt_proof_obligation qs fvar (vs, assms, arg) = |
128 mk_eqvt_at (fvar, arg) |
128 mk_eqvt_at (fvar, arg) |
|
129 |> curry Logic.list_implies (map prop_of assms) |
129 |> curry Term.list_all_free vs |
130 |> curry Term.list_all_free vs |
130 |> curry Logic.list_implies (map prop_of assms) |
|
131 |> curry Term.list_abs_free qs |
131 |> curry Term.list_abs_free qs |
132 |> strip_abs_body |
132 |> strip_abs_body |
133 |
133 |
134 (** building proof obligations *) |
134 (** building proof obligations *) |
135 fun mk_compat_proof_obligations domT ranT fvar f RCss glrs = |
135 fun mk_compat_proof_obligations domT ranT fvar f RCss glrs = |
264 let |
264 let |
265 val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,case_hyp=case_hypi,...} = ctxi |
265 val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,case_hyp=case_hypi,...} = ctxi |
266 val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,case_hyp=case_hypj,...} = ctxj |
266 val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,case_hyp=case_hypj,...} = ctxj |
267 |
267 |
268 val lhsi_eq_lhsj = cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj))) |
268 val lhsi_eq_lhsj = cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj))) |
269 |
|
270 val _ = tracing ("eqvtsi\n" ^ cat_lines (map (Syntax.string_of_term_global thy o prop_of) eqvtsi)) |
|
271 val _ = tracing ("eqvtsj\n" ^ cat_lines (map (Syntax.string_of_term_global thy o prop_of) eqvtsj)) |
|
272 in if j < i then |
269 in if j < i then |
273 let |
270 let |
274 val compat = lookup_compat_thm j i cts |
271 val compat = lookup_compat_thm j i cts |
275 in |
272 in |
276 compat (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) |
273 compat (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) |
277 |> fold Thm.forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) |
274 |> fold Thm.forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) |
278 |> tap (fn t => tracing ("1: " ^ Syntax.string_of_term_global thy (prop_of t))) |
|
279 |> fold Thm.elim_implies eqvtsj (* nominal *) |
275 |> fold Thm.elim_implies eqvtsj (* nominal *) |
280 |> fold Thm.elim_implies agsj |
276 |> fold Thm.elim_implies agsj |
281 |> fold Thm.elim_implies agsi |
277 |> fold Thm.elim_implies agsi |
282 |> Thm.elim_implies ((Thm.assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *) |
278 |> Thm.elim_implies ((Thm.assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *) |
283 end |
279 end |
285 let |
281 let |
286 val compat = lookup_compat_thm i j cts |
282 val compat = lookup_compat_thm i j cts |
287 in |
283 in |
288 compat (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) |
284 compat (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) |
289 |> fold Thm.forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) |
285 |> fold Thm.forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) |
290 |> tap (fn t => tracing ("2: " ^ Syntax.string_of_term_global thy (prop_of t))) |
|
291 |> fold Thm.elim_implies eqvtsi (* nominal *) |
286 |> fold Thm.elim_implies eqvtsi (* nominal *) |
292 |> fold Thm.elim_implies agsi |
287 |> fold Thm.elim_implies agsi |
293 |> fold Thm.elim_implies agsj |
288 |> fold Thm.elim_implies agsj |
294 |> Thm.elim_implies (Thm.assume lhsi_eq_lhsj) |
289 |> Thm.elim_implies (Thm.assume lhsi_eq_lhsj) |
295 |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *) |
290 |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *) |