src/HOL/Product_Type.thy
changeset 44921 58eef4843641
parent 44066 d74182c93f04
child 45175 ae8411edd939
child 45204 5e4a1270c000
     1.1 --- a/src/HOL/Product_Type.thy	Tue Sep 13 08:21:51 2011 -0700
     1.2 +++ b/src/HOL/Product_Type.thy	Tue Sep 13 17:07:33 2011 -0700
     1.3 @@ -830,10 +830,10 @@
     1.4    by (simp add: scomp_unfold prod_case_unfold)
     1.5  
     1.6  lemma Pair_scomp: "Pair x \<circ>\<rightarrow> f = f x"
     1.7 -  by (simp add: fun_eq_iff scomp_apply)
     1.8 +  by (simp add: fun_eq_iff)
     1.9  
    1.10  lemma scomp_Pair: "x \<circ>\<rightarrow> Pair = x"
    1.11 -  by (simp add: fun_eq_iff scomp_apply)
    1.12 +  by (simp add: fun_eq_iff)
    1.13  
    1.14  lemma scomp_scomp: "(f \<circ>\<rightarrow> g) \<circ>\<rightarrow> h = f \<circ>\<rightarrow> (\<lambda>x. g x \<circ>\<rightarrow> h)"
    1.15    by (simp add: fun_eq_iff scomp_unfold)
    1.16 @@ -842,7 +842,7 @@
    1.17    by (simp add: fun_eq_iff scomp_unfold fcomp_def)
    1.18  
    1.19  lemma fcomp_scomp: "(f \<circ>> g) \<circ>\<rightarrow> h = f \<circ>> (g \<circ>\<rightarrow> h)"
    1.20 -  by (simp add: fun_eq_iff scomp_unfold fcomp_apply)
    1.21 +  by (simp add: fun_eq_iff scomp_unfold)
    1.22  
    1.23  code_const scomp
    1.24    (Eval infixl 3 "#->")
    1.25 @@ -863,7 +863,7 @@
    1.26    by (simp add: map_pair_def)
    1.27  
    1.28  enriched_type map_pair: map_pair
    1.29 -  by (auto simp add: split_paired_all intro: ext)
    1.30 +  by (auto simp add: split_paired_all)
    1.31  
    1.32  lemma fst_map_pair [simp]:
    1.33    "fst (map_pair f g x) = f (fst x)"
    1.34 @@ -1110,10 +1110,10 @@
    1.35    by auto
    1.36  
    1.37  lemma fst_image_times[simp]: "fst ` (A \<times> B) = (if B = {} then {} else A)"
    1.38 -  by (auto intro!: image_eqI)
    1.39 +  by force
    1.40  
    1.41  lemma snd_image_times[simp]: "snd ` (A \<times> B) = (if A = {} then {} else B)"
    1.42 -  by (auto intro!: image_eqI)
    1.43 +  by force
    1.44  
    1.45  lemma insert_times_insert[simp]:
    1.46    "insert a A \<times> insert b B =