use point-free characterization for locale fun_left_comm_idem
authorhaftmann
Fri May 20 08:16:56 2011 +0200 (2011-05-20)
changeset 4286943b0f61f56d0
parent 42868 1608daf27c1f
child 42870 36abaf4cce1f
child 42871 1c0b99f950d9
use point-free characterization for locale fun_left_comm_idem
src/HOL/Finite_Set.thy
src/HOL/Multivariate_Analysis/Integration.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Fri May 20 08:16:13 2011 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Fri May 20 08:16:56 2011 +0200
     1.3 @@ -672,12 +672,11 @@
     1.4  text{* A simplified version for idempotent functions: *}
     1.5  
     1.6  locale fun_left_comm_idem = fun_left_comm +
     1.7 -  assumes fun_left_idem: "f x (f x z) = f x z"
     1.8 +  assumes fun_comp_idem: "f x o f x = f x"
     1.9  begin
    1.10  
    1.11 -text{* The nice version: *}
    1.12 -lemma fun_comp_idem : "f x o f x = f x"
    1.13 -by (simp add: fun_left_idem fun_eq_iff)
    1.14 +lemma fun_left_idem: "f x (f x z) = f x z"
    1.15 +  using fun_comp_idem by (simp add: fun_eq_iff)
    1.16  
    1.17  lemma fold_insert_idem:
    1.18    assumes fin: "finite A"
    1.19 @@ -701,15 +700,15 @@
    1.20  
    1.21  subsubsection {* Expressing set operations via @{const fold} *}
    1.22  
    1.23 -lemma (in fun_left_comm) fun_left_comm_apply:
    1.24 -  "fun_left_comm (\<lambda>x. f (g x))"
    1.25 +lemma (in fun_left_comm) comp_comp_fun_commute:
    1.26 +  "fun_left_comm (f \<circ> g)"
    1.27  proof
    1.28  qed (simp_all add: commute_comp)
    1.29  
    1.30 -lemma (in fun_left_comm_idem) fun_left_comm_idem_apply:
    1.31 -  "fun_left_comm_idem (\<lambda>x. f (g x))"
    1.32 -  by (rule fun_left_comm_idem.intro, rule fun_left_comm_apply, unfold_locales)
    1.33 -    (simp_all add: fun_left_idem)
    1.34 +lemma (in fun_left_comm_idem) comp_comp_fun_idem:
    1.35 +  "fun_left_comm_idem (f \<circ> g)"
    1.36 +  by (rule fun_left_comm_idem.intro, rule comp_comp_fun_commute, unfold_locales)
    1.37 +    (simp_all add: fun_comp_idem)
    1.38  
    1.39  lemma fun_left_comm_idem_insert:
    1.40    "fun_left_comm_idem insert"
    1.41 @@ -783,10 +782,11 @@
    1.42    shows "inf B (INFI A f) = fold (\<lambda>A. inf (f A)) B A" (is "?inf = ?fold") 
    1.43  proof (rule sym)
    1.44    interpret fun_left_comm_idem inf by (fact fun_left_comm_idem_inf)
    1.45 -  interpret fun_left_comm_idem "\<lambda>A. inf (f A)" by (fact fun_left_comm_idem_apply)
    1.46 -  from `finite A` show "?fold = ?inf"
    1.47 -  by (induct A arbitrary: B)
    1.48 -    (simp_all add: INFI_def Inf_insert inf_left_commute)
    1.49 +  interpret fun_left_comm_idem "inf \<circ> f" by (fact comp_comp_fun_idem)
    1.50 +  from `finite A` have "fold (inf \<circ> f) B A = ?inf"
    1.51 +    by (induct A arbitrary: B)
    1.52 +      (simp_all add: INFI_def Inf_insert inf_left_commute)
    1.53 +  then show "?fold = ?inf" by (simp add: comp_def)
    1.54  qed
    1.55  
    1.56  lemma sup_SUPR_fold_sup:
    1.57 @@ -794,10 +794,11 @@
    1.58    shows "sup B (SUPR A f) = fold (\<lambda>A. sup (f A)) B A" (is "?sup = ?fold") 
    1.59  proof (rule sym)
    1.60    interpret fun_left_comm_idem sup by (fact fun_left_comm_idem_sup)
    1.61 -  interpret fun_left_comm_idem "\<lambda>A. sup (f A)" by (fact fun_left_comm_idem_apply)
    1.62 -  from `finite A` show "?fold = ?sup"
    1.63 -  by (induct A arbitrary: B)
    1.64 -    (simp_all add: SUPR_def Sup_insert sup_left_commute)
    1.65 +  interpret fun_left_comm_idem "sup \<circ> f" by (fact comp_comp_fun_idem)
    1.66 +  from `finite A` have "fold (sup \<circ> f) B A = ?sup"
    1.67 +    by (induct A arbitrary: B)
    1.68 +      (simp_all add: SUPR_def Sup_insert sup_left_commute)
    1.69 +  then show "?fold = ?sup" by (simp add: comp_def)
    1.70  qed
    1.71  
    1.72  lemma INFI_fold_inf:
    1.73 @@ -1138,7 +1139,7 @@
    1.74  begin
    1.75  
    1.76  lemma fun_left_comm_idem: "fun_left_comm_idem (op *)" proof
    1.77 -qed (simp add: fun_eq_iff mult_left_commute, rule mult_left_idem)
    1.78 +qed (simp_all add: fun_eq_iff mult_left_commute)
    1.79  
    1.80  lemma fold1_insert_idem [simp]:
    1.81    assumes nonempty: "A \<noteq> {}" and A: "finite A" 
     2.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Fri May 20 08:16:13 2011 +0200
     2.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Fri May 20 08:16:56 2011 +0200
     2.3 @@ -1850,12 +1850,12 @@
     2.4  proof(cases "x\<in>s") case True hence *:"insert x s = s" by auto
     2.5    show ?thesis unfolding iterate_def if_P[OF True] * by auto
     2.6  next case False note x=this
     2.7 -  note * = fun_left_comm.fun_left_comm_apply[OF fun_left_comm_monoidal[OF assms(1)]]
     2.8 +  note * = fun_left_comm.comp_comp_fun_commute [OF fun_left_comm_monoidal[OF assms(1)]]
     2.9    show ?thesis proof(cases "f x = neutral opp")
    2.10      case True show ?thesis unfolding iterate_def if_not_P[OF x] support_clauses if_P[OF True]
    2.11        unfolding True monoidal_simps[OF assms(1)] by auto
    2.12    next case False show ?thesis unfolding iterate_def fold'_def  if_not_P[OF x] support_clauses if_not_P[OF False]
    2.13 -      apply(subst fun_left_comm.fold_insert[OF * finite_support])
    2.14 +      apply(subst fun_left_comm.fold_insert[OF * finite_support, simplified comp_def])
    2.15        using `finite s` unfolding support_def using False x by auto qed qed 
    2.16  
    2.17  lemma iterate_some: