equal
deleted
inserted
replaced
135 "rel_sp\<^sub>\<mu> R1 R2 (map_sp\<^sub>\<mu> f1 f2 sp) (map_sp\<^sub>\<mu> g1 g2 sp') = |
135 "rel_sp\<^sub>\<mu> R1 R2 (map_sp\<^sub>\<mu> f1 f2 sp) (map_sp\<^sub>\<mu> g1 g2 sp') = |
136 rel_sp\<^sub>\<mu> (BNF_Def.vimage2p f1 g1 R1) (BNF_Def.vimage2p f2 g2 R2) sp sp'" |
136 rel_sp\<^sub>\<mu> (BNF_Def.vimage2p f1 g1 R1) (BNF_Def.vimage2p f2 g2 R2) sp sp'" |
137 by (tactic \<open> |
137 by (tactic \<open> |
138 let |
138 let |
139 val ks = 1 upto 2; |
139 val ks = 1 upto 2; |
140 val ctxt = @{context}; |
140 val ctxt = \<^context>; |
141 in |
141 in |
142 BNF_Tactics.unfold_thms_tac ctxt |
142 BNF_Tactics.unfold_thms_tac ctxt |
143 @{thms sp\<^sub>\<mu>.rel_compp sp\<^sub>\<mu>.rel_conversep sp\<^sub>\<mu>.rel_Grp vimage2p_Grp} THEN |
143 @{thms sp\<^sub>\<mu>.rel_compp sp\<^sub>\<mu>.rel_conversep sp\<^sub>\<mu>.rel_Grp vimage2p_Grp} THEN |
144 HEADGOAL (EVERY' [resolve_tac ctxt [iffI], |
144 HEADGOAL (EVERY' [resolve_tac ctxt [iffI], |
145 resolve_tac ctxt @{thms relcomppI}, |
145 resolve_tac ctxt @{thms relcomppI}, |