insert now qualified and with authentic syntax
authorhaftmann
Thu Jun 04 15:28:59 2009 +0200 (2009-06-04)
changeset 3145655edadbd43d5
parent 31455 2754a0dadccc
child 31457 d1cb222438d8
insert now qualified and with authentic syntax
src/HOL/Set.thy
src/HOL/Tools/hologic.ML
     1.1 --- a/src/HOL/Set.thy	Thu Jun 04 15:28:59 2009 +0200
     1.2 +++ b/src/HOL/Set.thy	Thu Jun 04 15:28:59 2009 +0200
     1.3 @@ -20,7 +20,6 @@
     1.4  consts
     1.5    Collect       :: "('a => bool) => 'a set"              -- "comprehension"
     1.6    "op :"        :: "'a => 'a set => bool"                -- "membership"
     1.7 -  insert        :: "'a => 'a set => 'a set"
     1.8    Ball          :: "'a set => ('a => bool) => bool"      -- "bounded universal quantifiers"
     1.9    Bex           :: "'a set => ('a => bool) => bool"      -- "bounded existential quantifiers"
    1.10    Bex1          :: "'a set => ('a => bool) => bool"      -- "bounded unique existential quantifiers"
    1.11 @@ -58,19 +57,6 @@
    1.12  translations
    1.13    "{x. P}"      == "Collect (%x. P)"
    1.14  
    1.15 -definition empty :: "'a set" ("{}") where
    1.16 -  "empty \<equiv> {x. False}"
    1.17 -
    1.18 -definition UNIV :: "'a set" where
    1.19 -  "UNIV \<equiv> {x. True}"
    1.20 -
    1.21 -syntax
    1.22 -  "@Finset"     :: "args => 'a set"                       ("{(_)}")
    1.23 -
    1.24 -translations
    1.25 -  "{x, xs}"     == "insert x {xs}"
    1.26 -  "{x}"         == "insert x {}"
    1.27 -
    1.28  definition Int :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
    1.29    "A Int B \<equiv> {x. x \<in> A \<and> x \<in> B}"
    1.30  
    1.31 @@ -85,6 +71,22 @@
    1.32    "Int"  (infixl "\<inter>" 70) and
    1.33    "Un"  (infixl "\<union>" 65)
    1.34  
    1.35 +definition empty :: "'a set" ("{}") where
    1.36 +  "empty \<equiv> {x. False}"
    1.37 +
    1.38 +definition insert :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set" where
    1.39 +  "insert a B \<equiv> {x. x = a} \<union> B"
    1.40 +
    1.41 +definition UNIV :: "'a set" where
    1.42 +  "UNIV \<equiv> {x. True}"
    1.43 +
    1.44 +syntax
    1.45 +  "@Finset"     :: "args => 'a set"                       ("{(_)}")
    1.46 +
    1.47 +translations
    1.48 +  "{x, xs}"     == "CONST insert x {xs}"
    1.49 +  "{x}"         == "CONST insert x {}"
    1.50 +
    1.51  syntax
    1.52    "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3ALL _:_./ _)" [0, 0, 10] 10)
    1.53    "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3EX _:_./ _)" [0, 0, 10] 10)
    1.54 @@ -408,7 +410,6 @@
    1.55  
    1.56  defs
    1.57    Pow_def:      "Pow A          == {B. B <= A}"
    1.58 -  insert_def:   "insert a B     == {x. x=a} Un B"
    1.59    image_def:    "f`A            == {y. EX x:A. y = f(x)}"
    1.60  
    1.61  
    1.62 @@ -811,7 +812,7 @@
    1.63  by blast
    1.64  
    1.65  
    1.66 -subsubsection {* Augmenting a set -- insert *}
    1.67 +subsubsection {* Augmenting a set -- @{const insert} *}
    1.68  
    1.69  lemma insert_iff [simp]: "(a : insert b A) = (a = b | a:A)"
    1.70    by (unfold insert_def) blast
     2.1 --- a/src/HOL/Tools/hologic.ML	Thu Jun 04 15:28:59 2009 +0200
     2.2 +++ b/src/HOL/Tools/hologic.ML	Thu Jun 04 15:28:59 2009 +0200
     2.3 @@ -152,13 +152,13 @@
     2.4    let
     2.5      val sT = mk_setT T;
     2.6      val empty = Const ("Set.empty", sT);
     2.7 -    fun insert t u = Const ("insert", T --> sT --> sT) $ t $ u;
     2.8 +    fun insert t u = Const ("Set.insert", T --> sT --> sT) $ t $ u;
     2.9    in fold_rev insert ts empty end;
    2.10  
    2.11  fun mk_UNIV T = Const ("Set.UNIV", mk_setT T);
    2.12  
    2.13 -fun dest_set (Const ("Orderings.bot", _)) = []
    2.14 -  | dest_set (Const ("insert", _) $ t $ u) = t :: dest_set u
    2.15 +fun dest_set (Const ("Set.empty", _)) = []
    2.16 +  | dest_set (Const ("Set.insert", _) $ t $ u) = t :: dest_set u
    2.17    | dest_set t = raise TERM ("dest_set", [t]);
    2.18  
    2.19  fun Collect_const T = Const ("Collect", (T --> boolT) --> mk_setT T);