69 {context = ctxt, prems = _} = |
69 {context = ctxt, prems = _} = |
70 let |
70 let |
71 val n = length set_naturals; |
71 val n = length set_naturals; |
72 in |
72 in |
73 if null set_naturals then |
73 if null set_naturals then |
74 Local_Defs.unfold_tac ctxt rel_O_Grs THEN EVERY' [rtac @{thm Gr_UNIV_id}, rtac map_id] 1 |
74 unfold_defs_tac ctxt rel_O_Grs THEN EVERY' [rtac @{thm Gr_UNIV_id}, rtac map_id] 1 |
75 else Local_Defs.unfold_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN |
75 else unfold_defs_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN |
76 EVERY' [rtac equalityI, rtac subsetI, |
76 EVERY' [rtac equalityI, rtac subsetI, |
77 REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}], |
77 REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}], |
78 REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]}, |
78 REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]}, |
79 REPEAT_DETERM o etac conjE, hyp_subst_tac, |
79 REPEAT_DETERM o etac conjE, hyp_subst_tac, |
80 rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, |
80 rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, |
103 etac @{thm set_rev_mp}, rtac equalityD1, rtac in_cong, |
103 etac @{thm set_rev_mp}, rtac equalityD1, rtac in_cong, |
104 REPEAT_DETERM_N n o rtac @{thm Gr_def}]] 1 |
104 REPEAT_DETERM_N n o rtac @{thm Gr_def}]] 1 |
105 end; |
105 end; |
106 |
106 |
107 fun mk_rel_Id_tac n rel_Gr map_id {context = ctxt, prems = _} = |
107 fun mk_rel_Id_tac n rel_Gr map_id {context = ctxt, prems = _} = |
108 Local_Defs.unfold_tac ctxt [rel_Gr, @{thm Id_alt}] THEN |
108 unfold_defs_tac ctxt [rel_Gr, @{thm Id_alt}] THEN |
109 subst_tac ctxt [map_id] 1 THEN |
109 subst_tac ctxt [map_id] 1 THEN |
110 (if n = 0 then rtac refl 1 |
110 (if n = 0 then rtac refl 1 |
111 else EVERY' [rtac @{thm arg_cong2[of _ _ _ _ Gr]}, |
111 else EVERY' [rtac @{thm arg_cong2[of _ _ _ _ Gr]}, |
112 rtac equalityI, rtac @{thm subset_UNIV}, rtac subsetI, rtac CollectI, |
112 rtac equalityI, rtac @{thm subset_UNIV}, rtac subsetI, rtac CollectI, |
113 CONJ_WRAP' (K (rtac @{thm subset_UNIV})) (1 upto n), rtac refl] 1); |
113 CONJ_WRAP' (K (rtac @{thm subset_UNIV})) (1 upto n), rtac refl] 1); |
114 |
114 |
115 fun mk_rel_mono_tac rel_O_Grs in_mono {context = ctxt, prems = _} = |
115 fun mk_rel_mono_tac rel_O_Grs in_mono {context = ctxt, prems = _} = |
116 Local_Defs.unfold_tac ctxt rel_O_Grs THEN |
116 unfold_defs_tac ctxt rel_O_Grs THEN |
117 EVERY' [rtac @{thm relcomp_mono}, rtac @{thm iffD2[OF converse_mono]}, |
117 EVERY' [rtac @{thm relcomp_mono}, rtac @{thm iffD2[OF converse_mono]}, |
118 rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac, |
118 rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac, |
119 rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac] 1; |
119 rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac] 1; |
120 |
120 |
121 fun mk_rel_converse_le_tac rel_O_Grs rel_Id map_cong map_comp set_naturals |
121 fun mk_rel_converse_le_tac rel_O_Grs rel_Id map_cong map_comp set_naturals |
122 {context = ctxt, prems = _} = |
122 {context = ctxt, prems = _} = |
123 let |
123 let |
124 val n = length set_naturals; |
124 val n = length set_naturals; |
125 in |
125 in |
126 if null set_naturals then |
126 if null set_naturals then |
127 Local_Defs.unfold_tac ctxt [rel_Id] THEN rtac equalityD2 1 THEN rtac @{thm converse_Id} 1 |
127 unfold_defs_tac ctxt [rel_Id] THEN rtac equalityD2 1 THEN rtac @{thm converse_Id} 1 |
128 else Local_Defs.unfold_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN |
128 else unfold_defs_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN |
129 EVERY' [rtac @{thm subrelI}, |
129 EVERY' [rtac @{thm subrelI}, |
130 REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}], |
130 REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}], |
131 REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]}, |
131 REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]}, |
132 REPEAT_DETERM o etac conjE, hyp_subst_tac, rtac @{thm converseI}, |
132 REPEAT_DETERM o etac conjE, hyp_subst_tac, rtac @{thm converseI}, |
133 rtac @{thm relcompI}, rtac @{thm converseI}, |
133 rtac @{thm relcompI}, rtac @{thm converseI}, |
149 val n = length set_naturals; |
149 val n = length set_naturals; |
150 fun in_tac nthO_in = rtac CollectI THEN' |
150 fun in_tac nthO_in = rtac CollectI THEN' |
151 CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}), |
151 CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}), |
152 rtac @{thm image_subsetI}, rtac nthO_in, etac set_mp, atac]) set_naturals; |
152 rtac @{thm image_subsetI}, rtac nthO_in, etac set_mp, atac]) set_naturals; |
153 in |
153 in |
154 if null set_naturals then Local_Defs.unfold_tac ctxt [rel_Id] THEN rtac (@{thm Id_O_R} RS sym) 1 |
154 if null set_naturals then unfold_defs_tac ctxt [rel_Id] THEN rtac (@{thm Id_O_R} RS sym) 1 |
155 else Local_Defs.unfold_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN |
155 else unfold_defs_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN |
156 EVERY' [rtac equalityI, rtac @{thm subrelI}, |
156 EVERY' [rtac equalityI, rtac @{thm subrelI}, |
157 REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}], |
157 REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}], |
158 REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]}, |
158 REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]}, |
159 REPEAT_DETERM o etac conjE, hyp_subst_tac, |
159 REPEAT_DETERM o etac conjE, hyp_subst_tac, |
160 rtac @{thm relcompI}, rtac @{thm relcompI}, rtac @{thm converseI}, |
160 rtac @{thm relcompI}, rtac @{thm relcompI}, rtac @{thm converseI}, |
195 |
195 |
196 fun mk_in_rel_tac rel_O_Grs m {context = ctxt, prems = _} = |
196 fun mk_in_rel_tac rel_O_Grs m {context = ctxt, prems = _} = |
197 let |
197 let |
198 val ls' = replicate (Int.max (1, m)) (); |
198 val ls' = replicate (Int.max (1, m)) (); |
199 in |
199 in |
200 Local_Defs.unfold_tac ctxt (rel_O_Grs @ |
200 unfold_defs_tac ctxt (rel_O_Grs @ |
201 @{thms Gr_def converse_unfold relcomp_unfold mem_Collect_eq prod.cases Pair_eq}) THEN |
201 @{thms Gr_def converse_unfold relcomp_unfold mem_Collect_eq prod.cases Pair_eq}) THEN |
202 EVERY' [rtac iffI, REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac, rtac exI, |
202 EVERY' [rtac iffI, REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac, rtac exI, |
203 rtac conjI, CONJ_WRAP' (K atac) ls', rtac conjI, rtac refl, rtac refl, |
203 rtac conjI, CONJ_WRAP' (K atac) ls', rtac conjI, rtac refl, rtac refl, |
204 REPEAT_DETERM o eresolve_tac [exE, conjE], rtac exI, rtac conjI, |
204 REPEAT_DETERM o eresolve_tac [exE, conjE], rtac exI, rtac conjI, |
205 REPEAT_DETERM_N 2 o EVERY' [rtac exI, rtac conjI, etac @{thm conjI[OF refl sym]}, |
205 REPEAT_DETERM_N 2 o EVERY' [rtac exI, rtac conjI, etac @{thm conjI[OF refl sym]}, |