src/HOL/Library/List_Cset.thy
author haftmann
Fri, 26 Aug 2011 23:02:00 +0200
changeset 44556 c0fd385a41f4
parent 43979 9f27d2bf4087
child 44558 cc878a312673
permissions -rw-r--r--
adapted to changes in Cset.thy
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43241
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
     1
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
     2
(* Author: Florian Haftmann, TU Muenchen *)
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
     3
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
     4
header {* implementation of Cset.sets based on lists *}
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
     5
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
     6
theory List_Cset
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
     7
imports Cset
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
     8
begin
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
     9
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    10
declare mem_def [simp]
43971
892030194015 added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents: 43307
diff changeset
    11
declare Cset.set_code [code del]
43241
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    12
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    13
definition coset :: "'a list \<Rightarrow> 'a Cset.set" where
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    14
  "coset xs = Set (- set xs)"
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    15
hide_const (open) coset
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    16
44556
c0fd385a41f4 adapted to changes in Cset.thy
haftmann
parents: 43979
diff changeset
    17
lemma set_of_coset [simp]:
c0fd385a41f4 adapted to changes in Cset.thy
haftmann
parents: 43979
diff changeset
    18
  "set_of (List_Cset.coset xs) = - set xs"
c0fd385a41f4 adapted to changes in Cset.thy
haftmann
parents: 43979
diff changeset
    19
  by (simp add: coset_def)
c0fd385a41f4 adapted to changes in Cset.thy
haftmann
parents: 43979
diff changeset
    20
43241
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    21
lemma member_coset [simp]:
44556
c0fd385a41f4 adapted to changes in Cset.thy
haftmann
parents: 43979
diff changeset
    22
  "member (List_Cset.coset xs) = (\<lambda>x. x \<in> - set xs)"
c0fd385a41f4 adapted to changes in Cset.thy
haftmann
parents: 43979
diff changeset
    23
  by (simp add: coset_def fun_eq_iff)
43241
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    24
hide_fact (open) member_coset
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    25
43971
892030194015 added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents: 43307
diff changeset
    26
code_datatype Cset.set List_Cset.coset
43241
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    27
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    28
lemma member_code [code]:
43971
892030194015 added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents: 43307
diff changeset
    29
  "member (Cset.set xs) = List.member xs"
43241
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    30
  "member (List_Cset.coset xs) = Not \<circ> List.member xs"
44556
c0fd385a41f4 adapted to changes in Cset.thy
haftmann
parents: 43979
diff changeset
    31
  by (simp_all add: fun_eq_iff member_def fun_Compl_def member_set)
43241
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    32
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    33
definition (in term_syntax)
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    34
  setify :: "'a\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    35
    \<Rightarrow> 'a Cset.set \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
43971
892030194015 added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents: 43307
diff changeset
    36
  [code_unfold]: "setify xs = Code_Evaluation.valtermify Cset.set {\<cdot>} xs"
43241
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    37
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    38
notation fcomp (infixl "\<circ>>" 60)
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    39
notation scomp (infixl "\<circ>\<rightarrow>" 60)
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    40
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    41
instantiation Cset.set :: (random) random
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    42
begin
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    43
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    44
definition
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    45
  "Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>xs. Pair (setify xs))"
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    46
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    47
instance ..
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    48
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    49
end
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    50
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    51
no_notation fcomp (infixl "\<circ>>" 60)
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    52
no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    53
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    54
subsection {* Basic operations *}
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    55
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    56
lemma is_empty_set [code]:
43971
892030194015 added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents: 43307
diff changeset
    57
  "Cset.is_empty (Cset.set xs) \<longleftrightarrow> List.null xs"
43241
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    58
  by (simp add: is_empty_set null_def)
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    59
hide_fact (open) is_empty_set
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    60
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    61
lemma empty_set [code]:
43971
892030194015 added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents: 43307
diff changeset
    62
  "Cset.empty = Cset.set []"
43241
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    63
  by (simp add: set_def)
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    64
hide_fact (open) empty_set
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    65
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    66
lemma UNIV_set [code]:
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    67
  "top = List_Cset.coset []"
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    68
  by (simp add: coset_def)
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    69
hide_fact (open) UNIV_set
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    70
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    71
lemma remove_set [code]:
43971
892030194015 added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents: 43307
diff changeset
    72
  "Cset.remove x (Cset.set xs) = Cset.set (removeAll x xs)"
43241
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    73
  "Cset.remove x (List_Cset.coset xs) = List_Cset.coset (List.insert x xs)"
43971
892030194015 added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents: 43307
diff changeset
    74
