Set.UNIV and Set.empty are mere abbreviations for top and bot
authorhaftmann
Tue Jul 28 13:37:09 2009 +0200 (2009-07-28)
changeset 322640be31453f698
parent 32263 8bc0fd4a23a0
child 32265 fa8872f21ac3
Set.UNIV and Set.empty are mere abbreviations for top and bot
NEWS
src/HOL/NatTransfer.thy
src/HOL/Set.thy
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/Qelim/ferrante_rackoff.ML
src/HOL/Tools/Qelim/langford.ML
src/HOL/Tools/hologic.ML
src/HOL/Tools/res_clause.ML
     1.1 --- a/NEWS	Tue Jul 28 13:37:08 2009 +0200
     1.2 +++ b/NEWS	Tue Jul 28 13:37:09 2009 +0200
     1.3 @@ -18,6 +18,8 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Set.UNIV and Set.empty are mere abbreviations for top and bot.  INCOMPATIBILITY.
     1.8 +
     1.9  * More convenient names for set intersection and union.  INCOMPATIBILITY:
    1.10  
    1.11      Set.Int ~>  Set.inter
     2.1 --- a/src/HOL/NatTransfer.thy	Tue Jul 28 13:37:08 2009 +0200
     2.2 +++ b/src/HOL/NatTransfer.thy	Tue Jul 28 13:37:09 2009 +0200
     2.3 @@ -382,7 +382,7 @@
     2.4  
     2.5  lemma UNIV_apply:
     2.6    "UNIV x = True"
     2.7 -  by (simp add: top_set_eq [symmetric] top_fun_eq top_bool_eq)
     2.8 +  by (simp add: top_fun_eq top_bool_eq)
     2.9  
    2.10  declare TransferMorphism_int_nat[transfer add return:
    2.11    transfer_int_nat_numerals
     3.1 --- a/src/HOL/Set.thy	Tue Jul 28 13:37:08 2009 +0200
     3.2 +++ b/src/HOL/Set.thy	Tue Jul 28 13:37:09 2009 +0200
     3.3 @@ -100,8 +100,8 @@
     3.4  
     3.5  text {* Set enumerations *}
     3.6  
     3.7 -definition empty :: "'a set" ("{}") where
     3.8 -  bot_set_eq [symmetric]: "{} = bot"
     3.9 +abbreviation empty :: "'a set" ("{}") where
    3.10 +  "{} \<equiv> bot"
    3.11  
    3.12  definition insert :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set" where
    3.13    insert_compr: "insert a B = {x. x = a \<or> x \<in> B}"
    3.14 @@ -541,12 +541,12 @@
    3.15  
    3.16  subsubsection {* The universal set -- UNIV *}
    3.17  
    3.18 -definition UNIV :: "'a set" where
    3.19 -  top_set_eq [symmetric]: "UNIV = top"
    3.20 +abbreviation UNIV :: "'a set" where
    3.21 +  "UNIV \<equiv> top"
    3.22  
    3.23  lemma UNIV_def:
    3.24    "UNIV = {x. True}"
    3.25 -  by (simp add: top_set_eq [symmetric] top_fun_eq top_bool_eq Collect_def)
    3.26 +  by (simp add: top_fun_eq top_bool_eq Collect_def)
    3.27  
    3.28  lemma UNIV_I [simp]: "x : UNIV"
    3.29    by (simp add: UNIV_def)
    3.30 @@ -579,7 +579,7 @@
    3.31  
    3.32  lemma empty_def:
    3.33    "{} = {x. False}"
    3.34 -  by (simp add: bot_set_eq [symmetric] bot_fun_eq bot_bool_eq Collect_def)
    3.35 +  by (simp add: bot_fun_eq bot_bool_eq Collect_def)
    3.36  
    3.37  lemma empty_iff [simp]: "(c : {}) = False"
    3.38    by (simp add: empty_def)
     4.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Tue Jul 28 13:37:08 2009 +0200
     4.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Tue Jul 28 13:37:09 2009 +0200
     4.3 @@ -428,7 +428,7 @@
     4.4     in
     4.5      fun provein x S = 
     4.6       case term_of S of
     4.7 -        Const(@{const_name Set.empty}, _) => error "Unexpected error in Cooper, please email Amine Chaieb"
     4.8 +        Const(@{const_name Orderings.bot}, _) => error "Unexpected error in Cooper, please email Amine Chaieb"
     4.9        | Const(@{const_name insert}, _) $ y $ _ => 
    4.10           let val (cy,S') = Thm.dest_binop S
    4.11           in if term_of x aconv y then instantiate' [] [SOME x, SOME S'] insI1
     5.1 --- a/src/HOL/Tools/Qelim/ferrante_rackoff.ML	Tue Jul 28 13:37:08 2009 +0200
     5.2 +++ b/src/HOL/Tools/Qelim/ferrante_rackoff.ML	Tue Jul 28 13:37:09 2009 +0200
     5.3 @@ -99,7 +99,7 @@
     5.4     in
     5.5      fun provein x S =
     5.6       case term_of S of
     5.7 -        Const(@{const_name Set.empty}, _) => raise CTERM ("provein : not a member!", [S])
     5.8 +        Const(@{const_name Orderings.bot}, _) => raise CTERM ("provein : not a member!", [S])
     5.9        | Const(@{const_name insert}, _) $ y $_ =>
    5.10           let val (cy,S') = Thm.dest_binop S
    5.11           in if term_of x aconv y then instantiate' [] [SOME x, SOME S'] insI1
     6.1 --- a/src/HOL/Tools/Qelim/langford.ML	Tue Jul 28 13:37:08 2009 +0200
     6.2 +++ b/src/HOL/Tools/Qelim/langford.ML	Tue Jul 28 13:37:09 2009 +0200
     6.3 @@ -15,7 +15,7 @@
     6.4   let 
     6.5    fun h acc ct = 
     6.6     case term_of ct of
     6.7 -     Const (@{const_name Set.empty}, _) => acc
     6.8 +     Const (@{const_name Orderings.bot}, _) => acc
     6.9     | Const (@{const_name insert}, _) $ _ $ t => h (Thm.dest_arg1 ct :: acc) (Thm.dest_arg ct)
    6.10  in h [] end;
    6.11  
    6.12 @@ -48,11 +48,11 @@
    6.13         in (ne, f) end
    6.14  
    6.15       val qe = case (term_of L, term_of U) of 
    6.16 -      (Const (@{const_name Set.empty}, _),_) =>  
    6.17 +      (Const (@{const_name Orderings.bot}, _),_) =>  
    6.18          let
    6.19            val (neU,fU) = proveneF U 
    6.20          in simp_rule (transitive ths (dlo_qeth_nolb OF [neU, fU])) end
    6.21 -    | (_,Const (@{const_name Set.empty}, _)) =>  
    6.22 +    | (_,Const (@{const_name Orderings.bot}, _)) =>  
    6.23          let
    6.24            val (neL,fL) = proveneF L
    6.25          in simp_rule (transitive ths (dlo_qeth_noub OF [neL, fL])) end
     7.1 --- a/src/HOL/Tools/hologic.ML	Tue Jul 28 13:37:08 2009 +0200
     7.2 +++ b/src/HOL/Tools/hologic.ML	Tue Jul 28 13:37:09 2009 +0200
     7.3 @@ -153,13 +153,13 @@
     7.4  fun mk_set T ts =
     7.5    let
     7.6      val sT = mk_setT T;
     7.7 -    val empty = Const ("Set.empty", sT);
     7.8 +    val empty = Const ("Orderings.bot_class.bot", sT);
     7.9      fun insert t u = Const ("Set.insert", T --> sT --> sT) $ t $ u;
    7.10    in fold_rev insert ts empty end;
    7.11  
    7.12 -fun mk_UNIV T = Const ("Set.UNIV", mk_setT T);
    7.13 +fun mk_UNIV T = Const ("Orderings.top_class.top", mk_setT T);
    7.14  
    7.15 -fun dest_set (Const ("Set.empty", _)) = []
    7.16 +fun dest_set (Const ("Orderings.bot_class.bot", _)) = []
    7.17    | dest_set (Const ("Set.insert", _) $ t $ u) = t :: dest_set u
    7.18    | dest_set t = raise TERM ("dest_set", [t]);
    7.19  
     8.1 --- a/src/HOL/Tools/res_clause.ML	Tue Jul 28 13:37:08 2009 +0200
     8.2 +++ b/src/HOL/Tools/res_clause.ML	Tue Jul 28 13:37:09 2009 +0200
     8.3 @@ -99,20 +99,10 @@
     8.4  val const_trans_table =
     8.5        Symtab.make [(@{const_name "op ="}, "equal"),
     8.6                     (@{const_name HOL.less_eq}, "lessequals"),
     8.7 -                   (@{const_name HOL.less}, "less"),
     8.8                     (@{const_name "op &"}, "and"),
     8.9                     (@{const_name "op |"}, "or"),
    8.10 -                   (@{const_name HOL.plus}, "plus"),
    8.11 -                   (@{const_name HOL.minus}, "minus"),
    8.12 -                   (@{const_name HOL.times}, "times"),
    8.13 -                   (@{const_name Divides.div}, "div"),
    8.14 -                   (@{const_name HOL.divide}, "divide"),
    8.15                     (@{const_name "op -->"}, "implies"),
    8.16 -                   (@{const_name Set.empty}, "emptyset"),
    8.17                     (@{const_name "op :"}, "in"),
    8.18 -                   (@{const_name union}, "union"),
    8.19 -                   (@{const_name inter}, "inter"),
    8.20 -                   ("List.append", "append"),
    8.21                     ("ATP_Linkup.fequal", "fequal"),
    8.22                     ("ATP_Linkup.COMBI", "COMBI"),
    8.23                     ("ATP_Linkup.COMBK", "COMBK"),