# HG changeset patch # User haftmann # Date 1248781029 -7200 # Node ID 0be31453f698495cc0d5c9904b3ced8498ed86fc # Parent 8bc0fd4a23a087d4d4d844a6d3a3f1c7e5fa3466 Set.UNIV and Set.empty are mere abbreviations for top and bot diff -r 8bc0fd4a23a0 -r 0be31453f698 NEWS --- 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 diff -r 8bc0fd4a23a0 -r 0be31453f698 src/HOL/NatTransfer.thy --- 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 diff -r 8bc0fd4a23a0 -r 0be31453f698 src/HOL/Set.thy --- 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 + "{} \ bot" definition insert :: "'a \ 'a set \ 'a set" where insert_compr: "insert a B = {x. x = a \ x \ 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 \ 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) diff -r 8bc0fd4a23a0 -r 0be31453f698 src/HOL/Tools/Qelim/cooper.ML --- 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 diff -r 8bc0fd4a23a0 -r 0be31453f698 src/HOL/Tools/Qelim/ferrante_rackoff.ML --- 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 diff -r 8bc0fd4a23a0 -r 0be31453f698 src/HOL/Tools/Qelim/langford.ML --- 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 diff -r 8bc0fd4a23a0 -r 0be31453f698 src/HOL/Tools/hologic.ML --- 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]); diff -r 8bc0fd4a23a0 -r 0be31453f698 src/HOL/Tools/res_clause.ML --- 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"),