1 theory FSet3

     2 imports "../QuotMain" List

     3 begin

     4 

     5 definition

     6   list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50)

     7 where

     8   "list_eq x y = (\<forall>e. e mem x = e mem y)"

     9 

    10 lemma list_eq_reflp:

    11   shows "xs \<approx> xs"

    12   by (metis list_eq_def)

    13 

    14 lemma list_eq_equivp:

    15   shows "equivp list_eq"

    16   unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def

    17   apply (auto intro: list_eq_def)

    18   apply (metis list_eq_def)

    19   apply (metis list_eq_def)

    20   sorry

    21 

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

    23   by (rule list_eq_equivp)

    24 

    25 lemma not_nil_equiv_cons: "[] \<noteq> a # A" sorry

    26 

    27 (* The 2 lemmas below are different from the ones in QuotList *)

    28 lemma nil_rsp[quot_respect]:

    29   shows "[] \<approx> []"

    30 by (rule list_eq_reflp)

    31 

    32 lemma cons_rsp[quot_respect]: (* Better then the one from QuotList *)

    33   " (op = ===> op \<approx> ===> op \<approx>) op # op #"

    34   sorry

    35 

    36 lemma mem_rsp[quot_respect]:

    37   "(op = ===> op \<approx> ===> op =) (op mem) (op mem)"

    38   sorry

    39 

    40 lemma no_mem_nil: "(\<forall>a. \<not>(a mem A)) = (A = [])"

    41 sorry

    42 

    43 lemma none_mem_nil: "(\<forall>a. \<not>(a mem A)) = (A \<approx> [])"

    44 sorry

    45 

    46 lemma mem_cons: "a mem A \<Longrightarrow> a # A \<approx> A"

    47 sorry

    48 

    49 lemma cons_left_comm: "x # y # A \<approx> y # x # A"

    50 sorry

    51 

    52 lemma cons_left_idem: "x # x # A \<approx> x # A"

    53 sorry

    54 

    55 lemma finite_set_raw_strong_cases:

    56   "(X = []) \<or> (\<exists>a. \<exists> Y. (~(a mem Y) \<and> (X \<approx> a # Y)))"

    57   apply (induct X)

    58   apply (simp)

    59   sorry

    60 

    61 primrec

    62   delete_raw :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list"

    63 where

    64   "delete_raw [] x = []"

    65 | "delete_raw (a # A) x = (if (a = x) then delete_raw A x else a # (delete_raw A x))"

    66 

    67 lemma mem_delete_raw:

    68   "x mem (delete_raw A a) = x mem A \<and> \<not>(x = a)"

    69 sorry

    70 

    71 lemma mem_delete_raw_ident:

    72   "\<not>(MEM a (A delete_raw a))"

    73 sorry

    74 

    75 lemma not_mem_delete_raw_ident:

    76   "\<not>(b mem A) \<Longrightarrow> (delete_raw A b = A)"

    77 sorry

    78 

    79 lemma delete_raw_RSP:

    80   "A \<approx> B \<Longrightarrow> delete_raw A a \<approx> delete_raw B a"

    81 sorry

    82 

    83 lemma cons_delete_raw:

    84   "a # (delete_raw A a) \<approx> (if a mem A then A else (a # A))"

    85 sorry

    86 

    87 lemma mem_cons_delete_raw:

    88     "a mem A \<Longrightarrow> a # (delete_raw A a) \<approx> A"

    89 sorry

    90 

    91 lemma finite_set_raw_delete_raw_cases1:

    92     "X = [] \<or> (\<exists>a. X \<approx> a # delete_raw X a)"

    93 sorry

    94 

    95 lemma finite_set_raw_delete_raw_cases:

    96     "X = [] \<or> (\<exists>a. a mem X \<and> X \<approx> a # delete_raw X a)"

    97 sorry

    98 

    99 fun

   100   card_raw :: "'a list \<Rightarrow> nat"

   101 where

   102   card_raw_nil: "card_raw [] = 0"

   103 | card_raw_cons: "card_raw (x # xs) = (if x mem xs then card_raw xs else Suc (card_raw xs))"

   104 

   105 lemma not_mem_card_raw:

   106   fixes x :: "'a"

   107   fixes xs :: "'a list"

   108   shows "(\<not>(x mem xs)) = (card_raw (x # xs) = Suc (card_raw xs))"

   109   sorry

   110 

   111 lemma card_raw_suc:

   112   fixes xs :: "'a list"

   113   fixes n :: "nat"

   114   assumes c: "card_raw xs = Suc n"

   115   shows "\<exists>a ys. \<not>(a mem ys) \<and> xs \<approx> (a # ys)"

   116   using c

   117 apply(induct xs)

   118 apply(metis mem_delete_raw)

   119 apply(metis mem_delete_raw)

   120 done

   121 

   122 lemma mem_card_raw_not_0:

   123   "a mem A \<Longrightarrow> \<not>(card_raw A = 0)"

   124 sorry

   125 

   126 lemma card_raw_cons_gt_0:

   127   "0 < card_raw (a # A)"

   128 sorry

   129 

   130 lemma card_raw_delete_raw:

   131   "card_raw (delete_raw A a) = (if a mem A then card_raw A - 1 else card_raw A)"

   132 sorry

   133 

   134 lemma card_raw_rsp_aux:

   135   assumes e: "a \<approx> b"

   136   shows "card_raw a = card_raw b"

   137   using e sorry

   138 

   139 lemma card_raw_rsp[quot_respect]:

   140   "(op \<approx> ===> op =) card_raw card_raw"

   141   by (simp add: card_raw_rsp_aux)

   142 

   143 lemma card_raw_0:

   144   "(card_raw A = 0) = (A = [])"

   145 sorry

   146 

   147 lemma list2set_thm:

   148   shows "set [] = {}"

   149   and "set (h # t) = insert h (set t)"

   150 sorry

   151 

   152 lemma list2set_RSP:

   153   "A \<approx> B \<Longrightarrow> set A = set B"

   154 sorry

   155 

   156 definition

   157   rsp_fold

   158 where

   159   "rsp_fold f = (\<forall>u v w. (f u (f v w) = f v (f u w)))"

   160 

   161 primrec

   162   fold_raw :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"

   163 where

   164   "fold_raw f z [] = z"

   165 | "fold_raw f z (a # A) =

   166      (if (rsp_fold f) then

   167        if a mem A then fold_raw f z A

   168        else f a (fold_raw f z A)

   169      else z)"

   170 

   171 lemma mem_lcommuting_fold_raw:

   172   "rsp_fold f \<Longrightarrow> h mem B \<Longrightarrow> fold_raw f z B = f h (fold_raw f z (delete_raw B h))"

   173 sorry

   174 

   175 lemma fold_rsp[quot_respect]:

   176   "(op = ===> op = ===> op \<approx> ===> op =) fold_raw fold_raw"

   177   apply (auto)

   178   apply (case_tac "rsp_fold x")

   179 sorry

   180 

   181 lemma append_rsp[quot_respect]:

   182   "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"

   183   sorry

   184 

   185 primrec

   186   inter_raw

   187 where

   188   "inter_raw [] B = []"

   189 | "inter_raw (a # A) B = (if a mem B then a # inter_raw A B else inter_raw A B)"

   190 

   191 lemma mem_inter_raw:

   192   "x mem (inter_raw A B) = x mem A \<and> x mem B"

   193 sorry

   194 

   195 lemma inter_raw_RSP:

   196   "A1 \<approx> A2 \<and> B1 \<approx> B2 \<Longrightarrow> (inter_raw A1 B1) \<approx> (inter_raw A2 B2)"

   197 sorry

   198 

   199 

   200 (* LIFTING DEFS *)

   201 

   202 quotient_def

   203   "Empty :: 'a fset" as "[]::'a list"

   204 

   205 quotient_def

   206   "Insert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" as "op #"

   207 

   208 quotient_def

   209   "In :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" as "op mem"

   210 

   211 quotient_def

   212   "Card :: 'a fset \<Rightarrow> nat" as "card_raw"

   213 

   214 quotient_def

   215   "Delete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset" as "delete_raw"

   216 

   217 quotient_def

   218   "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" as "op @"

   219 

   220 quotient_def

   221   "finter :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" as "inter_raw"

   222 

   223 quotient_def

   224   "ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b" as "fold_raw"

   225 

   226 quotient_def

   227   "fset_to_set :: 'a fset \<Rightarrow> 'a set" as "set"

   228 

   229 

   230 (* LIFTING THMS *)

   231 

   232 thm list.cases (* ??? *)

   233 

   234 thm cons_left_comm

   235 lemma "Insert a (Insert b x) = Insert b (Insert a x)"

   236 by (lifting cons_left_comm)

   237 

   238 thm cons_left_idem

   239 lemma "Insert a (Insert a x) = Insert a x"

   240 by (lifting cons_left_idem)

   241 

   242 (* thm MEM:

   243   MEM x [] = F

   244   MEM x (h::t) = (x=h) \/ MEM x t *)

   245 thm none_mem_nil

   246 thm mem_cons

   247 thm finite_set_raw_strong_cases

   248 thm card_raw.simps

   249 thm not_mem_card_raw

   250 thm card_raw_suc

   251 lemma "Card x = Suc n \<Longrightarrow> (\<exists>a b. \<not> In a b & x = Insert a b)"

   252 by (lifting card_raw_suc)

   253 

   254 thm card_raw_cons_gt_0

   255 thm mem_card_raw_not_0

   256 thm not_nil_equiv_cons

   257 thm delete_raw.simps

   258 thm mem_delete_raw

   259 thm card_raw_delete_raw

   260 thm cons_delete_raw

   261 thm mem_cons_delete_raw

   262 thm finite_set_raw_delete_raw_cases

   263 thm append.simps

   264 (* MEM_APPEND: MEM e (APPEND l1 l2) = MEM e l1 \/ MEM e l2 *)

   265 thm inter_raw.simps

   266 thm mem_inter_raw

   267 thm fold_raw.simps

   268 thm list2set_thm

   269 thm list_eq_def

   270 thm list.induct

   271 lemma "\<lbrakk>P Empty; \<And>a x. P x \<Longrightarrow> P (Insert a x)\<rbrakk> \<Longrightarrow> P l"

   272 by (lifting list.induct)

   273 

   274 (* We also have map and some properties of it in FSet *)

   275 (* and the following which still lifts ok *)

   276 lemma "funion (funion x xa) xb = funion x (funion xa xb)"

   277 by (lifting append_assoc)

   278 

   279 end