src/HOL/Library/ExecutableSet.thy
author haftmann
Mon, 18 Dec 2006 08:21:31 +0100
changeset 21875 5df10a17644e
parent 21572 7442833ea2b6
child 21911 e29bcab0c81c
permissions -rw-r--r--
explicit nonfix declaration for ML "subset"
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17632
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
     1
(*  Title:      HOL/Library/ExecutableSet.thy
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
     2
    ID:         $Id$
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
     3
    Author:     Stefan Berghofer, TU Muenchen
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
     4
*)
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
     5
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
     6
header {* Implementation of finite sets by lists *}
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
     7
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
     8
theory ExecutableSet
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
     9
imports Main
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
    10
begin
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
    11
21323
haftmann
parents: 21321
diff changeset
    12
section {* Definitional rewrites *}
20597
65fe827aa595 code generation 2 adjustments
haftmann
parents: 20523
diff changeset
    13
65fe827aa595 code generation 2 adjustments
haftmann
parents: 20523
diff changeset
    14
instance set :: (eq) eq ..
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    15
21385
cf398bb8a8be added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents: 21323
diff changeset
    16
definition
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21385
diff changeset
    17
  minus_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
21385
cf398bb8a8be added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents: 21323
diff changeset
    18
  "minus_set xs ys = ys - xs"
cf398bb8a8be added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents: 21323
diff changeset
    19
cf398bb8a8be added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents: 21323
diff changeset
    20
lemma [code inline]:
cf398bb8a8be added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents: 21323
diff changeset
    21
  "op - = (\<lambda>xs ys. minus_set ys xs)"
cf398bb8a8be added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents: 21323
diff changeset
    22
  unfolding minus_set_def ..
cf398bb8a8be added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents: 21323
diff changeset
    23
cf398bb8a8be added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents: 21323
diff changeset
    24
definition
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21385
diff changeset
    25
  subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21385
diff changeset
    26
  "subset = op \<subseteq>"
21385
cf398bb8a8be added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents: 21323
diff changeset
    27
cf398bb8a8be added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents: 21323
diff changeset
    28
lemmas [symmetric, code inline] = subset_def
cf398bb8a8be added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents: 21323
diff changeset
    29
21572
7442833ea2b6 added strict_subset
haftmann
parents: 21511
diff changeset
    30
definition
7442833ea2b6 added strict_subset
haftmann
parents: 21511
diff changeset
    31
  strict_subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where 
7442833ea2b6 added strict_subset
haftmann
parents: 21511
diff changeset
    32
  "strict_subset = op \<subset>"
7442833ea2b6 added strict_subset
haftmann
parents: 21511
diff changeset
    33
7442833ea2b6 added strict_subset
haftmann
parents: 21511
diff changeset
    34
lemmas [symmetric, code inline] = strict_subset_def
7442833ea2b6 added strict_subset
haftmann
parents: 21511
diff changeset
    35
21153
8288c8f203de adapted to changes in codegen_data.ML
haftmann
parents: 21125
diff changeset
    36
lemma [code target: Set]:
21385
cf398bb8a8be added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents: 21323
diff changeset
    37
  "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
17632
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
    38
  by blast
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
    39
20597
65fe827aa595 code generation 2 adjustments
haftmann
parents: 20523
diff changeset
    40
lemma [code func]:
21572
7442833ea2b6 added strict_subset
haftmann
parents: 21511
diff changeset
    41
  "(A\<Colon>'a\<Colon>eq set) = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
7442833ea2b6 added strict_subset
haftmann
parents: 21511
diff changeset
    42
  by blast
7442833ea2b6 added strict_subset
haftmann
parents: 21511
diff changeset
    43
7442833ea2b6 added strict_subset
haftmann
parents: 21511
diff changeset
    44
lemma [code func]:
21385
cf398bb8a8be added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents: 21323
diff changeset
    45
  "subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
cf398bb8a8be added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents: 21323
diff changeset
    46
  unfolding subset_def Set.subset_def ..
20597
65fe827aa595 code generation 2 adjustments
haftmann
parents: 20523
diff changeset
    47
21572
7442833ea2b6 added strict_subset
haftmann
parents: 21511
diff changeset
    48
lemma [code func]:
7442833ea2b6 added strict_subset
haftmann
parents: 21511
diff changeset
    49
  "strict_subset A B \<longleftrightarrow> subset A B \<and> A \<noteq> B"
