src/HOL/Finite_Set.thy
changeset 41550 efa734d9b221
parent 40945 b8703f63bfb2
child 41656 011fcb70e32f
     1.1 --- a/src/HOL/Finite_Set.thy	Fri Jan 14 15:43:04 2011 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Fri Jan 14 15:44:47 2011 +0100
     1.3 @@ -803,7 +803,7 @@
     1.4  proof -
     1.5    interpret fun_left_comm_idem inf by (fact fun_left_comm_idem_inf)
     1.6    from `finite A` show ?thesis by (induct A arbitrary: B)
     1.7 -    (simp_all add: Inf_empty Inf_insert inf_commute fold_fun_comm)
     1.8 +    (simp_all add: Inf_insert inf_commute fold_fun_comm)
     1.9  qed
    1.10  
    1.11  lemma sup_Sup_fold_sup:
    1.12 @@ -812,7 +812,7 @@
    1.13  proof -
    1.14    interpret fun_left_comm_idem sup by (fact fun_left_comm_idem_sup)
    1.15    from `finite A` show ?thesis by (induct A arbitrary: B)
    1.16 -    (simp_all add: Sup_empty Sup_insert sup_commute fold_fun_comm)
    1.17 +    (simp_all add: Sup_insert sup_commute fold_fun_comm)
    1.18  qed
    1.19  
    1.20  lemma Inf_fold_inf:
    1.21 @@ -833,7 +833,7 @@
    1.22    interpret fun_left_comm_idem "\<lambda>A. inf (f A)" by (fact fun_left_comm_idem_apply)
    1.23    from `finite A` show "?fold = ?inf"
    1.24    by (induct A arbitrary: B)
    1.25 -    (simp_all add: INFI_def Inf_empty Inf_insert inf_left_commute)
    1.26 +    (simp_all add: INFI_def Inf_insert inf_left_commute)
    1.27  qed
    1.28  
    1.29  lemma sup_SUPR_fold_sup:
    1.30 @@ -844,7 +844,7 @@
    1.31    interpret fun_left_comm_idem "\<lambda>A. sup (f A)" by (fact fun_left_comm_idem_apply)
    1.32    from `finite A` show "?fold = ?sup"
    1.33    by (induct A arbitrary: B)
    1.34 -    (simp_all add: SUPR_def Sup_empty Sup_insert sup_left_commute)
    1.35 +    (simp_all add: SUPR_def Sup_insert sup_left_commute)
    1.36  qed
    1.37  
    1.38  lemma INFI_fold_inf:
    1.39 @@ -1197,19 +1197,19 @@
    1.40      by (auto simp add: nonempty_iff)
    1.41    show ?thesis
    1.42    proof cases
    1.43 -    assume "a = x"
    1.44 -    thus ?thesis
    1.45 +    assume a: "a = x"
    1.46 +    show ?thesis
    1.47      proof cases
    1.48        assume "A' = {}"
    1.49 -      with prems show ?thesis by simp
    1.50 +      with A' a show ?thesis by simp
    1.51      next
    1.52        assume "A' \<noteq> {}"
    1.53 -      with prems show ?thesis
    1.54 +      with A A' a show ?thesis
    1.55          by (simp add: fold1_insert mult_assoc [symmetric])
    1.56      qed
    1.57    next
    1.58      assume "a \<noteq> x"
    1.59 -    with prems show ?thesis
    1.60 +    with A A' show ?thesis
    1.61        by (simp add: insert_commute fold1_eq_fold)
    1.62    qed
    1.63  qed