67 {context = ctxt, prems = _} = |
67 {context = ctxt, prems = _} = |
68 let |
68 let |
69 val n = length set_naturals; |
69 val n = length set_naturals; |
70 in |
70 in |
71 if null set_naturals then |
71 if null set_naturals then |
72 unfold_defs_tac ctxt rel_O_Grs THEN EVERY' [rtac @{thm Gr_UNIV_id}, rtac map_id] 1 |
72 unfold_thms_tac ctxt rel_O_Grs THEN EVERY' [rtac @{thm Gr_UNIV_id}, rtac map_id] 1 |
73 else unfold_defs_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN |
73 else unfold_thms_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN |
74 EVERY' [rtac equalityI, rtac subsetI, |
74 EVERY' [rtac equalityI, rtac subsetI, |
75 REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}], |
75 REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}], |
76 REPEAT_DETERM o dtac Pair_eqD, |
76 REPEAT_DETERM o dtac Pair_eqD, |
77 REPEAT_DETERM o etac conjE, hyp_subst_tac, |
77 REPEAT_DETERM o etac conjE, hyp_subst_tac, |
78 rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, |
78 rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, |
103 set_naturals]) |
103 set_naturals]) |
104 @{thms fst_convol snd_convol} [map_id', refl])] 1 |
104 @{thms fst_convol snd_convol} [map_id', refl])] 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 unfold_defs_tac ctxt [rel_Gr, @{thm Id_alt}] THEN |
108 unfold_thms_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 subset_UNIV, rtac subsetI, rtac CollectI, |
112 rtac equalityI, rtac subset_UNIV, rtac subsetI, rtac CollectI, |
113 CONJ_WRAP' (K (rtac subset_UNIV)) (1 upto n), rtac refl] 1); |
113 CONJ_WRAP' (K (rtac 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 unfold_defs_tac ctxt rel_O_Grs THEN |
116 unfold_thms_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 unfold_defs_tac ctxt [rel_Id] THEN rtac equalityD2 1 THEN rtac @{thm converse_Id} 1 |
127 unfold_thms_tac ctxt [rel_Id] THEN rtac equalityD2 1 THEN rtac @{thm converse_Id} 1 |
128 else unfold_defs_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN |
128 else unfold_thms_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 Pair_eqD, |
131 REPEAT_DETERM o dtac Pair_eqD, |
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 unfold_defs_tac ctxt [rel_Id] THEN rtac (@{thm Id_O_R} RS sym) 1 |
154 if null set_naturals then unfold_thms_tac ctxt [rel_Id] THEN rtac (@{thm Id_O_R} RS sym) 1 |
155 else unfold_defs_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN |
155 else unfold_thms_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 Pair_eqD, |
158 REPEAT_DETERM o dtac Pair_eqD, |
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 unfold_defs_tac ctxt (rel_O_Grs @ |
200 unfold_thms_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]}, |