7442833ea2b6 added strict_subset
haftmann
parents: 21511
diff changeset
    50
  unfolding subset_def strict_subset_def by blast
7442833ea2b6 added strict_subset
haftmann
parents: 21511
diff changeset
    51
21323
haftmann
parents: 21321
diff changeset
    52
lemma [code]:
haftmann
parents: 21321
diff changeset
    53
  "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. x = a)"
haftmann
parents: 21321
diff changeset
    54
  unfolding bex_triv_one_point1 ..
17632
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
    55
21385
cf398bb8a8be added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents: 21323
diff changeset
    56
definition
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21385
diff changeset
    57
  filter_set :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21385
diff changeset
    58
  "filter_set P xs = {x\<in>xs. P x}"
20597
65fe827aa595 code generation 2 adjustments
haftmann
parents: 20523
diff changeset
    59
21385
cf398bb8a8be added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents: 21323
diff changeset
    60
lemmas [symmetric, code inline] = filter_set_def
cf398bb8a8be added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents: 21323
diff changeset
    61
cf398bb8a8be added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents: 21323
diff changeset
    62
cf398bb8a8be added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents: 21323
diff changeset
    63
section {* Operations on lists *}
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    64
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    65
subsection {* Basic definitions *}
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    66
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    67
definition
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21385
diff changeset
    68
  flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    69
  "flip f a b = f b a"
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21385
diff changeset
    70
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21385
diff changeset
    71
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21385
diff changeset
    72
  member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool" where
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    73
  "member xs x = (x \<in> set xs)"
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21385
diff changeset
    74
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21385
diff changeset
    75
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21385
diff changeset
    76
  insertl :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    77
  "insertl x xs = (if member xs x then xs else x#xs)"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    78
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    79
lemma
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    80
  [code target: List]: "member [] y = False"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    81
  and [code target: List]: "member (x#xs) y = (y = x \<or> member xs y)"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    82
unfolding member_def by (induct xs) simp_all
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    83
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    84
consts
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    85
  drop_first :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    86
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    87
primrec
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    88
  "drop_first f [] = []"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    89
  "drop_first f (x#xs) = (if f x then xs else x # drop_first f xs)"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    90
declare drop_first.simps [code del]
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    91
declare drop_first.simps [code target: List]
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    92
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    93
declare remove1.simps [code del]
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    94
lemma [code target: List]:
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    95
  "remove1 x xs = (if member xs x then drop_first (\<lambda>y. y = x) xs else xs)"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    96
proof (cases "member xs x")
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    97
  case False thus ?thesis unfolding member_def by (induct xs) auto
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    98
next
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    99
  case True
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   100
  have "remove1 x xs = drop_first (\<lambda>y. y = x) xs" by (induct xs) simp_all
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   101
  with True show ?thesis by simp
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   102
qed
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   103
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   104
lemma member_nil [simp]:
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   105
  "member [] = (\<lambda>x. False)"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   106
proof
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   107
  fix x
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   108
  show "member [] x = False" unfolding member_def by simp
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   109
qed
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   110
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   111
lemma member_insertl [simp]:
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   112
  "x \<in> set (insertl x xs)"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   113
  unfolding insertl_def member_def mem_iff by simp
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   114
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   115
lemma insertl_member [simp]:
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   116
  fixes xs x
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   117
  assumes member: "member xs x"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   118
  shows "insertl x xs = xs"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   119
  using member unfolding insertl_def by simp
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   120
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   121
lemma insertl_not_member [simp]:
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   122
  fixes xs x
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   123
  assumes member: "\<not> (member xs x)"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   124
  shows "insertl x xs = x # xs"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   125
  using member unfolding insertl_def by simp
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   126
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   127
lemma foldr_remove1_empty [simp]:
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   128
  "foldr remove1 xs [] = []"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   129
  by (induct xs) simp_all
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   130
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   131
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   132
subsection {* Derived definitions *}
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   133
20934
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   134
function unionl :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20503
diff changeset
   135
where
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   136
  "unionl [] ys = ys"
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20503
diff changeset
   137
| "unionl xs ys = foldr insertl xs ys"
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20503
diff changeset
   138
by pat_completeness auto
21321
9022a90f6fdd auto_term => lexicographic_order
krauss
parents: 21191
diff changeset
   139
termination by lexicographic_order
9022a90f6fdd auto_term => lexicographic_order
krauss
parents: 21191
diff changeset
   140
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   141
lemmas unionl_def = unionl.simps(2)
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   142
20934
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   143
function intersect :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20503
diff changeset
   144
