src/HOL/Library/ExecutableSet.thy
author haftmann
Tue, 10 Oct 2006 09:17:20 +0200
changeset 20934 2b872c161747
parent 20840 5e92606245b6
child 21008 330a8a6dd53c
permissions -rw-r--r--
added code_abstype
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
20597
65fe827aa595 code generation 2 adjustments
haftmann
parents: 20523
diff changeset
    12
section {* Definitional equality rewrites *}
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
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    16
lemma [code target: Set]:
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    17
  "(A = B) = (A \<subseteq> B \<and> B \<subseteq> A)"
17632
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
    18
  by blast
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
    19
20597
65fe827aa595 code generation 2 adjustments
haftmann
parents: 20523
diff changeset
    20
lemma [code func]:
65fe827aa595 code generation 2 adjustments
haftmann
parents: 20523
diff changeset
    21
  "OperationalEquality.eq A B = (A \<subseteq> B \<and> B \<subseteq> A)"
65fe827aa595 code generation 2 adjustments
haftmann
parents: 20523
diff changeset
    22
  unfolding eq_def by blast
65fe827aa595 code generation 2 adjustments
haftmann
parents: 20523
diff changeset
    23
17632
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
    24
declare bex_triv_one_point1 [symmetric, standard, code]
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
    25
20597
65fe827aa595 code generation 2 adjustments
haftmann
parents: 20523
diff changeset
    26
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    27
section {* HOL definitions *}
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    28
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    29
subsection {* Basic definitions *}
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    30
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    31
definition
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    32
  flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    33
  "flip f a b = f b a"
20934
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
    34
  member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool"
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    35
  "member xs x = (x \<in> set xs)"
20934
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
    36
  insertl :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    37
  "insertl x xs = (if member xs x then xs else x#xs)"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    38
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    39
lemma
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    40
  [code target: List]: "member [] y = False"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    41
  and [code target: List]: "member (x#xs) y = (y = x \<or> member xs y)"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    42
unfolding member_def by (induct xs) simp_all
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    43
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    44
consts
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    45
  drop_first :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    46
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    47
primrec
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    48
  "drop_first f [] = []"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    49
  "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
    50
declare drop_first.simps [code del]
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    51
declare drop_first.simps [code target: List]
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    52
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    53
declare remove1.simps [code del]
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    54
lemma [code target: List]:
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    55
  "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
    56
proof (cases "member xs x")
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    57
  case False thus ?thesis unfolding member_def by (induct xs) auto
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    58
next
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    59
  case True
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    60
  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
    61
  with True show ?thesis by simp
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    62
qed
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    63
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    64
lemma member_nil [simp]:
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    65
  "member [] = (\<lambda>x. False)"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    66
proof
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    67
  fix x
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    68
  show "member [] x = False" unfolding member_def by simp
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    69
qed
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    70
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    71
lemma member_insertl [simp]:
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    72
  "x \<in> set (insertl x xs)"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    73
  unfolding insertl_def member_def mem_iff by simp
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    74
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    75
lemma insertl_member [simp]:
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    76
  fixes xs x
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    77
  assumes member: "member xs x"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    78
  shows "insertl x xs = xs"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    79
  using member unfolding insertl_def by simp
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    80
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    81
lemma insertl_not_member [simp]:
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    82
  fixes xs x
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    83
  assumes member: "\<not> (member xs x)"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    84
  shows "insertl x xs = x # xs"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    85
  using member unfolding insertl_def by simp
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    86
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    87
lemma foldr_remove1_empty [simp]:
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    88
  "foldr remove1 xs [] = []"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    89
  by (induct xs) simp_all
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    90
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    91
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    92
subsection {* Derived definitions *}
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    93
20934
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
    94
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
    95
where
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    96
  "unionl [] ys = ys"
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20503
diff changeset
    97
| "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
    98
by pat_completeness auto
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
    99
termination unionl by (auto_term "{}")
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   100
lemmas unionl_def = unionl.simps(2)
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20503
diff changeset
   101
declare unionl.simps[code]
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   102
20934
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   103
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
   104
where
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   105
  "intersect [] ys = []"
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20503
diff changeset
   106
| "intersect xs [] = []"
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20503
diff changeset
   107
| "intersect xs ys = filter (member xs) ys"
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20503
diff changeset
   108
  by pat_completeness auto
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   109
termination intersect by (auto_term "{}")
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   110
lemmas intersect_def = intersect.simps(3)
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20503
diff changeset
   111
declare intersect.simps[code]
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   112
20934
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   113
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
   114
where
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   115
  "subtract [] ys = ys"
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20503
diff changeset
   116
