src/HOL/HOLCF/IOA/Sequence.thy

   THEN pair_tac ctxt "a" (i+3)
   THEN (REPEAT_DETERM (CHANGED (simp_tac ctxt (i+1))))
   THEN simp_tac (ctxt addsimps rws) i;
 \<close>
 
+lemma Mapnil: "Map f $ s = nil \<longleftrightarrow> s = nil"
+  by (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
+
+lemma MapUU: "Map f $ s = UU \<longleftrightarrow> s = UU"
+  by (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
+
+lemma MapTL: "Map f $ (TL $ s) = TL $ (Map f $ s)"
+  by (tactic \<open>Seq_induct_tac @{context} "s" [] 1\<close>)
+
 end