src/HOL/List.thy
changeset 46635 cde737f9c911
parent 46500 0196966d6d2d
child 46638 fc315796794e
     1.1 --- a/src/HOL/List.thy	Thu Feb 23 21:16:54 2012 +0100
     1.2 +++ b/src/HOL/List.thy	Thu Feb 23 21:25:59 2012 +0100
     1.3 @@ -2662,7 +2662,6 @@
     1.4    by (simp add: Sup_set_fold ac_simps foldr_fold fun_eq_iff)
     1.5  
     1.6  declare Inf_set_foldr [where 'a = "'a set", code] Sup_set_foldr [where 'a = "'a set", code]
     1.7 -declare Inf_set_foldr [where 'a = "'a Predicate.pred", code] Sup_set_foldr [where 'a = "'a Predicate.pred", code]
     1.8  
     1.9  lemma (in complete_lattice) INF_set_foldr [code]:
    1.10    "INFI (set xs) f = foldr (inf \<circ> f) xs top"
    1.11 @@ -2672,29 +2671,6 @@
    1.12    "SUPR (set xs) f = foldr (sup \<circ> f) xs bot"
    1.13    by (simp only: SUP_def Sup_set_foldr foldr_map set_map [symmetric])
    1.14  
    1.15 -(* FIXME: better implement conversion by bisection *)
    1.16 -
    1.17 -lemma pred_of_set_fold_sup:
    1.18 -  assumes "finite A"
    1.19 -  shows "pred_of_set A = Finite_Set.fold sup bot (Predicate.single ` A)" (is "?lhs = ?rhs")
    1.20 -proof (rule sym)
    1.21 -  interpret comp_fun_idem "sup :: 'a Predicate.pred \<Rightarrow> 'a Predicate.pred \<Rightarrow> 'a Predicate.pred"
    1.22 -    by (fact comp_fun_idem_sup)
    1.23 -  from `finite A` show "?rhs = ?lhs" by (induct A) (auto intro!: pred_eqI)
    1.24 -qed
    1.25 -
    1.26 -lemma pred_of_set_set_fold_sup:
    1.27 -  "pred_of_set (set xs) = fold sup (map Predicate.single xs) bot"
    1.28 -proof -
    1.29 -  interpret comp_fun_idem "sup :: 'a Predicate.pred \<Rightarrow> 'a Predicate.pred \<Rightarrow> 'a Predicate.pred"
    1.30 -    by (fact comp_fun_idem_sup)
    1.31 -  show ?thesis by (simp add: pred_of_set_fold_sup fold_set_fold [symmetric])
    1.32 -qed
    1.33 -
    1.34 -lemma pred_of_set_set_foldr_sup [code]:
    1.35 -  "pred_of_set (set xs) = foldr sup (map Predicate.single xs) bot"
    1.36 -  by (simp add: pred_of_set_set_fold_sup ac_simps foldr_fold fun_eq_iff)
    1.37 -
    1.38  
    1.39  subsubsection {* @{text upt} *}
    1.40