1766 @{fold_map 8} (fn b => fn map_b => fn rel_b => fn pred_b => fn set_bs => fn mapx => |
1766 @{fold_map 8} (fn b => fn map_b => fn rel_b => fn pred_b => fn set_bs => fn mapx => |
1767 fn sets => fn T => fn lthy => |
1767 fn sets => fn T => fn lthy => |
1768 define_bnf_consts Hardly_Inline (user_policy Note_Some lthy) false (SOME deads) |
1768 define_bnf_consts Hardly_Inline (user_policy Note_Some lthy) false (SOME deads) |
1769 map_b rel_b pred_b set_bs |
1769 map_b rel_b pred_b set_bs |
1770 (((((((b, T), fold_rev Term.absfree fs' mapx), sets), sbd), |
1770 (((((((b, T), fold_rev Term.absfree fs' mapx), sets), sbd), |
1771 [Const (@{const_name undefined}, T)]), NONE), NONE) lthy) |
1771 [Const (\<^const_name>\<open>undefined\<close>, T)]), NONE), NONE) lthy) |
1772 bs map_bs rel_bs pred_bs set_bss fs_maps setss Ts lthy; |
1772 bs map_bs rel_bs pred_bs set_bss fs_maps setss Ts lthy; |
1773 |
1773 |
1774 val (_, Jconsts, Jconst_defs, mk_Jconsts) = @{split_list 4} Jbnf_consts; |
1774 val (_, Jconsts, Jconst_defs, mk_Jconsts) = @{split_list 4} Jbnf_consts; |
1775 val (_, Jsetss, Jbds_Ds, _, _, _) = @{split_list 6} Jconsts; |
1775 val (_, Jsetss, Jbds_Ds, _, _, _) = @{split_list 6} Jconsts; |
1776 val (Jmap_defs, Jset_defss, Jbd_defs, _, Jrel_defs, Jpred_defs) = |
1776 val (Jmap_defs, Jset_defss, Jbd_defs, _, Jrel_defs, Jpred_defs) = |
2420 fun mk_conjunct set z dummy wit = |
2420 fun mk_conjunct set z dummy wit = |
2421 mk_Ball (set $ z) (Term.absfree y'_copy |
2421 mk_Ball (set $ z) (Term.absfree y'_copy |
2422 (if dummy = NONE orelse member (op =) I (j - 1) then |
2422 (if dummy = NONE orelse member (op =) I (j - 1) then |
2423 HOLogic.mk_imp (HOLogic.mk_eq (z, wit), |
2423 HOLogic.mk_imp (HOLogic.mk_eq (z, wit), |
2424 if member (op =) I (j - 1) then HOLogic.mk_eq (y_copy, y) |
2424 if member (op =) I (j - 1) then HOLogic.mk_eq (y_copy, y) |
2425 else @{term False}) |
2425 else \<^term>\<open>False\<close>) |
2426 else @{term True})); |
2426 else \<^term>\<open>True\<close>)); |
2427 in |
2427 in |
2428 HOLogic.mk_Trueprop |
2428 HOLogic.mk_Trueprop |
2429 (Library.foldr1 HOLogic.mk_conj (@{map 4} mk_conjunct sets Jzs dummys wits)) |
2429 (Library.foldr1 HOLogic.mk_conj (@{map 4} mk_conjunct sets Jzs dummys wits)) |
2430 end; |
2430 end; |
2431 val goals = @{map 5} mk_goal Jsetss_by_range ys ys_copy ys'_copy ls; |
2431 val goals = @{map 5} mk_goal Jsetss_by_range ys ys_copy ys'_copy ls; |