142 (** building proof obligations *) |
142 (** building proof obligations *) |
143 fun mk_eqvt_proof_obligation qs fvar (vs, assms, arg) = |
143 fun mk_eqvt_proof_obligation qs fvar (vs, assms, arg) = |
144 mk_eqvt_at (fvar, arg) |
144 mk_eqvt_at (fvar, arg) |
145 |> curry Logic.list_implies (map prop_of assms) |
145 |> curry Logic.list_implies (map prop_of assms) |
146 |> curry Term.list_all_free vs |
146 |> curry Term.list_all_free vs |
147 |> curry Term.list_abs_free qs |
147 |> fold_rev absfree qs |
148 |> strip_abs_body |
148 |> strip_abs_body |
149 |
149 |
150 fun mk_inv_proof_obligation inv qs fvar (vs, assms, arg) = |
150 fun mk_inv_proof_obligation inv qs fvar (vs, assms, arg) = |
151 mk_inv inv (fvar, arg) |
151 mk_inv inv (fvar, arg) |
152 |> curry Logic.list_implies (map prop_of assms) |
152 |> curry Logic.list_implies (map prop_of assms) |
153 |> curry Term.list_all_free vs |
153 |> curry Term.list_all_free vs |
154 |> curry Term.list_abs_free qs |
154 |> fold_rev absfree qs |
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 |