1 theory FSet2

     2 imports "../Quotient" "../Quotient_List" 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_type

    25   'a fset = "'a list" / "list_eq"

    26   by (rule equivp_list_eq)

    27 

    28 quotient_definition

    29   fempty ("{||}")

    30 where

    31   "fempty :: 'a fset"

    32 is

    33   "[]"

    34 

    35 quotient_definition

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

    37 is

    38   "(op #)"

    39 

    40 lemma finsert_rsp[quot_respect]:

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

    42 by (auto intro: list_eq.intros)

    43 

    44 quotient_definition

    45   funion ("_ \<union>f _" [65,66] 65)

    46 where

    47   "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"

    48 is

    49   "(op @)"

    50 

    51 lemma append_rsp_aux1:

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

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

    54 using a

    55 apply(induct h)

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

    57 done

    58 

    59 lemma append_rsp_aux2:

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

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

    62 using a

    63 apply(induct arbitrary: l2 r2)

    64 apply(simp_all)

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

    66 done

    67 

    68 lemma append_rsp[quot_respect]:

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

    70   by (auto simp add: append_rsp_aux2)

    71 

    72 

    73 quotient_definition

    74   fmem ("_ \<in>f _" [50, 51] 50)

    75 where

    76   "fmem :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool"

    77 is

    78   "(op mem)"

    79 

    80 lemma memb_rsp_aux:

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

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

    83   using a by induct auto

    84 

    85 lemma memb_rsp[quot_respect]:

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

    87   by (simp add: memb_rsp_aux)

    88 

    89 definition

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

    91 where

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

    93 

    94 definition

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

    96 where

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

    98 

    99 quotient_definition

   100   finter ("_ \<inter>f _" [70, 71] 70)

   101 where

   102   "finter::'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"

   103 is

   104   "inter_list"

   105 

   106 no_syntax

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

   108 syntax

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

   110 translations

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

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

   113 

   114 

   115 subsection {* Empty sets *}

   116 

   117 lemma test:

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

   119 sorry

   120 

   121 lemma finsert_not_empty[simp]: 

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

   123   by (lifting test)

   124 

   125 

   126 

   127 

   128 end;