equal
deleted
inserted
replaced
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 Logic.list_implies (map prop_of assms) |
129 |> curry Logic.list_implies (map prop_of assms) |
|
130 |> curry Term.list_all_free vs |
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 *) |
134 fun mk_compat_proof_obligations domT ranT fvar f RCss glrs = |
135 fun mk_compat_proof_obligations domT ranT fvar f RCss glrs = |
334 Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_eqvt |
335 Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_eqvt |
335 |
336 |
336 fun prep_eqvt (RCInfo {llRI, RIvs, CCas, ...}) = |
337 fun prep_eqvt (RCInfo {llRI, RIvs, CCas, ...}) = |
337 (llRI RS ih_eqvt_case) |
338 (llRI RS ih_eqvt_case) |
338 |> fold_rev (Thm.implies_intr o cprop_of) CCas |
339 |> fold_rev (Thm.implies_intr o cprop_of) CCas |
339 (* fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs *) |
340 |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs |
340 in |
341 in |
341 map prep_eqvt RCs |
342 map prep_eqvt RCs |
342 |> map (fold_rev (Thm.implies_intr o cprop_of) ags) |
343 |> map (fold_rev (Thm.implies_intr o cprop_of) ags) |
343 |> map (Thm.implies_intr (cprop_of case_hyp)) |
344 |> map (Thm.implies_intr (cprop_of case_hyp)) |
344 |> map (fold_rev Thm.forall_intr cqs) |
345 |> map (fold_rev Thm.forall_intr cqs) |