src/HOL/Quotient_Examples/FSet.thy
author Cezary Kaliszyk <kaliszyk@in.tum.de>
Fri Oct 15 21:50:26 2010 +0900 (2010-10-15)
changeset 39996 c02078ff8691
parent 39995 849578dd6127
child 40030 9f8dcf6ef563
permissions -rw-r--r--
FSet: definition changes propagated from Nominal and more use of 'descending' tactic
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
kaliszyk@36465
     5
A reasoning infrastructure for the type of finite sets.
kaliszyk@36280
     6
*)
kaliszyk@36465
     7
kaliszyk@36280
     8
theory FSet
kaliszyk@36465
     9
imports Quotient_List
kaliszyk@36280
    10
begin
kaliszyk@36280
    11
kaliszyk@36280
    12
text {* Definiton of List relation and the quotient type *}
kaliszyk@36280
    13
kaliszyk@36280
    14
fun
kaliszyk@36280
    15
  list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50)
kaliszyk@36280
    16
where
kaliszyk@39996
    17
  "list_eq xs ys = (set xs = set ys)"
kaliszyk@36280
    18
kaliszyk@36280
    19
lemma list_eq_equivp:
kaliszyk@36280
    20
  shows "equivp list_eq"
kaliszyk@36280
    21
  unfolding equivp_reflp_symp_transp
kaliszyk@36280
    22
  unfolding reflp_def symp_def transp_def
kaliszyk@36280
    23
  by auto
kaliszyk@36280
    24
kaliszyk@36280
    25
quotient_type
kaliszyk@36280
    26
  'a fset = "'a list" / "list_eq"
kaliszyk@36280
    27
  by (rule list_eq_equivp)
kaliszyk@36280
    28
kaliszyk@39994
    29
text {* Raw definitions of membership, sublist, cardinality,
kaliszyk@39994
    30
  intersection
kaliszyk@39994
    31
*}
kaliszyk@36280
    32
kaliszyk@36280
    33
definition
kaliszyk@36280
    34
  memb :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
kaliszyk@36280
    35
where
kaliszyk@36280
    36
  "memb x xs \<equiv> x \<in> set xs"
kaliszyk@36280
    37
kaliszyk@36280
    38
definition
kaliszyk@36280
    39
  sub_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
kaliszyk@36280
    40
where
kaliszyk@39996
    41
  "sub_list xs ys \<equiv> set xs \<subseteq> set ys"
kaliszyk@36280
    42
kaliszyk@39996
    43
definition
kaliszyk@36280
    44
  fcard_raw :: "'a list \<Rightarrow> nat"
kaliszyk@36280
    45
where
kaliszyk@39996
    46
  "fcard_raw xs = card (set xs)"
kaliszyk@36280
    47
kaliszyk@36280
    48
primrec
kaliszyk@36280
    49
  finter_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
kaliszyk@36280
    50
where
kaliszyk@39996
    51
  "finter_raw [] ys = []"
kaliszyk@39996
    52
| "finter_raw (x # xs) ys =
kaliszyk@39996
    53
    (if x \<in> set ys then x # (finter_raw xs ys) else finter_raw xs ys)"
kaliszyk@36675
    54
kaliszyk@36675
    55
primrec
kaliszyk@36675
    56
  fminus_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
kaliszyk@36675
    57
where
kaliszyk@39996
    58
  "fminus_raw ys [] = ys"
kaliszyk@39996
    59
| "fminus_raw ys (x # xs) = fminus_raw (removeAll x ys) xs"
kaliszyk@36280
    60
kaliszyk@36280
    61
definition
kaliszyk@36280
    62
  rsp_fold
kaliszyk@36280
    63
where
kaliszyk@36280
    64
  "rsp_fold f = (\<forall>u v w. (f u (f v w) = f v (f u w)))"
kaliszyk@36280
    65
kaliszyk@36280
    66
primrec
kaliszyk@36280
    67
  ffold_raw :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"
kaliszyk@36280
    68
where
kaliszyk@36280
    69
  "ffold_raw f z [] = z"
kaliszyk@36675
    70
| "ffold_raw f z (a # xs) =
kaliszyk@36280
    71
     (if (rsp_fold f) then
kaliszyk@39996
    72
       if a \<in> set xs then ffold_raw f z xs
kaliszyk@36675
    73
       else f a (ffold_raw f z xs)
kaliszyk@36280
    74
     else z)"
kaliszyk@36280
    75
kaliszyk@36280
    76
text {* Composition Quotient *}
kaliszyk@36280
    77
kaliszyk@39994
    78
lemma list_all2_refl1:
kaliszyk@37492
    79
  shows "(list_all2 op \<approx>) r r"
kaliszyk@37492
    80
  by (rule list_all2_refl) (metis equivp_def fset_equivp)
kaliszyk@36280
    81
kaliszyk@36280
    82
lemma compose_list_refl:
kaliszyk@37492
    83
  shows "(list_all2 op \<approx> OOO op \<approx>) r r"
kaliszyk@36280
    84
proof
kaliszyk@36465
    85
  have *: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp])
kaliszyk@39994
    86
  show "list_all2 op \<approx> r r" by (rule list_all2_refl1)
kaliszyk@37492
    87
  with * show "(op \<approx> OO list_all2 op \<approx>) r r" ..
kaliszyk@36280
    88
qed
kaliszyk@36280
    89
kaliszyk@36280
    90
lemma Quotient_fset_list:
kaliszyk@37492
    91
  shows "Quotient (list_all2 op \<approx>) (map abs_fset) (map rep_fset)"
kaliszyk@36280
    92
  by (fact list_quotient[OF Quotient_fset])
kaliszyk@36280
    93
kaliszyk@36280
    94
lemma map_rel_cong: "b \<approx> ba \<Longrightarrow> map f b \<approx> map f ba"
kaliszyk@36280
    95
  unfolding list_eq.simps
kaliszyk@39996
    96
  by (simp only: set_map)
kaliszyk@36280
    97
kaliszyk@36280
    98
lemma quotient_compose_list[quot_thm]:
kaliszyk@37492
    99
  shows  "Quotient ((list_all2 op \<approx>) OOO (op \<approx>))
kaliszyk@36280
   100
    (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)"
kaliszyk@36280
   101
  unfolding Quotient_def comp_def
kaliszyk@36280
   102
proof (intro conjI allI)
kaliszyk@36280
   103
  fix a r s
kaliszyk@36280
   104
  show "abs_fset (map abs_fset (map rep_fset (rep_fset a))) = a"
kaliszyk@36280
   105
    by (simp add: abs_o_rep[OF Quotient_fset] Quotient_abs_rep[OF Quotient_fset] map_id)
kaliszyk@37492
   106
  have b: "list_all2 op \<approx> (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
kaliszyk@39994
   107
    by (rule list_all2_refl1)
kaliszyk@37492
   108
  have c: "(op \<approx> OO list_all2 op \<approx>) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
kaliszyk@36280
   109
    by (rule, rule equivp_reflp[OF fset_equivp]) (rule b)
kaliszyk@37492
   110
  show "(list_all2 op \<approx> OOO op \<approx>) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
kaliszyk@39994
   111
    by (rule, rule list_all2_refl1) (rule c)
kaliszyk@37492
   112
  show "(list_all2 op \<approx> OOO op \<approx>) r s = ((list_all2 op \<approx> OOO op \<approx>) r r \<and>
kaliszyk@37492
   113
        (list_all2 op \<approx> OOO op \<approx>) s s \<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s))"
kaliszyk@36280
   114
  proof (intro iffI conjI)
kaliszyk@37492
   115
    show "(list_all2 op \<approx> OOO op \<approx>) r r" by (rule compose_list_refl)
kaliszyk@37492
   116
    show "(list_all2 op \<approx> OOO op \<approx>) s s" by (rule compose_list_refl)
kaliszyk@36280
   117
  next
kaliszyk@37492
   118
    assume a: "(list_all2 op \<approx> OOO op \<approx>) r s"
kaliszyk@36465
   119
    then have b: "map abs_fset r \<approx> map abs_fset s"
kaliszyk@36465
   120
    proof (elim pred_compE)
kaliszyk@36280
   121
      fix b ba
kaliszyk@37492
   122
      assume c: "list_all2 op \<approx> r b"
kaliszyk@36280
   123
      assume d: "b \<approx> ba"
kaliszyk@37492
   124
      assume e: "list_all2 op \<approx> ba s"
kaliszyk@36280
   125
      have f: "map abs_fset r = map abs_fset b"
kaliszyk@36280
   126
        using Quotient_rel[OF Quotient_fset_list] c by blast
kaliszyk@36280
   127
      have "map abs_fset ba = map abs_fset s"
kaliszyk@36280
   128
        using Quotient_rel[OF Quotient_fset_list] e by blast
kaliszyk@36280
   129
      then have g: "map abs_fset s = map abs_fset ba" by simp
kaliszyk@36280
   130
      then show "map abs_fset r \<approx> map abs_fset s" using d f map_rel_cong by simp
kaliszyk@36280
   131
    qed
kaliszyk@36280
   132
    then show "abs_fset (map abs_fset r) = abs_fset (map abs_fset s)"
kaliszyk@36280
   133
      using Quotient_rel[OF Quotient_fset] by blast
kaliszyk@36280
   134
  next
kaliszyk@37492
   135
    assume a: "(list_all2 op \<approx> OOO op \<approx>) r r \<and> (list_all2 op \<approx> OOO op \<approx>) s s
kaliszyk@36280
   136
      \<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s)"
kaliszyk@37492
   137
    then have s: "(list_all2 op \<approx> OOO op \<approx>) s s" by simp
kaliszyk@36280
   138
    have d: "map abs_fset r \<approx> map abs_fset s"
kaliszyk@36280
   139
      by (subst Quotient_rel[OF Quotient_fset]) (simp add: a)
kaliszyk@36280
   140
    have b: "map rep_fset (map abs_fset r) \<approx> map rep_fset (map abs_fset s)"
kaliszyk@36280
   141
      by (rule map_rel_cong[OF d])
kaliszyk@37492
   142
    have y: "list_all2 op \<approx> (map rep_fset (map abs_fset s)) s"
kaliszyk@39994
   143
      by (fact rep_abs_rsp_left[OF Quotient_fset_list, OF list_all2_refl1[of s]])
kaliszyk@37492
   144
    have c: "(op \<approx> OO list_all2 op \<approx>) (map rep_fset (map abs_fset r)) s"
kaliszyk@36280
   145
      by (rule pred_compI) (rule b, rule y)
kaliszyk@37492
   146
    have z: "list_all2 op \<approx> r (map rep_fset (map abs_fset r))"
kaliszyk@39994
   147
      by (fact rep_abs_rsp[OF Quotient_fset_list, OF list_all2_refl1[of r]])
kaliszyk@37492
   148
    then show "(list_all2 op \<approx> OOO op \<approx>) r s"
kaliszyk@36280
   149
      using a c pred_compI by simp
kaliszyk@36280
   150
  qed
kaliszyk@36280
   151
qed
kaliszyk@36280
   152
kaliszyk@39996
   153
kaliszyk@39996
   154
lemma set_finter_raw[simp]:
kaliszyk@39996
   155
  "set (finter_raw xs ys) = set xs \<inter> set ys"
