--- a/NEWS Tue Jul 28 19:49:42 2009 +0200
+++ b/NEWS Tue Jul 28 20:26:39 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/doc-src/Main/Docs/document/Main_Doc.tex Tue Jul 28 19:49:42 2009 +0200
+++ b/doc-src/Main/Docs/document/Main_Doc.tex Tue Jul 28 20:26:39 2009 +0200
@@ -231,7 +231,7 @@
\begin{supertabular}{@ {} l @ {~::~} l @ {}}
\isa{converse} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}b\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\
-\isa{op\ O} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}c\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}c\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set}\\
+\isa{op\ O} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}b\ {\isasymtimes}\ {\isacharprime}c{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}c{\isacharparenright}\ set}\\
\isa{op\ {\isacharbackquote}{\isacharbackquote}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b\ set}\\
\isa{inv{\isacharunderscore}image} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}b\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set}\\
\isa{Id{\isacharunderscore}on} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\
--- a/doc-src/TutorialI/Protocol/Message.thy Tue Jul 28 19:49:42 2009 +0200
+++ b/doc-src/TutorialI/Protocol/Message.thy Tue Jul 28 20:26:39 2009 +0200
@@ -841,6 +841,8 @@
(*Apply rules to break down assumptions of the form
Y \<in> parts(insert X H) and Y \<in> analz(insert X H)
*)
+fun impOfSubs th = th RSN (2, @{thm rev_subsetD})
+
val Fake_insert_tac =
dresolve_tac [impOfSubs Fake_analz_insert,
impOfSubs Fake_parts_insert] THEN'
--- a/src/HOL/MicroJava/BV/Listn.thy Tue Jul 28 19:49:42 2009 +0200
+++ b/src/HOL/MicroJava/BV/Listn.thy Tue Jul 28 20:26:39 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/MicroJava/BV/Listn.thy
- ID: $Id$
Author: Tobias Nipkow
Copyright 2000 TUM
@@ -8,7 +7,9 @@
header {* \isaheader{Fixed Length Lists} *}
-theory Listn imports Err begin
+theory Listn
+imports Err
+begin
constdefs
@@ -317,6 +318,10 @@
apply (simp add: nth_Cons split: nat.split)
done
+lemma equals0I_aux:
+ "(\<And>y. A y \<Longrightarrow> False) \<Longrightarrow> A = bot_class.bot"
+ by (rule equals0I) (auto simp add: mem_def)
+
lemma acc_le_listI [intro!]:
"\<lbrakk> order r; acc r \<rbrakk> \<Longrightarrow> acc(Listn.le r)"
apply (unfold acc_def)
@@ -330,7 +335,7 @@
apply (rename_tac m n)
apply (case_tac "m=n")
apply simp
- apply (fast intro!: equals0I [to_pred bot_empty_eq pred_equals_eq] dest: not_sym)
+ apply (fast intro!: equals0I_aux dest: not_sym)
apply clarify
apply (rename_tac n)
apply (induct_tac n)
--- a/src/HOL/NatTransfer.thy Tue Jul 28 19:49:42 2009 +0200
+++ b/src/HOL/NatTransfer.thy Tue Jul 28 20:26:39 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 19:49:42 2009 +0200
+++ b/src/HOL/Set.thy Tue Jul 28 20:26:39 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 19:49:42 2009 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Tue Jul 28 20:26:39 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 19:49:42 2009 +0200
+++ b/src/HOL/Tools/Qelim/ferrante_rackoff.ML Tue Jul 28 20:26:39 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 19:49:42 2009 +0200
+++ b/src/HOL/Tools/Qelim/langford.ML Tue Jul 28 20:26:39 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 19:49:42 2009 +0200
+++ b/src/HOL/Tools/hologic.ML Tue Jul 28 20:26:39 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 19:49:42 2009 +0200
+++ b/src/HOL/Tools/res_clause.ML Tue Jul 28 20:26:39 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"),
--- a/src/HOL/Wellfounded.thy Tue Jul 28 19:49:42 2009 +0200
+++ b/src/HOL/Wellfounded.thy Tue Jul 28 20:26:39 2009 +0200
@@ -283,8 +283,10 @@
apply (blast elim!: allE)
done
-lemmas wfP_SUP = wf_UN [where I=UNIV and r="\<lambda>i. {(x, y). r i x y}",
- to_pred SUP_UN_eq2 bot_empty_eq pred_equals_eq, simplified, standard]
+lemma wfP_SUP:
+ "\<forall>i. wfP (r i) \<Longrightarrow> \<forall>i j. r i \<noteq> r j \<longrightarrow> inf (DomainP (r i)) (RangeP (r j)) = bot \<Longrightarrow> wfP (SUPR UNIV r)"
+ by (rule wf_UN [where I=UNIV and r="\<lambda>i. {(x, y). r i x y}", to_pred SUP_UN_eq2 pred_equals_eq])
+ (simp_all add: bot_fun_eq bot_bool_eq)
lemma wf_Union:
"[| ALL r:R. wf r;