diff --git a/thys/HOLCF-Prelude/Data_Integer.thy b/thys/HOLCF-Prelude/Data_Integer.thy
--- a/thys/HOLCF-Prelude/Data_Integer.thy
+++ b/thys/HOLCF-Prelude/Data_Integer.thy
@@ -1,341 +1,343 @@
 section \<open>Data: Integers\<close>
 
 theory Data_Integer
   imports
     Numeral_Cpo
     Data_Bool
 begin
 
 domain Integer = MkI (lazy int)
 
 instance Integer :: flat
 proof
   fix x y :: Integer
   assume "x \<sqsubseteq> y" then show "x = \<bottom> \<or> x = y"
     by (cases x; cases y) simp_all
 qed
 
 instantiation Integer :: "{plus,times,minus,uminus,zero,one}"
 begin
 
 definition "0 = MkI\<cdot>0"
 definition "1 = MkI\<cdot>1"
 definition "a + b = (\<Lambda> (MkI\<cdot>x) (MkI\<cdot>y). MkI\<cdot>(x + y))\<cdot>a\<cdot>b"
 definition "a - b = (\<Lambda> (MkI\<cdot>x) (MkI\<cdot>y). MkI\<cdot>(x - y))\<cdot>a\<cdot>b"
 definition "a * b = (\<Lambda> (MkI\<cdot>x) (MkI\<cdot>y). MkI\<cdot>(x * y))\<cdot>a\<cdot>b"
 definition "- a = (\<Lambda> (MkI\<cdot>x). MkI\<cdot>(uminus x))\<cdot>a"
 
 instance ..
 
 end
 
 lemma Integer_arith_strict [simp]:
   fixes x :: Integer
   shows "\<bottom> + x = \<bottom>" and "x + \<bottom> = \<bottom>"
     and "\<bottom> * x = \<bottom>" and "x * \<bottom> = \<bottom>"
     and "\<bottom> - x = \<bottom>" and "x - \<bottom> = \<bottom>"
     and "- \<bottom> = (\<bottom>::Integer)"
   unfolding plus_Integer_def times_Integer_def
   unfolding minus_Integer_def uminus_Integer_def
   by (cases x, simp, simp)+
 
 lemma Integer_arith_simps [simp]:
   "MkI\<cdot>a + MkI\<cdot>b = MkI\<cdot>(a + b)"
   "MkI\<cdot>a * MkI\<cdot>b = MkI\<cdot>(a * b)"
   "MkI\<cdot>a - MkI\<cdot>b = MkI\<cdot>(a - b)"
   "- MkI\<cdot>a = MkI\<cdot>(uminus a)"
   unfolding plus_Integer_def times_Integer_def
   unfolding minus_Integer_def uminus_Integer_def
   by simp_all
 
 lemma plus_MkI_MkI:
   "MkI\<cdot>x + MkI\<cdot>y = MkI\<cdot>(x + y)"
   unfolding plus_Integer_def by simp
 
 instance Integer :: "{plus_cpo,minus_cpo,times_cpo}"
   by standard (simp_all add: flatdom_strict2cont)
 
 instance Integer :: comm_monoid_add
 proof
   fix a b c :: Integer
   show "(a + b) + c = a + (b + c)"
     by (cases a; cases b; cases c) simp_all
   show "a + b = b + a"
     by (cases a; cases b) simp_all
   show "0 + a = a"
     unfolding zero_Integer_def
     by (cases a) simp_all
 qed
 
 instance Integer :: comm_monoid_mult
 proof
   fix a b c :: Integer
   show "(a * b) * c = a * (b * c)"
     by (cases a; cases b; cases c) simp_all
   show "a * b = b * a"
     by (cases a; cases b) simp_all
   show "1 * a = a"
     unfolding one_Integer_def
     by (cases a) simp_all
 qed
 
 instance Integer :: comm_semiring
 proof
   fix a b c :: Integer
   show "(a + b) * c = a * c + b * c"
     by (cases a; cases b; cases c) (simp_all add: distrib_right)
 qed
 
 instance Integer :: semiring_numeral ..
 
 lemma Integer_add_diff_cancel [simp]:
   "b \<noteq> \<bottom> \<Longrightarrow> (a::Integer) + b - b = a"
   by (cases a; cases b) simp_all
 
 lemma zero_Integer_neq_bottom [simp]: "(0::Integer) \<noteq> \<bottom>"
   by (simp add: zero_Integer_def)
 
 lemma one_Integer_neq_bottom [simp]: "(1::Integer) \<noteq> \<bottom>"
   by (simp add: one_Integer_def)
 
 lemma plus_Integer_eq_bottom_iff [simp]:
   fixes x y :: Integer shows "x + y = \<bottom> \<longleftrightarrow> x = \<bottom> \<or> y = \<bottom>"
   by (cases x, simp, cases y, simp, simp)
 
 lemma diff_Integer_eq_bottom_iff [simp]:
   fixes x y :: Integer shows "x - y = \<bottom> \<longleftrightarrow> x = \<bottom> \<or> y = \<bottom>"
   by (cases x, simp, cases y, simp, simp)
 
 lemma mult_Integer_eq_bottom_iff [simp]:
   fixes x y :: Integer shows "x * y = \<bottom> \<longleftrightarrow> x = \<bottom> \<or> y = \<bottom>"
   by (cases x, simp, cases y, simp, simp)
 
 lemma minus_Integer_eq_bottom_iff [simp]:
   fixes x :: Integer shows "- x = \<bottom> \<longleftrightarrow> x = \<bottom>"
   by (cases x, simp, simp)
 
 lemma numeral_Integer_eq: "numeral k = MkI\<cdot>(numeral k)"
   by (induct k, simp_all only: numeral.simps one_Integer_def plus_MkI_MkI)
 
 lemma numeral_Integer_neq_bottom [simp]: "(numeral k::Integer) \<noteq> \<bottom>"
   unfolding numeral_Integer_eq by simp
 
 text \<open>Symmetric versions are also needed, because the reorient
   simproc does not apply to these comparisons.\<close>
 
 lemma bottom_neq_zero_Integer [simp]: "(\<bottom>::Integer) \<noteq> 0"
   by (simp add: zero_Integer_def)
 
 lemma bottom_neq_one_Integer [simp]: "(\<bottom>::Integer) \<noteq> 1"
   by (simp add: one_Integer_def)
 
 lemma bottom_neq_numeral_Integer [simp]: "(\<bottom>::Integer) \<noteq> numeral k"
   unfolding numeral_Integer_eq by simp
 
 instantiation Integer :: Ord_linear
 begin
 
 definition
   "eq = (\<Lambda> (MkI\<cdot>x) (MkI\<cdot>y). if x = y then TT else FF)"
 
 definition
   "compare = (\<Lambda> (MkI\<cdot>x) (MkI\<cdot>y).
     if x < y then LT else if x > y then GT else EQ)"
 
 instance proof
   fix x y z :: Integer
   show "compare\<cdot>\<bottom>\<cdot>y = \<bottom>"
     unfolding compare_Integer_def by simp
   show "compare\<cdot>x\<cdot>\<bottom> = \<bottom>"
     unfolding compare_Integer_def by (cases x, simp_all)
   show "oppOrdering\<cdot>(compare\<cdot>x\<cdot>y) = compare\<cdot>y\<cdot>x"
     unfolding compare_Integer_def
     by (cases x, cases y, simp, simp,
         cases y, simp, simp add: not_less less_imp_le)
-  { assume "compare\<cdot>x\<cdot>y = EQ" then show "x = y"
-      unfolding compare_Integer_def
-      by (cases x, cases y, simp, simp,
-          cases y, simp, simp split: if_splits) }
-  { assume "compare\<cdot>x\<cdot>y = LT" and "compare\<cdot>y\<cdot>z = LT" then show "compare\<cdot>x\<cdot>z = LT"
-      unfolding compare_Integer_def
-      by (cases x, simp, cases y, simp, cases z, simp,
-          auto split: if_splits) }
+  show "x = y" if "compare\<cdot>x\<cdot>y = EQ"
+    using that
+    unfolding compare_Integer_def
+    by (cases x, cases y, simp, simp,
+        cases y, simp, simp split: if_splits)
+  show "compare\<cdot>x\<cdot>z = LT" if "compare\<cdot>x\<cdot>y = LT" and "compare\<cdot>y\<cdot>z = LT"
+    using that
+    unfolding compare_Integer_def
+    by (cases x, simp, cases y, simp, cases z, simp,
+        auto split: if_splits)
   show "eq\<cdot>x\<cdot>y = is_EQ\<cdot>(compare\<cdot>x\<cdot>y)"
     unfolding eq_Integer_def compare_Integer_def
     by (cases x, simp, cases y, simp, auto)
   show "compare\<cdot>x\<cdot>x \<sqsubseteq> EQ"
     unfolding compare_Integer_def
     by (cases x, simp_all)
 qed
 
 end
 
 lemma eq_MkI_MkI [simp]:
   "eq\<cdot>(MkI\<cdot>m)\<cdot>(MkI\<cdot>n) = (if m = n then TT else FF)"
   by (simp add: eq_Integer_def)
 
 lemma compare_MkI_MkI [simp]:
   "compare\<cdot>(MkI\<cdot>x)\<cdot>(MkI\<cdot>y) = (if x < y then LT else if x > y then GT else EQ)"
   unfolding compare_Integer_def by simp
 
 lemma lt_MkI_MkI [simp]:
   "lt\<cdot>(MkI\<cdot>x)\<cdot>(MkI\<cdot>y) = (if x < y then TT else FF)"
   unfolding lt_def by simp
 
 lemma le_MkI_MkI [simp]:
   "le\<cdot>(MkI\<cdot>x)\<cdot>(MkI\<cdot>y) = (if x \<le> y then TT else FF)"
   unfolding le_def by simp
 
 lemma eq_Integer_bottom_iff [simp]:
   fixes x y :: Integer shows "eq\<cdot>x\<cdot>y = \<bottom> \<longleftrightarrow> x = \<bottom> \<or> y = \<bottom>"
   by (cases x, simp, cases y, simp, simp)
 
 lemma compare_Integer_bottom_iff [simp]:
   fixes x y :: Integer shows "compare\<cdot>x\<cdot>y = \<bottom> \<longleftrightarrow> x = \<bottom> \<or> y = \<bottom>"
   by (cases x, simp, cases y, simp, simp)
 
 lemma lt_Integer_bottom_iff [simp]:
   fixes x y :: Integer shows "lt\<cdot>x\<cdot>y = \<bottom> \<longleftrightarrow> x = \<bottom> \<or> y = \<bottom>"
   by (cases x, simp, cases y, simp, simp)
 
 lemma le_Integer_bottom_iff [simp]:
   fixes x y :: Integer shows "le\<cdot>x\<cdot>y = \<bottom> \<longleftrightarrow> x = \<bottom> \<or> y = \<bottom>"
   by (cases x, simp, cases y, simp, simp)
 
 lemma compare_refl_Integer [simp]:
   "(x::Integer) \<noteq> \<bottom> \<Longrightarrow> compare\<cdot>x\<cdot>x = EQ"
   by (cases x) simp_all
 
 lemma eq_refl_Integer [simp]:
   "(x::Integer) \<noteq> \<bottom> \<Longrightarrow> eq\<cdot>x\<cdot>x = TT"
   by (cases x) simp_all
 
 lemma lt_refl_Integer [simp]:
   "(x::Integer) \<noteq> \<bottom> \<Longrightarrow> lt\<cdot>x\<cdot>x = FF"
   by (cases x) simp_all
 
 lemma le_refl_Integer [simp]:
   "(x::Integer) \<noteq> \<bottom> \<Longrightarrow> le\<cdot>x\<cdot>x = TT"
   by (cases x) simp_all
 
 lemma eq_Integer_numeral_simps [simp]:
   "eq\<cdot>(0::Integer)\<cdot>0 = TT"
   "eq\<cdot>(0::Integer)\<cdot>1 = FF"
   "eq\<cdot>(1::Integer)\<cdot>0 = FF"
   "eq\<cdot>(1::Integer)\<cdot>1 = TT"
   "eq\<cdot>(0::Integer)\<cdot>(numeral k) = FF"
   "eq\<cdot>(numeral k)\<cdot>(0::Integer) = FF"
   "k \<noteq> Num.One \<Longrightarrow> eq\<cdot>(1::Integer)\<cdot>(numeral k) = FF"
   "k \<noteq> Num.One \<Longrightarrow> eq\<cdot>(numeral k)\<cdot>(1::Integer) = FF"
   "eq\<cdot>(numeral k::Integer)\<cdot>(numeral l) = (if k = l then TT else FF)"
   unfolding zero_Integer_def one_Integer_def numeral_Integer_eq
   by simp_all
 
 lemma compare_Integer_numeral_simps [simp]:
   "compare\<cdot>(0::Integer)\<cdot>0 = EQ"
   "compare\<cdot>(0::Integer)\<cdot>1 = LT"
   "compare\<cdot>(1::Integer)\<cdot>0 = GT"
   "compare\<cdot>(1::Integer)\<cdot>1 = EQ"
   "compare\<cdot>(0::Integer)\<cdot>(numeral k) = LT"
   "compare\<cdot>(numeral k)\<cdot>(0::Integer) = GT"
   "Num.One < k \<Longrightarrow> compare\<cdot>(1::Integer)\<cdot>(numeral k) = LT"
   "Num.One < k \<Longrightarrow> compare\<cdot>(numeral k)\<cdot>(1::Integer) = GT"
   "compare\<cdot>(numeral k::Integer)\<cdot>(numeral l) =
     (if k < l then LT else if k > l then GT else EQ)"
   unfolding zero_Integer_def one_Integer_def numeral_Integer_eq
   by simp_all
 
 lemma lt_Integer_numeral_simps [simp]:
   "lt\<cdot>(0::Integer)\<cdot>0 = FF"
   "lt\<cdot>(0::Integer)\<cdot>1 = TT"
   "lt\<cdot>(1::Integer)\<cdot>0 = FF"
   "lt\<cdot>(1::Integer)\<cdot>1 = FF"
   "lt\<cdot>(0::Integer)\<cdot>(numeral k) = TT"
   "lt\<cdot>(numeral k)\<cdot>(0::Integer) = FF"
   "Num.One < k \<Longrightarrow> lt\<cdot>(1::Integer)\<cdot>(numeral k) = TT"
   "lt\<cdot>(numeral k)\<cdot>(1::Integer) = FF"
   "lt\<cdot>(numeral k::Integer)\<cdot>(numeral l) = (if k < l then TT else FF)"
   unfolding zero_Integer_def one_Integer_def numeral_Integer_eq
   by simp_all
 
 lemma le_Integer_numeral_simps [simp]:
   "le\<cdot>(0::Integer)\<cdot>0 = TT"
   "le\<cdot>(0::Integer)\<cdot>1 = TT"
   "le\<cdot>(1::Integer)\<cdot>0 = FF"
   "le\<cdot>(1::Integer)\<cdot>1 = TT"
   "le\<cdot>(0::Integer)\<cdot>(numeral k) = TT"
   "le\<cdot>(numeral k)\<cdot>(0::Integer) = FF"
   "le\<cdot>(1::Integer)\<cdot>(numeral k) = TT"
   "Num.One < k \<Longrightarrow> le\<cdot>(numeral k)\<cdot>(1::Integer) = FF"
   "le\<cdot>(numeral k::Integer)\<cdot>(numeral l) = (if k \<le> l then TT else FF)"
   unfolding zero_Integer_def one_Integer_def numeral_Integer_eq
   by simp_all
 
 lemma MkI_eq_0_iff [simp]: "MkI\<cdot>n = 0 \<longleftrightarrow> n = 0"
   unfolding zero_Integer_def by simp
 
 lemma MkI_eq_1_iff [simp]: "MkI\<cdot>n = 1 \<longleftrightarrow> n = 1"
   unfolding one_Integer_def by simp
 
 lemma MkI_eq_numeral_iff [simp]: "MkI\<cdot>n = numeral k \<longleftrightarrow> n = numeral k"
   unfolding numeral_Integer_eq by simp
 
 lemma MkI_0: "MkI\<cdot>0 = 0"
   by simp
 
 lemma MkI_1: "MkI\<cdot>1 = 1"
   by simp
 
 lemma le_plus_1:
   fixes m :: "Integer"
   assumes "le\<cdot>m\<cdot>n = TT"
   shows "le\<cdot>m\<cdot>(n + 1) = TT"
 proof -
   from assms have "n \<noteq> \<bottom>" by auto
   then have "le\<cdot>n\<cdot>(n + 1) = TT"
     by (cases n) (auto, metis le_MkI_MkI less_add_one less_le_not_le one_Integer_def plus_MkI_MkI)
   with assms show ?thesis by (auto dest: le_trans)
 qed
 
 subsection \<open>Induction rules that do not break the abstraction\<close>
 
 lemma nonneg_Integer_induct [consumes 1, case_names 0 step]:
   fixes i :: Integer
   assumes i_nonneg: "le\<cdot>0\<cdot>i = TT"
     and zero: "P 0"
     and step: "\<And>i. le\<cdot>1\<cdot>i = TT \<Longrightarrow> P (i - 1) \<Longrightarrow> P i"
   shows "P i"
 proof (cases i)
   case bottom
   then have False using i_nonneg by simp
   then show ?thesis ..
 next
   case (MkI integer)
   show ?thesis
   proof (cases integer)
     case neg
     then have False using i_nonneg MkI by (auto simp add: zero_Integer_def one_Integer_def)
     then show ?thesis ..
   next
     case (nonneg nat)
     have "P (MkI\<cdot>(int nat))"
     proof(induct nat)
       case 0
       show ?case using zero by (simp add: zero_Integer_def)
     next
       case (Suc nat)
       have "le\<cdot>1\<cdot>(MkI\<cdot>(int (Suc nat))) = TT"
         by (simp add: one_Integer_def)
       moreover
       have "P (MkI\<cdot>(int (Suc nat)) - 1)"
         using Suc
         by (simp add: one_Integer_def)
       ultimately
       show ?case
         by (rule step)
     qed
     then show ?thesis using nonneg MkI by simp
   qed
 qed
 
 end
