src/HOL/Library/Executable_Set.thy
author haftmann
Mon, 01 Dec 2008 14:56:08 +0100
changeset 28939 08004ce1b167
parent 28522 eacb54d9e78d
child 29107 e70b9c2bee14
permissions -rw-r--r--
added code equation for subset
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23854
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
     1
(*  Title:      HOL/Library/Executable_Set.thy
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
     2
    ID:         $Id$
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
     3
    Author:     Stefan Berghofer, TU Muenchen
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
     4
*)
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
     5
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
     6
header {* Implementation of finite sets by lists *}
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
     7
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
     8
theory Executable_Set
27487
c8a6ce181805 absolute imports of HOL/*.thy theories
haftmann
parents: 27368
diff changeset
     9
imports Plain "~~/src/HOL/List"
23854
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    10
begin
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    11
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    12
subsection {* Definitional rewrites *}
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    13
28522
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 27487
diff changeset
    14
definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 27487
diff changeset
    15
  "subset = op \<le>"
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 27487
diff changeset
    16
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 27487
diff changeset
    17
declare subset_def [symmetric, code unfold]
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 27487
diff changeset
    18
28939
08004ce1b167 added code equation for subset
haftmann
parents: 28522
diff changeset
    19
lemma [code]: "subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
28522
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 27487
diff changeset
    20
  unfolding subset_def subset_eq ..
23854
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    21
28522
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 27487
diff changeset
    22
definition is_empty :: "'a set \<Rightarrow> bool" where
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 27487
diff changeset
    23
  "is_empty A \<longleftrightarrow> A = {}"
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 27487
diff changeset
    24
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 27487
diff changeset
    25
definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 27487
diff changeset
    26
  [code del]: "eq_set = op ="
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 27487
diff changeset
    27
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 27487
diff changeset
    28
lemma [code]: "eq_set A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 27487
diff changeset
    29
  unfolding eq_set_def by auto
26816
e82229ee8f43 - Declared subset_eq as code lemma
berghofe
parents: 26312
diff changeset
    30
23854
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    31
lemma [code]:
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    32
  "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. x = a)"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    33
  unfolding bex_triv_one_point1 ..
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    34
28939
08004ce1b167 added code equation for subset
haftmann
parents: 28522
diff changeset
    35
definition filter_set :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
23854
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    36
  "filter_set P xs = {x\<in>xs. P x}"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    37
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    38
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    39
subsection {* Operations on lists *}
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    40
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    41
subsubsection {* Basic definitions *}
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    42
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    43
definition
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    44
  flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    45
  "flip f a b = f b a"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    46
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    47
definition
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    48
  member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool" where
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    49
  "member xs x \<longleftrightarrow> x \<in> set xs"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    50
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    51
definition
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    52
  insertl :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    53
  "insertl x xs = (if member xs x then xs else x#xs)"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    54
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    55
lemma [code target: List]: "member [] y \<longleftrightarrow> False"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    56
  and [code target: List]: "member (x#xs) y \<longleftrightarrow> y = x \<or> member xs y"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    57
  unfolding member_def by (induct xs) simp_all
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    58
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    59
fun
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    60
  drop_first :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    61
  "drop_first f [] = []"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    62
| "drop_first f (x#xs) = (if f x then xs else x # drop_first f xs)"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    63
declare drop_first.simps [code del]
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    64
declare drop_first.simps [code target: List]
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    65
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    66
declare remove1.simps [code del]
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    67
lemma [code target: List]:
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    68
  "remove1 x xs = (if member xs x then drop_first (\<lambda>y. y = x) xs else xs)"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    69
proof (cases "member xs x")
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    70
  case False thus ?thesis unfolding member_def by (induct xs) auto
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    71
next
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    72
  case True
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    73
  have "remove1 x xs = drop_first (\<lambda>y. y = x) xs" by (induct xs) simp_all
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    74
  with True show ?thesis by simp
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    75
qed
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    76
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    77
lemma member_nil [simp]:
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    78
  "member [] = (\<lambda>x. False)"
26816
e82229ee8f43 - Declared subset_eq as code lemma
berghofe
parents: 26312
diff changeset
    79
proof (rule ext)
23854
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    80
  fix x
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    81
  show "member [] x = False" unfolding member_def by simp
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    82
qed
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    83
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    84
lemma member_insertl [simp]:
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    85
  "x \<in> set (insertl x xs)"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    86
  unfolding insertl_def member_def mem_iff by simp
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    87
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    88
lemma insertl_member [simp]:
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    89
  fixes xs x
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    90
  assumes member: "member xs x"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    91
  shows "insertl x xs = xs"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    92
  using member unfolding insertl_def by simp
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    93
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    94
lemma insertl_not_member [simp]:
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    95
  fixes xs x
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    96
  assumes member: "\<not> (member xs x)"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    97
  shows "insertl x xs = x # xs"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    98
  using member unfolding insertl_def by simp
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    99
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   100
lemma foldr_remove1_empty [simp]:
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   101
  "foldr remove1 xs [] = []"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   102
  by (induct xs) simp_all
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   103
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   104
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   105
subsubsection {* Derived definitions *}
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   106
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   107
function unionl :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   108
where
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   109
  "unionl [] ys = ys"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   110
| "unionl xs ys = foldr insertl xs ys"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   111
by pat_completeness auto
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   112
termination by lexicographic_order
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   113
26312
e9a65675e5e8 avoid rebinding of existing facts;
wenzelm
parents: 25885
diff changeset
   114
lemmas unionl_eq = unionl.simps(2)
23854
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   115
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   116
function intersect :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   117
where
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   118
  "intersect [] ys = []"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   119
| "intersect xs [] = []"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   120
| "intersect xs ys = filter (member xs) ys"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   121
by pat_completeness auto
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   122
termination by lexicographic_order
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   123
26312
e9a65675e5e8 avoid rebinding of existing facts;
wenzelm
parents: 25885
diff changeset
   124
lemmas intersect_eq = intersect.simps(3)
23854
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   125
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   126
function subtract :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   127
where
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   128
  "subtract [] ys = ys"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   129
| "subtract xs [] = []"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   130
| "subtract xs ys = foldr remove1 xs ys"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   131
by pat_completeness auto
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   132
termination by lexicographic_order
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   133
26312
e9a65675e5e8 avoid rebinding of existing facts;
wenzelm
parents: 25885
diff changeset
   134
lemmas subtract_eq = subtract.simps(3)
23854
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   135
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   136
function map_distinct :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   137
where
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   138
  "map_distinct f [] = []"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   139
| "map_distinct f xs = foldr (insertl o f) xs []"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   140
by pat_completeness auto
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   141
termination by lexicographic_order
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   142
26312
e9a65675e5e8 avoid rebinding of existing facts;
wenzelm
parents: 25885
diff changeset
   143
lemmas map_distinct_eq = map_distinct.simps(2)
23854
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   144
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   145
function unions :: "'a list list \<Rightarrow> 'a list"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   146
where
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   147
  "unions [] = []"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   148
| "unions xs = foldr unionl xs []"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   149
by pat_completeness auto
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   150
termination by lexicographic_order
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   151
26312
e9a65675e5e8 avoid rebinding of existing facts;
wenzelm
parents: 25885
diff changeset
   152
lemmas unions_eq = unions.simps(2)
23854
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   153
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   154
consts intersects :: "'a list list \<Rightarrow> 'a list"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   155
primrec
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   156
  "intersects (x#xs) = foldr intersect xs x"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   157
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   158
definition
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   159
  map_union :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   160
  "map_union xs f = unions (map f xs)"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   161
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   162
definition
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   163
  map_inter :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   164
  "map_inter xs f = intersects (map f xs)"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   165
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   166
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   167
subsection {* Isomorphism proofs *}
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   168
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   169
lemma iso_member:
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   170
  "member xs x \<longleftrightarrow> x \<in> set xs"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   171
  unfolding member_def mem_iff ..
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   172
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   173
lemma iso_insert:
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   174
  "set (insertl x xs) = insert x (set xs)"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   175
  unfolding insertl_def iso_member by (simp add: Set.insert_absorb)
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   176
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   177
lemma iso_remove1:
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   178
  assumes distnct: "distinct xs"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   179
  shows "set (remove1 x xs) = set xs - {x}"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   180
  using distnct set_remove1_eq by auto
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   181
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   182
lemma iso_union:
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   183
  "set (unionl xs ys) = set xs \<union> set ys"
26312
e9a65675e5e8 avoid rebinding of existing facts;
wenzelm
parents: 25885
diff changeset
   184
  unfolding unionl_eq
23854
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   185
  by (induct xs arbitrary: ys) (simp_all add: iso_insert)
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   186
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   187
lemma iso_intersect:
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   188
  "set (intersect xs ys) = set xs \<inter> set ys"
26312
e9a65675e5e8 avoid rebinding of existing facts;
wenzelm
parents: 25885
diff changeset
   189
  unfolding intersect_eq Int_def by (simp add: Int_def iso_member) auto
23854
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   190
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   191
definition
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   192
  subtract' :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   193
  "subtract' = flip subtract"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   194
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   195
lemma iso_subtract:
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   196
  fixes ys
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   197
  assumes distnct: "distinct ys"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   198
  shows "set (subtract' ys xs) = set ys - set xs"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   199
    and "distinct (subtract' ys xs)"
26312
e9a65675e5e8 avoid rebinding of existing facts;
wenzelm
parents: 25885
diff changeset
   200
  unfolding subtract'_def flip_def subtract_eq
23854
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   201
  using distnct by (induct xs arbitrary: ys) auto
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   202
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   203
lemma iso_map_distinct:
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   204
  "set (map_distinct f xs) = image f (set xs)"
26312
e9a65675e5e8 avoid rebinding of existing facts;
wenzelm
parents: 25885
diff changeset
   205
  unfolding map_distinct_eq by (induct xs) (simp_all add: iso_insert)
23854
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   206
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   207
lemma iso_unions:
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   208
  "set (unions xss) = \<Union> set (map set xss)"
26312
e9a65675e5e8 avoid rebinding of existing facts;
wenzelm
parents: 25885
diff changeset
   209
  unfolding unions_eq
23854
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   210
proof (induct xss)
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   211
  case Nil show ?case by simp
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   212
next
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   213
  case (Cons xs xss) thus ?case by (induct xs) (simp_all add: iso_insert)
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   214
qed
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   215
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   216
lemma iso_intersects:
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   217
  "set (intersects (xs#xss)) = \<Inter> set (map set (xs#xss))"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   218
  by (induct xss) (simp_all add: Int_def iso_member, auto)
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   219
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   220
lemma iso_UNION:
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   221
  "set (map_union xs f) = UNION (set xs) (set o f)"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   222
  unfolding map_union_def iso_unions by simp
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   223
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   224
lemma iso_INTER:
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   225
  "set (map_inter (x#xs) f) = INTER (set (x#xs)) (set o f)"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   226
  unfolding map_inter_def iso_intersects by (induct xs) (simp_all add: iso_member, auto)
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   227
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   228
definition
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   229
  Blall :: "'a list \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   230
  "Blall = flip list_all"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   231
definition
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   232
  Blex :: "'a list \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   233
  "Blex = flip list_ex"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   234
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   235
lemma iso_Ball:
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   236
  "Blall xs f = Ball (set xs) f"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   237
  unfolding Blall_def flip_def by (induct xs) simp_all
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   238
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   239
lemma iso_Bex:
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   240
  "Blex xs f = Bex (set xs) f"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   241
  unfolding Blex_def flip_def by (induct xs) simp_all
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   242
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   243
lemma iso_filter:
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   244
  "set (filter P xs) = filter_set P (set xs)"
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   245
  unfolding filter_set_def by (induct xs) auto
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   246
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   247
subsection {* code generator setup *}
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   248
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   249
ML {*
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   250
nonfix inter;
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   251
nonfix union;
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   252
nonfix subset;
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   253
*}
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   254
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   255
subsubsection {* const serializations *}
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   256
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   257
consts_code
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   258
  "{}" ("{*[]*}")
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   259
  insert ("{*insertl*}")
28522
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 27487
diff changeset
   260
  is_empty ("{*null*}")
23854
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   261
  "op \<union>" ("{*unionl*}")
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   262
  "op \<inter>" ("{*intersect*}")
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   263
  "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{* flip subtract *}")
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   264
  image ("{*map_distinct*}")
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   265
  Union ("{*unions*}")
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   266
  Inter ("{*intersects*}")
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   267
  UNION ("{*map_union*}")
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   268
  INTER ("{*map_inter*}")
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   269
  Ball ("{*Blall*}")
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   270
  Bex ("{*Blex*}")
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   271
  filter_set ("{*filter*}")
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   272
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   273
end