equal
deleted
inserted
replaced
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_srel_Id_tac n srel_Gr map_id {context = ctxt, prems = _} = |
107 fun mk_srel_Id_tac n srel_Gr map_id {context = ctxt, prems = _} = |
108 unfold_thms_tac ctxt [srel_Gr, @{thm Id_alt}] THEN |
108 unfold_thms_tac ctxt [srel_Gr, @{thm Id_alt}] THEN |
109 subst_tac ctxt [map_id] 1 THEN |
109 subst_tac ctxt NONE [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 |