121 in |
121 in |
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 fun mk_eqvt_proof_obligation qs fvar (assms, arg) = |
126 (** building proof obligations *) |
|
127 fun mk_eqvt_proof_obligation qs fvar (_, assms, arg) = |
127 mk_eqvt_at (fvar, arg) |
128 mk_eqvt_at (fvar, arg) |
128 |> curry Logic.list_implies assms |
129 |> curry Logic.list_implies (map prop_of assms) |
129 |> curry Term.list_abs_free qs |
130 |> curry Term.list_abs_free qs |
130 |> strip_abs_body |
131 |> strip_abs_body |
131 |
132 |
132 (** building proof obligations *) |
133 (** building proof obligations *) |
133 |
134 fun mk_compat_proof_obligations domT ranT fvar f RCss glrs = |
134 fun mk_compat_proof_obligations lthy domT ranT fvar f RCss glrs = |
|
135 let |
135 let |
136 fun mk_impl (((qs, gs, lhs, rhs), RCs), ((qs', gs', lhs', rhs'), _)) = |
136 fun mk_impl (((qs, gs, lhs, rhs), RCs), ((qs', gs', lhs', rhs'), _)) = |
137 let |
137 let |
138 val shift = incr_boundvars (length qs') |
138 val shift = incr_boundvars (length qs') |
139 |
139 val eqvts_proof_obligations = map (shift o mk_eqvt_proof_obligation qs fvar) RCs |
140 val rc_args = map (fn (_, thms, args) => (map prop_of thms, args)) RCs |
|
141 val tt = map (shift o mk_eqvt_proof_obligation qs fvar) rc_args |
|
142 in |
140 in |
143 Logic.mk_implies |
141 Logic.mk_implies |
144 (HOLogic.mk_Trueprop (HOLogic.eq_const domT $ shift lhs $ lhs'), |
142 (HOLogic.mk_Trueprop (HOLogic.eq_const domT $ shift lhs $ lhs'), |
145 HOLogic.mk_Trueprop (HOLogic.eq_const ranT $ shift rhs $ rhs')) |
143 HOLogic.mk_Trueprop (HOLogic.eq_const ranT $ shift rhs $ rhs')) |
146 |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs') |
144 |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs') |
147 |> fold_rev (curry Logic.mk_implies) tt (* nominal *) |
145 |> fold_rev (curry Logic.mk_implies) eqvts_proof_obligations (* nominal *) |
148 |> fold_rev (fn (n,T) => fn b => Term.all T $ Abs(n,T,b)) (qs @ qs') |
146 |> fold_rev (fn (n,T) => fn b => Term.all T $ Abs(n,T,b)) (qs @ qs') |
149 |> curry abstract_over fvar |
147 |> curry abstract_over fvar |
150 |> curry subst_bound f |
148 |> curry subst_bound f |
151 end |
149 end |
152 in |
150 in |