by (simp_all add: Cset.set_def coset_def)
43241
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    75
  (metis List.set_insert More_Set.remove_def remove_set_compl)
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    76
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    77
lemma insert_set [code]:
43971
892030194015 added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents: 43307
diff changeset
    78
  "Cset.insert x (Cset.set xs) = Cset.set (List.insert x xs)"
43241
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    79
  "Cset.insert x (List_Cset.coset xs) = List_Cset.coset (removeAll x xs)"
43971
892030194015 added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents: 43307
diff changeset
    80
  by (simp_all add: Cset.set_def coset_def)
43241
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    81
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    82
lemma map_set [code]:
43971
892030194015 added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents: 43307
diff changeset
    83
  "Cset.map f (Cset.set xs) = Cset.set (remdups (List.map f xs))"
892030194015 added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents: 43307
diff changeset
    84
  by (simp add: Cset.set_def)
43241
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    85
  
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    86
lemma filter_set [code]:
43971
892030194015 added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents: 43307
diff changeset
    87
  "Cset.filter P (Cset.set xs) = Cset.set (List.filter P xs)"
892030194015 added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents: 43307
diff changeset
    88
  by (simp add: Cset.set_def project_set)
43241
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    89
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    90
lemma forall_set [code]:
43971
892030194015 added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents: 43307
diff changeset
    91
  "Cset.forall P (Cset.set xs) \<longleftrightarrow> list_all P xs"
892030194015 added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents: 43307
diff changeset
    92
  by (simp add: Cset.set_def list_all_iff)
43241
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    93
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    94
lemma exists_set [code]:
43971
892030194015 added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents: 43307
diff changeset
    95
  "Cset.exists P (Cset.set xs) \<longleftrightarrow> list_ex P xs"
892030194015 added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents: 43307
diff changeset
    96
  by (simp add: Cset.set_def list_ex_iff)
43241
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    97
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
    98
lemma card_set [code]:
43971
892030194015 added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents: 43307
diff changeset
    99
  "Cset.card (Cset.set xs) = length (remdups xs)"
43241
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   100
proof -
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   101
  have "Finite_Set.card (set (remdups xs)) = length (remdups xs)"
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   102
    by (rule distinct_card) simp
43971
892030194015 added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents: 43307
diff changeset
   103
  then show ?thesis by (simp add: Cset.set_def)
43241
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   104
qed
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   105
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   106
lemma compl_set [simp, code]:
43971
892030194015 added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents: 43307
diff changeset
   107
  "- Cset.set xs = List_Cset.coset xs"
892030194015 added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents: 43307
diff changeset
   108
  by (simp add: Cset.set_def coset_def)
43241
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   109
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   110
lemma compl_coset [simp, code]:
43971
892030194015 added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents: 43307
diff changeset
   111
  "- List_Cset.coset xs = Cset.set xs"
892030194015 added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents: 43307
diff changeset
   112
  by (simp add: Cset.set_def coset_def)
43241
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   113
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   114
context complete_lattice
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   115
begin
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   116
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   117
lemma Infimum_inf [code]:
43971
892030194015 added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents: 43307
diff changeset
   118
  "Infimum (Cset.set As) = foldr inf As top"
43241
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   119
  "Infimum (List_Cset.coset []) = bot"
44556
c0fd385a41f4 adapted to changes in Cset.thy
haftmann
parents: 43979
diff changeset
   120
  by (simp_all add: Inf_set_foldr)
43241
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   121
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   122
lemma Supremum_sup [code]:
43971
892030194015 added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents: 43307
diff changeset
   123
  "Supremum (Cset.set As) = foldr sup As bot"
43241
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   124
  "Supremum (List_Cset.coset []) = top"
44556
c0fd385a41f4 adapted to changes in Cset.thy
haftmann
parents: 43979
diff changeset
   125
  by (simp_all add: Sup_set_foldr)
43241
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   126
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   127
end
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   128
43979
9f27d2bf4087 fixed code generator setup in List_Cset
Andreas Lochbihler
parents: 43971
diff changeset
   129
declare Cset.single_code [code del]
43971
892030194015 added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents: 43307
diff changeset
   130
lemma single_set [code]:
892030194015 added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents: 43307
diff changeset
   131
  "Cset.single a = Cset.set [a]"
892030194015 added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents: 43307
diff changeset
   132
by(simp add: Cset.single_code)
892030194015 added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents: 43307
diff changeset
   133
hide_fact (open) single_set
892030194015 added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents: 43307
diff changeset
   134
892030194015 added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents: 43307
diff changeset
   135
