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 (** building proof obligations *) |
126 (** building proof obligations *) |
127 fun mk_eqvt_proof_obligation qs fvar (_, 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 Term.list_all_free vs |
129 |> curry Logic.list_implies (map prop_of assms) |
130 |> curry Logic.list_implies (map prop_of assms) |
130 |> curry Term.list_abs_free qs |
131 |> curry Term.list_abs_free qs |
131 |> strip_abs_body |
132 |> strip_abs_body |
132 |
133 |
133 (** building proof obligations *) |
134 (** building proof obligations *) |
263 let |
264 let |
264 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 |
265 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 |
266 |
267 |
267 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)) |
268 in if j < i then |
272 in if j < i then |
269 let |
273 let |
270 val compat = lookup_compat_thm j i cts |
274 val compat = lookup_compat_thm j i cts |
271 in |
275 in |
272 compat (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) |
276 compat (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) |
273 |> fold Thm.forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) |
277 |> 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))) |
274 |> fold Thm.elim_implies eqvtsj (* nominal *) |
279 |> fold Thm.elim_implies eqvtsj (* nominal *) |
275 |> fold Thm.elim_implies agsj |
280 |> fold Thm.elim_implies agsj |
276 |> fold Thm.elim_implies agsi |
281 |> fold Thm.elim_implies agsi |
277 |> Thm.elim_implies ((Thm.assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *) |
282 |> Thm.elim_implies ((Thm.assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *) |
278 end |
283 end |
280 let |
285 let |
281 val compat = lookup_compat_thm i j cts |
286 val compat = lookup_compat_thm i j cts |
282 in |
287 in |
283 compat (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) |
288 compat (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) |
284 |> fold Thm.forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) |
289 |> 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))) |
285 |> fold Thm.elim_implies eqvtsi (* nominal *) |
291 |> fold Thm.elim_implies eqvtsi (* nominal *) |
286 |> fold Thm.elim_implies agsi |
292 |> fold Thm.elim_implies agsi |
287 |> fold Thm.elim_implies agsj |
293 |> fold Thm.elim_implies agsj |
288 |> Thm.elim_implies (Thm.assume lhsi_eq_lhsj) |
294 |> Thm.elim_implies (Thm.assume lhsi_eq_lhsj) |
289 |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *) |
295 |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *) |
334 Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_eqvt |
340 Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_eqvt |
335 |
341 |
336 fun prep_eqvt (RCInfo {llRI, RIvs, CCas, ...}) = |
342 fun prep_eqvt (RCInfo {llRI, RIvs, CCas, ...}) = |
337 (llRI RS ih_eqvt_case) |
343 (llRI RS ih_eqvt_case) |
338 |> fold_rev (Thm.implies_intr o cprop_of) CCas |
344 |> fold_rev (Thm.implies_intr o cprop_of) CCas |
339 (* fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs *) |
345 |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs |
340 in |
346 in |
341 map prep_eqvt RCs |
347 map prep_eqvt RCs |
342 |> map (fold_rev (Thm.implies_intr o cprop_of) ags) |
348 |> map (fold_rev (Thm.implies_intr o cprop_of) ags) |
343 |> map (Thm.implies_intr (cprop_of case_hyp)) |
349 |> map (Thm.implies_intr (cprop_of case_hyp)) |
344 |> map (fold_rev Thm.forall_intr cqs) |
350 |> map (fold_rev Thm.forall_intr cqs) |