76 let |
76 let |
77 val thms = constr_defs @ map mk_sym [rel_eq_of_bnf bnf, rel_conversep_of_bnf bnf, |
77 val thms = constr_defs @ map mk_sym [rel_eq_of_bnf bnf, rel_conversep_of_bnf bnf, |
78 rel_OO_of_bnf bnf] |
78 rel_OO_of_bnf bnf] |
79 in |
79 in |
80 (SELECT_GOAL (Local_Defs.unfold_tac ctxt thms) THEN' rtac (rel_mono_of_bnf bnf) |
80 (SELECT_GOAL (Local_Defs.unfold_tac ctxt thms) THEN' rtac (rel_mono_of_bnf bnf) |
81 THEN_ALL_NEW atac) i |
81 THEN_ALL_NEW assume_tac ctxt) i |
82 end |
82 end |
83 |
83 |
84 fun bi_constraint_tac constr_iff sided_constr_intros ctxt i = |
84 fun bi_constraint_tac constr_iff sided_constr_intros ctxt i = |
85 (SELECT_GOAL (Local_Defs.unfold_tac ctxt [constr_iff]) THEN' |
85 (SELECT_GOAL (Local_Defs.unfold_tac ctxt [constr_iff]) THEN' |
86 CONJ_WRAP' (fn thm => rtac thm THEN_ALL_NEW (REPEAT_DETERM o etac conjE THEN' atac)) sided_constr_intros) i |
86 CONJ_WRAP' (fn thm => rtac thm THEN_ALL_NEW |
|
87 (REPEAT_DETERM o etac conjE THEN' assume_tac ctxt)) sided_constr_intros) i |
87 |
88 |
88 fun generate_relation_constraint_goal ctxt bnf constraint_def = |
89 fun generate_relation_constraint_goal ctxt bnf constraint_def = |
89 let |
90 let |
90 val constr_name = constraint_def |> prop_of |> HOLogic.dest_Trueprop |> fst o HOLogic.dest_eq |
91 val constr_name = constraint_def |> prop_of |> HOLogic.dest_Trueprop |> fst o HOLogic.dest_eq |
91 |> head_of |> fst o dest_Const |
92 |> head_of |> fst o dest_Const |
197 in |
198 in |
198 EVERY' [rtac ext, SELECT_GOAL (Local_Defs.unfold_tac ctxt [@{thm Domainp.simps}, |
199 EVERY' [rtac ext, SELECT_GOAL (Local_Defs.unfold_tac ctxt [@{thm Domainp.simps}, |
199 in_rel_of_bnf bnf, pred_def]), rtac iffI, |
200 in_rel_of_bnf bnf, pred_def]), rtac iffI, |
200 REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE], hyp_subst_tac ctxt, |
201 REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE], hyp_subst_tac ctxt, |
201 CONJ_WRAP' (fn set_map => EVERY' [rtac ballI, dtac (set_map RS equalityD1 RS set_mp), |
202 CONJ_WRAP' (fn set_map => EVERY' [rtac ballI, dtac (set_map RS equalityD1 RS set_mp), |
202 etac imageE, dtac set_rev_mp, atac, REPEAT_DETERM o eresolve_tac [CollectE, @{thm case_prodE}], |
203 etac imageE, dtac set_rev_mp, assume_tac ctxt, |
|
204 REPEAT_DETERM o eresolve_tac [CollectE, @{thm case_prodE}], |
203 hyp_subst_tac ctxt, rtac @{thm iffD2[OF arg_cong2[of _ _ _ _ Domainp, OF refl fst_conv]]}, |
205 hyp_subst_tac ctxt, rtac @{thm iffD2[OF arg_cong2[of _ _ _ _ Domainp, OF refl fst_conv]]}, |
204 etac @{thm DomainPI}]) set_map's, |
206 etac @{thm DomainPI}]) set_map's, |
205 REPEAT_DETERM o etac conjE, REPEAT_DETERM o resolve_tac [exI, (refl RS conjI), rotate_prems 1 conjI], |
207 REPEAT_DETERM o etac conjE, REPEAT_DETERM o resolve_tac [exI, (refl RS conjI), rotate_prems 1 conjI], |
206 rtac refl, rtac (box_equals OF [map_cong0_of_bnf bnf, map_comp_of_bnf bnf RS sym, |
208 rtac refl, rtac (box_equals OF [map_cong0_of_bnf bnf, map_comp_of_bnf bnf RS sym, |
207 map_id_of_bnf bnf]), |
209 map_id_of_bnf bnf]), |
208 REPEAT_DETERM_N n o (EVERY' [rtac @{thm box_equals[OF _ sym[OF o_apply] sym[OF id_apply]]}, |
210 REPEAT_DETERM_N n o (EVERY' [rtac @{thm box_equals[OF _ sym[OF o_apply] sym[OF id_apply]]}, |
209 rtac @{thm fst_conv}]), rtac CollectI, |
211 rtac @{thm fst_conv}]), rtac CollectI, |
210 CONJ_WRAP' (fn set_map => EVERY' [rtac (set_map RS @{thm ord_eq_le_trans}), |
212 CONJ_WRAP' (fn set_map => EVERY' [rtac (set_map RS @{thm ord_eq_le_trans}), |
211 REPEAT_DETERM o resolve_tac [@{thm image_subsetI}, CollectI, @{thm case_prodI}], |
213 REPEAT_DETERM o resolve_tac [@{thm image_subsetI}, CollectI, @{thm case_prodI}], |
212 dtac (rotate_prems 1 bspec), atac, etac @{thm DomainpE}, etac @{thm someI}]) set_map's |
214 dtac (rotate_prems 1 bspec), assume_tac ctxt, |
|
215 etac @{thm DomainpE}, etac @{thm someI}]) set_map's |
213 ] i |
216 ] i |
214 end |
217 end |
215 |
218 |
216 fun prove_Domainp_rel ctxt bnf pred_def = |
219 fun prove_Domainp_rel ctxt bnf pred_def = |
217 let |
220 let |