src/HOL/Library/List_Cset.thy
author kuncar
Fri Dec 09 18:07:04 2011 +0100 (2011-12-09)
changeset 45802 b16f976db515
parent 44560 1711be44e76a
child 45969 562e99c3d316
permissions -rw-r--r--
Quotient_Info stores only relation maps
     1 
     2 (* Author: Florian Haftmann, TU Muenchen *)
     3 
     4 header {* implementation of Cset.sets based on lists *}
     5 
     6 theory List_Cset
     7 imports Cset
     8 begin
     9 
    10 code_datatype Cset.set Cset.coset
    11 
    12 lemma member_code [code]:
    13   "member (Cset.set xs) = List.member xs"
    14   "member (Cset.coset xs) = Not \<circ> List.member xs"
    15   by (simp_all add: fun_eq_iff List.member_def)
    16 
    17 definition (in term_syntax)
    18   setify :: "'a\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
    19     \<Rightarrow> 'a Cset.set \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
    20   [code_unfold]: "setify xs = Code_Evaluation.valtermify Cset.set {\<cdot>} xs"
    21 
    22 notation fcomp (infixl "\<circ>>" 60)
    23 notation scomp (infixl "\<circ>\<rightarrow>" 60)
    24 
    25 instantiation Cset.set :: (random) random
    26 begin
    27 
    28 definition
    29   "Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>xs. Pair (setify xs))"
    30 
    31 instance ..
    32 
    33 end
    34 
    35 no_notation fcomp (infixl "\<circ>>" 60)
    36 no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
    37 
    38 subsection {* Basic operations *}
    39 
    40 lemma is_empty_set [code]:
    41   "Cset.is_empty (Cset.set xs) \<longleftrightarrow> List.null xs"
    42   by (simp add: is_empty_set null_def)
    43 hide_fact (open) is_empty_set
    44 
    45 lemma empty_set [code]:
    46   "Cset.empty = Cset.set []"
    47   by simp
    48 hide_fact (open) empty_set
    49 
    50 lemma UNIV_set [code]:
    51   "top = Cset.coset []"
    52   by (simp add: Cset.coset_def)
    53 hide_fact (open) UNIV_set
    54 
    55 lemma remove_set [code]:
    56   "Cset.remove x (Cset.set xs) = Cset.set (removeAll x xs)"
    57   "Cset.remove x (Cset.coset xs) = Cset.coset (List.insert x xs)"
    58   by (simp_all add: Cset.set_def Cset.coset_def Compl_insert)
    59 
    60 lemma insert_set [code]:
    61   "Cset.insert x (Cset.set xs) = Cset.set (List.insert x xs)"
    62   "Cset.insert x (Cset.coset xs) = Cset.coset (removeAll x xs)"
    63   by (simp_all add: Cset.set_def Cset.coset_def)
    64 
    65 declare compl_set [code]
    66 declare compl_coset [code]
    67 declare subtract_remove [code]
    68 
    69 lemma map_set [code]:
    70   "Cset.map f (Cset.set xs) = Cset.set (remdups (List.map f xs))"
    71   by (simp add: Cset.set_def)
    72   
    73 lemma filter_set [code]:
    74   "Cset.filter P (Cset.set xs) = Cset.set (List.filter P xs)"
    75   by (simp add: Cset.set_def project_set)
    76 
    77 lemma forall_set [code]:
    78   "Cset.forall P (Cset.set xs) \<longleftrightarrow> list_all P xs"
    79   by (simp add: Cset.set_def list_all_iff)
    80 
    81 lemma exists_set [code]:
    82   "Cset.exists P (Cset.set xs) \<longleftrightarrow> list_ex P xs"
    83   by (simp add: Cset.set_def list_ex_iff)
    84 
    85 lemma card_set [code]:
    86   "Cset.card (Cset.set xs) = length (remdups xs)"
    87 proof -
    88   have "Finite_Set.card (set (remdups xs)) = length (remdups xs)"
    89     by (rule distinct_card) simp
    90   then show ?thesis by (simp add: Cset.set_def)
    91 qed
    92 
    93 context complete_lattice
    94 begin
    95 
    96 declare Infimum_inf [code]
    97 declare Supremum_sup [code]
    98 
    99 end
   100 
   101 declare Cset.single_code [code del]
   102 lemma single_set [code]:
   103   "Cset.single a = Cset.set [a]"
   104 by(simp add: Cset.single_code)
   105 hide_fact (open) single_set
   106 
   107 declare Cset.bind_set [code]
   108 declare Cset.pred_of_cset_set [code]
   109 
   110 
   111 subsection {* Derived operations *}
   112 
   113 lemma subset_eq_forall [code]:
   114   "A \<le> B \<longleftrightarrow> Cset.forall (member B) A"
   115   by (simp add: subset_eq member_def)
   116 
   117 lemma subset_subset_eq [code]:
   118   "A < B \<longleftrightarrow> A \<le> B \<and> \<not> B \<le> (A :: 'a Cset.set)"
   119   by (fact less_le_not_le)
   120 
   121 instantiation Cset.set :: (type) equal
   122 begin
   123 
   124 definition [code]:
   125   "HOL.equal A B \<longleftrightarrow> A \<le> B \<and> B \<le> (A :: 'a Cset.set)"
   126 
   127 instance proof
   128 qed (auto simp add: equal_set_def Cset.set_eq_iff Cset.member_def fun_eq_iff mem_def)
   129 
   130 end
   131 
   132 lemma [code nbe]:
   133   "HOL.equal (A :: 'a Cset.set) A \<longleftrightarrow> True"
   134   by (fact equal_refl)
   135 
   136 
   137 subsection {* Functorial operations *}
   138 
   139 declare inter_project [code]
   140 declare union_insert [code]
   141 
   142 end