src/HOL/Quotient_Examples/FSet.thy
author haftmann
Tue Dec 27 09:45:10 2011 +0100 (2011-12-27)
changeset 45994 38a46e029784
parent 45990 b7b905b23b2a
child 46133 d9fe85d3d2cd
permissions -rw-r--r--
be explicit about Finite_Set.fold
kaliszyk@36524
     1
(*  Title:      HOL/Quotient_Examples/FSet.thy
kaliszyk@36465
     2
    Author:     Cezary Kaliszyk, TU Munich
kaliszyk@36465
     3
    Author:     Christian Urban, TU Munich
kaliszyk@36280
     4
wenzelm@41467
     5
Type of finite sets.
kaliszyk@36280
     6
*)
kaliszyk@36465
     7
kaliszyk@36280
     8
theory FSet
haftmann@45994
     9
imports "~~/src/HOL/Library/Multiset" "~~/src/HOL/Library/Quotient_List"
kaliszyk@36280
    10
begin
kaliszyk@36280
    11
urbanc@40030
    12
text {* 
urbanc@40030
    13
  The type of finite sets is created by a quotient construction
urbanc@40030
    14
  over lists. The definition of the equivalence:
urbanc@40030
    15
*}
kaliszyk@36280
    16
haftmann@40467
    17
definition
kaliszyk@36280
    18
  list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50)
kaliszyk@36280
    19
where
haftmann@40952
    20
  [simp]: "xs \<approx> ys \<longleftrightarrow> set xs = set ys"
kaliszyk@36280
    21
haftmann@40822
    22
lemma list_eq_reflp:
haftmann@40822
    23
  "reflp list_eq"
haftmann@40822
    24
  by (auto intro: reflpI)
haftmann@40822
    25
haftmann@40822
    26
lemma list_eq_symp:
haftmann@40822
    27
  "symp list_eq"
haftmann@40822
    28
  by (auto intro: sympI)
haftmann@40822
    29
haftmann@40822
    30
lemma list_eq_transp:
haftmann@40822
    31
  "transp list_eq"
haftmann@40822
    32
  by (auto intro: transpI)
haftmann@40822
    33
kaliszyk@36280
    34
lemma list_eq_equivp:
haftmann@40822
    35
  "equivp list_eq"
haftmann@40822
    36
  by (auto intro: equivpI list_eq_reflp list_eq_symp list_eq_transp)
kaliszyk@36280
    37
haftmann@40688
    38
text {* The @{text fset} type *}
urbanc@40030
    39
kaliszyk@36280
    40
quotient_type
kaliszyk@36280
    41
  'a fset = "'a list" / "list_eq"
kaliszyk@36280
    42
  by (rule list_eq_equivp)
kaliszyk@36280
    43
urbanc@40030
    44
text {* 
haftmann@40953
    45
  Definitions for sublist, cardinality, 
urbanc@40030
    46
  intersection, difference and respectful fold over 
urbanc@40030
    47
  lists.
kaliszyk@39994
    48
*}
kaliszyk@36280
    49
haftmann@40953
    50
declare List.member_def [simp]
kaliszyk@36280
    51
urbanc@40034
    52
definition
kaliszyk@36280
    53
  sub_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
urbanc@40030
    54
where 
urbanc@40034
    55
  [simp]: "sub_list xs ys \<longleftrightarrow> set xs \<subseteq> set ys"
kaliszyk@36280
    56
urbanc@40034
    57
definition
urbanc@40030
    58
  card_list :: "'a list \<Rightarrow> nat"
kaliszyk@36280
    59
where
urbanc@40034
    60
  [simp]: "card_list xs = card (set xs)"
kaliszyk@36675
    61
urbanc@40034
    62
definition
urbanc@40030
    63
  inter_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
kaliszyk@36675
    64
where
urbanc@40034
    65
  [simp]: "inter_list xs ys = [x \<leftarrow> xs. x \<in> set xs \<and> x \<in> set ys]"
urbanc@40030
    66
urbanc@40034
    67
definition
urbanc@40030
    68
  diff_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
urbanc@40030
    69
where
urbanc@40034
    70
  [simp]: "diff_list xs ys = [x \<leftarrow> xs. x \<notin> set ys]"
kaliszyk@36280
    71
kaliszyk@36280
    72
definition
haftmann@40954
    73
  rsp_fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> bool"
kaliszyk@36280
    74
where
haftmann@40954
    75
  "rsp_fold f \<longleftrightarrow> (\<forall>u v. f u \<circ> f v = f v \<circ> f u)"
kaliszyk@36280
    76
haftmann@40961
    77
lemma rsp_foldI:
haftmann@40961
    78
  "(\<And>u v. f u \<circ> f v = f v \<circ> f u) \<Longrightarrow> rsp_fold f"
haftmann@40961
    79
  by (simp add: rsp_fold_def)
haftmann@40961
    80
haftmann@40961
    81
lemma rsp_foldE:
haftmann@40961
    82
  assumes "rsp_fold f"
haftmann@40961
    83
  obtains "f u \<circ> f v = f v \<circ> f u"
haftmann@40961
    84
  using assms by (simp add: rsp_fold_def)
haftmann@40961
    85
haftmann@40962
    86
definition
haftmann@40962
    87
  fold_once :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b"
kaliszyk@36280
    88
where
haftmann@40962
    89
  "fold_once f xs = (if rsp_fold f then fold f (remdups xs) else id)"
kaliszyk@36280
    90
haftmann@40962
    91
lemma fold_once_default [simp]:
haftmann@40962
    92
  "\<not> rsp_fold f \<Longrightarrow> fold_once f xs = id"
haftmann@40962
    93
  by (simp add: fold_once_def)
haftmann@40961
    94
haftmann@40962
    95
lemma fold_once_fold_remdups:
haftmann@40962
    96
  "rsp_fold f \<Longrightarrow> fold_once f xs = fold f (remdups xs)"
haftmann@40962
    97
  by (simp add: fold_once_def)
urbanc@40030
    98
urbanc@40030
    99
urbanc@40030
   100
section {* Quotient composition lemmas *}
kaliszyk@36280
   101
urbanc@40030
   102
lemma list_all2_refl':
urbanc@40030
   103
  assumes q: "equivp R"
urbanc@40030
   104
  shows "(list_all2 R) r r"
urbanc@40030
   105
  by (rule list_all2_refl) (metis equivp_def q)
kaliszyk@36280
   106
kaliszyk@36280
   107
lemma compose_list_refl:
urbanc@40030
   108
  assumes q: "equivp R"
urbanc@40030
   109
  shows "(list_all2 R OOO op \<approx>) r r"
kaliszyk@36280
   110
proof
kaliszyk@36465
   111
  have *: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp])