where
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   145
  "intersect [] ys = []"
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20503
diff changeset
   146
| "intersect xs [] = []"
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20503
diff changeset
   147
| "intersect xs ys = filter (member xs) ys"
21321
9022a90f6fdd auto_term => lexicographic_order
krauss
parents: 21191
diff changeset
   148
by pat_completeness auto
9022a90f6fdd auto_term => lexicographic_order
krauss
parents: 21191
diff changeset
   149
termination by lexicographic_order
9022a90f6fdd auto_term => lexicographic_order
krauss
parents: 21191
diff changeset
   150
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   151
lemmas intersect_def = intersect.simps(3)
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   152
20934
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   153
function subtract :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20503
diff changeset
   154
where
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   155
  "subtract [] ys = ys"
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20503
diff changeset
   156
| "subtract xs [] = []"
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20503
diff changeset
   157
| "subtract xs ys = foldr remove1 xs ys"
21321
9022a90f6fdd auto_term => lexicographic_order
krauss
parents: 21191
diff changeset
   158
by pat_completeness auto
9022a90f6fdd auto_term => lexicographic_order
krauss
parents: 21191
diff changeset
   159
termination by lexicographic_order
9022a90f6fdd auto_term => lexicographic_order
krauss
parents: 21191
diff changeset
   160
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   161
lemmas subtract_def = subtract.simps(3)
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   162
20934
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   163
function map_distinct :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20503
diff changeset
   164
where
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   165
  "map_distinct f [] = []"
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20503
diff changeset
   166
| "map_distinct f xs = foldr (insertl o f) xs []"
21321
9022a90f6fdd auto_term => lexicographic_order
krauss
parents: 21191
diff changeset
   167
by pat_completeness auto
9022a90f6fdd auto_term => lexicographic_order
krauss
parents: 21191
diff changeset
   168
termination by lexicographic_order
9022a90f6fdd auto_term => lexicographic_order
krauss
parents: 21191
diff changeset
   169
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   170
lemmas map_distinct_def = map_distinct.simps(2)
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   171
20934
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   172
function unions :: "'a list list \<Rightarrow> 'a list"
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20503
diff changeset
   173
where
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   174
  "unions [] = []"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   175
  "unions xs = foldr unionl xs []"
21321
9022a90f6fdd auto_term => lexicographic_order
krauss
parents: 21191
diff changeset
   176
by pat_completeness auto
9022a90f6fdd auto_term => lexicographic_order
krauss
parents: 21191
diff changeset
   177
termination by lexicographic_order
9022a90f6fdd auto_term => lexicographic_order
krauss
parents: 21191
diff changeset
   178
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   179
lemmas unions_def = unions.simps(2)
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   180
20934
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   181
consts intersects :: "'a list list \<Rightarrow> 'a list"
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   182
primrec
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   183
  "intersects (x#xs) = foldr intersect xs x"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   184
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   185
definition
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21385
diff changeset
   186
  map_union :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   187
  "map_union xs f = unions (map f xs)"
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21385
diff changeset
   188
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21385
diff changeset
   189
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21385
diff changeset
   190
  map_inter :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   191
  "map_inter xs f = intersects (map f xs)"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   192
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   193
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   194
section {* Isomorphism proofs *}
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   195
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   196
lemma iso_member:
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   197
  "member xs x = (x \<in> set xs)"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   198
  unfolding member_def mem_iff ..
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   199
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   200
lemma iso_insert:
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   201
  "set (insertl x xs) = insert x (set xs)"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   202
  unfolding insertl_def iso_member by (simp add: Set.insert_absorb)
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   203
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   204
lemma iso_remove1:
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   205
  assumes distnct: "distinct xs"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   206
  shows "set (remove1 x xs) = set xs - {x}"
21385
cf398bb8a8be added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents: 21323
diff changeset
   207
  using distnct set_remove1_eq by auto
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   208
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   209
lemma iso_union:
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   210
  "set (unionl xs ys) = set xs \<union> set ys"
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20503
diff changeset
   211
  unfolding unionl_def
21385
cf398bb8a8be added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents: 21323
diff changeset
   212
  by (induct xs arbitrary: ys) (simp_all add: iso_insert)
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   213
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   214
lemma iso_intersect:
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   215
  "set (intersect xs ys) = set xs \<inter> set ys"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   216
  unfolding intersect_def Int_def by (simp add: Int_def iso_member) auto
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   217
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   218
lemma iso_subtract:
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   219
  fixes ys
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   220
  assumes distnct: "distinct ys"
