1 theory FSet2

     2 imports "../QuotMain" List

     3 begin

     4 

     5 inductive

     6   list_eq (infix "\<approx>" 50)

     7 where

     8   "a#b#xs \<approx> b#a#xs"

     9 | "[] \<approx> []"

    10 | "xs \<approx> ys \<Longrightarrow> ys \<approx> xs"

    11 | "a#a#xs \<approx> a#xs"

    12 | "xs \<approx> ys \<Longrightarrow> a#xs \<approx> a#ys"

    13 | "\<lbrakk>xs1 \<approx> xs2; xs2 \<approx> xs3\<rbrakk> \<Longrightarrow> xs1 \<approx> xs3"

    14 

    15 lemma list_eq_refl:

    16   shows "xs \<approx> xs"

    17 by (induct xs) (auto intro: list_eq.intros)

    18 

    19 lemma equivp_list_eq:

    20   shows "equivp list_eq"

    21 unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def

    22 by (auto intro: list_eq.intros list_eq_refl)

    23 

    24 quotient fset = "'a list" / "list_eq"

    25   by (rule equivp_list_eq)

    26 

    27 quotient_def 

    28   fempty :: "fempty :: 'a fset" ("{||}")

    29 where

    30   "[]"

    31 

    32 quotient_def 

    33   finsert :: "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"

    34 where

    35   "(op #)"

    36 

    37 lemma finsert_rsp[quot_respect]:

    38   shows "(op = ===> op \<approx> ===> op \<approx>) (op #) (op #)"

    39 by (auto intro: list_eq.intros)

    40 

    41 quotient_def 

    42   funion :: "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<union>f _" [65,66] 65)

    43 where

    44   "(op @)"

    45 

    46 lemma append_rsp_aux1:

    47   assumes a : "l2 \<approx> r2 "

    48   shows "(h @ l2) \<approx> (h @ r2)"

    49 using a

    50 apply(induct h)

    51 apply(auto intro: list_eq.intros(5))

    52 done

    53 

    54 lemma append_rsp_aux2:

    55   assumes a : "l1 \<approx> r1" "l2 \<approx> r2 "

    56   shows "(l1 @ l2) \<approx> (r1 @ r2)"

    57 using a

    58 apply(induct arbitrary: l2 r2)

    59 apply(simp_all)

    60 apply(blast intro: list_eq.intros append_rsp_aux1)+

    61 done

    62 

    63 lemma append_rsp[quot_respect]:

    64   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"

    65   by (auto simp add: append_rsp_aux2)

    66 

    67 

    68 quotient_def 

    69   fmem :: " fmem :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ \<in>f _" [50, 51] 50)

    70 where

    71   "(op mem)"

    72 

    73 lemma memb_rsp_aux:

    74   assumes a: "x \<approx> y"

    75   shows "(z mem x) = (z mem y)"

    76   using a by induct auto

    77 

    78 lemma memb_rsp[quot_respect]:

    79   shows "(op = ===> (op \<approx> ===> op =)) (op mem) (op mem)"

    80   by (simp add: memb_rsp_aux)

    81 

    82 definition 

    83   fnot_mem :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ \<notin>f _" [50, 51] 50)

    84 where

    85   "x \<notin>f S \<equiv> \<not>(x \<in>f S)"

    86 

    87 definition

    88   "inter_list" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"

    89 where

    90   "inter_list X Y \<equiv> [x \<leftarrow> X. x\<in>set Y]"

    91 

    92 quotient_def 

    93   finter :: "finter::'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<inter>f _" [70, 71] 70)

    94 where

    95   "inter_list"

    96 

    97 no_syntax

    98   "@Finset"     :: "args => 'a fset"                       ("{|(_)|}")

    99 syntax

   100   "@Finfset"     :: "args => 'a fset"                       ("{|(_)|}")

   101 translations

   102   "{|x, xs|}"     == "CONST finsert x {|xs|}"

   103   "{|x|}"         == "CONST finsert x {||}"

   104 

   105 

   106 subsection {* Empty sets *}

   107 

   108 lemma test:

   109   shows "\<not>(x # xs \<approx> [])"

   110 sorry

   111 

   112 lemma finsert_not_empty[simp]: 

   113   shows "finsert x S \<noteq> {||}"

   114   by (lifting test)

   115 

   116 

   117 

   118 

   119 end;