urbanc@40030
   112
  show "list_all2 R r r" by (rule list_all2_refl'[OF q])
urbanc@40030
   113
  with * show "(op \<approx> OO list_all2 R) r r" ..
kaliszyk@36280
   114
qed
kaliszyk@36280
   115
urbanc@40030
   116
lemma map_list_eq_cong: "b \<approx> ba \<Longrightarrow> map f b \<approx> map f ba"
haftmann@40467
   117
  by (simp only: list_eq_def set_map)
kaliszyk@36280
   118
urbanc@40030
   119
lemma quotient_compose_list_g:
urbanc@40030
   120
  assumes q: "Quotient R Abs Rep"
urbanc@40030
   121
  and     e: "equivp R"
urbanc@40030
   122
  shows  "Quotient ((list_all2 R) OOO (op \<approx>))
urbanc@40030
   123
    (abs_fset \<circ> (map Abs)) ((map Rep) \<circ> rep_fset)"
urbanc@40030
   124
  unfolding Quotient_def comp_def
urbanc@40030
   125
proof (intro conjI allI)
urbanc@40030
   126
  fix a r s
urbanc@40030
   127
  show "abs_fset (map Abs (map Rep (rep_fset a))) = a"
urbanc@40030
   128
    by (simp add: abs_o_rep[OF q] Quotient_abs_rep[OF Quotient_fset] map_id)
urbanc@40030
   129
  have b: "list_all2 R (map Rep (rep_fset a)) (map Rep (rep_fset a))"
urbanc@40030
   130
    by (rule list_all2_refl'[OF e])
urbanc@40030
   131
  have c: "(op \<approx> OO list_all2 R) (map Rep (rep_fset a)) (map Rep (rep_fset a))"
urbanc@40030
   132
    by (rule, rule equivp_reflp[OF fset_equivp]) (rule b)
urbanc@40030
   133
  show "(list_all2 R OOO op \<approx>) (map Rep (rep_fset a)) (map Rep (rep_fset a))"
urbanc@40030
   134
    by (rule, rule list_all2_refl'[OF e]) (rule c)
urbanc@40030
   135
  show "(list_all2 R OOO op \<approx>) r s = ((list_all2 R OOO op \<approx>) r r \<and>
urbanc@40030
   136
        (list_all2 R OOO op \<approx>) s s \<and> abs_fset (map Abs r) = abs_fset (map Abs s))"
urbanc@40030
   137
  proof (intro iffI conjI)
urbanc@40030
   138
    show "(list_all2 R OOO op \<approx>) r r" by (rule compose_list_refl[OF e])
urbanc@40030
   139
    show "(list_all2 R OOO op \<approx>) s s" by (rule compose_list_refl[OF e])
urbanc@40030
   140
  next
urbanc@40030
   141
    assume a: "(list_all2 R OOO op \<approx>) r s"
urbanc@40030
   142
    then have b: "map Abs r \<approx> map Abs s"
urbanc@40030
   143
    proof (elim pred_compE)
urbanc@40030
   144
      fix b ba
urbanc@40030
   145
      assume c: "list_all2 R r b"
urbanc@40030
   146
      assume d: "b \<approx> ba"
urbanc@40030
   147
      assume e: "list_all2 R ba s"
urbanc@40030
   148
      have f: "map Abs r = map Abs b"
urbanc@40030
   149
        using Quotient_rel[OF list_quotient[OF q]] c by blast
urbanc@40030
   150
      have "map Abs ba = map Abs s"
urbanc@40030
   151
        using Quotient_rel[OF list_quotient[OF q]] e by blast
urbanc@40030
   152
      then have g: "map Abs s = map Abs ba" by simp
urbanc@40030
   153
      then show "map Abs r \<approx> map Abs s" using d f map_list_eq_cong by simp
urbanc@40030
   154
    qed
urbanc@40030
   155
    then show "abs_fset (map Abs r) = abs_fset (map Abs s)"
urbanc@40030
   156
      using Quotient_rel[OF Quotient_fset] by blast
urbanc@40030
   157
  next
urbanc@40030
   158
    assume a: "(list_all2 R OOO op \<approx>) r r \<and> (list_all2 R OOO op \<approx>) s s
urbanc@40030
   159
      \<and> abs_fset (map Abs r) = abs_fset (map Abs s)"
urbanc@40030
   160
    then have s: "(list_all2 R OOO op \<approx>) s s" by simp
urbanc@40030
   161
    have d: "map Abs r \<approx> map Abs s"
haftmann@40822
   162
      by (subst Quotient_rel [OF Quotient_fset, symmetric]) (simp add: a)
urbanc@40030
   163
    have b: "map Rep (map Abs r) \<approx> map Rep (map Abs s)"
urbanc@40030
   164
      by (rule map_list_eq_cong[OF d])
urbanc@40030
   165
    have y: "list_all2 R (map Rep (map Abs s)) s"
urbanc@40030
   166
      by (fact rep_abs_rsp_left[OF list_quotient[OF q], OF list_all2_refl'[OF e, of s]])
urbanc@40030
   167
    have c: "(op \<approx> OO list_all2 R) (map Rep (map Abs r)) s"
urbanc@40030
   168
      by (rule pred_compI) (rule b, rule y)
urbanc@40030
   169
    have z: "list_all2 R r (map Rep (map Abs r))"
urbanc@40030
   170
      by (fact rep_abs_rsp[OF list_quotient[OF q], OF list_all2_refl'[OF e, of r]])
urbanc@40030
   171
    then show "(list_all2 R OOO op \<approx>) r s"
urbanc@40030
   172
      using a c pred_compI by simp
urbanc@40030
   173
  qed
urbanc@40030
   174
qed
urbanc@40030
   175
kaliszyk@36280
   176
lemma quotient_compose_list[quot_thm]:
kaliszyk@37492
   177
  shows  "Quotient ((list_all2 op \<approx>) OOO (op \<approx>))
kaliszyk@36280
   178
    (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)"
urbanc@40030
   179
  by (rule quotient_compose_list_g, rule Quotient_fset, rule list_eq_equivp)
urbanc@40030
   180
kaliszyk@36280
   181
kaliszyk@39996
   182
urbanc@40030
   183
subsection {* Respectfulness lemmas for list operations *}
kaliszyk@39996
   184
urbanc@40030
   185
lemma list_equiv_rsp [quot_respect]:
urbanc@40030
   186
  shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
haftmann@40467
   187
  by (auto intro!: fun_relI)
kaliszyk@39996
   188
urbanc@40030
   189
lemma append_rsp [quot_respect]:
urbanc@40030
   190
  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) append append"
haftmann@40467
   191
  by (auto intro!: fun_relI)
kaliszyk@36280
   192
urbanc@40030
   193
lemma sub_list_rsp [quot_respect]:
kaliszyk@36280
   194
  shows "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list"
haftmann@40467
   195
  by (auto intro!: fun_relI)
kaliszyk@36280
   196
haftmann@40953
   197
lemma member_rsp [quot_respect]:
haftmann@40953
   198
  shows "(op \<approx> ===> op =) List.member List.member"
kaliszyk@44512
   199
proof
kaliszyk@44512
   200
  fix x y assume "x \<approx> y"
kaliszyk@44512
   201
  then show "List.member x = List.member y"
kaliszyk@44512
   202
    unfolding fun_eq_iff by simp
kaliszyk@44512
   203
qed
kaliszyk@36280
   204
urbanc@40030
   205
lemma nil_rsp [quot_respect]:
kaliszyk@39994
   206
  shows "(op \<approx>) Nil Nil"
kaliszyk@36280
   207
  by simp
kaliszyk@36280
   208
urbanc@40030
   209
lemma cons_rsp [quot_respect]:
kaliszyk@39994
   210
  shows "(op = ===> op \<approx> ===> op \<approx>) Cons Cons"
haftmann@40467
   211
  by (auto intro!: fun_relI)
kaliszyk@36280
   212
urbanc@40030
   213
lemma map_rsp [quot_respect]:
kaliszyk@36280
   214
  shows "(op = ===> op \<approx> ===> op \<approx>) map map"
haftmann@40467
   215
  by (auto intro!: fun_relI)
kaliszyk@36280
   216
urbanc@40030
   217
lemma set_rsp [quot_respect]:
kaliszyk@36280
   218
  "(op \<approx> ===> op =) set set"
haftmann@40467
   219
  by (auto intro!: fun_relI)
kaliszyk@36280
   220
urbanc@40030
   221
lemma inter_list_rsp [quot_respect]:
urbanc@40030
   222
  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) inter_list inter_list"
haftmann@40467
   223
  by (auto intro!: fun_relI)
kaliszyk@39996
   224
urbanc@40030
   225
lemma removeAll_rsp [quot_respect]:
kaliszyk@39996
   226
  shows "(op = ===> op \<approx> ===> op \<approx>) removeAll removeAll"
haftmann@40467
   227
  by (auto intro!: fun_relI)
kaliszyk@39996
   228
urbanc@40030
   229
lemma diff_list_rsp [quot_respect]:
urbanc@40030
   230
  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) diff_list diff_list"
haftmann@40467
   231
  by (auto intro!: fun_relI)
urbanc@40030
   232
urbanc@40030
   233
lemma card_list_rsp [quot_respect]:
urbanc@40030
   234
  shows "(op \<approx> ===> op =) card_list card_list"
haftmann@40467
   235
  by (auto intro!: fun_relI)
urbanc@40030
   236
urbanc@40030
   237
lemma filter_rsp [quot_respect]:
urbanc@40030
   238
  shows "(op = ===> op \<approx> ===> op \<approx>) filter filter"
haftmann@40467
   239
  by (auto intro!: fun_relI)
kaliszyk@39996
   240
haftmann@40962
   241
lemma remdups_removeAll: (*FIXME move*)
haftmann@40962
   242
  "remdups (removeAll x xs) = remove1 x (remdups xs)"
haftmann@40962
   243
  by (induct xs) auto
kaliszyk@36280
   244
haftmann@40962
   245
lemma member_commute_fold_once:
haftmann@40962
   246
  assumes "rsp_fold f"
haftmann@40962
   247
    and "x \<in> set xs"
haftmann@40962
   248
  shows "fold_once f xs = fold_once f (removeAll x xs) \<circ> f x"
haftmann@40962
   249
proof -
haftmann@40962
   250
  from assms have "More_List.fold f (remdups xs) = More_List.fold f (remove1 x (remdups xs)) \<circ> f x"
haftmann@40962
   251
    by (auto intro!: fold_remove1_split elim: rsp_foldE)
haftmann@40962
   252
  then show ?thesis using `rsp_fold f` by (simp add: fold_once_fold_remdups remdups_removeAll)
haftmann@40962
   253
qed
haftmann@40962
   254
haftmann@40962
   255
lemma fold_once_set_equiv:
haftmann@40961
   256
  assumes "xs \<approx> ys"
haftmann@40962
   257
  shows "fold_once f xs = fold_once f ys"
haftmann@40961
   258
proof (cases "rsp_fold f")
haftmann@40961
   259
  case False then show ?thesis by simp
haftmann@40961
   260
next
haftmann@40961
   261
  case True
haftmann@40961
   262
  then have "\<And>x y. x \<in> set (remdups xs) \<Longrightarrow> y \<in> set (remdups xs) \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"
haftmann@40961
   263
    by (rule rsp_foldE)
haftmann@40961
   264
  moreover from assms have "multiset_of (remdups xs) = multiset_of (remdups ys)"
haftmann@40961
   265
    by (simp add: set_eq_iff_multiset_of_remdups_eq)
haftmann@40961
   266
  ultimately have "fold f (remdups xs) = fold f (remdups ys)"
haftmann@40961
   267
    by (rule fold_multiset_equiv)
haftmann@40962
   268
  with True show ?thesis by (simp add: fold_once_fold_remdups)
haftmann@40961
   269
qed
kaliszyk@36280
   270
haftmann@40962
   271
lemma fold_once_rsp [quot_respect]:
haftmann@40962
   272
  shows "(op = ===> op \<approx> ===> op =) fold_once fold_once"
haftmann@40962
   273
  unfolding fun_rel_def by (auto intro: fold_once_set_equiv) 
kaliszyk@36280
   274
kaliszyk@36280
   275
lemma concat_rsp_pre:
kaliszyk@37492
   276
  assumes a: "list_all2 op \<approx> x x'"
kaliszyk@36280
   277
  and     b: "x' \<approx> y'"
kaliszyk@37492
   278
  and     c: "list_all2 op \<approx> y' y"
kaliszyk@36280
   279
  and     d: "\<exists>x\<in>set x. xa \<in> set x"
kaliszyk@36280
   280
  shows "\<exists>x\<in>set y. xa \<in> set x"
kaliszyk@36280
   281
proof -
kaliszyk@36280
   282
  obtain xb where e: "xb \<in> set x" and f: "xa \<in> set xb" using d by auto
kaliszyk@37492
   283
  have "\<exists>y. y \<in> set x' \<and> xb \<approx> y" by (rule list_all2_find_element[OF e a])
kaliszyk@36280
   284
  then obtain ya where h: "ya \<in> set x'" and i: "xb \<approx> ya" by auto
kaliszyk@36465
   285
  have "ya \<in> set y'" using b h by simp
kaliszyk@37492
   286
  then have "\<exists>yb. yb \<in> set y \<and> ya \<approx> yb" using c by (rule list_all2_find_element)
kaliszyk@36280
   287
  then show ?thesis using f i by auto
kaliszyk@36280
   288
qed
kaliszyk@36280
   289
urbanc@40030
   290
lemma concat_rsp [quot_respect]:
kaliszyk@37492
   291
  shows "(list_all2 op \<approx> OOO op \<approx> ===> op \<approx>) concat concat"
kaliszyk@36280
   292
proof (rule fun_relI, elim pred_compE)
kaliszyk@36280
   293
  fix a b ba bb
kaliszyk@37492
   294
  assume a: "list_all2 op \<approx> a ba"
haftmann@40822
   295
  with list_symp [OF list_eq_symp] have a': "list_all2 op \<approx> ba a" by (rule sympE)
kaliszyk@36280
   296
  assume b: "ba \<approx> bb"
haftmann@40822
   297
  with list_eq_symp have b': "bb \<approx> ba" by (rule sympE)
kaliszyk@37492
   298
  assume c: "list_all2 op \<approx> bb b"
haftmann@40822
   299
  with list_symp [OF list_eq_symp] have c': "list_all2 op \<approx> b bb" by (rule sympE)
kaliszyk@39996
   300
  have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" 
kaliszyk@39996
   301
  proof
kaliszyk@36280
   302
    fix x
kaliszyk@39996
   303
    show "(\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" 
kaliszyk@39996
   304
    proof
kaliszyk@36280
   305
      assume d: "\<exists>xa\<in>set a. x \<in> set xa"
kaliszyk@36280
   306
      show "\<exists>xa\<in>set b. x \<in> set xa" by (rule concat_rsp_pre[OF a b c d])
kaliszyk@36280
   307
    next
kaliszyk@36280
   308
      assume e: "\<exists>xa\<in>set b. x \<in> set xa"
kaliszyk@36280
   309
      show "\<exists>xa\<in>set a. x \<in> set xa" by (rule concat_rsp_pre[OF c' b' a' e])
kaliszyk@36280
   310
    qed
kaliszyk@36280
   311
  qed
kaliszyk@39996
   312
  then show "concat a \<approx> concat b" by auto
kaliszyk@36280
   313
qed
kaliszyk@36280
   314
bulwahn@36639
   315
urbanc@40030
   316
section {* Quotient definitions for fsets *}
urbanc@40030
   317
urbanc@40030
   318
urbanc@40030
   319
subsection {* Finite sets are a bounded, distributive lattice with minus *}
kaliszyk@36280
   320
urbanc@37634
   321
instantiation fset :: (type) "{bounded_lattice_bot, distrib_lattice, minus}"
kaliszyk@36280
   322
begin
kaliszyk@36280
   323
kaliszyk@36280
   324
quotient_definition
urbanc@40030
   325
  "bot :: 'a fset" 
urbanc@40030
   326
  is "Nil :: 'a list"
kaliszyk@36280
   327
kaliszyk@36280
   328
abbreviation
urbanc@40030
   329
  empty_fset  ("{||}")
kaliszyk@36280
   330
where
kaliszyk@36280
   331
  "{||} \<equiv> bot :: 'a fset"
kaliszyk@36280
   332
kaliszyk@36280
   333
quotient_definition
urbanc@40030
   334
  "less_eq_fset :: ('a fset \<Rightarrow> 'a fset \<Rightarrow> bool)"
urbanc@40030
   335
  is "sub_list :: ('a list \<Rightarrow> 'a list \<Rightarrow> bool)"
kaliszyk@36280
   336
kaliszyk@36280
   337
abbreviation
urbanc@40030
   338
  subset_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subseteq>|" 50)
kaliszyk@36280
   339
where
kaliszyk@36280
   340
  "xs |\<subseteq>| ys \<equiv> xs \<le> ys"
kaliszyk@36280
   341
kaliszyk@36280
   342
definition
kaliszyk@39995
   343
  less_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool"
kaliszyk@39995
   344
where  
kaliszyk@39995
   345
  "xs < ys \<equiv> xs \<le> ys \<and> xs \<noteq> (ys::'a fset)"
kaliszyk@36280
   346
kaliszyk@36280
   347
abbreviation
urbanc@40030
   348
  psubset_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subset>|" 50)
kaliszyk@36280
   349
where
kaliszyk@36280
   350
  "xs |\<subset>| ys \<equiv> xs < ys"
kaliszyk@36280
   351
kaliszyk@36280
   352
quotient_definition
kaliszyk@39995
   353
  "sup :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
urbanc@40030
   354
  is "append :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
kaliszyk@36280
   355
kaliszyk@36280
   356
abbreviation
urbanc@40030
   357
  union_fset (infixl "|\<union>|" 65)
kaliszyk@36280
   358
where
urbanc@40030
   359
  "xs |\<union>| ys \<equiv> sup xs (ys::'a fset)"
kaliszyk@36280
   360
kaliszyk@36280
   361
quotient_definition
kaliszyk@39995
   362
  "inf :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
urbanc@40030
   363
  is "inter_list :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
kaliszyk@36280
   364
kaliszyk@36280
   365
abbreviation
urbanc@40030
   366
  inter_fset (infixl "|\<inter>|" 65)
kaliszyk@36280
   367
where
urbanc@40030
   368
  "xs |\<inter>| ys \<equiv> inf xs (ys::'a fset)"
kaliszyk@36280
   369
kaliszyk@36675
   370
quotient_definition
urbanc@37634
   371
  "minus :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
urbanc@40030
   372
  is "diff_list :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
urbanc@40030
   373
kaliszyk@36280
   374
instance
kaliszyk@36280
   375
proof
kaliszyk@36280
   376
  fix x y z :: "'a fset"
urbanc@37634
   377
  show "x |\<subset>| y \<longleftrightarrow> x |\<subseteq>| y \<and> \<not> y |\<subseteq>| x"
haftmann@40467
   378
    by (unfold less_fset_def, descending) auto
urbanc@40030
   379
  show "x |\<subseteq>| x"  by (descending) (simp)
urbanc@40030
   380
  show "{||} |\<subseteq>| x" by (descending) (simp)
urbanc@40030
   381
  show "x |\<subseteq>| x |\<union>| y" by (descending) (simp)
urbanc@40030
   382
  show "y |\<subseteq>| x |\<union>| y" by (descending) (simp)
urbanc@40030
   383
  show "x |\<inter>| y |\<subseteq>| x" by (descending) (auto)
urbanc@40030
   384
  show "x |\<inter>| y |\<subseteq>| y" by (descending) (auto)
urbanc@37634
   385
  show "x |\<union>| (y |\<inter>| z) = x |\<union>| y |\<inter>| (x |\<union>| z)" 
urbanc@40030
   386
    by (descending) (auto)
kaliszyk@36280
   387
next
kaliszyk@36280
   388
  fix x y z :: "'a fset"
kaliszyk@36280
   389
  assume a: "x |\<subseteq>| y"
kaliszyk@36280
   390
  assume b: "y |\<subseteq>| z"
urbanc@40030
   391
  show "x |\<subseteq>| z" using a b by (descending) (simp)
kaliszyk@36280
   392
next
kaliszyk@36280
   393
  fix x y :: "'a fset"
kaliszyk@36280
   394
  assume a: "x |\<subseteq>| y"
kaliszyk@36280
   395
  assume b: "y |\<subseteq>| x"
urbanc@40030
   396
  show "x = y" using a b by (descending) (auto)
kaliszyk@36280
   397
next
kaliszyk@36280
   398
  fix x y z :: "'a fset"
kaliszyk@36280
   399
  assume a: "y |\<subseteq>| x"
kaliszyk@36280
   400
  assume b: "z |\<subseteq>| x"
urbanc@40030
   401
  show "y |\<union>| z |\<subseteq>| x" using a b by (descending) (simp)
kaliszyk@36280
   402
next
kaliszyk@36280
   403
  fix x y z :: "'a fset"
kaliszyk@36280
   404
  assume a: "x |\<subseteq>| y"
kaliszyk@36280
   405
  assume b: "x |\<subseteq>| z"
urbanc@40030
   406
  show "x |\<subseteq>| y |\<inter>| z" using a b by (descending) (auto)
kaliszyk@36280
   407
qed
kaliszyk@36280
   408
kaliszyk@36280
   409
end
kaliszyk@36280
   410
urbanc@40030
   411
urbanc@40030
   412
subsection {* Other constants for fsets *}
kaliszyk@36280
   413
kaliszyk@36280
   414
quotient_definition
urbanc@40030
   415
  "insert_fset :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
urbanc@40030
   416
  is "Cons"
kaliszyk@36280
   417
kaliszyk@36280
   418
syntax
wenzelm@45343
   419
  "_insert_fset"     :: "args => 'a fset"  ("{|(_)|}")
kaliszyk@36280
   420
kaliszyk@36280
   421
translations
urbanc@40030
   422
  "{|x, xs|}" == "CONST insert_fset x {|xs|}"
urbanc@40030
   423
  "{|x|}"     == "CONST insert_fset x {||}"
kaliszyk@36280
   424
kaliszyk@36280
   425
quotient_definition
haftmann@40953
   426
  fset_member
kaliszyk@36280
   427
where
haftmann@40953
   428
  "fset_member :: 'a fset \<Rightarrow> 'a \<Rightarrow> bool" is "List.member"
haftmann@40953
   429
haftmann@40953
   430
abbreviation
haftmann@40953
   431
  in_fset :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<in>|" 50)
haftmann@40953
   432
where
haftmann@40953
   433
  "x |\<in>| S \<equiv> fset_member S x"
kaliszyk@36280
   434
kaliszyk@36280
   435
abbreviation
urbanc@40030
   436
  notin_fset :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<notin>|" 50)
kaliszyk@36280
   437
where
kaliszyk@36280
   438
  "x |\<notin>| S \<equiv> \<not> (x |\<in>| S)"
kaliszyk@36280
   439
urbanc@40030
   440
urbanc@40030
   441
subsection {* Other constants on the Quotient Type *}
kaliszyk@36280
   442
kaliszyk@36280
   443
quotient_definition
urbanc@40030
   444
  "card_fset :: 'a fset \<Rightarrow> nat"
urbanc@40030
   445
  is card_list
kaliszyk@36280
   446
kaliszyk@36280
   447
quotient_definition
urbanc@40030
   448
  "map_fset :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
urbanc@40030
   449
  is map
kaliszyk@36280
   450
kaliszyk@36280
   451
quotient_definition
urbanc@40030
   452
  "remove_fset :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
kaliszyk@39996
   453
  is removeAll
kaliszyk@36280
   454
kaliszyk@36280
   455
quotient_definition
kaliszyk@39996
   456
  "fset :: 'a fset \<Rightarrow> 'a set"
kaliszyk@36280
   457
  is "set"
kaliszyk@36280
   458
kaliszyk@36280
   459
quotient_definition
haftmann@40961
   460
  "fold_fset :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b \<Rightarrow> 'b"
haftmann@40962
   461
  is fold_once
kaliszyk@36280
   462
kaliszyk@36280
   463
quotient_definition
urbanc@40030
   464
  "concat_fset :: ('a fset) fset \<Rightarrow> 'a fset"
urbanc@40030
   465
  is concat
kaliszyk@36280
   466
bulwahn@36639
   467
quotient_definition
urbanc@40030
   468
  "filter_fset :: ('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
urbanc@40030
   469
  is filter
bulwahn@36639
   470
urbanc@40030
   471
urbanc@40030
   472
subsection {* Compositional respectfulness and preservation lemmas *}
kaliszyk@36280
   473
urbanc@40030
   474
lemma Nil_rsp2 [quot_respect]: 
urbanc@40030
   475
  shows "(list_all2 op \<approx> OOO op \<approx>) Nil Nil"
urbanc@40030
   476
  by (rule compose_list_refl, rule list_eq_equivp)
kaliszyk@36280
   477
urbanc@40030
   478
lemma Cons_rsp2 [quot_respect]:
kaliszyk@39994
   479
  shows "(op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) Cons Cons"
haftmann@40467
   480
  apply (auto intro!: fun_relI)
kaliszyk@36280
   481
  apply (rule_tac b="x # b" in pred_compI)
kaliszyk@36280
   482
  apply auto
kaliszyk@36280
   483
  apply (rule_tac b="x # ba" in pred_compI)
kaliszyk@36280
   484
  apply auto
kaliszyk@36280
   485
  done
kaliszyk@36280
   486
urbanc@40030
   487
lemma map_prs [quot_preserve]: 
urbanc@40030
   488
  shows "(abs_fset \<circ> map f) [] = abs_fset []"
urbanc@40030
   489
  by simp
urbanc@40030
   490
urbanc@40030
   491
lemma insert_fset_rsp [quot_preserve]:
urbanc@40030
   492
  "(rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) Cons = insert_fset"
nipkow@39302
   493
  by (simp add: fun_eq_iff Quotient_abs_rep[OF Quotient_fset]
urbanc@40030
   494
      abs_o_rep[OF Quotient_fset] map_id insert_fset_def)
kaliszyk@36280
   495
urbanc@40030
   496
lemma union_fset_rsp [quot_preserve]:
urbanc@40030
   497
  "((map rep_fset \<circ> rep_fset) ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) 
urbanc@40030
   498
  append = union_fset"
nipkow@39302
   499
  by (simp add: fun_eq_iff Quotient_abs_rep[OF Quotient_fset]
kaliszyk@36280
   500
      abs_o_rep[OF Quotient_fset] map_id sup_fset_def)
kaliszyk@36280
   501
kaliszyk@37492
   502
lemma list_all2_app_l:
kaliszyk@36280
   503
  assumes a: "reflp R"
kaliszyk@37492
   504
  and b: "list_all2 R l r"
kaliszyk@37492
   505
  shows "list_all2 R (z @ l) (z @ r)"
haftmann@40822
   506
  using a b by (induct z) (auto elim: reflpE)
kaliszyk@36280
   507
kaliszyk@36280
   508
lemma append_rsp2_pre0:
kaliszyk@37492
   509
  assumes a:"list_all2 op \<approx> x x'"
kaliszyk@37492
   510
  shows "list_all2 op \<approx> (x @ z) (x' @ z)"
kaliszyk@36280
   511
  using a apply (induct x x' rule: list_induct2')
urbanc@40030
   512
  by simp_all (rule list_all2_refl'[OF list_eq_equivp])
kaliszyk@36280
   513
kaliszyk@36280
   514
lemma append_rsp2_pre1:
kaliszyk@37492
   515
  assumes a:"list_all2 op \<approx> x x'"
kaliszyk@37492
   516
  shows "list_all2 op \<approx> (z @ x) (z @ x')"
kaliszyk@36280
   517
  using a apply (induct x x' arbitrary: z rule: list_induct2')
urbanc@40030
   518
  apply (rule list_all2_refl'[OF list_eq_equivp])
haftmann@40467
   519
  apply (simp_all del: list_eq_def)
kaliszyk@37492
   520
  apply (rule list_all2_app_l)
haftmann@40822
   521
  apply (simp_all add: reflpI)
kaliszyk@36280
   522
  done
kaliszyk@36280
   523
kaliszyk@36280
   524
lemma append_rsp2_pre:
haftmann@40822
   525
  assumes "list_all2 op \<approx> x x'"
haftmann@40822
   526
    and "list_all2 op \<approx> z z'"
kaliszyk@37492
   527
  shows "list_all2 op \<approx> (x @ z) (x' @ z')"
haftmann@40822
   528
  using assms by (rule list_all2_appendI)
kaliszyk@36280
   529
urbanc@40030
   530
lemma append_rsp2 [quot_respect]:
urbanc@40030
   531
  "(list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) append append"
kaliszyk@36280
   532
proof (intro fun_relI, elim pred_compE)
kaliszyk@36280
   533
  fix x y z w x' z' y' w' :: "'a list list"
kaliszyk@37492
   534
  assume a:"list_all2 op \<approx> x x'"
kaliszyk@36280
   535
  and b:    "x' \<approx> y'"
kaliszyk@37492
   536
  and c:    "list_all2 op \<approx> y' y"
kaliszyk@37492
   537
  assume aa: "list_all2 op \<approx> z z'"
kaliszyk@36280
   538
  and bb:   "z' \<approx> w'"
kaliszyk@37492
   539
  and cc:   "list_all2 op \<approx> w' w"
kaliszyk@37492
   540
  have a': "list_all2 op \<approx> (x @ z) (x' @ z')" using a aa append_rsp2_pre by auto
kaliszyk@36280
   541
  have b': "x' @ z' \<approx> y' @ w'" using b bb by simp
kaliszyk@37492
   542
  have c': "list_all2 op \<approx> (y' @ w') (y @ w)" using c cc append_rsp2_pre by auto
kaliszyk@37492
   543
  have d': "(op \<approx> OO list_all2 op \<approx>) (x' @ z') (y @ w)"
kaliszyk@36280
   544
    by (rule pred_compI) (rule b', rule c')
kaliszyk@37492
   545
  show "(list_all2 op \<approx> OOO op \<approx>) (x @ z) (y @ w)"
kaliszyk@36280
   546
    by (rule pred_compI) (rule a', rule d')
kaliszyk@36280
   547
qed
kaliszyk@36280
   548
urbanc@40030
   549
urbanc@40030
   550
urbanc@40030
   551
section {* Lifted theorems *}
urbanc@40030
   552
urbanc@40030
   553
subsection {* fset *}
urbanc@40030
   554
urbanc@40030
   555
lemma fset_simps [simp]:
urbanc@40030
   556
  shows "fset {||} = {}"
urbanc@40030
   557
  and   "fset (insert_fset x S) = insert x (fset S)"
urbanc@40030
   558
  by (descending, simp)+
urbanc@40030
   559
urbanc@40030
   560
lemma finite_fset [simp]: 
urbanc@40030
   561
  shows "finite (fset S)"
urbanc@40030
   562
  by (descending) (simp)
urbanc@40030
   563
urbanc@40030
   564
lemma fset_cong:
urbanc@40030
   565
  shows "fset S = fset T \<longleftrightarrow> S = T"
urbanc@40030
   566
  by (descending) (simp)
urbanc@40030
   567
kaliszyk@44204
   568
lemma filter_fset [simp]:
kaliszyk@44204
   569
  shows "fset (filter_fset P xs) = Collect P \<inter> fset xs"
kaliszyk@44204
   570
  by (descending) (auto)
urbanc@40030
   571
urbanc@40030
   572
lemma remove_fset [simp]: 
urbanc@40030
   573
  shows "fset (remove_fset x xs) = fset xs - {x}"
urbanc@40030
   574
  by (descending) (simp)
urbanc@40030
   575
urbanc@40030
   576
lemma inter_fset [simp]: 
urbanc@40030
   577
  shows "fset (xs |\<inter>| ys) = fset xs \<inter> fset ys"
urbanc@40030
   578
  by (descending) (auto)
urbanc@40030
   579
urbanc@40030
   580
lemma union_fset [simp]: 
urbanc@40030
   581
  shows "fset (xs |\<union>| ys) = fset xs \<union> fset ys"
urbanc@40030
   582
  by (lifting set_append)
urbanc@40030
   583
urbanc@40030
   584
lemma minus_fset [simp]: 
urbanc@40030
   585
  shows "fset (xs - ys) = fset xs - fset ys"
urbanc@40030
   586
  by (descending) (auto)
urbanc@40030
   587
urbanc@40030
   588
urbanc@40030
   589
subsection {* in_fset *}
urbanc@40030
   590
urbanc@40030
   591
lemma in_fset: 
urbanc@40030
   592
  shows "x |\<in>| S \<longleftrightarrow> x \<in> fset S"
haftmann@40953
   593
  by descending simp
urbanc@40030
   594
urbanc@40030
   595
lemma notin_fset: 
urbanc@40030
   596
  shows "x |\<notin>| S \<longleftrightarrow> x \<notin> fset S"
urbanc@40030
   597
  by (simp add: in_fset)
urbanc@40030
   598
urbanc@40030
   599
lemma notin_empty_fset: 
urbanc@40030
   600
  shows "x |\<notin>| {||}"
urbanc@40030
   601
  by (simp add: in_fset)
kaliszyk@36280
   602
urbanc@40030
   603
lemma fset_eq_iff:
urbanc@40030
   604
  shows "S = T \<longleftrightarrow> (\<forall>x. (x |\<in>| S) = (x |\<in>| T))"
haftmann@40953
   605
  by descending auto
urbanc@40030
   606
urbanc@40030
   607
lemma none_in_empty_fset:
urbanc@40030
   608
  shows "(\<forall>x. x |\<notin>| S) \<longleftrightarrow> S = {||}"
haftmann@40953
   609
  by descending simp
urbanc@40030
   610
urbanc@40030
   611
urbanc@40030
   612
subsection {* insert_fset *}
urbanc@40030
   613
urbanc@40030
   614
lemma in_insert_fset_iff [simp]:
urbanc@40030
   615
  shows "x |\<in>| insert_fset y S \<longleftrightarrow> x = y \<or> x |\<in>| S"
haftmann@40953
   616
  by descending simp
urbanc@40030
   617
urbanc@40030
   618
lemma
urbanc@40030
   619
  shows insert_fsetI1: "x |\<in>| insert_fset x S"
urbanc@40030
   620
  and   insert_fsetI2: "x |\<in>| S \<Longrightarrow> x |\<in>| insert_fset y S"
urbanc@40030
   621
  by simp_all
urbanc@40030
   622
urbanc@40030
   623
lemma insert_absorb_fset [simp]:
urbanc@40030
   624
  shows "x |\<in>| S \<Longrightarrow> insert_fset x S = S"
urbanc@40030
   625
  by (descending) (auto)
kaliszyk@36280
   626
urbanc@40030
   627
lemma empty_not_insert_fset[simp]:
urbanc@40030
   628
  shows "{||} \<noteq> insert_fset x S"
urbanc@40030
   629
  and   "insert_fset x S \<noteq> {||}"
urbanc@40030
   630
  by (descending, simp)+
urbanc@40030
   631
urbanc@40030
   632
lemma insert_fset_left_comm:
urbanc@40030
   633
  shows "insert_fset x (insert_fset y S) = insert_fset y (insert_fset x S)"
urbanc@40030
   634
  by (descending) (auto)
urbanc@40030
   635
urbanc@40030
   636
lemma insert_fset_left_idem:
urbanc@40030
   637
  shows "insert_fset x (insert_fset x S) = insert_fset x S"
urbanc@40030
   638
  by (descending) (auto)
urbanc@40030
   639
urbanc@40030
   640
lemma singleton_fset_eq[simp]:
urbanc@40030
   641
  shows "{|x|} = {|y|} \<longleftrightarrow> x = y"
urbanc@40030
   642
  by (descending) (auto)
urbanc@40030
   643
urbanc@40030
   644
lemma in_fset_mdef:
urbanc@40030
   645
  shows "x |\<in>| F \<longleftrightarrow> x |\<notin>| (F - {|x|}) \<and> F = insert_fset x (F - {|x|})"
urbanc@40030
   646
  by (descending) (auto)
urbanc@40030
   647
urbanc@40030
   648
urbanc@40030
   649
subsection {* union_fset *}
urbanc@40030
   650
urbanc@40030
   651
lemmas [simp] =
wenzelm@45605
   652
  sup_bot_left[where 'a="'a fset"]
wenzelm@45605
   653
  sup_bot_right[where 'a="'a fset"]
urbanc@40030
   654
urbanc@40030
   655
lemma union_insert_fset [simp]:
urbanc@40030
   656
  shows "insert_fset x S |\<union>| T = insert_fset x (S |\<union>| T)"
urbanc@40030
   657
  by (lifting append.simps(2))
kaliszyk@36280
   658
urbanc@40030
   659
lemma singleton_union_fset_left:
urbanc@40030
   660
  shows "{|a|} |\<union>| S = insert_fset a S"
urbanc@40030
   661
  by simp
urbanc@40030
   662
urbanc@40030
   663
lemma singleton_union_fset_right:
urbanc@40030
   664
  shows "S |\<union>| {|a|} = insert_fset a S"
urbanc@40030
   665
  by (subst sup.commute) simp
urbanc@40030
   666
urbanc@40030
   667
lemma in_union_fset:
urbanc@40030
   668
  shows "x |\<in>| S |\<union>| T \<longleftrightarrow> x |\<in>| S \<or> x |\<in>| T"
urbanc@40030
   669
  by (descending) (simp)
urbanc@40030
   670
urbanc@40030
   671
urbanc@40030
   672
subsection {* minus_fset *}
urbanc@40030
   673
urbanc@40030
   674
lemma minus_in_fset: 
urbanc@40030
   675
  shows "x |\<in>| (xs - ys) \<longleftrightarrow> x |\<in>| xs \<and> x |\<notin>| ys"
urbanc@40030
   676
  by (descending) (simp)
urbanc@40030
   677
urbanc@40030
   678
lemma minus_insert_fset: 
urbanc@40030
   679
  shows "insert_fset x xs - ys = (if x |\<in>| ys then xs - ys else insert_fset x (xs - ys))"
urbanc@40030
   680
  by (descending) (auto)
urbanc@40030
   681
urbanc@40030
   682
lemma minus_insert_in_fset[simp]: 
urbanc@40030
   683
  shows "x |\<in>| ys \<Longrightarrow> insert_fset x xs - ys = xs - ys"
urbanc@40030
   684
  by (simp add: minus_insert_fset)
urbanc@40030
   685
urbanc@40030
   686
lemma minus_insert_notin_fset[simp]: 
urbanc@40030
   687
  shows "x |\<notin>| ys \<Longrightarrow> insert_fset x xs - ys = insert_fset x (xs - ys)"
urbanc@40030
   688
  by (simp add: minus_insert_fset)
urbanc@40030
   689
urbanc@40030
   690
lemma in_minus_fset: 
urbanc@40030
   691
  shows "x |\<in>| F - S \<Longrightarrow> x |\<notin>| S"
urbanc@40030
   692
  unfolding in_fset minus_fset
urbanc@40030
   693
  by blast
urbanc@40030
   694
urbanc@40030
   695
lemma notin_minus_fset: 
urbanc@40030
   696
  shows "x |\<in>| S \<Longrightarrow> x |\<notin>| F - S"
urbanc@40030
   697
  unfolding in_fset minus_fset
urbanc@40030
   698
  by blast
urbanc@40030
   699
urbanc@40030
   700
urbanc@40030
   701
subsection {* remove_fset *}
urbanc@40030
   702
urbanc@40030
   703
lemma in_remove_fset:
urbanc@40030
   704
  shows "x |\<in>| remove_fset y S \<longleftrightarrow> x |\<in>| S \<and> x \<noteq> y"
urbanc@40030
   705
  by (descending) (simp)
urbanc@40030
   706
urbanc@40030
   707
lemma notin_remove_fset:
urbanc@40030
   708
  shows "x |\<notin>| remove_fset x S"
urbanc@40030
   709
  by (descending) (simp)
kaliszyk@36280
   710
urbanc@40030
   711
lemma notin_remove_ident_fset:
urbanc@40030
   712
  shows "x |\<notin>| S \<Longrightarrow> remove_fset x S = S"
urbanc@40030
   713
  by (descending) (simp)
urbanc@40030
   714
urbanc@40030
   715
lemma remove_fset_cases:
urbanc@40030
   716
  shows "S = {||} \<or> (\<exists>x. x |\<in>| S \<and> S = insert_fset x (remove_fset x S))"
urbanc@40030
   717
  by (descending) (auto simp add: insert_absorb)
urbanc@40030
   718
  
urbanc@40030
   719
urbanc@40030
   720
subsection {* inter_fset *}
urbanc@40030
   721
urbanc@40030
   722
lemma inter_empty_fset_l:
urbanc@40030
   723
  shows "{||} |\<inter>| S = {||}"
urbanc@40030
   724
  by simp
urbanc@40030
   725
urbanc@40030
   726
lemma inter_empty_fset_r:
urbanc@40030
   727
  shows "S |\<inter>| {||} = {||}"
urbanc@40030
   728
  by simp
urbanc@40030
   729
urbanc@40030
   730
lemma inter_insert_fset:
urbanc@40030
   731
  shows "insert_fset x S |\<inter>| T = (if x |\<in>| T then insert_fset x (S |\<inter>| T) else S |\<inter>| T)"
urbanc@40030
   732
  by (descending) (auto)
urbanc@40030
   733
urbanc@40030
   734
lemma in_inter_fset:
urbanc@40030
   735
  shows "x |\<in>| (S |\<inter>| T) \<longleftrightarrow> x |\<in>| S \<and> x |\<in>| T"
urbanc@40030
   736
  by (descending) (simp)
urbanc@40030
   737
kaliszyk@36280
   738
urbanc@40030
   739
subsection {* subset_fset and psubset_fset *}
urbanc@40030
   740
urbanc@40030
   741
lemma subset_fset: 
urbanc@40030
   742
  shows "xs |\<subseteq>| ys \<longleftrightarrow> fset xs \<subseteq> fset ys"
urbanc@40030
   743
  by (descending) (simp)
urbanc@40030
   744
urbanc@40030
   745
lemma psubset_fset: 
urbanc@40030
   746
  shows "xs |\<subset>| ys \<longleftrightarrow> fset xs \<subset> fset ys"
urbanc@40030
   747
  unfolding less_fset_def 
urbanc@40030
   748
  by (descending) (auto)
urbanc@40030
   749
urbanc@40030
   750
lemma subset_insert_fset:
urbanc@40030
   751
  shows "(insert_fset x xs) |\<subseteq>| ys \<longleftrightarrow> x |\<in>| ys \<and> xs |\<subseteq>| ys"
urbanc@40030
   752
  by (descending) (simp)
urbanc@40030
   753
urbanc@40030
   754
lemma subset_in_fset: 
urbanc@40030
   755
  shows "xs |\<subseteq>| ys = (\<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys)"
urbanc@40030
   756
  by (descending) (auto)
urbanc@40030
   757
urbanc@40030
   758
lemma subset_empty_fset:
urbanc@40030
   759
  shows "xs |\<subseteq>| {||} \<longleftrightarrow> xs = {||}"
urbanc@40030
   760
  by (descending) (simp)
urbanc@40030
   761
urbanc@40030
   762
lemma not_psubset_empty_fset: 
urbanc@40030
   763
  shows "\<not> xs |\<subset>| {||}"
urbanc@40030
   764
  by (metis fset_simps(1) psubset_fset not_psubset_empty)
urbanc@40030
   765
urbanc@40030
   766
urbanc@40030
   767
subsection {* map_fset *}
kaliszyk@36280
   768
urbanc@40030
   769
lemma map_fset_simps [simp]:
urbanc@40030
   770
   shows "map_fset f {||} = {||}"
urbanc@40030
   771
  and   "map_fset f (insert_fset x S) = insert_fset (f x) (map_fset f S)"
urbanc@40030
   772
  by (descending, simp)+
urbanc@40030
   773
urbanc@40030
   774
lemma map_fset_image [simp]:
urbanc@40030
   775
  shows "fset (map_fset f S) = f ` (fset S)"
urbanc@40030
   776
  by (descending) (simp)
urbanc@40030
   777
urbanc@40030
   778
lemma inj_map_fset_cong:
urbanc@40030
   779
  shows "inj f \<Longrightarrow> map_fset f S = map_fset f T \<longleftrightarrow> S = T"
haftmann@40467
   780
  by (descending) (metis inj_vimage_image_eq list_eq_def set_map)
urbanc@40030
   781
urbanc@40030
   782
lemma map_union_fset: 
urbanc@40030
   783
  shows "map_fset f (S |\<union>| T) = map_fset f S |\<union>| map_fset f T"
urbanc@40030
   784
  by (descending) (simp)
urbanc@40030
   785
urbanc@40030
   786
urbanc@40030
   787
subsection {* card_fset *}
urbanc@40030
   788
urbanc@40030
   789
lemma card_fset: 
urbanc@40030
   790
  shows "card_fset xs = card (fset xs)"
urbanc@40030
   791
  by (descending) (simp)
urbanc@40030
   792
urbanc@40030
   793
lemma card_insert_fset_iff [simp]:
urbanc@40030
   794
  shows "card_fset (insert_fset x S) = (if x |\<in>| S then card_fset S else Suc (card_fset S))"
urbanc@40030
   795
  by (descending) (simp add: insert_absorb)
urbanc@40030
   796
urbanc@40030
   797
lemma card_fset_0[simp]:
urbanc@40030
   798
  shows "card_fset S = 0 \<longleftrightarrow> S = {||}"
urbanc@40030
   799
  by (descending) (simp)
urbanc@40030
   800
urbanc@40030
   801
lemma card_empty_fset[simp]:
urbanc@40030
   802
  shows "card_fset {||} = 0"
urbanc@40030
   803
  by (simp add: card_fset)
urbanc@40030
   804
urbanc@40030
   805
lemma card_fset_1:
urbanc@40030
   806
  shows "card_fset S = 1 \<longleftrightarrow> (\<exists>x. S = {|x|})"
urbanc@40030
   807
  by (descending) (auto simp add: card_Suc_eq)
urbanc@40030
   808
urbanc@40030
   809
lemma card_fset_gt_0:
urbanc@40030
   810
  shows "x \<in> fset S \<Longrightarrow> 0 < card_fset S"
urbanc@40030
   811
  by (descending) (auto simp add: card_gt_0_iff)
urbanc@40030
   812
  
urbanc@40030
   813
lemma card_notin_fset:
urbanc@40030
   814
  shows "(x |\<notin>| S) = (card_fset (insert_fset x S) = Suc (card_fset S))"
urbanc@40030
   815
  by simp
kaliszyk@36280
   816
urbanc@40030
   817
lemma card_fset_Suc: 
urbanc@40030
   818
  shows "card_fset S = Suc n \<Longrightarrow> \<exists>x T. x |\<notin>| T \<and> S = insert_fset x T \<and> card_fset T = n"
urbanc@40030
   819
  apply(descending)
urbanc@40030
   820
  apply(auto dest!: card_eq_SucD)
urbanc@40030
   821
  by (metis Diff_insert_absorb set_removeAll)
urbanc@40030
   822
urbanc@40030
   823
lemma card_remove_fset_iff [simp]:
urbanc@40030
   824
  shows "card_fset (remove_fset y S) = (if y |\<in>| S then card_fset S - 1 else card_fset S)"
urbanc@40030
   825
  by (descending) (simp)
urbanc@40030
   826
urbanc@40030
   827
lemma card_Suc_exists_in_fset: 
urbanc@40030
   828
  shows "card_fset S = Suc n \<Longrightarrow> \<exists>a. a |\<in>| S"
urbanc@40030
   829
  by (drule card_fset_Suc) (auto)
urbanc@40030
   830
urbanc@40030
   831
lemma in_card_fset_not_0: 
urbanc@40030
   832
  shows "a |\<in>| A \<Longrightarrow> card_fset A \<noteq> 0"
urbanc@40030
   833
  by (descending) (auto)
urbanc@40030
   834
urbanc@40030
   835
lemma card_fset_mono: 
urbanc@40030
   836
  shows "xs |\<subseteq>| ys \<Longrightarrow> card_fset xs \<le> card_fset ys"
urbanc@40030
   837
  unfolding card_fset psubset_fset
urbanc@40030
   838
  by (simp add: card_mono subset_fset)
urbanc@40030
   839
urbanc@40030
   840
lemma card_subset_fset_eq: 
urbanc@40030
   841
  shows "xs |\<subseteq>| ys \<Longrightarrow> card_fset ys \<le> card_fset xs \<Longrightarrow> xs = ys"
urbanc@40030
   842
  unfolding card_fset subset_fset
urbanc@40030
   843
  by (auto dest: card_seteq[OF finite_fset] simp add: fset_cong)
kaliszyk@36675
   844
urbanc@40030
   845
lemma psubset_card_fset_mono: 
urbanc@40030
   846
  shows "xs |\<subset>| ys \<Longrightarrow> card_fset xs < card_fset ys"
urbanc@40030
   847
  unfolding card_fset subset_fset
urbanc@40030
   848
  by (metis finite_fset psubset_fset psubset_card_mono)
urbanc@40030
   849
urbanc@40030
   850
lemma card_union_inter_fset: 
urbanc@40030
   851
  shows "card_fset xs + card_fset ys = card_fset (xs |\<union>| ys) + card_fset (xs |\<inter>| ys)"
urbanc@40030
   852
  unfolding card_fset union_fset inter_fset
urbanc@40030
   853
  by (rule card_Un_Int[OF finite_fset finite_fset])
urbanc@40030
   854
urbanc@40030
   855
lemma card_union_disjoint_fset: 
urbanc@40030
   856
  shows "xs |\<inter>| ys = {||} \<Longrightarrow> card_fset (xs |\<union>| ys) = card_fset xs + card_fset ys"
urbanc@40030
   857
  unfolding card_fset union_fset 
urbanc@40030
   858
  apply (rule card_Un_disjoint[OF finite_fset finite_fset])
urbanc@40030
   859
  by (metis inter_fset fset_simps(1))
urbanc@40030
   860
urbanc@40030
   861
lemma card_remove_fset_less1: 
urbanc@40030
   862
  shows "x |\<in>| xs \<Longrightarrow> card_fset (remove_fset x xs) < card_fset xs"
urbanc@40030
   863
  unfolding card_fset in_fset remove_fset 
urbanc@40030
   864
  by (rule card_Diff1_less[OF finite_fset])
urbanc@40030
   865
urbanc@40030
   866
lemma card_remove_fset_less2: 
urbanc@40030
   867
  shows "x |\<in>| xs \<Longrightarrow> y |\<in>| xs \<Longrightarrow> card_fset (remove_fset y (remove_fset x xs)) < card_fset xs"
urbanc@40030
   868
  unfolding card_fset remove_fset in_fset
urbanc@40030
   869
  by (rule card_Diff2_less[OF finite_fset])
urbanc@40030
   870
urbanc@40030
   871
lemma card_remove_fset_le1: 
urbanc@40030
   872
  shows "card_fset (remove_fset x xs) \<le> card_fset xs"
urbanc@40030
   873
  unfolding remove_fset card_fset
urbanc@40030
   874
  by (rule card_Diff1_le[OF finite_fset])
kaliszyk@36280
   875
urbanc@40030
   876
lemma card_psubset_fset: 
urbanc@40030
   877
  shows "ys |\<subseteq>| xs \<Longrightarrow> card_fset ys < card_fset xs \<Longrightarrow> ys |\<subset>| xs"
urbanc@40030
   878
  unfolding card_fset psubset_fset subset_fset
urbanc@40030
   879
  by (rule card_psubset[OF finite_fset])
urbanc@40030
   880
urbanc@40030
   881
lemma card_map_fset_le: 
urbanc@40030
   882
  shows "card_fset (map_fset f xs) \<le> card_fset xs"
urbanc@40030
   883
  unfolding card_fset map_fset_image
urbanc@40030
   884
  by (rule card_image_le[OF finite_fset])
urbanc@40030
   885
urbanc@40030
   886
lemma card_minus_insert_fset[simp]:
urbanc@40030
   887
  assumes "a |\<in>| A" and "a |\<notin>| B"
urbanc@40030
   888
  shows "card_fset (A - insert_fset a B) = card_fset (A - B) - 1"
urbanc@40030
   889
  using assms 
urbanc@40030
   890
  unfolding in_fset card_fset minus_fset
urbanc@40030
   891
  by (simp add: card_Diff_insert[OF finite_fset])
urbanc@40030
   892
urbanc@40030
   893
lemma card_minus_subset_fset:
urbanc@40030
   894
  assumes "B |\<subseteq>| A"
urbanc@40030
   895
  shows "card_fset (A - B) = card_fset A - card_fset B"
urbanc@40030
   896
  using assms 
urbanc@40030
   897
  unfolding subset_fset card_fset minus_fset
urbanc@40030
   898
  by (rule card_Diff_subset[OF finite_fset])
urbanc@40030
   899
urbanc@40030
   900
lemma card_minus_fset:
urbanc@40030
   901
  shows "card_fset (A - B) = card_fset A - card_fset (A |\<inter>| B)"
urbanc@40030
   902
  unfolding inter_fset card_fset minus_fset
urbanc@40030
   903
  by (rule card_Diff_subset_Int) (simp)
urbanc@40030
   904
urbanc@40030
   905
urbanc@40030
   906
subsection {* concat_fset *}
urbanc@40030
   907
urbanc@40030
   908
lemma concat_empty_fset [simp]:
urbanc@40030
   909
  shows "concat_fset {||} = {||}"
urbanc@40030
   910
  by (lifting concat.simps(1))
urbanc@40030
   911
urbanc@40030
   912
lemma concat_insert_fset [simp]:
urbanc@40030
   913
  shows "concat_fset (insert_fset x S) = x |\<union>| concat_fset S"
urbanc@40030
   914
  by (lifting concat.simps(2))
urbanc@40030
   915
urbanc@40030
   916
lemma concat_inter_fset [simp]:
urbanc@40030
   917
  shows "concat_fset (xs |\<union>| ys) = concat_fset xs |\<union>| concat_fset ys"
urbanc@40030
   918
  by (lifting concat_append)
urbanc@40030
   919
urbanc@40030
   920
urbanc@40030
   921
subsection {* filter_fset *}
urbanc@40030
   922
urbanc@40030
   923
lemma subset_filter_fset: 
haftmann@40961
   924
  "filter_fset P xs |\<subseteq>| filter_fset Q xs = (\<forall> x. x |\<in>| xs \<longrightarrow> P x \<longrightarrow> Q x)"
haftmann@40961
   925
  by descending auto
urbanc@40030
   926
urbanc@40030
   927
lemma eq_filter_fset: 
haftmann@40961
   928
  "(filter_fset P xs = filter_fset Q xs) = (\<forall>x. x |\<in>| xs \<longrightarrow> P x = Q x)"
haftmann@40961
   929
  by descending auto
kaliszyk@36280
   930
urbanc@40030
   931
lemma psubset_filter_fset:
haftmann@40961
   932
  "(\<And>x. x |\<in>| xs \<Longrightarrow> P x \<Longrightarrow> Q x) \<Longrightarrow> (x |\<in>| xs & \<not> P x & Q x) \<Longrightarrow> 
urbanc@40030
   933
    filter_fset P xs |\<subset>| filter_fset Q xs"
urbanc@40030
   934
  unfolding less_fset_def by (auto simp add: subset_filter_fset eq_filter_fset)
urbanc@40030
   935
urbanc@40030
   936
urbanc@40030
   937
subsection {* fold_fset *}
urbanc@40030
   938
urbanc@40030
   939
lemma fold_empty_fset: 
haftmann@40961
   940
  "fold_fset f {||} = id"
haftmann@40962
   941
  by descending (simp add: fold_once_def)
urbanc@40030
   942
haftmann@40961
   943
lemma fold_insert_fset: "fold_fset f (insert_fset a A) =
haftmann@40962
   944
  (if rsp_fold f then if a |\<in>| A then fold_fset f A else fold_fset f A \<circ> f a else id)"
haftmann@40962
   945
  by descending (simp add: fold_once_fold_remdups)
urbanc@40030
   946
urbanc@40030
   947
lemma in_commute_fold_fset:
haftmann@40962
   948
  "rsp_fold f \<Longrightarrow> h |\<in>| b \<Longrightarrow> fold_fset f b = fold_fset f (remove_fset h b) \<circ> f h"
haftmann@40962
   949
  by descending (simp add: member_commute_fold_once)
urbanc@40030
   950
urbanc@40030
   951
urbanc@40030
   952
subsection {* Choice in fsets *}
urbanc@40030
   953
urbanc@40030
   954
lemma fset_choice: 
urbanc@40030
   955
  assumes a: "\<forall>x. x |\<in>| A \<longrightarrow> (\<exists>y. P x y)"
urbanc@40030
   956
  shows "\<exists>f. \<forall>x. x |\<in>| A \<longrightarrow> P x (f x)"
urbanc@40030
   957
  using a
urbanc@40030
   958
  apply(descending)
urbanc@40030
   959
  using finite_set_choice
urbanc@40030
   960
  by (auto simp add: Ball_def)
urbanc@40030
   961
urbanc@40030
   962
urbanc@40030
   963
section {* Induction and Cases rules for fsets *}
urbanc@40030
   964
haftmann@41070
   965
lemma fset_exhaust [case_names empty insert, cases type: fset]:
urbanc@40030
   966
  assumes empty_fset_case: "S = {||} \<Longrightarrow> P" 
urbanc@40030
   967
  and     insert_fset_case: "\<And>x S'. S = insert_fset x S' \<Longrightarrow> P"
urbanc@40030
   968
  shows "P"
urbanc@40030
   969
  using assms by (lifting list.exhaust)
urbanc@40030
   970
haftmann@41070
   971
lemma fset_induct [case_names empty insert]:
urbanc@40030
   972
  assumes empty_fset_case: "P {||}"
urbanc@40030
   973
  and     insert_fset_case: "\<And>x S. P S \<Longrightarrow> P (insert_fset x S)"
urbanc@40030
   974
  shows "P S"
urbanc@40030
   975
  using assms 
urbanc@40030
   976
  by (descending) (blast intro: list.induct)
urbanc@40030
   977
haftmann@41070
   978
lemma fset_induct_stronger [case_names empty insert, induct type: fset]:
urbanc@40030
   979
  assumes empty_fset_case: "P {||}"
urbanc@40030
   980
  and     insert_fset_case: "\<And>x S. \<lbrakk>x |\<notin>| S; P S\<rbrakk> \<Longrightarrow> P (insert_fset x S)"
urbanc@40030
   981
  shows "P S"
urbanc@40030
   982
proof(induct S rule: fset_induct)
haftmann@41070
   983
  case empty
urbanc@40030
   984
  show "P {||}" using empty_fset_case by simp
urbanc@40030
   985
next
haftmann@41070
   986
  case (insert x S)
urbanc@40030
   987
  have "P S" by fact
urbanc@40030
   988
  then show "P (insert_fset x S)" using insert_fset_case 
urbanc@40030
   989
    by (cases "x |\<in>| S") (simp_all)
kaliszyk@36280
   990
qed
kaliszyk@36280
   991
urbanc@40030
   992
lemma fset_card_induct:
urbanc@40030
   993
  assumes empty_fset_case: "P {||}"
urbanc@40030
   994
  and     card_fset_Suc_case: "\<And>S T. Suc (card_fset S) = (card_fset T) \<Longrightarrow> P S \<Longrightarrow> P T"
urbanc@40030
   995
  shows "P S"
urbanc@40030
   996
proof (induct S)
haftmann@41070
   997
  case empty
urbanc@40030
   998
  show "P {||}" by (rule empty_fset_case)
urbanc@40030
   999
next
haftmann@41070
  1000
  case (insert x S)
urbanc@40030
  1001
  have h: "P S" by fact
urbanc@40030
  1002
  have "x |\<notin>| S" by fact
urbanc@40030
  1003
  then have "Suc (card_fset S) = card_fset (insert_fset x S)" 
urbanc@40030
  1004
    using card_fset_Suc by auto
urbanc@40030
  1005
  then show "P (insert_fset x S)" 
urbanc@40030
  1006
    using h card_fset_Suc_case by simp
urbanc@40030
  1007
qed
kaliszyk@36280
  1008
kaliszyk@36280
  1009
lemma fset_raw_strong_cases:
kaliszyk@36465
  1010
  obtains "xs = []"
haftmann@40953
  1011
    | ys x where "\<not> List.member ys x" and "xs \<approx> x # ys"
wenzelm@45129
  1012
proof (induct xs)
kaliszyk@36465
  1013
  case Nil
kaliszyk@36465
  1014
  then show thesis by simp
kaliszyk@36465
  1015
next
kaliszyk@36465
  1016
  case (Cons a xs)
haftmann@40953
  1017
  have a: "\<lbrakk>xs = [] \<Longrightarrow> thesis; \<And>x ys. \<lbrakk>\<not> List.member ys x; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis"
haftmann@40953
  1018
    by (rule Cons(1))
haftmann@40953
  1019
  have b: "\<And>x' ys'. \<lbrakk>\<not> List.member ys' x'; a # xs \<approx> x' # ys'\<rbrakk> \<Longrightarrow> thesis" by fact
urbanc@40030
  1020
  have c: "xs = [] \<Longrightarrow> thesis" using b 
urbanc@40030
  1021
    apply(simp)
urbanc@40030
  1022
    by (metis List.set.simps(1) emptyE empty_subsetI)
haftmann@40953
  1023
  have "\<And>x ys. \<lbrakk>\<not> List.member ys x; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis"
kaliszyk@36465
  1024
  proof -
kaliszyk@36465
  1025
    fix x :: 'a
kaliszyk@36465
  1026
    fix ys :: "'a list"
haftmann@40953
  1027
    assume d:"\<not> List.member ys x"
kaliszyk@36465
  1028
    assume e:"xs \<approx> x # ys"
kaliszyk@36465
  1029
    show thesis
kaliszyk@36465
  1030
    proof (cases "x = a")
kaliszyk@36465
  1031
      assume h: "x = a"
haftmann@40953
  1032
      then have f: "\<not> List.member ys a" using d by simp
kaliszyk@36465
  1033
      have g: "a # xs \<approx> a # ys" using e h by auto
kaliszyk@36465
  1034
      show thesis using b f g by simp
kaliszyk@36465
  1035
    next
kaliszyk@36465
  1036
      assume h: "x \<noteq> a"
haftmann@40953
  1037
      then have f: "\<not> List.member (a # ys) x" using d by auto
kaliszyk@36465
  1038
      have g: "a # xs \<approx> x # (a # ys)" using e h by auto
haftmann@40953
  1039
      show thesis using b f g by (simp del: List.member_def) 
kaliszyk@36465
  1040
    qed
kaliszyk@36465
  1041
  qed
kaliszyk@36465
  1042
  then show thesis using a c by blast
kaliszyk@36465
  1043
qed
kaliszyk@36280
  1044
urbanc@40030
  1045
urbanc@40030
  1046
lemma fset_strong_cases:
urbanc@40030
  1047
  obtains "xs = {||}"
haftmann@40953
  1048
    | ys x where "x |\<notin>| ys" and "xs = insert_fset x ys"
urbanc@40030
  1049
  by (lifting fset_raw_strong_cases)
kaliszyk@36280
  1050
kaliszyk@39996
  1051
urbanc@40030
  1052
lemma fset_induct2:
urbanc@40030
  1053
  "P {||} {||} \<Longrightarrow>
urbanc@40030
  1054
  (\<And>x xs. x |\<notin>| xs \<Longrightarrow> P (insert_fset x xs) {||}) \<Longrightarrow>
urbanc@40030
  1055
  (\<And>y ys. y |\<notin>| ys \<Longrightarrow> P {||} (insert_fset y ys)) \<Longrightarrow>
urbanc@40030
  1056
  (\<And>x xs y ys. \<lbrakk>P xs ys; x |\<notin>| xs; y |\<notin>| ys\<rbrakk> \<Longrightarrow> P (insert_fset x xs) (insert_fset y ys)) \<Longrightarrow>
urbanc@40030
  1057
  P xsa ysa"
urbanc@40030
  1058
  apply (induct xsa arbitrary: ysa)
urbanc@40030
  1059
  apply (induct_tac x rule: fset_induct_stronger)
urbanc@40030
  1060
  apply simp_all
urbanc@40030
  1061
  apply (induct_tac xa rule: fset_induct_stronger)
urbanc@40030
  1062
  apply simp_all
urbanc@40030
  1063
  done
kaliszyk@36280
  1064
haftmann@41070
  1065
text {* Extensionality *}
urbanc@40030
  1066
haftmann@41070
  1067
lemma fset_eqI:
haftmann@41070
  1068
  assumes "\<And>x. x \<in> fset A \<longleftrightarrow> x \<in> fset B"
haftmann@41070
  1069
  shows "A = B"
haftmann@41070
  1070
using assms proof (induct A arbitrary: B)
haftmann@41070
  1071
  case empty then show ?case
haftmann@41070
  1072
    by (auto simp add: in_fset none_in_empty_fset [symmetric] sym)
haftmann@41070
  1073
next
haftmann@41070
  1074
  case (insert x A)
haftmann@41070
  1075
  from insert.prems insert.hyps(1) have "\<And>z. z \<in> fset A \<longleftrightarrow> z \<in> fset (B - {|x|})"
haftmann@41070
  1076
    by (auto simp add: in_fset)
haftmann@41070
  1077
  then have "A = B - {|x|}" by (rule insert.hyps(2))
haftmann@41070
  1078
  moreover with insert.prems [symmetric, of x] have "x |\<in>| B" by (simp add: in_fset)
haftmann@41070
  1079
  ultimately show ?case by (metis in_fset_mdef)
haftmann@41070
  1080
qed
kaliszyk@36280
  1081
urbanc@40030
  1082
subsection {* alternate formulation with a different decomposition principle
kaliszyk@36280
  1083
  and a proof of equivalence *}
kaliszyk@36280
  1084
kaliszyk@36280
  1085
inductive
haftmann@40952
  1086
  list_eq2 :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<approx>2 _")
kaliszyk@36280
  1087
where
urbanc@40030
  1088
  "(a # b # xs) \<approx>2 (b # a # xs)"
urbanc@40030
  1089
| "[] \<approx>2 []"
haftmann@40952
  1090
| "xs \<approx>2 ys \<Longrightarrow> ys \<approx>2 xs"
urbanc@40030
  1091
| "(a # a # xs) \<approx>2 (a # xs)"
haftmann@40952
  1092
| "xs \<approx>2 ys \<Longrightarrow> (a # xs) \<approx>2 (a # ys)"
haftmann@40952
  1093
| "xs1 \<approx>2 xs2 \<Longrightarrow> xs2 \<approx>2 xs3 \<Longrightarrow> xs1 \<approx>2 xs3"
kaliszyk@36280
  1094
kaliszyk@36280
  1095
lemma list_eq2_refl:
urbanc@40030
  1096
  shows "xs \<approx>2 xs"
kaliszyk@36280
  1097
  by (induct xs) (auto intro: list_eq2.intros)
kaliszyk@36280
  1098
kaliszyk@36280
  1099
lemma cons_delete_list_eq2:
haftmann@40953
  1100
  shows "(a # (removeAll a A)) \<approx>2 (if List.member A a then A else a # A)"
kaliszyk@36280
  1101
  apply (induct A)
urbanc@40030
  1102
  apply (simp add: list_eq2_refl)
haftmann@40953
  1103
  apply (case_tac "List.member (aa # A) a")
urbanc@40030
  1104
  apply (simp_all)
kaliszyk@36280
  1105
  apply (case_tac [!] "a = aa")
kaliszyk@36280
  1106
  apply (simp_all)
haftmann@40953
  1107
  apply (case_tac "List.member A a")
urbanc@40030
  1108
  apply (auto)[2]
kaliszyk@36280
  1109
  apply (metis list_eq2.intros(3) list_eq2.intros(4) list_eq2.intros(5) list_eq2.intros(6))
kaliszyk@36280
  1110
  apply (metis list_eq2.intros(1) list_eq2.intros(5) list_eq2.intros(6))
haftmann@40953
  1111
  apply (auto simp add: list_eq2_refl)
kaliszyk@36280
  1112
  done
kaliszyk@36280
  1113
haftmann@40953
  1114
lemma member_delete_list_eq2:
haftmann@40953
  1115
  assumes a: "List.member r e"
urbanc@40030
  1116
  shows "(e # removeAll e r) \<approx>2 r"
kaliszyk@36280
  1117
  using a cons_delete_list_eq2[of e r]
kaliszyk@36280
  1118
  by simp
kaliszyk@36280
  1119
kaliszyk@36280
  1120
lemma list_eq2_equiv:
kaliszyk@36280
  1121
  "(l \<approx> r) \<longleftrightarrow> (list_eq2 l r)"
kaliszyk@36280
  1122
proof
kaliszyk@36280
  1123
  show "list_eq2 l r \<Longrightarrow> l \<approx> r" by (induct rule: list_eq2.induct) auto
kaliszyk@36280
  1124
next
kaliszyk@36280
  1125
  {
kaliszyk@36280
  1126
    fix n
urbanc@40030
  1127
    assume a: "card_list l = n" and b: "l \<approx> r"
urbanc@40030
  1128
    have "l \<approx>2 r"
kaliszyk@36280
  1129
      using a b
kaliszyk@36280
  1130
    proof (induct n arbitrary: l r)
kaliszyk@36280
  1131
      case 0
urbanc@40030
  1132
      have "card_list l = 0" by fact
haftmann@40953
  1133
      then have "\<forall>x. \<not> List.member l x" by auto
urbanc@40030
  1134
      then have z: "l = []" by auto
kaliszyk@36280
  1135
      then have "r = []" using `l \<approx> r` by simp
kaliszyk@36280
  1136
      then show ?case using z list_eq2_refl by simp
kaliszyk@36280
  1137
    next
kaliszyk@36280
  1138
      case (Suc m)
kaliszyk@36280
  1139
      have b: "l \<approx> r" by fact
urbanc@40030
  1140
      have d: "card_list l = Suc m" by fact
haftmann@40953
  1141
      then have "\<exists>a. List.member l a" 
wenzelm@41067
  1142
        apply(simp)
wenzelm@41067
  1143
        apply(drule card_eq_SucD)
wenzelm@41067
  1144
        apply(blast)
wenzelm@41067
  1145
        done
haftmann@40953
  1146
      then obtain a where e: "List.member l a" by auto
haftmann@40953
  1147
      then have e': "List.member r a" using list_eq_def [simplified List.member_def [symmetric], of l r] b 
wenzelm@41067
  1148
        by auto
urbanc@40030
  1149
      have f: "card_list (removeAll a l) = m" using e d by (simp)
kaliszyk@39996
  1150
      have g: "removeAll a l \<approx> removeAll a r" using removeAll_rsp b by simp
urbanc@40030
  1151
      have "(removeAll a l) \<approx>2 (removeAll a r)" by (rule Suc.hyps[OF f g])
urbanc@40030
  1152
      then have h: "(a # removeAll a l) \<approx>2 (a # removeAll a r)" by (rule list_eq2.intros(5))
wenzelm@41067
  1153
      have i: "l \<approx>2 (a # removeAll a l)"
haftmann@40953
  1154
        by (rule list_eq2.intros(3)[OF member_delete_list_eq2[OF e]])
urbanc@40030
  1155
      have "l \<approx>2 (a # removeAll a r)" by (rule list_eq2.intros(6)[OF i h])
haftmann@40953
  1156
      then show ?case using list_eq2.intros(6)[OF _ member_delete_list_eq2[OF e']] by simp
kaliszyk@36280
  1157
    qed
kaliszyk@36280
  1158
    }
urbanc@40030
  1159
  then show "l \<approx> r \<Longrightarrow> l \<approx>2 r" by blast
kaliszyk@36280
  1160
qed
kaliszyk@36280
  1161
kaliszyk@36280
  1162
kaliszyk@36280
  1163
(* We cannot write it as "assumes .. shows" since Isabelle changes
kaliszyk@36280
  1164
   the quantifiers to schematic variables and reintroduces them in
kaliszyk@36280
  1165
   a different order *)
kaliszyk@36280
  1166
lemma fset_eq_cases:
kaliszyk@36280
  1167
 "\<lbrakk>a1 = a2;
urbanc@40030
  1168
   \<And>a b xs. \<lbrakk>a1 = insert_fset a (insert_fset b xs); a2 = insert_fset b (insert_fset a xs)\<rbrakk> \<Longrightarrow> P;
kaliszyk@36280
  1169
   \<lbrakk>a1 = {||}; a2 = {||}\<rbrakk> \<Longrightarrow> P; \<And>xs ys. \<lbrakk>a1 = ys; a2 = xs; xs = ys\<rbrakk> \<Longrightarrow> P;
urbanc@40030
  1170
   \<And>a xs. \<lbrakk>a1 = insert_fset a (insert_fset a xs); a2 = insert_fset a xs\<rbrakk> \<Longrightarrow> P;
urbanc@40030
  1171
   \<And>xs ys a. \<lbrakk>a1 = insert_fset a xs; a2 = insert_fset a ys; xs = ys\<rbrakk> \<Longrightarrow> P;
kaliszyk@36280
  1172
   \<And>xs1 xs2 xs3. \<lbrakk>a1 = xs1; a2 = xs3; xs1 = xs2; xs2 = xs3\<rbrakk> \<Longrightarrow> P\<rbrakk>
kaliszyk@36280
  1173
  \<Longrightarrow> P"
kaliszyk@36280
  1174
  by (lifting list_eq2.cases[simplified list_eq2_equiv[symmetric]])
kaliszyk@36280
  1175
kaliszyk@36280
  1176
lemma fset_eq_induct:
kaliszyk@36280
  1177
  assumes "x1 = x2"
urbanc@40030
  1178
  and "\<And>a b xs. P (insert_fset a (insert_fset b xs)) (insert_fset b (insert_fset a xs))"
kaliszyk@36280
  1179
  and "P {||} {||}"
kaliszyk@36280
  1180
  and "\<And>xs ys. \<lbrakk>xs = ys; P xs ys\<rbrakk> \<Longrightarrow> P ys xs"
urbanc@40030
  1181
  and "\<And>a xs. P (insert_fset a (insert_fset a xs)) (insert_fset a xs)"
urbanc@40030
  1182
  and "\<And>xs ys a. \<lbrakk>xs = ys; P xs ys\<rbrakk> \<Longrightarrow> P (insert_fset a xs) (insert_fset a ys)"
kaliszyk@36280
  1183
  and "\<And>xs1 xs2 xs3. \<lbrakk>xs1 = xs2; P xs1 xs2; xs2 = xs3; P xs2 xs3\<rbrakk> \<Longrightarrow> P xs1 xs3"
kaliszyk@36280
  1184
  shows "P x1 x2"
kaliszyk@36280
  1185
  using assms
kaliszyk@36280
  1186
  by (lifting list_eq2.induct[simplified list_eq2_equiv[symmetric]])
kaliszyk@36280
  1187
kaliszyk@36280
  1188
ML {*
kaliszyk@36465
  1189
fun dest_fsetT (Type (@{type_name fset}, [T])) = T
kaliszyk@36280
  1190
  | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
kaliszyk@36280
  1191
*}
kaliszyk@36280
  1192
kaliszyk@36280
  1193
no_notation
urbanc@40034
  1194
  list_eq (infix "\<approx>" 50) and 
urbanc@40034
  1195
  list_eq2 (infix "\<approx>2" 50)
kaliszyk@36280
  1196
kaliszyk@36280
  1197
end