tuned proofs
authorhaftmann
Thu Mar 13 08:56:08 2014 +0100 (2014-03-13)
changeset 56077d397030fb27e
parent 56076 e52fc7c37ed3
child 56078 624faeda77b5
child 56113 e3b8f8319d73
tuned proofs
src/HOL/BNF_Cardinal_Order_Relation.thy
src/HOL/BNF_Constructions_on_Wellorders.thy
src/HOL/Basic_BNFs.thy
src/HOL/Fun.thy
src/HOL/Product_Type.thy
src/HOL/Set.thy
     1.1 --- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Thu Mar 13 08:56:08 2014 +0100
     1.2 +++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Thu Mar 13 08:56:08 2014 +0100
     1.3 @@ -600,7 +600,7 @@
     1.4  shows "|B| \<le>o |B \<times> A|"
     1.5  proof(cases "B = {}", simp add: card_of_empty)
     1.6    assume *: "B \<noteq> {}"
     1.7 -  have "fst `(B \<times> A) = B" unfolding image_def using assms by auto
     1.8 +  have "fst `(B \<times> A) = B" using assms by auto
     1.9    thus ?thesis using inj_on_iff_surj[of B "B \<times> A"]
    1.10                       card_of_ordLeq[of B "B \<times> A"] * by blast
    1.11  qed
    1.12 @@ -1652,7 +1652,7 @@
    1.13      hence "\<forall> a. \<exists> b. h a = b" unfolding Func_def by auto
    1.14      then obtain f where f: "\<forall> a. h a = f a" by blast
    1.15      hence "range f \<subseteq> B" using h unfolding Func_def by auto
    1.16 -    thus "h \<in> (\<lambda>f a. f a) ` {f. range f \<subseteq> B}" using f unfolding image_def by auto
    1.17 +    thus "h \<in> (\<lambda>f a. f a) ` {f. range f \<subseteq> B}" using f by auto
    1.18    qed(unfold Func_def fun_eq_iff, auto)
    1.19  qed
    1.20  
     2.1 --- a/src/HOL/BNF_Constructions_on_Wellorders.thy	Thu Mar 13 08:56:08 2014 +0100
     2.2 +++ b/src/HOL/BNF_Constructions_on_Wellorders.thy	Thu Mar 13 08:56:08 2014 +0100
     2.3 @@ -1653,9 +1653,9 @@
     2.4        qed(insert h, unfold Func_def Func_map_def, auto)
     2.5      qed
     2.6      moreover have "g \<in> Func A2 A1" unfolding g_def apply(rule Func_map[OF h])
     2.7 -    using j2A2 B1 A2 unfolding j1_def image_def by (fast intro: inv_into_into)+
     2.8 +    using j2A2 B1 A2 unfolding j1_def by (fast intro: inv_into_into)+
     2.9      ultimately show "h \<in> Func_map B2 f1 f2 ` Func A2 A1"
    2.10 -    unfolding Func_map_def[abs_def] unfolding image_def by auto
    2.11 +    unfolding Func_map_def[abs_def] by auto
    2.12    qed(insert B1 Func_map[OF _ _ A2(2)], auto)
    2.13  qed
    2.14  
     3.1 --- a/src/HOL/Basic_BNFs.thy	Thu Mar 13 08:56:08 2014 +0100
     3.2 +++ b/src/HOL/Basic_BNFs.thy	Thu Mar 13 08:56:08 2014 +0100
     3.3 @@ -175,7 +175,7 @@
     3.4    thus "f \<circ> x = g \<circ> x" by auto
     3.5  next
     3.6    fix f show "range \<circ> op \<circ> f = op ` f \<circ> range"
     3.7 -  unfolding image_def comp_def[abs_def] by auto
     3.8 +    by (auto simp add: fun_eq_iff)
     3.9  next
    3.10    show "card_order (natLeq +c |UNIV| )" (is "_ (_ +c ?U)")
    3.11    apply (rule card_order_csum)
     4.1 --- a/src/HOL/Fun.thy	Thu Mar 13 08:56:08 2014 +0100
     4.2 +++ b/src/HOL/Fun.thy	Thu Mar 13 08:56:08 2014 +0100
     4.3 @@ -159,8 +159,8 @@
     4.4  unfolding inj_on_def by auto
     4.5  
     4.6  lemma inj_on_strict_subset:
     4.7 -  "\<lbrakk> inj_on f B; A < B \<rbrakk> \<Longrightarrow> f`A < f`B"
     4.8 -unfolding inj_on_def unfolding image_def by blast
     4.9 +  "inj_on f B \<Longrightarrow> A \<subset> B \<Longrightarrow> f ` A \<subset> f ` B"
    4.10 +  unfolding inj_on_def by blast
    4.11  
    4.12  lemma inj_comp:
    4.13    "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (f \<circ> g)"
    4.14 @@ -198,16 +198,14 @@
    4.15  by (unfold inj_on_def, blast)
    4.16  
    4.17  lemma inj_on_iff: "[| inj_on f A;  x:A;  y:A |] ==> (f(x)=f(y)) = (x=y)"
    4.18 -by (blast dest!: inj_onD)
    4.19 +  by (fact inj_on_eq_iff)
    4.20  
    4.21  lemma comp_inj_on:
    4.22       "[| inj_on f A;  inj_on g (f`A) |] ==> inj_on (g o f) A"
    4.23  by (simp add: comp_def inj_on_def)
    4.24  
    4.25  lemma inj_on_imageI: "inj_on (g o f) A \<Longrightarrow> inj_on g (f ` A)"
    4.26 -apply(simp add:inj_on_def image_def)
    4.27 -apply blast
    4.28 -done
    4.29 +  by (simp add: inj_on_def) blast
    4.30  
    4.31  lemma inj_on_image_iff: "\<lbrakk> ALL x:A. ALL y:A. (g(f x) = g(f y)) = (g x = g y);
    4.32    inj_on f A \<rbrakk> \<Longrightarrow> inj_on g (f ` A) = inj_on g A"
    4.33 @@ -368,26 +366,26 @@
    4.34      using assms by(auto simp:bij_betw_def)
    4.35    let ?P = "%b a. a:A \<and> f a = b" let ?g = "%b. The (?P b)"
    4.36    { fix a b assume P: "?P b a"
    4.37 -    hence ex1: "\<exists>a. ?P b a" using s unfolding image_def by blast
    4.38 +    hence ex1: "\<exists>a. ?P b a" using s by blast
    4.39      hence uex1: "\<exists>!a. ?P b a" by(blast dest:inj_onD[OF i])
    4.40      hence " ?g b = a" using the1_equality[OF uex1, OF P] P by simp
    4.41    } note g = this
    4.42    have "inj_on ?g B"
    4.43    proof(rule inj_onI)
    4.44      fix x y assume "x:B" "y:B" "?g x = ?g y"
    4.45 -    from s `x:B` obtain a1 where a1: "?P x a1" unfolding image_def by blast
    4.46 -    from s `y:B` obtain a2 where a2: "?P y a2" unfolding image_def by blast
    4.47 +    from s `x:B` obtain a1 where a1: "?P x a1" by blast
    4.48 +    from s `y:B` obtain a2 where a2: "?P y a2" by blast
    4.49      from g[OF a1] a1 g[OF a2] a2 `?g x = ?g y` show "x=y" by simp
    4.50    qed
    4.51    moreover have "?g ` B = A"
    4.52 -  proof(auto simp:image_def)
    4.53 +  proof(auto simp: image_def)
    4.54      fix b assume "b:B"
    4.55 -    with s obtain a where P: "?P b a" unfolding image_def by blast
    4.56 +    with s obtain a where P: "?P b a" by blast
    4.57      thus "?g b \<in> A" using g[OF P] by auto
    4.58    next
    4.59      fix a assume "a:A"
    4.60 -    then obtain b where P: "?P b a" using s unfolding image_def by blast
    4.61 -    then have "b:B" using s unfolding image_def by blast
    4.62 +    then obtain b where P: "?P b a" using s by blast
    4.63 +    then have "b:B" using s by blast
    4.64      with g[OF P] show "\<exists>b\<in>B. a = ?g b" by blast
    4.65    qed
    4.66    ultimately show ?thesis by(auto simp:bij_betw_def)
    4.67 @@ -614,8 +612,9 @@
    4.68  lemma fun_upd_twist: "a ~= c ==> (m(a:=b))(c:=d) = (m(c:=d))(a:=b)"
    4.69  by (rule ext, auto)
    4.70  
    4.71 -lemma inj_on_fun_updI: "\<lbrakk> inj_on f A; y \<notin> f`A \<rbrakk> \<Longrightarrow> inj_on (f(x:=y)) A"
    4.72 -by (fastforce simp:inj_on_def image_def)
    4.73 +lemma inj_on_fun_updI:
    4.74 +  "inj_on f A \<Longrightarrow> y \<notin> f ` A \<Longrightarrow> inj_on (f(x := y)) A"
    4.75 +  by (fastforce simp: inj_on_def)
    4.76  
    4.77  lemma fun_upd_image:
    4.78       "f(x:=y) ` A = (if x \<in> A then insert y (f ` (A-{x})) else f ` A)"
    4.79 @@ -750,7 +749,7 @@
    4.80  
    4.81  lemma inj_on_the_inv_into:
    4.82    "inj_on f A \<Longrightarrow> inj_on (the_inv_into A f) (f ` A)"
    4.83 -by (auto intro: inj_onI simp: image_def the_inv_into_f_f)
    4.84 +by (auto intro: inj_onI simp: the_inv_into_f_f)
    4.85  
    4.86  lemma bij_betw_the_inv_into:
    4.87    "bij_betw f A B \<Longrightarrow> bij_betw (the_inv_into A f) B A"
     5.1 --- a/src/HOL/Product_Type.thy	Thu Mar 13 08:56:08 2014 +0100
     5.2 +++ b/src/HOL/Product_Type.thy	Thu Mar 13 08:56:08 2014 +0100
     5.3 @@ -1125,7 +1125,7 @@
     5.4  
     5.5  lemma swap_product:
     5.6    "(%(i, j). (j, i)) ` (A \<times> B) = B \<times> A"
     5.7 -  by (simp add: split_def image_def) blast
     5.8 +  by (simp add: split_def image_def set_eq_iff)
     5.9  
    5.10  lemma image_split_eq_Sigma:
    5.11    "(\<lambda>x. (f x, g x)) ` A = Sigma (f ` A) (\<lambda>x. g ` (f -` {x} \<inter> A))"
     6.1 --- a/src/HOL/Set.thy	Thu Mar 13 08:56:08 2014 +0100
     6.2 +++ b/src/HOL/Set.thy	Thu Mar 13 08:56:08 2014 +0100
     6.3 @@ -1003,7 +1003,7 @@
     6.4  lemma if_image_distrib [simp]:
     6.5    "(\<lambda>x. if P x then f x else g x) ` S
     6.6      = (f ` (S \<inter> {x. P x})) \<union> (g ` (S \<inter> {x. \<not> P x}))"
     6.7 -  by (auto simp add: image_def)
     6.8 +  by auto
     6.9  
    6.10  lemma image_cong:
    6.11    "M = N \<Longrightarrow> (\<And>x. x \<in> N \<Longrightarrow> f x = g x) \<Longrightarrow> f ` M = g ` N"
    6.12 @@ -1054,7 +1054,7 @@
    6.13  
    6.14  lemma range_composition: 
    6.15    "range (\<lambda>x. f (g x)) = f ` range g"
    6.16 -  by (subst image_image) simp
    6.17 +  by auto
    6.18  
    6.19  
    6.20  subsubsection {* Some rules with @{text "if"} *}