lemma bind_set [code]:
44556
c0fd385a41f4 adapted to changes in Cset.thy
haftmann
parents: 43979
diff changeset
   136
  "Cset.bind (Cset.set xs) f = fold (sup \<circ> f) xs (Cset.set [])"
c0fd385a41f4 adapted to changes in Cset.thy
haftmann
parents: 43979
diff changeset
   137
  by (simp add: Cset.bind_def SUPR_set_fold)
43971
892030194015 added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents: 43307
diff changeset
   138
892030194015 added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents: 43307
diff changeset
   139
lemma pred_of_cset_set [code]:
892030194015 added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents: 43307
diff changeset
   140
  "pred_of_cset (Cset.set xs) = foldr sup (map Predicate.single xs) bot"
892030194015 added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents: 43307
diff changeset
   141
proof -
892030194015 added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents: 43307
diff changeset
   142
  have "pred_of_cset (Cset.set xs) = Predicate.Pred (\<lambda>x. x \<in> set xs)"
44556
c0fd385a41f4 adapted to changes in Cset.thy
haftmann
parents: 43979
diff changeset
   143
    by (simp add: Cset.pred_of_cset_def member_code member_set)
43971
892030194015 added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents: 43307
diff changeset
   144
  moreover have "foldr sup (map Predicate.single xs) bot = \<dots>"
44556
c0fd385a41f4 adapted to changes in Cset.thy
haftmann
parents: 43979
diff changeset
   145
    by (induct xs) (auto simp add: bot_pred_def simp del: mem_def intro: pred_eqI, simp)
c0fd385a41f4 adapted to changes in Cset.thy
haftmann
parents: 43979
diff changeset
   146
  ultimately show ?thesis by simp
43971
892030194015 added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents: 43307
diff changeset
   147
qed
892030194015 added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents: 43307
diff changeset
   148
hide_fact (open) pred_of_cset_set
43241
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   149
44556
c0fd385a41f4 adapted to changes in Cset.thy
haftmann
parents: 43979
diff changeset
   150
43241
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   151
subsection {* Derived operations *}
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   152
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   153
lemma subset_eq_forall [code]:
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   154
  "A \<le> B \<longleftrightarrow> Cset.forall (member B) A"
44556
c0fd385a41f4 adapted to changes in Cset.thy
haftmann
parents: 43979
diff changeset
   155
  by (simp add: subset_eq member_def)
43241
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   156
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   157
lemma subset_subset_eq [code]:
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   158
  "A < B \<longleftrightarrow> A \<le> B \<and> \<not> B \<le> (A :: 'a Cset.set)"
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   159
  by (fact less_le_not_le)
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   160
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   161
instantiation Cset.set :: (type) equal
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   162
begin
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   163
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   164
definition [code]:
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   165
  "HOL.equal A B \<longleftrightarrow> A \<le> B \<and> B \<le> (A :: 'a Cset.set)"
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   166
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   167
instance proof
44556
c0fd385a41f4 adapted to changes in Cset.thy
haftmann
parents: 43979
diff changeset
   168
qed (simp add: equal_set_def set_eq [symmetric] Cset.set_eq_iff fun_eq_iff member_def)
43241
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   169
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   170
end
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   171
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   172
lemma [code nbe]:
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   173
  "HOL.equal (A :: 'a Cset.set) A \<longleftrightarrow> True"
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   174
  by (fact equal_refl)
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   175
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   176
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   177
subsection {* Functorial operations *}
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   178
44556
c0fd385a41f4 adapted to changes in Cset.thy
haftmann
parents: 43979
diff changeset
   179
lemma member_cset_of:
c0fd385a41f4 adapted to changes in Cset.thy
haftmann
parents: 43979
diff changeset
   180
  "member = set_of"
c0fd385a41f4 adapted to changes in Cset.thy
haftmann
parents: 43979
diff changeset
   181
  by (rule ext)+ (simp add: member_def)
c0fd385a41f4 adapted to changes in Cset.thy
haftmann
parents: 43979
diff changeset
   182
43241
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   183
lemma inter_project [code]:
43971
892030194015 added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents: 43307
diff changeset
   184
  "inf A (Cset.set xs) = Cset.set (List.filter (Cset.member A) xs)"
43241
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   185
  "inf A (List_Cset.coset xs) = foldr Cset.remove xs A"
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   186
proof -
43971
892030194015 added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents: 43307
diff changeset
   187
  show "inf A (Cset.set xs) = Cset.set (List.filter (member A) xs)"
44556
c0fd385a41f4 adapted to changes in Cset.thy
haftmann
parents: 43979
diff changeset
   188
    by (simp add: inter project_def Cset.set_def member_cset_of)
43241
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   189
  have *: "\<And>x::'a. Cset.remove = (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member)"
