src/HOL/List.thy
changeset 42871 1c0b99f950d9
parent 42809 5b45125b15ba
child 43324 2b47822868e4
     1.1 --- a/src/HOL/List.thy	Fri May 20 08:16:56 2011 +0200
     1.2 +++ b/src/HOL/List.thy	Fri May 20 11:44:16 2011 +0200
     1.3 @@ -2478,11 +2478,11 @@
     1.4  
     1.5  text {* @{const Finite_Set.fold} and @{const foldl} *}
     1.6  
     1.7 -lemma (in fun_left_comm) fold_set_remdups:
     1.8 +lemma (in comp_fun_commute) fold_set_remdups:
     1.9    "fold f y (set xs) = foldl (\<lambda>y x. f x y) y (remdups xs)"
    1.10    by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm insert_absorb)
    1.11  
    1.12 -lemma (in fun_left_comm_idem) fold_set:
    1.13 +lemma (in comp_fun_idem) fold_set:
    1.14    "fold f y (set xs) = foldl (\<lambda>y x. f x y) y xs"
    1.15    by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm)
    1.16  
    1.17 @@ -2490,7 +2490,7 @@
    1.18    assumes "xs \<noteq> []"
    1.19    shows "fold1 times (set xs) = foldl times (hd xs) (tl xs)"
    1.20  proof -
    1.21 -  interpret fun_left_comm_idem times by (fact fun_left_comm_idem)
    1.22 +  interpret comp_fun_idem times by (fact comp_fun_idem)
    1.23    from assms obtain y ys where xs: "xs = y # ys"
    1.24      by (cases xs) auto
    1.25    show ?thesis
    1.26 @@ -2543,16 +2543,16 @@
    1.27  lemma (in complete_lattice) Inf_set_fold [code_unfold]:
    1.28    "Inf (set xs) = foldl inf top xs"
    1.29  proof -
    1.30 -  interpret fun_left_comm_idem "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
    1.31 -    by (fact fun_left_comm_idem_inf)
    1.32 +  interpret comp_fun_idem "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
    1.33 +    by (fact comp_fun_idem_inf)
    1.34    show ?thesis by (simp add: Inf_fold_inf fold_set inf_commute)
    1.35  qed
    1.36  
    1.37  lemma (in complete_lattice) Sup_set_fold [code_unfold]:
    1.38    "Sup (set xs) = foldl sup bot xs"
    1.39  proof -
    1.40 -  interpret fun_left_comm_idem "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
    1.41 -    by (fact fun_left_comm_idem_sup)
    1.42 +  interpret comp_fun_idem "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
    1.43 +    by (fact comp_fun_idem_sup)
    1.44    show ?thesis by (simp add: Sup_fold_sup fold_set sup_commute)
    1.45  qed
    1.46  
    1.47 @@ -3762,8 +3762,8 @@
    1.48    "insort x (insort y xs) = insort y (insort x xs)"
    1.49    by (cases "x = y") (auto intro: insort_key_left_comm)
    1.50  
    1.51 -lemma fun_left_comm_insort:
    1.52 -  "fun_left_comm insort"
    1.53 +lemma comp_fun_commute_insort:
    1.54 +  "comp_fun_commute insort"
    1.55  proof
    1.56  qed (simp add: insort_left_comm fun_eq_iff)
    1.57  
    1.58 @@ -4249,7 +4249,7 @@
    1.59    assumes "finite A"
    1.60    shows "sorted_list_of_set (insert x A) = insort x (sorted_list_of_set (A - {x}))"
    1.61  proof -
    1.62 -  interpret fun_left_comm insort by (fact fun_left_comm_insort)
    1.63 +  interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
    1.64    with assms show ?thesis by (simp add: sorted_list_of_set_def fold_insert_remove)
    1.65  qed
    1.66  
    1.67 @@ -4261,7 +4261,7 @@
    1.68  lemma sorted_list_of_set_sort_remdups:
    1.69    "sorted_list_of_set (set xs) = sort (remdups xs)"
    1.70  proof -
    1.71 -  interpret fun_left_comm insort by (fact fun_left_comm_insort)
    1.72 +  interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
    1.73    show ?thesis by (simp add: sort_foldl_insort sorted_list_of_set_def fold_set_remdups)
    1.74  qed
    1.75