--- a/NEWS Sat Sep 19 07:35:27 2009 +0200
+++ b/NEWS Sat Sep 19 07:38:11 2009 +0200
@@ -87,6 +87,8 @@
- mere abbreviations:
Set.empty (for bot)
Set.UNIV (for top)
+ Set.inter (for inf)
+ Set.union (for sup)
Complete_Lattice.Inter (for Inf)
Complete_Lattice.Union (for Sup)
Complete_Lattice.INTER (for INFI)
--- a/src/HOL/Finite_Set.thy Sat Sep 19 07:35:27 2009 +0200
+++ b/src/HOL/Finite_Set.thy Sat Sep 19 07:38:11 2009 +0200
@@ -1566,8 +1566,6 @@
prefer 2
apply assumption
apply auto
- apply (rule setsum_cong)
- apply auto
done
lemma setsum_right_distrib:
--- a/src/HOL/Inductive.thy Sat Sep 19 07:35:27 2009 +0200
+++ b/src/HOL/Inductive.thy Sat Sep 19 07:38:11 2009 +0200
@@ -83,7 +83,7 @@
and indhyp: "!!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x)"
shows "P(a)"
by (rule lfp_induct [THEN subsetD, THEN CollectD, OF mono _ lfp])
- (auto simp: inf_set_eq intro: indhyp)
+ (auto simp: intro: indhyp)
lemma lfp_ordinal_induct:
fixes f :: "'a\<Colon>complete_lattice \<Rightarrow> 'a"
@@ -184,7 +184,7 @@
text{*strong version, thanks to Coen and Frost*}
lemma coinduct_set: "[| mono(f); a: X; X \<subseteq> f(X Un gfp(f)) |] ==> a : gfp(f)"
-by (blast intro: weak_coinduct [OF _ coinduct_lemma, simplified sup_set_eq])
+by (blast intro: weak_coinduct [OF _ coinduct_lemma])
lemma coinduct: "[| mono(f); X \<le> f (sup X (gfp f)) |] ==> X \<le> gfp(f)"
apply (rule order_trans)
--- a/src/HOL/Library/Executable_Set.thy Sat Sep 19 07:35:27 2009 +0200
+++ b/src/HOL/Library/Executable_Set.thy Sat Sep 19 07:38:11 2009 +0200
@@ -12,6 +12,21 @@
declare member [code]
+definition empty :: "'a set" where
+ "empty = {}"
+
+declare empty_def [symmetric, code_unfold]
+
+definition inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
+ "inter = op \<inter>"
+
+declare inter_def [symmetric, code_unfold]
+
+definition union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
+ "union = op \<union>"
+
+declare union_def [symmetric, code_unfold]
+
definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
"subset = op \<le>"
@@ -69,7 +84,7 @@
Set ("\<module>Set")
consts_code
- "Set.empty" ("{*Fset.empty*}")
+ "empty" ("{*Fset.empty*}")
"List_Set.is_empty" ("{*Fset.is_empty*}")
"Set.insert" ("{*Fset.insert*}")
"List_Set.remove" ("{*Fset.remove*}")
@@ -77,8 +92,8 @@
"List_Set.project" ("{*Fset.filter*}")
"Ball" ("{*flip Fset.forall*}")
"Bex" ("{*flip Fset.exists*}")
- "op \<union>" ("{*Fset.union*}")
- "op \<inter>" ("{*Fset.inter*}")
+ "union" ("{*Fset.union*}")
+ "inter" ("{*Fset.inter*}")
"op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{*flip Fset.subtract*}")
"Union" ("{*Fset.Union*}")
"Inter" ("{*Fset.Inter*}")
--- a/src/HOL/Set.thy Sat Sep 19 07:35:27 2009 +0200
+++ b/src/HOL/Set.thy Sat Sep 19 07:38:11 2009 +0200
@@ -652,8 +652,8 @@
subsubsection {* Binary union -- Un *}
-definition union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Un" 65) where
- sup_set_eq [symmetric]: "A Un B = sup A B"
+abbreviation union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Un" 65) where
+ "op Un \<equiv> sup"
notation (xsymbols)
union (infixl "\<union>" 65)
@@ -663,7 +663,7 @@
lemma Un_def:
"A \<union> B = {x. x \<in> A \<or> x \<in> B}"
- by (simp add: sup_fun_eq sup_bool_eq sup_set_eq [symmetric] Collect_def mem_def)
+ by (simp add: sup_fun_eq sup_bool_eq Collect_def mem_def)
lemma Un_iff [simp]: "(c : A Un B) = (c:A | c:B)"
by (unfold Un_def) blast
@@ -689,15 +689,13 @@
by (simp add: Collect_def mem_def insert_compr Un_def)
lemma mono_Un: "mono f \<Longrightarrow> f A \<union> f B \<subseteq> f (A \<union> B)"
- apply (fold sup_set_eq)
- apply (erule mono_sup)
- done
+ by (fact mono_sup)
subsubsection {* Binary intersection -- Int *}
-definition inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
- inf_set_eq [symmetric]: "A Int B = inf A B"
+abbreviation inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
+ "op Int \<equiv> inf"
notation (xsymbols)
inter (infixl "\<inter>" 70)
@@ -707,7 +705,7 @@
lemma Int_def:
"A \<inter> B = {x. x \<in> A \<and> x \<in> B}"
- by (simp add: inf_fun_eq inf_bool_eq inf_set_eq [symmetric] Collect_def mem_def)
+ by (simp add: inf_fun_eq inf_bool_eq Collect_def mem_def)
lemma Int_iff [simp]: "(c : A Int B) = (c:A & c:B)"
by (unfold Int_def) blast
@@ -725,9 +723,7 @@
by simp
lemma mono_Int: "mono f \<Longrightarrow> f (A \<inter> B) \<subseteq> f A \<inter> f B"
- apply (fold inf_set_eq)
- apply (erule mono_inf)
- done
+ by (fact mono_inf)
subsubsection {* Set difference *}
--- a/src/HOL/Tools/Function/fundef_lib.ML Sat Sep 19 07:35:27 2009 +0200
+++ b/src/HOL/Tools/Function/fundef_lib.ML Sat Sep 19 07:38:11 2009 +0200
@@ -170,7 +170,7 @@
end
(* instance for unions *)
-fun regroup_union_conv t = regroup_conv @{const_name Set.empty} @{const_name Set.union}
+fun regroup_union_conv t = regroup_conv @{const_name Set.empty} @{const_name Lattices.sup}
(map (fn t => t RS eq_reflection) (@{thms Un_ac} @
@{thms Un_empty_right} @
@{thms Un_empty_left})) t
--- a/src/HOL/Tools/Function/termination.ML Sat Sep 19 07:35:27 2009 +0200
+++ b/src/HOL/Tools/Function/termination.ML Sat Sep 19 07:38:11 2009 +0200
@@ -145,7 +145,7 @@
fun mk_sum_skel rel =
let
- val cs = FundefLib.dest_binop_list @{const_name Set.union} rel
+ val cs = FundefLib.dest_binop_list @{const_name Lattices.sup} rel
fun collect_pats (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
let
val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const ("Pair", _) $ r $ l)) $ Gam)
@@ -233,7 +233,7 @@
fun CALLS tac i st =
if Thm.no_prems st then all_tac st
else case Thm.term_of (Thm.cprem_of st i) of
- (_ $ (_ $ rel)) => tac (FundefLib.dest_binop_list @{const_name Set.union} rel, i) st
+ (_ $ (_ $ rel)) => tac (FundefLib.dest_binop_list @{const_name Lattices.sup} rel, i) st
|_ => no_tac st
type ttac = (data -> int -> tactic) -> (data -> int -> tactic) -> data -> int -> tactic
@@ -293,7 +293,7 @@
if null ineqs then
Const (@{const_name Set.empty}, fastype_of rel)
else
- foldr1 (HOLogic.mk_binop @{const_name Set.union}) (map mk_compr ineqs)
+ foldr1 (HOLogic.mk_binop @{const_name Lattices.sup}) (map mk_compr ineqs)
fun solve_membership_tac i =
(EVERY' (replicate (i - 2) (rtac @{thm UnI2})) (* pick the right component of the union *)
--- a/src/HOL/Tools/inductive_set.ML Sat Sep 19 07:35:27 2009 +0200
+++ b/src/HOL/Tools/inductive_set.ML Sat Sep 19 07:38:11 2009 +0200
@@ -74,8 +74,8 @@
in Drule.instantiate' [] (rev (map (SOME o cterm_of thy o Var) vs))
(p (fold (Logic.all o Var) vs t) f)
end;
- fun mkop "op &" T x = SOME (Const (@{const_name Set.inter}, T --> T --> T), x)
- | mkop "op |" T x = SOME (Const (@{const_name Set.union}, T --> T --> T), x)
+ fun mkop "op &" T x = SOME (Const (@{const_name Lattices.inf}, T --> T --> T), x)
+ | mkop "op |" T x = SOME (Const (@{const_name Lattices.sup}, T --> T --> T), x)
| mkop _ _ _ = NONE;
fun mk_collect p T t =
let val U = HOLogic.dest_setT T
--- a/src/HOL/ex/predicate_compile.ML Sat Sep 19 07:35:27 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML Sat Sep 19 07:38:11 2009 +0200
@@ -2152,7 +2152,7 @@
val (ts, _) = Predicate.yieldn k t;
val elemsT = HOLogic.mk_set T ts;
in if k = ~1 orelse length ts < k then elemsT
- else Const (@{const_name Set.union}, setT --> setT --> setT) $ elemsT $ t_compr
+ else Const (@{const_name Lattices.sup}, setT --> setT --> setT) $ elemsT $ t_compr
end;
fun values_cmd modes k raw_t state =