1 theory FSet

     2 imports "../Quotient" "../Quotient_List" "../Quotient_Product" 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   apply(auto intro: list_eq.intros list_eq_refl)

    23   done

    24 

    25 quotient_type 

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

    27   by (rule equivp_list_eq)

    28 

    29 quotient_definition

    30    "EMPTY :: 'a fset"

    31 is

    32   "[]::'a list"

    33 

    34 quotient_definition

    35    "INSERT :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"

    36 is

    37   "op #"

    38 

    39 quotient_definition

    40    "FUNION :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"

    41 is

    42   "op @"

    43 

    44 fun

    45   card1 :: "'a list \<Rightarrow> nat"

    46 where

    47   card1_nil: "(card1 []) = 0"

    48 | card1_cons: "(card1 (x # xs)) = (if (x mem xs) then (card1 xs) else (Suc (card1 xs)))"

    49 

    50 quotient_definition

    51    "CARD :: 'a fset \<Rightarrow> nat"

    52 is

    53   "card1"

    54 

    55 quotient_definition

    56   "fconcat :: ('a fset) fset \<Rightarrow> 'a fset"

    57 is

    58   "concat"

    59 

    60 term concat

    61 term fconcat

    62 

    63 text {*

    64  Maybe make_const_def should require a theorem that says that the particular lifted function

    65  respects the relation. With it such a definition would be impossible:

    66  make_const_def CARD @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd

    67 *}

    68 

    69 lemma card1_0:

    70   fixes a :: "'a list"

    71   shows "(card1 a = 0) = (a = [])"

    72   by (induct a) auto

    73 

    74 lemma not_mem_card1:

    75   fixes x :: "'a"

    76   fixes xs :: "'a list"

    77   shows "(~(x mem xs)) = (card1 (x # xs) = Suc (card1 xs))"

    78   by auto

    79 

    80 lemma mem_cons:

    81   fixes x :: "'a"

    82   fixes xs :: "'a list"

    83   assumes a : "x mem xs"

    84   shows "x # xs \<approx> xs"

    85   using a by (induct xs) (auto intro: list_eq.intros )

    86 

    87 lemma card1_suc:

    88   fixes xs :: "'a list"

    89   fixes n :: "nat"

    90   assumes c: "card1 xs = Suc n"

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

    92   using c

    93 apply(induct xs)

    94 apply (metis Suc_neq_Zero card1_0)

    95 apply (metis FSet.card1_cons list_eq.intros(6) list_eq_refl mem_cons)

    96 done

    97 

    98 definition

    99   rsp_fold

   100 where

   101   "rsp_fold f = ((!u v. (f u v = f v u)) \<and> (!u v w. ((f u (f v w) = f (f u v) w))))"

   102 

   103 primrec

   104   fold1

   105 where

   106   "fold1 f (g :: 'a \<Rightarrow> 'b) (z :: 'b) [] = z"

   107 | "fold1 f g z (a # A) =

   108      (if rsp_fold f

   109      then (

   110        if (a mem A) then (fold1 f g z A) else (f (g a) (fold1 f g z A))

   111      ) else z)"

   112 

   113 lemma fs1_strong_cases:

   114   fixes X :: "'a list"

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

   116   apply (induct X)

   117   apply (simp)

   118   apply (metis List.member.simps(1) list_eq.intros(6) list_eq_refl mem_cons)

   119   done

   120 

   121 quotient_definition

   122    "IN :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool"

   123 is

   124   "op mem"

   125 

   126 quotient_definition

   127    "FOLD :: ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b fset \<Rightarrow> 'a"

   128 is

   129   "fold1"

   130 

   131 quotient_definition

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

   133 is

   134   "map"

   135 

   136 lemma mem_rsp:

   137   fixes z

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

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

   140   using a by induct auto

   141 

   142 lemma ho_memb_rsp[quot_respect]:

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

   144   by (simp add: mem_rsp)

   145 

   146 lemma card1_rsp:

   147   fixes a b :: "'a list"

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

   149   shows "card1 a = card1 b"

   150   using e by induct (simp_all add: mem_rsp)

   151 

   152 lemma ho_card1_rsp[quot_respect]: 

   153   "(op \<approx> ===> op =) card1 card1"

   154   by (simp add: card1_rsp)

   155 

   156 lemma cons_rsp:

   157   fixes z

   158   assumes a: "xs \<approx> ys"

   159   shows "(z # xs) \<approx> (z # ys)"

   160   using a by (rule list_eq.intros(5))

   161 

   162 lemma ho_cons_rsp[quot_respect]:

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

   164   by (simp add: cons_rsp)

   165 

   166 lemma append_rsp_aux1:

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

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

   169 using a

   170 apply(induct h)

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

   172 done

   173 

   174 lemma append_rsp_aux2:

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

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

   177 using a

   178 apply(induct arbitrary: l2 r2)

   179 apply(simp_all)

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

   181 done

   182 

   183 lemma append_rsp[quot_respect]:

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

   185   by (auto simp add: append_rsp_aux2)

   186 

   187 lemma map_rsp:

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

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

   190   using a

   191   apply (induct)

   192   apply(auto intro: list_eq.intros)

   193   done

   194 

   195 lemma ho_map_rsp[quot_respect]:

   196   "(op = ===> op \<approx> ===> op \<approx>) map map"

   197   by (simp add: map_rsp)

   198 

   199 lemma map_append:

   200   "(map f (a @ b)) \<approx> (map f a) @ (map f b)"

   201  by simp (rule list_eq_refl)

   202 

   203 lemma ho_fold_rsp[quot_respect]:

   204   "(op = ===> op = ===> op = ===> op \<approx> ===> op =) fold1 fold1"

   205   apply (auto)

   206   apply (case_tac "rsp_fold x")

   207   prefer 2

   208   apply (erule_tac list_eq.induct)

   209   apply (simp_all)

   210   apply (erule_tac list_eq.induct)

   211   apply (simp_all)

   212   apply (auto simp add: mem_rsp rsp_fold_def)

   213 done

   214 

   215 lemma list_equiv_rsp[quot_respect]:

   216   shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"

   217 by (auto intro: list_eq.intros)

   218 

   219 lemma "IN x EMPTY = False"

   220 apply(lifting member.simps(1))

   221 done

   222 

   223 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)"

   224 apply (lifting member.simps(2))

   225 done

   226 

   227 lemma "INSERT a (INSERT a x) = INSERT a x"

   228 apply (lifting list_eq.intros(4))

   229 done

   230 

   231 lemma "x = xa \<Longrightarrow> INSERT a x = INSERT a xa"

   232 apply (lifting list_eq.intros(5))

   233 done

   234 

   235 lemma "CARD x = Suc n \<Longrightarrow> (\<exists>a b. \<not> IN a b & x = INSERT a b)"

   236 apply (lifting card1_suc)

   237 done

   238 

   239 lemma "(\<not> IN x xa) = (CARD (INSERT x xa) = Suc (CARD xa))"

   240 apply (lifting not_mem_card1)

   241 done

   242 

   243 lemma "FOLD f g (z::'b) (INSERT a x) =

   244   (if rsp_fold f then if IN a x then FOLD f g z x else f (g a) (FOLD f g z x) else z)"

   245 apply(lifting fold1.simps(2))

   246 done

   247 

   248 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"

   249 apply (lifting map_append)

   250 done

   251 

   252 lemma "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)"

   253 apply (lifting append_assoc)

   254 done

   255 

   256 

   257 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"

   258 apply(lifting list.induct)

   259 done

   260 

   261 lemma list_induct_part:

   262   assumes a: "P (x :: 'a list) ([] :: 'c list)"

   263   assumes b: "\<And>e t. P x t \<Longrightarrow> P x (e # t)"

   264   shows "P x l"

   265   apply (rule_tac P="P x" in list.induct)

   266   apply (rule a)

   267   apply (rule b)

   268   apply (assumption)

   269   done

   270 

   271 lemma "P (x :: 'a list) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"

   272 apply (lifting list_induct_part)

   273 done

   274 

   275 lemma "P (x :: 'a fset) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"

   276 apply (lifting list_induct_part)

   277 done

   278 

   279 lemma "P (x :: 'a fset) ([] :: 'c list) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (e # t)) \<Longrightarrow> P x l"

   280 apply (lifting list_induct_part)

   281 done

   282 

   283 quotient_type 'a fset2 = "'a list" / "list_eq"

   284   by (rule equivp_list_eq)

   285 

   286 quotient_definition

   287    "EMPTY2 :: 'a fset2"

   288 is

   289   "[]::'a list"

   290 

   291 quotient_definition

   292    "INSERT2 :: 'a \<Rightarrow> 'a fset2 \<Rightarrow> 'a fset2"

   293 is

   294   "op #"

   295 

   296 lemma "P (x :: 'a fset2) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"

   297 apply (lifting list_induct_part)

   298 done

   299 

   300 lemma "P (x :: 'a fset) (EMPTY2 :: 'c fset2) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT2 e t)) \<Longrightarrow> P x l"

   301 apply (lifting list_induct_part)

   302 done

   303 

   304 quotient_definition

   305   "fset_rec :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"

   306 is

   307   "list_rec"

   308 

   309 quotient_definition

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

   311 is

   312   "list_case"

   313 

   314 (* Probably not true without additional assumptions about the function *)

   315 lemma list_rec_rsp[quot_respect]:

   316   "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_rec list_rec"

   317   apply (auto)

   318   apply (erule_tac list_eq.induct)

   319   apply (simp_all)

   320   sorry

   321 

   322 lemma list_case_rsp[quot_respect]:

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

   324   apply (auto)

   325   sorry

   326 

   327 lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"

   328 apply (lifting list.recs(2))

   329 done

   330 

   331 lemma "fset_case (f1::'t) f2 (INSERT a xa) = f2 a xa"

   332 apply (lifting list.cases(2))

   333 done

   334 

   335 lemma ttt: "((op @) x ((op #) e [])) = (((op #) e x))"

   336 sorry

   337 

   338 lemma "(FUNION x (INSERT e EMPTY)) = ((INSERT e x))"

   339 apply (lifting ttt)

   340 done

   341 

   342 

   343 lemma ttt2: "(\<lambda>e. ((op @) x ((op #) e []))) = (\<lambda>e. ((op #) e x))"

   344 sorry

   345 

   346 lemma "(\<lambda>e. (FUNION x (INSERT e EMPTY))) = (\<lambda>e. (INSERT e x))"

   347 apply(lifting ttt2)

   348 apply(regularize)

   349 apply(rule impI)

   350 apply(simp)

   351 apply(rule allI)

   352 apply(rule list_eq_refl)

   353 done

   354 

   355 lemma ttt3: "(\<lambda>x. ((op @) x (e # []))) = (op #) e"

   356 sorry

   357 

   358 lemma "(\<lambda>x. (FUNION x (INSERT e EMPTY))) = INSERT e"

   359 apply(lifting ttt3)

   360 apply(regularize)

   361 apply(auto simp add: cons_rsp)

   362 done

   363 lemma hard: "(\<lambda>P. \<lambda>Q. P (Q (x::'a list))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a list)))"

   364 sorry

   365 

   366 lemma eq_imp_rel:

   367   shows "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b"

   368   by (simp add: equivp_reflp)

   369 

   370 

   371 lemma hard_lift: "(\<lambda>P. \<lambda>Q. P (Q (x::'a fset))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a fset)))"

   372 apply(lifting hard)

   373 apply(regularize)

   374 apply(rule fun_rel_id_asm)

   375 apply(subst babs_simp)

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

   377 apply(rule fun_rel_id_asm)

   378 apply(rule impI)

   379 apply(rule mp[OF eq_imp_rel[OF fset_equivp]])

   380 apply(drule fun_cong)

   381 apply(drule fun_cong)

   382 apply(assumption)

   383 done

   384 

   385 lemma test: "All (\<lambda>(x::'a list, y). x = y)"

   386 sorry

   387 

   388 lemma  "All (\<lambda>(x::'a fset, y). x = y)"

   389 apply(lifting test)

   390 done

   391 

   392 lemma test2: "Ex (\<lambda>(x::'a list, y). x = y)"

   393 sorry

   394 

   395 lemma  "Ex (\<lambda>(x::'a fset, y). x = y)"

   396 apply(lifting test2)

   397 done

   398 

   399 lemma test3: "All (\<lambda> (x :: 'a list, y, z). x = y \<and> y = z)"

   400 sorry

   401 

   402 lemma "All (\<lambda> (x :: 'a fset, y, z). x = y \<and> y = z)"

   403 apply(lifting test3)

   404 done

   405 

   406 lemma test4: "\<forall> (x :: 'a list, y, z) \<in> Respects(

   407   prod_rel (op \<approx>) (prod_rel (op \<approx>) (op \<approx>))

   408 ). x = y \<and> y = z"

   409 sorry

   410 

   411 lemma "All (\<lambda> (x :: 'a fset, y, z). x = y \<and> y = z)"

   412 apply (lifting test4)

   413 sorry

   414 

   415 lemma test5: "\<forall> (x :: 'a list \<Rightarrow> 'a list, y) \<in> Respects(

   416   prod_rel (op \<approx> ===> op \<approx>) (op \<approx> ===> op \<approx>)

   417 ). (op \<approx> ===> op \<approx>) x y"

   418 sorry

   419 

   420 lemma "All (\<lambda> (x :: 'a fset \<Rightarrow> 'a fset, y). x = y)"

   421 apply (lifting test5)

   422 done

   423 

   424 lemma test6: "\<forall> (x :: 'a list \<Rightarrow> 'a list, y, z) \<in> Respects(

   425   prod_rel (op \<approx> ===> op \<approx>) (prod_rel (op \<approx> ===> op \<approx>) (op \<approx> ===> op \<approx>))

   426 ). (op \<approx> ===> op \<approx>) x y \<and> (op \<approx> ===> op \<approx>) y z"

   427 sorry

   428 

   429 lemma "All (\<lambda> (x :: 'a fset \<Rightarrow> 'a fset, y, z). x = y \<and> y = z)"

   430 apply (lifting test6)

   431 done

   432 

   433 end