authentic syntax for Pow and image
authorhaftmann
Mon Jun 15 16:13:19 2009 +0200 (2009-06-15)
changeset 31643b040f1679f77
parent 31642 ce68241f711f
child 31644 f4723b1ae5a1
child 31665 a1f4d3b3f6c8
authentic syntax for Pow and image
NEWS
src/HOL/Set.thy
src/HOL/Tools/datatype_package/datatype_rep_proofs.ML
     1.1 --- a/NEWS	Mon Jun 15 16:13:04 2009 +0200
     1.2 +++ b/NEWS	Mon Jun 15 16:13:19 2009 +0200
     1.3 @@ -40,6 +40,9 @@
     1.4  * Implementation of quickcheck using generic code generator; default generators
     1.5  are provided for all suitable HOL types, records and datatypes.
     1.6  
     1.7 +* Constants Set.Pow and Set.image now with authentic syntax; object-logic definitions
     1.8 +Set.Pow_def and Set.image_def.  INCOMPATIBILITY.
     1.9 +
    1.10  
    1.11  *** ML ***
    1.12  
     2.1 --- a/src/HOL/Set.thy	Mon Jun 15 16:13:04 2009 +0200
     2.2 +++ b/src/HOL/Set.thy	Mon Jun 15 16:13:19 2009 +0200
     2.3 @@ -23,8 +23,6 @@
     2.4    Ball          :: "'a set => ('a => bool) => bool"      -- "bounded universal quantifiers"
     2.5    Bex           :: "'a set => ('a => bool) => bool"      -- "bounded existential quantifiers"
     2.6    Bex1          :: "'a set => ('a => bool) => bool"      -- "bounded unique existential quantifiers"
     2.7 -  Pow           :: "'a set => 'a set set"                -- "powerset"
     2.8 -  image         :: "('a => 'b) => 'a set => 'b set"      (infixr "`" 90)
     2.9  
    2.10  local
    2.11  
    2.12 @@ -215,9 +213,6 @@
    2.13    supset_eq  ("op \<supseteq>") and
    2.14    supset_eq  ("(_/ \<supseteq> _)" [50, 51] 50)
    2.15  
    2.16 -abbreviation
    2.17 -  range :: "('a => 'b) => 'b set" where -- "of function"
    2.18 -  "range f == f ` UNIV"
    2.19  
    2.20  
    2.21  subsubsection "Bounded quantifiers"
    2.22 @@ -408,9 +403,15 @@
    2.23  
    2.24  end
    2.25  
    2.26 -defs
    2.27 -  Pow_def:      "Pow A          == {B. B <= A}"
    2.28 -  image_def:    "f`A            == {y. EX x:A. y = f(x)}"
    2.29 +definition Pow :: "'a set => 'a set set" where
    2.30 +  Pow_def: "Pow A = {B. B \<le> A}"
    2.31 +
    2.32 +definition image :: "('a => 'b) => 'a set => 'b set" (infixr "`" 90) where
    2.33 +  image_def: "f ` A = {y. EX x:A. y = f(x)}"
    2.34 +
    2.35 +abbreviation
    2.36 +  range :: "('a => 'b) => 'b set" where -- "of function"
    2.37 +  "range f == f ` UNIV"
    2.38  
    2.39  
    2.40  subsection {* Lemmas and proof tool setup *}
     3.1 --- a/src/HOL/Tools/datatype_package/datatype_rep_proofs.ML	Mon Jun 15 16:13:04 2009 +0200
     3.2 +++ b/src/HOL/Tools/datatype_package/datatype_rep_proofs.ML	Mon Jun 15 16:13:19 2009 +0200
     3.3 @@ -458,9 +458,9 @@
     3.4        let val isoT = T --> Univ_elT
     3.5        in HOLogic.imp $ 
     3.6          (Const (set_name, UnivT') $ mk_Free "x" Univ_elT i) $
     3.7 -          (if i < length newTs then Const ("True", HOLogic.boolT)
     3.8 +          (if i < length newTs then HOLogic.true_const
     3.9             else HOLogic.mk_mem (mk_Free "x" Univ_elT i,
    3.10 -             Const ("image", [isoT, HOLogic.mk_setT T] ---> UnivT) $
    3.11 +             Const (@{const_name image}, isoT --> HOLogic.mk_setT T --> UnivT) $
    3.12                 Const (iso_name, isoT) $ Const (@{const_name UNIV}, HOLogic.mk_setT T)))
    3.13        end;
    3.14