tune proofs
authornoschinl
Tue Sep 13 16:22:01 2011 +0200 (2011-09-13)
changeset 44919482f1807976e
parent 44918 6a80fbc4e72c
child 44920 4657b4c11138
tune proofs
src/HOL/Complete_Lattices.thy
src/HOL/Finite_Set.thy
src/HOL/Lattices.thy
     1.1 --- a/src/HOL/Complete_Lattices.thy	Tue Sep 13 16:21:48 2011 +0200
     1.2 +++ b/src/HOL/Complete_Lattices.thy	Tue Sep 13 16:22:01 2011 +0200
     1.3 @@ -164,13 +164,13 @@
     1.4    by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
     1.5  
     1.6  lemma INF_insert: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> INFI A f"
     1.7 -  by (simp add: INF_def Inf_insert)
     1.8 +  by (simp add: INF_def)
     1.9  
    1.10  lemma Sup_insert [simp]: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
    1.11    by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper)
    1.12  
    1.13  lemma SUP_insert: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> SUPR A f"
    1.14 -  by (simp add: SUP_def Sup_insert)
    1.15 +  by (simp add: SUP_def)
    1.16  
    1.17  lemma INF_image [simp]: "(\<Sqinter>x\<in>f`A. g x) = (\<Sqinter>x\<in>A. g (f x))"
    1.18    by (simp add: INF_def image_image)
    1.19 @@ -293,7 +293,7 @@
    1.20    proof
    1.21      assume "\<forall>x\<in>A. x = \<top>"
    1.22      then have "A = {} \<or> A = {\<top>}" by auto
    1.23 -    then show "\<Sqinter>A = \<top>" by (auto simp add: Inf_insert)
    1.24 +    then show "\<Sqinter>A = \<top>" by auto
    1.25    next
    1.26      assume "\<Sqinter>A = \<top>"
    1.27      show "\<forall>x\<in>A. x = \<top>"
    1.28 @@ -301,7 +301,7 @@
    1.29        assume "\<not> (\<forall>x\<in>A. x = \<top>)"
    1.30        then obtain x where "x \<in> A" and "x \<noteq> \<top>" by blast
    1.31        then obtain B where "A = insert x B" by blast
    1.32 -      with `\<Sqinter>A = \<top>` `x \<noteq> \<top>` show False by (simp add: Inf_insert)
    1.33 +      with `\<Sqinter>A = \<top>` `x \<noteq> \<top>` show False by simp
    1.34      qed
    1.35    qed
    1.36    then show "\<top> = \<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)" by auto
    1.37 @@ -310,7 +310,7 @@
    1.38  lemma INF_top_conv [simp]:
    1.39   "(\<Sqinter>x\<in>A. B x) = \<top> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
    1.40   "\<top> = (\<Sqinter>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
    1.41 -  by (auto simp add: INF_def Inf_top_conv)
    1.42 +  by (auto simp add: INF_def)
    1.43  
    1.44  lemma Sup_bot_conv [simp, no_atp]:
    1.45    "\<Squnion>A = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)" (is ?P)
    1.46 @@ -324,7 +324,7 @@
    1.47  lemma SUP_bot_conv [simp]:
    1.48   "(\<Squnion>x\<in>A. B x) = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
    1.49   "\<bottom> = (\<Squnion>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
    1.50 -  by (auto simp add: SUP_def Sup_bot_conv)
    1.51 +  by (auto simp add: SUP_def)
    1.52  
    1.53  lemma INF_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Sqinter>i\<in>A. f) = f"
    1.54    by (auto intro: antisym INF_lower INF_greatest)
    1.55 @@ -420,7 +420,7 @@
    1.56  subclass distrib_lattice proof
    1.57    fix a b c
    1.58    from sup_Inf have "a \<squnion> \<Sqinter>{b, c} = (\<Sqinter>d\<in>{b, c}. a \<squnion> d)" .
    1.59 -  then show "a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c)" by (simp add: INF_def Inf_insert)
    1.60 +  then show "a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c)" by (simp add: INF_def)
    1.61  qed
    1.62  
    1.63  lemma Inf_sup:
    1.64 @@ -535,7 +535,7 @@
    1.65  
    1.66  lemma SUP_eq_top_iff [simp]:
    1.67    "(\<Squnion>i\<in>A. f i) = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < f i)"
    1.68 -  unfolding SUP_def Sup_eq_top_iff by auto
    1.69 +  unfolding SUP_def by auto
    1.70  
    1.71  lemma Inf_eq_bot_iff [simp]:
    1.72    "\<Sqinter>A = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. i < x)"
    1.73 @@ -547,7 +547,7 @@
    1.74  
    1.75  lemma INF_eq_bot_iff [simp]:
    1.76    "(\<Sqinter>i\<in>A. f i) = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. f i < x)"
    1.77 -  unfolding INF_def Inf_eq_bot_iff by auto
    1.78 +  unfolding INF_def by auto
    1.79  
    1.80  end
    1.81  
    1.82 @@ -1152,19 +1152,19 @@
    1.83  
    1.84  lemma (in complete_lattice) Inf_singleton [simp]:
    1.85    "\<Sqinter>{a} = a"
    1.86 -  by (simp add: Inf_insert)
    1.87 +  by simp
    1.88  
    1.89  lemma (in complete_lattice) Sup_singleton [simp]:
    1.90    "\<Squnion>{a} = a"
    1.91 -  by (simp add: Sup_insert)
    1.92 +  by simp
    1.93  
    1.94  lemma (in complete_lattice) Inf_binary:
    1.95    "\<Sqinter>{a, b} = a \<sqinter> b"
    1.96 -  by (simp add: Inf_insert)
    1.97 +  by simp
    1.98  
    1.99  lemma (in complete_lattice) Sup_binary:
   1.100    "\<Squnion>{a, b} = a \<squnion> b"
   1.101 -  by (simp add: Sup_insert)
   1.102 +  by simp
   1.103  
   1.104  lemmas (in complete_lattice) INFI_def = INF_def
   1.105  lemmas (in complete_lattice) SUPR_def = SUP_def
   1.106 @@ -1202,7 +1202,7 @@
   1.107    by (fact SUP_def)
   1.108  
   1.109  lemma Int_eq_Inter: "A \<inter> B = \<Inter>{A, B}"
   1.110 -  by (simp add: Inf_insert)
   1.111 +  by simp
   1.112  
   1.113  lemma INTER_eq_Inter_image:
   1.114    "(\<Inter>x\<in>A. B x) = \<Inter>(B`A)"
     2.1 --- a/src/HOL/Finite_Set.thy	Tue Sep 13 16:21:48 2011 +0200
     2.2 +++ b/src/HOL/Finite_Set.thy	Tue Sep 13 16:22:01 2011 +0200
     2.3 @@ -754,7 +754,7 @@
     2.4  proof -
     2.5    interpret comp_fun_idem inf by (fact comp_fun_idem_inf)
     2.6    from `finite A` show ?thesis by (induct A arbitrary: B)
     2.7 -    (simp_all add: Inf_insert inf_commute fold_fun_comm)
     2.8 +    (simp_all add: inf_commute fold_fun_comm)
     2.9  qed
    2.10  
    2.11  lemma sup_Sup_fold_sup:
    2.12 @@ -763,7 +763,7 @@
    2.13  proof -
    2.14    interpret comp_fun_idem sup by (fact comp_fun_idem_sup)
    2.15    from `finite A` show ?thesis by (induct A arbitrary: B)
    2.16 -    (simp_all add: Sup_insert sup_commute fold_fun_comm)
    2.17 +    (simp_all add: sup_commute fold_fun_comm)
    2.18  qed
    2.19  
    2.20  lemma Inf_fold_inf:
    2.21 @@ -784,7 +784,7 @@
    2.22    interpret comp_fun_idem "inf \<circ> f" by (fact comp_comp_fun_idem)
    2.23    from `finite A` show "?fold = ?inf"
    2.24      by (induct A arbitrary: B)
    2.25 -      (simp_all add: INFI_def Inf_insert inf_left_commute)
    2.26 +      (simp_all add: INFI_def inf_left_commute)
    2.27  qed
    2.28  
    2.29  lemma sup_SUPR_fold_sup:
    2.30 @@ -795,7 +795,7 @@
    2.31    interpret comp_fun_idem "sup \<circ> f" by (fact comp_comp_fun_idem)
    2.32    from `finite A` show "?fold = ?sup"
    2.33      by (induct A arbitrary: B)
    2.34 -      (simp_all add: SUPR_def Sup_insert sup_left_commute)
    2.35 +      (simp_all add: SUPR_def sup_left_commute)
    2.36  qed
    2.37  
    2.38  lemma INFI_fold_inf:
     3.1 --- a/src/HOL/Lattices.thy	Tue Sep 13 16:21:48 2011 +0200
     3.2 +++ b/src/HOL/Lattices.thy	Tue Sep 13 16:22:01 2011 +0200
     3.3 @@ -271,7 +271,7 @@
     3.4    also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))"
     3.5      by (simp add: D inf_commute sup_assoc del: sup_inf_absorb)
     3.6    also have "\<dots> = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)"
     3.7 -    by(simp add:inf_sup_absorb inf_commute)
     3.8 +    by(simp add: inf_commute)
     3.9    also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by(simp add:D)
    3.10    finally show ?thesis .
    3.11  qed
    3.12 @@ -284,7 +284,7 @@
    3.13    also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))"
    3.14      by (simp add: D sup_commute inf_assoc del: inf_sup_absorb)
    3.15    also have "\<dots> = ((x \<sqinter> y) \<squnion> x) \<sqinter> ((x \<sqinter> y) \<squnion> z)"
    3.16 -    by(simp add:sup_inf_absorb sup_commute)
    3.17 +    by(simp add: sup_commute)
    3.18    also have "\<dots> = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" by(simp add:D)
    3.19    finally show ?thesis .
    3.20  qed
    3.21 @@ -547,7 +547,7 @@
    3.22  
    3.23  lemma compl_less_compl_iff: (* TODO: declare [simp] ? *)
    3.24    "- x \<sqsubset> - y \<longleftrightarrow> y \<sqsubset> x"
    3.25 -  by (auto simp add: less_le compl_le_compl_iff)
    3.26 +  by (auto simp add: less_le)
    3.27  
    3.28  lemma compl_less_swap1:
    3.29    assumes "y \<sqsubset> - x" shows "x \<sqsubset> - y"