| "subtract xs [] = []"
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20503
diff changeset
   117
| "subtract xs ys = foldr remove1 xs ys"
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20503
diff changeset
   118
  by pat_completeness auto
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   119
termination subtract by (auto_term "{}")
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   120
lemmas subtract_def = subtract.simps(3)
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20503
diff changeset
   121
declare subtract.simps[code]
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   122
20934
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   123
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
   124
where
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   125
  "map_distinct f [] = []"
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20503
diff changeset
   126
| "map_distinct f xs = foldr (insertl o f) xs []"
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20503
diff changeset
   127
  by pat_completeness auto
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   128
termination map_distinct by (auto_term "{}")
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   129
lemmas map_distinct_def = map_distinct.simps(2)
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20503
diff changeset
   130
declare map_distinct.simps[code]
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   131
20934
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   132
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
   133
where
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   134
  "unions [] = []"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   135
  "unions xs = foldr unionl xs []"
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20503
diff changeset
   136
  by pat_completeness auto
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   137
termination unions by (auto_term "{}")
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   138
lemmas unions_def = unions.simps(2)
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20503
diff changeset
   139
declare unions.simps[code]
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   140
20934
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   141
consts intersects :: "'a list list \<Rightarrow> 'a list"
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   142
primrec
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   143
  "intersects (x#xs) = foldr intersect xs x"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   144
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   145
definition
20934
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   146
  map_union :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list"
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   147
  "map_union xs f = unions (map f xs)"
20934
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   148
  map_inter :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list"
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   149
  "map_inter xs f = intersects (map f xs)"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   150
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   151
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   152
section {* Isomorphism proofs *}
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   153
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   154
lemma iso_member:
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   155
  "member xs x = (x \<in> set xs)"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   156
  unfolding member_def mem_iff ..
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   157
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   158
lemma iso_insert:
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   159
  "set (insertl x xs) = insert x (set xs)"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   160
  unfolding insertl_def iso_member by (simp add: Set.insert_absorb)
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   161
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   162
lemma iso_remove1:
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   163
  assumes distnct: "distinct xs"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   164
  shows "set (remove1 x xs) = set xs - {x}"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   165
using distnct set_remove1_eq by auto
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   166
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   167
lemma iso_union:
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   168
  "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
   169
  unfolding unionl_def
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20503
diff changeset
   170
 by (induct xs arbitrary: ys) (simp_all add: iso_insert)
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   171
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   172
lemma iso_intersect:
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   173
  "set (intersect xs ys) = set xs \<inter> set ys"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   174
  unfolding intersect_def Int_def by (simp add: Int_def iso_member) auto
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   175
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   176
lemma iso_subtract:
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   177
  fixes ys
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   178
  assumes distnct: "distinct ys"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   179
  shows "set (subtract xs ys) = set ys - set xs"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   180
  and "distinct (subtract xs ys)"
20503
503ac4c5ef91 induct method: renamed 'fixing' to 'arbitrary';
wenzelm
parents: 20453
diff changeset
   181
unfolding subtract_def using distnct by (induct xs arbitrary: ys) (simp_all, auto)
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   182
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   183
corollary iso_subtract':
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   184
  fixes xs ys
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   185
  assumes distnct: "distinct xs"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   186
  shows "set ((flip subtract) xs ys) = set xs - set ys"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   187
proof -
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   188
  from distnct iso_subtract have "set (subtract ys xs) = set xs - set ys" by auto
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   189
  thus ?thesis unfolding flip_def by auto
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   190
qed
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   191
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   192
lemma iso_map_distinct:
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   193
  "set (map_distinct f xs) = image f (set xs)"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   194
  unfolding map_distinct_def by (induct xs) (simp_all add: iso_insert)
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   195
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   196
lemma iso_unions:
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   197
  "set (unions xss) = \<Union> set (map set xss)"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   198