21385
cf398bb8a8be added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents: 21323
diff changeset
   221
  shows "set (subtract xs ys) = minus_set (set xs) (set ys)"
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   222
  and "distinct (subtract xs ys)"
21385
cf398bb8a8be added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents: 21323
diff changeset
   223
  unfolding subtract_def minus_set_def
cf398bb8a8be added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents: 21323
diff changeset
   224
  using distnct by (induct xs arbitrary: ys) auto
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   225
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   226
lemma iso_map_distinct:
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   227
  "set (map_distinct f xs) = image f (set xs)"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   228
  unfolding map_distinct_def by (induct xs) (simp_all add: iso_insert)
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   229
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   230
lemma iso_unions:
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   231
  "set (unions xss) = \<Union> set (map set xss)"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   232
unfolding unions_def proof (induct xss)
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   233
  case Nil show ?case by simp
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   234
next
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   235
  case (Cons xs xss) thus ?case by (induct xs) (simp_all add: iso_insert)
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   236
qed
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   237
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   238
lemma iso_intersects:
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   239
  "set (intersects (xs#xss)) = \<Inter> set (map set (xs#xss))"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   240
  by (induct xss) (simp_all add: Int_def iso_member, auto)
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   241
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   242
lemma iso_UNION:
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   243
  "set (map_union xs f) = UNION (set xs) (set o f)"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   244
  unfolding map_union_def iso_unions by simp
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   245
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   246
lemma iso_INTER:
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   247
  "set (map_inter (x#xs) f) = INTER (set (x#xs)) (set o f)"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   248
  unfolding map_inter_def iso_intersects by (induct xs) (simp_all add: iso_member, auto)
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   249
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   250
definition
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21385
diff changeset
   251
  Blall :: "'a list \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   252
  "Blall = flip list_all"
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21385
diff changeset
   253
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21385
diff changeset
   254
  Blex :: "'a list \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   255
  "Blex = flip list_ex"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   256
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   257
lemma iso_Ball:
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   258
  "Blall xs f = Ball (set xs) f"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   259
  unfolding Blall_def flip_def by (induct xs) simp_all
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   260
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   261
lemma iso_Bex:
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   262
  "Blex xs f = Bex (set xs) f"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   263
  unfolding Blex_def flip_def by (induct xs) simp_all
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   264
21385
cf398bb8a8be added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents: 21323
diff changeset
   265
lemma iso_filter:
cf398bb8a8be added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents: 21323
diff changeset
   266
  "set (filter P xs) = filter_set P (set xs)"
cf398bb8a8be added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents: 21323
diff changeset
   267
  unfolding filter_set_def by (induct xs) auto
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   268
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   269
section {* code generator setup *}
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   270
21008
330a8a6dd53c explicit nonfix for union and inter
haftmann
parents: 20934
diff changeset
   271
ML {*
330a8a6dd53c explicit nonfix for union and inter
haftmann
parents: 20934
diff changeset
   272
nonfix inter;
330a8a6dd53c explicit nonfix for union and inter
haftmann
parents: 20934
diff changeset
   273
nonfix union;
21875
5df10a17644e explicit nonfix declaration for ML "subset"
haftmann
parents: 21572
diff changeset
   274
nonfix subset;
21008
330a8a6dd53c explicit nonfix for union and inter
haftmann
parents: 20934
diff changeset
   275
*}
330a8a6dd53c explicit nonfix for union and inter
haftmann
parents: 20934
diff changeset
   276
21191
c00161fbf990 code generator module naming improved
haftmann
parents: 21153
diff changeset
   277
code_modulename SML
c00161fbf990 code generator module naming improved
haftmann
parents: 21153
diff changeset
   278
  ExecutableSet List
21385
cf398bb8a8be added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents: 21323
diff changeset
   279
  Set List
cf398bb8a8be added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents: 21323
diff changeset
   280
cf398bb8a8be added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents: 21323
diff changeset
   281
code_modulename Haskell
cf398bb8a8be added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents: 21323
diff changeset
   282
  ExecutableSet List
cf398bb8a8be added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents: 21323
diff changeset
   283
  Set List
20934
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   284
21063
3c5074f028c8 slight cleanup
haftmann
parents: 21046
diff changeset
   285