kaliszyk@39996
   156
  by (induct xs) (auto simp add: memb_def)
kaliszyk@39996
   157
kaliszyk@39996
   158
lemma set_fminus_raw[simp]: 
kaliszyk@39996
   159
  "set (fminus_raw xs ys) = (set xs - set ys)"
kaliszyk@39996
   160
  by (induct ys arbitrary: xs) (auto)
kaliszyk@39996
   161
kaliszyk@39996
   162
kaliszyk@36280
   163
text {* Respectfullness *}
kaliszyk@36280
   164
kaliszyk@39994
   165
lemma append_rsp[quot_respect]:
kaliszyk@39994
   166
  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) append append"
kaliszyk@39994
   167
  by (simp)
kaliszyk@36280
   168
kaliszyk@39994
   169
lemma sub_list_rsp[quot_respect]:
kaliszyk@36280
   170
  shows "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list"
kaliszyk@36280
   171
  by (auto simp add: sub_list_def)
kaliszyk@36280
   172
kaliszyk@36280
   173
lemma memb_rsp[quot_respect]:
kaliszyk@36280
   174
  shows "(op = ===> op \<approx> ===> op =) memb memb"
kaliszyk@36280
   175
  by (auto simp add: memb_def)
kaliszyk@36280
   176
kaliszyk@36280
   177
lemma nil_rsp[quot_respect]:
kaliszyk@39994
   178
  shows "(op \<approx>) Nil Nil"
kaliszyk@36280
   179
  by simp
kaliszyk@36280
   180
kaliszyk@36280
   181
lemma cons_rsp[quot_respect]:
kaliszyk@39994
   182
  shows "(op = ===> op \<approx> ===> op \<approx>) Cons Cons"
kaliszyk@36280
   183
  by simp
kaliszyk@36280
   184
kaliszyk@36280
   185
lemma map_rsp[quot_respect]:
kaliszyk@36280
   186
  shows "(op = ===> op \<approx> ===> op \<approx>) map map"
kaliszyk@36280
   187
  by auto
kaliszyk@36280
   188
kaliszyk@36280
   189
lemma set_rsp[quot_respect]:
kaliszyk@36280
   190
  "(op \<approx> ===> op =) set set"
kaliszyk@36280
   191
  by auto
kaliszyk@36280
   192
kaliszyk@36280
   193
lemma list_equiv_rsp[quot_respect]:
kaliszyk@36280
   194
  shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
kaliszyk@36280
   195
  by auto
kaliszyk@36280
   196
kaliszyk@39996
   197
lemma finter_raw_rsp[quot_respect]:
kaliszyk@39996
   198
  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) finter_raw finter_raw"
kaliszyk@39996
   199
  by simp
kaliszyk@39996
   200
kaliszyk@39996
   201
lemma removeAll_rsp[quot_respect]:
kaliszyk@39996
   202
  shows "(op = ===> op \<approx> ===> op \<approx>) removeAll removeAll"
kaliszyk@39996
   203
  by simp
kaliszyk@39996
   204
kaliszyk@39996
   205
lemma fminus_raw_rsp[quot_respect]:
kaliszyk@39996
   206
  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) fminus_raw fminus_raw"
kaliszyk@39996
   207
  by simp
kaliszyk@39996
   208
kaliszyk@39996
   209
lemma fcard_raw_rsp[quot_respect]:
kaliszyk@39996
   210
  shows "(op \<approx> ===> op =) fcard_raw fcard_raw"
kaliszyk@39996
   211
  by (simp add: fcard_raw_def)
kaliszyk@39996
   212
kaliszyk@39996
   213
kaliszyk@39996
   214
kaliszyk@36280
   215
lemma not_memb_nil:
kaliszyk@36280
   216
  shows "\<not> memb x []"
kaliszyk@36280
   217
  by (simp add: memb_def)
kaliszyk@36280
   218
kaliszyk@36280
   219
lemma memb_cons_iff:
kaliszyk@36280
   220
  shows "memb x (y # xs) = (x = y \<or> memb x xs)"
kaliszyk@36280
   221
  by (induct xs) (auto simp add: memb_def)
kaliszyk@36280
   222
kaliszyk@36280
   223
lemma memb_absorb:
kaliszyk@36280
   224
  shows "memb x xs \<Longrightarrow> x # xs \<approx> xs"
kaliszyk@36280
   225
  by (induct xs) (auto simp add: memb_def)
kaliszyk@36280
   226
kaliszyk@36280
   227
lemma none_memb_nil:
kaliszyk@36280
   228
  "(\<forall>x. \<not> memb x xs) = (xs \<approx> [])"
kaliszyk@36280
   229
  by (simp add: memb_def)
kaliszyk@36280
   230
kaliszyk@36280
   231
kaliszyk@36280
   232
lemma memb_commute_ffold_raw:
kaliszyk@39996
   233
  "rsp_fold f \<Longrightarrow> h \<in> set b \<Longrightarrow> ffold_raw f z b = f h (ffold_raw f z (removeAll h b))"
kaliszyk@36280
   234
  apply (induct b)
kaliszyk@39996
   235
  apply (auto simp add: rsp_fold_def)
kaliszyk@36280
   236
  done
kaliszyk@36280
   237
kaliszyk@36280
   238
lemma ffold_raw_rsp_pre:
kaliszyk@39996
   239
  "set a = set b \<Longrightarrow> ffold_raw f z a = ffold_raw f z b"
kaliszyk@36280
   240
  apply (induct a arbitrary: b)
kaliszyk@36280
   241
  apply (simp)
kaliszyk@39996
   242
  apply (simp (no_asm_use))
kaliszyk@36280
   243
  apply (rule conjI)
kaliszyk@36280
   244
  apply (rule_tac [!] impI)
kaliszyk@36280
   245
  apply (rule_tac [!] conjI)
kaliszyk@36280
   246
  apply (rule_tac [!] impI)
kaliszyk@39996
   247
  apply (metis insert_absorb)
kaliszyk@39996
   248
  apply (metis List.insert_def List.set.simps(2) List.set_insert ffold_raw.simps(2))
kaliszyk@39996
   249
  apply (metis Diff_insert_absorb insertI1 memb_commute_ffold_raw set_removeAll)
kaliszyk@39996
   250
  apply(drule_tac x="removeAll a1 b" in meta_spec)
kaliszyk@39996
   251
  apply(auto)
kaliszyk@39996
   252
  apply(drule meta_mp)
kaliszyk@39996
   253
  apply(blast)
kaliszyk@39996
   254
  by (metis List.set.simps(2) emptyE ffold_raw.simps(2) in_listsp_conv_set listsp.simps mem_def)
kaliszyk@36280
   255
kaliszyk@39995
   256
lemma ffold_raw_rsp[quot_respect]:
kaliszyk@39995
   257
  shows "(op = ===> op = ===> op \<approx> ===> op =) ffold_raw ffold_raw"
kaliszyk@39996
   258
  unfolding fun_rel_def
kaliszyk@39996
   259
  by(auto intro: ffold_raw_rsp_pre)
kaliszyk@36280
   260
kaliszyk@36280
   261
lemma concat_rsp_pre:
kaliszyk@37492
   262
  assumes a: "list_all2 op \<approx> x x'"
kaliszyk@36280
   263
  and     b: "x' \<approx> y'"
kaliszyk@37492
   264
  and     c: "list_all2 op \<approx> y' y"
kaliszyk@36280
   265
  and     d: "\<exists>x\<in>set x. xa \<in> set x"
kaliszyk@36280
   266
  shows "\<exists>x\<in>set y. xa \<in> set x"
kaliszyk@36280
   267
proof -
kaliszyk@36280
   268
  obtain xb where e: "xb \<in> set x" and f: "xa \<in> set xb" using d by auto
kaliszyk@37492
   269
  have "\<exists>y. y \<in> set x' \<and> xb \<approx> y" by (rule list_all2_find_element[OF e a])
kaliszyk@36280
   270
  then obtain ya where h: "ya \<in> set x'" and i: "xb \<approx> ya" by auto
kaliszyk@36465
   271
  have "ya \<in> set y'" using b h by simp
kaliszyk@37492
   272
  then have "\<exists>yb. yb \<in> set y \<and> ya \<approx> yb" using c by (rule list_all2_find_element)
kaliszyk@36280
   273
  then show ?thesis using f i by auto
kaliszyk@36280
   274
qed
kaliszyk@36280
   275
kaliszyk@39994
   276
lemma concat_rsp[quot_respect]:
kaliszyk@37492
   277
  shows "(list_all2 op \<approx> OOO op \<approx> ===> op \<approx>) concat concat"
kaliszyk@36280
   278
proof (rule fun_relI, elim pred_compE)
kaliszyk@36280
   279
  fix a b ba bb
kaliszyk@37492
   280
  assume a: "list_all2 op \<approx> a ba"
kaliszyk@36280
   281
  assume b: "ba \<approx> bb"
kaliszyk@37492
   282
  assume c: "list_all2 op \<approx> bb b"
kaliszyk@39996
   283
  have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" 
kaliszyk@39996
   284
  proof
kaliszyk@36280
   285
    fix x
kaliszyk@39996
   286
    show "(\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" 
kaliszyk@39996
   287
    proof
kaliszyk@36280
   288
      assume d: "\<exists>xa\<in>set a. x \<in> set xa"
kaliszyk@36280
   289
      show "\<exists>xa\<in>set b. x \<in> set xa" by (rule concat_rsp_pre[OF a b c d])
kaliszyk@36280
   290
    next
kaliszyk@36280
   291
      assume e: "\<exists>xa\<in>set b. x \<in> set xa"
kaliszyk@37492
   292
      have a': "list_all2 op \<approx> ba a" by (rule list_all2_symp[OF list_eq_equivp, OF a])
kaliszyk@36280
   293
      have b': "bb \<approx> ba" by (rule equivp_symp[OF list_eq_equivp, OF b])
kaliszyk@37492
   294
      have c': "list_all2 op \<approx> b bb" by (rule list_all2_symp[OF list_eq_equivp, OF c])
