141 |
141 |
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 |> fold_rev (Logic.all o Free) vs |
147 |> fold_rev absfree 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 |> fold_rev (Logic.all o Free) vs |
154 |> fold_rev absfree 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 = |
171 |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs') |
171 |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs') |
172 |> fold_rev (curry Logic.mk_implies) invs_obligations_rhs (* nominal *) |
172 |> fold_rev (curry Logic.mk_implies) invs_obligations_rhs (* nominal *) |
173 |> fold_rev (curry Logic.mk_implies) invs_obligations_lhs (* nominal *) |
173 |> fold_rev (curry Logic.mk_implies) invs_obligations_lhs (* nominal *) |
174 |> fold_rev (curry Logic.mk_implies) eqvts_obligations_rhs (* nominal *) |
174 |> fold_rev (curry Logic.mk_implies) eqvts_obligations_rhs (* nominal *) |
175 |> fold_rev (curry Logic.mk_implies) eqvts_obligations_lhs (* nominal *) |
175 |> fold_rev (curry Logic.mk_implies) eqvts_obligations_lhs (* nominal *) |
176 |> fold_rev (fn (n,T) => fn b => Term.all T $ Abs(n,T,b)) (qs @ qs') |
176 |> fold_rev (fn (n,T) => fn b => Logic.all_const T $ Abs(n,T,b)) (qs @ qs') |
177 |> curry abstract_over fvar |
177 |> curry abstract_over fvar |
178 |> curry subst_bound f |
178 |> curry subst_bound f |
179 end |
179 end |
180 in |
180 in |
181 map mk_impl (unordered_pairs (glrs ~~ RCss)) |
181 map mk_impl (unordered_pairs (glrs ~~ RCss)) |
533 let |
533 let |
534 val Globals {h, domT, ranT, x, ...} = globals |
534 val Globals {h, domT, ranT, x, ...} = globals |
535 val thy = Proof_Context.theory_of ctxt |
535 val thy = Proof_Context.theory_of ctxt |
536 |
536 |
537 (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *) |
537 (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *) |
538 val ihyp = Term.all domT $ Abs ("z", domT, |
538 val ihyp = Logic.all_const domT $ Abs ("z", domT, |
539 Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x), |
539 Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x), |
540 HOLogic.mk_Trueprop (Const (@{const_name Ex1}, (ranT --> boolT) --> boolT) $ |
540 HOLogic.mk_Trueprop (Const (@{const_name Ex1}, (ranT --> boolT) --> boolT) $ |
541 Abs ("y", ranT, G $ Bound 1 $ Bound 0)))) |
541 Abs ("y", ranT, G $ Bound 1 $ Bound 0)))) |
542 |> cterm_of thy |
542 |> cterm_of thy |
543 |
543 |
758 Logic.mk_implies (HOLogic.mk_Trueprop (R $ z $ x), |
758 Logic.mk_implies (HOLogic.mk_Trueprop (R $ z $ x), |
759 HOLogic.mk_Trueprop (D $ z))))) |
759 HOLogic.mk_Trueprop (D $ z))))) |
760 |> cterm_of thy |
760 |> cterm_of thy |
761 |
761 |
762 (* Inductive Hypothesis: !!z. (z,x):R ==> P z *) |
762 (* Inductive Hypothesis: !!z. (z,x):R ==> P z *) |
763 val ihyp = Term.all domT $ Abs ("z", domT, |
763 val ihyp = Logic.all_const domT $ Abs ("z", domT, |
764 Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x), |
764 Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x), |
765 HOLogic.mk_Trueprop (P $ Bound 0))) |
765 HOLogic.mk_Trueprop (P $ Bound 0))) |
766 |> cterm_of thy |
766 |> cterm_of thy |
767 |
767 |
768 val aihyp = Thm.assume ihyp |
768 val aihyp = Thm.assume ihyp |
938 val wfR' = HOLogic.mk_Trueprop (Const (@{const_name Wellfounded.wfP}, |
938 val wfR' = HOLogic.mk_Trueprop (Const (@{const_name Wellfounded.wfP}, |
939 (domT --> domT --> boolT) --> boolT) $ R') |
939 (domT --> domT --> boolT) --> boolT) $ R') |
940 |> cterm_of thy (* "wf R'" *) |
940 |> cterm_of thy (* "wf R'" *) |
941 |
941 |
942 (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *) |
942 (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *) |
943 val ihyp = Term.all domT $ Abs ("z", domT, |
943 val ihyp = Logic.all_const domT $ Abs ("z", domT, |
944 Logic.mk_implies (HOLogic.mk_Trueprop (R' $ Bound 0 $ x), |
944 Logic.mk_implies (HOLogic.mk_Trueprop (R' $ Bound 0 $ x), |
945 HOLogic.mk_Trueprop (acc_R $ Bound 0))) |
945 HOLogic.mk_Trueprop (acc_R $ Bound 0))) |
946 |> cterm_of thy |
946 |> cterm_of thy |
947 |
947 |
948 val ihyp_a = Thm.assume ihyp |> Thm.forall_elim_vars 0 |
948 val ihyp_a = Thm.assume ihyp |> Thm.forall_elim_vars 0 |