unfolding unions_def proof (induct xss)
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   199
  case Nil show ?case by simp
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   200
next
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   201
  case (Cons xs xss) thus ?case by (induct xs) (simp_all add: iso_insert)
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   202
qed
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   203
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   204
lemma iso_intersects:
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   205
  "set (intersects (xs#xss)) = \<Inter> set (map set (xs#xss))"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   206
  by (induct xss) (simp_all add: Int_def iso_member, auto)
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   207
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   208
lemma iso_UNION:
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   209
  "set (map_union xs f) = UNION (set xs) (set o f)"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   210
  unfolding map_union_def iso_unions by simp
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   211
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   212
lemma iso_INTER:
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   213
  "set (map_inter (x#xs) f) = INTER (set (x#xs)) (set o f)"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   214
  unfolding map_inter_def iso_intersects by (induct xs) (simp_all add: iso_member, auto)
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   215
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   216
definition
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   217
  Blall :: "'a list \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   218
  "Blall = flip list_all"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   219
  Blex :: "'a list \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   220
  "Blex = flip list_ex"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   221
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   222
lemma iso_Ball:
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   223
  "Blall xs f = Ball (set xs) f"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   224
  unfolding Blall_def flip_def by (induct xs) simp_all
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   225
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   226
lemma iso_Bex:
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   227
  "Blex xs f = Bex (set xs) f"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   228
  unfolding Blex_def flip_def by (induct xs) simp_all
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   229
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   230
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   231
section {* code generator setup *}
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   232
20934
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   233
code_constname
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   234
  "ExecutableSet.member" "List.member"
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   235
  "ExecutableSet.insertl" "List.insertl"
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   236
  "ExecutableSet.drop_first" "List.drop_first"
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   237
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   238
definition
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   239
  "empty_list = []"
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   240
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   241
declare empty_list_def [code inline]
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   242
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   243
lemma [code func]:
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   244
  "insert (x \<Colon> 'a\<Colon>eq) = insert x" ..
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   245
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   246
lemma [code func]:
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   247
  "(xs \<Colon> 'a\<Colon>eq set) \<union> ys = xs \<union> ys" ..
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   248
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   249
lemma [code func]:
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   250
  "(xs \<Colon> 'a\<Colon>eq set) \<inter> ys = xs \<inter> ys" ..
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   251
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   252
definition
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   253
  "subtract' = flip subtract"
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   254
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   255
lemma [code func]:
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   256
  "image (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq) = image f" ..
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   257
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   258
lemma [code func]:
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   259
  "UNION xs (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq set) = UNION xs f" ..
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   260
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   261
lemma [code func]:
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   262
  "INTER xs (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq set) = INTER xs f" ..
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   263
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   264
lemma [code func]:
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   265
  "Ball (xs \<Colon> 'a\<Colon>type set) = Ball xs" ..
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   266
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   267
lemma [code func]:
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   268
  "Bex (xs \<Colon> 'a\<Colon>type set) = Bex xs" ..
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   269
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   270
code_abstype "'a set" "'a list" where
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   271
  "{}" \<equiv> "empty_list"
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   272
  insert \<equiv> insertl
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   273
  "op \<union>" \<equiv> unionl
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   274
  "op \<inter>" \<equiv> intersect
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   275
  "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" \<equiv> subtract'
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   276
  image \<equiv> map_distinct
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   277
  Union \<equiv> unions
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   278
  Inter \<equiv> intersects
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   279
  UNION \<equiv> map_union
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   280
  INTER \<equiv> map_inter
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   281
  Ball \<equiv> Blall
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   282
  Bex \<equiv> Blex
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   283
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   284
code_gen "{}" insert "op \<union>" "op \<inter>" "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   285
  image Union Inter UNION INTER Ball Bex (SML -)
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   286
2b872c161747 added code_abstype
haftmann
parents: 20840
diff changeset
   287
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   288
subsection {* type serializations *}
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   289
17632
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
   290
types_code
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
   291
  set ("_ list")
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
   292
attach (term_of) {*
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
   293
fun term_of_set f T [] = Const ("{}", Type ("set", [T]))
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
   294
  | term_of_set f T (x :: xs) = Const ("insert",
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
   295
      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
   296
*}
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
   297
attach (test) {*
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
   298
fun gen_set' aG i j = frequency
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
   299
  [(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
   300
and gen_set aG i = gen_set' aG i i;
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
   301
*}
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
   302
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   303
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   304
subsection {* const serializations *}
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 17632
diff changeset
   305
17632
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
   306
consts_code
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
   307
  "{}"      ("[]")
19791
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   308
  "insert"  ("{*insertl*}")
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   309
  "op Un"   ("{*unionl*}")
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   310
  "op Int"  ("{*intersect*}")
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   311
  "HOL.minus" :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   312
            ("{*flip subtract*}")
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   313
  "image"   ("{*map_distinct*}")
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   314
  "Union"   ("{*unions*}")
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   315
  "Inter"   ("{*intersects*}")
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   316
  "UNION"   ("{*map_union*}")
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   317
  "INTER"   ("{*map_inter*}")
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   318
  "Ball"    ("{*Blall*}")
ab326de16ad5 refined code generation
haftmann
parents: 19233
diff changeset
   319
  "Bex"     ("{*Blex*}")
17632
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
   320
13d6a689efe9 New theory for implementing finite sets by lists.
berghofe
parents:
diff changeset
   321
end