definition [code inline]:
20934
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   286
  "empty_list = []"
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   287
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   288
lemma [code func]:
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   289
  "insert (x \<Colon> 'a\<Colon>eq) = insert x" ..
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   290
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   291
lemma [code func]:
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   292
  "(xs \<Colon> 'a\<Colon>eq set) \<union> ys = xs \<union> ys" ..
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   293
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   294
lemma [code func]:
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   295
  "(xs \<Colon> 'a\<Colon>eq set) \<inter> ys = xs \<inter> ys" ..
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   296
21385
cf398bb8a8be added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents: 21323
diff changeset
   297
lemma [code func]:
cf398bb8a8be added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents: 21323
diff changeset
   298
  "minus_set xs = minus_set (xs \<Colon> 'a\<Colon>eq set)" ..
20934
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   299
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   300
lemma [code func]:
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   301
  "image (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq) = image f" ..
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   302
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   303
lemma [code func]:
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   304
  "UNION xs (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq set) = UNION xs f" ..
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   305
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   306
lemma [code func]:
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   307
  "INTER xs (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq set) = INTER xs f" ..
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   308
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   309
lemma [code func]:
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   310
  "Ball (xs \<Colon> 'a\<Colon>type set) = Ball xs" ..
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   311
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   312
lemma [code func]:
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   313
  "Bex (xs \<Colon> 'a\<Colon>type set) = Bex xs" ..
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   314
21385
cf398bb8a8be added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents: 21323
diff changeset
   315
lemma [code func]:
cf398bb8a8be added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents: 21323
diff changeset
   316
  "filter_set P (xs \<Colon> 'a\<Colon>type set) = filter_set P xs" ..
cf398bb8a8be added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents: 21323
diff changeset
   317
20934
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   318
code_abstype "'a set" "'a list" where
21115
f4e79a09c305 dropped junk
haftmann
parents: 21063
diff changeset
   319
  "{}" \<equiv> empty_list
20934
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   320
  insert \<equiv> insertl
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   321
  "op \<union>" \<equiv> unionl
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   322
  "op \<inter>" \<equiv> intersect
21385
cf398bb8a8be added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents: 21323
diff changeset
   323
  minus_set \<equiv> subtract
20934
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   324
  image \<equiv> map_distinct
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   325
  Union \<equiv> unions
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   326
  Inter \<equiv> intersects
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   327
  UNION \<equiv> map_union
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   328
  INTER \<equiv> map_inter
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   329
  Ball \<equiv> Blall
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   330
  Bex \<equiv> Blex
21385
cf398bb8a8be added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents: 21323
diff changeset
   331
  filter_set \<equiv> filter
20934
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   332
21385
cf398bb8a8be added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents: 21323
diff changeset
   333
code_gen "{}" insert "op \<union>" "op \<inter>" minus_set
cf398bb8a8be added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents: 21323
diff changeset
   334
  image Union Inter UNION INTER Ball Bex filter_set (SML -)
20934
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   335
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   336
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   337
subsection {* type serializations *}
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   338
17632
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
   339
types_code
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
   340
  set ("_ list")
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
   341
attach (term_of) {*
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
   342
fun term_of_set f T [] = Const ("{}", Type ("set", [T]))
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
   343
  | term_of_set f T (x :: xs) = Const ("insert",
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
   344
      T --> Type ("set", [T]) --> Type ("set", [T])) $ f x $ term_of_set f T xs;
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
   345
*}
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
   346
attach (test) {*
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
   347
fun gen_set' aG i j = frequency
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
   348
  [(i, fn () => aG j :: gen_set' aG (i-1) j), (1, fn () => [])] ()
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
   349
and gen_set aG i = gen_set' aG i i;
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
   350
*}
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
   351
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   352
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   353
subsection {* const serializations *}
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 17632
diff changeset
   354
17632
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
   355
consts_code
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
   356
  "{}"      ("[]")
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   357
  "insert"  ("{*insertl*}")
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   358
  "op Un"   ("{*unionl*}")
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   359
  "op Int"  ("{*intersect*}")
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   360
  "HOL.minus" :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   361
            ("{*flip subtract*}")
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   362
  "image"   ("{*map_distinct*}")
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   363
  "Union"   ("{*unions*}")
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   364
  "Inter"   ("{*intersects*}")
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   365
  "UNION"   ("{*map_union*}")
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   366
  "INTER"   ("{*map_inter*}")
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   367
  "Ball"    ("{*Blall*}")
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   368
  "Bex"     ("{*Blex*}")
21385
cf398bb8a8be added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents: 21323
diff changeset
   369
  "filter_set" ("{*filter*}")
17632
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
   370
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
   371
end