# HG changeset patch
# User haftmann
# Date 1253812458 -7200
# Node ID 304a477394079d32b2286bb57be4e14b296f8214
# Parent  adeac3cbb659ecf46424b56d60d9f253142b4e6a# Parent  8854e892cf3eaa308c0f5837c6bcbc3af114846d
merged

diff -r 8854e892cf3e -r 304a47739407 src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Thu Sep 24 17:26:05 2009 +0200
+++ b/src/HOL/Complete_Lattice.thy	Thu Sep 24 19:14:18 2009 +0200
@@ -10,7 +10,9 @@
   less_eq  (infix "\<sqsubseteq>" 50) and
   less (infix "\<sqsubset>" 50) and
   inf  (infixl "\<sqinter>" 70) and
-  sup  (infixl "\<squnion>" 65)
+  sup  (infixl "\<squnion>" 65) and
+  top ("\<top>") and
+  bot ("\<bottom>")
 
 
 subsection {* Abstract complete lattices *}
@@ -24,6 +26,15 @@
      and Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z) \<Longrightarrow> \<Squnion>A \<sqsubseteq> z"
 begin
 
+term complete_lattice
+
+lemma dual_complete_lattice:
+  "complete_lattice (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom> Sup Inf"
+  by (auto intro!: complete_lattice.intro dual_lattice
+    bot.intro top.intro dual_preorder, unfold_locales)
+      (fact bot_least top_greatest
+        Sup_upper Sup_least Inf_lower Inf_greatest)+
+
 lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<le> a}"
   by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
 
@@ -784,7 +795,9 @@
   inf  (infixl "\<sqinter>" 70) and
   sup  (infixl "\<squnion>" 65) and
   Inf  ("\<Sqinter>_" [900] 900) and
-  Sup  ("\<Squnion>_" [900] 900)
+  Sup  ("\<Squnion>_" [900] 900) and
+  top ("\<top>") and
+  bot ("\<bottom>")
 
 lemmas mem_simps =
   insert_iff empty_iff Un_iff Int_iff Compl_iff Diff_iff
diff -r 8854e892cf3e -r 304a47739407 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Thu Sep 24 17:26:05 2009 +0200
+++ b/src/HOL/Finite_Set.thy	Thu Sep 24 19:14:18 2009 +0200
@@ -2615,6 +2615,23 @@
   finally show ?case .
 qed
 
+lemma fold1_eq_fold_idem:
+  assumes "finite A"
+  shows "fold1 times (insert a A) = fold times a A"
+proof (cases "a \<in> A")
+  case False
+  with assms show ?thesis by (simp add: fold1_eq_fold)
+next
+  interpret fun_left_comm_idem times by (fact fun_left_comm_idem)
+  case True then obtain b B
+    where A: "A = insert a B" and "a \<notin> B" by (rule set_insert)
+  with assms have "finite B" by auto
+  then have "fold times a (insert a B) = fold times (a * a) B"
+    using `a \<notin> B` by (rule fold_insert2)
+  then show ?thesis
+    using `a \<notin> B` `finite B` by (simp add: fold1_eq_fold A)
+qed
+
 end
 
 
diff -r 8854e892cf3e -r 304a47739407 src/HOL/Library/Executable_Set.thy
--- a/src/HOL/Library/Executable_Set.thy	Thu Sep 24 17:26:05 2009 +0200
+++ b/src/HOL/Library/Executable_Set.thy	Thu Sep 24 19:14:18 2009 +0200
@@ -32,9 +32,6 @@
 
 declare inter [code]
 
-declare Inter_image_eq [symmetric, code_unfold]
-declare Union_image_eq [symmetric, code_unfold]
-
 declare List_Set.project_def [symmetric, code_unfold]
 
 definition Inter :: "'a set set \<Rightarrow> 'a set" where
diff -r 8854e892cf3e -r 304a47739407 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Sep 24 17:26:05 2009 +0200
+++ b/src/HOL/List.thy	Thu Sep 24 19:14:18 2009 +0200
@@ -2167,6 +2167,71 @@
   "fold f y (set xs) = foldl (\<lambda>y x. f x y) y xs"
   by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm)
 
+lemma (in ab_semigroup_idem_mult) fold1_set:
+  assumes "xs \<noteq> []"
+  shows "fold1 times (set xs) = foldl times (hd xs) (tl xs)"
+proof -
+  interpret fun_left_comm_idem times by (fact fun_left_comm_idem)
+  from assms obtain y ys where xs: "xs = y # ys"
+    by (cases xs) auto
+  show ?thesis
+  proof (cases "set ys = {}")
+    case True with xs show ?thesis by simp
+  next
+    case False
+    then have "fold1 times (insert y (set ys)) = fold times y (set ys)"
+      by (simp only: finite_set fold1_eq_fold_idem)
+    with xs show ?thesis by (simp add: fold_set mult_commute)
+  qed
+qed
+
+lemma (in lattice) Inf_fin_set_fold [code_unfold]:
+  "Inf_fin (set (x # xs)) = foldl inf x xs"
+proof -
+  interpret ab_semigroup_idem_mult "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
+    by (fact ab_semigroup_idem_mult_inf)
+  show ?thesis
+    by (simp add: Inf_fin_def fold1_set del: set.simps)
+qed
+
+lemma (in lattice) Sup_fin_set_fold [code_unfold]:
+  "Sup_fin (set (x # xs)) = foldl sup x xs"
+proof -
+  interpret ab_semigroup_idem_mult "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
+    by (fact ab_semigroup_idem_mult_sup)
+  show ?thesis
+    by (simp add: Sup_fin_def fold1_set del: set.simps)
+qed
+
+lemma (in linorder) Min_fin_set_fold [code_unfold]:
+  "Min (set (x # xs)) = foldl min x xs"
+proof -
+  interpret ab_semigroup_idem_mult "min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
+    by (fact ab_semigroup_idem_mult_min)
+  show ?thesis
+    by (simp add: Min_def fold1_set del: set.simps)
+qed
+
+lemma (in linorder) Max_fin_set_fold [code_unfold]:
+  "Max (set (x # xs)) = foldl max x xs"
+proof -
+  interpret ab_semigroup_idem_mult "max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
+    by (fact ab_semigroup_idem_mult_max)
+  show ?thesis
+    by (simp add: Max_def fold1_set del: set.simps)
+qed
+
+lemma (in complete_lattice) Inf_set_fold [code_unfold]:
+  "Inf (set xs) = foldl inf top xs"
+  by (cases xs)
+    (simp_all add: Inf_fin_Inf [symmetric] Inf_fin_set_fold
+      inf_commute del: set.simps, simp add: top_def)
+
+lemma (in complete_lattice) Sup_set_fold [code_unfold]:
+  "Sup (set xs) = foldl sup bot xs"
+  by (cases xs)
+    (simp_all add: Sup_fin_Sup [symmetric] Sup_fin_set_fold
+      sup_commute del: set.simps, simp add: bot_def)
 
 
 subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
@@ -3763,6 +3828,11 @@
   "length (remdups xs) = length_unique xs"
   by (induct xs) simp_all
 
+declare INFI_def [code_unfold]
+declare SUPR_def [code_unfold]
+
+declare set_map [symmetric, code_unfold]
+
 hide (open) const length_unique