equal
deleted
inserted
replaced
37 thm list list -> thm list -> thm list -> thm list -> thm list -> tactic |
37 thm list list -> thm list -> thm list -> thm list -> thm list -> tactic |
38 val mk_rel_sel_tac: Proof.context -> cterm -> cterm -> thm -> thm list -> thm list -> thm list -> |
38 val mk_rel_sel_tac: Proof.context -> cterm -> cterm -> thm -> thm list -> thm list -> thm list -> |
39 thm list -> thm list -> tactic |
39 thm list -> thm list -> tactic |
40 val mk_sel_map_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> tactic |
40 val mk_sel_map_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> tactic |
41 val mk_sel_set_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> tactic |
41 val mk_sel_set_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> tactic |
|
42 val mk_set_cases_tac: Proof.context -> cterm -> thm list -> thm -> thm list -> tactic |
42 val mk_set_empty_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic |
43 val mk_set_empty_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic |
43 val mk_set_induct0_tac: Proof.context -> cterm list -> thm list -> thm list -> thm list -> |
44 val mk_set_induct0_tac: Proof.context -> cterm list -> thm list -> thm list -> thm list -> |
44 thm list -> thm list -> thm list -> thm list -> tactic |
45 thm list -> thm list -> thm list -> thm list -> tactic |
45 val mk_set_intros_tac: Proof.context -> thm list -> tactic |
46 val mk_set_intros_tac: Proof.context -> thm list -> tactic |
46 end; |
47 end; |
300 ALLGOALS (REPEAT o (resolve_tac @{thms UnI1 UnI2 imageI} ORELSE' |
301 ALLGOALS (REPEAT o (resolve_tac @{thms UnI1 UnI2 imageI} ORELSE' |
301 eresolve_tac @{thms UN_I UN_I[rotated] imageE} ORELSE' |
302 eresolve_tac @{thms UN_I UN_I[rotated] imageE} ORELSE' |
302 hyp_subst_tac ctxt) THEN' |
303 hyp_subst_tac ctxt) THEN' |
303 (rtac @{thm singletonI} ORELSE' atac)); |
304 (rtac @{thm singletonI} ORELSE' atac)); |
304 |
305 |
|
306 fun mk_set_cases_tac ctxt ct assms exhaust sets = |
|
307 HEADGOAL (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW hyp_subst_tac ctxt) THEN |
|
308 unfold_thms_tac ctxt sets THEN |
|
309 REPEAT_DETERM (HEADGOAL |
|
310 (eresolve_tac @{thms FalseE emptyE singletonE UnE UN_E insertE} ORELSE' |
|
311 hyp_subst_tac ctxt ORELSE' |
|
312 SELECT_GOAL (SOLVE (HEADGOAL (eresolve_tac assms THEN' REPEAT_DETERM o atac))))); |
|
313 |
305 fun mk_set_empty_tac ctxt ct exhaust sets discs = |
314 fun mk_set_empty_tac ctxt ct exhaust sets discs = |
306 TRYALL Goal.conjunction_tac THEN |
315 TRYALL Goal.conjunction_tac THEN |
307 ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW |
316 ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW |
308 REPEAT_DETERM o hyp_subst_tac ctxt) THEN |
317 REPEAT_DETERM o hyp_subst_tac ctxt) THEN |
309 unfold_thms_tac ctxt (sets @ map_filter (fn thm => |
318 unfold_thms_tac ctxt (sets @ map_filter (fn thm => |
312 |
321 |
313 fun mk_set_intros_tac ctxt sets = |
322 fun mk_set_intros_tac ctxt sets = |
314 TRYALL Goal.conjunction_tac THEN |
323 TRYALL Goal.conjunction_tac THEN |
315 unfold_thms_tac ctxt sets THEN |
324 unfold_thms_tac ctxt sets THEN |
316 TRYALL (REPEAT o |
325 TRYALL (REPEAT o |
317 (resolve_tac @{thms UnI1 UnI2} ORELSE' eresolve_tac @{thms UN_I UN_I[rotated]}) THEN' |
326 (resolve_tac @{thms UnI1 UnI2} ORELSE' |
318 (rtac @{thm singletonI} ORELSE' atac)); |
327 eresolve_tac @{thms UN_I UN_I[rotated]}) THEN' (rtac @{thm singletonI} ORELSE' atac)); |
319 |
328 |
320 fun mk_set_induct0_tac ctxt cts assms dtor_set_inducts exhausts set_pre_defs ctor_defs dtor_ctors |
329 fun mk_set_induct0_tac ctxt cts assms dtor_set_inducts exhausts set_pre_defs ctor_defs dtor_ctors |
321 Abs_pre_inverses = |
330 Abs_pre_inverses = |
322 let |
331 let |
323 val assms_ctor_defs = |
332 val assms_ctor_defs = |