diff --git a/thys/HOLCF-Prelude/Data_List.thy b/thys/HOLCF-Prelude/Data_List.thy
--- a/thys/HOLCF-Prelude/Data_List.thy
+++ b/thys/HOLCF-Prelude/Data_List.thy
@@ -1,1625 +1,1621 @@
 section \<open>Data: List\<close>
 
 theory Data_List
   imports
     Type_Classes
     Data_Function
     Data_Bool
     Data_Tuple
     Data_Integer
     Numeral_Cpo
 begin
 
 no_notation (ASCII)
   Set.member  ("'(:')") and
   Set.member  ("(_/ : _)" [51, 51] 50)
 
 subsection \<open>Datatype definition\<close>
 
 domain 'a list ("[_]") =
   Nil ("[]") |
   Cons (lazy head :: 'a) (lazy tail :: "['a]") (infixr ":" 65)
 (*FIXME: We need to standardize a mapping from Haskell fixities
 (0 to 9) to Isabelle ones (between 50 and 100).*)
 
 
 subsubsection \<open>Section syntax for @{const Cons}\<close>
 
 syntax
   "_Cons_section" :: "'a \<rightarrow> ['a] \<rightarrow> ['a]" ("'(:')")
   "_Cons_section_left" :: "'a \<Rightarrow> ['a] \<rightarrow> ['a]" ("'(_:')")
 translations
   "(x:)" == "(CONST Rep_cfun) (CONST Cons) x"
 
 abbreviation Cons_section_right :: "['a] \<Rightarrow> 'a \<rightarrow> ['a]" ("'(:_')") where
   "(:xs) \<equiv> \<Lambda> x. x:xs"
 
 syntax
   "_lazy_list" :: "args \<Rightarrow> ['a]" ("[(_)]")
 translations
   "[x, xs]" == "x : [xs]"
   "[x]" == "x : []"
 
 abbreviation null :: "['a] \<rightarrow> tr" where "null \<equiv> is_Nil"
 
 
 subsection \<open>Haskell function definitions\<close>
 
 instantiation list :: (Eq) Eq_strict
 begin
 
 fixrec eq_list :: "['a] \<rightarrow> ['a] \<rightarrow> tr" where
   "eq_list\<cdot>[]\<cdot>[] = TT" |
   "eq_list\<cdot>(x : xs)\<cdot>[] = FF" |
   "eq_list\<cdot>[]\<cdot>(y : ys) = FF" |
   "eq_list\<cdot>(x : xs)\<cdot>(y : ys) = (eq\<cdot>x\<cdot>y andalso eq_list\<cdot>xs\<cdot>ys)"
 
 instance proof
   fix xs :: "['a]"
   show "eq\<cdot>xs\<cdot>\<bottom> = \<bottom>"
     by (cases xs, fixrec_simp+)
   show "eq\<cdot>\<bottom>\<cdot>xs = \<bottom>"
     by fixrec_simp
 qed
 
 end
 
 instance list :: (Eq_sym) Eq_sym
 proof
   fix xs ys :: "['a]"
   show "eq\<cdot>xs\<cdot>ys = eq\<cdot>ys\<cdot>xs"
   proof (induct xs arbitrary: ys)
     case Nil
     show ?case by (cases ys; simp)
   next
     case Cons
     then show ?case by (cases ys; simp add: eq_sym)
   qed simp_all
 qed
 
 instance list :: (Eq_equiv) Eq_equiv
 proof
   fix xs ys zs :: "['a]"
   show "eq\<cdot>xs\<cdot>xs \<noteq> FF"
     by (induct xs, simp_all)
   assume "eq\<cdot>xs\<cdot>ys = TT" and "eq\<cdot>ys\<cdot>zs = TT" then show "eq\<cdot>xs\<cdot>zs = TT"
   proof (induct xs arbitrary: ys zs)
     case (Nil ys zs) then show ?case by (cases ys, simp_all)
   next
     case (Cons x xs ys zs)
     from Cons.prems show ?case
       by (cases ys; cases zs) (auto intro: eq_trans Cons.hyps)
   qed simp_all
 qed
 
 instance list :: (Eq_eq) Eq_eq
 proof
   fix xs ys :: "['a]"
   show "eq\<cdot>xs\<cdot>xs \<noteq> FF"
     by (induct xs) simp_all
   assume "eq\<cdot>xs\<cdot>ys = TT" then show "xs = ys"
   proof (induct xs arbitrary: ys)
     case Nil
     then show ?case by (cases ys) auto
   next
     case Cons
     then show ?case by (cases ys) auto
   qed auto
 qed
 
 instantiation list :: (Ord) Ord_strict
 begin
 
 fixrec compare_list :: "['a] \<rightarrow> ['a] \<rightarrow> Ordering" where
   "compare_list\<cdot>[]\<cdot>[] = EQ" |
   "compare_list\<cdot>(x : xs)\<cdot>[] = GT" |
   "compare_list\<cdot>[]\<cdot>(y : ys) = LT" |
   "compare_list\<cdot>(x : xs)\<cdot>(y : ys) =
     thenOrdering\<cdot>(compare\<cdot>x\<cdot>y)\<cdot>(compare_list\<cdot>xs\<cdot>ys)"
 
 instance
   by standard (fixrec_simp, rename_tac x, case_tac x, fixrec_simp+)
 
 end
 
 instance list :: (Ord_linear) Ord_linear
 proof
   fix xs ys zs :: "['a]"
   show "oppOrdering\<cdot>(compare\<cdot>xs\<cdot>ys) = compare\<cdot>ys\<cdot>xs"
   proof (induct xs arbitrary: ys)
     case Nil
     show ?case by (cases ys; simp)
   next
     case Cons
     then show ?case by (cases ys; simp add: oppOrdering_thenOrdering)
   qed simp_all
   show "xs = ys" if "compare\<cdot>xs\<cdot>ys = EQ"
     using that
   proof (induct xs arbitrary: ys)
     case Nil
     then show ?case by (cases ys; simp)
   next
     case Cons
     then show ?case by (cases ys; auto elim: compare_EQ_dest)
   qed simp_all
   show "compare\<cdot>xs\<cdot>zs = LT" if "compare\<cdot>xs\<cdot>ys = LT" and "compare\<cdot>ys\<cdot>zs = LT"
     using that
   proof (induct xs arbitrary: ys zs)
     case Nil
     then show ?case by (cases ys; cases zs; simp)
   next
     case (Cons a xs)
     then show ?case
       by (cases ys; cases zs) (auto dest: compare_EQ_dest compare_LT_trans)
   qed simp_all
   show "eq\<cdot>xs\<cdot>ys = is_EQ\<cdot>(compare\<cdot>xs\<cdot>ys)"
   proof (induct xs arbitrary: ys)
     case Nil
     show ?case by (cases ys; simp)
   next
     case Cons
     then show ?case by (cases ys; simp add: eq_conv_compare)
   qed simp_all
   show "compare\<cdot>xs\<cdot>xs \<sqsubseteq> EQ"
     by (induct xs) simp_all
 qed
 
 fixrec zipWith :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ['a] \<rightarrow> ['b] \<rightarrow> ['c]" where
   "zipWith\<cdot>f\<cdot>(x : xs)\<cdot>(y : ys) = f\<cdot>x\<cdot>y : zipWith\<cdot>f\<cdot>xs\<cdot>ys" |
   "zipWith\<cdot>f\<cdot>(x : xs)\<cdot>[] = []" |
   "zipWith\<cdot>f\<cdot>[]\<cdot>ys = []"
 
 definition zip :: "['a] \<rightarrow> ['b] \<rightarrow> [\<langle>'a, 'b\<rangle>]" where
   "zip = zipWith\<cdot>\<langle>,\<rangle>"
 
 fixrec zipWith3 :: "('a \<rightarrow> 'b \<rightarrow> 'c \<rightarrow> 'd) \<rightarrow> ['a] \<rightarrow> ['b] \<rightarrow> ['c] \<rightarrow> ['d]" where
   "zipWith3\<cdot>f\<cdot>(x : xs)\<cdot>(y : ys)\<cdot>(z : zs) = f\<cdot>x\<cdot>y\<cdot>z : zipWith3\<cdot>f\<cdot>xs\<cdot>ys\<cdot>zs" |
   (unchecked) "zipWith3\<cdot>f\<cdot>xs\<cdot>ys\<cdot>zs = []"
 
 definition zip3 :: "['a] \<rightarrow> ['b] \<rightarrow> ['c] \<rightarrow> [\<langle>'a, 'b, 'c\<rangle>]" where
   "zip3 = zipWith3\<cdot>\<langle>,,\<rangle>"
 
 fixrec map :: "('a \<rightarrow> 'b) \<rightarrow> ['a] \<rightarrow> ['b]" where
   "map\<cdot>f\<cdot>[] = []" |
   "map\<cdot>f\<cdot>(x : xs) = f\<cdot>x : map\<cdot>f\<cdot>xs"
 
 fixrec filter :: "('a \<rightarrow> tr) \<rightarrow> ['a] \<rightarrow> ['a]" where
   "filter\<cdot>P\<cdot>[] = []" |
   "filter\<cdot>P\<cdot>(x : xs) =
     If (P\<cdot>x) then x : filter\<cdot>P\<cdot>xs else filter\<cdot>P\<cdot>xs"
 
 fixrec repeat :: "'a \<rightarrow> ['a]" where
   [simp del]: "repeat\<cdot>x = x : repeat\<cdot>x"
 
 fixrec takeWhile :: "('a \<rightarrow> tr) \<rightarrow> ['a] \<rightarrow> ['a]" where
  "takeWhile\<cdot>p\<cdot>[]     =  []" |
  "takeWhile\<cdot>p\<cdot>(x:xs) = If p\<cdot>x then x : takeWhile\<cdot>p\<cdot>xs else  []"
 
 fixrec dropWhile :: "('a \<rightarrow> tr) \<rightarrow> ['a] \<rightarrow> ['a]" where
  "dropWhile\<cdot>p\<cdot>[]     =  []" |
  "dropWhile\<cdot>p\<cdot>(x:xs) = If p\<cdot>x then dropWhile\<cdot>p\<cdot>xs else (x:xs)"
 
 fixrec span :: "('a -> tr) -> ['a] -> \<langle>['a],['a]\<rangle>" where
  "span\<cdot>p\<cdot>[]     = \<langle>[],[]\<rangle>" |
  "span\<cdot>p\<cdot>(x:xs) = If p\<cdot>x then (case span\<cdot>p\<cdot>xs of \<langle>ys, zs\<rangle> \<Rightarrow> \<langle>x:ys,zs\<rangle>) else \<langle>[], x:xs\<rangle>"
 
 fixrec break :: "('a -> tr) -> ['a] -> \<langle>['a],['a]\<rangle>" where
  "break\<cdot>p = span\<cdot>(neg oo p)"
 
 fixrec nth :: "['a] \<rightarrow> Integer \<rightarrow> 'a" where
   "nth\<cdot>[]\<cdot>n = \<bottom>" |
   nth_Cons [simp del]:
   "nth\<cdot>(x : xs)\<cdot>n = If eq\<cdot>n\<cdot>0 then x else nth\<cdot>xs\<cdot>(n - 1)"
 (* bh: Perhaps we should rename this to 'index',
 to match the standard Haskell function named 'genericIndex'. *)
 
 abbreviation nth_syn :: "['a] \<Rightarrow> Integer \<Rightarrow> 'a" (infixl "!!" 100) where
   "xs !! n \<equiv> nth\<cdot>xs\<cdot>n"
 
 definition partition :: "('a \<rightarrow> tr) \<rightarrow> ['a] \<rightarrow> \<langle>['a], ['a]\<rangle>" where
   "partition = (\<Lambda> P xs. \<langle>filter\<cdot>P\<cdot>xs, filter\<cdot>(neg oo P)\<cdot>xs\<rangle>)"
 
 fixrec iterate :: "('a \<rightarrow> 'a) \<rightarrow> 'a \<rightarrow> ['a]" where
   "iterate\<cdot>f\<cdot>x = x : iterate\<cdot>f\<cdot>(f\<cdot>x)"
 
 fixrec foldl ::  "('a -> 'b -> 'a) -> 'a -> ['b] -> 'a" where
   "foldl\<cdot>f\<cdot>z\<cdot>[]     = z" |
   "foldl\<cdot>f\<cdot>z\<cdot>(x:xs) = foldl\<cdot>f\<cdot>(f\<cdot>z\<cdot>x)\<cdot>xs"
 
 fixrec foldl1 ::  "('a -> 'a -> 'a) -> ['a] -> 'a" where
   "foldl1\<cdot>f\<cdot>[]     = \<bottom>" |
   "foldl1\<cdot>f\<cdot>(x:xs) = foldl\<cdot>f\<cdot>x\<cdot>xs"
 
 fixrec foldr :: "('a \<rightarrow> 'b \<rightarrow> 'b) \<rightarrow> 'b \<rightarrow> ['a] \<rightarrow> 'b" where
   "foldr\<cdot>f\<cdot>d\<cdot>[] = d" |
   "foldr\<cdot>f\<cdot>d\<cdot>(x : xs) = f\<cdot>x\<cdot>(foldr\<cdot>f\<cdot>d\<cdot>xs)"
 
 fixrec foldr1 :: "('a \<rightarrow> 'a \<rightarrow> 'a) \<rightarrow> ['a] \<rightarrow> 'a" where
   "foldr1\<cdot>f\<cdot>[] = \<bottom>" |
   "foldr1\<cdot>f\<cdot>[x] = x" |
   "foldr1\<cdot>f\<cdot>(x : (x':xs)) = f\<cdot>x\<cdot>(foldr1\<cdot>f\<cdot>(x':xs))"
 
 fixrec elem :: "'a::Eq \<rightarrow> ['a] \<rightarrow> tr" where
   "elem\<cdot>x\<cdot>[] = FF" |
   "elem\<cdot>x\<cdot>(y : ys) = (eq\<cdot>y\<cdot>x orelse elem\<cdot>x\<cdot>ys)"
 
 fixrec notElem :: "'a::Eq \<rightarrow> ['a] \<rightarrow> tr" where
   "notElem\<cdot>x\<cdot>[] = TT" |
   "notElem\<cdot>x\<cdot>(y : ys) = (neq\<cdot>y\<cdot>x andalso notElem\<cdot>x\<cdot>ys)"
 
 fixrec append :: "['a] \<rightarrow> ['a] \<rightarrow> ['a]" where
   "append\<cdot>[]\<cdot>ys = ys" |
   "append\<cdot>(x : xs)\<cdot>ys = x : append\<cdot>xs\<cdot>ys"
 
 abbreviation append_syn :: "['a] \<Rightarrow> ['a] \<Rightarrow> ['a]" (infixr "++" 65) where
   "xs ++ ys \<equiv> append\<cdot>xs\<cdot>ys"
 
 definition concat :: "[['a]] \<rightarrow> ['a]" where
   "concat = foldr\<cdot>append\<cdot>[]"
 
 definition concatMap :: "('a \<rightarrow> ['b]) \<rightarrow> ['a] \<rightarrow> ['b]" where
   "concatMap = (\<Lambda> f. concat oo map\<cdot>f)"
 
 fixrec last :: "['a] -> 'a" where
   "last\<cdot>[x] = x" |
   "last\<cdot>(_:(x:xs)) = last\<cdot>(x:xs)"
 
 fixrec init :: "['a] -> ['a]" where
   "init\<cdot>[x] = []" |
   "init\<cdot>(x:(y:xs)) = x:(init\<cdot>(y:xs))"
 
 fixrec reverse :: "['a] -> ['a]" where
   [simp del]:"reverse = foldl\<cdot>(flip\<cdot>(:))\<cdot>[]"
 
 fixrec the_and :: "[tr] \<rightarrow> tr" where
   "the_and = foldr\<cdot>trand\<cdot>TT"
 
 fixrec the_or :: "[tr] \<rightarrow> tr" where
   "the_or = foldr\<cdot>tror\<cdot>FF"
 
 fixrec all :: "('a \<rightarrow> tr) \<rightarrow> ['a] \<rightarrow> tr" where
   "all\<cdot>P = the_and oo (map\<cdot>P)"
 
 fixrec any :: "('a \<rightarrow> tr) \<rightarrow> ['a] \<rightarrow> tr" where
   "any\<cdot>P = the_or oo (map\<cdot>P)"
 
 fixrec tails :: "['a] \<rightarrow> [['a]]" where
   "tails\<cdot>[] = [[]]" |
   "tails\<cdot>(x : xs) = (x : xs) : tails\<cdot>xs"
 
 fixrec inits :: "['a] \<rightarrow> [['a]]" where
   "inits\<cdot>[] = [[]]" |
   "inits\<cdot>(x : xs) = [[]] ++ map\<cdot>(x:)\<cdot>(inits\<cdot>xs)"
 
 fixrec scanr :: "('a \<rightarrow> 'b \<rightarrow> 'b) \<rightarrow> 'b \<rightarrow> ['a] \<rightarrow> ['b]"
 where
   "scanr\<cdot>f\<cdot>q0\<cdot>[] = [q0]" |
   "scanr\<cdot>f\<cdot>q0\<cdot>(x : xs) = (
     let qs = scanr\<cdot>f\<cdot>q0\<cdot>xs in
     (case qs of
       [] \<Rightarrow> \<bottom>
     | q : qs' \<Rightarrow> f\<cdot>x\<cdot>q : qs))"
 
 fixrec scanr1 :: "('a \<rightarrow> 'a \<rightarrow> 'a) \<rightarrow> ['a] \<rightarrow> ['a]"
 where
   "scanr1\<cdot>f\<cdot>[] = []" |
   "scanr1\<cdot>f\<cdot>(x : xs) =
     (case xs of
       [] \<Rightarrow> [x]
     | x' : xs' \<Rightarrow> (
       let qs = scanr1\<cdot>f\<cdot>xs in
       (case qs of
         [] \<Rightarrow> \<bottom>
       | q : qs' \<Rightarrow> f\<cdot>x\<cdot>q : qs)))"
 
 fixrec scanl :: "('a \<rightarrow> 'b \<rightarrow> 'a) \<rightarrow> 'a \<rightarrow> ['b] \<rightarrow> ['a]" where
   "scanl\<cdot>f\<cdot>q\<cdot>ls = q : (case ls of
     [] \<Rightarrow> []
   | x : xs \<Rightarrow> scanl\<cdot>f\<cdot>(f\<cdot>q\<cdot>x)\<cdot>xs)"
 
 definition scanl1 :: "('a \<rightarrow> 'a \<rightarrow> 'a) \<rightarrow> ['a] \<rightarrow> ['a]" where
   "scanl1 = (\<Lambda> f ls. (case ls of
     [] \<Rightarrow> []
   | x : xs \<Rightarrow> scanl\<cdot>f\<cdot>x\<cdot>xs))"
 
 subsubsection \<open>Arithmetic Sequences\<close>
 
 fixrec upto :: "Integer \<rightarrow> Integer \<rightarrow> [Integer]" where
   [simp del]: "upto\<cdot>x\<cdot>y = If le\<cdot>x\<cdot>y then x : upto\<cdot>(x+1)\<cdot>y else []"
 
 fixrec intsFrom :: "Integer \<rightarrow> [Integer]" where
   [simp del]: "intsFrom\<cdot>x = seq\<cdot>x\<cdot>(x : intsFrom\<cdot>(x+1))"
 
 class Enum =
   fixes toEnum :: "Integer \<rightarrow> 'a"
     and fromEnum :: "'a \<rightarrow> Integer"
 begin
 
 definition succ :: "'a \<rightarrow> 'a" where
   "succ = toEnum oo (+1) oo fromEnum"
 
 definition pred :: "'a \<rightarrow> 'a" where
   "pred = toEnum oo (-1) oo fromEnum"
 
 definition enumFrom :: "'a \<rightarrow> ['a]" where
   "enumFrom = (\<Lambda> x. map\<cdot>toEnum\<cdot>(intsFrom\<cdot>(fromEnum\<cdot>x)))"
 
 definition enumFromTo :: "'a \<rightarrow> 'a \<rightarrow> ['a]" where
   "enumFromTo = (\<Lambda> x y. map\<cdot>toEnum\<cdot>(upto\<cdot>(fromEnum\<cdot>x)\<cdot>(fromEnum\<cdot>y)))"
 
 end
 
 abbreviation enumFrom_To_syn :: "'a::Enum \<Rightarrow> 'a \<Rightarrow> ['a]" ("(1[_../_])") where
   "[m..n] \<equiv> enumFromTo\<cdot>m\<cdot>n"
 
 abbreviation enumFrom_syn :: "'a::Enum \<Rightarrow> ['a]" ("(1[_..])") where
   "[n..] \<equiv> enumFrom\<cdot>n"
 
 instantiation Integer :: Enum
 begin
 definition [simp]: "toEnum = ID"
 definition [simp]: "fromEnum = ID"
 instance ..
 end
 
 fixrec take :: "Integer \<rightarrow> ['a] \<rightarrow> ['a]" where
   [simp del]: "take\<cdot>n\<cdot>xs = If le\<cdot>n\<cdot>0 then [] else
     (case xs of [] \<Rightarrow> [] | y : ys \<Rightarrow> y : take\<cdot>(n - 1)\<cdot>ys)"
 
 fixrec drop :: "Integer \<rightarrow> ['a] \<rightarrow> ['a]" where
   [simp del]: "drop\<cdot>n\<cdot>xs = If le\<cdot>n\<cdot>0 then xs else
     (case xs of [] \<Rightarrow> [] | y : ys \<Rightarrow> drop\<cdot>(n - 1)\<cdot>ys)"
 
 fixrec isPrefixOf :: "['a::Eq] \<rightarrow> ['a] \<rightarrow> tr" where
   "isPrefixOf\<cdot>[]\<cdot>_ = TT" |
   "isPrefixOf\<cdot>(x:xs)\<cdot>[] = FF" |
   "isPrefixOf\<cdot>(x:xs)\<cdot>(y:ys) = (eq\<cdot>x\<cdot>y andalso isPrefixOf\<cdot>xs\<cdot>ys)"
 
 fixrec isSuffixOf :: "['a::Eq] \<rightarrow> ['a] \<rightarrow> tr" where
   "isSuffixOf\<cdot>x\<cdot>y = isPrefixOf\<cdot>(reverse\<cdot>x)\<cdot>(reverse\<cdot>y)"
 
 fixrec intersperse :: "'a \<rightarrow> ['a] \<rightarrow> ['a]" where
   "intersperse\<cdot>sep\<cdot>[] = []" |
   "intersperse\<cdot>sep\<cdot>[x] = [x]" |
   "intersperse\<cdot>sep\<cdot>(x:y:xs) = x:sep:intersperse\<cdot>sep\<cdot>(y:xs)"
 
 fixrec intercalate :: "['a] \<rightarrow> [['a]] \<rightarrow> ['a]" where
   "intercalate\<cdot>xs\<cdot>xss = concat\<cdot>(intersperse\<cdot>xs\<cdot>xss)"
 
 definition replicate :: "Integer \<rightarrow> 'a \<rightarrow> ['a]" where
   "replicate = (\<Lambda> n x. take\<cdot>n\<cdot>(repeat\<cdot>x))"
 
 definition findIndices :: "('a \<rightarrow> tr) \<rightarrow> ['a] \<rightarrow> [Integer]" where
   "findIndices = (\<Lambda> P xs.
     map\<cdot>snd\<cdot>(filter\<cdot>(\<Lambda> \<langle>x, i\<rangle>. P\<cdot>x)\<cdot>(zip\<cdot>xs\<cdot>[0..])))"
 
 fixrec length :: "['a] \<rightarrow> Integer" where
   "length\<cdot>[] = 0" |
   "length\<cdot>(x : xs) = length\<cdot>xs + 1"
 
 fixrec delete :: "'a::Eq \<rightarrow> ['a] \<rightarrow> ['a]" where
   "delete\<cdot>x\<cdot>[] = []" |
   "delete\<cdot>x\<cdot>(y : ys) = If eq\<cdot>x\<cdot>y then ys else y : delete\<cdot>x\<cdot>ys"
 
 fixrec diff :: "['a::Eq] \<rightarrow> ['a] \<rightarrow> ['a]" where
   "diff\<cdot>xs\<cdot>[] = xs" |
   "diff\<cdot>xs\<cdot>(y : ys) = diff\<cdot>(delete\<cdot>y\<cdot>xs)\<cdot>ys"
 
 abbreviation diff_syn :: "['a::Eq] \<Rightarrow> ['a] \<Rightarrow> ['a]" (infixl "\\\\" 70) where
   "xs \\\\ ys \<equiv> diff\<cdot>xs\<cdot>ys"
 
 
 subsection \<open>Logical predicates on lists\<close>
 
 inductive finite_list :: "['a] \<Rightarrow> bool" where
   Nil [intro!, simp]: "finite_list []" |
   Cons [intro!, simp]: "\<And>x xs. finite_list xs \<Longrightarrow> finite_list (x : xs)"
 
 inductive_cases finite_listE [elim!]: "finite_list (x : xs)"
 
 lemma finite_list_upwards:
   assumes "finite_list xs" and "xs \<sqsubseteq> ys"
   shows "finite_list ys"
 using assms
 proof (induct xs arbitrary: ys)
   case Nil
   then have "ys = []" by (cases ys) simp+
   then show ?case by auto
 next
   case (Cons x xs)
   from \<open>x : xs \<sqsubseteq> ys\<close> obtain y ys' where "ys = y : ys'" by (cases ys) auto
   with \<open>x : xs \<sqsubseteq> ys\<close> have "xs \<sqsubseteq> ys'" by auto
   then have "finite_list ys'" by (rule Cons.hyps)
   with \<open>ys = _\<close> show ?case by auto
 qed
 
 lemma adm_finite_list [simp]: "adm finite_list"
   by (metis finite_list_upwards adm_upward)
 
 lemma bot_not_finite_list [simp]:
   "finite_list \<bottom> = False"
   by (rule, cases rule: finite_list.cases) auto
 
 inductive listmem :: "'a \<Rightarrow> ['a] \<Rightarrow> bool" where
   "listmem x (x : xs)" |
   "listmem x xs \<Longrightarrow> listmem x (y : xs)"
 
 lemma listmem_simps [simp]:
   shows "\<not> listmem x \<bottom>" and "\<not> listmem x []"
   and "listmem x (y : ys) \<longleftrightarrow> x = y \<or> listmem x ys"
   by (auto elim: listmem.cases intro: listmem.intros)
 
 definition set :: "['a] \<Rightarrow> 'a set" where
   "set xs = {x. listmem x xs}"
 
 lemma set_simps [simp]:
   shows "set \<bottom> = {}" and "set [] = {}"
   and "set (x : xs) = insert x (set xs)"
   unfolding set_def by auto
 
 inductive distinct :: "['a] \<Rightarrow> bool" where
   Nil [intro!, simp]: "distinct []" |
   Cons [intro!, simp]: "\<And>x xs. distinct xs \<Longrightarrow> x \<notin> set xs \<Longrightarrow> distinct (x : xs)"
 
 
 subsection \<open>Properties\<close>
 
 lemma map_strict [simp]:
   "map\<cdot>P\<cdot>\<bottom> = \<bottom>"
   by (fixrec_simp)
 
 lemma map_ID [simp]:
   "map\<cdot>ID\<cdot>xs = xs"
   by (induct xs) simp_all
 
 lemma enumFrom_intsFrom_conv [simp]:
   "enumFrom = intsFrom"
   by (intro cfun_eqI) (simp add: enumFrom_def)
 
 lemma enumFromTo_upto_conv [simp]:
   "enumFromTo = upto"
   by (intro cfun_eqI) (simp add: enumFromTo_def)
 
 lemma zipWith_strict [simp]:
   "zipWith\<cdot>f\<cdot>\<bottom>\<cdot>ys = \<bottom>"
   "zipWith\<cdot>f\<cdot>(x : xs)\<cdot>\<bottom> = \<bottom>"
   by fixrec_simp+
 
 lemma zip_simps [simp]:
   "zip\<cdot>(x : xs)\<cdot>(y : ys) = \<langle>x, y\<rangle> : zip\<cdot>xs\<cdot>ys"
   "zip\<cdot>(x : xs)\<cdot>[] = []"
   "zip\<cdot>(x : xs)\<cdot>\<bottom> = \<bottom>"
   "zip\<cdot>[]\<cdot>ys = []"
   "zip\<cdot>\<bottom>\<cdot>ys = \<bottom>"
   unfolding zip_def by simp_all
 
 lemma zip_Nil2 [simp]:
   "xs \<noteq> \<bottom> \<Longrightarrow> zip\<cdot>xs\<cdot>[] = []"
   by (cases xs) simp_all
 
 lemma nth_strict [simp]:
   "nth\<cdot>\<bottom>\<cdot>n = \<bottom>"
   "nth\<cdot>xs\<cdot>\<bottom> = \<bottom>"
   by (fixrec_simp) (cases xs, fixrec_simp+)
 
 lemma upto_strict [simp]:
   "upto\<cdot>\<bottom>\<cdot>y = \<bottom>"
   "upto\<cdot>x\<cdot>\<bottom> = \<bottom>"
   by fixrec_simp+
 
 lemma upto_simps [simp]:
   "n < m \<Longrightarrow> upto\<cdot>(MkI\<cdot>m)\<cdot>(MkI\<cdot>n) = []"
   "m \<le> n \<Longrightarrow> upto\<cdot>(MkI\<cdot>m)\<cdot>(MkI\<cdot>n) = MkI\<cdot>m : [MkI\<cdot>m+1..MkI\<cdot>n]"
   by (subst upto.simps, simp)+
 
 lemma filter_strict [simp]:
   "filter\<cdot>P\<cdot>\<bottom> = \<bottom>"
   by (fixrec_simp)
 
 lemma nth_Cons_simp [simp]:
   "eq\<cdot>n\<cdot>0 = TT \<Longrightarrow> nth\<cdot>(x : xs)\<cdot>n = x"
   "eq\<cdot>n\<cdot>0 = FF \<Longrightarrow> nth\<cdot>(x : xs)\<cdot>n = nth\<cdot>xs\<cdot>(n - 1)"
   by (subst nth.simps, simp)+
 
 lemma nth_Cons_split:
    "P (nth\<cdot>(x : xs)\<cdot>n) = ((eq\<cdot>n\<cdot>0 = FF \<longrightarrow> P (nth\<cdot>(x : xs)\<cdot>n)) \<and>
                               (eq\<cdot>n\<cdot>0 = TT \<longrightarrow> P (nth\<cdot>(x : xs)\<cdot>n)) \<and>
                               (n = \<bottom> \<longrightarrow> P (nth\<cdot>(x : xs)\<cdot>n)))"
 (*   "!!x. P (test x) = (~ (\<exists>a b. x = (a, b) & ~ P (test (a, b))))" *)
 apply (cases n, simp)
 apply (cases "n = 0", simp_all add: zero_Integer_def)
 done
 
 
 
 lemma nth_Cons_numeral [simp]:
   "(x : xs) !! 0 = x"
   "(x : xs) !! 1 = xs !! 0"
   "(x : xs) !! numeral (Num.Bit0 k) = xs !! numeral (Num.BitM k)"
   "(x : xs) !! numeral (Num.Bit1 k) = xs !! numeral (Num.Bit0 k)"
   by (simp_all add: nth_Cons numeral_Integer_eq
     zero_Integer_def one_Integer_def)
 
 lemma take_strict [simp]:
   "take\<cdot>\<bottom>\<cdot>xs = \<bottom>"
   by (fixrec_simp)
 
 lemma take_strict_2 [simp]:
   "le\<cdot>1\<cdot>i = TT \<Longrightarrow> take\<cdot>i\<cdot>\<bottom> = \<bottom>"
   by (subst take.simps, cases "le\<cdot>i\<cdot>0") (auto dest: le_trans)
 
 lemma drop_strict [simp]:
   "drop\<cdot>\<bottom>\<cdot>xs = \<bottom>"
   by (fixrec_simp)
 
 lemma isPrefixOf_strict [simp]:
   "isPrefixOf\<cdot>\<bottom>\<cdot>xs = \<bottom>"
   "isPrefixOf\<cdot>(x:xs)\<cdot>\<bottom> = \<bottom>"
   by (fixrec_simp)+
 
 lemma last_strict[simp]:
   "last\<cdot>\<bottom>= \<bottom>"
   "last\<cdot>(x:\<bottom>) = \<bottom>"
   by (fixrec_simp+)
 
 lemma last_nil [simp]:
   "last\<cdot>[] = \<bottom>"
   by (fixrec_simp)
 
 lemma last_spine_strict: "\<not> finite_list xs \<Longrightarrow> last\<cdot>xs = \<bottom>"
 proof (induct xs)
   case (Cons a xs)
   then show ?case by (cases xs) auto
 qed auto
 
 lemma init_strict [simp]:
   "init\<cdot>\<bottom>= \<bottom>"
   "init\<cdot>(x:\<bottom>) = \<bottom>"
   by (fixrec_simp+)
 
 lemma init_nil [simp]:
   "init\<cdot>[] = \<bottom>"
   by (fixrec_simp)
 
 lemma strict_foldr_strict2 [simp]:
   "(\<And>x. f\<cdot>x\<cdot>\<bottom> = \<bottom>) \<Longrightarrow> foldr\<cdot>f\<cdot>\<bottom>\<cdot>xs = \<bottom>"
   by (induct xs, auto) fixrec_simp
 
 lemma foldr_strict [simp]:
   "foldr\<cdot>f\<cdot>d\<cdot>\<bottom> = \<bottom>"
   "foldr\<cdot>f\<cdot>\<bottom>\<cdot>[] = \<bottom>"
   "foldr\<cdot>\<bottom>\<cdot>d\<cdot>(x : xs) = \<bottom>"
   by fixrec_simp+
 
 lemma foldr_Cons_Nil [simp]:
   "foldr\<cdot>(:)\<cdot>[]\<cdot>xs = xs"
   by (induct xs) simp+
 
 lemma append_strict1 [simp]:
   "\<bottom> ++ ys = \<bottom>"
   by fixrec_simp
 
 lemma foldr_append [simp]:
   "foldr\<cdot>f\<cdot>a\<cdot>(xs ++ ys) = foldr\<cdot>f\<cdot>(foldr\<cdot>f\<cdot>a\<cdot>ys)\<cdot>xs"
   by (induct xs) simp+
 
 lemma foldl_strict [simp]:
   "foldl\<cdot>f\<cdot>d\<cdot>\<bottom> = \<bottom>"
   "foldl\<cdot>f\<cdot>\<bottom>\<cdot>[] = \<bottom>"
   by fixrec_simp+
 
 lemma foldr1_strict [simp]:
   "foldr1\<cdot>f\<cdot>\<bottom>= \<bottom>"
   "foldr1\<cdot>f\<cdot>(x:\<bottom>)= \<bottom>"
   by fixrec_simp+
 
 lemma foldl1_strict [simp]:
   "foldl1\<cdot>f\<cdot>\<bottom>= \<bottom>"
   by fixrec_simp
 
 lemma foldl_spine_strict:
   "\<not> finite_list xs \<Longrightarrow> foldl\<cdot>f\<cdot>x\<cdot>xs = \<bottom>"
   by (induct xs arbitrary: x) auto
 
 lemma foldl_assoc_foldr:
   assumes "finite_list xs"
     and assoc: "\<And>x y z. f\<cdot>(f\<cdot>x\<cdot>y)\<cdot>z = f\<cdot>x\<cdot>(f\<cdot>y\<cdot>z)"
     and neutr1: "\<And>x. f\<cdot>z\<cdot>x = x"
     and neutr2: "\<And>x. f\<cdot>x\<cdot>z = x"
   shows "foldl\<cdot>f\<cdot>z\<cdot>xs = foldr\<cdot>f\<cdot>z\<cdot>xs"
   using \<open>finite_list xs\<close>
 proof (induct xs)
   case (Cons x xs)
   from \<open>finite_list xs\<close> have step: "\<And>y. f\<cdot>y\<cdot>(foldl\<cdot>f\<cdot>z\<cdot>xs) = foldl\<cdot>f\<cdot>(f\<cdot>z\<cdot>y)\<cdot>xs"
   proof (induct xs)
     case (Cons x xs y)
     have "f\<cdot>y\<cdot>(foldl\<cdot>f\<cdot>z\<cdot>(x : xs)) = f\<cdot>y\<cdot>(foldl\<cdot>f\<cdot>(f\<cdot>z\<cdot>x)\<cdot>xs)" by auto
     also have "... = f\<cdot>y\<cdot>(f\<cdot>x\<cdot>(foldl\<cdot>f\<cdot>z\<cdot>xs))" by (simp only: Cons.hyps)
     also have "... = f\<cdot>(f\<cdot>y\<cdot>x)\<cdot>(foldl\<cdot>f\<cdot>z\<cdot>xs)" by (simp only: assoc)
     also have "... = foldl\<cdot>f\<cdot>(f\<cdot>z\<cdot>(f\<cdot>y\<cdot>x))\<cdot>xs" by (simp only: Cons.hyps)
     also have "... = foldl\<cdot>f\<cdot>(f\<cdot>(f\<cdot>z\<cdot>y)\<cdot>x)\<cdot>xs" by (simp only: assoc)
     also have "... = foldl\<cdot>f\<cdot>(f\<cdot>z\<cdot>y)\<cdot>(x : xs)" by auto
     finally show ?case.
   qed (simp add: neutr1 neutr2)
 
   have "foldl\<cdot>f\<cdot>z\<cdot>(x : xs) = foldl\<cdot>f\<cdot>(f\<cdot>z\<cdot>x)\<cdot>xs" by auto
   also have "... = f\<cdot>x\<cdot>(foldl\<cdot>f\<cdot>z\<cdot>xs)" by (simp only: step)
   also have "... = f\<cdot>x\<cdot>(foldr\<cdot>f\<cdot>z\<cdot>xs)" by (simp only: Cons.hyps)
   also have "... = (foldr\<cdot>f\<cdot>z\<cdot>(x:xs))" by auto
   finally show ?case .
 qed auto
 
 lemma elem_strict [simp]:
   "elem\<cdot>x\<cdot>\<bottom> = \<bottom>"
   by fixrec_simp
 
 lemma notElem_strict [simp]:
   "notElem\<cdot>x\<cdot>\<bottom> = \<bottom>"
   by fixrec_simp
 
 lemma list_eq_nil[simp]:
   "eq\<cdot>l\<cdot>[] = TT \<longleftrightarrow> l = []"
   "eq\<cdot>[]\<cdot>l = TT \<longleftrightarrow> l = []"
   by (cases l, auto)+
 
 lemma take_Nil [simp]:
   "n \<noteq> \<bottom> \<Longrightarrow> take\<cdot>n\<cdot>[] = []"
   by (subst take.simps) (cases "le\<cdot>n\<cdot>0"; simp)
 
 lemma take_0 [simp]:
   "take\<cdot>0\<cdot>xs = []"
   "take\<cdot>(MkI\<cdot>0)\<cdot>xs = []"
   by (subst take.simps, simp add: zero_Integer_def)+
 
 lemma take_Cons [simp]:
   "le\<cdot>1\<cdot>i = TT \<Longrightarrow> take\<cdot>i\<cdot>(x:xs) = x : take\<cdot>(i - 1)\<cdot>xs"
   by (subst take.simps, cases "le\<cdot>i\<cdot>0") (auto dest: le_trans)
 
 lemma take_MkI_Cons [simp]:
   "0 < n \<Longrightarrow> take\<cdot>(MkI\<cdot>n)\<cdot>(x : xs) = x : take\<cdot>(MkI\<cdot>(n - 1))\<cdot>xs"
   by (subst take.simps) (simp add: zero_Integer_def one_Integer_def)
 
 lemma take_numeral_Cons [simp]:
   "take\<cdot>1\<cdot>(x : xs) = [x]"
   "take\<cdot>(numeral (Num.Bit0 k))\<cdot>(x : xs) = x : take\<cdot>(numeral (Num.BitM k))\<cdot>xs"
   "take\<cdot>(numeral (Num.Bit1 k))\<cdot>(x : xs) = x : take\<cdot>(numeral (Num.Bit0 k))\<cdot>xs"
   by (subst take.simps,
       simp add: zero_Integer_def one_Integer_def numeral_Integer_eq)+
 
 lemma drop_0 [simp]:
   "drop\<cdot>0\<cdot>xs = xs"
   "drop\<cdot>(MkI\<cdot>0)\<cdot>xs = xs"
   by (subst drop.simps, simp add: zero_Integer_def)+
 
 lemma drop_pos [simp]:
   "le\<cdot>n\<cdot>0 = FF \<Longrightarrow> drop\<cdot>n\<cdot>xs = (case xs of [] \<Rightarrow> [] | y : ys \<Rightarrow> drop\<cdot>(n - 1)\<cdot>ys)"
   by (subst drop.simps, simp)
 
 lemma drop_numeral_Cons [simp]:
   "drop\<cdot>1\<cdot>(x : xs) = xs"
   "drop\<cdot>(numeral (Num.Bit0 k))\<cdot>(x : xs) = drop\<cdot>(numeral (Num.BitM k))\<cdot>xs"
   "drop\<cdot>(numeral (Num.Bit1 k))\<cdot>(x : xs) = drop\<cdot>(numeral (Num.Bit0 k))\<cdot>xs"
   by (subst drop.simps,
       simp add: zero_Integer_def one_Integer_def numeral_Integer_eq)+
 
 lemma take_drop_append:
   "take\<cdot>(MkI\<cdot>i)\<cdot>xs ++ drop\<cdot>(MkI\<cdot>i)\<cdot>xs = xs"
 proof (cases i)
   case (nonneg n)
   then show ?thesis
   proof (induct n arbitrary : i xs)
     case (Suc n)
     thus ?case
       apply (subst drop.simps)
       apply (subst take.simps)
       apply (cases xs)
         apply (auto simp add: zero_Integer_def one_Integer_def )
       done
   qed simp
 next
   case (neg nat)
   then show ?thesis
     apply (subst drop.simps)
     apply (subst take.simps)
     apply (auto simp add: zero_Integer_def one_Integer_def )
     done
 qed
 
 lemma take_intsFrom_enumFrom [simp]:
   "take\<cdot>(MkI\<cdot>n)\<cdot>[MkI\<cdot>i..] = [MkI\<cdot>i..MkI\<cdot>(n+i) - 1]"
 proof (cases n)
   fix m
   assume "n = int m"
   then show ?thesis
   proof (induct m arbitrary: n i)
     case 0 then show ?case by (simp add: one_Integer_def)
   next
     case (Suc m)
     then have "n - 1 = int m" by simp
     from Suc(1) [OF this]
     have "take\<cdot>(MkI\<cdot>(n - 1))\<cdot>[MkI\<cdot>(i+1)..] = [MkI\<cdot>(i+1)..MkI\<cdot>(n - 1 + (i+1)) - 1]" .
     moreover have "(n - 1) + (i+1) - 1 = n + i - 1" by arith
     ultimately have IH: "take\<cdot>(MkI\<cdot>(n - 1))\<cdot>[MkI\<cdot>(i+1)..] = [MkI\<cdot>(i+1)..MkI\<cdot>(n+i) - 1]" by simp
     from Suc(2) have gt: "n > 0" by simp
     moreover have "[MkI\<cdot>i..] = MkI\<cdot>i : [MkI\<cdot>i + 1..]" by (simp, subst intsFrom.simps) simp
     ultimately
     have *: "take\<cdot>(MkI\<cdot>n)\<cdot>[MkI\<cdot>i..] = MkI\<cdot>i : take\<cdot>(MkI\<cdot>(n - 1))\<cdot>[MkI\<cdot>(i+1)..]"
       by (simp add: one_Integer_def)
     show ?case unfolding IH * using gt by (simp add: one_Integer_def)
   qed
 next
   fix m
   assume "n = - int m"
   then have "n \<le> 0" by simp
   then show ?thesis
     by (subst take.simps) (simp add: zero_Integer_def one_Integer_def)
 qed
 
 lemma drop_intsFrom_enumFrom [simp]:
   assumes "n \<ge> 0"
   shows "drop\<cdot>(MkI\<cdot>n)\<cdot>[MkI\<cdot>i..] = [MkI\<cdot>(n+i)..]"
 proof-
   from assms obtain n' where "n = int n'" by (cases n, auto)
   then show ?thesis
     apply(induct n' arbitrary: n i )
      apply simp
     apply (subst intsFrom.simps[unfolded enumFrom_intsFrom_conv[symmetric]])
     apply (subst drop.simps)
     apply (auto simp add: zero_Integer_def one_Integer_def)
     apply (rule cfun_arg_cong)
     apply (rule cfun_arg_cong)
     apply arith
     done
 qed
 
 lemma last_append_singleton:
   "finite_list xs \<Longrightarrow> last\<cdot>(xs ++ [x]) = x"
 proof (induct xs rule:finite_list.induct)
   case (Cons x xs)
   then show ?case by (cases xs) auto
 qed auto
 
 lemma init_append_singleton:
   "finite_list xs \<Longrightarrow> init\<cdot>(xs ++ [x]) = xs"
 proof (induct xs rule:finite_list.induct)
   case (Cons x xs)
   then show ?case by (cases xs) auto
 qed auto
 
 lemma append_Nil2 [simp]:
   "xs ++ [] = xs"
   by (induct xs) simp_all
 
 lemma append_assoc [simp]:
   "(xs ++ ys) ++ zs = xs ++ ys ++ zs"
   by (induct xs) simp_all
 
 lemma concat_simps [simp]:
   "concat\<cdot>[] = []"
   "concat\<cdot>(xs : xss) = xs ++ concat\<cdot>xss"
   "concat\<cdot>\<bottom> = \<bottom>"
   unfolding concat_def by simp_all
 
 lemma concatMap_simps [simp]:
   "concatMap\<cdot>f\<cdot>[] = []"
   "concatMap\<cdot>f\<cdot>(x : xs) = f\<cdot>x ++ concatMap\<cdot>f\<cdot>xs"
   "concatMap\<cdot>f\<cdot>\<bottom> = \<bottom>"
   unfolding concatMap_def by simp_all
 
 lemma filter_append [simp]:
   "filter\<cdot>P\<cdot>(xs ++ ys) = filter\<cdot>P\<cdot>xs ++ filter\<cdot>P\<cdot>ys"
 proof (induct xs)
   case (Cons x xs) then show ?case by (cases "P\<cdot>x") (auto simp: If_and_if)
 qed simp_all
 
 lemma elem_append [simp]:
   "elem\<cdot>x\<cdot>(xs ++ ys) = (elem\<cdot>x\<cdot>xs orelse elem\<cdot>x\<cdot>ys)"
     by (induct xs) auto
 
 lemma filter_filter [simp]:
   "filter\<cdot>P\<cdot>(filter\<cdot>Q\<cdot>xs) = filter\<cdot>(\<Lambda> x. Q\<cdot>x andalso P\<cdot>x)\<cdot>xs"
   by (induct xs) (auto simp: If2_def [symmetric] split: split_If2)
 
 lemma filter_const_TT [simp]:
   "filter\<cdot>(\<Lambda> _. TT)\<cdot>xs = xs"
   by (induct xs) simp_all
 
 lemma tails_strict [simp]:
   "tails\<cdot>\<bottom> = \<bottom>"
   by fixrec_simp
 
 lemma inits_strict [simp]:
   "inits\<cdot>\<bottom> = \<bottom>"
   by fixrec_simp
 
 lemma the_and_strict [simp]:
   "the_and\<cdot>\<bottom> = \<bottom>"
   by fixrec_simp
 
 lemma the_or_strict [simp]:
   "the_or\<cdot>\<bottom> = \<bottom>"
   by fixrec_simp
 
 lemma all_strict [simp]:
   "all\<cdot>P\<cdot>\<bottom> = \<bottom>"
   by fixrec_simp
 
 lemma any_strict [simp]:
   "any\<cdot>P\<cdot>\<bottom> = \<bottom>"
   by fixrec_simp
 
 lemma tails_neq_Nil [simp]:
   "tails\<cdot>xs \<noteq> []"
   by (cases xs) simp_all
 
 lemma inits_neq_Nil [simp]:
   "inits\<cdot>xs \<noteq> []"
   by (cases xs) simp_all
 
 lemma Nil_neq_tails [simp]:
   "[] \<noteq> tails\<cdot>xs"
   by (cases xs) simp_all
 
 lemma Nil_neq_inits [simp]:
   "[] \<noteq> inits\<cdot>xs"
   by (cases xs) simp_all
 
 lemma finite_list_not_bottom [simp]:
   assumes "finite_list xs" shows "xs \<noteq> \<bottom>"
   using assms by (cases) simp_all
 
 lemma head_append [simp]:
   "head\<cdot>(xs ++ ys) = If null\<cdot>xs then head\<cdot>ys else head\<cdot>xs"
   by (cases xs) simp_all
 
 lemma filter_cong:
   "\<forall>x\<in>set xs. p\<cdot>x = q\<cdot>x \<Longrightarrow> filter\<cdot>p\<cdot>xs = filter\<cdot>q\<cdot>xs"
 proof (induct arbitrary: xs rule: filter.induct)
   case (3 x)
   then show ?case by (cases xs) auto
 qed simp_all
 
 lemma filter_TT [simp]:
   assumes "\<forall>x\<in>set xs. P\<cdot>x = TT"
   shows "filter\<cdot>P\<cdot>xs = xs"
   by (rule filter_cong [of xs P "\<Lambda> _. TT", simplified, OF assms])
 
 lemma filter_FF [simp]:
   assumes "finite_list xs"
     and "\<forall>x\<in>set xs. P\<cdot>x = FF"
   shows "filter\<cdot>P\<cdot>xs = []"
   using assms by (induct xs) simp_all
 
 lemma map_cong:
   "\<forall>x\<in>set xs. p\<cdot>x = q\<cdot>x \<Longrightarrow> map\<cdot>p\<cdot>xs = map\<cdot>q\<cdot>xs"
 proof (induct arbitrary: xs rule: map.induct)
   case (3 x)
   then show ?case by (cases xs) auto
 qed simp_all
 
 lemma finite_list_upto:
   "finite_list (upto\<cdot>(MkI\<cdot>m)\<cdot>(MkI\<cdot>n))" (is "?P m n")
 proof (cases "n - m")
   fix d
   assume "n - m = int d"
   then show "?P m n"
   proof (induct d arbitrary: m n)
     case (Suc d)
     then have "n - (m + 1) = int d" and le: "m \<le> n" by simp_all
     from Suc(1) [OF this(1)] have IH: "?P (m+1) n" .
     then show ?case using le by (simp add: one_Integer_def)
   qed (simp add: one_Integer_def)
 next
   fix d
   assume "n - m = - int d"
   then have "n \<le> m" by auto
   moreover
-  { assume "n = m" then have "?P m n" by (simp add: one_Integer_def) }
+  have "?P m n" if "n = m" using that by (simp add: one_Integer_def)
   moreover
-  { assume "n < m" then have "?P m n" by (simp add: one_Integer_def) }
+  have "?P m n" if "n < m" using that by (simp add: one_Integer_def)
   ultimately show ?thesis by arith
 qed
 
 lemma filter_commute:
   assumes "\<forall>x\<in>set xs. (Q\<cdot>x andalso P\<cdot>x) = (P\<cdot>x andalso Q\<cdot>x)"
   shows "filter\<cdot>P\<cdot>(filter\<cdot>Q\<cdot>xs) = filter\<cdot>Q\<cdot>(filter\<cdot>P\<cdot>xs)"
   using filter_cong [of xs "\<Lambda> x. Q\<cdot>x andalso P\<cdot>x" "\<Lambda> x. P\<cdot>x andalso Q\<cdot>x"]
     and assms by simp
 
 lemma upto_append_intsFrom [simp]:
   assumes "m \<le> n"
   shows "upto\<cdot>(MkI\<cdot>m)\<cdot>(MkI\<cdot>n) ++ intsFrom\<cdot>(MkI\<cdot>n+1) = intsFrom\<cdot>(MkI\<cdot>m)"
     (is "?u m n ++ _ = ?i m")
 proof (cases "n - m")
   case (nonneg i)
   with assms show ?thesis
   proof (induct i arbitrary: m n)
     case (Suc i)
     then have "m + 1 \<le> n" and "n - (m + 1) = int i" by simp_all
     from Suc(1) [OF this]
     have IH: "?u (m+1) n ++ ?i (n+1) = ?i (m+1)" by (simp add: one_Integer_def)
     from \<open>m + 1 \<le> n\<close> have "m \<le> n" by simp
     then have "?u m n ++ ?i (n+1) = (MkI\<cdot>m : ?u (m+1) n) ++ ?i (n+1)"
       by (simp add: one_Integer_def)
     also have "\<dots> = MkI\<cdot>m : ?i (m+1)" by (simp add: IH)
     finally show ?case by (subst (2) intsFrom.simps) (simp add: one_Integer_def)
   qed (subst (2) intsFrom.simps, simp add: one_Integer_def)
 next
   case (neg i)
   then have "n < m" by simp
   with assms show ?thesis by simp
 qed
 
 lemma set_upto [simp]:
   "set (upto\<cdot>(MkI\<cdot>m)\<cdot>(MkI\<cdot>n)) = {MkI\<cdot>i | i. m \<le> i \<and> i \<le> n}"
   (is "set (?u m n) = ?R m n")
 proof (cases "n - m")
   case (nonneg i)
   then show ?thesis
   proof (induct i arbitrary: m n)
     case (Suc i)
     then have *: "n - (m + 1) = int i" by simp
     from Suc(1) [OF *] have IH: "set (?u (m+1) n) = ?R (m+1) n" .
     from * have "m \<le> n" by simp
     then have "set (?u m n) = set (MkI\<cdot>m : ?u (m+1) n)" by (simp add: one_Integer_def)
     also have "\<dots> = insert (MkI\<cdot>m) (?R (m+1) n)" by (simp add: IH)
     also have "\<dots> = ?R m n" using \<open>m \<le> n\<close> by auto
     finally show ?case .
   qed (force simp: one_Integer_def)
 qed simp
 
 lemma Nil_append_iff [iff]:
   "xs ++ ys = [] \<longleftrightarrow> xs = [] \<and> ys = []"
   by (induct xs) simp_all
 
 text \<open>This version of definedness rule for Nil is made necessary by
 the reorient simproc.\<close>
 
 lemma bottom_neq_Nil [simp]: "\<bottom> \<noteq> []"
   by simp
 
 text \<open>Simproc to rewrite @{term "Nil = x"} to @{term "x = Nil"}.\<close>
 
 setup \<open>
   Reorient_Proc.add
     (fn Const(@{const_name Nil}, _) => true | _ => false)
 \<close>
 
-simproc_setup reorient_Nil ("Nil = x") = Reorient_Proc.proc
+simproc_setup reorient_Nil ("Nil = x") = \<open>K Reorient_Proc.proc\<close>
 
 
 lemma set_append [simp]:
   assumes "finite_list xs"
   shows "set (xs ++ ys) = set xs \<union> set ys"
   using assms by (induct) simp_all
 
 lemma distinct_Cons [simp]:
   "distinct (x : xs) \<longleftrightarrow> distinct xs \<and> x \<notin> set xs"
   (is "?l = ?r")
 proof
   assume ?l then show ?r by (cases) simp_all
 next
   assume ?r then show ?l by auto
 qed
 
 lemma finite_list_append [iff]:
   "finite_list (xs ++ ys) \<longleftrightarrow> finite_list xs \<and> finite_list ys"
   (is "?l = ?r")
 proof
   presume "finite_list xs" and "finite_list ys"
   then show ?l by (induct) simp_all
 next
   assume "?l" then show "?r"
   proof (induct "xs ++ ys" arbitrary: xs ys)
     case (Cons x xs)
     then show ?case by (cases xs) auto
   qed simp
 qed simp_all
 
 lemma distinct_append [simp]:
   assumes "finite_list (xs ++ ys)"
   shows "distinct (xs ++ ys) \<longleftrightarrow> distinct xs \<and> distinct ys \<and> set xs \<inter> set ys = {}"
     (is "?P xs ys")
   using assms
 proof (induct "xs ++ ys" arbitrary: xs ys)
-  case (Cons z zs)
+  case Cons': (Cons z zs)
   show ?case
   proof (cases xs)
-    note Cons' = Cons
     case (Cons u us)
     with Cons' have "finite_list us"
       and [simp]: "zs = us ++ ys" "?P us ys" by simp_all
     then show ?thesis by (auto simp: Cons)
-  qed (insert Cons, simp_all)
+  qed (use Cons' in simp_all)
 qed simp
 
 lemma finite_set [simp]:
   assumes "distinct xs"
   shows "finite (set xs)"
   using assms by induct auto
 
 lemma distinct_card:
   assumes "distinct xs"
   shows "MkI\<cdot>(int (card (set xs))) = length\<cdot>xs"
   using assms
   by (induct)
      (simp_all add: zero_Integer_def plus_MkI_MkI [symmetric] one_Integer_def ac_simps)
 
 lemma set_delete [simp]:
   fixes xs :: "['a::Eq_eq]"
   assumes "distinct xs"
     and "\<forall>x\<in>set xs. eq\<cdot>a\<cdot>x \<noteq> \<bottom>"
   shows "set (delete\<cdot>a\<cdot>xs) = set xs - {a}"
   using assms
 proof induct
   case (Cons x xs)
   then show ?case by (cases "eq\<cdot>a\<cdot>x", force+)
 qed simp
 
 lemma distinct_delete [simp]:
   fixes xs :: "['a::Eq_eq]"
   assumes "distinct xs"
     and "\<forall>x\<in>set xs. eq\<cdot>a\<cdot>x \<noteq> \<bottom>"
   shows "distinct (delete\<cdot>a\<cdot>xs)"
   using assms
 proof induct
   case (Cons x xs)
   then show ?case by (cases "eq\<cdot>a\<cdot>x", force+)
 qed simp
 
 lemma set_diff [simp]:
   fixes xs ys :: "['a::Eq_eq]"
   assumes "distinct ys" and "distinct xs"
     and "\<forall>a\<in>set ys. \<forall>x\<in>set xs. eq\<cdot>a\<cdot>x \<noteq> \<bottom>"
   shows "set (xs \\\\ ys) = set xs - set ys"
   using assms
 proof (induct arbitrary: xs)
   case Nil then show ?case by (induct xs rule: distinct.induct) simp_all
 next
   case (Cons y ys)
   let ?xs = "delete\<cdot>y\<cdot>xs"
   from Cons have *: "\<forall>x\<in>set xs. eq\<cdot>y\<cdot>x \<noteq> \<bottom>" by simp
   from set_delete [OF \<open>distinct xs\<close> this]
   have **: "set ?xs = set xs - {y}" .
   with Cons have "\<forall>a\<in>set ys. \<forall>x\<in>set ?xs. eq\<cdot>a\<cdot>x \<noteq> \<bottom>" by simp
   moreover from * and \<open>distinct xs\<close> have "distinct ?xs" by simp
   ultimately have "set (?xs \\\\ ys) = set ?xs - set ys"
     using Cons by blast
   then show ?case by (force simp: **)
 qed
 
 lemma distinct_delete_filter:
   fixes xs :: "['a::Eq_eq]"
   assumes "distinct xs"
     and "\<forall>x\<in>set xs. eq\<cdot>a\<cdot>x \<noteq> \<bottom>"
   shows "delete\<cdot>a\<cdot>xs = filter\<cdot>(\<Lambda> x. neq\<cdot>a\<cdot>x)\<cdot>xs"
   using assms
 proof (induct)
   case (Cons x xs)
   then have IH: "delete\<cdot>a\<cdot>xs = filter\<cdot>(\<Lambda> x. neq\<cdot>a\<cdot>x)\<cdot>xs" by simp
   show ?case
   proof (cases "eq\<cdot>a\<cdot>x")
     case TT
     have "\<forall>x\<in>set xs. (\<Lambda> x. neq\<cdot>a\<cdot>x)\<cdot>x = (\<Lambda> _. TT)\<cdot>x"
     proof
       fix y
       assume "y \<in> set xs"
       with Cons(3, 4) have "x \<noteq> y" and "eq\<cdot>a\<cdot>y \<noteq> \<bottom>" by auto
       with TT have "eq\<cdot>a\<cdot>y = FF" by (metis (no_types) eqD(1) trE)
       then show "(\<Lambda> x. neq\<cdot>a\<cdot>x)\<cdot>y = (\<Lambda> _. TT)\<cdot>y" by simp
     qed
     from filter_cong [OF this] and TT
     show ?thesis by simp
   qed (simp_all add: IH)
 qed simp
 
 lemma distinct_diff_filter:
   fixes xs ys :: "['a::Eq_eq]"
   assumes "finite_list ys"
     and "distinct xs"
     and "\<forall>a\<in>set ys. \<forall>x\<in>set xs. eq\<cdot>a\<cdot>x \<noteq> \<bottom>"
   shows "xs \\\\ ys = filter\<cdot>(\<Lambda> x. neg\<cdot>(elem\<cdot>x\<cdot>ys))\<cdot>xs"
   using assms
 proof (induct arbitrary: xs)
   case Nil then show ?case by simp
 next
   case (Cons y ys)
   let ?xs = "delete\<cdot>y\<cdot>xs"
   from Cons have *: "\<forall>x\<in>set xs. eq\<cdot>y\<cdot>x \<noteq> \<bottom>" by simp
   from set_delete [OF \<open>distinct xs\<close> this]
   have "set ?xs = set xs - {y}" .
   with Cons have "\<forall>a\<in>set ys. \<forall>x\<in>set ?xs. eq\<cdot>a\<cdot>x \<noteq> \<bottom>" by simp
   moreover from * and \<open>distinct xs\<close> have "distinct ?xs" by simp
   ultimately have "?xs \\\\ ys = filter\<cdot>(\<Lambda> x. neg\<cdot>(elem\<cdot>x\<cdot>ys))\<cdot>?xs"
     using Cons by blast
   then show ?case
     using \<open>distinct xs\<close> and *
     by (simp add: distinct_delete_filter)
 qed
 
 lemma distinct_upto [intro, simp]:
   "distinct [MkI\<cdot>m..MkI\<cdot>n]"
 proof (cases "n - m")
   case (nonneg i)
   then show ?thesis
   proof (induct i arbitrary: m)
     case (Suc i)
     then have "n - (m + 1) = int i" and "m \<le> n" by simp_all
     with Suc have "distinct [MkI\<cdot>(m+1)..MkI\<cdot>n]" by force
     with \<open>m \<le> n\<close> show ?case by (simp add: one_Integer_def)
   qed (simp add: one_Integer_def)
 qed simp
 
 lemma set_intsFrom [simp]:
   "set (intsFrom\<cdot>(MkI\<cdot>m)) = {MkI\<cdot>n | n. m \<le> n}"
   (is "set (?i m) = ?I")
 proof
   show "set (?i m) \<subseteq> ?I"
   proof
     fix n
     assume "n \<in> set (?i m)"
     then have "listmem n (?i m)" by (simp add: set_def)
     then show "n \<in> ?I"
     proof (induct n "(?i m)" arbitrary: m)
       fix x xs m
       assume "x : xs = ?i m"
       then have "x : xs = MkI\<cdot>m : ?i (m+1)"
         by (subst (asm) intsFrom.simps) (simp add: one_Integer_def)
       then have [simp]: "x = MkI\<cdot>m" "xs = ?i (m+1)" by simp_all
       show "x \<in> {MkI\<cdot>n | n. m \<le> n}" by simp
     next
       fix x xs y m
       assume IH: "listmem x xs"
         "\<And>m. xs = ?i m \<Longrightarrow> x \<in> {MkI\<cdot>n | n. m \<le> n}"
         "y : xs = ?i m"
       then have "y : xs = MkI\<cdot>m : ?i (m+1)"
         by (subst (asm) (2) intsFrom.simps) (simp add: one_Integer_def)
       then have [simp]: "y = MkI\<cdot>m" "xs = ?i (m+1)" by simp_all
       from IH (2) [of "m+1"] have "x \<in> {MkI\<cdot>n | n. m+1 \<le> n}" by (simp add: one_Integer_def)
       then show "x \<in> {MkI\<cdot>n | n. m \<le> n}" by force
     qed
   qed
 next
   show "?I \<subseteq> set (?i m)"
   proof
     fix x
     assume "x \<in> ?I"
     then obtain n where [simp]: "x = MkI\<cdot>n" and "m \<le> n" by blast
     from upto_append_intsFrom [OF this(2), symmetric]
     have *: "set (?i m) = set (upto\<cdot>(MkI\<cdot>m)\<cdot>(MkI\<cdot>n)) \<union> set (?i (n+1))"
       using finite_list_upto [of m n] by (simp add: one_Integer_def)
     show "x \<in> set (?i m)" using \<open>m \<le> n\<close> by (auto simp: * one_Integer_def)
   qed
 qed
 
 lemma If_eq_bottom_iff [simp]: (* FIXME: move *)
   "(If b then x else y = \<bottom>) \<longleftrightarrow> b = \<bottom> \<or> b = TT \<and> x = \<bottom> \<or> b = FF \<and> y = \<bottom>"
   by (induct b) simp_all
 
 lemma upto_eq_bottom_iff [simp]:
   "upto\<cdot>m\<cdot>n = \<bottom> \<longleftrightarrow> m = \<bottom> \<or> n = \<bottom>"
   by (subst upto.simps, simp)
 
 lemma seq_eq_bottom_iff [simp]: (* FIXME: move *)
   "seq\<cdot>x\<cdot>y = \<bottom> \<longleftrightarrow> x = \<bottom> \<or> y = \<bottom>"
   by (simp add: seq_conv_if)
 
 lemma intsFrom_eq_bottom_iff [simp]:
   "intsFrom\<cdot>m = \<bottom> \<longleftrightarrow> m = \<bottom>"
   by (subst intsFrom.simps, simp)
 
 lemma intsFrom_split:
   assumes "m \<ge> n"
   shows "[MkI\<cdot>n..] = [MkI\<cdot>n .. MkI\<cdot>(m - 1)] ++ [MkI\<cdot>m..]"
 proof-
   from assms have ge: "m - n \<ge> 0" by arith
   have "[MkI\<cdot>n..] = (take\<cdot>(MkI\<cdot>(m - n)) \<cdot> [MkI\<cdot>n..]) ++ (drop\<cdot>(MkI\<cdot>(m - n)) \<cdot> [MkI\<cdot>n..])"
     by (subst take_drop_append, rule)
   also have "... = [MkI\<cdot>n.. MkI\<cdot>(m - 1)] ++ [MkI\<cdot>m..]"
     by (subst drop_intsFrom_enumFrom[OF ge], auto simp add:take_intsFrom_enumFrom[simplified] one_Integer_def)
   finally show ?thesis .
 qed
 
 lemma filter_fast_forward:
   assumes "n+1 \<le> n'"
     and  "\<forall>k . n < k \<longrightarrow> k < n' \<longrightarrow> \<not> P k"
   shows "filter\<cdot>(\<Lambda> (MkI\<cdot>i) . Def (P i))\<cdot>[MkI\<cdot>(n+1)..] = filter\<cdot>(\<Lambda> (MkI\<cdot>i) . Def (P i))\<cdot>[MkI\<cdot>n'..]"
 proof-
   from assms(1)
   have"[MkI\<cdot>(n+1)..] = [MkI\<cdot>(n+1).. MkI\<cdot>(n'- 1)] ++ [MkI\<cdot>n'..]" (is "_ = ?l1 ++ ?l2")
     by (subst intsFrom_split[of "n+1" n'], auto)
   moreover
   have "filter\<cdot>(\<Lambda> (MkI\<cdot>i) . Def (P i))\<cdot>[MkI\<cdot>(n+1).. MkI\<cdot>(n'- 1)] = []"
     apply (rule filter_FF)
      apply (simp, rule finite_list_upto)
     using assms(2)
     apply auto
     done
   ultimately
   show ?thesis by simp
 qed
 
 lemma null_eq_TT_iff [simp]:
   "null\<cdot>xs = TT \<longleftrightarrow> xs = []"
   by (cases xs) simp_all
 
 lemma null_set_empty_conv:
   "xs \<noteq> \<bottom> \<Longrightarrow> null\<cdot>xs = TT \<longleftrightarrow> set xs = {}"
   by (cases xs) simp_all
 
 lemma elem_TT [simp]:
   fixes x :: "'a::Eq_eq" shows "elem\<cdot>x\<cdot>xs = TT \<Longrightarrow> x \<in> set xs"
   apply (induct arbitrary: xs rule: elem.induct, simp_all)
   apply (rename_tac xs, case_tac xs, simp_all)
   apply (rename_tac a list, case_tac "eq\<cdot>a\<cdot>x", force+)
   done
 
 lemma elem_FF [simp]:
   fixes x :: "'a::Eq_equiv" shows "elem\<cdot>x\<cdot>xs = FF \<Longrightarrow> x \<notin> set xs"
   by (induct arbitrary: xs rule: elem.induct, simp_all)
      (rename_tac xs, case_tac xs, simp_all, force)
 
 lemma length_strict [simp]:
   "length\<cdot>\<bottom> = \<bottom>"
   by (fixrec_simp)
 
 lemma repeat_neq_bottom [simp]:
   "repeat\<cdot>x \<noteq> \<bottom>"
   by (subst repeat.simps) simp
 
 lemma list_case_repeat [simp]:
   "list_case\<cdot>a\<cdot>f\<cdot>(repeat\<cdot>x) = f\<cdot>x\<cdot>(repeat\<cdot>x)"
   by (subst repeat.simps) simp
 
 lemma length_append [simp]:
   "length\<cdot>(xs ++ ys) = length\<cdot>xs + length\<cdot>ys"
   by (induct xs) (simp_all add: ac_simps)
 
 lemma replicate_strict [simp]:
   "replicate\<cdot>\<bottom>\<cdot>x = \<bottom>"
   by (simp add: replicate_def)
 
 lemma replicate_0 [simp]:
   "replicate\<cdot>0\<cdot>x = []"
   "replicate\<cdot>(MkI\<cdot>0)\<cdot>xs = []"
   by (simp add: replicate_def)+
 
 lemma Integer_add_0 [simp]: "MkI\<cdot>0 + n = n"
   by (cases n) simp_all
 
 lemma replicate_MkI_plus_1 [simp]:
   "0 \<le> n \<Longrightarrow> replicate\<cdot>(MkI\<cdot>(n+1))\<cdot>x = x : replicate\<cdot>(MkI\<cdot>n)\<cdot>x"
   "0 \<le> n \<Longrightarrow> replicate\<cdot>(MkI\<cdot>(1+n))\<cdot>x = x : replicate\<cdot>(MkI\<cdot>n)\<cdot>x"
   by (simp add: replicate_def, subst take.simps, simp add: one_Integer_def zero_Integer_def)+
 
 lemma replicate_append_plus_conv:
   assumes "0 \<le> m" and "0 \<le> n"
   shows "replicate\<cdot>(MkI\<cdot>m)\<cdot>x ++ replicate\<cdot>(MkI\<cdot>n)\<cdot>x
     = replicate\<cdot>(MkI\<cdot>m + MkI\<cdot>n)\<cdot>x"
 proof (cases m)
   case (nonneg i)
   with assms show ?thesis
   proof (induct i arbitrary: m)
     case (Suc i)
     then have ge: "int i + n \<ge> 0" by force
     have "replicate\<cdot>(MkI\<cdot>m)\<cdot>x ++ replicate\<cdot>(MkI\<cdot>n)\<cdot>x = x : (replicate\<cdot>(MkI\<cdot>(int i))\<cdot>x ++ replicate\<cdot>(MkI\<cdot>n)\<cdot>x)" by (simp add: Suc)
     also have "\<dots> = x : replicate\<cdot>(MkI\<cdot>(int i) + MkI\<cdot>n)\<cdot>x" using Suc by simp
     finally show ?case using ge by (simp add: Suc ac_simps)
   qed simp
 next
   case (neg i)
   with assms show ?thesis by simp
 qed
 
 lemma replicate_MkI_1 [simp]:
   "replicate\<cdot>(MkI\<cdot>1)\<cdot>x = x : []"
   by (simp add: replicate_def, subst take.simps, simp add: zero_Integer_def one_Integer_def)
 
 lemma length_replicate [simp]:
   assumes "0 \<le> n"
   shows "length\<cdot>(replicate\<cdot>(MkI\<cdot>n)\<cdot>x) = MkI\<cdot>n"
 proof (cases n)
   case (nonneg i)
   with assms show ?thesis
     by (induct i arbitrary: n)
        (simp_all add: replicate_append_plus_conv zero_Integer_def one_Integer_def)
 next
   case (neg i)
   with assms show ?thesis by (simp add: replicate_def)
 qed
 
 lemma map_oo [simp]:
   "map\<cdot>f\<cdot>(map\<cdot>g\<cdot>xs) = map\<cdot>(f oo g)\<cdot>xs"
   by (induct xs) simp_all
 
 lemma nth_Cons_MkI [simp]:
   "0 < i \<Longrightarrow> (a : xs) !! (MkI\<cdot>i) = xs !! (MkI\<cdot>(i - 1))"
   unfolding nth_Cons
   by (cases i, simp add: zero_Integer_def one_Integer_def) (case_tac n, simp_all)
 
 lemma map_plus_intsFrom:
   "map\<cdot>(+ MkI\<cdot>n)\<cdot>(intsFrom\<cdot>(MkI\<cdot>m)) = intsFrom\<cdot>(MkI\<cdot>(m+n))" (is "?l = ?r")
 proof (rule list.take_lemma)
   fix i show "list_take i\<cdot>?l = list_take i\<cdot>?r"
   proof (induct i arbitrary: m)
     case (Suc i) then show ?case
       by (subst (1 2) intsFrom.simps) (simp add: ac_simps one_Integer_def)
   qed simp
 qed
 
 lemma plus_eq_MkI_conv:
   "l + n = MkI\<cdot>m \<longleftrightarrow> (\<exists>l' n'. l = MkI\<cdot>l' \<and> n = MkI\<cdot>n' \<and> m = l' + n')"
   by (cases l, simp) (cases n, auto)
 
 lemma length_ge_0:
   "length\<cdot>xs = MkI\<cdot>n \<Longrightarrow> n \<ge> 0"
   by (induct xs arbitrary: n) (auto simp: one_Integer_def plus_eq_MkI_conv)
 
 lemma length_0_conv [simp]:
   "length\<cdot>xs = MkI\<cdot>0 \<longleftrightarrow> xs = []"
   apply (cases xs)
     apply (simp_all add: one_Integer_def)
   apply (case_tac "length\<cdot>list")
    apply (auto dest: length_ge_0)
   done
 
 lemma length_ge_1 [simp]:
   "length\<cdot>xs = MkI\<cdot>(1 + int n)
     \<longleftrightarrow> (\<exists>u us. xs = u : us \<and> length\<cdot>us = MkI\<cdot>(int n))"
   (is "?l = ?r")
 proof
   assume ?r then show ?l by (auto simp: one_Integer_def)
 next
   assume 1: ?l
   then obtain u us where [simp]: "xs = u : us" by (cases xs) auto
   from 1 have 2: "1 + length\<cdot>us = MkI\<cdot>(1 + int n)" by (simp add: ac_simps)
   then have "length\<cdot>us \<noteq> \<bottom>" by (cases "length\<cdot>us") simp_all
   moreover from 2 have "length\<cdot>us + 1 = MkI\<cdot>(int n) + 1" by (simp add: one_Integer_def ac_simps)
   ultimately have "length\<cdot>us = MkI\<cdot>(int n)"
     by (cases "length\<cdot>us") (simp_all add: one_Integer_def)
   then show ?r by simp
 qed
 
 lemma finite_list_length_conv:
   "finite_list xs \<longleftrightarrow> (\<exists>n. length\<cdot>xs = MkI\<cdot>(int n))" (is "?l = ?r")
 proof
   assume "?l" then show "?r"
     by (induct, auto simp: one_Integer_def) presburger
 next
   assume "?r"
   then obtain n where "length\<cdot>xs = MkI\<cdot>(int n)" by blast
   then show "?l" by (induct n arbitrary: xs) auto
 qed
 
 lemma nth_append:
   assumes "length\<cdot>xs = MkI\<cdot>n" and "n \<le> m"
   shows "(xs ++ ys) !! MkI\<cdot>m = ys !! MkI\<cdot>(m - n)"
   using assms
 proof (induct xs arbitrary: n m)
   case (Cons x xs)
   then have ge: "n \<ge> 0" by (blast intro: length_ge_0)
   from Cons(2)
   have len: "length\<cdot>xs = MkI\<cdot>(n - 1)"
     by (auto simp: plus_eq_MkI_conv one_Integer_def)
   from Cons(3) have le: "n - 1 \<le> m - 1" by simp
-  { assume "m < 0"
-    with ge have ?case using Cons(3) by simp }
-  moreover
-  { assume "m = 0"
+  consider "m < 0" | "m = 0" | "m > 0" by arith
+  then show ?case
+  proof cases
+    case 1
+    with ge show ?thesis using Cons(3) by simp
+  next
+    case 2
     with Cons(3) and ge have "n = 0" by simp
-    with Cons(2) have ?case
-      by (auto dest: length_ge_0 simp: one_Integer_def plus_eq_MkI_conv) }
-  moreover
-  { assume "m > 0"
-    then have ?case
-      by (auto simp: Cons(1) [OF len le] zero_Integer_def one_Integer_def) }
-  ultimately show ?case by arith
+    with Cons(2) show ?thesis
+      by (auto dest: length_ge_0 simp: one_Integer_def plus_eq_MkI_conv)
+  next
+    case 3
+    then show ?thesis
+      by (auto simp: Cons(1) [OF len le] zero_Integer_def one_Integer_def)
+  qed
 qed (simp_all add: zero_Integer_def)
 
 lemma replicate_nth [simp]:
   assumes "0 \<le> n"
   shows "(replicate\<cdot>(MkI\<cdot>n)\<cdot>x ++ xs) !! MkI\<cdot>n = xs !! MkI\<cdot>0"
   using nth_append [OF length_replicate [OF assms], of n]
     by simp
 
 lemma map2_zip:
   "map\<cdot>(\<Lambda>\<langle>x, y\<rangle>. \<langle>x, f\<cdot>y\<rangle>)\<cdot>(zip\<cdot>xs\<cdot>ys) = zip\<cdot>xs\<cdot>(map\<cdot>f\<cdot>ys)"
   by (induct xs arbitrary: ys) (simp_all, case_tac ys, simp_all)
 
 lemma map2_filter:
   "map\<cdot>(\<Lambda>\<langle>x, y\<rangle>. \<langle>x, f\<cdot>y\<rangle>)\<cdot>(filter\<cdot>(\<Lambda>\<langle>x, y\<rangle>. P\<cdot>x)\<cdot>xs)
     = filter\<cdot>(\<Lambda>\<langle>x, y\<rangle>. P\<cdot>x)\<cdot>(map\<cdot>(\<Lambda>\<langle>x, y\<rangle>. \<langle>x, f\<cdot>y\<rangle>)\<cdot>xs)"
   apply (induct xs, simp_all)
   apply (rename_tac x xs, case_tac x, simp, simp)
   apply (rename_tac a b, case_tac "P\<cdot>a", auto)
 done
 
 lemma map_map_snd:
   "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> map\<cdot>f\<cdot>(map\<cdot>snd\<cdot>xs)
     = map\<cdot>snd\<cdot>(map\<cdot>(\<Lambda>\<langle>x, y\<rangle>. \<langle>x, f\<cdot>y\<rangle>)\<cdot>xs)"
   by (induct xs, simp_all, rename_tac a b, case_tac a, simp_all)
 
 lemma findIndices_Cons [simp]:
   "findIndices\<cdot>P\<cdot>(a : xs) =
     If P\<cdot>a then 0 : map\<cdot>(+1)\<cdot>(findIndices\<cdot>P\<cdot>xs)
     else map\<cdot>(+1)\<cdot>(findIndices\<cdot>P\<cdot>xs)"
   by (auto simp: findIndices_def, subst intsFrom.simps, cases "P\<cdot>a")
      (simp_all
        del: map_oo
        add: map_oo [symmetric] map_map_snd one_Integer_def zero_Integer_def
        map_plus_intsFrom [of 1 0, simplified, symmetric]
        map2_zip [of "(+ MkI\<cdot>1)", simplified]
        map2_filter [of "(+ MkI\<cdot>1)", simplified])
 
 lemma filter_alt_def:
   fixes xs :: "['a]"
   shows "filter\<cdot>P\<cdot>xs = map\<cdot>(nth\<cdot>xs)\<cdot>(findIndices\<cdot>P\<cdot>xs)"
 proof -
-  {
-    fix f g :: "Integer \<rightarrow> 'a"
+  have 1: "map\<cdot>f\<cdot>(map\<cdot>snd\<cdot>(filter\<cdot>(\<Lambda>\<langle>x, i\<rangle>. P\<cdot>x)\<cdot>(zip\<cdot>xs\<cdot>[MkI\<cdot>i..])))
+    = map\<cdot>g\<cdot>(map\<cdot>snd\<cdot>(filter\<cdot>(\<Lambda>\<langle>x, i\<rangle>. P\<cdot>x)\<cdot>(zip\<cdot>xs\<cdot>[MkI\<cdot>i..])))"
+    if "\<forall>j\<ge>i. f\<cdot>(MkI\<cdot>j) = g\<cdot>(MkI\<cdot>j)"
+    for f g :: "Integer \<rightarrow> 'a"
       and P :: "'a \<rightarrow> tr"
       and i xs
-    assume "\<forall>j\<ge>i. f\<cdot>(MkI\<cdot>j) = g\<cdot>(MkI\<cdot>j)"
-    then have "map\<cdot>f\<cdot>(map\<cdot>snd\<cdot>(filter\<cdot>(\<Lambda>\<langle>x, i\<rangle>. P\<cdot>x)\<cdot>(zip\<cdot>xs\<cdot>[MkI\<cdot>i..])))
-      = map\<cdot>g\<cdot>(map\<cdot>snd\<cdot>(filter\<cdot>(\<Lambda>\<langle>x, i\<rangle>. P\<cdot>x)\<cdot>(zip\<cdot>xs\<cdot>[MkI\<cdot>i..])))"
-      by (induct xs arbitrary: i, simp_all, subst (1 2) intsFrom.simps)
-        (rename_tac a b c, case_tac "P\<cdot>a", simp_all add: one_Integer_def)
-  } note 1 = this
-  {
-    fix a and ys :: "['a]"
-    have "\<forall>i\<ge>0. nth\<cdot>ys\<cdot>(MkI\<cdot>i) = (nth\<cdot>(a : ys) oo (+1))\<cdot>(MkI\<cdot>i)"
-      by (auto simp: one_Integer_def zero_Integer_def)
-  } note 2 = this
-  {
-    fix a P and ys xs :: "['a]"
-    have "map\<cdot>(nth\<cdot>(a : ys) oo (+1))\<cdot>(findIndices\<cdot>P\<cdot>xs)
-      = map\<cdot>(nth\<cdot>ys)\<cdot>(findIndices\<cdot>P\<cdot>xs)"
-      by (simp add: findIndices_def 1 [OF 2, simplified, of ys P xs a] zero_Integer_def)
-  } note 3 = this
+    using that
+    by (induct xs arbitrary: i, simp_all, subst (1 2) intsFrom.simps)
+      (rename_tac a b c, case_tac "P\<cdot>a", simp_all add: one_Integer_def)
+  have 2: "\<forall>i\<ge>0. nth\<cdot>ys\<cdot>(MkI\<cdot>i) = (nth\<cdot>(a : ys) oo (+1))\<cdot>(MkI\<cdot>i)"
+    for a and ys :: "['a]"
+    by (auto simp: one_Integer_def zero_Integer_def)
+  have 3: "map\<cdot>(nth\<cdot>(a : ys) oo (+1))\<cdot>(findIndices\<cdot>P\<cdot>xs)
+    = map\<cdot>(nth\<cdot>ys)\<cdot>(findIndices\<cdot>P\<cdot>xs)"
+    for a P and ys xs :: "['a]"
+    by (simp add: findIndices_def 1 [OF 2, simplified, of ys P xs a] zero_Integer_def)
   show ?thesis
     by (induct xs, simp_all, simp add: findIndices_def, simp add: findIndices_def)
        (rename_tac a b, case_tac "P\<cdot>a", simp add: findIndices_def, simp_all add: 3)
 qed
 
 abbreviation cfun_image :: "('a \<rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b set" (infixr "`\<cdot>" 90) where
   "f `\<cdot> A \<equiv> Rep_cfun f ` A"
 
 lemma set_map:
   "set (map\<cdot>f\<cdot>xs) = f `\<cdot> set xs" (is "?l = ?r")
 proof
-  { fix a assume "listmem a xs" then have "listmem (f\<cdot>a) (map\<cdot>f\<cdot>xs)"
-      by (induct) simp_all }
+  have "listmem (f\<cdot>a) (map\<cdot>f\<cdot>xs)" if "listmem a xs" for a
+    using that by (induct) simp_all
   then show "?r \<subseteq> ?l" by (auto simp: set_def)
 next
-  { fix a assume "listmem a (map\<cdot>f\<cdot>xs)"
-    then have "\<exists>b. a = f\<cdot>b \<and> listmem b xs"
+  have "\<exists>b. a = f\<cdot>b \<and> listmem b xs" if "listmem a (map\<cdot>f\<cdot>xs)" for a
+    using that
     by (induct a "map\<cdot>f\<cdot>xs" arbitrary: xs)
-       (rename_tac xsa, case_tac xsa, auto)+ }
+       (rename_tac xsa, case_tac xsa, auto)+
   then show "?l \<subseteq> ?r" unfolding set_def by auto
 qed
 
 
 subsection \<open>@{const reverse} and @{const reverse} induction\<close>
 
 text \<open>Alternative simplification rules for @{const reverse} (easier
 to use for equational reasoning):\<close>
 lemma reverse_Nil [simp]:
   "reverse\<cdot>[] = []"
   by (simp add: reverse.simps)
 
 lemma reverse_singleton [simp]:
   "reverse\<cdot>[x] = [x]"
   by (simp add: reverse.simps)
 
 lemma reverse_strict [simp]:
   "reverse\<cdot>\<bottom> = \<bottom>"
   by (simp add: reverse.simps)
 
 lemma foldl_flip_Cons_append:
   "foldl\<cdot>(flip\<cdot>(:))\<cdot>ys\<cdot>xs = foldl\<cdot>(flip\<cdot>(:))\<cdot>[]\<cdot>xs ++ ys"
 proof (induct xs arbitrary: ys)
   case (Cons x xs)
   show ?case by simp (metis (no_types) Cons append.simps append_assoc)
 qed simp+
 
 lemma reverse_Cons [simp]:
   "reverse\<cdot>(x:xs) = reverse\<cdot>xs ++ [x]"
   by (simp add: reverse.simps)
      (subst foldl_flip_Cons_append, rule refl)
 
 lemma reverse_append_below:
   "reverse\<cdot>(xs ++ ys) \<sqsubseteq> reverse\<cdot>ys ++ reverse\<cdot>xs"
   apply (induction xs)
      apply (simp del: append_assoc add: append_assoc [symmetric])+
   apply (blast intro: monofun_cfun append_assoc)
   done
 
 lemma reverse_reverse_below:
   "reverse\<cdot>(reverse\<cdot>xs) \<sqsubseteq> xs"
 proof (induction xs)
   case (Cons x xs)
   have "reverse\<cdot>(reverse\<cdot>(x:xs)) = reverse\<cdot>(reverse\<cdot>xs ++ [x])" by simp
   also have "\<dots> \<sqsubseteq> reverse\<cdot>[x] ++ reverse\<cdot>(reverse\<cdot>xs)" by (rule reverse_append_below)
   also have "\<dots> = x : reverse\<cdot>(reverse\<cdot>xs)" by simp
   also have "\<dots> \<sqsubseteq> x : xs" by (simp add: Cons)
   finally show ?case .
 qed simp+
 
 lemma reverse_append [simp]:
   assumes "finite_list xs"
   shows "reverse\<cdot>(xs ++ ys) = reverse\<cdot>ys ++ reverse\<cdot>xs"
   using assms by (induct xs) simp+
 
 lemma reverse_spine_strict:
   "\<not> finite_list xs \<Longrightarrow> reverse\<cdot>xs = \<bottom>"
   by (auto simp add: reverse.simps foldl_spine_strict)
 
 lemma reverse_finite [simp]:
   assumes "finite_list xs" shows "finite_list (reverse\<cdot>xs)"
   using assms by (induct xs) simp+
 
 lemma reverse_reverse [simp]:
   assumes "finite_list xs" shows "reverse\<cdot>(reverse\<cdot>xs) = xs"
   using assms by (induct xs) simp+
 
 lemma reverse_induct [consumes 1, case_names Nil snoc]:
   "\<lbrakk>finite_list xs; P []; \<And>x xs . finite_list xs \<Longrightarrow> P xs \<Longrightarrow> P (xs ++ [x])\<rbrakk> \<Longrightarrow> P xs"
   apply (subst reverse_reverse [symmetric])
    apply assumption
   apply (rule finite_list.induct[where x = "reverse\<cdot>xs"])
     apply simp+
   done
 
 lemma length_plus_not_0:
   "le\<cdot>1\<cdot>n = TT \<Longrightarrow> le\<cdot>(length\<cdot>xs + n)\<cdot>0 = TT \<Longrightarrow> False"
 proof (induct xs arbitrary: n)
   case Nil then show ?case
     by auto (metis Ord_linear_class.le_trans dist_eq_tr(3) le_Integer_numeral_simps(3))
 next
   case (Cons x xs)
   from Cons(1) [of "n + 1"] show ?case
     using Cons(2-) by (auto simp: ac_simps dest: le_plus_1)
 qed simp+
 
 lemma take_length_plus_1:
   "length\<cdot>xs \<noteq> \<bottom> \<Longrightarrow> take\<cdot>(length\<cdot>xs + 1)\<cdot>(y:ys) = y : take\<cdot>(length\<cdot>xs)\<cdot>ys"
   by (subst take.simps, cases "le\<cdot>(length\<cdot>xs + 1)\<cdot>0")
      (auto, metis (no_types) length_plus_not_0 le_Integer_numeral_simps(4))
 
 lemma le_length_plus:
   "length\<cdot>xs \<noteq> \<bottom> \<Longrightarrow> n \<noteq> \<bottom> \<Longrightarrow> le\<cdot>n\<cdot>(length\<cdot>xs + n) = TT"
 proof (induct xs arbitrary: n)
   case (Cons x xs)
   then have "le\<cdot>(n + 1)\<cdot>(length\<cdot>xs + (n + 1)) = TT" by simp
   moreover have "le\<cdot>n\<cdot>(n + 1) = TT" using \<open>n \<noteq> \<bottom>\<close> by (metis le_plus_1 le_refl_Integer)
   ultimately have "le\<cdot>n\<cdot>(length\<cdot>xs + (n + 1)) = TT" by (blast dest: le_trans)
   then show ?case by (simp add: ac_simps)
 qed simp+
 
 lemma eq_take_length_isPrefixOf:
   "eq\<cdot>xs\<cdot>(take\<cdot>(length\<cdot>xs)\<cdot>ys) \<sqsubseteq> isPrefixOf\<cdot>xs\<cdot>ys"
 proof (induct xs arbitrary: ys)
-  case (Cons x xs)
-  note IH = this
+  case IH: (Cons x xs)
   show ?case
   proof (cases "length\<cdot>xs = \<bottom>")
     case True then show ?thesis by simp
   next
     case False
     show ?thesis
     proof (cases ys)
       case bottom
       then show ?thesis using False
         using le_length_plus [of xs 1] by simp
     next
       case Nil then show ?thesis using False by simp
     next
       case (Cons z zs)
       then show ?thesis
         using False and IH [of zs]
         by (simp add: take_length_plus_1 monofun_cfun_arg)
     qed
   qed
 qed simp+
 
 end
diff --git a/thys/HOLCF-Prelude/Data_Maybe.thy b/thys/HOLCF-Prelude/Data_Maybe.thy
--- a/thys/HOLCF-Prelude/Data_Maybe.thy
+++ b/thys/HOLCF-Prelude/Data_Maybe.thy
@@ -1,147 +1,149 @@
 section \<open>Data: Maybe\<close>
 
 theory Data_Maybe
   imports
     Type_Classes
     Data_Function
     Data_List
     Data_Bool
 begin
 
 domain 'a Maybe = Nothing | Just (lazy "'a")
 
 abbreviation maybe :: "'b \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'a Maybe \<rightarrow> 'b" where
   "maybe \<equiv> Maybe_case"
 
 fixrec isJust :: "'a Maybe \<rightarrow> tr" where
   "isJust\<cdot>(Just\<cdot>a) = TT" |
   "isJust\<cdot>Nothing = FF"
 
 fixrec isNothing :: "'a Maybe \<rightarrow> tr" where
   "isNothing = neg oo isJust"
 
 fixrec fromJust :: "'a Maybe \<rightarrow> 'a" where
   "fromJust\<cdot>(Just\<cdot>a) = a" |
   "fromJust\<cdot>Nothing = \<bottom>"
 
 fixrec fromMaybe :: "'a \<rightarrow> 'a Maybe \<rightarrow> 'a" where
   "fromMaybe\<cdot>d\<cdot>Nothing = d" |
   "fromMaybe\<cdot>d\<cdot>(Just\<cdot>a) = a"
 
 fixrec maybeToList :: "'a Maybe \<rightarrow> ['a]" where
   "maybeToList\<cdot>Nothing = []" |
   "maybeToList\<cdot>(Just\<cdot>a) = [a]"
 
 fixrec listToMaybe :: "['a] \<rightarrow> 'a Maybe" where
   "listToMaybe\<cdot>[] = Nothing" |
   "listToMaybe\<cdot>(a:_) = Just\<cdot>a"
 
 (* FIXME: The Prelude definition uses list comps, which are too advanced for our syntax *)
 fixrec catMaybes :: "['a Maybe] \<rightarrow> ['a]" where
   "catMaybes = concatMap\<cdot>maybeToList"
 
 fixrec mapMaybe :: "('a \<rightarrow> 'b Maybe) \<rightarrow> ['a] \<rightarrow> ['b]" where
   "mapMaybe\<cdot>f = catMaybes oo map\<cdot>f"
 
 instantiation Maybe :: (Eq) Eq_strict
 begin
 
 definition
   "eq = maybe\<cdot>(maybe\<cdot>TT\<cdot>(\<Lambda> y. FF))\<cdot>(\<Lambda> x. maybe\<cdot>FF\<cdot>(\<Lambda> y. eq\<cdot>x\<cdot>y))"
 
 instance proof
   fix x :: "'a Maybe"
   show "eq\<cdot>x\<cdot>\<bottom> = \<bottom>"
     unfolding eq_Maybe_def by (cases x) simp_all
   show "eq\<cdot>\<bottom>\<cdot>x = \<bottom>"
     unfolding eq_Maybe_def by simp
 qed
 
 end
 
 lemma eq_Maybe_simps [simp]:
   "eq\<cdot>Nothing\<cdot>Nothing = TT"
   "eq\<cdot>Nothing\<cdot>(Just\<cdot>y) = FF"
   "eq\<cdot>(Just\<cdot>x)\<cdot>Nothing = FF"
   "eq\<cdot>(Just\<cdot>x)\<cdot>(Just\<cdot>y) = eq\<cdot>x\<cdot>y"
   unfolding eq_Maybe_def by simp_all
 
 instance Maybe :: (Eq_sym) Eq_sym
 proof
   fix x y :: "'a Maybe"
   show "eq\<cdot>x\<cdot>y = eq\<cdot>y\<cdot>x"
     by (cases x, simp, cases y, simp, simp, simp,
         cases y, simp, simp, simp add: eq_sym)
 qed
 
 instance Maybe :: (Eq_equiv) Eq_equiv
 proof
   fix x y z :: "'a Maybe"
   show "eq\<cdot>x\<cdot>x \<noteq> FF"
     by (cases x, simp_all)
   assume "eq\<cdot>x\<cdot>y = TT" and "eq\<cdot>y\<cdot>z = TT" then show "eq\<cdot>x\<cdot>z = TT"
     by (cases x, simp, cases y, simp, cases z, simp, simp, simp, simp,
         cases y, simp, simp, cases z, simp, simp, simp, fast elim: eq_trans)
 qed
 
 instance Maybe :: (Eq_eq) Eq_eq
 proof
   fix x y :: "'a Maybe"
   show "eq\<cdot>x\<cdot>x \<noteq> FF"
     by (cases x, simp_all)
   assume "eq\<cdot>x\<cdot>y = TT" then show "x = y"
     by (cases x, simp, cases y, simp, simp, simp,
         cases y, simp, simp, simp, fast)
 qed
 
 instantiation Maybe :: (Ord) Ord_strict
 begin
 
 definition
   "compare = maybe\<cdot>(maybe\<cdot>EQ\<cdot>(\<Lambda> y. LT))\<cdot>(\<Lambda> x. maybe\<cdot>GT\<cdot>(\<Lambda> y. compare\<cdot>x\<cdot>y))"
 
 instance proof
   fix x :: "'a Maybe"
   show "compare\<cdot>x\<cdot>\<bottom> = \<bottom>"
     unfolding compare_Maybe_def by (cases x) simp_all
   show "compare\<cdot>\<bottom>\<cdot>x = \<bottom>"
     unfolding compare_Maybe_def by simp
 qed
 
 end
 
 lemma compare_Maybe_simps [simp]:
   "compare\<cdot>Nothing\<cdot>Nothing = EQ"
   "compare\<cdot>Nothing\<cdot>(Just\<cdot>y) = LT"
   "compare\<cdot>(Just\<cdot>x)\<cdot>Nothing = GT"
   "compare\<cdot>(Just\<cdot>x)\<cdot>(Just\<cdot>y) = compare\<cdot>x\<cdot>y"
   unfolding compare_Maybe_def by simp_all
 
 instance Maybe :: (Ord_linear) Ord_linear
 proof
   fix x y z :: "'a Maybe"
   show "eq\<cdot>x\<cdot>y = is_EQ\<cdot>(compare\<cdot>x\<cdot>y)"
     by (cases x, simp, cases y, simp, simp, simp,
         cases y, simp, simp, simp add: eq_conv_compare)
   show "oppOrdering\<cdot>(compare\<cdot>x\<cdot>y) = compare\<cdot>y\<cdot>x"
     by (cases x, simp, (cases y, simp, simp, simp)+)
   show "compare\<cdot>x\<cdot>x \<sqsubseteq> EQ"
     by (cases x) simp_all
-  { assume "compare\<cdot>x\<cdot>y = EQ" then show "x = y"
-      by (cases x, simp, cases y, simp, simp, simp,
-          cases y, simp, simp, simp) (erule compare_EQ_dest) }
-  { assume "compare\<cdot>x\<cdot>y = LT" and "compare\<cdot>y\<cdot>z = LT" then show "compare\<cdot>x\<cdot>z = LT"
-      apply (cases x, simp)
-       apply (cases y, simp, simp)
-       apply (cases z, simp, simp, simp)
-      apply (cases y, simp, simp)
-      apply (cases z, simp, simp)
-      apply (auto elim: compare_LT_trans)
-      done }
+  show "x = y" if "compare\<cdot>x\<cdot>y = EQ"
+    using that
+    by (cases x, simp, cases y, simp, simp, simp,
+        cases y, simp, simp, simp) (erule compare_EQ_dest)
+  show "compare\<cdot>x\<cdot>z = LT" if "compare\<cdot>x\<cdot>y = LT" and "compare\<cdot>y\<cdot>z = LT"
+    using that
+    apply (cases x, simp)
+     apply (cases y, simp, simp)
+     apply (cases z, simp, simp, simp)
+    apply (cases y, simp, simp)
+    apply (cases z, simp, simp)
+    apply (auto elim: compare_LT_trans)
+    done
 qed
 
 lemma isJust_strict [simp]: "isJust\<cdot>\<bottom>  = \<bottom>" by (fixrec_simp)
 lemma fromMaybe_strict [simp]: "fromMaybe\<cdot>x\<cdot>\<bottom>  = \<bottom>" by (fixrec_simp)
 lemma maybeToList_strict [simp]: "maybeToList\<cdot>\<bottom>  = \<bottom>" by (fixrec_simp)
 
 end
diff --git a/thys/HOLCF-Prelude/Data_Tuple.thy b/thys/HOLCF-Prelude/Data_Tuple.thy
--- a/thys/HOLCF-Prelude/Data_Tuple.thy
+++ b/thys/HOLCF-Prelude/Data_Tuple.thy
@@ -1,234 +1,238 @@
 section \<open>Data: Tuple\<close>
 
 theory Data_Tuple
   imports
     Type_Classes
     Data_Bool
 begin
 
 subsection \<open>Datatype definitions\<close>
 
 domain Unit ("\<langle>\<rangle>") = Unit ("\<langle>\<rangle>")
 
 domain ('a, 'b) Tuple2 ("\<langle>_, _\<rangle>") =
   Tuple2 (lazy fst :: "'a") (lazy snd :: "'b") ("\<langle>_, _\<rangle>")
 
 notation Tuple2 ("\<langle>,\<rangle>")
 
 fixrec uncurry :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> \<langle>'a, 'b\<rangle> \<rightarrow> 'c"
   where "uncurry\<cdot>f\<cdot>p = f\<cdot>(fst\<cdot>p)\<cdot>(snd\<cdot>p)"
 
 fixrec curry :: "(\<langle>'a, 'b\<rangle>  \<rightarrow> 'c) \<rightarrow> 'a \<rightarrow> 'b \<rightarrow> 'c"
   where "curry\<cdot>f\<cdot>a\<cdot>b = f\<cdot>\<langle>a, b\<rangle>"
 
 domain ('a, 'b, 'c) Tuple3 ("\<langle>_, _, _\<rangle>") =
   Tuple3 (lazy "'a") (lazy "'b") (lazy "'c") ("\<langle>_, _, _\<rangle>")
 
 notation Tuple3 ("\<langle>,,\<rangle>")
 
 subsection \<open>Type class instances\<close>
 
 instantiation Unit :: Ord_linear
 begin
 
 definition
   "eq = (\<Lambda> \<langle>\<rangle> \<langle>\<rangle>. TT)"
 
 definition
   "compare = (\<Lambda> \<langle>\<rangle> \<langle>\<rangle>. EQ)"
 
 instance
   apply standard
         apply (unfold eq_Unit_def compare_Unit_def)
         apply simp
        apply (rename_tac x, case_tac x, simp, simp)
       apply (rename_tac x y, case_tac x, simp, case_tac y, simp, simp)
      apply (rename_tac x y, case_tac x, case_tac y, simp, simp, case_tac y, simp, simp)
     apply (rename_tac x y, case_tac x, simp, case_tac y, simp, simp)
    apply (rename_tac x, case_tac x, simp, simp)
   apply (rename_tac x y z, case_tac x, simp, case_tac y, simp, case_tac z, simp, simp)
   done
 
 end
 
 instantiation Tuple2 :: (Eq, Eq) Eq_strict
 begin
 
 definition
   "eq = (\<Lambda> \<langle>x1, y1\<rangle> \<langle>x2, y2\<rangle>. eq\<cdot>x1\<cdot>x2 andalso eq\<cdot>y1\<cdot>y2)"
 
 instance proof
   fix x :: "\<langle>'a, 'b\<rangle>"
   show "eq\<cdot>x\<cdot>\<bottom> = \<bottom>"
     unfolding eq_Tuple2_def by (cases x, simp_all)
   show "eq\<cdot>\<bottom>\<cdot>x = \<bottom>"
     unfolding eq_Tuple2_def by simp
 qed
 
 end
 
 lemma eq_Tuple2_simps [simp]:
   "eq\<cdot>\<langle>x1, y1\<rangle>\<cdot>\<langle>x2, y2\<rangle> = (eq\<cdot>x1\<cdot>x2 andalso eq\<cdot>y1\<cdot>y2)"
   unfolding eq_Tuple2_def by simp
 
 instance Tuple2 :: (Eq_sym, Eq_sym) Eq_sym
 proof
   fix x y :: "\<langle>'a, 'b\<rangle>"
   show "eq\<cdot>x\<cdot>y = eq\<cdot>y\<cdot>x"
     unfolding eq_Tuple2_def
     by (cases x, simp, (cases y, simp, simp add: eq_sym)+)
 qed
 
 instance Tuple2 :: (Eq_equiv, Eq_equiv) Eq_equiv
 proof
   fix x y z :: "\<langle>'a, 'b\<rangle>"
   show "eq\<cdot>x\<cdot>x \<noteq> FF"
     by (cases x, simp_all)
-  { assume "eq\<cdot>x\<cdot>y = TT" and "eq\<cdot>y\<cdot>z = TT" then show "eq\<cdot>x\<cdot>z = TT"
-      by (cases x, simp, cases y, simp, cases z, simp, simp,
-          fast intro: eq_trans) }
+  show "eq\<cdot>x\<cdot>z = TT" if "eq\<cdot>x\<cdot>y = TT" and "eq\<cdot>y\<cdot>z = TT"
+    using that
+    by (cases x, simp, cases y, simp, cases z, simp, simp,
+        fast intro: eq_trans)
 qed
 
 instance Tuple2 :: (Eq_eq, Eq_eq) Eq_eq
 proof
   fix x y :: "\<langle>'a, 'b\<rangle>"
   show "eq\<cdot>x\<cdot>x \<noteq> FF"
     by (cases x, simp_all)
-  { assume "eq\<cdot>x\<cdot>y = TT" then show "x = y"
-      by (cases x, simp, cases y, simp, simp, fast) }
+  show "x = y" if "eq\<cdot>x\<cdot>y = TT"
+    using that by (cases x, simp, cases y, simp, simp, fast)
 qed
 
 instantiation Tuple2 :: (Ord, Ord) Ord_strict
 begin
 
 definition
   "compare = (\<Lambda> \<langle>x1, y1\<rangle> \<langle>x2, y2\<rangle>.
     thenOrdering\<cdot>(compare\<cdot>x1\<cdot>x2)\<cdot>(compare\<cdot>y1\<cdot>y2))"
 
 instance
   by standard (simp add: compare_Tuple2_def,
       rename_tac x, case_tac x, simp_all add: compare_Tuple2_def)
 
 end
 
 lemma compare_Tuple2_simps [simp]:
   "compare\<cdot>\<langle>x1, y1\<rangle>\<cdot>\<langle>x2, y2\<rangle> = thenOrdering\<cdot>(compare\<cdot>x1\<cdot>x2)\<cdot>(compare\<cdot>y1\<cdot>y2)"
   unfolding compare_Tuple2_def by simp
 
 instance Tuple2 :: (Ord_linear, Ord_linear) Ord_linear
 proof
   fix x y z :: "\<langle>'a, 'b\<rangle>"
   show "eq\<cdot>x\<cdot>y = is_EQ\<cdot>(compare\<cdot>x\<cdot>y)"
     by (cases x, simp, cases y, simp, simp add: eq_conv_compare)
   show "oppOrdering\<cdot>(compare\<cdot>x\<cdot>y) = compare\<cdot>y\<cdot>x"
     by (cases x, simp, cases y, simp, simp add: oppOrdering_thenOrdering)
-  { assume "compare\<cdot>x\<cdot>y = EQ" then show "x = y"
-      by (cases x, simp, cases y, simp, auto elim: compare_EQ_dest) }
-  { assume "compare\<cdot>x\<cdot>y = LT" and "compare\<cdot>y\<cdot>z = LT" then show "compare\<cdot>x\<cdot>z = LT"
-      apply (cases x, simp, cases y, simp, cases z, simp, simp)
-      apply (elim disjE conjE)
-         apply (fast elim!: compare_LT_trans)
-        apply (fast dest: compare_EQ_dest)
-       apply (fast dest: compare_EQ_dest)
-      apply (drule compare_EQ_dest)
-      apply (fast elim!: compare_LT_trans)
-      done }
+  show "x = y" if "compare\<cdot>x\<cdot>y = EQ"
+    using that by (cases x, simp, cases y, simp, auto elim: compare_EQ_dest)
+  show "compare\<cdot>x\<cdot>z = LT" if "compare\<cdot>x\<cdot>y = LT" and "compare\<cdot>y\<cdot>z = LT"
+    using that
+    apply (cases x, simp, cases y, simp, cases z, simp, simp)
+    apply (elim disjE conjE)
+       apply (fast elim!: compare_LT_trans)
+      apply (fast dest: compare_EQ_dest)
+     apply (fast dest: compare_EQ_dest)
+    apply (drule compare_EQ_dest)
+    apply (fast elim!: compare_LT_trans)
+    done
   show "compare\<cdot>x\<cdot>x \<sqsubseteq> EQ"
     by (cases x, simp_all)
 qed
 
 instantiation Tuple3 :: (Eq, Eq, Eq) Eq_strict
 begin
 
 definition
   "eq = (\<Lambda> \<langle>x1, y1, z1\<rangle> \<langle>x2, y2, z2\<rangle>.
     eq\<cdot>x1\<cdot>x2 andalso eq\<cdot>y1\<cdot>y2 andalso eq\<cdot>z1\<cdot>z2)"
 
 instance proof
   fix x :: "\<langle>'a, 'b, 'c\<rangle>"
   show "eq\<cdot>x\<cdot>\<bottom> = \<bottom>"
     unfolding eq_Tuple3_def by (cases x, simp_all)
   show "eq\<cdot>\<bottom>\<cdot>x = \<bottom>"
     unfolding eq_Tuple3_def by simp
 qed
 
 end
 
 lemma eq_Tuple3_simps [simp]:
   "eq\<cdot>\<langle>x1, y1, z1\<rangle>\<cdot>\<langle>x2, y2, z2\<rangle> = (eq\<cdot>x1\<cdot>x2 andalso eq\<cdot>y1\<cdot>y2 andalso eq\<cdot>z1\<cdot>z2)"
   unfolding eq_Tuple3_def by simp
 
 instance Tuple3 :: (Eq_sym, Eq_sym, Eq_sym) Eq_sym
 proof
   fix x y :: "\<langle>'a, 'b, 'c\<rangle>"
   show "eq\<cdot>x\<cdot>y = eq\<cdot>y\<cdot>x"
     unfolding eq_Tuple3_def
     by (cases x, simp, (cases y, simp, simp add: eq_sym)+)
 qed
 
 instance Tuple3 :: (Eq_equiv, Eq_equiv, Eq_equiv) Eq_equiv
 proof
   fix x y z :: "\<langle>'a, 'b, 'c\<rangle>"
   show "eq\<cdot>x\<cdot>x \<noteq> FF"
     by (cases x, simp_all)
-  { assume "eq\<cdot>x\<cdot>y = TT" and "eq\<cdot>y\<cdot>z = TT" then show "eq\<cdot>x\<cdot>z = TT"
-      by (cases x, simp, cases y, simp, cases z, simp, simp,
-          fast intro: eq_trans) }
+  show "eq\<cdot>x\<cdot>z = TT" if "eq\<cdot>x\<cdot>y = TT" and "eq\<cdot>y\<cdot>z = TT"
+    using that
+    by (cases x, simp, cases y, simp, cases z, simp, simp,
+        fast intro: eq_trans)
 qed
 
 instance Tuple3 :: (Eq_eq, Eq_eq, Eq_eq) Eq_eq
 proof
   fix x y :: "\<langle>'a, 'b, 'c\<rangle>"
   show "eq\<cdot>x\<cdot>x \<noteq> FF"
     by (cases x, simp_all)
-  { assume "eq\<cdot>x\<cdot>y = TT" then show "x = y"
-      by (cases x, simp, cases y, simp, simp, fast) }
+  show "x = y" if "eq\<cdot>x\<cdot>y = TT"
+    using that by (cases x, simp, cases y, simp, simp, fast)
 qed
 
 instantiation Tuple3 :: (Ord, Ord, Ord) Ord_strict
 begin
 
 definition
   "compare = (\<Lambda> \<langle>x1, y1, z1\<rangle> \<langle>x2, y2, z2\<rangle>.
     thenOrdering\<cdot>(compare\<cdot>x1\<cdot>x2)\<cdot>(thenOrdering\<cdot>(compare\<cdot>y1\<cdot>y2)\<cdot>(compare\<cdot>z1\<cdot>z2)))"
 
 instance
   by standard (simp add: compare_Tuple3_def,
     rename_tac x, case_tac x, simp_all add: compare_Tuple3_def)
 
 end
 
 lemma compare_Tuple3_simps [simp]:
   "compare\<cdot>\<langle>x1, y1, z1\<rangle>\<cdot>\<langle>x2, y2, z2\<rangle> =
     thenOrdering\<cdot>(compare\<cdot>x1\<cdot>x2)\<cdot>
       (thenOrdering\<cdot>(compare\<cdot>y1\<cdot>y2)\<cdot>(compare\<cdot>z1\<cdot>z2))"
   unfolding compare_Tuple3_def by simp
 
 instance Tuple3 :: (Ord_linear, Ord_linear, Ord_linear) Ord_linear
 proof
   fix x y z :: "\<langle>'a, 'b, 'c\<rangle>"
   show "eq\<cdot>x\<cdot>y = is_EQ\<cdot>(compare\<cdot>x\<cdot>y)"
     by (cases x, simp, cases y, simp, simp add: eq_conv_compare)
   show "oppOrdering\<cdot>(compare\<cdot>x\<cdot>y) = compare\<cdot>y\<cdot>x"
     by (cases x, simp, cases y, simp, simp add: oppOrdering_thenOrdering)
-  { assume "compare\<cdot>x\<cdot>y = EQ" then show "x = y"
-      by (cases x, simp, cases y, simp, auto elim: compare_EQ_dest) }
-  { assume "compare\<cdot>x\<cdot>y = LT" and "compare\<cdot>y\<cdot>z = LT" then show "compare\<cdot>x\<cdot>z = LT"
-      apply (cases x, simp, cases y, simp, cases z, simp, simp)
-      apply (elim disjE conjE)
-              apply (fast elim!: compare_LT_trans)
-             apply (fast dest: compare_EQ_dest)
-            apply (fast dest: compare_EQ_dest)
+  show "x = y" if "compare\<cdot>x\<cdot>y = EQ"
+    using that by (cases x, simp, cases y, simp, auto elim: compare_EQ_dest)
+  show "compare\<cdot>x\<cdot>z = LT" if "compare\<cdot>x\<cdot>y = LT" and "compare\<cdot>y\<cdot>z = LT"
+    using that
+    apply (cases x, simp, cases y, simp, cases z, simp, simp)
+    apply (elim disjE conjE)
+            apply (fast elim!: compare_LT_trans)
            apply (fast dest: compare_EQ_dest)
           apply (fast dest: compare_EQ_dest)
-         apply (drule compare_EQ_dest)
-         apply (fast elim!: compare_LT_trans)
+         apply (fast dest: compare_EQ_dest)
         apply (fast dest: compare_EQ_dest)
-       apply (fast dest: compare_EQ_dest)
-      apply (fast dest: compare_EQ_dest elim!: compare_LT_trans)
-      done }
+       apply (drule compare_EQ_dest)
+       apply (fast elim!: compare_LT_trans)
+      apply (fast dest: compare_EQ_dest)
+     apply (fast dest: compare_EQ_dest)
+    apply (fast dest: compare_EQ_dest elim!: compare_LT_trans)
+    done
   show "compare\<cdot>x\<cdot>x \<sqsubseteq> EQ"
     by (cases x, simp_all)
 qed
 
 end
diff --git a/thys/HOLCF-Prelude/Definedness.thy b/thys/HOLCF-Prelude/Definedness.thy
--- a/thys/HOLCF-Prelude/Definedness.thy
+++ b/thys/HOLCF-Prelude/Definedness.thy
@@ -1,224 +1,221 @@
 section \<open>Definedness\<close>
 
 theory Definedness
   imports
     Data_List
 begin
 
 text \<open>
   This is an attempt for a setup for better handling bottom, by a better
   simp setup, and less breaking the abstractions.
 \<close>
 
 definition defined :: "'a :: pcpo \<Rightarrow> bool" where
   "defined x = (x \<noteq> \<bottom>)"
 
 lemma defined_bottom [simp]: "\<not> defined \<bottom>"
   by (simp add: defined_def)
 
 lemma defined_seq [simp]: "defined x \<Longrightarrow> seq\<cdot>x\<cdot>y = y"
   by (simp add: defined_def)
 
 consts val :: "'a::type \<Rightarrow> 'b::type" ("\<lbrakk>_\<rbrakk>")
 
 text \<open>val for booleans\<close>
 
 definition val_Bool :: "tr \<Rightarrow> bool" where
   "val_Bool i = (THE j. i = Def j)"
 
 adhoc_overloading
   val val_Bool
 
 lemma defined_Bool_simps [simp]:
   "defined (Def i)"
   "defined TT"
   "defined FF"
   by (simp_all add: defined_def)
 
 lemma val_Bool_simp1 [simp]:
   "\<lbrakk>Def i\<rbrakk> = i"
   by (simp_all add: val_Bool_def TT_def FF_def)
 
 lemma val_Bool_simp2 [simp]:
   "\<lbrakk>TT\<rbrakk> = True"
   "\<lbrakk>FF\<rbrakk> = False"
   by (simp_all add: TT_def FF_def)
 
 lemma IF_simps [simp]:
   "defined b \<Longrightarrow> \<lbrakk> b \<rbrakk> \<Longrightarrow> (If b then x else y) = x"
   "defined b \<Longrightarrow> \<lbrakk> b \<rbrakk> = False \<Longrightarrow> (If b then x else y) = y"
   by (cases b, simp_all)+
 
 lemma defined_neg [simp]: "defined (neg\<cdot>b) \<longleftrightarrow> defined b"
   by (cases b, auto)
 
 lemma val_Bool_neg [simp]: "defined b \<Longrightarrow> \<lbrakk> neg \<cdot> b \<rbrakk> = (\<not> \<lbrakk> b \<rbrakk>)"
   by (cases b, auto)
 
 text \<open>val for integers\<close>
 
 definition val_Integer :: "Integer \<Rightarrow> int" where
   "val_Integer i = (THE j. i = MkI\<cdot>j)"
 
 adhoc_overloading
   val val_Integer
 
 lemma defined_Integer_simps [simp]:
   "defined (MkI\<cdot>i)"
   "defined (0::Integer)"
   "defined (1::Integer)"
   by (simp_all add: defined_def)
 
 lemma defined_numeral [simp]: "defined (numeral x :: Integer)"
   by (simp add: defined_def)
 
 lemma val_Integer_simps [simp]:
   "\<lbrakk>MkI\<cdot>i\<rbrakk> = i"
   "\<lbrakk>0\<rbrakk> = 0"
   "\<lbrakk>1\<rbrakk> = 1"
   by (simp_all add: val_Integer_def)
 
 lemma val_Integer_numeral [simp]: "\<lbrakk> numeral x :: Integer \<rbrakk> = numeral x"
   by (simp_all add: val_Integer_def)
 
 
 lemma val_Integer_to_MkI:
   "defined i \<Longrightarrow> i = (MkI \<cdot> \<lbrakk> i \<rbrakk>)"
   apply (cases i)
    apply (auto simp add: val_Integer_def defined_def)
   done
 
 lemma defined_Integer_minus [simp]: "defined i \<Longrightarrow> defined j \<Longrightarrow> defined (i - (j::Integer))"
   apply (cases i, auto)
   apply (cases j, auto)
   done
 
 lemma val_Integer_minus [simp]: "defined i \<Longrightarrow> defined j \<Longrightarrow> \<lbrakk> i - j \<rbrakk> = \<lbrakk> i \<rbrakk> - \<lbrakk> j \<rbrakk>"
   apply (cases i, auto)
   apply (cases j, auto)
   done
 
 lemma defined_Integer_plus [simp]: "defined i \<Longrightarrow> defined j \<Longrightarrow> defined (i + (j::Integer))"
   apply (cases i, auto)
   apply (cases j, auto)
   done
 
 lemma val_Integer_plus [simp]: "defined i \<Longrightarrow> defined j \<Longrightarrow> \<lbrakk> i + j \<rbrakk> = \<lbrakk> i \<rbrakk> + \<lbrakk> j \<rbrakk>"
   apply (cases i, auto)
   apply (cases j, auto)
   done
 
 lemma defined_Integer_eq [simp]: "defined (eq\<cdot>a\<cdot>b) \<longleftrightarrow> defined a \<and> defined (b::Integer)"
   apply (cases a, simp)
   apply (cases b, simp)
   apply simp
   done
 
 lemma val_Integer_eq [simp]: "defined a \<Longrightarrow> defined b \<Longrightarrow> \<lbrakk> eq\<cdot>a\<cdot>b \<rbrakk> = (\<lbrakk> a \<rbrakk> = (\<lbrakk> b \<rbrakk> :: int))"
   apply (cases a, simp)
   apply (cases b, simp)
   apply simp
   done
 
 
 text \<open>Full induction for non-negative integers\<close>
 
 lemma nonneg_full_Int_induct [consumes 1, case_names neg Suc]:
   assumes defined: "defined i"
   assumes neg: "\<And> i. defined i \<Longrightarrow> \<lbrakk>i\<rbrakk> < 0 \<Longrightarrow> P i"
   assumes step: "\<And> i. defined i \<Longrightarrow> 0 \<le> \<lbrakk>i\<rbrakk> \<Longrightarrow> (\<And> j. defined j \<Longrightarrow> \<lbrakk> j \<rbrakk> < \<lbrakk> i \<rbrakk> \<Longrightarrow> P j) \<Longrightarrow> P i"
   shows "P (i::Integer)"
 proof (cases i)
   case bottom
   then have False using defined by simp
   then show ?thesis ..
 next
   case (MkI integer)
   show ?thesis
   proof (cases integer)
     case neg
     then show ?thesis using assms(2) MkI by simp
   next
     case (nonneg nat)
     have "P (MkI\<cdot>(int nat))"
     proof(induction nat rule:full_nat_induct)
       case (1 nat)
       have "defined (MkI\<cdot>(int nat))" by simp
       moreover
       have "0 \<le> \<lbrakk> MkI\<cdot>(int nat) \<rbrakk>"  by simp
       moreover
-      { fix j::Integer
-        assume "defined j" and le: "\<lbrakk> j \<rbrakk> < \<lbrakk> MkI\<cdot>(int nat) \<rbrakk>"
-        have "P j"
-        proof(cases j)
-          case bottom with \<open>defined j\<close> show ?thesis by simp
+      have "P j" if "defined j" and le: "\<lbrakk> j \<rbrakk> < \<lbrakk> MkI\<cdot>(int nat) \<rbrakk>" for j::Integer
+      proof(cases j)
+        case bottom with \<open>defined j\<close> show ?thesis by simp
+      next
+        case (MkI integer)
+        show ?thesis
+        proof(cases integer)
+          case (neg nat)
+          have "\<lbrakk>j\<rbrakk> < 0" using neg MkI by simp
+          with \<open>defined j\<close>
+          show ?thesis by (rule assms(2))
         next
-          case (MkI integer)
-          show ?thesis
-          proof(cases integer)
-            case (neg nat)
-            have "\<lbrakk>j\<rbrakk> < 0" using neg MkI by simp
-            with \<open>defined j\<close>
-            show ?thesis by (rule assms(2))
-          next
-            case (nonneg m)
-            have "Suc m \<le> nat" using le nonneg MkI by simp
-            then have "P (MkI\<cdot>(int m))" by (metis "1.IH")
-            then show ?thesis using nonneg MkI by simp
-          qed
+          case (nonneg m)
+          have "Suc m \<le> nat" using le nonneg MkI by simp
+          then have "P (MkI\<cdot>(int m))" by (metis "1.IH")
+          then show ?thesis using nonneg MkI by simp
         qed
-      }
+      qed
       ultimately
       show ?case
         by (rule step)
     qed
     then show ?thesis using nonneg MkI by simp
   qed
 qed
 
 text \<open>Some list lemmas re-done with the new setup.\<close>
 
 lemma nth_tail: (* TODO: move *)
   "defined n \<Longrightarrow> \<lbrakk> n \<rbrakk> \<ge> 0  \<Longrightarrow> tail\<cdot>xs !! n = xs !! (1 + n)"
   apply (cases xs, simp_all)
   apply (cases n, simp)
   apply (simp add: one_Integer_def zero_Integer_def)
   done
 
 lemma nth_zipWith: (* TODO: move *)
   assumes f1 [simp]: "\<And>y. f\<cdot>\<bottom>\<cdot>y = \<bottom>"
   assumes f2 [simp]: "\<And>x. f\<cdot>x\<cdot>\<bottom> = \<bottom>"
   shows "zipWith\<cdot>f\<cdot>xs\<cdot>ys !! n = f\<cdot>(xs !! n)\<cdot>(ys !! n)"
 proof (induct xs arbitrary: ys n)
   case (Cons x xs ys n) then show ?case
     by (cases ys, simp_all split:nth_Cons_split)
 qed simp_all
 
 
 lemma nth_neg [simp]: "defined n \<Longrightarrow> \<lbrakk> n \<rbrakk> < 0 \<Longrightarrow> nth\<cdot>xs\<cdot>n = \<bottom>"
 proof (induction xs arbitrary: n)
   have [simp]: "eq\<cdot>n\<cdot>0 = TT \<longleftrightarrow> (n::Integer) = 0" for n
     by (cases n, auto simp add: zero_Integer_def)
   case (Cons a xs n)
   have "eq\<cdot>n\<cdot>0 = FF"
     using Cons.prems
     by (cases "eq\<cdot>n\<cdot>0") auto
   then show ?case
     using Cons.prems
     by (auto intro: Cons.IH)
 qed simp_all
 
 lemma nth_Cons_simp [simp]:
   "defined n \<Longrightarrow> \<lbrakk> n \<rbrakk> = 0 \<Longrightarrow> nth\<cdot>(x : xs)\<cdot>n = x"
   "defined n \<Longrightarrow> \<lbrakk> n \<rbrakk> > 0 \<Longrightarrow> nth\<cdot>(x : xs)\<cdot>n = nth\<cdot>xs\<cdot>(n - 1)"
 proof -
   assume "defined n" and "\<lbrakk> n \<rbrakk> = 0"
   then have "n = 0"  by (cases n) auto
   then show "nth\<cdot>(x : xs)\<cdot>n = x" by simp
 next
   assume "defined n" and "\<lbrakk> n \<rbrakk> > 0"
   then have "eq\<cdot>n\<cdot>0 = FF" by (cases "eq\<cdot>n\<cdot>0") auto
   then show "nth\<cdot>(x : xs)\<cdot>n = nth\<cdot>xs\<cdot>(n - 1)" by simp
 qed
 
 end
diff --git a/thys/HOLCF-Prelude/Type_Classes.thy b/thys/HOLCF-Prelude/Type_Classes.thy
--- a/thys/HOLCF-Prelude/Type_Classes.thy
+++ b/thys/HOLCF-Prelude/Type_Classes.thy
@@ -1,276 +1,279 @@
 section \<open>Type Classes\<close>
 
 theory Type_Classes
   imports HOLCF_Main
 begin
 
 
 subsection \<open>Eq class\<close>
 
 class Eq =
   fixes eq :: "'a \<rightarrow> 'a \<rightarrow> tr"
 
 text \<open>
   The Haskell type class does allow /= to be specified separately. For now, we assume
   that all modeled type classes use the default implementation, or an equivalent.
 \<close>
 fixrec neq :: "'a::Eq \<rightarrow> 'a \<rightarrow> tr" where
   "neq\<cdot>x\<cdot>y = neg\<cdot>(eq\<cdot>x\<cdot>y)"
 
 class Eq_strict = Eq +
   assumes eq_strict [simp]:
     "eq\<cdot>x\<cdot>\<bottom> = \<bottom>"
     "eq\<cdot>\<bottom>\<cdot>y = \<bottom>"
 
 class Eq_sym = Eq_strict +
   assumes eq_sym: "eq\<cdot>x\<cdot>y = eq\<cdot>y\<cdot>x"
 
 class Eq_equiv = Eq_sym +
   assumes eq_self_neq_FF [simp]: "eq\<cdot>x\<cdot>x \<noteq> FF"
     and eq_trans: "eq\<cdot>x\<cdot>y = TT \<Longrightarrow> eq\<cdot>y\<cdot>z = TT \<Longrightarrow> eq\<cdot>x\<cdot>z = TT"
 begin
 
 lemma eq_refl: "eq\<cdot>x\<cdot>x \<noteq> \<bottom> \<Longrightarrow> eq\<cdot>x\<cdot>x = TT"
   by (cases "eq\<cdot>x\<cdot>x") simp+
 
 end
 
 class Eq_eq = Eq_sym +
   assumes eq_self_neq_FF': "eq\<cdot>x\<cdot>x \<noteq> FF"
     and eq_TT_dest: "eq\<cdot>x\<cdot>y = TT \<Longrightarrow> x = y"
 begin
 
 subclass Eq_equiv
   by standard (auto simp: eq_self_neq_FF' dest: eq_TT_dest)
 
 lemma eqD [dest]:
   "eq\<cdot>x\<cdot>y = TT \<Longrightarrow> x = y"
   "eq\<cdot>x\<cdot>y = FF \<Longrightarrow> x \<noteq> y"
   by (auto elim: eq_TT_dest)
 
 end
 
 subsubsection \<open>Class instances\<close>
 
 instantiation lift :: (countable) Eq_eq
 begin
 
 definition "eq \<equiv> (\<Lambda>(Def x) (Def y). Def (x = y))"
 
 instance
   by standard (auto simp: eq_lift_def flift1_def split: lift.splits)
 
 end
 
 lemma eq_ONE_ONE [simp]: "eq\<cdot>ONE\<cdot>ONE = TT"
   unfolding ONE_def eq_lift_def by simp
 
 
 subsection \<open>Ord class\<close>
 
 domain Ordering = LT | EQ | GT
 
 definition oppOrdering :: "Ordering \<rightarrow> Ordering" where
   "oppOrdering = (\<Lambda> x. case x of LT \<Rightarrow> GT | EQ \<Rightarrow> EQ | GT \<Rightarrow> LT)"
 
 lemma oppOrdering_simps [simp]:
   "oppOrdering\<cdot>LT = GT"
   "oppOrdering\<cdot>EQ = EQ"
   "oppOrdering\<cdot>GT = LT"
   "oppOrdering\<cdot>\<bottom> = \<bottom>"
   unfolding oppOrdering_def by simp_all
 
 class Ord = Eq +
   fixes compare :: "'a \<rightarrow> 'a \<rightarrow> Ordering"
 begin
 
 definition lt :: "'a \<rightarrow> 'a \<rightarrow> tr" where
   "lt = (\<Lambda> x y. case compare\<cdot>x\<cdot>y of LT \<Rightarrow> TT | EQ \<Rightarrow> FF | GT \<Rightarrow> FF)"
 
 definition le :: "'a \<rightarrow> 'a \<rightarrow> tr" where
   "le = (\<Lambda> x y. case compare\<cdot>x\<cdot>y of LT \<Rightarrow> TT | EQ \<Rightarrow> TT | GT \<Rightarrow> FF)"
 
 lemma lt_eq_TT_iff: "lt\<cdot>x\<cdot>y = TT \<longleftrightarrow> compare\<cdot>x\<cdot>y = LT"
   by (cases "compare\<cdot>x\<cdot>y") (simp add: lt_def)+
 
 end
 
 class Ord_strict = Ord +
   assumes compare_strict [simp]:
     "compare\<cdot>\<bottom>\<cdot>y = \<bottom>"
     "compare\<cdot>x\<cdot>\<bottom> = \<bottom>"
 begin
 
 lemma lt_strict [simp]:
   shows "lt\<cdot>\<bottom>\<cdot>x = \<bottom>"
     and "lt\<cdot>x\<cdot>\<bottom> = \<bottom>"
   by (simp add: lt_def)+
 
 lemma le_strict [simp]:
   shows "le\<cdot>\<bottom>\<cdot>x = \<bottom>"
     and "le\<cdot>x\<cdot>\<bottom> = \<bottom>"
   by (simp add: le_def)+
 
 end
 
 text \<open>TODO: It might make sense to have a class for preorders too,
 analogous to class \<open>eq_equiv\<close>.\<close>
 
 class Ord_linear = Ord_strict +
   assumes eq_conv_compare: "eq\<cdot>x\<cdot>y = is_EQ\<cdot>(compare\<cdot>x\<cdot>y)"
     and oppOrdering_compare [simp]:
     "oppOrdering\<cdot>(compare\<cdot>x\<cdot>y) = compare\<cdot>y\<cdot>x"
     and compare_EQ_dest: "compare\<cdot>x\<cdot>y = EQ \<Longrightarrow> x = y"
     and compare_self_below_EQ: "compare\<cdot>x\<cdot>x \<sqsubseteq> EQ"
     and compare_LT_trans:
     "compare\<cdot>x\<cdot>y = LT \<Longrightarrow> compare\<cdot>y\<cdot>z = LT \<Longrightarrow> compare\<cdot>x\<cdot>z = LT"
   (*BH: Is this set of axioms complete?*)
   (*CS: How about totality of the order?*)
 begin
 
 lemma eq_TT_dest: "eq\<cdot>x\<cdot>y = TT \<Longrightarrow> x = y"
   by (cases "compare\<cdot>x\<cdot>y") (auto dest: compare_EQ_dest simp: eq_conv_compare)+
 
 lemma le_iff_lt_or_eq:
   "le\<cdot>x\<cdot>y = TT \<longleftrightarrow> lt\<cdot>x\<cdot>y = TT \<or> eq\<cdot>x\<cdot>y = TT"
   by (cases "compare\<cdot>x\<cdot>y") (simp add: le_def lt_def eq_conv_compare)+
 
 lemma compare_sym:
   "compare\<cdot>x\<cdot>y = (case compare\<cdot>y\<cdot>x of LT \<Rightarrow> GT | EQ \<Rightarrow> EQ | GT \<Rightarrow> LT)"
   by (subst oppOrdering_compare [symmetric]) (simp add: oppOrdering_def)
 
 lemma compare_self_neq_LT [simp]: "compare\<cdot>x\<cdot>x \<noteq> LT"
   using compare_self_below_EQ [of x] by clarsimp
 
 lemma compare_self_neq_GT [simp]: "compare\<cdot>x\<cdot>x \<noteq> GT"
   using compare_self_below_EQ [of x] by clarsimp
 
 declare compare_self_below_EQ [simp]
 
 lemma lt_trans: "lt\<cdot>x\<cdot>y = TT \<Longrightarrow> lt\<cdot>y\<cdot>z = TT \<Longrightarrow> lt\<cdot>x\<cdot>z = TT"
   unfolding lt_eq_TT_iff by (rule compare_LT_trans)
 
 lemma compare_GT_iff_LT: "compare\<cdot>x\<cdot>y = GT \<longleftrightarrow> compare\<cdot>y\<cdot>x = LT"
   by (cases "compare\<cdot>x\<cdot>y", simp_all add: compare_sym [of y x])
 
 lemma compare_GT_trans:
   "compare\<cdot>x\<cdot>y = GT \<Longrightarrow> compare\<cdot>y\<cdot>z = GT \<Longrightarrow> compare\<cdot>x\<cdot>z = GT"
   unfolding compare_GT_iff_LT by (rule compare_LT_trans)
 
 lemma compare_EQ_iff_eq_TT:
   "compare\<cdot>x\<cdot>y = EQ \<longleftrightarrow> eq\<cdot>x\<cdot>y = TT"
   by (cases "compare\<cdot>x\<cdot>y") (simp add: is_EQ_def eq_conv_compare)+
 
 lemma compare_EQ_trans:
   "compare\<cdot>x\<cdot>y = EQ \<Longrightarrow> compare\<cdot>y\<cdot>z = EQ \<Longrightarrow> compare\<cdot>x\<cdot>z = EQ"
   by (blast dest: compare_EQ_dest)
 
 lemma le_trans:
   "le\<cdot>x\<cdot>y = TT \<Longrightarrow> le\<cdot>y\<cdot>z = TT \<Longrightarrow> le\<cdot>x\<cdot>z = TT"
   by (auto dest: eq_TT_dest lt_trans simp: le_iff_lt_or_eq)
 
 lemma neg_lt: "neg\<cdot>(lt\<cdot>x\<cdot>y) = le\<cdot>y\<cdot>x"
   by (cases "compare\<cdot>x\<cdot>y", simp_all add: le_def lt_def compare_sym [of y x])
 
 lemma neg_le: "neg\<cdot>(le\<cdot>x\<cdot>y) = lt\<cdot>y\<cdot>x"
   by (cases "compare\<cdot>x\<cdot>y", simp_all add: le_def lt_def compare_sym [of y x])
 
 subclass Eq_eq
 proof
   fix x y
   show "eq\<cdot>x\<cdot>y = eq\<cdot>y\<cdot>x"
     unfolding eq_conv_compare
     by (cases "compare\<cdot>x\<cdot>y", simp_all add: compare_sym [of y x])
   show "eq\<cdot>x\<cdot>\<bottom> = \<bottom>"
     unfolding eq_conv_compare by simp
   show "eq\<cdot>\<bottom>\<cdot>y = \<bottom>"
     unfolding eq_conv_compare by simp
   show "eq\<cdot>x\<cdot>x \<noteq> FF"
     unfolding eq_conv_compare
     by (cases "compare\<cdot>x\<cdot>x", simp_all)
-  { assume "eq\<cdot>x\<cdot>y = TT" then show "x = y"
-      unfolding eq_conv_compare
-      by (cases "compare\<cdot>x\<cdot>y", auto dest: compare_EQ_dest) }
+  show "x = y" if "eq\<cdot>x\<cdot>y = TT"
+    using that
+    unfolding eq_conv_compare
+    by (cases "compare\<cdot>x\<cdot>y", auto dest: compare_EQ_dest)
 qed
 
 end
 
 text \<open>A combinator for defining Ord instances for datatypes.\<close>
 
 definition thenOrdering :: "Ordering \<rightarrow> Ordering \<rightarrow> Ordering" where
   "thenOrdering = (\<Lambda> x y. case x of LT \<Rightarrow> LT | EQ \<Rightarrow> y | GT \<Rightarrow> GT)"
 
 lemma thenOrdering_simps [simp]:
   "thenOrdering\<cdot>LT\<cdot>y = LT"
   "thenOrdering\<cdot>EQ\<cdot>y = y"
   "thenOrdering\<cdot>GT\<cdot>y = GT"
   "thenOrdering\<cdot>\<bottom>\<cdot>y = \<bottom>"
   unfolding thenOrdering_def by simp_all
 
 lemma thenOrdering_LT_iff [simp]:
   "thenOrdering\<cdot>x\<cdot>y = LT \<longleftrightarrow> x = LT \<or> x = EQ \<and> y = LT"
   by (cases x, simp_all)
 
 lemma thenOrdering_EQ_iff [simp]:
   "thenOrdering\<cdot>x\<cdot>y = EQ \<longleftrightarrow> x = EQ \<and> y = EQ"
   by (cases x, simp_all)
 
 lemma thenOrdering_GT_iff [simp]:
   "thenOrdering\<cdot>x\<cdot>y = GT \<longleftrightarrow> x = GT \<or> x = EQ \<and> y = GT"
   by (cases x, simp_all)
 
 lemma thenOrdering_below_EQ_iff [simp]:
   "thenOrdering\<cdot>x\<cdot>y \<sqsubseteq> EQ \<longleftrightarrow> x \<sqsubseteq> EQ \<and> (x = \<bottom> \<or> y \<sqsubseteq> EQ)"
   by (cases x) simp_all
 
 lemma is_EQ_thenOrdering [simp]:
   "is_EQ\<cdot>(thenOrdering\<cdot>x\<cdot>y) = (is_EQ\<cdot>x andalso is_EQ\<cdot>y)"
   by (cases x) simp_all
 
 lemma oppOrdering_thenOrdering:
   "oppOrdering\<cdot>(thenOrdering\<cdot>x\<cdot>y) =
     thenOrdering\<cdot>(oppOrdering\<cdot>x)\<cdot>(oppOrdering\<cdot>y)"
   by (cases x) simp_all
 
 instantiation lift :: ("{linorder,countable}") Ord_linear
 begin
 
 definition
   "compare \<equiv> (\<Lambda> (Def x) (Def y).
     if x < y then LT else if x > y then GT else EQ)"
 
 instance proof
   fix x y z :: "'a lift"
   show "compare\<cdot>\<bottom>\<cdot>y = \<bottom>"
     unfolding compare_lift_def by simp
   show "compare\<cdot>x\<cdot>\<bottom> = \<bottom>"
     unfolding compare_lift_def by (cases x, simp_all)
   show "oppOrdering\<cdot>(compare\<cdot>x\<cdot>y) = compare\<cdot>y\<cdot>x"
     unfolding compare_lift_def
     by (cases x, cases y, simp, simp,
       cases y, simp, simp add: not_less less_imp_le)
-  { assume "compare\<cdot>x\<cdot>y = EQ" then show "x = y"
-      unfolding compare_lift_def
-      by (cases x, cases y, simp, simp,
-        cases y, simp, simp split: if_splits) }
-  { assume "compare\<cdot>x\<cdot>y = LT" and "compare\<cdot>y\<cdot>z = LT" then show "compare\<cdot>x\<cdot>z = LT"
-      unfolding compare_lift_def
-      by (cases x, simp, cases y, simp, cases z, simp,
-        auto split: if_splits) }
+  show "x = y" if "compare\<cdot>x\<cdot>y = EQ"
+    using that
+    unfolding compare_lift_def
+    by (cases x, cases y, simp, simp,
+        cases y, simp, simp split: if_splits)
+  show "compare\<cdot>x\<cdot>z = LT" if "compare\<cdot>x\<cdot>y = LT" and "compare\<cdot>y\<cdot>z = LT"
+    using that
+    unfolding compare_lift_def
+    by (cases x, simp, cases y, simp, cases z, simp,
+        auto split: if_splits)
   show "eq\<cdot>x\<cdot>y = is_EQ\<cdot>(compare\<cdot>x\<cdot>y)"
     unfolding eq_lift_def compare_lift_def
     by (cases x, simp, cases y, simp, auto)
   show "compare\<cdot>x\<cdot>x \<sqsubseteq> EQ"
     unfolding compare_lift_def
     by (cases x, simp_all)
 qed
 
 end
 
 lemma lt_le:
   "lt\<cdot>(x::'a::Ord_linear)\<cdot>y = (le\<cdot>x\<cdot>y andalso neq\<cdot>x\<cdot>y)"
   by (cases "compare\<cdot>x\<cdot>y")
      (auto simp: lt_def le_def eq_conv_compare)
 
 end
 
diff --git a/thys/HOLCF-Prelude/examples/HLint.thy b/thys/HOLCF-Prelude/examples/HLint.thy
--- a/thys/HOLCF-Prelude/examples/HLint.thy
+++ b/thys/HOLCF-Prelude/examples/HLint.thy
@@ -1,990 +1,989 @@
 theory HLint
   imports
     "../HOLCF_Prelude"
     "../List_Comprehension"
 begin
 
 section \<open>HLint\<close>
 
 text \<open>
   The tool \texttt{hlint} analyses Haskell code and, based on a data base of
   rewrite rules, suggests stylistic improvements to it. We verify
   a number of these rules using our implementation of the Haskell standard
   library.
 \<close>
 
 (* -- I/O *)
 (*  putStrLn (show x) ==> print x *)
 (*  mapM_ putChar ==> putStr *)
 (*  hGetChar stdin ==> getChar *)
 (*  hGetLine stdin ==> getLine *)
 (*  hGetContents stdin ==> getContents *)
 (*  hPutChar stdout ==> putChar *)
 (*  hPutStr stdout ==> putStr *)
 (*  hPutStrLn stdout ==> putStrLn *)
 (*  hPrint stdout ==> print *)
 (*  hWaitForInput a 0 ==> hReady a *)
 (*  hPutStrLn a (show b) ==> hPrint a b *)
 (*  hIsEOF stdin ==> isEOF *)
 (* -- EXIT *)
 (*  exitWith ExitSuccess ==> exitSuccess *)
 
 subsection \<open>Ord\<close>
 
 (*  not (a == b) ==> a /= b where note = "incorrect if either value is NaN" *)
 (*  not (a /= b) ==> a == b where note = "incorrect if either value is NaN" *)
 (*  not (a >  b) ==> a <= b where note = "incorrect if either value is NaN" *)
 (*  not (a >= b) ==> a <  b where note = "incorrect if either value is NaN" *)
 (*  not (a <  b) ==> a >= b where note = "incorrect if either value is NaN" *)
 (*  not (a <= b) ==> a >  b where note = "incorrect if either value is NaN" *)
 
 (*  compare x y /= GT ==> x <= y *)
 (*  compare x y == LT ==> x < y *)
 (*  compare x y /= LT ==> x >= y *)
 (*  compare x y == GT ==> x > y *)
 
 text \<open>@{verbatim \<open>x == a || x == b || x == c ==> x `elem` [a,b,c]\<close> } \<close>
 lemma "(eq\<cdot>(x::'a::Eq_sym)\<cdot>a orelse eq\<cdot>x\<cdot>b orelse eq\<cdot>x\<cdot>c) = elem\<cdot>x\<cdot>[a, b, c]"
   by (auto simp add: eq_sym)
 
 text \<open>@{verbatim \<open> x /= a && x /= b && x /= c ==> x `notElem` [a,b,c]\<close> } \<close>
 lemma "(neq\<cdot>(x::'a::Eq_sym)\<cdot>a andalso neq\<cdot>x\<cdot>b andalso neq\<cdot>x\<cdot>c) = notElem\<cdot>x\<cdot>[a, b, c]"
   by (auto simp add: eq_sym)
 
     (*  compare (f x) (f y) ==> Data.Ord.comparing f x y -- not that great *)
     (*  on compare f ==> Data.Ord.comparing f -- not that great *)
     (* -- READ/SHOW *)
     (*  showsPrec 0 x "" ==> show x *)
     (*  readsPrec 0 ==> reads *)
     (*  showsPrec 0 ==> shows *)
     (*  showIntAtBase 16 intToDigit ==> showHex *)
     (*  showIntAtBase 8 intToDigit ==> showOct *)
 
 subsection \<open>List\<close>
 
 text \<open>@{verbatim \<open> concat (map f x) ==> concatMap f x\<close> } \<close>
 lemma "concat\<cdot>(map\<cdot>f\<cdot>x) = concatMap\<cdot>f\<cdot>x"
   by (auto simp add: concatMap_def)
 
 text \<open>@{verbatim \<open> concat [a, b] ==> a ++ b\<close> } \<close>
 lemma "concat\<cdot>[a, b] = a ++ b"
   by auto
 
 text \<open>@{verbatim \<open> map f (map g x) ==> map (f . g) x\<close> } \<close>
 lemma "map\<cdot>f\<cdot>(map\<cdot>g\<cdot>x) = map\<cdot>(f oo g)\<cdot>x"
   by auto
 
 text \<open>@{verbatim \<open> x !! 0 ==> head x\<close> } \<close>
 lemma "x !! 0 = head\<cdot>x"
   by (cases x) auto
 
 text \<open>@{verbatim \<open> take n (repeat x) ==> replicate n x\<close> } \<close>
 lemma "take\<cdot>n\<cdot>(repeat\<cdot>x) = replicate\<cdot>n\<cdot>x"
   by (simp add: replicate_def)
 
 text \<open>@{verbatim \<open>lemma "head\<cdot>(reverse\<cdot>x) = last\<cdot>x" \<close> } \<close>
 lemma "head\<cdot>(reverse\<cdot>x) = last\<cdot>x"
 proof (cases "finite_list x")
   case True then show ?thesis
     by (induct x rule: reverse_induct) (auto simp add: last_append_singleton)
 next
   case False then show ?thesis
     by (simp add: last_spine_strict reverse_spine_strict)
 qed
 
 text \<open>@{verbatim \<open> head (drop n x) ==> x !! n where note = "if the index is non-negative"\<close> } \<close>
 lemma
   assumes "le\<cdot>0\<cdot>n \<noteq> FF"
   shows "head\<cdot>(drop\<cdot>n\<cdot>x) = x !! n"
 proof (cases "le\<cdot>0\<cdot>n")
   assume "le\<cdot>0\<cdot>n = FF" with assms show ?thesis..
 next
   assume "le\<cdot>0\<cdot>n = TT"
   then show ?thesis
   proof (induction arbitrary: x rule: nonneg_Integer_induct)
     case 0
     show ?case by (cases x) auto
   next
     case (step i x)
     from step.hyps have [simp]:"le\<cdot>i\<cdot>0 = FF" by (cases i, auto simp add: one_Integer_def zero_Integer_def)
     from step.hyps have [simp]:"eq\<cdot>i\<cdot>0 = FF" by (cases i, auto simp add: one_Integer_def zero_Integer_def)
     show ?case
       using step.IH  by (cases x)auto
   qed
 qed simp
 
 text \<open>@{verbatim \<open> reverse (tail (reverse x)) ==> init x\<close> } \<close>
 lemma "reverse\<cdot>(tail\<cdot>(reverse\<cdot>x)) \<sqsubseteq> init\<cdot>x"
 proof (cases "finite_list x")
   case True
   then show ?thesis
     by (induct x rule: reverse_induct) (auto simp add: init_append_singleton)
 next
   case False
   then show ?thesis
     by (auto simp add: reverse_spine_strict)
 qed
 
 text \<open>@{verbatim \<open> take (length x - 1) x ==> init x\<close> } \<close>
 lemma
   assumes "x \<noteq> []"
   shows "take\<cdot>(length\<cdot>x - 1)\<cdot>x \<sqsubseteq> init\<cdot>x"
   using assms
 proof (induct x)
-  case (Cons y ys)
+  case IH: (Cons y ys)
   show ?case
   proof (cases ys)
-    note IH = Cons
     case (Cons z zs)
     show ?thesis
       using IH
       by (cases "length\<cdot>zs")
          (auto simp: Cons one_Integer_def dest: length_ge_0)
   qed (auto simp: one_Integer_def)
 qed auto
 
 text \<open>@{verbatim \<open> foldr (++) [] ==> concat\<close> } \<close>
 lemma foldr_append_concat:"foldr\<cdot>append\<cdot>[] = concat"
 proof (rule cfun_eqI)
   fix xs :: "[['a]]"
   show "foldr\<cdot>append\<cdot>[]\<cdot>xs = concat\<cdot>xs"
     by (induct xs) auto
 qed
 
 text \<open>@{verbatim \<open> foldl (++) [] ==> concat\<close> } \<close>
 lemma "foldl\<cdot>append\<cdot>[] \<sqsubseteq> concat"
 proof (rule cfun_belowI)
   fix xs :: "[['a]]"
   show "foldl\<cdot>append\<cdot>[]\<cdot>xs \<sqsubseteq> concat\<cdot>xs"
     by (cases "finite_list xs")
        (auto simp add: foldr_append_concat foldl_assoc_foldr foldl_spine_strict)
 qed
 
 text \<open>@{verbatim \<open> span (not . p) ==> break p\<close> } \<close>
 lemma "span\<cdot>(neg oo p) = break\<cdot>p"
   by simp
 
 text \<open>@{verbatim \<open> break (not . p) ==> span p\<close> } \<close>
 lemma "break\<cdot>(neg oo p) = span\<cdot>p"
   by (unfold break.simps) (subst assoc_oo, simp)
 
 (*  concatMap (++ "\n") ==> unlines *)
 
 text \<open>@{verbatim \<open> or (map p x) ==> any p x\<close> } \<close>
 lemma "the_or\<cdot>(map\<cdot>p\<cdot>x) = any\<cdot>p\<cdot>x"
   by simp
 
 text \<open>@{verbatim \<open> and (map p x) ==> all p x\<close> } \<close>
 lemma "the_and\<cdot>(map\<cdot>p\<cdot>x) = all\<cdot>p\<cdot>x"
   by simp
 
 text \<open>@{verbatim \<open> zipWith (,) ==> zip\<close> } \<close>
 lemma "zipWith\<cdot>\<langle>,\<rangle> = zip"
   by (simp add: zip_def)
 
 text \<open>@{verbatim \<open> zipWith3 (,,) ==> zip3\<close> } \<close>
 lemma "zipWith3\<cdot>\<langle>,,\<rangle> = zip3"
   by (simp add: zip3_def)
 
 text \<open>@{verbatim \<open> length x == 0 ==> null x where note = "increases laziness"\<close> } \<close>
 lemma "eq\<cdot>(length\<cdot>x)\<cdot>0 \<sqsubseteq> null\<cdot>x"
 proof (cases x)
   case (Cons y ys)
   then show ?thesis
     by (cases "length\<cdot>ys")
        (auto dest: length_ge_0 simp: zero_Integer_def one_Integer_def)
 qed simp+
 
 text \<open>@{verbatim \<open> length x /= 0 ==> not (null x)\<close> } \<close>
 lemma "neq\<cdot>(length\<cdot>x)\<cdot>0 \<sqsubseteq> neg\<cdot>(null\<cdot>x)"
 proof (cases x)
   case (Cons y ys)
   then show ?thesis
     by (cases "length\<cdot>ys")
        (auto dest: length_ge_0 simp: zero_Integer_def one_Integer_def)
 qed simp+
 
 (*  (\x -> [x]) ==> (:[]) *)
 
 text \<open>@{verbatim \<open> map (uncurry f) (zip x y) ==> zipWith f x y\<close> } \<close>
 lemma "map\<cdot>(uncurry\<cdot>f)\<cdot>(zip\<cdot>x\<cdot>y) = zipWith\<cdot>f\<cdot>x\<cdot>y"
 proof (induct x arbitrary: y)
   case (Cons x xs y) then show ?case by (cases y) auto
 qed auto
 
 text \<open>@{verbatim \<open> map f (zip x y) ==> zipWith (curry f) x y where _ = isVar f\<close> } \<close>
 lemma "map\<cdot>f\<cdot>(zip\<cdot>x\<cdot>y) = zipWith\<cdot>(curry\<cdot>f)\<cdot>x\<cdot>y"
 proof(induct x arbitrary: y)
   case (Cons x xs y) then show ?case by (cases y) auto
 qed auto
 
 text \<open>@{verbatim \<open> not (elem x y) ==> notElem x y\<close> } \<close>
 lemma "neg\<cdot>(elem\<cdot>x\<cdot>y) = notElem\<cdot>x\<cdot>y"
   by (induct y) auto
 
 text \<open>@{verbatim \<open> foldr f z (map g x) ==> foldr (f . g) z x\<close> } \<close>
 lemma "foldr\<cdot>f\<cdot>z\<cdot>(map\<cdot>g\<cdot>x) = foldr\<cdot>(f oo g)\<cdot>z\<cdot>x"
   by (induct x) auto
 
 (*  x ++ concatMap (' ':) y ==> unwords (x:y) *)
 (*  intercalate " " ==> unwords *)
 (*  concat (intersperse x y) ==> intercalate x y where _ = notEq x " " *)
 (*  concat (intersperse " " x) ==> unwords x *)
 text \<open>@{verbatim \<open> null (filter f x) ==> not (any f x)\<close> } \<close>
 lemma "null\<cdot>(filter\<cdot>f\<cdot>x) = neg\<cdot>(any\<cdot>f\<cdot>x)"
 proof (induct x)
   case (Cons x xs)
   then show ?case by (cases "f\<cdot>x") auto
 qed auto
 
 text \<open>@{verbatim \<open> filter f x == [] ==> not (any f x)\<close> } \<close>
 lemma "eq\<cdot>(filter\<cdot>f\<cdot>x)\<cdot>[] = neg\<cdot>(any\<cdot>f\<cdot>x)"
 proof (induct x)
   case (Cons x xs)
   then show ?case by (cases "f\<cdot>x") auto
 qed auto
 
 text \<open>@{verbatim \<open> filter f x /= [] ==> any f x\<close> } \<close>
 lemma "neq\<cdot>(filter\<cdot>f\<cdot>x)\<cdot>[] = any\<cdot>f\<cdot>x"
 proof (induct x)
   case (Cons x xs)
   then show ?case by (cases "f\<cdot>x") auto
 qed auto
 
 text \<open>@{verbatim \<open> any (== a) ==> elem a\<close> } \<close>
 lemma "any\<cdot>(\<Lambda> z. eq\<cdot>z\<cdot>a) = elem\<cdot>a"
 proof (rule cfun_eqI)
   fix xs
   show "any\<cdot>(\<Lambda> z. eq\<cdot>z\<cdot>a)\<cdot>xs = elem\<cdot>a\<cdot>xs"
     by (induct xs) auto
 qed
 
 text \<open>@{verbatim \<open> any ((==) a) ==> elem a\<close> } \<close>
 lemma "any\<cdot>(eq\<cdot>(a::'a::Eq_sym)) = elem\<cdot>a"
 proof (rule cfun_eqI)
   fix xs
   show "any\<cdot>(eq\<cdot>a)\<cdot>xs = elem\<cdot>a\<cdot>xs"
     by (induct xs) (auto simp: eq_sym)
 qed
 
 text \<open>@{verbatim \<open>any (a ==) ==> elem a\<close> } \<close>
 lemma "any\<cdot>(\<Lambda> z. eq\<cdot>(a::'a::Eq_sym)\<cdot>z) = elem\<cdot>a"
 proof (rule cfun_eqI)
   fix xs
   show "any\<cdot>(\<Lambda> z. eq\<cdot>a\<cdot>z)\<cdot>xs = elem\<cdot>a\<cdot>xs"
     by (induct xs) (auto simp: eq_sym)
 qed
 
 text \<open>@{verbatim \<open> all (/= a) ==> notElem a\<close> } \<close>
 lemma "all\<cdot>(\<Lambda> z. neq\<cdot>z\<cdot>(a::'a::Eq_sym)) = notElem\<cdot>a"
 proof (rule cfun_eqI)
   fix xs
   show "all\<cdot>(\<Lambda> z. neq\<cdot>z\<cdot>a)\<cdot>xs = notElem\<cdot>a\<cdot>xs"
     by (induct xs) auto
 qed
 
 text \<open>@{verbatim \<open> all (a /=) ==> notElem a\<close> } \<close>
 lemma "all\<cdot>(\<Lambda> z. neq\<cdot>(a::'a::Eq_sym)\<cdot>z) = notElem\<cdot>a"
 proof (rule cfun_eqI)
   fix xs
   show "all\<cdot>(\<Lambda> z. neq\<cdot>a\<cdot>z)\<cdot>xs = notElem\<cdot>a\<cdot>xs"
     by (induct xs) (auto simp: eq_sym)
 qed
 
 (* findIndex ((==) a) ==> elemIndex a *)
 (* findIndex (a ==) ==> elemIndex a *)
 (* findIndex (== a) ==> elemIndex a *)
 (* findIndices ((==) a) ==> elemIndices a *)
 (* findIndices (a ==) ==> elemIndices a *)
 (* findIndices (== a) ==> elemIndices a *)
 (* lookup b (zip l [0..]) ==> elemIndex b l *)
 
 subsection \<open>Folds\<close>
 
 (*  foldr  (>>) (return ()) ==> sequence_ *)
 
 text \<open>@{verbatim \<open> foldr  (&&) True ==> and\<close> } \<close>
 lemma "foldr\<cdot>trand\<cdot>TT = the_and"
   by (subst the_and.simps, rule)
 
 text \<open>@{verbatim \<open> foldl  (&&) True ==> and\<close> } \<close>
 lemma foldl_to_and:"foldl\<cdot>trand\<cdot>TT \<sqsubseteq> the_and"
 proof (rule cfun_belowI)
   fix xs
   show "foldl\<cdot>trand\<cdot>TT\<cdot>xs \<sqsubseteq> the_and\<cdot>xs"
     by (cases "finite_list xs") (auto simp: foldl_assoc_foldr foldl_spine_strict)
 qed
 
 text \<open>@{verbatim \<open> foldr1 (&&)  ==> and\<close> } \<close>
 lemma "foldr1\<cdot>trand \<sqsubseteq> the_and"
 proof (rule cfun_belowI)
   fix xs
   show "foldr1\<cdot>trand\<cdot>xs \<sqsubseteq> the_and\<cdot>xs"
   proof (induct xs)
     case (Cons y ys)
     then show ?case by (cases ys) (auto elim: monofun_cfun_arg)
   qed simp+
 qed
 
 text \<open>@{verbatim \<open> foldl1 (&&)  ==> and\<close> } \<close>
 lemma "foldl1\<cdot>trand \<sqsubseteq> the_and"
 proof (rule cfun_belowI)
   fix x
   have "foldl1\<cdot>trand\<cdot>x \<sqsubseteq> foldl\<cdot>trand\<cdot>TT\<cdot>x"
     by (cases x, auto)
   also have "... \<sqsubseteq> the_and\<cdot>x"
     by (rule monofun_cfun_fun[OF foldl_to_and])
   finally show "foldl1\<cdot>trand\<cdot>x \<sqsubseteq> the_and\<cdot>x" .
 qed
 
 text \<open>@{verbatim \<open> foldr  (||) False ==> or\<close> } \<close>
 lemma "foldr\<cdot>tror\<cdot>FF = the_or"
   by (subst the_or.simps, rule)
 
 text \<open>@{verbatim \<open> foldl  (||) False ==> or\<close> } \<close>
 lemma foldl_to_or: "foldl\<cdot>tror\<cdot>FF \<sqsubseteq> the_or"
 proof (rule cfun_belowI)
   fix xs
   show "foldl\<cdot>tror\<cdot>FF\<cdot>xs \<sqsubseteq> the_or\<cdot>xs"
     by (cases "finite_list xs") (auto simp: foldl_assoc_foldr foldl_spine_strict)
 qed
 
 text \<open>@{verbatim \<open> foldr1 (||)  ==> or\<close> } \<close>
 lemma "foldr1\<cdot>tror \<sqsubseteq> the_or"
 proof (rule cfun_belowI)
   fix xs
   show "foldr1\<cdot>tror\<cdot>xs \<sqsubseteq> the_or\<cdot>xs"
   proof (induct xs)
     case (Cons y ys)
     then show ?case by (cases ys) (auto elim: monofun_cfun_arg)
   qed simp+
 qed
 
 text \<open>@{verbatim \<open> foldl1 (||)  ==> or\<close> } \<close>
 lemma "foldl1\<cdot>tror \<sqsubseteq> the_or"
 proof(rule cfun_belowI)
   fix x
   have "foldl1\<cdot>tror\<cdot>x \<sqsubseteq> foldl\<cdot>tror\<cdot>FF\<cdot>x"
     by (cases x, auto)
   also have "... \<sqsubseteq> the_or\<cdot>x"
     by (rule monofun_cfun_fun[OF foldl_to_or])
   finally show "foldl1\<cdot>tror\<cdot>x \<sqsubseteq> the_or\<cdot>x" .
 qed
 
 (*  foldl  (+) 0 ==> sum *)
 (*  foldr  (+) 0 ==> sum *)
 (*  foldl1 (+)   ==> sum *)
 (*  foldr1 (+)   ==> sum *)
 (*  foldl  ( * ) 1 ==> product *)
 (*  foldr  ( * ) 1 ==> product *)
 (*  foldl1 ( * )   ==> product *)
 (*  foldr1 ( * )   ==> product *)
 (*  foldl1 max   ==> maximum *)
 (*  foldr1 max   ==> maximum *)
 (*  foldl1 min   ==> minimum *)
 (*  foldr1 min   ==> minimum *)
 (*  foldr mplus mzero ==> msum *)
 
 subsection \<open>Function\<close>
 text \<open>@{verbatim \<open> (\x -> x) ==> id\<close> } \<close>
 lemma "(\<Lambda> x. x) = ID"
   by (metis ID_def)
 
 text \<open>@{verbatim \<open> (\x y -> x) ==> const\<close> } \<close>
 lemma "(\<Lambda> x y. x) = const"
   by (intro cfun_eqI) simp
 
 text \<open>@{verbatim \<open>(\(x,y) -> y) ==> fst where _ = notIn x y\<close> } \<close>
 lemma "(\<Lambda> \<langle>x, y\<rangle>. x) = fst"
 proof (rule cfun_eqI)
   fix p
   show "(case p of \<langle>x, y\<rangle> \<Rightarrow> x) = fst \<cdot> p"
   proof (cases p)
     case bottom then show ?thesis by simp
   next
     case Tuple2 then show ?thesis by simp
   qed
 qed
 
 text \<open>@{verbatim \<open>(\(x,y) -> y) ==> snd where _ = notIn x y\<close> } \<close>
 lemma "(\<Lambda> \<langle>x, y\<rangle>. y) = snd"
 proof (rule cfun_eqI)
   fix p
   show "(case p of \<langle>x, y\<rangle> \<Rightarrow> y) = snd \<cdot> p"
   proof (cases p)
     case bottom then show ?thesis by simp
   next
     case Tuple2 then show ?thesis by simp
   qed
 qed
 
 text \<open>@{verbatim \<open> (\x y-> f (x,y)) ==> curry f where _ = notIn [x,y] f\<close> } \<close>
 lemma "(\<Lambda> x y. f\<cdot>\<langle>x, y\<rangle>) = curry\<cdot>f"
   by (auto intro!: cfun_eqI)
 
 text \<open>@{verbatim \<open> (\(x,y) -> f x y) ==> uncurry f where _ = notIn [x,y] f\<close> } \<close>
 lemma "(\<Lambda> \<langle>x, y\<rangle>. f\<cdot>x\<cdot>y) \<sqsubseteq> uncurry\<cdot>f"
   by (rule cfun_belowI, rename_tac x, case_tac x, auto)
 
 (*  (($) . f) ==> f *)
 (*  (f $) ==> f *)
 
 text \<open>@{verbatim \<open> (\x -> y) ==> const y where _ = isAtom y && notIn x y\<close> } \<close>
 lemma "(\<Lambda> x. y) = const\<cdot>y"
   by (intro cfun_eqI) simp
 
 (*  flip f x y ==> f y x where _ = isApp original *)
 lemma "flip\<cdot>f\<cdot>x\<cdot>y = f\<cdot>y\<cdot>x" by simp
 
 (*  (\a b -> o (f a) (f b)) ==> o `Data.Function.on` f *)
 (* -- CHAR *)
 (*  a >= 'a' && a <= 'z' ==> isAsciiLower a *)
 (*  a >= 'A' && a <= 'Z' ==> isAsciiUpper a *)
 (*  a >= '0' && a <= '9' ==> isDigit a *)
 (*  a >= '0' && a <= '7' ==> isOctDigit a *)
 (*  not (isControl a) ==> isPrint a *)
 (*  isLower a || isUpper a ==> isAlpha a *)
 (*  isAlpha a || isDigit a ==> isAlphaNum a *)
 
 subsection \<open>Bool\<close>
 
 text \<open>@{verbatim \<open> a == True ==> a\<close> } \<close>
 lemma eq_true:"eq\<cdot>x\<cdot>TT = x"
   by (cases x, auto)
 
 text \<open>@{verbatim \<open> a == False ==> not a\<close> } \<close>
 lemma eq_false:"eq\<cdot>x\<cdot>FF = neg\<cdot>x"
   by (cases x, auto)
 
 text \<open>@{verbatim \<open> (if a then x else x) ==> x where note = "reduces strictness"\<close> } \<close>
 lemma if_equal:"(If a then x else x) \<sqsubseteq> x"
   by (cases a, auto)
 
 text \<open>@{verbatim \<open> (if a then True else False) ==> a\<close> } \<close>
 lemma "(If a then TT else FF) = a"
   by (cases a, auto)
 
 text \<open>@{verbatim \<open> (if a then False else True) ==> not a\<close> } \<close>
 lemma "(If a then FF else TT) = neg\<cdot>a"
   by (cases a, auto)
 
 text \<open>@{verbatim \<open> (if a then t else (if b then t else f)) ==> if a || b then t else f\<close> } \<close>
 lemma "(If a then t else (If b then t else f)) = (If a orelse b then t else f)"
   by (cases a, auto)
 
 text \<open>@{verbatim \<open> (if a then (if b then t else f) else f) ==> if a && b then t else f\<close> } \<close>
 lemma "(If a then (If b then t else f) else f) = (If a andalso b then t else f)"
   by (cases a, auto)
 
 text \<open>@{verbatim \<open> (if x then True else y) ==> x || y where _ = notEq y False\<close> } \<close>
 lemma "(If x then TT else y) = (x orelse y)"
   by (cases x, auto)
 
 text \<open>@{verbatim \<open> (if x then y else False) ==> x && y where _ = notEq y True\<close> } \<close>
 lemma "(If x then y else FF) = (x andalso y)"
   by (cases x, auto)
 
 (*  case a of {True -> t; False -> f} ==> if a then t else f *)
 (*  case a of {False -> f; True -> t} ==> if a then t else f *)
 (*  case a of {True -> t; _ -> f} ==> if a then t else f *)
 (*  case a of {False -> f; _ -> t} ==> if a then t else f *)
 text \<open>@{verbatim \<open> (if c then (True, x) else (False, x)) ==> (c, x) where note = "reduces strictness"\<close> } \<close>
 lemma "(If c then \<langle>TT, x\<rangle> else \<langle>FF, x\<rangle>) \<sqsubseteq> \<langle>c, x\<rangle>"
   by (cases c, auto)
 
 text \<open>@{verbatim \<open> (if c then (False, x) else (True, x)) ==> (not c, x) where note = "reduces strictness"\<close> } \<close>
 lemma "(If c then \<langle>FF, x\<rangle> else \<langle>TT, x\<rangle>) \<sqsubseteq> \<langle>neg\<cdot>c, x\<rangle>"
   by (cases c, auto)
 
 text \<open>@{verbatim \<open> or [x,y]  ==> x || y\<close> } \<close>
 lemma "the_or\<cdot>[x, y] = (x orelse y)"
   by (fixrec_simp)
 
 text \<open>@{verbatim \<open> or [x,y,z]  ==> x || y || z\<close> } \<close>
 lemma "the_or\<cdot>[x, y, z] = (x orelse y orelse z)"
   by (fixrec_simp)
 
 text \<open>@{verbatim \<open> and [x,y]  ==> x && y\<close> } \<close>
 lemma "the_and\<cdot>[x, y] = (x andalso y)"
   by (fixrec_simp)
 
 text \<open>@{verbatim \<open> and [x,y,z]  ==> x && y && z\<close> } \<close>
 lemma "the_and\<cdot>[x, y, z] = (x andalso y andalso z)"
   by (fixrec_simp)
 
 subsection \<open>Arrow\<close>
 
 (*  id *** g ==> second g *)
 (*  f *** id ==> first f *)
 (*  zip (map f x) (map g x) ==> map (f Control.Arrow.&&& g) x *)
 (*  (\(x,y) -> (f x, g y)) ==> f Control.Arrow.*** g where _ = notIn [x,y] [f,g] *)
 (*  (\x -> (f x, g x)) ==> f Control.Arrow.&&& g where _ = notIn x [f,g] *)
 (*  (\(x,y) -> (f x,y)) ==> Control.Arrow.first f where _ = notIn [x,y] f *)
 (*  (\(x,y) -> (x,f y)) ==> Control.Arrow.second f where _ = notIn [x,y] f *)
 (*  (f (fst x), g (snd x)) ==> (f Control.Arrow.*** g) x *)
 
 text \<open>@{verbatim \<open> (fst x, snd x) ==>  x\<close> } \<close>
 lemma "x \<sqsubseteq> \<langle>fst\<cdot>x, snd\<cdot>x\<rangle>"
   by (cases x, auto)
 
 (* -- FUNCTOR *)
 (*  fmap f (fmap g x) ==> fmap (f . g) x *)
 (*  fmap id ==> id *)
 (* -- MONAD *)
 (*  return a >>= f ==> f a *)
 (*  m >>= return ==> m *)
 (*  m >>= return . f ==> Control.Monad.liftM f m -- cannot be fmap, because is in Functor not Monad *)
 (*  (if x then y else return ()) ==> Control.Monad.when x $ _noParen_ y where _ = not (isAtom y) *)
 (*  (if x then y else return ()) ==> Control.Monad.when x y where _ = isAtom y *)
 (*  (if x then return () else y) ==> Control.Monad.unless x $ _noParen_ y where _ = not (isAtom y) *)
 (*  (if x then return () else y) ==> Control.Monad.unless x y where _ = isAtom y *)
 (*  sequence (map f x) ==> mapM f x *)
 (*  sequence_ (map f x) ==> mapM_ f x *)
 (*  flip mapM ==> Control.Monad.forM *)
 (*  flip mapM_ ==> Control.Monad.forM_ *)
 (*  flip forM ==> mapM *)
 (*  flip forM_ ==> mapM_ *)
 (*  when (not x) ==> unless x *)
 (*  x >>= id ==> Control.Monad.join x *)
 (*  liftM f (liftM g x) ==> liftM (f . g) x *)
 (*  a >> return () ==> void a *)
 (*  fmap (const ()) ==> void *)
 (*  flip (>=>) ==> (<=<) *)
 (*  flip (<=<) ==> (>=>) *)
 (*  (\x -> f x >>= g) ==> f Control.Monad.>=> g where _ = notIn x [f,g] *)
 (*  (\x -> f =<< g x) ==> f Control.Monad.<=< g where _ = notIn x [f,g] *)
 (*  a >> forever a ==> forever a *)
 (*  liftM2 id ==> ap *)
 (* -- MONAD LIST *)
 (*  liftM unzip (mapM f x) ==> Control.Monad.mapAndUnzipM f x *)
 (*  sequence (zipWith f x y) ==> Control.Monad.zipWithM f x y *)
 (*  sequence_ (zipWith f x y) ==> Control.Monad.zipWithM_ f x y *)
 (*  sequence (replicate n x) ==> Control.Monad.replicateM n x *)
 (*  sequence_ (replicate n x) ==> Control.Monad.replicateM_ n x *)
 (*  mapM f (map g x) ==> mapM (f . g) x *)
 (*  mapM_ f (map g x) ==> mapM_ (f . g) x *)
 (* -- APPLICATIVE / TRAVERSABLE *)
 (*  flip traverse ==> for *)
 (*  flip for ==> traverse *)
 (*  flip traverse_ ==> for_ *)
 (*  flip for_ ==> traverse_ *)
 (*  foldr ( *>) (pure ()) ==> sequenceA_ *)
 (*  foldr (<|>) empty ==> asum *)
 (*  liftA2 (flip ($)) ==> (<**>) *)
 (*  Just <$> a <|> pure Nothing ==> optional a *)
 (* -- LIST COMP *)
 (*  (if b then [x] else []) ==> [x | b] *)
 (*  [x | x <- y] ==> y where _ = isVar x *)
 (* -- SEQ *)
 
 subsection \<open>Seq\<close>
 
 text \<open>@{verbatim \<open> x `seq` x ==> x\<close> } \<close>
 lemma "seq\<cdot>x\<cdot>x = x" by (simp add: seq_def)
 
 (*  id $! x ==> x *)
 (*  x `seq` y ==> y where _ = isWHNF x *)
 (*  f $! x ==> f x where _ = isWHNF x *)
 (*  evaluate x ==> return x where _ = isWHNF x *)
 (* -- MAYBE *)
 (*  maybe x id ==> Data.Maybe.fromMaybe x *)
 (*  maybe False (const True) ==> Data.Maybe.isJust *)
 (*  maybe True (const False) ==> Data.Maybe.isNothing *)
 (*  not (isNothing x) ==> isJust x *)
 (*  not (isJust x) ==> isNothing x *)
 (*  maybe [] (:[]) ==> maybeToList *)
 (*  catMaybes (map f x) ==> mapMaybe f x *)
 (*  (case x of Nothing -> y; Just a -> a)  ==> fromMaybe y x *)
 (*  (if isNothing x then y else f (fromJust x)) ==> maybe y f x *)
 (*  (if isJust x then f (fromJust x) else y) ==> maybe y f x *)
 (*  maybe Nothing (Just . f) ==> fmap f *)
 (*  map fromJust . filter isJust  ==>  Data.Maybe.catMaybes *)
 (*  x == Nothing  ==>  isNothing x *)
 (*  Nothing == x  ==>  isNothing x *)
 (*  x /= Nothing  ==>  Data.Maybe.isJust x *)
 (*  Nothing /= x  ==>  Data.Maybe.isJust x *)
 (*  concatMap (maybeToList . f) ==> Data.Maybe.mapMaybe f *)
 (*  concatMap maybeToList ==> catMaybes *)
 (*  maybe n Just x ==> Control.Monad.mplus x n *)
 (*  (case x of Just a -> a; Nothing -> y)  ==> fromMaybe y x *)
 (*  (if isNothing x then y else fromJust x) ==> fromMaybe y x *)
 (*  (if isJust x then fromJust x else y) ==> fromMaybe y x *)
 (*  isJust x && (fromJust x == y) ==> x == Just y *)
 (*  mapMaybe f (map g x) ==> mapMaybe (f . g) x *)
 (*  fromMaybe a (fmap f x) ==> maybe a f x *)
 (*  [x | Just x <- a] ==> Data.Maybe.catMaybes a *)
 (* -- EITHER *)
 (*  [a | Left a <- a] ==> lefts a *)
 (*  [a | Right a <- a] ==> rights a *)
 (* -- INFIX *)
 (*  X.elem x y ==> x `X.elem` y where _ = not (isInfixApp original) && not (isParen result) *)
 (*  X.notElem x y ==> x `X.notElem` y where _ = not (isInfixApp original) && not (isParen result) *)
 (*  X.isInfixOf x y ==> x `X.isInfixOf` y where _ = not (isInfixApp original) && not (isParen result) *)
 (*  X.isSuffixOf x y ==> x `X.isSuffixOf` y where _ = not (isInfixApp original) && not (isParen result) *)
 (*  X.isPrefixOf x y ==> x `X.isPrefixOf` y where _ = not (isInfixApp original) && not (isParen result) *)
 (*  X.union x y ==> x `X.union` y where _ = not (isInfixApp original) && not (isParen result) *)
 (*  X.intersect x y ==> x `X.intersect` y where _ = not (isInfixApp original) && not (isParen result) *)
 (* -- MATHS *)
 (*  fromIntegral x ==> x where _ = isLitInt x *)
 (*  fromInteger x ==> x where _ = isLitInt x *)
 (*  x + negate y ==> x - y *)
 (*  0 - x ==> negate x *)
 (*  log y / log x ==> logBase x y *)
 (*  x ** 0.5 ==> sqrt x *)
 (*  sin x / cos x ==> tan x *)
 (*  sinh x / cosh x ==> tanh x *)
 (*  n `rem` 2 == 0 ==> even n *)
 (*  n `rem` 2 /= 0 ==> odd n *)
 (*  not (even x) ==> odd x *)
 (*  not (odd x) ==> even x *)
 (*  x ** 0.5 ==> sqrt x *)
 (*  x ^^ y ==> x ** y where _ = isLitInt y *)
 (*  x ^ 0 ==> 1 *)
 (*  round (x - 0.5) ==> floor x *)
 (* -- CONCURRENT *)
 (*  mapM_ (writeChan a) ==> writeList2Chan a *)
 (* -- EXCEPTION *)
 (*  Prelude.catch ==> Control.Exception.catch where note = "Prelude.catch does not catch most exceptions" *)
 (*  flip Control.Exception.catch ==> handle *)
 (*  flip handle ==> Control.Exception.catch *)
 (*  flip (catchJust p) ==> handleJust p *)
 (*  flip (handleJust p) ==> catchJust p *)
 (*  Control.Exception.bracket b (const a) (const t) ==> Control.Exception.bracket_ b a t *)
 (*  Control.Exception.bracket (openFile x y) hClose ==> withFile x y *)
 (*  Control.Exception.bracket (openBinaryFile x y) hClose ==> withBinaryFile x y *)
 (*  throw (ErrorCall a) ==> error a *)
 (*  a `seq` return a ==> Control.Exception.evaluate a *)
 (*  toException NonTermination ==> nonTermination *)
 (*  toException NestedAtomically ==> nestedAtomically *)
 (* -- WEAK POINTERS *)
 (*  mkWeak a a b ==> mkWeakPtr a b *)
 (*  mkWeak a (a, b) c ==> mkWeakPair a b c *)
 
 subsection \<open>Evaluate\<close>
 
 text \<open>@{verbatim \<open> True && x ==> x\<close> } \<close>
 lemma "(TT andalso x) = x" by auto
 
 text \<open>@{verbatim \<open> False && x ==> False\<close> } \<close>
 lemma "(FF andalso x) = FF" by auto
 
 text \<open>@{verbatim \<open> True || x ==> True\<close> } \<close>
 lemma "(TT orelse x) = TT" by auto
 
 text \<open>@{verbatim \<open> False || x ==> x\<close> } \<close>
 lemma "(FF orelse x) = x" by auto
 
 text \<open>@{verbatim \<open> not True ==> False\<close> } \<close>
 lemma "neg\<cdot>TT = FF" by auto
 
 text \<open>@{verbatim \<open> not False ==> True\<close> } \<close>
 lemma "neg\<cdot>FF = TT" by auto
 
 (*  Nothing >>= k ==> Nothing *)
 (*  either f g (Left x) ==> f x *)
 (*  either f g (Right y) ==> g y *)
 text \<open>@{verbatim \<open> fst (x,y) ==> x\<close> } \<close>
 lemma "fst\<cdot>\<langle>x, y\<rangle> = x" by auto
 
 text \<open>@{verbatim \<open> snd (x,y) ==> y\<close> } \<close>
 lemma "snd\<cdot>\<langle>x, y\<rangle> = y" by auto
 
 text \<open>@{verbatim \<open> f (fst p) (snd p) ==> uncurry f p\<close> } \<close>
 lemma "f\<cdot>(fst\<cdot>p)\<cdot>(snd\<cdot>p) = uncurry\<cdot>f\<cdot>p"
   by (cases p, auto)
 
 text \<open>@{verbatim \<open> init [x] ==> []\<close> } \<close>
 lemma "init\<cdot>[x] = []" by auto
 
 text \<open>@{verbatim \<open> null [] ==> True\<close> } \<close>
 lemma "null\<cdot>[] = TT" by auto
 
 text \<open>@{verbatim \<open> length [] ==> 0\<close> } \<close>
 lemma "length\<cdot>[] = 0" by auto
 
 text \<open>@{verbatim \<open> foldl f z [] ==> z\<close> } \<close>
 lemma "foldl\<cdot>f\<cdot>z\<cdot>[] = z" by simp
 
 text \<open>@{verbatim \<open> foldr f z [] ==> z\<close> } \<close>
 lemma "foldr\<cdot>f\<cdot>z\<cdot>[] = z" by auto
 
 text \<open>@{verbatim \<open> foldr1 f [x] ==> x\<close> } \<close>
 lemma "foldr1\<cdot>f\<cdot>[x] = x" by simp
 
 text \<open>@{verbatim \<open> scanr f z [] ==> [z]\<close> } \<close>
 lemma "scanr\<cdot>f\<cdot>z\<cdot>[] = [z]" by simp
 
 text \<open>@{verbatim \<open> scanr1 f [] ==> []\<close> } \<close>
 lemma "scanr1\<cdot>f\<cdot>[] = []" by simp
 
 text \<open>@{verbatim \<open> scanr1 f [x] ==> [x]\<close> } \<close>
 lemma "scanr1\<cdot>f\<cdot>[x] = [x]" by simp
 
 text \<open>@{verbatim \<open> take n [] ==> []\<close> } \<close>
 lemma "take\<cdot>n\<cdot>[] \<sqsubseteq> []" by (cases n, auto)
 
 text \<open>@{verbatim \<open> drop n [] ==> []\<close> } \<close>
 lemma "drop\<cdot>n\<cdot>[] \<sqsubseteq> []"
   by (subst drop.simps) (auto simp: if_equal)
 
 text \<open>@{verbatim \<open> takeWhile p [] ==> []\<close> } \<close>
 lemma "takeWhile\<cdot>p\<cdot>[] = []" by (fixrec_simp)
 
 text \<open>@{verbatim \<open> dropWhile p [] ==> []\<close> } \<close>
 lemma "dropWhile\<cdot>p\<cdot>[] = []" by (fixrec_simp)
 
 text \<open>@{verbatim \<open> span p [] ==> ([],[])\<close> } \<close>
 lemma "span\<cdot>p\<cdot>[] = \<langle>[], []\<rangle>" by (fixrec_simp)
 
 (*  lines "" ==> [] *)
 (*  unwords [] ==> "" *)
 (*  x - 0 ==> x *)
 (*  x * 1 ==> x *)
 (*  x / 1 ==> x *)
 text \<open>@{verbatim \<open> concat [a] ==> a\<close> } \<close>
 lemma "concat\<cdot>[a] = a" by auto
 
 text \<open>@{verbatim \<open> concat [] ==> []\<close> } \<close>
 lemma "concat\<cdot>[] = []" by auto
 
 text \<open>@{verbatim \<open> zip [] [] ==> []\<close> } \<close>
 lemma "zip\<cdot>[]\<cdot>[] = []" by auto
 
 text \<open>@{verbatim \<open> id x ==> x\<close> } \<close>
 lemma "ID\<cdot>x = x" by auto
 
 text \<open>@{verbatim \<open> const x y ==> x\<close> } \<close>
 lemma "const\<cdot>x\<cdot>y = x" by simp
 
 subsection \<open>Complex hints\<close>
 
 text \<open>@{verbatim \<open> take (length t) s == t ==> t `Data.List.isPrefixOf` s\<close> } \<close>
 lemma
   fixes t :: "['a::Eq_sym]"
   shows "eq\<cdot>(take\<cdot>(length\<cdot>t)\<cdot>s)\<cdot>t \<sqsubseteq> isPrefixOf\<cdot>t\<cdot>s"
   by (subst eq_sym) (rule eq_take_length_isPrefixOf)
 
 text \<open>@{verbatim \<open> (take i s == t) ==> _eval_ ((i >= length t) && (t `Data.List.isPrefixOf` s))\<close> } \<close>
 text \<open>The hint is not true in general, as the following two lemmas show:\<close>
 lemma
   assumes "t = []" and "s = x : xs" and "i = 1"
   shows "\<not> (eq\<cdot>(take\<cdot>i\<cdot>s)\<cdot>t \<sqsubseteq> (le\<cdot>(length\<cdot>t)\<cdot>i andalso isPrefixOf\<cdot>t\<cdot>s))"
   using assms by simp
 
 lemma
   assumes "le\<cdot>0\<cdot>i = TT" and "le\<cdot>i\<cdot>0 = FF"
     and "s = \<bottom>" and "t = []"
   shows "\<not> ((le\<cdot>(length\<cdot>t)\<cdot>i andalso isPrefixOf\<cdot>t\<cdot>s) \<sqsubseteq> eq\<cdot>(take\<cdot>i\<cdot>s)\<cdot>t)"
   using assms by (subst take.simps) simp
 
 (* -- clever hint, but not actually a good idea *)
 (*  (do a <- f; g a) ==> f >>= g *)
 (*  a $$$$ b $$$$ c ==> a . b $$$$$ c *)
 
 (* not (a == b) ==> a /= b *)
 lemma "neg\<cdot>(eq\<cdot>a\<cdot>b) = neq\<cdot>a\<cdot>b" by auto
 
 text \<open>@{verbatim \<open>not (a /= b) ==> a == b\<close> } \<close>
 lemma "neg\<cdot>(neq\<cdot>a\<cdot>b) = eq\<cdot>a\<cdot>b" by auto
 
 text \<open>@{verbatim \<open>map id ==> id\<close> } \<close>
 lemma map_id:"map\<cdot>ID = ID" by (auto simp add: cfun_eq_iff)
 
 text \<open>@{verbatim \<open>x == [] ==> null x\<close> } \<close>
 lemma "eq\<cdot>x\<cdot>[] = null\<cdot>x" by (cases x, auto)
 
 text \<open>@{verbatim \<open>any id ==> or\<close> } \<close>
 lemma "any\<cdot>ID = the_or" by (auto simp add:map_id)
 
 text \<open>@{verbatim \<open>all id ==> and\<close> } \<close>
 lemma "all\<cdot>ID = the_and" by (auto simp add:map_id)
 
 text \<open>@{verbatim \<open>(if x then False else y) ==> (not x && y)\<close> } \<close>
 lemma "(If x then FF else y) = (neg\<cdot>x andalso y)" by (cases x, auto)
 
 text \<open>@{verbatim \<open>(if x then y else True) ==> (not x || y)\<close> } \<close>
 lemma "(If x then y else TT) = (neg\<cdot>x orelse y)" by (cases x, auto)
 
 text \<open>@{verbatim \<open>not (not x) ==> x\<close> } \<close>
 lemma "neg\<cdot>(neg\<cdot>x) = x" by auto
 
 text \<open>@{verbatim \<open>(if c then f x else f y) ==> f (if c then x else y)\<close> } \<close>
 lemma "(If c then f\<cdot>x else f\<cdot>y) \<sqsubseteq> f\<cdot>(If c then x else y)" by (cases c, auto)
 
 text \<open>@{verbatim \<open>(\ x -> [x]) ==> (: [])\<close> } \<close>
 lemma "(\<Lambda> x. [x]) = (\<Lambda> z. z : [])" by auto
 
 text \<open>@{verbatim \<open>True == a ==> a\<close> } \<close>
 lemma "eq\<cdot>TT\<cdot>a = a" by (cases a, auto)
 
 text \<open>@{verbatim \<open>False == a ==> not a\<close> } \<close>
 lemma "eq\<cdot>FF\<cdot>a = neg\<cdot>a" by (cases a, auto)
 
 text \<open>@{verbatim \<open>a /= True ==> not a\<close> } \<close>
 lemma "neq\<cdot>a\<cdot>TT = neg\<cdot>a" by (cases a, auto)
 
 text \<open>@{verbatim \<open>a /= False ==> a\<close> } \<close>
 lemma "neq\<cdot>a\<cdot>FF = a" by (cases a, auto)
 
 text \<open>@{verbatim \<open>True /= a ==> not a\<close> } \<close>
 lemma "neq\<cdot>TT\<cdot>a = neg\<cdot>a" by (cases a, auto)
 
 text \<open>@{verbatim \<open>False /= a ==> a\<close> } \<close>
 lemma "neq\<cdot>FF\<cdot>a = a" by (cases a, auto)
 
 text \<open>@{verbatim \<open>not (isNothing x) ==> isJust x\<close> } \<close>
 lemma "neg\<cdot>(isNothing\<cdot>x) = isJust\<cdot>x" by auto
 
 text \<open>@{verbatim \<open>not (isJust x) ==> isNothing x\<close> } \<close>
 lemma "neg\<cdot>(isJust\<cdot>x) = isNothing\<cdot>x" by auto
 
 text \<open>@{verbatim \<open>x == Nothing ==> isNothing x\<close> } \<close>
 lemma "eq\<cdot>x\<cdot>Nothing = isNothing\<cdot>x" by (cases x, auto)
 
 text \<open>@{verbatim \<open>Nothing == x ==> isNothing x\<close> } \<close>
 lemma "eq\<cdot>Nothing\<cdot>x = isNothing\<cdot>x" by (cases x, auto)
 
 text \<open>@{verbatim \<open>x /= Nothing ==> Data.Maybe.isJust x\<close> } \<close>
 lemma "neq\<cdot>x\<cdot>Nothing = isJust\<cdot>x" by (cases x, auto)
 
 text \<open>@{verbatim \<open>Nothing /= x ==> Data.Maybe.isJust x\<close> } \<close>
 lemma "neq\<cdot>Nothing\<cdot>x = isJust\<cdot>x" by (cases x, auto)
 
 text \<open>@{verbatim \<open>(if isNothing x then y else fromJust x) ==> fromMaybe y x\<close> } \<close>
 lemma "(If isNothing\<cdot>x then y else fromJust\<cdot>x) = fromMaybe\<cdot>y\<cdot>x" by (cases x, auto)
 
 text \<open>@{verbatim \<open>(if isJust x then fromJust x else y) ==> fromMaybe y x\<close> } \<close>
 lemma "(If isJust\<cdot>x then fromJust\<cdot>x else y) = fromMaybe\<cdot>y\<cdot>x" by (cases x, auto)
 
 text \<open>@{verbatim \<open>(isJust x && (fromJust x == y)) ==> x == Just y\<close> } \<close>
 lemma "(isJust\<cdot>x andalso (eq\<cdot>(fromJust\<cdot>x)\<cdot>y)) = eq\<cdot>x\<cdot>(Just\<cdot>y)" by (cases x, auto)
 
 text \<open>@{verbatim \<open>elem True ==> or\<close> } \<close>
 lemma "elem\<cdot>TT = the_or"
 proof (rule cfun_eqI)
   fix xs
   show "elem\<cdot>TT\<cdot>xs = the_or\<cdot>xs"
     by (induct xs) (auto simp: eq_true)
 qed
 
 text \<open>@{verbatim \<open>notElem False ==> and\<close> } \<close>
 lemma "notElem\<cdot>FF = the_and"
 proof (rule cfun_eqI)
   fix xs
   show "notElem\<cdot>FF\<cdot>xs = the_and\<cdot>xs"
     by (induct xs) (auto simp: eq_false)
 qed
 
 text \<open>@{verbatim \<open>all ((/=) a) ==> notElem a\<close> } \<close>
 lemma "all\<cdot>(neq\<cdot>(a::'a::Eq_sym)) = notElem\<cdot>a"
 proof (rule cfun_eqI)
   fix xs
   show "all\<cdot>(neq\<cdot>a)\<cdot>xs = notElem\<cdot>a\<cdot>xs"
     by (induct xs) (auto simp: eq_sym)
 qed
 
 text \<open>@{verbatim \<open>maybe x id ==> Data.Maybe.fromMaybe x\<close> } \<close>
 lemma "maybe\<cdot>x\<cdot>ID = fromMaybe\<cdot>x"
 proof (rule cfun_eqI)
   fix xs
   show "maybe\<cdot>x\<cdot>ID\<cdot>xs = fromMaybe\<cdot>x\<cdot>xs"
     by (cases xs) auto
 qed
 
 text \<open>@{verbatim \<open>maybe False (const True) ==> Data.Maybe.isJust\<close> } \<close>
 lemma "maybe\<cdot>FF\<cdot>(const\<cdot>TT) = isJust"
 proof (rule cfun_eqI)
   fix x :: "'a Maybe"
   show "maybe\<cdot>FF\<cdot>(const\<cdot>TT)\<cdot>x = isJust\<cdot>x"
     by (cases x) simp+
 qed
 
 text \<open>@{verbatim \<open>maybe True (const False) ==> Data.Maybe.isNothing\<close> } \<close>
 lemma "maybe\<cdot>TT\<cdot>(const\<cdot>FF) = isNothing"
 proof (rule cfun_eqI)
   fix x :: "'a Maybe"
   show "maybe\<cdot>TT\<cdot>(const\<cdot>FF)\<cdot>x = isNothing\<cdot>x"
     by (cases x) simp+
 qed
 
 text \<open>@{verbatim \<open>maybe [] (: []) ==> maybeToList\<close> } \<close>
 lemma "maybe\<cdot>[]\<cdot>(\<Lambda> z. z : []) = maybeToList"
 proof (rule cfun_eqI)
   fix x :: "'a Maybe"
   show "maybe\<cdot>[]\<cdot>(\<Lambda> z. z : [])\<cdot>x = maybeToList\<cdot>x"
     by (cases x) simp+
 qed
 
 text \<open>@{verbatim \<open>catMaybes (map f x) ==> mapMaybe f x\<close> } \<close>
 lemma "catMaybes\<cdot>(map\<cdot>f\<cdot>x) = mapMaybe\<cdot>f\<cdot>x" by auto
 
 text \<open>@{verbatim \<open>(if isNothing x then y else f (fromJust x)) ==> maybe y f x\<close> } \<close>
 lemma "(If isNothing\<cdot>x then y else f\<cdot>(fromJust\<cdot>x)) = maybe\<cdot>y\<cdot>f\<cdot>x" by (cases x, auto)
 
 text \<open>@{verbatim \<open>(if isJust x then f (fromJust x) else y) ==> maybe y f x\<close> } \<close>
 lemma "(If isJust\<cdot>x then f\<cdot>(fromJust\<cdot>x) else y) = maybe\<cdot>y\<cdot>f\<cdot>x" by (cases x, auto)
 
 text \<open>@{verbatim \<open>(map fromJust . filter isJust) ==> Data.Maybe.catMaybes\<close> } \<close>
 lemma "(map\<cdot>fromJust oo filter\<cdot>isJust) = catMaybes"
 proof (rule cfun_eqI)
   fix xs :: "['a Maybe]"
   show "(map\<cdot>fromJust oo filter\<cdot>isJust)\<cdot>xs = catMaybes\<cdot>xs"
   proof (induct xs)
     case (Cons y ys)
     then show ?case by (cases y) simp+
   qed simp+
 qed
 
 text \<open>@{verbatim \<open>concatMap (maybeToList . f) ==> Data.Maybe.mapMaybe f\<close> } \<close>
 lemma "concatMap\<cdot>(maybeToList oo f) = mapMaybe\<cdot>f"
 proof (rule cfun_eqI)
   fix xs
   show "concatMap\<cdot>(maybeToList oo f)\<cdot>xs = mapMaybe\<cdot>f\<cdot>xs"
     by (induct xs) auto
 qed
 
 text \<open>@{verbatim \<open>concatMap maybeToList ==> catMaybes\<close> } \<close>
 lemma "concatMap\<cdot>maybeToList = catMaybes" by auto
 
 text \<open>@{verbatim \<open>mapMaybe f (map g x) ==> mapMaybe (f . g) x\<close> } \<close>
 lemma "mapMaybe\<cdot>f\<cdot>(map\<cdot>g\<cdot>x) = mapMaybe\<cdot>(f oo g)\<cdot>x" by auto
 
 text \<open>@{verbatim \<open>(($) . f) ==> f\<close> } \<close>
 lemma "(dollar oo f) = f" by (auto simp add:cfun_eq_iff)
 
 text \<open>@{verbatim \<open>(f $) ==> f\<close> } \<close>
 lemma "(\<Lambda> z. dollar\<cdot>f\<cdot>z) = f" by (auto simp add:cfun_eq_iff)
 
 text \<open>@{verbatim \<open>(\ a b -> g (f a) (f b)) ==> g `Data.Function.on` f\<close> } \<close>
 lemma "(\<Lambda> a b. g\<cdot>(f\<cdot>a)\<cdot>(f\<cdot>b)) = on\<cdot>g\<cdot>f" by (auto simp add:cfun_eq_iff)
 
 text \<open>@{verbatim \<open>id $! x ==> x\<close> } \<close>
 lemma "dollarBang\<cdot>ID\<cdot>x = x" by (auto simp add:seq_def)
 
 text \<open>@{verbatim \<open>[x | x <- y] ==> y\<close> } \<close>
 lemma "[x | x <- y] = y" by (induct y, auto)
 
 text \<open>@{verbatim \<open>isPrefixOf (reverse x) (reverse y) ==> isSuffixOf x y\<close> } \<close>
 lemma "isPrefixOf\<cdot>(reverse\<cdot>x)\<cdot>(reverse\<cdot>y) = isSuffixOf\<cdot>x\<cdot>y" by auto
 
 text \<open>@{verbatim \<open>concat (intersperse x y) ==> intercalate x y\<close> } \<close>
 lemma "concat\<cdot>(intersperse\<cdot>x\<cdot>y) = intercalate\<cdot>x\<cdot>y" by auto
 
 text \<open>@{verbatim \<open>x `seq` y ==> y\<close> } \<close>
 lemma
   assumes "x \<noteq> \<bottom>" shows "seq\<cdot>x\<cdot>y = y"
   using assms by (simp add: seq_def)
 
 text \<open>@{verbatim \<open>f $! x ==> f x\<close> } \<close>
 lemma assumes "x \<noteq> \<bottom>" shows "dollarBang\<cdot>f\<cdot>x = f\<cdot>x"
   using assms by (simp add: seq_def)
 
 text \<open>@{verbatim \<open>maybe (f x) (f . g) ==> (f . maybe x g)\<close> } \<close>
 lemma "maybe\<cdot>(f\<cdot>x)\<cdot>(f oo g) \<sqsubseteq> (f oo maybe\<cdot>x\<cdot>g)"
 proof (rule cfun_belowI)
   fix y
   show "maybe\<cdot>(f\<cdot>x)\<cdot>(f oo g)\<cdot>y \<sqsubseteq> (f oo maybe\<cdot>x\<cdot>g)\<cdot>y"
     by (cases y) auto
 qed
 
 end