--- a/NEWS Tue Jul 28 13:37:08 2009 +0200
+++ b/NEWS Tue Jul 28 13:37:09 2009 +0200
@@ -18,6 +18,8 @@
*** HOL ***
+* Set.UNIV and Set.empty are mere abbreviations for top and bot. INCOMPATIBILITY.
+
* More convenient names for set intersection and union. INCOMPATIBILITY:
Set.Int ~> Set.inter
--- a/src/HOL/NatTransfer.thy Tue Jul 28 13:37:08 2009 +0200
+++ b/src/HOL/NatTransfer.thy Tue Jul 28 13:37:09 2009 +0200
@@ -382,7 +382,7 @@
lemma UNIV_apply:
"UNIV x = True"
- by (simp add: top_set_eq [symmetric] top_fun_eq top_bool_eq)
+ by (simp add: top_fun_eq top_bool_eq)
declare TransferMorphism_int_nat[transfer add return:
transfer_int_nat_numerals
--- a/src/HOL/Set.thy Tue Jul 28 13:37:08 2009 +0200
+++ b/src/HOL/Set.thy Tue Jul 28 13:37:09 2009 +0200
@@ -100,8 +100,8 @@
text {* Set enumerations *}
-definition empty :: "'a set" ("{}") where
- bot_set_eq [symmetric]: "{} = bot"
+abbreviation empty :: "'a set" ("{}") where
+ "{} \<equiv> bot"
definition insert :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set" where
insert_compr: "insert a B = {x. x = a \<or> x \<in> B}"
@@ -541,12 +541,12 @@
subsubsection {* The universal set -- UNIV *}
-definition UNIV :: "'a set" where
- top_set_eq [symmetric]: "UNIV = top"
+abbreviation UNIV :: "'a set" where
+ "UNIV \<equiv> top"
lemma UNIV_def:
"UNIV = {x. True}"
- by (simp add: top_set_eq [symmetric] top_fun_eq top_bool_eq Collect_def)
+ by (simp add: top_fun_eq top_bool_eq Collect_def)
lemma UNIV_I [simp]: "x : UNIV"
by (simp add: UNIV_def)
@@ -579,7 +579,7 @@
lemma empty_def:
"{} = {x. False}"
- by (simp add: bot_set_eq [symmetric] bot_fun_eq bot_bool_eq Collect_def)
+ by (simp add: bot_fun_eq bot_bool_eq Collect_def)
lemma empty_iff [simp]: "(c : {}) = False"
by (simp add: empty_def)
--- a/src/HOL/Tools/Qelim/cooper.ML Tue Jul 28 13:37:08 2009 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Tue Jul 28 13:37:09 2009 +0200
@@ -428,7 +428,7 @@
in
fun provein x S =
case term_of S of
- Const(@{const_name Set.empty}, _) => error "Unexpected error in Cooper, please email Amine Chaieb"
+ Const(@{const_name Orderings.bot}, _) => error "Unexpected error in Cooper, please email Amine Chaieb"
| Const(@{const_name insert}, _) $ y $ _ =>
let val (cy,S') = Thm.dest_binop S
in if term_of x aconv y then instantiate' [] [SOME x, SOME S'] insI1
--- a/src/HOL/Tools/Qelim/ferrante_rackoff.ML Tue Jul 28 13:37:08 2009 +0200
+++ b/src/HOL/Tools/Qelim/ferrante_rackoff.ML Tue Jul 28 13:37:09 2009 +0200
@@ -99,7 +99,7 @@
in
fun provein x S =
case term_of S of
- Const(@{const_name Set.empty}, _) => raise CTERM ("provein : not a member!", [S])
+ Const(@{const_name Orderings.bot}, _) => raise CTERM ("provein : not a member!", [S])
| Const(@{const_name insert}, _) $ y $_ =>
let val (cy,S') = Thm.dest_binop S
in if term_of x aconv y then instantiate' [] [SOME x, SOME S'] insI1
--- a/src/HOL/Tools/Qelim/langford.ML Tue Jul 28 13:37:08 2009 +0200
+++ b/src/HOL/Tools/Qelim/langford.ML Tue Jul 28 13:37:09 2009 +0200
@@ -15,7 +15,7 @@
let
fun h acc ct =
case term_of ct of
- Const (@{const_name Set.empty}, _) => acc
+ Const (@{const_name Orderings.bot}, _) => acc
| Const (@{const_name insert}, _) $ _ $ t => h (Thm.dest_arg1 ct :: acc) (Thm.dest_arg ct)
in h [] end;
@@ -48,11 +48,11 @@
in (ne, f) end
val qe = case (term_of L, term_of U) of
- (Const (@{const_name Set.empty}, _),_) =>
+ (Const (@{const_name Orderings.bot}, _),_) =>
let
val (neU,fU) = proveneF U
in simp_rule (transitive ths (dlo_qeth_nolb OF [neU, fU])) end
- | (_,Const (@{const_name Set.empty}, _)) =>
+ | (_,Const (@{const_name Orderings.bot}, _)) =>
let
val (neL,fL) = proveneF L
in simp_rule (transitive ths (dlo_qeth_noub OF [neL, fL])) end
--- a/src/HOL/Tools/hologic.ML Tue Jul 28 13:37:08 2009 +0200
+++ b/src/HOL/Tools/hologic.ML Tue Jul 28 13:37:09 2009 +0200
@@ -153,13 +153,13 @@
fun mk_set T ts =
let
val sT = mk_setT T;
- val empty = Const ("Set.empty", sT);
+ val empty = Const ("Orderings.bot_class.bot", sT);
fun insert t u = Const ("Set.insert", T --> sT --> sT) $ t $ u;
in fold_rev insert ts empty end;
-fun mk_UNIV T = Const ("Set.UNIV", mk_setT T);
+fun mk_UNIV T = Const ("Orderings.top_class.top", mk_setT T);
-fun dest_set (Const ("Set.empty", _)) = []
+fun dest_set (Const ("Orderings.bot_class.bot", _)) = []
| dest_set (Const ("Set.insert", _) $ t $ u) = t :: dest_set u
| dest_set t = raise TERM ("dest_set", [t]);
--- a/src/HOL/Tools/res_clause.ML Tue Jul 28 13:37:08 2009 +0200
+++ b/src/HOL/Tools/res_clause.ML Tue Jul 28 13:37:09 2009 +0200
@@ -99,20 +99,10 @@
val const_trans_table =
Symtab.make [(@{const_name "op ="}, "equal"),
(@{const_name HOL.less_eq}, "lessequals"),
- (@{const_name HOL.less}, "less"),
(@{const_name "op &"}, "and"),
(@{const_name "op |"}, "or"),
- (@{const_name HOL.plus}, "plus"),
- (@{const_name HOL.minus}, "minus"),
- (@{const_name HOL.times}, "times"),
- (@{const_name Divides.div}, "div"),
- (@{const_name HOL.divide}, "divide"),
(@{const_name "op -->"}, "implies"),
- (@{const_name Set.empty}, "emptyset"),
(@{const_name "op :"}, "in"),
- (@{const_name union}, "union"),
- (@{const_name inter}, "inter"),
- ("List.append", "append"),
("ATP_Linkup.fequal", "fequal"),
("ATP_Linkup.COMBI", "COMBI"),
("ATP_Linkup.COMBK", "COMBK"),