44556
c0fd385a41f4 adapted to changes in Cset.thy
haftmann
parents: 43979
diff changeset
   190
    by (simp add: fun_eq_iff More_Set.remove_def member_cset_of)
43241
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   191
  have "member \<circ> fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member) xs =
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   192
    fold More_Set.remove xs \<circ> member"
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   193
    by (rule fold_commute) (simp add: fun_eq_iff)
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   194
  then have "fold More_Set.remove xs (member A) = 
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   195
    member (fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member) xs A)"
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   196
    by (simp add: fun_eq_iff)
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   197
  then have "inf A (List_Cset.coset xs) = fold Cset.remove xs A"
44556
c0fd385a41f4 adapted to changes in Cset.thy
haftmann
parents: 43979
diff changeset
   198
    by (simp add: Diff_eq [symmetric] minus_set * member_cset_of)
43241
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   199
  moreover have "\<And>x y :: 'a. Cset.remove y \<circ> Cset.remove x = Cset.remove x \<circ> Cset.remove y"
44556
c0fd385a41f4 adapted to changes in Cset.thy
haftmann
parents: 43979
diff changeset
   200
    by (auto simp add: More_Set.remove_def * member_cset_of intro: ext)
43241
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   201
  ultimately show "inf A (List_Cset.coset xs) = foldr Cset.remove xs A"
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   202
    by (simp add: foldr_fold)
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   203
qed
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   204
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   205
lemma subtract_remove [code]:
43971
892030194015 added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents: 43307
diff changeset
   206
  "A - Cset.set xs = foldr Cset.remove xs A"
892030194015 added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents: 43307
diff changeset
   207
  "A - List_Cset.coset xs = Cset.set (List.filter (member A) xs)"
43241
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   208
  by (simp_all only: diff_eq compl_set compl_coset inter_project)
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   209
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   210
lemma union_insert [code]:
43971
892030194015 added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents: 43307
diff changeset
   211
  "sup (Cset.set xs) A = foldr Cset.insert xs A"
43241
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   212
  "sup (List_Cset.coset xs) A = List_Cset.coset (List.filter (Not \<circ> member A) xs)"
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   213
proof -
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   214
  have *: "\<And>x::'a. Cset.insert = (\<lambda>x. Set \<circ> Set.insert x \<circ> member)"
44556
c0fd385a41f4 adapted to changes in Cset.thy
haftmann
parents: 43979
diff changeset
   215
    by (simp add: fun_eq_iff member_cset_of)
43241
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   216
  have "member \<circ> fold (\<lambda>x. Set \<circ> Set.insert x \<circ> member) xs =
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   217
    fold Set.insert xs \<circ> member"
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   218
    by (rule fold_commute) (simp add: fun_eq_iff)
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   219
  then have "fold Set.insert xs (member A) =
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   220
    member (fold (\<lambda>x. Set \<circ> Set.insert x \<circ> member) xs A)"
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   221
    by (simp add: fun_eq_iff)
43971
892030194015 added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents: 43307
diff changeset
   222
  then have "sup (Cset.set xs) A = fold Cset.insert xs A"
44556
c0fd385a41f4 adapted to changes in Cset.thy
haftmann
parents: 43979
diff changeset
   223
    by (simp add: union_set * member_cset_of)
43241
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   224
  moreover have "\<And>x y :: 'a. Cset.insert y \<circ> Cset.insert x = Cset.insert x \<circ> Cset.insert y"
44556
c0fd385a41f4 adapted to changes in Cset.thy
haftmann
parents: 43979
diff changeset
   225
    by (auto simp add: * member_cset_of intro: ext)
43971
892030194015 added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents: 43307
diff changeset
   226
  ultimately show "sup (Cset.set xs) A = foldr Cset.insert xs A"
43241
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   227
    by (simp add: foldr_fold)
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   228
  show "sup (List_Cset.coset xs) A = List_Cset.coset (List.filter (Not \<circ> member A) xs)"
44556
c0fd385a41f4 adapted to changes in Cset.thy
haftmann
parents: 43979
diff changeset
   229
    by (auto simp add: coset_def member_cset_of)
43241
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   230
qed
93b1183e43e5 splitting Cset into Cset and List_Cset
bulwahn
parents:
diff changeset
   231
43307
1a32a953cef1 local simp rule in List_Cset
bulwahn
parents: 43241
diff changeset
   232
declare mem_def[simp del]
1a32a953cef1 local simp rule in List_Cset
bulwahn
parents: 43241
diff changeset
   233
44556
c0fd385a41f4 adapted to changes in Cset.thy
haftmann
parents: 43979
diff changeset
   234
end