Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/FSet.thy
changeset 1935 266abc3ee228
parent 1927 6c5e3ac737d9
child 1936 99367d481f78
equal deleted inserted replaced
1934:8f6e68dc6cbc 1935:266abc3ee228 
    68 | "ffold_raw f z (a # A) =
 
    68 | "ffold_raw f z (a # A) =
 
    69      (if (rsp_fold f) then
 
    69      (if (rsp_fold f) then
 
    70        if memb a A then ffold_raw f z A
 
    70        if memb a A then ffold_raw f z A
 
    71        else f a (ffold_raw f z A)
 
    71        else f a (ffold_raw f z A)
 
    72      else z)"
 
    72      else z)"
 
       
    73 
       
    74 text {* Composition Quotient *}
 
       
    75 
       
    76 lemma compose_list_refl:
 
       
    77   shows "(list_rel op \<approx> OOO op \<approx>) r r"
 
       
    78 proof
 
       
    79   show c: "list_rel op \<approx> r r" by (rule list_rel_refl) (metis equivp_def fset_equivp)
 
       
    80   have d: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp])
 
       
    81   show b: "(op \<approx> OO list_rel op \<approx>) r r" by (rule pred_compI) (rule d, rule c)
 
       
    82 qed
 
       
    83 
       
    84 lemma list_rel_refl:
 
       
    85   shows "(list_rel op \<approx>) r r"
 
       
    86   by (rule list_rel_refl)(metis equivp_def fset_equivp)
 
       
    87 
       
    88 lemma Quotient_fset_list:
 
       
    89   shows "Quotient (list_rel op \<approx>) (map abs_fset) (map rep_fset)"
 
       
    90   by (fact list_quotient[OF Quotient_fset])
 
       
    91 
       
    92 lemma set_in_eq: "(\<forall>e. ((e \<in> A) \<longleftrightarrow> (e \<in> B))) \<equiv> A = B"
 
       
    93   by (rule eq_reflection) auto
 
       
    94 
       
    95 lemma map_rel_cong: "b \<approx> ba \<Longrightarrow> map f b \<approx> map f ba"
 
       
    96   unfolding list_eq.simps
 
       
    97   by (simp only: set_map set_in_eq)
 
       
    98 
       
    99 lemma quotient_compose_list[quot_thm]:
 
       
   100   shows  "Quotient ((list_rel op \<approx>) OOO (op \<approx>))
 
       
   101     (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)"
 
       
   102   unfolding Quotient_def comp_def
 
       
   103 proof (intro conjI allI)
 
       
   104   fix a r s
 
       
   105   show "abs_fset (map abs_fset (map rep_fset (rep_fset a))) = a"
 
       
   106     by (simp add: abs_o_rep[OF Quotient_fset] Quotient_abs_rep[OF Quotient_fset] map_id)
 
       
   107   have b: "list_rel op \<approx> (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
 
       
   108     by (rule list_rel_refl)
 
       
   109   have c: "(op \<approx> OO list_rel op \<approx>) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
 
       
   110     by (rule, rule equivp_reflp[OF fset_equivp]) (rule b)
 
       
   111   show "(list_rel op \<approx> OOO op \<approx>) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
 
       
   112     by (rule, rule list_rel_refl) (rule c)
 
       
   113   show "(list_rel op \<approx> OOO op \<approx>) r s = ((list_rel op \<approx> OOO op \<approx>) r r \<and>
 
       
   114         (list_rel op \<approx> OOO op \<approx>) s s \<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s))"
 
       
   115   proof (intro iffI conjI)
 
       
   116     show "(list_rel op \<approx> OOO op \<approx>) r r" by (rule compose_list_refl)
 
       
   117     show "(list_rel op \<approx> OOO op \<approx>) s s" by (rule compose_list_refl)
 
       
   118   next
 
       
   119     assume a: "(list_rel op \<approx> OOO op \<approx>) r s"
 
       
   120     then have b: "map abs_fset r \<approx> map abs_fset s" proof (elim pred_compE)
 
       
   121       fix b ba
 
       
   122       assume c: "list_rel op \<approx> r b"
 
       
   123       assume d: "b \<approx> ba"
 
       
   124       assume e: "list_rel op \<approx> ba s"
 
       
   125       have f: "map abs_fset r = map abs_fset b"
 
       
   126         by (metis Quotient_rel[OF Quotient_fset_list] c)
 
       
   127       have g: "map abs_fset s = map abs_fset ba"
 
       
   128         by (metis Quotient_rel[OF Quotient_fset_list] e)
 
       
   129       show "map abs_fset r \<approx> map abs_fset s" using d f g map_rel_cong by simp
 
       
   130     qed
 
       
   131     then show "abs_fset (map abs_fset r) = abs_fset (map abs_fset s)"
 
       
   132       by (metis Quotient_rel[OF Quotient_fset])
 
       
   133   next
 
       
   134     assume a: "(list_rel op \<approx> OOO op \<approx>) r r \<and> (list_rel op \<approx> OOO op \<approx>) s s
 
       
   135       \<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s)"
 
       
   136     then have s: "(list_rel op \<approx> OOO op \<approx>) s s" by simp
 
       
   137     have d: "map abs_fset r \<approx> map abs_fset s"
 
       
   138       by (subst Quotient_rel[OF Quotient_fset]) (simp add: a)
 
       
   139     have b: "map rep_fset (map abs_fset r) \<approx> map rep_fset (map abs_fset s)"
 
       
   140       by (rule map_rel_cong[OF d])
 
       
   141     have y: "list_rel op \<approx> (map rep_fset (map abs_fset s)) s"
 
       
   142       by (fact rep_abs_rsp_left[OF Quotient_fset_list, OF list_rel_refl[of s]])
 
       
   143     have c: "(op \<approx> OO list_rel op \<approx>) (map rep_fset (map abs_fset r)) s"
 
       
   144       by (rule pred_compI) (rule b, rule y)
 
       
   145     have z: "list_rel op \<approx> r (map rep_fset (map abs_fset r))"
 
       
   146       by (fact rep_abs_rsp[OF Quotient_fset_list, OF list_rel_refl[of r]])
 
       
   147     then show "(list_rel op \<approx> OOO op \<approx>) r s"
 
       
   148       using a c pred_compI by simp
 
       
   149   qed
 
       
   150 qed
 
    73 
   151 
    74 text {* Respectfullness *}
 
   152 text {* Respectfullness *}
 
    75 
   153 
    76 lemma [quot_respect]:
 
   154 lemma [quot_respect]:
 
    77   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
 
   155   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
 
   214   done
 
   292   done
 
   215 
   293 
   216 lemma [quot_respect]:
 
   294 lemma [quot_respect]:
 
   217   "(op = ===> op = ===> op \<approx> ===> op =) ffold_raw ffold_raw"
 
   295   "(op = ===> op = ===> op \<approx> ===> op =) ffold_raw ffold_raw"
 
   218   by (simp add: memb_def[symmetric] ffold_raw_rsp_pre)
 
   296   by (simp add: memb_def[symmetric] ffold_raw_rsp_pre)
 
       
   297 
       
   298 lemma concat_rsp_pre:
 
       
   299   assumes a: "list_rel op \<approx> x x'"
 
       
   300   and     b: "x' \<approx> y'"
 
       
   301   and     c: "list_rel op \<approx> y' y"
 
       
   302   and     d: "\<exists>x\<in>set x. xa \<in> set x"
 
       
   303   shows "\<exists>x\<in>set y. xa \<in> set x"
 
       
   304 proof -
 
       
   305   obtain xb where e: "xb \<in> set x" and f: "xa \<in> set xb" using d by auto
 
       
   306   have "\<exists>y. y \<in> set x' \<and> xb \<approx> y" by (rule list_rel_find_element[OF e a])
 
       
   307   then obtain ya where h: "ya \<in> set x'" and i: "xb \<approx> ya" by auto
 
       
   308   have j: "ya \<in> set y'" using b h by simp
 
       
   309   have "\<exists>yb. yb \<in> set y \<and> ya \<approx> yb" by (rule list_rel_find_element[OF j c])
 
       
   310   then show ?thesis using f i by auto
 
       
   311 qed
 
       
   312 
       
   313 lemma [quot_respect]:
 
       
   314   shows "(list_rel op \<approx> OOO op \<approx> ===> op \<approx>) concat concat"
 
       
   315 proof (rule fun_relI, elim pred_compE)
 
       
   316   fix a b ba bb
 
       
   317   assume a: "list_rel op \<approx> a ba"
 
       
   318   assume b: "ba \<approx> bb"
 
       
   319   assume c: "list_rel op \<approx> bb b"
 
       
   320   have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof
 
       
   321     fix x
 
       
   322     show "(\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof
 
       
   323       assume d: "\<exists>xa\<in>set a. x \<in> set xa"
 
       
   324       show "\<exists>xa\<in>set b. x \<in> set xa" by (rule concat_rsp_pre[OF a b c d])
 
       
   325     next
 
       
   326       assume e: "\<exists>xa\<in>set b. x \<in> set xa"
 
       
   327       have a': "list_rel op \<approx> ba a" by (rule list_rel_symp[OF list_eq_equivp, OF a])
 
       
   328       have b': "bb \<approx> ba" by (rule equivp_symp[OF list_eq_equivp, OF b])
 
       
   329       have c': "list_rel op \<approx> b bb" by (rule list_rel_symp[OF list_eq_equivp, OF c])
 
       
   330       show "\<exists>xa\<in>set a. x \<in> set xa" by (rule concat_rsp_pre[OF c' b' a' e])
 
       
   331     qed
 
       
   332   qed
 
       
   333   then show "concat a \<approx> concat b" by simp
 
       
   334 qed
 
   219 
   335 
   220 text {* Distributive lattice with bot *}
 
   336 text {* Distributive lattice with bot *}
 
   221 
   337 
   222 lemma sub_list_not_eq:
 
   338 lemma sub_list_not_eq:
 
   223   "(sub_list x y \<and> \<not> list_eq x y) = (sub_list x y \<and> \<not> sub_list y x)"
 
   339   "(sub_list x y \<and> \<not> list_eq x y) = (sub_list x y \<and> \<not> sub_list y x)"
 
   377 abbreviation
 
   493 abbreviation
 
   378   fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<notin>| _" [50, 51] 50)
 
   494   fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<notin>| _" [50, 51] 50)
 
   379 where
 
   495 where
 
   380   "x |\<notin>| S \<equiv> \<not> (x |\<in>| S)"
 
   496   "x |\<notin>| S \<equiv> \<not> (x |\<in>| S)"
 
   381 
   497 
   382 section {* Augmenting an fset -- @{const finsert} *}
 
   498 section {* Other constants on the Quotient Type *} 
       
   499 
       
   500 quotient_definition
 
       
   501   "fcard :: 'a fset \<Rightarrow> nat" 
       
   502 is
 
       
   503   "fcard_raw"
 
       
   504 
       
   505 quotient_definition
 
       
   506   "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
 
       
   507 is
 
       
   508  "map"
 
       
   509 
       
   510 quotient_definition
 
       
   511   "fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset" 
       
   512   is "delete_raw"
 
       
   513 
       
   514 quotient_definition
 
       
   515   "fset_to_set :: 'a fset \<Rightarrow> 'a set" 
       
   516   is "set"
 
       
   517 
       
   518 quotient_definition
 
       
   519   "ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b"
 
       
   520   is "ffold_raw"
 
       
   521 
       
   522 quotient_definition
 
       
   523   "fconcat :: ('a fset) fset \<Rightarrow> 'a fset"
 
       
   524 is
 
       
   525   "concat"
 
       
   526 
       
   527 text {* Compositional Respectfullness and Preservation *}
 
       
   528 
       
   529 lemma [quot_respect]: "(list_rel op \<approx> OOO op \<approx>) [] []"
 
       
   530   by (metis nil_rsp list_rel.simps(1) pred_compI)
 
       
   531 
       
   532 lemma [quot_preserve]: "(abs_fset \<circ> map f) [] = abs_fset []"
 
       
   533   by simp
 
       
   534 
       
   535 lemma [quot_respect]:
 
       
   536   "(op \<approx> ===> list_rel op \<approx> OOO op \<approx> ===> list_rel op \<approx> OOO op \<approx>) op # op #"
 
       
   537   apply auto
 
       
   538   apply (simp add: set_in_eq)
 
       
   539   apply (rule_tac b="x # b" in pred_compI)
 
       
   540   apply auto
 
       
   541   apply (rule_tac b="x # ba" in pred_compI)
 
       
   542   apply auto
 
       
   543   done
 
       
   544 
       
   545 lemma [quot_preserve]:
 
       
   546   "(rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op # = finsert"
 
       
   547   by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset]
 
       
   548       abs_o_rep[OF Quotient_fset] map_id finsert_def)
 
       
   549 
       
   550 lemma [quot_preserve]:
 
       
   551   "((map rep_fset \<circ> rep_fset) ---> (map rep_fset \<circ> rep_fset) ---> abs_fset \<circ> map abs_fset) op @ = funion"
 
       
   552   by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset]
 
       
   553       abs_o_rep[OF Quotient_fset] map_id sup_fset_def)
 
       
   554 
       
   555 lemma list_rel_app_l:
 
       
   556   assumes a: "reflp R"
 
       
   557   and b: "list_rel R l r"
 
       
   558   shows "list_rel R (z @ l) (z @ r)"
 
       
   559   by (induct z) (simp_all add: b, metis a reflp_def)
 
       
   560 
       
   561 lemma append_rsp2_pre0:
 
       
   562   assumes a:"list_rel op \<approx> x x'"
 
       
   563   shows "list_rel op \<approx> (x @ z) (x' @ z)"
 
       
   564   using a apply (induct x x' rule: list_induct2')
 
       
   565   apply simp_all
 
       
   566   apply (rule list_rel_refl)
 
       
   567   done
 
       
   568 
       
   569 lemma append_rsp2_pre1:
 
       
   570   assumes a:"list_rel op \<approx> x x'"
 
       
   571   shows "list_rel op \<approx> (z @ x) (z @ x')"
 
       
   572   using a apply (induct x x' arbitrary: z rule: list_induct2')
 
       
   573   apply (rule list_rel_refl)
 
       
   574   apply (simp_all del: list_eq.simps)
 
       
   575   apply (rule list_rel_app_l)
 
       
   576   apply (simp_all add: reflp_def)
 
       
   577   done
 
       
   578 
       
   579 lemma append_rsp2_pre:
 
       
   580   assumes a:"list_rel op \<approx> x x'"
 
       
   581   and     b: "list_rel op \<approx> z z'"
 
       
   582   shows "list_rel op \<approx> (x @ z) (x' @ z')"
 
       
   583   apply (rule list_rel_transp[OF fset_equivp])
 
       
   584   apply (rule append_rsp2_pre0)
 
       
   585   apply (rule a)
 
       
   586   using b apply (induct z z' rule: list_induct2')
 
       
   587   apply (simp_all only: append_Nil2)
 
       
   588   apply (rule list_rel_refl)
 
       
   589   apply simp_all
 
       
   590   apply (rule append_rsp2_pre1)
 
       
   591   apply simp
 
       
   592   done
 
       
   593 
       
   594 lemma [quot_respect]:
 
       
   595   "(list_rel op \<approx> OOO op \<approx> ===> list_rel op \<approx> OOO op \<approx> ===> list_rel op \<approx> OOO op \<approx>) op @ op @"
 
       
   596 proof (intro fun_relI, elim pred_compE)
 
       
   597   fix x y z w x' z' y' w' :: "'a list list"
 
       
   598   assume a:"list_rel op \<approx> x x'"
 
       
   599   and b:    "x' \<approx> y'"
 
       
   600   and c:    "list_rel op \<approx> y' y"
 
       
   601   assume aa: "list_rel op \<approx> z z'"
 
       
   602   and bb:   "z' \<approx> w'"
 
       
   603   and cc:   "list_rel op \<approx> w' w"
 
       
   604   have a': "list_rel op \<approx> (x @ z) (x' @ z')" using a aa append_rsp2_pre by auto
 
       
   605   have b': "x' @ z' \<approx> y' @ w'" using b bb by simp
 
       
   606   have c': "list_rel op \<approx> (y' @ w') (y @ w)" using c cc append_rsp2_pre by auto
 
       
   607   have d': "(op \<approx> OO list_rel op \<approx>) (x' @ z') (y @ w)"
 
       
   608     by (rule pred_compI) (rule b', rule c')
 
       
   609   show "(list_rel op \<approx> OOO op \<approx>) (x @ z) (y @ w)"
 
       
   610     by (rule pred_compI) (rule a', rule d')
 
       
   611 qed
 
       
   612 
       
   613 text {* Raw theorems. Finsert, memb, singleron, sub_list *}
 
   383 
   614 
   384 lemma nil_not_cons:
 
   615 lemma nil_not_cons:
 
   385   shows "\<not> ([] \<approx> x # xs)"
 
   616   shows "\<not> ([] \<approx> x # xs)"
 
   386   and   "\<not> (x # xs \<approx> [])"
 
   617   and   "\<not> (x # xs \<approx> [])"
 
   387   by auto
 
   618   by auto
 
   396 
   627 
   397 lemma memb_consI2:
 
   628 lemma memb_consI2:
 
   398   shows "memb x xs \<Longrightarrow> memb x (y # xs)"
 
   629   shows "memb x xs \<Longrightarrow> memb x (y # xs)"
 
   399   by (simp add: memb_def)
 
   630   by (simp add: memb_def)
 
   400 
   631 
   401 section {* Singletons *}
 
       
   402 
       
   403 lemma singleton_list_eq:
 
   632 lemma singleton_list_eq:
 
   404   shows "[x] \<approx> [y] \<longleftrightarrow> x = y"
 
   633   shows "[x] \<approx> [y] \<longleftrightarrow> x = y"
 
   405   by (simp add: id_simps) auto
 
   634   by (simp add: id_simps) auto
 
   406 
   635 
   407 section {* sub_list *}
 
       
   408 
       
   409 lemma sub_list_cons:
 
   636 lemma sub_list_cons:
 
   410   "sub_list (x # xs) ys = (memb x ys \<and> sub_list xs ys)"
 
   637   "sub_list (x # xs) ys = (memb x ys \<and> sub_list xs ys)"
 
   411   by (auto simp add: memb_def sub_list_def)
 
   638   by (auto simp add: memb_def sub_list_def)
 
   412 
   639 
   413 section {* Cardinality of finite sets *}
 
   640 text {* Cardinality of finite sets *}
 
   414 
       
   415 quotient_definition
 
       
   416   "fcard :: 'a fset \<Rightarrow> nat" 
       
   417 is
 
       
   418   "fcard_raw"
 
       
   419 
   641 
   420 lemma fcard_raw_0:
 
   642 lemma fcard_raw_0:
 
   421   shows "fcard_raw xs = 0 \<longleftrightarrow> xs \<approx> []"
 
   643   shows "fcard_raw xs = 0 \<longleftrightarrow> xs \<approx> []"
 
   422   by (induct xs) (auto simp add: memb_def)
 
   644   by (induct xs) (auto simp add: memb_def)
 
   423 
       
   424 
   645 
   425 lemma fcard_raw_not_memb:
 
   646 lemma fcard_raw_not_memb:
 
   426   shows "\<not> memb x xs \<longleftrightarrow> fcard_raw (x # xs) = Suc (fcard_raw xs)"
 
   647   shows "\<not> memb x xs \<longleftrightarrow> fcard_raw (x # xs) = Suc (fcard_raw xs)"
 
   427   by auto
 
   648   by auto
 
   428 
   649 
   430   assumes a: "fcard_raw xs = Suc n"
 
   651   assumes a: "fcard_raw xs = Suc n"
 
   431   shows "\<exists>x ys. \<not> (memb x ys) \<and> xs \<approx> (x # ys) \<and> fcard_raw ys = n"
 
   652   shows "\<exists>x ys. \<not> (memb x ys) \<and> xs \<approx> (x # ys) \<and> fcard_raw ys = n"
 
   432   using a
 
   653   using a
 
   433   by (induct xs) (auto simp add: memb_def split: if_splits)
 
   654   by (induct xs) (auto simp add: memb_def split: if_splits)
 
   434 
   655 
   435 lemma singleton_fcard_1: 
   656 lemma singleton_fcard_1:
 
   436   shows "set xs = {x} \<Longrightarrow> fcard_raw xs = 1"
 
   657   shows "set xs = {x} \<Longrightarrow> fcard_raw xs = 1"
 
   437   by (induct xs) (auto simp add: memb_def subset_insert)
 
   658   by (induct xs) (auto simp add: memb_def subset_insert)
 
   438 
   659 
   439 lemma fcard_raw_1:
 
   660 lemma fcard_raw_1:
 
   440   shows "fcard_raw xs = 1 \<longleftrightarrow> (\<exists>x. xs \<approx> [x])"
 
   661   shows "fcard_raw xs = 1 \<longleftrightarrow> (\<exists>x. xs \<approx> [x])"
 
   464   have "\<not>(\<forall>x. \<not> memb x A)" using a by auto
 
   685   have "\<not>(\<forall>x. \<not> memb x A)" using a by auto
 
   465   then have "\<not>A \<approx> []" using none_memb_nil[of A] by simp
 
   686   then have "\<not>A \<approx> []" using none_memb_nil[of A] by simp
 
   466   then show ?thesis using fcard_raw_0[of A] by simp
 
   687   then show ?thesis using fcard_raw_0[of A] by simp
 
   467 qed
 
   688 qed
 
   468 
   689 
   469 section {* fmap *}
 
   690 text {* fmap *}
 
   470 
       
   471 quotient_definition
 
       
   472   "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
 
       
   473 is
 
       
   474  "map"
 
       
   475 
   691 
   476 lemma map_append:
 
   692 lemma map_append:
 
   477   "map f (xs @ ys) \<approx> (map f xs) @ (map f ys)"
 
   693   "map f (xs @ ys) \<approx> (map f xs) @ (map f ys)"
 
   478   by simp
 
   694   by simp
 
   479 
   695 
   524 
   740 
   525 lemma fcard_raw_delete:
 
   741 lemma fcard_raw_delete:
 
   526   "fcard_raw (delete_raw xs y) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)"
 
   742   "fcard_raw (delete_raw xs y) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)"
 
   527   by (simp add: fdelete_raw_filter fcard_raw_delete_one)
 
   743   by (simp add: fdelete_raw_filter fcard_raw_delete_one)
 
   528 
   744 
   529 
       
   530 
       
   531 
       
   532 
       
   533 lemma finter_raw_empty:
 
   745 lemma finter_raw_empty:
 
   534   "finter_raw l [] = []"
 
   746   "finter_raw l [] = []"
 
   535   by (induct l) (simp_all add: not_memb_nil)
 
   747   by (induct l) (simp_all add: not_memb_nil)
 
   536 
   748 
   537 section {* Constants on the Quotient Type *} 
       
   538 
       
   539 quotient_definition
 
       
   540   "fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset" 
       
   541   is "delete_raw"
 
       
   542 
       
   543 quotient_definition
 
       
   544   "fset_to_set :: 'a fset \<Rightarrow> 'a set" 
       
   545   is "set"
 
       
   546 
       
   547 quotient_definition
 
       
   548   "ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b"
 
       
   549   is "ffold_raw"
 
       
   550 
       
   551 lemma set_cong: 
   749 lemma set_cong: 
   552   shows "(set x = set y) = (x \<approx> y)"
 
   750   shows "(set x = set y) = (x \<approx> y)"
 
   553   by auto
 
   751   by auto
 
   554 
   752 
   555 lemma inj_map_eq_iff:
 
   753 lemma inj_map_eq_iff:
 
   556   "inj f \<Longrightarrow> (map f l \<approx> map f m) = (l \<approx> m)"
 
   754   "inj f \<Longrightarrow> (map f l \<approx> map f m) = (l \<approx> m)"
 
   557   by (simp add: expand_set_eq[symmetric] inj_image_eq_iff)
 
   755   by (simp add: expand_set_eq[symmetric] inj_image_eq_iff)
 
   558 
       
   559 quotient_definition
 
       
   560   "fconcat :: ('a fset) fset \<Rightarrow> 'a fset"
 
       
   561 is
 
       
   562   "concat"
 
       
   563 
       
   564 
   756 
   565 text {* alternate formulation with a different decomposition principle
 
   757 text {* alternate formulation with a different decomposition principle
 
   566   and a proof of equivalence *}
 
   758   and a proof of equivalence *}
 
   567 
   759 
   568 inductive
 
   760 inductive
 
   639 proof
 
   831 proof
 
   640   show "list_eq2 l r \<Longrightarrow> l \<approx> r" by (induct rule: list_eq2.induct) auto
 
   832   show "list_eq2 l r \<Longrightarrow> l \<approx> r" by (induct rule: list_eq2.induct) auto
 
   641   show "l \<approx> r \<Longrightarrow> list_eq2 l r" using list_eq2_equiv_aux by blast
 
   833   show "l \<approx> r \<Longrightarrow> list_eq2 l r" using list_eq2_equiv_aux by blast
 
   642 qed
 
   834 qed
 
   643 
   835 
   644 section {* lifted part *}
 
   836 text {* Lifted theorems *}
 
   645 
   837 
   646 lemma not_fin_fnil: "x |\<notin>| {||}"
 
   838 lemma not_fin_fnil: "x |\<notin>| {||}"
 
   647   by (lifting not_memb_nil)
 
   839   by (lifting not_memb_nil)
 
   648 
   840 
   649 lemma fin_finsert_iff[simp]:
 
   841 lemma fin_finsert_iff[simp]:
 
   911   and "\<And>xs1 xs2 xs3. \<lbrakk>xs1 = xs2; P xs1 xs2; xs2 = xs3; P xs2 xs3\<rbrakk> \<Longrightarrow> P xs1 xs3"
 
  1103   and "\<And>xs1 xs2 xs3. \<lbrakk>xs1 = xs2; P xs1 xs2; xs2 = xs3; P xs2 xs3\<rbrakk> \<Longrightarrow> P xs1 xs3"
 
   912   shows "P x1 x2"
 
  1104   shows "P x1 x2"
 
   913   using assms
 
  1105   using assms
 
   914   by (lifting list_eq2.induct[simplified list_eq2_equiv[symmetric]])
 
  1106   by (lifting list_eq2.induct[simplified list_eq2_equiv[symmetric]])
 
   915 
  1107 
       
  1108 text {* concat *}
 
       
  1109 
       
  1110 lemma fconcat_empty:
 
       
  1111   shows "fconcat {||} = {||}"
 
       
  1112   by (lifting concat.simps(1))
 
       
  1113 
       
  1114 lemma fconcat_insert:
 
       
  1115   shows "fconcat (finsert x S) = x |\<union>| fconcat S"
 
       
  1116   by (lifting concat.simps(2))
 
       
  1117 
       
  1118 lemma "fconcat (xs |\<union>| ys) = fconcat xs |\<union>| fconcat ys"
 
       
  1119   by (lifting concat_append)
 
       
  1120 
   916 ML {*
 
  1121 ML {*
 
   917 fun dest_fsetT (Type ("FSet.fset", [T])) = T
 
  1122 fun dest_fsetT (Type ("FSet.fset", [T])) = T
 
   918   | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
 
  1123   | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
 
   919 *}
 
  1124 *}
 
   920 
  1125
nominal2