1 theory FSet3

     2 imports "../Quotient" "../Quotient_List" List

     3 begin

     4 

     5 ML {*

     6 structure QuotientRules = Named_Thms

     7   (val name = "quot_thm"

     8    val description = "Quotient theorems.")

     9 *}

    10 

    11 ML {*

    12 open QuotientRules

    13 *}

    14 

    15 fun

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

    17 where

    18   "list_eq xs ys = (\<forall>x. x \<in> set xs \<longleftrightarrow> x \<in> set ys)"

    19 

    20 lemma list_eq_equivp:

    21   shows "equivp list_eq"

    22 unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def

    23 by auto

    24 

    25 (* FIXME-TODO: because of beta-reduction, one cannot give the *)

    26 (* FIXME-TODO: relation as a term or abbreviation             *) 

    27 quotient_type 

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

    29 by (rule list_eq_equivp)

    30 

    31 

    32 section {* empty fset, finsert and membership *} 

    33 

    34 quotient_definition

    35   fempty  ("{||}")

    36 where

    37   "fempty :: 'a fset"

    38 is "[]::'a list"

    39 

    40 quotient_definition

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

    42 is "op #"

    43 

    44 syntax

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

    46 

    47 translations

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

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

    50 

    51 definition 

    52   memb :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"

    53 where

    54   "memb x xs \<equiv> x \<in> set xs"

    55 

    56 quotient_definition

    57   fin ("_ |\<in>| _" [50, 51] 50)

    58 where

    59   "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool"

    60 is "memb"

    61 

    62 abbreviation

    63   fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<notin>| _" [50, 51] 50)

    64 where

    65   "a |\<notin>| S \<equiv> \<not>(a |\<in>| S)"

    66 

    67 lemma memb_rsp[quot_respect]: 

    68   shows "(op = ===> op \<approx> ===> op =) memb memb"

    69 by (auto simp add: memb_def)

    70 

    71 lemma nil_rsp[quot_respect]:

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

    73 by simp

    74 

    75 lemma cons_rsp[quot_respect]: 

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

    77 by simp

    78 

    79 

    80 section {* Augmenting a set -- @{const finsert} *}

    81 

    82 text {* raw section *}

    83 

    84 lemma nil_not_cons:

    85   shows "\<not>[] \<approx> x # xs"

    86   by auto

    87 

    88 lemma memb_cons_iff:

    89   shows "memb x (y # xs) = (x = y \<or> memb x xs)"

    90   by (induct xs) (auto simp add: memb_def)

    91 

    92 lemma memb_consI1:

    93   shows "memb x (x # xs)"

    94   by (simp add: memb_def)

    95 

    96 lemma memb_consI2:

    97   shows "memb x xs \<Longrightarrow> memb x (y # xs)"

    98   by (simp add: memb_def)

    99 

   100 lemma memb_absorb:

   101   shows "memb x xs \<Longrightarrow> x # xs \<approx> xs"

   102   by (induct xs) (auto simp add: memb_def id_simps)

   103 

   104 text {* lifted section *}

   105 

   106 lemma fin_finsert_iff[simp]:

   107   "x |\<in>| finsert y S = (x = y \<or> x |\<in>| S)"

   108 by (lifting memb_cons_iff) 

   109 

   110 lemma

   111   shows finsertI1: "x |\<in>| finsert x S"

   112   and   finsertI2: "x |\<in>| S \<Longrightarrow> x |\<in>| finsert y S"

   113   by (lifting memb_consI1, lifting memb_consI2)

   114 

   115 

   116 lemma finsert_absorb [simp]: 

   117   shows "x |\<in>| S \<Longrightarrow> finsert x S = S"

   118   by (lifting memb_absorb)

   119 

   120 

   121 section {* Singletons *}

   122 

   123 text {* raw section *}

   124 

   125 lemma singleton_list_eq:

   126   shows "[x] \<approx> [y] \<longleftrightarrow> x = y"

   127   by (simp add: id_simps) auto

   128 

   129 text {* lifted section *}

   130 

   131 lemma fempty_not_finsert[simp]:

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

   133   by (lifting nil_not_cons)

   134 

   135 lemma fsingleton_eq[simp]:

   136   shows "{|x|} = {|y|} \<longleftrightarrow> x = y"

   137   by (lifting singleton_list_eq)

   138 

   139 section {* Union *}

   140 

   141 quotient_definition

   142   funion  (infixl "|\<union>|" 65)

   143 where

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

   145 is

   146   "op @"

   147 

   148 section {* Cardinality of finite sets *}

   149 

   150 fun

   151   fcard_raw :: "'a list \<Rightarrow> nat"

   152 where

   153   fcard_raw_nil:  "fcard_raw [] = 0"

   154 | fcard_raw_cons: "fcard_raw (x # xs) = (if memb x xs then fcard_raw xs else Suc (fcard_raw xs))"

   155 

   156 quotient_definition

   157   "fcard :: 'a fset \<Rightarrow> nat" 

   158 is "fcard_raw"

   159 

   160 text {* raw section *}

   161 

   162 lemma fcard_raw_ge_0:

   163   assumes a: "x \<in> set xs"

   164   shows "0 < fcard_raw xs"

   165 using a

   166 by (induct xs) (auto simp add: memb_def)

   167 

   168 lemma fcard_raw_delete_one:

   169   "fcard_raw ([x \<leftarrow> xs. x \<noteq> y]) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)"

   170 by (induct xs) (auto dest: fcard_raw_ge_0 simp add: memb_def)

   171 

   172 lemma fcard_raw_rsp_aux:

   173   assumes a: "a \<approx> b"

   174   shows "fcard_raw a = fcard_raw b"

   175 using a

   176 apply(induct a arbitrary: b)

   177 apply(auto simp add: memb_def)

   178 apply(metis)

   179 apply(drule_tac x="[x \<leftarrow> b. x \<noteq> a1]" in meta_spec)

   180 apply(simp add: fcard_raw_delete_one)

   181 apply(metis Suc_pred' fcard_raw_ge_0 fcard_raw_delete_one memb_def)

   182 done

   183 

   184 lemma fcard_raw_rsp[quot_respect]:

   185   "(op \<approx> ===> op =) fcard_raw fcard_raw"

   186   by (simp add: fcard_raw_rsp_aux)

   187 

   188 text {* lifted section *}

   189 

   190 lemma fcard_fempty [simp]:

   191   shows "fcard {||} = 0"

   192 by (lifting fcard_raw_nil)

   193 

   194 lemma fcard_finsert_if [simp]:

   195   shows "fcard (finsert x S) = (if x |\<in>| S then fcard S else Suc (fcard S))"

   196 by (lifting fcard_raw_cons)

   197 

   198 

   199 section {* Induction and Cases rules for finite sets *}

   200 

   201 lemma fset_exhaust[case_names fempty finsert, cases type: fset]:

   202   shows "\<lbrakk>S = {||} \<Longrightarrow> P; \<And>x S'. S = finsert x S' \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"

   203 by (lifting list.exhaust)

   204 

   205 lemma fset_induct[case_names fempty finsert]:

   206   shows "\<lbrakk>P {||}; \<And>x S. P S \<Longrightarrow> P (finsert x S)\<rbrakk> \<Longrightarrow> P S"

   207 by (lifting list.induct)

   208 

   209 lemma fset_induct2[case_names fempty finsert, induct type: fset]:

   210   assumes prem1: "P {||}" 

   211   and     prem2: "\<And>x S. \<lbrakk>x |\<notin>| S; P S\<rbrakk> \<Longrightarrow> P (finsert x S)"

   212   shows "P S"

   213 proof(induct S rule: fset_induct)

   214   case fempty

   215   show "P {||}" by (rule prem1)

   216 next

   217   case (finsert x S)

   218   have asm: "P S" by fact

   219   show "P (finsert x S)"

   220   proof(cases "x |\<in>| S")

   221     case True

   222     have "x |\<in>| S" by fact

   223     then show "P (finsert x S)" using asm by simp

   224   next

   225     case False

   226     have "x |\<notin>| S" by fact

   227     then show "P (finsert x S)" using prem2 asm by simp

   228   qed

   229 qed

   230 

   231 

   232 section {* fmap and fset comprehension *}

   233 

   234 quotient_definition

   235   "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"

   236 is

   237  "map"

   238 

   239 quotient_definition

   240   "fconcat :: ('a fset) fset => 'a fset"

   241 is

   242  "concat"

   243 

   244 (*lemma fconcat_rsp[quot_respect]:

   245   shows "((list_rel op \<approx>) ===> op \<approx>) concat concat"

   246 apply(auto)

   247 sorry

   248 *)

   249 

   250 (* PROBLEM: these lemmas needs to be restated, since  *)

   251 (* concat.simps(1) and concat.simps(2) contain the    *)

   252 (* type variables ?'a1.0 (which are turned into frees *)

   253 (* 'a_1                                               *)

   254 lemma concat1:

   255   shows "concat [] \<approx> []"

   256 by (simp add: id_simps)

   257 

   258 lemma concat2:

   259   shows "concat (x # xs) \<approx> x @ concat xs"

   260 by (simp add: id_simps)

   261 

   262 lemma concat_rsp[quot_respect]:

   263   shows "(list_rel op \<approx> OOO op \<approx> ===> op \<approx>) concat concat"

   264 sorry

   265 

   266 lemma nil_rsp2[quot_respect]: "(list_rel op \<approx> OOO op \<approx>) [] []"

   267   apply (metis FSet3.nil_rsp list_rel.simps(1) pred_comp.intros)

   268   done

   269 

   270 lemma set_in_eq: "(\<forall>e. ((e \<in> A) \<longleftrightarrow> (e \<in> B))) \<equiv> A = B"

   271   apply (rule eq_reflection)

   272   apply auto

   273   done

   274 

   275 lemma map_rel_cong: "b \<approx> ba \<Longrightarrow> map f b \<approx> map f ba"

   276   unfolding list_eq.simps

   277   apply(simp only: set_map set_in_eq)

   278   done

   279 

   280 lemma quotient_compose_list_pre:

   281   "(list_rel op \<approx> OOO op \<approx>) r s =

   282   ((list_rel op \<approx> OOO op \<approx>) r r \<and> (list_rel op \<approx> OOO op \<approx>) s s \<and>

   283   abs_fset (map abs_fset r) = abs_fset (map abs_fset s))"

   284   apply rule

   285   apply rule

   286   apply rule

   287   apply (rule list_rel_refl)

   288   apply (metis equivp_def fset_equivp)

   289   apply rule

   290   apply (rule equivp_reflp[OF fset_equivp])

   291   apply (rule list_rel_refl)

   292   apply (metis equivp_def fset_equivp)

   293   apply(rule)

   294   apply rule

   295   apply (rule list_rel_refl)

   296   apply (metis equivp_def fset_equivp)

   297   apply rule

   298   apply (rule equivp_reflp[OF fset_equivp])

   299   apply (rule list_rel_refl)

   300   apply (metis equivp_def fset_equivp)

   301   apply (subgoal_tac "map abs_fset r \<approx> map abs_fset s")

   302   apply (metis Quotient_rel[OF Quotient_fset])

   303   apply (auto simp only:)[1]

   304   apply (subgoal_tac "map abs_fset r = map abs_fset b")

   305   prefer 2

   306   apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]])

   307   apply (subgoal_tac "map abs_fset s = map abs_fset ba")

   308   prefer 2

   309   apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]])

   310   apply (simp only: map_rel_cong)

   311   apply rule

   312   apply (rule rep_abs_rsp[of "list_rel op \<approx>" "map abs_fset"])

   313   apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *})

   314   apply (rule list_rel_refl)

   315   apply (metis equivp_def fset_equivp)

   316   apply rule

   317   prefer 2

   318   apply (rule rep_abs_rsp_left[of "list_rel op \<approx>" "map abs_fset"])

   319   apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *})

   320   apply (rule list_rel_refl)

   321   apply (metis equivp_def fset_equivp)

   322   apply (erule conjE)+

   323   apply (subgoal_tac "map abs_fset r \<approx> map abs_fset s")

   324   prefer 2

   325   apply (metis Quotient_def Quotient_fset equivp_reflp fset_equivp)

   326   apply (rule map_rel_cong)

   327   apply (assumption)

   328   done

   329 

   330 lemma quotient_compose_list[quot_thm]:

   331   shows  "Quotient ((list_rel op \<approx>) OOO (op \<approx>))

   332     (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)"

   333   unfolding Quotient_def comp_def

   334   apply (rule)+

   335   apply (simp add: abs_o_rep[OF Quotient_fset] id_simps Quotient_abs_rep[OF Quotient_fset])

   336   apply (rule)

   337   apply (rule)

   338   apply (rule)

   339   apply (rule list_rel_refl)

   340   apply (metis equivp_def fset_equivp)

   341   apply (rule)

   342   apply (rule equivp_reflp[OF fset_equivp])

   343   apply (rule list_rel_refl)

   344   apply (metis equivp_def fset_equivp)

   345   apply rule

   346   apply rule

   347   apply(rule quotient_compose_list_pre)

   348   done

   349 

   350 lemma fconcat_empty:

   351   shows "fconcat {||} = {||}"

   352 apply(lifting concat1)

   353 apply(cleaning)

   354 apply(simp add: comp_def)

   355 apply(fold fempty_def[simplified id_simps])

   356 apply(rule refl)

   357 done

   358 

   359 (* Should be true *)

   360 

   361 lemma insert_rsp2[quot_respect]:

   362   "(op \<approx> ===> list_rel op \<approx> OOO op \<approx> ===> list_rel op \<approx> OOO op \<approx>) op # op #"

   363 apply auto

   364 apply (simp add: set_in_eq)

   365 sorry

   366 

   367 lemma append_rsp[quot_respect]:

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

   369   by (auto)

   370 

   371 lemma fconcat_insert:

   372   shows "fconcat (finsert x S) = x |\<union>| fconcat S"

   373 apply(lifting concat2)

   374 apply(cleaning)

   375 apply (simp add: finsert_def fconcat_def comp_def)

   376 apply cleaning

   377 done

   378 

   379 text {* raw section *}

   380 

   381 lemma map_rsp_aux:

   382   assumes a: "a \<approx> b"

   383   shows "map f a \<approx> map f b"

   384   using a

   385 apply(induct a arbitrary: b)

   386 apply(auto)

   387 apply(metis rev_image_eqI)

   388 done

   389 

   390 lemma map_rsp[quot_respect]:

   391   shows "(op = ===> op \<approx> ===> op \<approx>) map map"

   392 by (auto simp add: map_rsp_aux)

   393 

   394 

   395 text {* lifted section *}

   396 

   397 (* TBD *)

   398 

   399 text {* syntax for fset comprehensions (adapted from lists) *}

   400 

   401 nonterminals fsc_qual fsc_quals

   402 

   403 syntax

   404 "_fsetcompr" :: "'a \<Rightarrow> fsc_qual \<Rightarrow> fsc_quals \<Rightarrow> 'a fset"  ("{|_ . __")

   405 "_fsc_gen" :: "'a \<Rightarrow> 'a fset \<Rightarrow> fsc_qual" ("_ <- _")

   406 "_fsc_test" :: "bool \<Rightarrow> fsc_qual" ("_")

   407 "_fsc_end" :: "fsc_quals" ("|}")

   408 "_fsc_quals" :: "fsc_qual \<Rightarrow> fsc_quals \<Rightarrow> fsc_quals" (", __")

   409 "_fsc_abs" :: "'a => 'b fset => 'b fset"

   410 

   411 syntax (xsymbols)

   412 "_fsc_gen" :: "'a \<Rightarrow> 'a fset \<Rightarrow> fsc_qual" ("_ \<leftarrow> _")

   413 syntax (HTML output)

   414 "_fsc_gen" :: "'a \<Rightarrow> 'a fset \<Rightarrow> fsc_qual" ("_ \<leftarrow> _")

   415 

   416 parse_translation (advanced) {*

   417 let

   418   val femptyC = Syntax.const @{const_name fempty};

   419   val finsertC = Syntax.const @{const_name finsert};

   420   val fmapC = Syntax.const @{const_name fmap};

   421   val fconcatC = Syntax.const @{const_name fconcat};

   422   val IfC = Syntax.const @{const_name If};

   423   fun fsingl x = finsertC $ x $ femptyC;

   424 

   425   fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *)

   426     let

   427       val x = Free (Name.variant (fold Term.add_free_names [p, e] []) "x", dummyT);

   428       val e = if opti then fsingl e else e;

   429       val case1 = Syntax.const "_case1" $ p $ e;

   430       val case2 = Syntax.const "_case1" $ Syntax.const Term.dummy_patternN

   431                                         $ femptyC;

   432       val cs = Syntax.const "_case2" $ case1 $ case2

   433       val ft = Datatype_Case.case_tr false Datatype.info_of_constr

   434                  ctxt [x, cs]

   435     in lambda x ft end;

   436 

   437   fun abs_tr ctxt (p as Free(s,T)) e opti =

   438         let val thy = ProofContext.theory_of ctxt;

   439             val s' = Sign.intern_const thy s

   440         in if Sign.declared_const thy s'

   441            then (pat_tr ctxt p e opti, false)

   442            else (lambda p e, true)

   443         end

   444     | abs_tr ctxt p e opti = (pat_tr ctxt p e opti, false);

   445 

   446   fun fsc_tr ctxt [e, Const("_fsc_test",_) $ b, qs] =

   447         let 

   448           val res = case qs of 

   449                       Const("_fsc_end",_) => fsingl e

   450                     | Const("_fsc_quals",_)$ q $ qs => fsc_tr ctxt [e, q, qs];

   451         in 

   452           IfC $ b $ res $ femptyC 

   453         end

   454 

   455     | fsc_tr ctxt [e, Const("_fsc_gen",_) $ p $ es, Const("_fsc_end",_)] =

   456          (case abs_tr ctxt p e true of

   457             (f,true) => fmapC $ f $ es

   458           | (f, false) => fconcatC $ (fmapC $ f $ es))

   459        

   460     | fsc_tr ctxt [e, Const("_fsc_gen",_) $ p $ es, Const("_fsc_quals",_) $ q $ qs] =

   461         let

   462           val e' = fsc_tr ctxt [e, q, qs];

   463         in 

   464           fconcatC $ (fmapC $ (fst (abs_tr ctxt p e' false)) $ es) 

   465         end

   466 

   467 in [("_fsetcompr", fsc_tr)] end

   468 *}

   469 

   470 

   471 (* NEEDS FIXING *)

   472 (* examles *)

   473 (*

   474 term "{|(x,y,z). b|}"

   475 term "{|x. x \<leftarrow> xs|}"

   476 term "{|(x,y,z). x\<leftarrow>xs|}"

   477 term "{|e x y. x\<leftarrow>xs, y\<leftarrow>ys|}"

   478 term "{|(x,y,z). x<a, x>b|}"

   479 term "{|(x,y,z). x\<leftarrow>xs, x>b|}"

   480 term "{|(x,y,z). x<a, x\<leftarrow>xs|}"

   481 term "{|(x,y). Cons True x \<leftarrow> xs|}"

   482 term "{|(x,y,z). Cons x [] \<leftarrow> xs|}"

   483 term "{|(x,y,z). x<a, x>b, x=d|}"

   484 term "{|(x,y,z). x<a, x>b, y\<leftarrow>ys|}"

   485 term "{|(x,y,z). x<a, x\<leftarrow>xs,y>b|}"

   486 term "{|(x,y,z). x<a, x\<leftarrow>xs, y\<leftarrow>ys|}"

   487 term "{|(x,y,z). x\<leftarrow>xs, x>b, y<a|}"

   488 term "{|(x,y,z). x\<leftarrow>xs, x>b, y\<leftarrow>ys|}"

   489 term "{|(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,y>x|}"

   490 term "{|(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,z\<leftarrow>zs|}"

   491 *)

   492 

   493 (* BELOW CONSTRUCTION SITE *)

   494 

   495 

   496 lemma no_mem_nil: 

   497   "(\<forall>a. a \<notin> set A) = (A = [])"

   498 by (induct A) (auto)

   499 

   500 lemma none_mem_nil: 

   501   "(\<forall>a. a \<notin> set A) = (A \<approx> [])"

   502 by simp

   503 

   504 lemma mem_cons: 

   505   "a \<in> set A \<Longrightarrow> a # A \<approx> A"

   506 by auto

   507 

   508 lemma cons_left_comm:

   509   "x # y # A \<approx> y # x # A"

   510 by (auto simp add: id_simps)

   511 

   512 lemma cons_left_idem:

   513   "x # x # A \<approx> x # A"

   514 by (auto simp add: id_simps)

   515 

   516 lemma finite_set_raw_strong_cases:

   517   "(X = []) \<or> (\<exists>a Y. ((a \<notin> set Y) \<and> (X \<approx> a # Y)))"

   518   apply (induct X)

   519   apply (simp)

   520   apply (rule disjI2)

   521   apply (erule disjE)

   522   apply (rule_tac x="a" in exI)

   523   apply (rule_tac x="[]" in exI)

   524   apply (simp)

   525   apply (erule exE)+

   526   apply (case_tac "a = aa")

   527   apply (rule_tac x="a" in exI)

   528   apply (rule_tac x="Y" in exI)

   529   apply (simp)

   530   apply (rule_tac x="aa" in exI)

   531   apply (rule_tac x="a # Y" in exI)

   532   apply (auto)

   533   done

   534 

   535 fun

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

   537 where

   538   "delete_raw [] x = []"

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

   540 

   541 lemma mem_delete_raw:

   542   "x \<in> set (delete_raw A a) = (x \<in> set A \<and> \<not>(x = a))"

   543   by (induct A arbitrary: x a) (auto)

   544 

   545 lemma mem_delete_raw_ident:

   546   "\<not>(a \<in> set (delete_raw A a))"

   547 by (induct A) (auto)

   548 

   549 lemma not_mem_delete_raw_ident:

   550   "b \<notin> set A \<Longrightarrow> (delete_raw A b = A)"

   551 by (induct A) (auto)

   552 

   553 lemma delete_raw_RSP:

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

   555 apply(induct A arbitrary: B a)

   556 apply(auto)

   557 sorry

   558 

   559 lemma cons_delete_raw:

   560   "a # (delete_raw A a) \<approx> (if a \<in> set A then A else (a # A))"

   561 sorry

   562 

   563 lemma mem_cons_delete_raw:

   564     "a \<in> set A \<Longrightarrow> a # (delete_raw A a) \<approx> A"

   565 sorry

   566 

   567 lemma finite_set_raw_delete_raw_cases:

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

   569   by (induct X) (auto)

   570 

   571 

   572 

   573 

   574 

   575 lemma list2set_thm:

   576   shows "set [] = {}"

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

   578   by (auto)

   579 

   580 lemma list2set_RSP:

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

   582   by auto

   583 

   584 definition

   585   rsp_fold

   586 where

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

   588 

   589 primrec

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

   591 where

   592   "fold_raw f z [] = z"

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

   594      (if (rsp_fold f) then

   595        if a mem A then fold_raw f z A

   596        else f a (fold_raw f z A)

   597      else z)"

   598 

   599 lemma mem_lcommuting_fold_raw:

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

   601 sorry

   602 

   603 lemma fold_rsp[quot_respect]:

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

   605 apply(auto)

   606 sorry

   607 

   608 primrec

   609   inter_raw

   610 where

   611   "inter_raw [] B = []"

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

   613 

   614 lemma mem_inter_raw:

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

   616 sorry

   617 

   618 lemma inter_raw_RSP:

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

   620 sorry

   621 

   622 

   623 (* LIFTING DEFS *)

   624 

   625 

   626 section {* Constants on the Quotient Type *} 

   627 

   628 

   629 quotient_definition

   630   "fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset" 

   631   is "delete_raw"

   632 

   633 quotient_definition

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

   635 where

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

   637   is "inter_raw"

   638 

   639 quotient_definition

   640   "ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b" 

   641   is "fold_raw"

   642 

   643 quotient_definition

   644   "fset_to_set :: 'a fset \<Rightarrow> 'a set" 

   645   is "set"

   646 

   647 

   648 section {* Lifted Theorems *}

   649 

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

   651 

   652 thm cons_left_comm

   653 lemma "finsert a (finsert b S) = finsert b (finsert a S)"

   654 by (lifting cons_left_comm)

   655 

   656 thm cons_left_idem

   657 lemma "finsert a (finsert a S) = finsert a S"

   658 by (lifting cons_left_idem)

   659 

   660 (* thm MEM:

   661   MEM x [] = F

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

   663 thm none_mem_nil

   664 (*lemma "(\<forall>a. a \<notin>f A) = (A = fempty)"*)

   665 

   666 thm mem_cons

   667 thm finite_set_raw_strong_cases

   668 (*thm card_raw.simps*)

   669 (*thm not_mem_card_raw*)

   670 (*thm card_raw_suc*)

   671 

   672 lemma "fcard X = Suc n \<Longrightarrow> (\<exists>a S. a \<notin>f S & X = finsert a S)"

   673 (*by (lifting card_raw_suc)*)

   674 sorry

   675 

   676 (*thm card_raw_cons_gt_0

   677 thm mem_card_raw_gt_0

   678 thm not_nil_equiv_cons

   679 *)

   680 thm delete_raw.simps

   681 (*thm mem_delete_raw*)

   682 (*thm card_raw_delete_raw*)

   683 thm cons_delete_raw

   684 thm mem_cons_delete_raw

   685 thm finite_set_raw_delete_raw_cases

   686 thm append.simps

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

   688 thm inter_raw.simps

   689 thm mem_inter_raw

   690 thm fold_raw.simps

   691 thm list2set_thm

   692 thm list_eq_def

   693 thm list.induct

   694 lemma "\<lbrakk>P fempty; \<And>a x. P x \<Longrightarrow> P (finsert a x)\<rbrakk> \<Longrightarrow> P l"

   695 by (lifting list.induct)

   696 

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

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

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

   700 by (lifting append_assoc)

   701 

   702 quotient_definition

   703   "fset_case :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"

   704 is

   705   "list_case"

   706 

   707 (* NOT SURE IF TRUE *)

   708 lemma list_case_rsp[quot_respect]:

   709   "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case"

   710   apply (auto)

   711   sorry

   712 

   713 lemma "fset_case (f1::'t) f2 (finsert a xa) = f2 a xa"

   714 apply (lifting list.cases(2))

   715 done

   716 

   717 end