kaliszyk@36280
   295
      show "\<exists>xa\<in>set a. x \<in> set xa" by (rule concat_rsp_pre[OF c' b' a' e])
kaliszyk@36280
   296
    qed
kaliszyk@36280
   297
  qed
kaliszyk@39996
   298
  then show "concat a \<approx> concat b" by auto
kaliszyk@36280
   299
qed
kaliszyk@36280
   300
bulwahn@36639
   301
lemma [quot_respect]:
kaliszyk@39994
   302
  shows "((op =) ===> op \<approx> ===> op \<approx>) filter filter"
bulwahn@36639
   303
  by auto
bulwahn@36639
   304
kaliszyk@36280
   305
text {* Distributive lattice with bot *}
kaliszyk@36280
   306
kaliszyk@36280
   307
lemma append_inter_distrib:
kaliszyk@36280
   308
  "x @ (finter_raw y z) \<approx> finter_raw (x @ y) (x @ z)"
kaliszyk@36280
   309
  apply (induct x)
kaliszyk@39996
   310
  apply (auto)
kaliszyk@36465
   311
  done
kaliszyk@36280
   312
urbanc@37634
   313
instantiation fset :: (type) "{bounded_lattice_bot, distrib_lattice, minus}"
kaliszyk@36280
   314
begin
kaliszyk@36280
   315
kaliszyk@36280
   316
quotient_definition
kaliszyk@36280
   317
  "bot :: 'a fset" is "[] :: 'a list"
kaliszyk@36280
   318
kaliszyk@36280
   319
abbreviation
kaliszyk@36280
   320
  fempty  ("{||}")
kaliszyk@36280
   321
where
kaliszyk@36280
   322
  "{||} \<equiv> bot :: 'a fset"
kaliszyk@36280
   323
kaliszyk@36280
   324
quotient_definition
kaliszyk@36280
   325
  "less_eq_fset \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> bool)"
kaliszyk@36280
   326
is
kaliszyk@36280
   327
  "sub_list \<Colon> ('a list \<Rightarrow> 'a list \<Rightarrow> bool)"
kaliszyk@36280
   328
kaliszyk@36280
   329
abbreviation
kaliszyk@36280
   330
  f_subset_eq :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subseteq>|" 50)
kaliszyk@36280
   331
where
kaliszyk@36280
   332
  "xs |\<subseteq>| ys \<equiv> xs \<le> ys"
kaliszyk@36280
   333
kaliszyk@36280
   334
definition
kaliszyk@39995
   335
  less_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool"
kaliszyk@39995
   336
where  
kaliszyk@39995
   337
  "xs < ys \<equiv> xs \<le> ys \<and> xs \<noteq> (ys::'a fset)"
kaliszyk@36280
   338
kaliszyk@36280
   339
abbreviation
kaliszyk@39996
   340
  fsubset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subset>|" 50)
kaliszyk@36280
   341
where
kaliszyk@36280
   342
  "xs |\<subset>| ys \<equiv> xs < ys"
kaliszyk@36280
   343
kaliszyk@36280
   344
quotient_definition
kaliszyk@39995
   345
  "sup :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
kaliszyk@36280
   346
is
kaliszyk@39994
   347
  "append :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
kaliszyk@36280
   348
kaliszyk@36280
   349
abbreviation
kaliszyk@36675
   350
  funion (infixl "|\<union>|" 65)
kaliszyk@36280
   351
where
kaliszyk@36280
   352
  "xs |\<union>| ys \<equiv> sup (xs :: 'a fset) ys"
kaliszyk@36280
   353
kaliszyk@36280
   354
quotient_definition
kaliszyk@39995
   355
  "inf :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
kaliszyk@36280
   356
is
kaliszyk@39995
   357
  "finter_raw :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
kaliszyk@36280
   358
kaliszyk@36280
   359
abbreviation
kaliszyk@36280
   360
  finter (infixl "|\<inter>|" 65)
kaliszyk@36280
   361
where
kaliszyk@36280
   362
  "xs |\<inter>| ys \<equiv> inf (xs :: 'a fset) ys"
kaliszyk@36280
   363
kaliszyk@36675
   364
quotient_definition
urbanc@37634
   365
  "minus :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
kaliszyk@36675
   366
is
urbanc@37634
   367
  "fminus_raw :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
kaliszyk@36675
   368
kaliszyk@36280
   369
instance
kaliszyk@36280
   370
proof
kaliszyk@36280
   371
  fix x y z :: "'a fset"
urbanc@37634
   372
  show "x |\<subset>| y \<longleftrightarrow> x |\<subseteq>| y \<and> \<not> y |\<subseteq>| x"
kaliszyk@39995
   373
    unfolding less_fset_def 
urbanc@37634
   374
    by (descending) (auto simp add: sub_list_def)
urbanc@37634
   375
  show "x |\<subseteq>| x"  by (descending) (simp add: sub_list_def)
urbanc@37634
   376
  show "{||} |\<subseteq>| x" by (descending) (simp add: sub_list_def)
urbanc@37634
   377
  show "x |\<subseteq>| x |\<union>| y" by (descending) (simp add: sub_list_def)
urbanc@37634
   378
  show "y |\<subseteq>| x |\<union>| y" by (descending) (simp add: sub_list_def)
kaliszyk@39996
   379
  show "x |\<inter>| y |\<subseteq>| x"
kaliszyk@39996
   380
    by (descending) (simp add: sub_list_def memb_def[symmetric])
urbanc@37634
   381
  show "x |\<inter>| y |\<subseteq>| y" 
kaliszyk@39996
   382
    by (descending) (simp add: sub_list_def memb_def[symmetric])
urbanc@37634
   383
  show "x |\<union>| (y |\<inter>| z) = x |\<union>| y |\<inter>| (x |\<union>| z)" 
urbanc@37634
   384
    by (descending) (rule append_inter_distrib)
kaliszyk@36280
   385
next
kaliszyk@36280
   386
  fix x y z :: "'a fset"
kaliszyk@36280
   387
  assume a: "x |\<subseteq>| y"
kaliszyk@36280
   388
  assume b: "y |\<subseteq>| z"
urbanc@37634
   389
  show "x |\<subseteq>| z" using a b 
urbanc@37634
   390
    by (descending) (simp add: sub_list_def)
kaliszyk@36280
   391
next
kaliszyk@36280
   392
  fix x y :: "'a fset"
kaliszyk@36280
   393
  assume a: "x |\<subseteq>| y"
kaliszyk@36280
   394
  assume b: "y |\<subseteq>| x"
urbanc@37634
   395
  show "x = y" using a b 
urbanc@37634
   396
    by (descending) (unfold sub_list_def list_eq.simps, blast)
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@37634
   401
  show "y |\<union>| z |\<subseteq>| x" using a b 
urbanc@37634
   402
    by (descending) (simp add: sub_list_def)
kaliszyk@36280
   403
next
kaliszyk@36280
   404
  fix x y z :: "'a fset"
kaliszyk@36280
   405
  assume a: "x |\<subseteq>| y"
kaliszyk@36280
   406
  assume b: "x |\<subseteq>| z"
urbanc@37634
   407
  show "x |\<subseteq>| y |\<inter>| z" using a b 
kaliszyk@39996
   408
    by (descending) (simp add: sub_list_def memb_def[symmetric])
kaliszyk@36280
   409
qed
kaliszyk@36280
   410
kaliszyk@36280
   411
end
kaliszyk@36280
   412
kaliszyk@36280
   413
section {* Finsert and Membership *}
kaliszyk@36280
   414
kaliszyk@36280
   415
quotient_definition
kaliszyk@36280
   416
  "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
kaliszyk@39994
   417
is "Cons"
kaliszyk@36280
   418
kaliszyk@36280
   419
syntax
kaliszyk@36280
   420
  "@Finset"     :: "args => 'a fset"  ("{|(_)|}")
kaliszyk@36280
   421
kaliszyk@36280
   422
translations
kaliszyk@36280
   423
  "{|x, xs|}" == "CONST finsert x {|xs|}"
kaliszyk@36280
   424
  "{|x|}"     == "CONST finsert x {||}"
kaliszyk@36280
   425
kaliszyk@36280
   426
quotient_definition
kaliszyk@36280
   427
  fin (infix "|\<in>|" 50)
kaliszyk@36280
   428
where
kaliszyk@36280
   429
  "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" is "memb"
kaliszyk@36280
   430
kaliszyk@36280
   431
abbreviation
kaliszyk@36280
   432
  fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<notin>|" 50)
kaliszyk@36280
   433
where
kaliszyk@36280
   434
  "x |\<notin>| S \<equiv> \<not> (x |\<in>| S)"
kaliszyk@36280
   435
kaliszyk@36465
   436
section {* Other constants on the Quotient Type *}
kaliszyk@36280
   437
kaliszyk@36280
   438
quotient_definition
kaliszyk@36465
   439
  "fcard :: 'a fset \<Rightarrow> nat"
kaliszyk@36280
   440
is
kaliszyk@39995
   441
  fcard_raw
kaliszyk@36280
   442
kaliszyk@36280
   443
quotient_definition
kaliszyk@36280
   444
  "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
kaliszyk@36280
   445
is
kaliszyk@39995
   446
  map
kaliszyk@36280
   447
kaliszyk@36280
   448
quotient_definition
kaliszyk@39996
   449
  "fdelete :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
kaliszyk@39996
   450
  is removeAll
kaliszyk@36280
   451
kaliszyk@36280
   452
quotient_definition
kaliszyk@39996
   453
  "fset :: 'a fset \<Rightarrow> 'a set"
kaliszyk@36280
   454
  is "set"
kaliszyk@36280
   455
kaliszyk@36280
   456
quotient_definition
kaliszyk@36280
   457
  "ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b"
kaliszyk@36280
   458
  is "ffold_raw"
kaliszyk@36280
   459
kaliszyk@36280
   460
quotient_definition
kaliszyk@36280
   461
  "fconcat :: ('a fset) fset \<Rightarrow> 'a fset"
kaliszyk@36280
   462
is
kaliszyk@36280
   463
  "concat"
kaliszyk@36280
   464
bulwahn@36639
   465
quotient_definition
bulwahn@36639
   466
  "ffilter :: ('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
bulwahn@36639
   467
is
bulwahn@36639
   468
  "filter"
bulwahn@36639
   469
kaliszyk@36280
   470
text {* Compositional Respectfullness and Preservation *}
kaliszyk@36280
   471
kaliszyk@37492
   472
lemma [quot_respect]: "(list_all2 op \<approx> OOO op \<approx>) [] []"
kaliszyk@36280
   473
  by (fact compose_list_refl)
kaliszyk@36280
   474
kaliszyk@36280
   475
lemma [quot_preserve]: "(abs_fset \<circ> map f) [] = abs_fset []"
kaliszyk@36280
   476
  by simp
kaliszyk@36280
   477
kaliszyk@36280
   478
lemma [quot_respect]:
kaliszyk@39994
   479
  shows "(op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) Cons Cons"
kaliszyk@36280
   480
  apply auto
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
kaliszyk@36280
   487
lemma [quot_preserve]:
kaliszyk@36280
   488
  "(rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op # = finsert"
nipkow@39302
   489
  by (simp add: fun_eq_iff Quotient_abs_rep[OF Quotient_fset]
kaliszyk@36280
   490
      abs_o_rep[OF Quotient_fset] map_id finsert_def)
kaliszyk@36280
   491
kaliszyk@36280
   492
lemma [quot_preserve]:
kaliszyk@36280
   493
  "((map rep_fset \<circ> rep_fset) ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op @ = funion"
nipkow@39302
   494
  by (simp add: fun_eq_iff Quotient_abs_rep[OF Quotient_fset]
kaliszyk@36280
   495
      abs_o_rep[OF Quotient_fset] map_id sup_fset_def)
kaliszyk@36280
   496
kaliszyk@37492
   497
lemma list_all2_app_l:
kaliszyk@36280
   498
  assumes a: "reflp R"
kaliszyk@37492
   499
  and b: "list_all2 R l r"
kaliszyk@37492
   500
  shows "list_all2 R (z @ l) (z @ r)"
kaliszyk@36280
   501
  by (induct z) (simp_all add: b rev_iffD1[OF a meta_eq_to_obj_eq[OF reflp_def]])
kaliszyk@36280
   502
kaliszyk@36280
   503
lemma append_rsp2_pre0:
kaliszyk@37492
   504
  assumes a:"list_all2 op \<approx> x x'"
kaliszyk@37492
   505
  shows "list_all2 op \<approx> (x @ z) (x' @ z)"
kaliszyk@36280
   506
  using a apply (induct x x' rule: list_induct2')
kaliszyk@39994
   507
  by simp_all (rule list_all2_refl1)
kaliszyk@36280
   508
kaliszyk@36280
   509
lemma append_rsp2_pre1:
kaliszyk@37492
   510
  assumes a:"list_all2 op \<approx> x x'"
kaliszyk@37492
   511
  shows "list_all2 op \<approx> (z @ x) (z @ x')"
kaliszyk@36280
   512
  using a apply (induct x x' arbitrary: z rule: list_induct2')
kaliszyk@39994
   513
  apply (rule list_all2_refl1)
kaliszyk@36280
   514
  apply (simp_all del: list_eq.simps)
kaliszyk@37492
   515
  apply (rule list_all2_app_l)
kaliszyk@36280
   516
  apply (simp_all add: reflp_def)
kaliszyk@36280
   517
  done
kaliszyk@36280
   518
kaliszyk@36280
   519
lemma append_rsp2_pre:
kaliszyk@37492
   520
  assumes a:"list_all2 op \<approx> x x'"
kaliszyk@37492
   521
  and     b: "list_all2 op \<approx> z z'"
kaliszyk@37492
   522
  shows "list_all2 op \<approx> (x @ z) (x' @ z')"
kaliszyk@37492
   523
  apply (rule list_all2_transp[OF fset_equivp])
kaliszyk@36280
   524
  apply (rule append_rsp2_pre0)
kaliszyk@36280
   525
  apply (rule a)
kaliszyk@36280
   526
  using b apply (induct z z' rule: list_induct2')
kaliszyk@36280
   527
  apply (simp_all only: append_Nil2)
kaliszyk@39994
   528
  apply (rule list_all2_refl1)
kaliszyk@36280
   529
  apply simp_all
kaliszyk@36280
   530
  apply (rule append_rsp2_pre1)
kaliszyk@36280
   531
  apply simp
kaliszyk@36280
   532
  done
kaliszyk@36280
   533
kaliszyk@36280
   534
lemma [quot_respect]:
kaliszyk@37492
   535
  "(list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) op @ op @"
kaliszyk@36280
   536
proof (intro fun_relI, elim pred_compE)
kaliszyk@36280
   537
  fix x y z w x' z' y' w' :: "'a list list"
kaliszyk@37492
   538
  assume a:"list_all2 op \<approx> x x'"
kaliszyk@36280
   539
  and b:    "x' \<approx> y'"
kaliszyk@37492
   540
  and c:    "list_all2 op \<approx> y' y"
kaliszyk@37492
   541
  assume aa: "list_all2 op \<approx> z z'"
kaliszyk@36280
   542
  and bb:   "z' \<approx> w'"
kaliszyk@37492
   543
  and cc:   "list_all2 op \<approx> w' w"
kaliszyk@37492
   544
  have a': "list_all2 op \<approx> (x @ z) (x' @ z')" using a aa append_rsp2_pre by auto
kaliszyk@36280
   545
  have b': "x' @ z' \<approx> y' @ w'" using b bb by simp
kaliszyk@37492
   546
  have c': "list_all2 op \<approx> (y' @ w') (y @ w)" using c cc append_rsp2_pre by auto
kaliszyk@37492
   547
  have d': "(op \<approx> OO list_all2 op \<approx>) (x' @ z') (y @ w)"
kaliszyk@36280
   548
    by (rule pred_compI) (rule b', rule c')
kaliszyk@37492
   549
  show "(list_all2 op \<approx> OOO op \<approx>) (x @ z) (y @ w)"
kaliszyk@36280
   550
    by (rule pred_compI) (rule a', rule d')
kaliszyk@36280
   551
qed
kaliszyk@36280
   552
kaliszyk@36280
   553
text {* Raw theorems. Finsert, memb, singleron, sub_list *}
kaliszyk@36280
   554
kaliszyk@36280
   555
lemma nil_not_cons:
kaliszyk@36280
   556
  shows "\<not> ([] \<approx> x # xs)"
kaliszyk@36280
   557
  and   "\<not> (x # xs \<approx> [])"
kaliszyk@36280
   558
  by auto
kaliszyk@36280
   559
kaliszyk@36280
   560
lemma no_memb_nil:
kaliszyk@36280
   561
  "(\<forall>x. \<not> memb x xs) = (xs = [])"
kaliszyk@36280
   562
  by (simp add: memb_def)
kaliszyk@36280
   563
kaliszyk@36280
   564
lemma memb_consI1:
kaliszyk@36280
   565
  shows "memb x (x # xs)"
kaliszyk@36280
   566
  by (simp add: memb_def)
kaliszyk@36280
   567
kaliszyk@36280
   568
lemma memb_consI2:
kaliszyk@36280
   569
  shows "memb x xs \<Longrightarrow> memb x (y # xs)"
kaliszyk@36280
   570
  by (simp add: memb_def)
kaliszyk@36280
   571
kaliszyk@36280
   572
lemma singleton_list_eq:
kaliszyk@36280
   573
  shows "[x] \<approx> [y] \<longleftrightarrow> x = y"
kaliszyk@39996
   574
  by (simp)
kaliszyk@36280
   575
kaliszyk@36280
   576
lemma sub_list_cons:
kaliszyk@36280
   577
  "sub_list (x # xs) ys = (memb x ys \<and> sub_list xs ys)"
kaliszyk@36280
   578
  by (auto simp add: memb_def sub_list_def)
kaliszyk@36280
   579
kaliszyk@39996
   580
lemma fminus_raw_red: 
kaliszyk@39996
   581
  "fminus_raw (x # xs) ys = (if x \<in> set ys then fminus_raw xs ys else x # (fminus_raw xs ys))"
kaliszyk@39996
   582
  by (induct ys arbitrary: xs x) (simp_all)
kaliszyk@36675
   583
kaliszyk@36280
   584
text {* Cardinality of finite sets *}
kaliszyk@36280
   585
kaliszyk@36280
   586
lemma fcard_raw_0:
kaliszyk@36280
   587
  shows "fcard_raw xs = 0 \<longleftrightarrow> xs \<approx> []"
kaliszyk@39996
   588
  unfolding fcard_raw_def
kaliszyk@39996
   589
  by (induct xs) (auto)
kaliszyk@36280
   590
kaliszyk@36280
   591
lemma memb_card_not_0:
kaliszyk@36280
   592
  assumes a: "memb a A"
kaliszyk@36280
   593
  shows "\<not>(fcard_raw A = 0)"
kaliszyk@36280
   594
proof -
kaliszyk@36280
   595
  have "\<not>(\<forall>x. \<not> memb x A)" using a by auto
kaliszyk@36280
   596
  then have "\<not>A \<approx> []" using none_memb_nil[of A] by simp
kaliszyk@36280
   597
  then show ?thesis using fcard_raw_0[of A] by simp
kaliszyk@36280
   598
qed
kaliszyk@36280
   599
kaliszyk@36280
   600
text {* fmap *}
kaliszyk@36280
   601
kaliszyk@36280
   602
lemma map_append:
kaliszyk@36280
   603
  "map f (xs @ ys) \<approx> (map f xs) @ (map f ys)"
kaliszyk@36280
   604
  by simp
kaliszyk@36280
   605
kaliszyk@36280
   606
lemma memb_append:
kaliszyk@36280
   607
  "memb x (xs @ ys) \<longleftrightarrow> memb x xs \<or> memb x ys"
kaliszyk@36280
   608
  by (induct xs) (simp_all add: not_memb_nil memb_cons_iff)
kaliszyk@36280
   609
kaliszyk@36280
   610
lemma fset_raw_strong_cases:
kaliszyk@36465
   611
  obtains "xs = []"
kaliszyk@36465
   612
    | x ys where "\<not> memb x ys" and "xs \<approx> x # ys"
kaliszyk@36465
   613
proof (induct xs arbitrary: x ys)
kaliszyk@36465
   614
  case Nil
kaliszyk@36465
   615
  then show thesis by simp
kaliszyk@36465
   616
next
kaliszyk@36465
   617
  case (Cons a xs)
kaliszyk@36465
   618
  have a: "\<lbrakk>xs = [] \<Longrightarrow> thesis; \<And>x ys. \<lbrakk>\<not> memb x ys; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis" by fact
kaliszyk@36465
   619
  have b: "\<And>x' ys'. \<lbrakk>\<not> memb x' ys'; a # xs \<approx> x' # ys'\<rbrakk> \<Longrightarrow> thesis" by fact
kaliszyk@36465
   620
  have c: "xs = [] \<Longrightarrow> thesis" by (metis no_memb_nil singleton_list_eq b)
kaliszyk@36465
   621
  have "\<And>x ys. \<lbrakk>\<not> memb x ys; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis"
kaliszyk@36465
   622
  proof -
kaliszyk@36465
   623
    fix x :: 'a
kaliszyk@36465
   624
    fix ys :: "'a list"
kaliszyk@36465
   625
    assume d:"\<not> memb x ys"
kaliszyk@36465
   626
    assume e:"xs \<approx> x # ys"
kaliszyk@36465
   627
    show thesis
kaliszyk@36465
   628
    proof (cases "x = a")
kaliszyk@36465
   629
      assume h: "x = a"
kaliszyk@36465
   630
      then have f: "\<not> memb a ys" using d by simp
kaliszyk@36465
   631
      have g: "a # xs \<approx> a # ys" using e h by auto
kaliszyk@36465
   632
      show thesis using b f g by simp
kaliszyk@36465
   633
    next
kaliszyk@36465
   634
      assume h: "x \<noteq> a"
kaliszyk@36465
   635
      then have f: "\<not> memb x (a # ys)" using d unfolding memb_def by auto
kaliszyk@36465
   636
      have g: "a # xs \<approx> x # (a # ys)" using e h by auto
kaliszyk@36465
   637
      show thesis using b f g by simp
kaliszyk@36465
   638
    qed
kaliszyk@36465
   639
  qed
kaliszyk@36465
   640
  then show thesis using a c by blast
kaliszyk@36465
   641
qed
kaliszyk@36280
   642
kaliszyk@36280
   643
section {* deletion *}
kaliszyk@36280
   644
kaliszyk@39996
   645
kaliszyk@39996
   646
lemma fset_raw_removeAll_cases:
kaliszyk@39996
   647
  "xs = [] \<or> (\<exists>x. memb x xs \<and> xs \<approx> x # removeAll x xs)"
kaliszyk@36280
   648
  by (induct xs) (auto simp add: memb_def)
kaliszyk@36280
   649
kaliszyk@39996
   650
lemma fremoveAll_filter:
kaliszyk@39996
   651
  "removeAll y xs = [x \<leftarrow> xs. x \<noteq> y]"
kaliszyk@36280
   652
  by (induct xs) simp_all
kaliszyk@36280
   653
kaliszyk@36280
   654
lemma fcard_raw_delete:
kaliszyk@39996
   655
  "fcard_raw (removeAll y xs) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)"
kaliszyk@39996
   656
  by (auto simp add: fcard_raw_def memb_def)
kaliszyk@36280
   657
kaliszyk@36465
   658
lemma set_cong:
kaliszyk@36646
   659
  shows "(x \<approx> y) = (set x = set y)"
kaliszyk@36280
   660
  by auto
kaliszyk@36280
   661
kaliszyk@36280
   662
lemma inj_map_eq_iff:
kaliszyk@36280
   663
  "inj f \<Longrightarrow> (map f l \<approx> map f m) = (l \<approx> m)"
nipkow@39302
   664
  by (simp add: set_eq_iff[symmetric] inj_image_eq_iff)
kaliszyk@36280
   665
kaliszyk@36280
   666
text {* alternate formulation with a different decomposition principle
kaliszyk@36280
   667
  and a proof of equivalence *}
kaliszyk@36280
   668
kaliszyk@36280
   669
inductive
kaliszyk@36280
   670
  list_eq2
kaliszyk@36280
   671
where
kaliszyk@36280
   672
  "list_eq2 (a # b # xs) (b # a # xs)"
kaliszyk@36280
   673
| "list_eq2 [] []"
kaliszyk@36280
   674
| "list_eq2 xs ys \<Longrightarrow> list_eq2 ys xs"
kaliszyk@36280
   675
| "list_eq2 (a # a # xs) (a # xs)"
kaliszyk@36280
   676
| "list_eq2 xs ys \<Longrightarrow> list_eq2 (a # xs) (a # ys)"
kaliszyk@36280
   677
| "\<lbrakk>list_eq2 xs1 xs2; list_eq2 xs2 xs3\<rbrakk> \<Longrightarrow> list_eq2 xs1 xs3"
kaliszyk@36280
   678
kaliszyk@36280
   679
lemma list_eq2_refl:
kaliszyk@36280
   680
  shows "list_eq2 xs xs"
kaliszyk@36280
   681
  by (induct xs) (auto intro: list_eq2.intros)
kaliszyk@36280
   682
kaliszyk@36280
   683
lemma cons_delete_list_eq2:
kaliszyk@39996
   684
  shows "list_eq2 (a # (removeAll a A)) (if memb a A then A else a # A)"
kaliszyk@36280
   685
  apply (induct A)
kaliszyk@36280
   686
  apply (simp add: memb_def list_eq2_refl)
kaliszyk@36280
   687
  apply (case_tac "memb a (aa # A)")
kaliszyk@36280
   688
  apply (simp_all only: memb_cons_iff)
kaliszyk@36280
   689
  apply (case_tac [!] "a = aa")
kaliszyk@36280
   690
  apply (simp_all)
kaliszyk@36280
   691
  apply (case_tac "memb a A")
kaliszyk@36280
   692
  apply (auto simp add: memb_def)[2]
kaliszyk@36280
   693
  apply (metis list_eq2.intros(3) list_eq2.intros(4) list_eq2.intros(5) list_eq2.intros(6))
kaliszyk@36280
   694
  apply (metis list_eq2.intros(1) list_eq2.intros(5) list_eq2.intros(6))
kaliszyk@39996
   695
  apply (auto simp add: list_eq2_refl memb_def)
kaliszyk@36280
   696
  done
kaliszyk@36280
   697
kaliszyk@36280
   698
lemma memb_delete_list_eq2:
kaliszyk@36280
   699
  assumes a: "memb e r"
kaliszyk@39996
   700
  shows "list_eq2 (e # removeAll e r) r"
kaliszyk@36280
   701
  using a cons_delete_list_eq2[of e r]
kaliszyk@36280
   702
  by simp
kaliszyk@36280
   703
kaliszyk@36280
   704
lemma list_eq2_equiv:
kaliszyk@36280
   705
  "(l \<approx> r) \<longleftrightarrow> (list_eq2 l r)"
kaliszyk@36280
   706
proof
kaliszyk@36280
   707
  show "list_eq2 l r \<Longrightarrow> l \<approx> r" by (induct rule: list_eq2.induct) auto
kaliszyk@36280
   708
next
kaliszyk@36280
   709
  {
kaliszyk@36280
   710
    fix n
kaliszyk@36280
   711
    assume a: "fcard_raw l = n" and b: "l \<approx> r"
kaliszyk@36280
   712
    have "list_eq2 l r"
kaliszyk@36280
   713
      using a b
kaliszyk@36280
   714
    proof (induct n arbitrary: l r)
kaliszyk@36280
   715
      case 0
kaliszyk@36280
   716
      have "fcard_raw l = 0" by fact
kaliszyk@36280
   717
      then have "\<forall>x. \<not> memb x l" using memb_card_not_0[of _ l] by auto
kaliszyk@36280
   718
      then have z: "l = []" using no_memb_nil by auto
kaliszyk@36280
   719
      then have "r = []" using `l \<approx> r` by simp
kaliszyk@36280
   720
      then show ?case using z list_eq2_refl by simp
kaliszyk@36280
   721
    next
kaliszyk@36280
   722
      case (Suc m)
kaliszyk@36280
   723
      have b: "l \<approx> r" by fact
kaliszyk@36280
   724
      have d: "fcard_raw l = Suc m" by fact
kaliszyk@39996
   725
      then have "\<exists>a. memb a l" 
kaliszyk@39996
   726
	apply(simp add: fcard_raw_def memb_def)
kaliszyk@39996
   727
	apply(drule card_eq_SucD)
kaliszyk@39996
   728
	apply(blast)
kaliszyk@39996
   729
	done
kaliszyk@36280
   730
      then obtain a where e: "memb a l" by auto
kaliszyk@39996
   731
      then have e': "memb a r" using list_eq.simps[simplified memb_def[symmetric], of l r] b 
kaliszyk@39996
   732
	unfolding memb_def by auto
kaliszyk@39996
   733
      have f: "fcard_raw (removeAll a l) = m" using fcard_raw_delete[of a l] e d by simp
kaliszyk@39996
   734
      have g: "removeAll a l \<approx> removeAll a r" using removeAll_rsp b by simp
kaliszyk@39996
   735
      have "list_eq2 (removeAll a l) (removeAll a r)" by (rule Suc.hyps[OF f g])
kaliszyk@39996
   736
      then have h: "list_eq2 (a # removeAll a l) (a # removeAll a r)" by (rule list_eq2.intros(5))
kaliszyk@39996
   737
      have i: "list_eq2 l (a # removeAll a l)"
kaliszyk@36280
   738
        by (rule list_eq2.intros(3)[OF memb_delete_list_eq2[OF e]])
kaliszyk@39996
   739
      have "list_eq2 l (a # removeAll a r)" by (rule list_eq2.intros(6)[OF i h])
kaliszyk@36280
   740
      then show ?case using list_eq2.intros(6)[OF _ memb_delete_list_eq2[OF e']] by simp
kaliszyk@36280
   741
    qed
kaliszyk@36280
   742
    }
kaliszyk@36280
   743
  then show "l \<approx> r \<Longrightarrow> list_eq2 l r" by blast
kaliszyk@36280
   744
qed
kaliszyk@36280
   745
kaliszyk@36280
   746
text {* Lifted theorems *}
kaliszyk@36280
   747
kaliszyk@36280
   748
lemma not_fin_fnil: "x |\<notin>| {||}"
urbanc@37634
   749
  by (descending) (simp add: memb_def)
kaliszyk@36280
   750
kaliszyk@36280
   751
lemma fin_finsert_iff[simp]:
urbanc@37634
   752
  "x |\<in>| finsert y S \<longleftrightarrow> x = y \<or> x |\<in>| S"
urbanc@37634
   753
  by (descending) (simp add: memb_def)
kaliszyk@36280
   754
kaliszyk@36280
   755
lemma
kaliszyk@36280
   756
  shows finsertI1: "x |\<in>| finsert x S"
kaliszyk@36280
   757
  and   finsertI2: "x |\<in>| S \<Longrightarrow> x |\<in>| finsert y S"
urbanc@37634
   758
  by (lifting memb_consI1 memb_consI2)
kaliszyk@36280
   759
kaliszyk@36280
   760
lemma finsert_absorb[simp]:
kaliszyk@36280
   761
  shows "x |\<in>| S \<Longrightarrow> finsert x S = S"
urbanc@37634
   762
  by (descending) (auto simp add: memb_def)
kaliszyk@36280
   763
kaliszyk@36280
   764
lemma fempty_not_finsert[simp]:
kaliszyk@36280
   765
  "{||} \<noteq> finsert x S"
kaliszyk@36280
   766
  "finsert x S \<noteq> {||}"
kaliszyk@36280
   767
  by (lifting nil_not_cons)
kaliszyk@36280
   768
kaliszyk@36280
   769
lemma finsert_left_comm:
kaliszyk@36280
   770
  "finsert x (finsert y S) = finsert y (finsert x S)"
urbanc@37634
   771
  by (descending) (auto)
kaliszyk@36280
   772
kaliszyk@36280
   773
lemma finsert_left_idem:
kaliszyk@36280
   774
  "finsert x (finsert x S) = finsert x S"
urbanc@37634
   775
  by (descending) (auto)
kaliszyk@36280
   776
kaliszyk@36280
   777
lemma fsingleton_eq[simp]:
kaliszyk@36280
   778
  shows "{|x|} = {|y|} \<longleftrightarrow> x = y"
urbanc@37634
   779
  by (descending) (auto)
urbanc@37634
   780
kaliszyk@36280
   781
kaliszyk@39996
   782
text {* fset *}
kaliszyk@36280
   783
kaliszyk@39996
   784
lemma fset_simps[simp]:
kaliszyk@39996
   785
  "fset {||} = ({} :: 'a set)"
kaliszyk@39996
   786
  "fset (finsert (h :: 'a) t) = insert h (fset t)"
kaliszyk@36280
   787
  by (lifting set.simps)
kaliszyk@36280
   788
kaliszyk@39996
   789
lemma in_fset:
kaliszyk@39996
   790
  "x \<in> fset S \<equiv> x |\<in>| S"
kaliszyk@36280
   791
  by (lifting memb_def[symmetric])
kaliszyk@36280
   792
kaliszyk@36280
   793
lemma none_fin_fempty:
urbanc@37634
   794
  "(\<forall>x. x |\<notin>| S) \<longleftrightarrow> S = {||}"
kaliszyk@36280
   795
  by (lifting none_memb_nil)
kaliszyk@36280
   796
kaliszyk@36280
   797
lemma fset_cong:
kaliszyk@39996
   798
  "S = T \<longleftrightarrow> fset S = fset T"
kaliszyk@36280
   799
  by (lifting set_cong)
kaliszyk@36280
   800
kaliszyk@39996
   801
kaliszyk@36280
   802
text {* fcard *}
kaliszyk@36280
   803
kaliszyk@36280
   804
lemma fcard_finsert_if [simp]:
kaliszyk@36280
   805
  shows "fcard (finsert x S) = (if x |\<in>| S then fcard S else Suc (fcard S))"
kaliszyk@39996
   806
  by (descending) (auto simp add: fcard_raw_def memb_def insert_absorb)
kaliszyk@36280
   807
kaliszyk@39996
   808
lemma fcard_0[simp]:
kaliszyk@39996
   809
  shows "fcard S = 0 \<longleftrightarrow> S = {||}"
kaliszyk@39996
   810
  by (descending) (simp add: fcard_raw_def)
kaliszyk@39996
   811
kaliszyk@39996
   812
lemma fcard_fempty[simp]:
kaliszyk@39996
   813
  shows "fcard {||} = 0"
kaliszyk@39996
   814
  by (simp add: fcard_0)
kaliszyk@36280
   815
kaliszyk@36280
   816
lemma fcard_1:
urbanc@37634
   817
  shows "fcard S = 1 \<longleftrightarrow> (\<exists>x. S = {|x|})"
kaliszyk@39996
   818
  by (descending) (auto simp add: fcard_raw_def card_Suc_eq)
kaliszyk@36280
   819
kaliszyk@36465
   820
lemma fcard_gt_0:
kaliszyk@39996
   821
  shows "x \<in> fset S \<Longrightarrow> 0 < fcard S"
kaliszyk@39996
   822
  by (descending) (auto simp add: fcard_raw_def card_gt_0_iff)
kaliszyk@39996
   823
  
kaliszyk@36465
   824
lemma fcard_not_fin:
kaliszyk@36280
   825
  shows "(x |\<notin>| S) = (fcard (finsert x S) = Suc (fcard S))"
kaliszyk@39996
   826
  by (descending) (auto simp add: memb_def fcard_raw_def insert_absorb)
kaliszyk@36280
   827
kaliszyk@36280
   828
lemma fcard_suc: "fcard S = Suc n \<Longrightarrow> \<exists>x T. x |\<notin>| T \<and> S = finsert x T \<and> fcard T = n"
kaliszyk@39996
   829
  apply descending
kaliszyk@39996
   830
  apply(simp add: fcard_raw_def memb_def)
kaliszyk@39996
   831
  apply(drule card_eq_SucD)
kaliszyk@39996
   832
  apply(auto)
kaliszyk@39996
   833
  apply(rule_tac x="b" in exI)
kaliszyk@39996
   834
  apply(rule_tac x="removeAll b S" in exI)
kaliszyk@39996
   835
  apply(auto)
kaliszyk@39996
   836
  done
kaliszyk@36280
   837
kaliszyk@36280
   838
lemma fcard_delete:
kaliszyk@39996
   839
  "fcard (fdelete y S) = (if y |\<in>| S then fcard S - 1 else fcard S)"
kaliszyk@36280
   840
  by (lifting fcard_raw_delete)
kaliszyk@36280
   841
kaliszyk@39996
   842
lemma fcard_suc_memb: 
kaliszyk@39996
   843
  shows "fcard A = Suc n \<Longrightarrow> \<exists>a. a |\<in>| A"
kaliszyk@39996
   844
  apply(descending)
kaliszyk@39996
   845
  apply(simp add: fcard_raw_def memb_def)
kaliszyk@39996
   846
  apply(drule card_eq_SucD)
kaliszyk@39996
   847
  apply(auto)
kaliszyk@39996
   848
  done
kaliszyk@36280
   849
kaliszyk@39996
   850
lemma fin_fcard_not_0: 
kaliszyk@39996
   851
  shows "a |\<in>| A \<Longrightarrow> fcard A \<noteq> 0"
kaliszyk@39996
   852
  by (descending) (auto simp add: fcard_raw_def memb_def)
kaliszyk@39996
   853
kaliszyk@36280
   854
kaliszyk@36280
   855
text {* funion *}
kaliszyk@36280
   856
kaliszyk@36352
   857
lemmas [simp] =
kaliszyk@36465
   858
  sup_bot_left[where 'a="'a fset", standard]
kaliszyk@36465
   859
  sup_bot_right[where 'a="'a fset", standard]
kaliszyk@36280
   860
kaliszyk@36352
   861
lemma funion_finsert[simp]:
kaliszyk@36352
   862
  shows "finsert x S |\<union>| T = finsert x (S |\<union>| T)"
kaliszyk@36352
   863
  by (lifting append.simps(2))
kaliszyk@36280
   864
kaliszyk@36280
   865
lemma singleton_union_left:
urbanc@37634
   866
  shows "{|a|} |\<union>| S = finsert a S"
kaliszyk@36280
   867
  by simp
kaliszyk@36280
   868
kaliszyk@36280
   869
lemma singleton_union_right:
urbanc@37634
   870
  shows "S |\<union>| {|a|} = finsert a S"
kaliszyk@36280
   871
  by (subst sup.commute) simp
kaliszyk@36280
   872
kaliszyk@39994
   873
kaliszyk@39994
   874
section {* Induction and Cases rules for fsets *}
kaliszyk@36280
   875
kaliszyk@36280
   876
lemma fset_strong_cases:
kaliszyk@36465
   877
  obtains "xs = {||}"
kaliszyk@36465
   878
    | x ys where "x |\<notin>| ys" and "xs = finsert x ys"
kaliszyk@36280
   879
  by (lifting fset_raw_strong_cases)
kaliszyk@36280
   880
kaliszyk@36280
   881
lemma fset_exhaust[case_names fempty finsert, cases type: fset]:
kaliszyk@36280
   882
  shows "\<lbrakk>S = {||} \<Longrightarrow> P; \<And>x S'. S = finsert x S' \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
kaliszyk@36280
   883
  by (lifting list.exhaust)
kaliszyk@36280
   884
kaliszyk@36280
   885
lemma fset_induct_weak[case_names fempty finsert]:
kaliszyk@36280
   886
  shows "\<lbrakk>P {||}; \<And>x S. P S \<Longrightarrow> P (finsert x S)\<rbrakk> \<Longrightarrow> P S"
kaliszyk@36280
   887
  by (lifting list.induct)
kaliszyk@36280
   888
kaliszyk@36280
   889
lemma fset_induct[case_names fempty finsert, induct type: fset]:
kaliszyk@36465
   890
  assumes prem1: "P {||}"
kaliszyk@36280
   891
  and     prem2: "\<And>x S. \<lbrakk>x |\<notin>| S; P S\<rbrakk> \<Longrightarrow> P (finsert x S)"
kaliszyk@36280
   892
  shows "P S"
kaliszyk@36280
   893
proof(induct S rule: fset_induct_weak)
kaliszyk@36280
   894
  case fempty
kaliszyk@36280
   895
  show "P {||}" by (rule prem1)
kaliszyk@36280
   896
next
kaliszyk@36280
   897
  case (finsert x S)
kaliszyk@36280
   898
  have asm: "P S" by fact
kaliszyk@36280
   899
  show "P (finsert x S)"
kaliszyk@36280
   900
    by (cases "x |\<in>| S") (simp_all add: asm prem2)
kaliszyk@36280
   901
qed
kaliszyk@36280
   902
kaliszyk@36280
   903
lemma fset_induct2:
kaliszyk@36280
   904
  "P {||} {||} \<Longrightarrow>
kaliszyk@36280
   905
  (\<And>x xs. x |\<notin>| xs \<Longrightarrow> P (finsert x xs) {||}) \<Longrightarrow>
kaliszyk@36280
   906
  (\<And>y ys. y |\<notin>| ys \<Longrightarrow> P {||} (finsert y ys)) \<Longrightarrow>
kaliszyk@36280
   907
  (\<And>x xs y ys. \<lbrakk>P xs ys; x |\<notin>| xs; y |\<notin>| ys\<rbrakk> \<Longrightarrow> P (finsert x xs) (finsert y ys)) \<Longrightarrow>
kaliszyk@36280
   908
  P xsa ysa"
kaliszyk@36280
   909
  apply (induct xsa arbitrary: ysa)
kaliszyk@36280
   910
  apply (induct_tac x rule: fset_induct)
kaliszyk@36280
   911
  apply simp_all
kaliszyk@36280
   912
  apply (induct_tac xa rule: fset_induct)
kaliszyk@36280
   913
  apply simp_all
kaliszyk@36280
   914
  done
kaliszyk@36280
   915
kaliszyk@36675
   916
lemma fset_fcard_induct:
kaliszyk@36675
   917
  assumes a: "P {||}"
kaliszyk@36675
   918
  and     b: "\<And>xs ys. Suc (fcard xs) = (fcard ys) \<Longrightarrow> P xs \<Longrightarrow> P ys"
kaliszyk@36675
   919
  shows "P zs"
kaliszyk@36675
   920
proof (induct zs)
kaliszyk@36675
   921
  show "P {||}" by (rule a)
kaliszyk@36675
   922
next
kaliszyk@36675
   923
  fix x :: 'a and zs :: "'a fset"
kaliszyk@36675
   924
  assume h: "P zs"
kaliszyk@36675
   925
  assume "x |\<notin>| zs"
kaliszyk@36675
   926
  then have H1: "Suc (fcard zs) = fcard (finsert x zs)" using fcard_suc by auto
kaliszyk@36675
   927
  then show "P (finsert x zs)" using b h by simp
kaliszyk@36675
   928
qed
kaliszyk@36675
   929
kaliszyk@36280
   930
text {* fmap *}
kaliszyk@36280
   931
kaliszyk@36280
   932
lemma fmap_simps[simp]:
urbanc@37634
   933
  fixes f::"'a \<Rightarrow> 'b"
urbanc@37634
   934
  shows "fmap f {||} = {||}"
urbanc@37634
   935
  and   "fmap f (finsert x S) = finsert (f x) (fmap f S)"
kaliszyk@36280
   936
  by (lifting map.simps)
kaliszyk@36280
   937
kaliszyk@36280
   938
lemma fmap_set_image:
kaliszyk@39996
   939
  "fset (fmap f S) = f ` (fset S)"
kaliszyk@36646
   940
  by (induct S) simp_all
kaliszyk@36280
   941
kaliszyk@36280
   942
lemma inj_fmap_eq_iff:
urbanc@37634
   943
  "inj f \<Longrightarrow> fmap f S = fmap f T \<longleftrightarrow> S = T"
kaliszyk@36280
   944
  by (lifting inj_map_eq_iff)
kaliszyk@36280
   945
urbanc@37634
   946
lemma fmap_funion: 
urbanc@37634
   947
  shows "fmap f (S |\<union>| T) = fmap f S |\<union>| fmap f T"
kaliszyk@36280
   948
  by (lifting map_append)
kaliszyk@36280
   949
kaliszyk@36280
   950
lemma fin_funion:
urbanc@37634
   951
  shows "x |\<in>| S |\<union>| T \<longleftrightarrow> x |\<in>| S \<or> x |\<in>| T"
kaliszyk@36280
   952
  by (lifting memb_append)
kaliszyk@36280
   953
kaliszyk@39996
   954
kaliszyk@39996
   955
section {* fset *}
kaliszyk@36646
   956
urbanc@37634
   957
lemma fin_set: 
kaliszyk@39996
   958
  shows "x |\<in>| xs \<longleftrightarrow> x \<in> fset xs"
kaliszyk@39996
   959
  by (lifting memb_def)
kaliszyk@36646
   960
urbanc@37634
   961
lemma fnotin_set: 
kaliszyk@39996
   962
  shows "x |\<notin>| xs \<longleftrightarrow> x \<notin> fset xs"
kaliszyk@36646
   963
  by (simp add: fin_set)
kaliszyk@36646
   964
urbanc@37634
   965
lemma fcard_set: 
kaliszyk@39996
   966
  shows "fcard xs = card (fset xs)"
kaliszyk@39996
   967
  by (lifting fcard_raw_def)
kaliszyk@36646
   968
urbanc@37634
   969
lemma fsubseteq_set: 
kaliszyk@39996
   970
  shows "xs |\<subseteq>| ys \<longleftrightarrow> fset xs \<subseteq> fset ys"
kaliszyk@39996
   971
  by (lifting sub_list_def)
kaliszyk@36646
   972
urbanc@37634
   973
lemma fsubset_set: 
kaliszyk@39996
   974
  shows "xs |\<subset>| ys \<longleftrightarrow> fset xs \<subset> fset ys"
kaliszyk@39996
   975
  unfolding less_fset_def 
kaliszyk@39996
   976
  by (descending) (auto simp add: sub_list_def)
kaliszyk@36646
   977
kaliszyk@39996
   978
lemma ffilter_set [simp]: 
kaliszyk@39996
   979
  shows "fset (ffilter P xs) = P \<inter> fset xs"
kaliszyk@39996
   980
  by (descending) (auto simp add: mem_def)
kaliszyk@36646
   981
kaliszyk@39996
   982
lemma fdelete_set [simp]: 
kaliszyk@39996
   983
  shows "fset (fdelete x xs) = fset xs - {x}"
kaliszyk@39996
   984
  by (lifting set_removeAll)
kaliszyk@36646
   985
kaliszyk@39996
   986
lemma finter_set [simp]: 
kaliszyk@39996
   987
  shows "fset (xs |\<inter>| ys) = fset xs \<inter> fset ys"
kaliszyk@39996
   988
  by (lifting set_finter_raw)
kaliszyk@36646
   989
kaliszyk@39996
   990
lemma funion_set [simp]: 
kaliszyk@39996
   991
  shows "fset (xs |\<union>| ys) = fset xs \<union> fset ys"
kaliszyk@36646
   992
  by (lifting set_append)
kaliszyk@36646
   993
kaliszyk@39996
   994
lemma fminus_set [simp]: 
kaliszyk@39996
   995
  shows "fset (xs - ys) = fset xs - fset ys"
kaliszyk@39996
   996
  by (lifting set_fminus_raw)
kaliszyk@36675
   997
kaliszyk@36646
   998
lemmas fset_to_set_trans =
kaliszyk@36646
   999
  fin_set fnotin_set fcard_set fsubseteq_set fsubset_set
kaliszyk@39996
  1000
  finter_set funion_set ffilter_set fset_simps
kaliszyk@36675
  1001
  fset_cong fdelete_set fmap_set_image fminus_set
kaliszyk@36675
  1002
kaliszyk@36646
  1003
kaliszyk@36280
  1004
text {* ffold *}
kaliszyk@36280
  1005
kaliszyk@39996
  1006
lemma ffold_nil: 
kaliszyk@39996
  1007
  shows "ffold f z {||} = z"
kaliszyk@36280
  1008
  by (lifting ffold_raw.simps(1)[where 'a="'b" and 'b="'a"])
kaliszyk@36280
  1009
kaliszyk@36280
  1010
lemma ffold_finsert: "ffold f z (finsert a A) =
kaliszyk@36280
  1011
  (if rsp_fold f then if a |\<in>| A then ffold f z A else f a (ffold f z A) else z)"
kaliszyk@39996
  1012
  by (descending) (simp add: memb_def)
kaliszyk@36280
  1013
kaliszyk@36280
  1014
lemma fin_commute_ffold:
kaliszyk@39996
  1015
  "\<lbrakk>rsp_fold f; h |\<in>| b\<rbrakk> \<Longrightarrow> ffold f z b = f h (ffold f z (fdelete h b))"
kaliszyk@39996
  1016
  by (descending) (simp add: memb_def memb_commute_ffold_raw)
kaliszyk@39996
  1017
kaliszyk@36280
  1018
kaliszyk@36280
  1019
text {* fdelete *}
kaliszyk@36280
  1020
kaliszyk@36465
  1021
lemma fin_fdelete:
kaliszyk@39996
  1022
  shows "x |\<in>| fdelete y S \<longleftrightarrow> x |\<in>| S \<and> x \<noteq> y"
kaliszyk@39996
  1023
  by (descending) (simp add: memb_def)
kaliszyk@36280
  1024
kaliszyk@39996
  1025
lemma fnotin_fdelete:
kaliszyk@39996
  1026
  shows "x |\<notin>| fdelete x S"
kaliszyk@39996
  1027
  by (descending) (simp add: memb_def)
kaliszyk@36280
  1028
kaliszyk@39996
  1029
lemma fnotin_fdelete_ident:
kaliszyk@39996
  1030
  shows "x |\<notin>| S \<Longrightarrow> fdelete x S = S"
kaliszyk@39996
  1031
  by (descending) (simp add: memb_def)
kaliszyk@36280
  1032
kaliszyk@36280
  1033
lemma fset_fdelete_cases:
kaliszyk@39996
  1034
  shows "S = {||} \<or> (\<exists>x. x |\<in>| S \<and> S = finsert x (fdelete x S))"
kaliszyk@39996
  1035
  by (lifting fset_raw_removeAll_cases)
kaliszyk@36280
  1036
urbanc@37634
  1037
text {* finite intersection *}
kaliszyk@36280
  1038
kaliszyk@39996
  1039
lemma finter_empty_l:
urbanc@37634
  1040
  shows "{||} |\<inter>| S = {||}"
urbanc@37634
  1041
  by simp
kaliszyk@36280
  1042
urbanc@37634
  1043
kaliszyk@39996
  1044
lemma finter_empty_r:
urbanc@37634
  1045
  shows "S |\<inter>| {||} = {||}"
urbanc@37634
  1046
  by simp
kaliszyk@36280
  1047
kaliszyk@36280
  1048
lemma finter_finsert:
kaliszyk@39996
  1049
  shows "finsert x S |\<inter>| T = (if x |\<in>| T then finsert x (S |\<inter>| T) else S |\<inter>| T)"
kaliszyk@39996
  1050
  by (descending) (simp add: memb_def)
kaliszyk@36280
  1051
kaliszyk@36280
  1052
lemma fin_finter:
kaliszyk@39996
  1053
  shows "x |\<in>| (S |\<inter>| T) \<longleftrightarrow> x |\<in>| S \<and> x |\<in>| T"
kaliszyk@39996
  1054
  by (descending) (simp add: memb_def)
kaliszyk@36280
  1055
kaliszyk@36280
  1056
lemma fsubset_finsert:
urbanc@37634
  1057
  shows "finsert x xs |\<subseteq>| ys \<longleftrightarrow> x |\<in>| ys \<and> xs |\<subseteq>| ys"
kaliszyk@36280
  1058
  by (lifting sub_list_cons)
kaliszyk@36280
  1059
urbanc@37634
  1060
lemma 
urbanc@37634
  1061
  shows "xs |\<subseteq>| ys \<equiv> \<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys"
kaliszyk@39996
  1062
  by (descending) (auto simp add: sub_list_def memb_def)
kaliszyk@36280
  1063
urbanc@37634
  1064
lemma fsubset_fin: 
urbanc@37634
  1065
  shows "xs |\<subseteq>| ys = (\<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys)"
kaliszyk@39996
  1066
  by (descending) (auto simp add: sub_list_def memb_def)
kaliszyk@36280
  1067
urbanc@37634
  1068
lemma fminus_fin: 
urbanc@37634
  1069
  shows "x |\<in>| xs - ys \<longleftrightarrow> x |\<in>| xs \<and> x |\<notin>| ys"
kaliszyk@39996
  1070
  by (descending) (simp add: memb_def)
kaliszyk@36675
  1071
urbanc@37634
  1072
lemma fminus_red: 
urbanc@37634
  1073
  shows "finsert x xs - ys = (if x |\<in>| ys then xs - ys else finsert x (xs - ys))"
kaliszyk@39996
  1074
  by (descending) (auto simp add: memb_def)
kaliszyk@36675
  1075
urbanc@37634
  1076
lemma fminus_red_fin [simp]: 
urbanc@37634
  1077
  shows "x |\<in>| ys \<Longrightarrow> finsert x xs - ys = xs - ys"
kaliszyk@36675
  1078
  by (simp add: fminus_red)
kaliszyk@36675
  1079
urbanc@37634
  1080
lemma fminus_red_fnotin[simp]: 
urbanc@37634
  1081
  shows "x |\<notin>| ys \<Longrightarrow> finsert x xs - ys = finsert x (xs - ys)"
kaliszyk@36675
  1082
  by (simp add: fminus_red)
kaliszyk@36675
  1083
kaliszyk@39996
  1084
lemma fset_eq_iff:
urbanc@37634
  1085
  shows "S = T \<longleftrightarrow> (\<forall>x. (x |\<in>| S) = (x |\<in>| T))"
kaliszyk@39995
  1086
  by (descending) (auto simp add: memb_def)
kaliszyk@36280
  1087
kaliszyk@36280
  1088
(* We cannot write it as "assumes .. shows" since Isabelle changes
kaliszyk@36280
  1089
   the quantifiers to schematic variables and reintroduces them in
kaliszyk@36280
  1090
   a different order *)
kaliszyk@36280
  1091
lemma fset_eq_cases:
kaliszyk@36280
  1092
 "\<lbrakk>a1 = a2;
kaliszyk@36280
  1093
   \<And>a b xs. \<lbrakk>a1 = finsert a (finsert b xs); a2 = finsert b (finsert a xs)\<rbrakk> \<Longrightarrow> P;
kaliszyk@36280
  1094
   \<lbrakk>a1 = {||}; a2 = {||}\<rbrakk> \<Longrightarrow> P; \<And>xs ys. \<lbrakk>a1 = ys; a2 = xs; xs = ys\<rbrakk> \<Longrightarrow> P;
kaliszyk@36280
  1095
   \<And>a xs. \<lbrakk>a1 = finsert a (finsert a xs); a2 = finsert a xs\<rbrakk> \<Longrightarrow> P;
kaliszyk@36280
  1096
   \<And>xs ys a. \<lbrakk>a1 = finsert a xs; a2 = finsert a ys; xs = ys\<rbrakk> \<Longrightarrow> P;
kaliszyk@36280
  1097
   \<And>xs1 xs2 xs3. \<lbrakk>a1 = xs1; a2 = xs3; xs1 = xs2; xs2 = xs3\<rbrakk> \<Longrightarrow> P\<rbrakk>
kaliszyk@36280
  1098
  \<Longrightarrow> P"
kaliszyk@36280
  1099
  by (lifting list_eq2.cases[simplified list_eq2_equiv[symmetric]])
kaliszyk@36280
  1100
kaliszyk@36280
  1101
lemma fset_eq_induct:
kaliszyk@36280
  1102
  assumes "x1 = x2"
kaliszyk@36280
  1103
  and "\<And>a b xs. P (finsert a (finsert b xs)) (finsert b (finsert a xs))"
kaliszyk@36280
  1104
  and "P {||} {||}"
kaliszyk@36280
  1105
  and "\<And>xs ys. \<lbrakk>xs = ys; P xs ys\<rbrakk> \<Longrightarrow> P ys xs"
kaliszyk@36280
  1106
  and "\<And>a xs. P (finsert a (finsert a xs)) (finsert a xs)"
kaliszyk@36280
  1107
  and "\<And>xs ys a. \<lbrakk>xs = ys; P xs ys\<rbrakk> \<Longrightarrow> P (finsert a xs) (finsert a ys)"
kaliszyk@36280
  1108
  and "\<And>xs1 xs2 xs3. \<lbrakk>xs1 = xs2; P xs1 xs2; xs2 = xs3; P xs2 xs3\<rbrakk> \<Longrightarrow> P xs1 xs3"
kaliszyk@36280
  1109
  shows "P x1 x2"
kaliszyk@36280
  1110
  using assms
kaliszyk@36280
  1111
  by (lifting list_eq2.induct[simplified list_eq2_equiv[symmetric]])
kaliszyk@36280
  1112
urbanc@37634
  1113
section {* fconcat *}
kaliszyk@36280
  1114
kaliszyk@36280
  1115
lemma fconcat_empty:
kaliszyk@36280
  1116
  shows "fconcat {||} = {||}"
kaliszyk@36280
  1117
  by (lifting concat.simps(1))
kaliszyk@36280
  1118
kaliszyk@36280
  1119
lemma fconcat_insert:
kaliszyk@36280
  1120
  shows "fconcat (finsert x S) = x |\<union>| fconcat S"
kaliszyk@36280
  1121
  by (lifting concat.simps(2))
kaliszyk@36280
  1122
urbanc@37634
  1123
lemma 
urbanc@37634
  1124
  shows "fconcat (xs |\<union>| ys) = fconcat xs |\<union>| fconcat ys"
kaliszyk@36280
  1125
  by (lifting concat_append)
kaliszyk@36280
  1126
urbanc@37634
  1127
urbanc@37634
  1128
section {* ffilter *}
bulwahn@36639
  1129
urbanc@37634
  1130
lemma subseteq_filter: 
urbanc@37634
  1131
  shows "ffilter P xs <= ffilter Q xs = (\<forall> x. x |\<in>| xs \<longrightarrow> P x \<longrightarrow> Q x)"
kaliszyk@39994
  1132
  by  (descending) (auto simp add: memb_def sub_list_def)
bulwahn@36639
  1133
urbanc@37634
  1134
lemma eq_ffilter: 
urbanc@37634
  1135
  shows "(ffilter P xs = ffilter Q xs) = (\<forall>x. x |\<in>| xs \<longrightarrow> P x = Q x)"
kaliszyk@39994
  1136
  by (descending) (auto simp add: memb_def)
bulwahn@36639
  1137
kaliszyk@39995
  1138
lemma subset_ffilter:
urbanc@37634
  1139
  shows "(\<And>x. x |\<in>| xs \<Longrightarrow> P x \<Longrightarrow> Q x) \<Longrightarrow> (x |\<in>| xs & \<not> P x & Q x) \<Longrightarrow> ffilter P xs < ffilter Q xs"
kaliszyk@39995
  1140
  unfolding less_fset_def by (auto simp add: subseteq_filter eq_ffilter)
kaliszyk@39995
  1141
bulwahn@36639
  1142
bulwahn@36639
  1143
section {* lemmas transferred from Finite_Set theory *}
bulwahn@36639
  1144
bulwahn@36639
  1145
text {* finiteness for finite sets holds *}
kaliszyk@39994
  1146
lemma finite_fset [simp]: 
kaliszyk@39996
  1147
  shows "finite (fset S)"
kaliszyk@36646
  1148
  by (induct S) auto
bulwahn@36639
  1149
urbanc@37634
  1150
lemma fset_choice: 
urbanc@37634
  1151
  shows "\<forall>x. x |\<in>| A \<longrightarrow> (\<exists>y. P x y) \<Longrightarrow> \<exists>f. \<forall>x. x |\<in>| A \<longrightarrow> P x (f x)"
kaliszyk@36646
  1152
  unfolding fset_to_set_trans
kaliszyk@36646
  1153
  by (rule finite_set_choice[simplified Ball_def, OF finite_fset])
bulwahn@36639
  1154
kaliszyk@39996
  1155
lemma fsubseteq_fempty:
urbanc@37634
  1156
  shows "xs |\<subseteq>| {||} \<longleftrightarrow> xs = {||}"
kaliszyk@39996
  1157
  by (metis finter_empty_r le_iff_inf)
kaliszyk@36646
  1158
urbanc@37634
  1159
lemma not_fsubset_fnil: 
urbanc@37634
  1160
  shows "\<not> xs |\<subset>| {||}"
kaliszyk@39996
  1161
  by (metis fset_simps(1) fsubset_set not_psubset_empty)
kaliszyk@39996
  1162
  
urbanc@37634
  1163
lemma fcard_mono: 
urbanc@37634
  1164
  shows "xs |\<subseteq>| ys \<Longrightarrow> fcard xs \<le> fcard ys"
kaliszyk@36646
  1165
  unfolding fset_to_set_trans
kaliszyk@36646
  1166
  by (rule card_mono[OF finite_fset])
bulwahn@36639
  1167
urbanc@37634
  1168
lemma fcard_fseteq: 
urbanc@37634
  1169
  shows "xs |\<subseteq>| ys \<Longrightarrow> fcard ys \<le> fcard xs \<Longrightarrow> xs = ys"
kaliszyk@39996
  1170
  unfolding fcard_set fsubseteq_set
kaliszyk@39996
  1171
  by (simp add: card_seteq[OF finite_fset] fset_cong)
kaliszyk@36646
  1172
urbanc@37634
  1173
lemma psubset_fcard_mono: 
urbanc@37634
  1174
  shows "xs |\<subset>| ys \<Longrightarrow> fcard xs < fcard ys"
kaliszyk@36646
  1175
  unfolding fset_to_set_trans
kaliszyk@36646
  1176
  by (rule psubset_card_mono[OF finite_fset])
kaliszyk@36646
  1177
urbanc@37634
  1178
lemma fcard_funion_finter: 
urbanc@37634
  1179
  shows "fcard xs + fcard ys = fcard (xs |\<union>| ys) + fcard (xs |\<inter>| ys)"
kaliszyk@36646
  1180
  unfolding fset_to_set_trans
kaliszyk@36646
  1181
  by (rule card_Un_Int[OF finite_fset finite_fset])
kaliszyk@36646
  1182
urbanc@37634
  1183
lemma fcard_funion_disjoint: 
urbanc@37634
  1184
  shows "xs |\<inter>| ys = {||} \<Longrightarrow> fcard (xs |\<union>| ys) = fcard xs + fcard ys"
kaliszyk@36646
  1185
  unfolding fset_to_set_trans
kaliszyk@36646
  1186
  by (rule card_Un_disjoint[OF finite_fset finite_fset])
bulwahn@36639
  1187
urbanc@37634
  1188
lemma fcard_delete1_less: 
kaliszyk@39996
  1189
  shows "x |\<in>| xs \<Longrightarrow> fcard (fdelete x xs) < fcard xs"
kaliszyk@36646
  1190
  unfolding fset_to_set_trans
kaliszyk@36646
  1191
  by (rule card_Diff1_less[OF finite_fset])
kaliszyk@36646
  1192
urbanc@37634
  1193
lemma fcard_delete2_less: 
kaliszyk@39996
  1194
  shows "x |\<in>| xs \<Longrightarrow> y |\<in>| xs \<Longrightarrow> fcard (fdelete y (fdelete x xs)) < fcard xs"
kaliszyk@36646
  1195
  unfolding fset_to_set_trans
kaliszyk@36646
  1196
  by (rule card_Diff2_less[OF finite_fset])
bulwahn@36639
  1197
urbanc@37634
  1198
lemma fcard_delete1_le: 
kaliszyk@39996
  1199
  shows "fcard (fdelete x xs) \<le> fcard xs"
kaliszyk@36646
  1200
  unfolding fset_to_set_trans
kaliszyk@36646
  1201
  by (rule card_Diff1_le[OF finite_fset])
kaliszyk@36646
  1202
urbanc@37634
  1203
lemma fcard_psubset: 
urbanc@37634
  1204
  shows "ys |\<subseteq>| xs \<Longrightarrow> fcard ys < fcard xs \<Longrightarrow> ys |\<subset>| xs"
kaliszyk@36646
  1205
  unfolding fset_to_set_trans
kaliszyk@36646
  1206
  by (rule card_psubset[OF finite_fset])
kaliszyk@36646
  1207
urbanc@37634
  1208
lemma fcard_fmap_le: 
urbanc@37634
  1209
  shows "fcard (fmap f xs) \<le> fcard xs"
kaliszyk@36646
  1210
  unfolding fset_to_set_trans
kaliszyk@36646
  1211
  by (rule card_image_le[OF finite_fset])
bulwahn@36639
  1212
urbanc@37634
  1213
lemma fin_fminus_fnotin: 
urbanc@37634
  1214
  shows "x |\<in>| F - S \<Longrightarrow> x |\<notin>| S"
kaliszyk@36675
  1215
  unfolding fset_to_set_trans
kaliszyk@36675
  1216
  by blast
kaliszyk@36675
  1217
urbanc@37634
  1218
lemma fin_fnotin_fminus: 
urbanc@37634
  1219
  shows "x |\<in>| S \<Longrightarrow> x |\<notin>| F - S"
kaliszyk@36675
  1220
  unfolding fset_to_set_trans
kaliszyk@36675
  1221
  by blast
kaliszyk@36675
  1222
kaliszyk@39996
  1223
lemma fin_mdef: 
kaliszyk@39996
  1224
  "x |\<in>| F \<longleftrightarrow> x |\<notin>| (F - {|x|}) \<and> F = finsert x (F - {|x|})"
kaliszyk@36675
  1225
  unfolding fset_to_set_trans
kaliszyk@36675
  1226
  by blast
kaliszyk@36675
  1227
kaliszyk@36675
  1228
lemma fcard_fminus_finsert[simp]:
kaliszyk@36675
  1229
  assumes "a |\<in>| A" and "a |\<notin>| B"
kaliszyk@36675
  1230
  shows "fcard(A - finsert a B) = fcard(A - B) - 1"
kaliszyk@39996
  1231
  using assms 
kaliszyk@39996
  1232
  unfolding fset_to_set_trans
kaliszyk@36675
  1233
  by (rule card_Diff_insert[OF finite_fset])
kaliszyk@36675
  1234
kaliszyk@36675
  1235
lemma fcard_fminus_fsubset:
kaliszyk@36675
  1236
  assumes "B |\<subseteq>| A"
kaliszyk@36675
  1237
  shows "fcard (A - B) = fcard A - fcard B"
kaliszyk@36675
  1238
  using assms unfolding fset_to_set_trans
kaliszyk@36675
  1239
  by (rule card_Diff_subset[OF finite_fset])
kaliszyk@36675
  1240
kaliszyk@36675
  1241
lemma fcard_fminus_subset_finter:
kaliszyk@39996
  1242
  shows "fcard (A - B) = fcard A - fcard (A |\<inter>| B)"
kaliszyk@36675
  1243
  unfolding fset_to_set_trans
urbanc@37634
  1244
  by (rule card_Diff_subset_Int) (fold finter_set, rule finite_fset)
kaliszyk@36675
  1245
kaliszyk@36675
  1246
kaliszyk@36280
  1247
ML {*
kaliszyk@36465
  1248
fun dest_fsetT (Type (@{type_name fset}, [T])) = T
kaliszyk@36280
  1249
  | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
kaliszyk@36280
  1250
*}
kaliszyk@36280
  1251
kaliszyk@36280
  1252
no_notation
kaliszyk@36280
  1253
  list_eq (infix "\<approx>" 50)
kaliszyk@36280
  1254
kaliszyk@36280
  1255
end