inter and union are mere abbreviations for inf and sup
authorhaftmann
Sat Sep 19 07:38:03 2009 +0200 (2009-09-19)
changeset 326837c1fe854ca6a
parent 32606 b5c3a8a75772
child 32684 139257823133
inter and union are mere abbreviations for inf and sup
NEWS
src/HOL/Finite_Set.thy
src/HOL/Inductive.thy
src/HOL/Library/Executable_Set.thy
src/HOL/Set.thy
src/HOL/Tools/Function/fundef_lib.ML
src/HOL/Tools/Function/termination.ML
src/HOL/Tools/inductive_set.ML
src/HOL/ex/predicate_compile.ML
     1.1 --- a/NEWS	Fri Sep 18 14:09:38 2009 +0200
     1.2 +++ b/NEWS	Sat Sep 19 07:38:03 2009 +0200
     1.3 @@ -87,6 +87,8 @@
     1.4    - mere abbreviations:
     1.5      Set.empty               (for bot)
     1.6      Set.UNIV                (for top)
     1.7 +    Set.inter               (for inf)
     1.8 +    Set.union               (for sup)
     1.9      Complete_Lattice.Inter  (for Inf)
    1.10      Complete_Lattice.Union  (for Sup)
    1.11      Complete_Lattice.INTER  (for INFI)
     2.1 --- a/src/HOL/Finite_Set.thy	Fri Sep 18 14:09:38 2009 +0200
     2.2 +++ b/src/HOL/Finite_Set.thy	Sat Sep 19 07:38:03 2009 +0200
     2.3 @@ -1566,8 +1566,6 @@
     2.4    prefer 2
     2.5    apply assumption
     2.6    apply auto
     2.7 -  apply (rule setsum_cong)
     2.8 -  apply auto
     2.9  done
    2.10  
    2.11  lemma setsum_right_distrib: 
     3.1 --- a/src/HOL/Inductive.thy	Fri Sep 18 14:09:38 2009 +0200
     3.2 +++ b/src/HOL/Inductive.thy	Sat Sep 19 07:38:03 2009 +0200
     3.3 @@ -83,7 +83,7 @@
     3.4        and indhyp: "!!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x)"
     3.5    shows "P(a)"
     3.6    by (rule lfp_induct [THEN subsetD, THEN CollectD, OF mono _ lfp])
     3.7 -    (auto simp: inf_set_eq intro: indhyp)
     3.8 +    (auto simp: intro: indhyp)
     3.9  
    3.10  lemma lfp_ordinal_induct:
    3.11    fixes f :: "'a\<Colon>complete_lattice \<Rightarrow> 'a"
    3.12 @@ -184,7 +184,7 @@
    3.13  
    3.14  text{*strong version, thanks to Coen and Frost*}
    3.15  lemma coinduct_set: "[| mono(f);  a: X;  X \<subseteq> f(X Un gfp(f)) |] ==> a : gfp(f)"
    3.16 -by (blast intro: weak_coinduct [OF _ coinduct_lemma, simplified sup_set_eq])
    3.17 +by (blast intro: weak_coinduct [OF _ coinduct_lemma])
    3.18  
    3.19  lemma coinduct: "[| mono(f); X \<le> f (sup X (gfp f)) |] ==> X \<le> gfp(f)"
    3.20    apply (rule order_trans)
     4.1 --- a/src/HOL/Library/Executable_Set.thy	Fri Sep 18 14:09:38 2009 +0200
     4.2 +++ b/src/HOL/Library/Executable_Set.thy	Sat Sep 19 07:38:03 2009 +0200
     4.3 @@ -12,6 +12,21 @@
     4.4  
     4.5  declare member [code] 
     4.6  
     4.7 +definition empty :: "'a set" where
     4.8 +  "empty = {}"
     4.9 +
    4.10 +declare empty_def [symmetric, code_unfold]
    4.11 +
    4.12 +definition inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
    4.13 +  "inter = op \<inter>"
    4.14 +
    4.15 +declare inter_def [symmetric, code_unfold]
    4.16 +
    4.17 +definition union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
    4.18 +  "union = op \<union>"
    4.19 +
    4.20 +declare union_def [symmetric, code_unfold]
    4.21 +
    4.22  definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
    4.23    "subset = op \<le>"
    4.24  
    4.25 @@ -69,7 +84,7 @@
    4.26    Set ("\<module>Set")
    4.27  
    4.28  consts_code
    4.29 -  "Set.empty"         ("{*Fset.empty*}")
    4.30 +  "empty"             ("{*Fset.empty*}")
    4.31    "List_Set.is_empty" ("{*Fset.is_empty*}")
    4.32    "Set.insert"        ("{*Fset.insert*}")
    4.33    "List_Set.remove"   ("{*Fset.remove*}")
    4.34 @@ -77,8 +92,8 @@
    4.35    "List_Set.project"  ("{*Fset.filter*}")
    4.36    "Ball"              ("{*flip Fset.forall*}")
    4.37    "Bex"               ("{*flip Fset.exists*}")
    4.38 -  "op \<union>"              ("{*Fset.union*}")
    4.39 -  "op \<inter>"              ("{*Fset.inter*}")
    4.40 +  "union"             ("{*Fset.union*}")
    4.41 +  "inter"             ("{*Fset.inter*}")
    4.42    "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{*flip Fset.subtract*}")
    4.43    "Union"             ("{*Fset.Union*}")
    4.44    "Inter"             ("{*Fset.Inter*}")
     5.1 --- a/src/HOL/Set.thy	Fri Sep 18 14:09:38 2009 +0200
     5.2 +++ b/src/HOL/Set.thy	Sat Sep 19 07:38:03 2009 +0200
     5.3 @@ -652,8 +652,8 @@
     5.4  
     5.5  subsubsection {* Binary union -- Un *}
     5.6  
     5.7 -definition union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Un" 65) where
     5.8 -  sup_set_eq [symmetric]: "A Un B = sup A B"
     5.9 +abbreviation union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Un" 65) where
    5.10 +  "op Un \<equiv> sup"
    5.11  
    5.12  notation (xsymbols)
    5.13    union  (infixl "\<union>" 65)
    5.14 @@ -663,7 +663,7 @@
    5.15  
    5.16  lemma Un_def:
    5.17    "A \<union> B = {x. x \<in> A \<or> x \<in> B}"
    5.18 -  by (simp add: sup_fun_eq sup_bool_eq sup_set_eq [symmetric] Collect_def mem_def)
    5.19 +  by (simp add: sup_fun_eq sup_bool_eq Collect_def mem_def)
    5.20  
    5.21  lemma Un_iff [simp]: "(c : A Un B) = (c:A | c:B)"
    5.22    by (unfold Un_def) blast
    5.23 @@ -689,15 +689,13 @@
    5.24    by (simp add: Collect_def mem_def insert_compr Un_def)
    5.25  
    5.26  lemma mono_Un: "mono f \<Longrightarrow> f A \<union> f B \<subseteq> f (A \<union> B)"
    5.27 -  apply (fold sup_set_eq)
    5.28 -  apply (erule mono_sup)
    5.29 -  done
    5.30 +  by (fact mono_sup)
    5.31  
    5.32  
    5.33  subsubsection {* Binary intersection -- Int *}
    5.34  
    5.35 -definition inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
    5.36 -  inf_set_eq [symmetric]: "A Int B = inf A B"
    5.37 +abbreviation inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
    5.38 +  "op Int \<equiv> inf"
    5.39  
    5.40  notation (xsymbols)
    5.41    inter  (infixl "\<inter>" 70)
    5.42 @@ -707,7 +705,7 @@
    5.43  
    5.44  lemma Int_def:
    5.45    "A \<inter> B = {x. x \<in> A \<and> x \<in> B}"
    5.46 -  by (simp add: inf_fun_eq inf_bool_eq inf_set_eq [symmetric] Collect_def mem_def)
    5.47 +  by (simp add: inf_fun_eq inf_bool_eq Collect_def mem_def)
    5.48  
    5.49  lemma Int_iff [simp]: "(c : A Int B) = (c:A & c:B)"
    5.50    by (unfold Int_def) blast
    5.51 @@ -725,9 +723,7 @@
    5.52    by simp
    5.53  
    5.54  lemma mono_Int: "mono f \<Longrightarrow> f (A \<inter> B) \<subseteq> f A \<inter> f B"
    5.55 -  apply (fold inf_set_eq)
    5.56 -  apply (erule mono_inf)
    5.57 -  done
    5.58 +  by (fact mono_inf)
    5.59  
    5.60  
    5.61  subsubsection {* Set difference *}
     6.1 --- a/src/HOL/Tools/Function/fundef_lib.ML	Fri Sep 18 14:09:38 2009 +0200
     6.2 +++ b/src/HOL/Tools/Function/fundef_lib.ML	Sat Sep 19 07:38:03 2009 +0200
     6.3 @@ -170,7 +170,7 @@
     6.4   end
     6.5  
     6.6  (* instance for unions *)
     6.7 -fun regroup_union_conv t = regroup_conv @{const_name Set.empty} @{const_name Set.union}
     6.8 +fun regroup_union_conv t = regroup_conv @{const_name Set.empty} @{const_name Lattices.sup}
     6.9    (map (fn t => t RS eq_reflection) (@{thms Un_ac} @
    6.10                                       @{thms Un_empty_right} @
    6.11                                       @{thms Un_empty_left})) t
     7.1 --- a/src/HOL/Tools/Function/termination.ML	Fri Sep 18 14:09:38 2009 +0200
     7.2 +++ b/src/HOL/Tools/Function/termination.ML	Sat Sep 19 07:38:03 2009 +0200
     7.3 @@ -145,7 +145,7 @@
     7.4  
     7.5  fun mk_sum_skel rel =
     7.6    let
     7.7 -    val cs = FundefLib.dest_binop_list @{const_name Set.union} rel
     7.8 +    val cs = FundefLib.dest_binop_list @{const_name Lattices.sup} rel
     7.9      fun collect_pats (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
    7.10        let
    7.11          val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const ("Pair", _) $ r $ l)) $ Gam)
    7.12 @@ -233,7 +233,7 @@
    7.13  fun CALLS tac i st =
    7.14    if Thm.no_prems st then all_tac st
    7.15    else case Thm.term_of (Thm.cprem_of st i) of
    7.16 -    (_ $ (_ $ rel)) => tac (FundefLib.dest_binop_list @{const_name Set.union} rel, i) st
    7.17 +    (_ $ (_ $ rel)) => tac (FundefLib.dest_binop_list @{const_name Lattices.sup} rel, i) st
    7.18    |_ => no_tac st
    7.19  
    7.20  type ttac = (data -> int -> tactic) -> (data -> int -> tactic) -> data -> int -> tactic
    7.21 @@ -293,7 +293,7 @@
    7.22            if null ineqs then
    7.23                Const (@{const_name Set.empty}, fastype_of rel)
    7.24            else
    7.25 -              foldr1 (HOLogic.mk_binop @{const_name Set.union}) (map mk_compr ineqs)
    7.26 +              foldr1 (HOLogic.mk_binop @{const_name Lattices.sup}) (map mk_compr ineqs)
    7.27  
    7.28        fun solve_membership_tac i =
    7.29            (EVERY' (replicate (i - 2) (rtac @{thm UnI2}))  (* pick the right component of the union *)
     8.1 --- a/src/HOL/Tools/inductive_set.ML	Fri Sep 18 14:09:38 2009 +0200
     8.2 +++ b/src/HOL/Tools/inductive_set.ML	Sat Sep 19 07:38:03 2009 +0200
     8.3 @@ -74,8 +74,8 @@
     8.4          in Drule.instantiate' [] (rev (map (SOME o cterm_of thy o Var) vs))
     8.5            (p (fold (Logic.all o Var) vs t) f)
     8.6          end;
     8.7 -      fun mkop "op &" T x = SOME (Const (@{const_name Set.inter}, T --> T --> T), x)
     8.8 -        | mkop "op |" T x = SOME (Const (@{const_name Set.union}, T --> T --> T), x)
     8.9 +      fun mkop "op &" T x = SOME (Const (@{const_name Lattices.inf}, T --> T --> T), x)
    8.10 +        | mkop "op |" T x = SOME (Const (@{const_name Lattices.sup}, T --> T --> T), x)
    8.11          | mkop _ _ _ = NONE;
    8.12        fun mk_collect p T t =
    8.13          let val U = HOLogic.dest_setT T
     9.1 --- a/src/HOL/ex/predicate_compile.ML	Fri Sep 18 14:09:38 2009 +0200
     9.2 +++ b/src/HOL/ex/predicate_compile.ML	Sat Sep 19 07:38:03 2009 +0200
     9.3 @@ -2152,7 +2152,7 @@
     9.4      val (ts, _) = Predicate.yieldn k t;
     9.5      val elemsT = HOLogic.mk_set T ts;
     9.6    in if k = ~1 orelse length ts < k then elemsT
     9.7 -    else Const (@{const_name Set.union}, setT --> setT --> setT) $ elemsT $ t_compr
     9.8 +    else Const (@{const_name Lattices.sup}, setT --> setT --> setT) $ elemsT $ t_compr
     9.9    end;
    9.10  
    9.11  fun values_cmd modes k raw_t state =