src/HOL/Quotient_Examples/Quotient_Cset.thy
author haftmann
Mon Dec 26 22:17:10 2011 +0100 (2011-12-26)
changeset 45990 b7b905b23b2a
parent 45986 c9e50153e5ae
child 47092 fa3538d6004b
permissions -rw-r--r--
incorporated More_Set and More_List into the Main body -- to be consolidated later
     1 (*  Title:      HOL/Quotient_Examples/Quotient_Cset.thy
     2     Author:     Florian Haftmann, Alexander Krauss, TU Muenchen
     3 *)
     4 
     5 header {* A variant of theory Cset from Library, defined as a quotient *}
     6 
     7 theory Quotient_Cset
     8 imports Main "~~/src/HOL/Library/Quotient_Syntax"
     9 begin
    10 
    11 subsection {* Lifting *}
    12 
    13 (*FIXME: quotient package requires a dedicated constant*)
    14 definition set_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
    15 where [simp]: "set_eq \<equiv> op ="
    16 
    17 quotient_type 'a set = "'a Set.set" / "set_eq"
    18 by (simp add: identity_equivp)
    19 
    20 hide_type (open) set
    21 
    22 subsection {* Operations *}
    23 
    24 lemma [quot_respect]:
    25   "(op = ===> set_eq ===> op =) (op \<in>) (op \<in>)"
    26   "(op = ===> set_eq) Collect Collect"
    27   "(set_eq ===> op =) Set.is_empty Set.is_empty"
    28   "(op = ===> set_eq ===> set_eq) Set.insert Set.insert"
    29   "(op = ===> set_eq ===> set_eq) Set.remove Set.remove"
    30   "(op = ===> set_eq ===> set_eq) image image"
    31   "(op = ===> set_eq ===> set_eq) Set.project Set.project"
    32   "(set_eq ===> op =) Ball Ball"
    33   "(set_eq ===> op =) Bex Bex"
    34   "(set_eq ===> op =) Finite_Set.card Finite_Set.card"
    35   "(set_eq ===> set_eq ===> op =) (op \<subseteq>) (op \<subseteq>)"
    36   "(set_eq ===> set_eq ===> op =) (op \<subset>) (op \<subset>)"
    37   "(set_eq ===> set_eq ===> set_eq) (op \<inter>) (op \<inter>)"
    38   "(set_eq ===> set_eq ===> set_eq) (op \<union>) (op \<union>)"
    39   "set_eq {} {}"
    40   "set_eq UNIV UNIV"
    41   "(set_eq ===> set_eq) uminus uminus"
    42   "(set_eq ===> set_eq ===> set_eq) minus minus"
    43   "(set_eq ===> op =) Inf Inf"
    44   "(set_eq ===> op =) Sup Sup"
    45   "(op = ===> set_eq) List.set List.set"
    46   "(set_eq ===> (op = ===> set_eq) ===> set_eq) UNION UNION"
    47 by (auto simp: fun_rel_eq)
    48 
    49 quotient_definition "member :: 'a => 'a Quotient_Cset.set => bool"
    50 is "op \<in>"
    51 quotient_definition "Set :: ('a => bool) => 'a Quotient_Cset.set"
    52 is Collect
    53 quotient_definition is_empty where "is_empty :: 'a Quotient_Cset.set \<Rightarrow> bool"
    54 is Set.is_empty
    55 quotient_definition insert where "insert :: 'a \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
    56 is Set.insert
    57 quotient_definition remove where "remove :: 'a \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
    58 is Set.remove
    59 quotient_definition map where "map :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'b Quotient_Cset.set"
    60 is image
    61 quotient_definition filter where "filter :: ('a \<Rightarrow> bool) \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
    62 is Set.project
    63 quotient_definition "forall :: 'a Quotient_Cset.set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
    64 is Ball
    65 quotient_definition "exists :: 'a Quotient_Cset.set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
    66 is Bex
    67 quotient_definition card where "card :: 'a Quotient_Cset.set \<Rightarrow> nat"
    68 is Finite_Set.card
    69 quotient_definition set where "set :: 'a list => 'a Quotient_Cset.set"
    70 is List.set
    71 quotient_definition subset where "subset :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> bool"
    72 is "op \<subseteq> :: 'a set \<Rightarrow> 'a set \<Rightarrow> bool"
    73 quotient_definition psubset where "psubset :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> bool"
    74 is "op \<subset> :: 'a set \<Rightarrow> 'a set \<Rightarrow> bool"
    75 quotient_definition inter where "inter :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
    76 is "op \<inter> :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
    77 quotient_definition union where "union :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
    78 is "op \<union> :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
    79 quotient_definition empty where "empty :: 'a Quotient_Cset.set"
    80 is "{} :: 'a set"
    81 quotient_definition UNIV where "UNIV :: 'a Quotient_Cset.set"
    82 is "Set.UNIV :: 'a set"
    83 quotient_definition uminus where "uminus :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
    84 is "uminus_class.uminus :: 'a set \<Rightarrow> 'a set"
    85 quotient_definition minus where "minus :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
    86 is "(op -) :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
    87 quotient_definition Inf where "Inf :: ('a :: Inf) Quotient_Cset.set \<Rightarrow> 'a"
    88 is "Inf_class.Inf :: ('a :: Inf) set \<Rightarrow> 'a"
    89 quotient_definition Sup where "Sup :: ('a :: Sup) Quotient_Cset.set \<Rightarrow> 'a"
    90 is "Sup_class.Sup :: ('a :: Sup) set \<Rightarrow> 'a"
    91 quotient_definition UNION where "UNION :: 'a Quotient_Cset.set \<Rightarrow> ('a \<Rightarrow> 'b Quotient_Cset.set) \<Rightarrow> 'b Quotient_Cset.set"
    92 is "Complete_Lattices.UNION :: 'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"
    93 
    94 hide_const (open) is_empty insert remove map filter forall exists card
    95   set subset psubset inter union empty UNIV uminus minus Inf Sup UNION
    96 
    97 hide_fact (open) is_empty_def insert_def remove_def map_def filter_def
    98   forall_def exists_def card_def set_def subset_def psubset_def
    99   inter_def union_def empty_def UNIV_def uminus_def minus_def Inf_def Sup_def
   100   UNION_eq
   101 
   102 end