Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Quot/Examples/FSet3.thy
changeset 830 89d772dae4d4
parent 827 dd26fbdee924
child 833 129caba33c03
equal deleted inserted replaced
829:42b90994ac77 830:89d772dae4d4 
    75 
    75 
    76 section {* Augmenting a set -- @{const finsert} *}
 
    76 section {* Augmenting a set -- @{const finsert} *}
 
    77 
    77 
    78 text {* raw section *}
 
    78 text {* raw section *}
 
    79 
    79 
    80 lemma nil_not_cons: 
    80 lemma nil_not_cons:
 
    81   shows "\<not>[] \<approx> x # xs" 
    81   shows "\<not>[] \<approx> x # xs"
 
    82 by auto
 
    82   by auto
 
    83 
    83 
    84 lemma memb_cons_iff:
 
    84 lemma memb_cons_iff:
 
    85   shows "memb x (y # xs) = (x = y \<or> memb x xs)"
 
    85   shows "memb x (y # xs) = (x = y \<or> memb x xs)"
 
    86 by (induct xs) (auto simp add: memb_def)
 
    86   by (induct xs) (auto simp add: memb_def)
 
    87 
    87 
    88 lemma memb_consI1:
 
    88 lemma memb_consI1:
 
    89   shows "memb x (x # xs)"
 
    89   shows "memb x (x # xs)"
 
    90 by (simp add: memb_def)
 
    90   by (simp add: memb_def)
 
    91 
    91 
    92 lemma memb_consI2: 
    92 lemma memb_consI2:
 
    93   shows "memb x xs \<Longrightarrow> memb x (y # xs)"
 
    93   shows "memb x xs \<Longrightarrow> memb x (y # xs)"
 
    94   by (simp add: memb_def)
 
    94   by (simp add: memb_def)
 
    95 
    95 
    96 lemma memb_absorb:
 
    96 lemma memb_absorb:
 
    97   shows "memb x xs \<Longrightarrow> (x # xs) \<approx> xs"
 
    97   shows "memb x xs \<Longrightarrow> x # xs \<approx> xs"
 
    98 by (induct xs) (auto simp add: memb_def)
 
    98   by (induct xs) (auto simp add: memb_def id_simps)
 
    99 
    99 
   100 text {* lifted section *}
 
   100 text {* lifted section *}
 
   101 
       
   102 lemma fempty_not_finsert[simp]:
 
       
   103   shows "{||} \<noteq> finsert x S"
 
       
   104 by (lifting nil_not_cons)
 
       
   105 
   101 
   106 lemma fin_finsert_iff[simp]:
 
   102 lemma fin_finsert_iff[simp]:
 
   107   "x |\<in>| finsert y S = (x = y \<or> x |\<in>| S)"
 
   103   "x |\<in>| finsert y S = (x = y \<or> x |\<in>| S)"
 
   108 by (lifting memb_cons_iff) 
   104 by (lifting memb_cons_iff) 
   109 
   105 
   110 lemma
 
   106 lemma
 
   111   shows finsertI1: "x |\<in>| finsert x S"
 
   107   shows finsertI1: "x |\<in>| finsert x S"
 
   112   and   finsertI2: "x |\<in>| S \<Longrightarrow> x |\<in>| finsert y S"
 
   108   and   finsertI2: "x |\<in>| S \<Longrightarrow> x |\<in>| finsert y S"
 
   113   by (lifting memb_consI1, lifting memb_consI2)
 
   109   by (lifting memb_consI1, lifting memb_consI2)
 
   114 
   110 
       
   111 
   115 lemma finsert_absorb [simp]: 
   112 lemma finsert_absorb [simp]: 
   116   shows "x |\<in>| S \<Longrightarrow> finsert x S = S"
 
   113   shows "x |\<in>| S \<Longrightarrow> finsert x S = S"
 
   117 by (lifting memb_absorb)
 
   114   by (lifting memb_absorb)
 
   118 
   115 
   119 
   116 
   120 section {* Singletons *}
 
   117 section {* Singletons *}
 
   121 
   118 
   122 text {* raw section *}
 
   119 text {* raw section *}
 
   123 
   120 
   124 lemma singleton_list_eq:
 
   121 lemma singleton_list_eq:
 
   125   shows "[x] \<approx> [y] \<longleftrightarrow> x = y"
 
   122   shows "[x] \<approx> [y] \<longleftrightarrow> x = y"
 
   126 by auto
 
   123   by (simp add: id_simps) auto
 
   127 
   124 
   128 text {* lifted section *}
 
   125 text {* lifted section *}
 
       
   126 
       
   127 lemma fempty_not_finsert[simp]:
 
       
   128   shows "{||} \<noteq> finsert x S"
 
       
   129   by (lifting nil_not_cons)
 
   129 
   130 
   130 lemma fsingleton_eq[simp]:
 
   131 lemma fsingleton_eq[simp]:
 
   131   shows "{|x|} = {|y|} \<longleftrightarrow> x = y"
 
   132   shows "{|x|} = {|y|} \<longleftrightarrow> x = y"
 
   132 by (lifting singleton_list_eq)
 
   133   by (lifting singleton_list_eq)
 
   133 
   134 
   134 section {* Union *}
 
   135 section {* Union *}
 
   135 
   136 
   136 quotient_definition
 
   137 quotient_definition
 
   137    "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" (infixl "|\<union>|" 65)
 
   138   "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" (infixl "|\<union>|" 65)
 
   138 as
 
   139 as
 
   139   "op @"
 
   140   "op @"
 
   140 
   141 
   141 section {* Cardinality of finite sets *}
 
   142 section {* Cardinality of finite sets *}
 
   142 
   143 
   242 
   243 
   243 (* PROBLEM: these lemmas needs to be restated, since  *)
 
   244 (* PROBLEM: these lemmas needs to be restated, since  *)
 
   244 (* concat.simps(1) and concat.simps(2) contain the    *)
 
   245 (* concat.simps(1) and concat.simps(2) contain the    *)
 
   245 (* type variables ?'a1.0 (which are turned into frees *)
 
   246 (* type variables ?'a1.0 (which are turned into frees *)
 
   246 (* 'a_1                                               *)
 
   247 (* 'a_1                                               *)
 
   247 lemma concat1: 
   248 lemma concat1:
 
   248   shows "concat [] \<approx> []"
 
   249   shows "concat [] \<approx> []"
 
   249 by (simp)
 
   250 by (simp add: id_simps)
 
   250 
   251 
   251 lemma concat2: 
   252 lemma concat2:
 
   252   shows "concat (x # xs) \<approx>  x @ concat xs"
 
   253   shows "concat (x # xs) \<approx> x @ concat xs"
 
   253 by (simp)
 
   254 by (simp add: id_simps)
 
   254 
   255 
   255 lemma concat_rsp[quot_respect]:
 
   256 lemma concat_rsp[quot_respect]:
 
   256   shows "(list_rel op \<approx> OO op \<approx> OO list_rel op \<approx> ===> op \<approx>) concat concat"
 
   257   shows "(list_rel op \<approx> OO op \<approx> OO list_rel op \<approx> ===> op \<approx>) concat concat"
 
   257 sorry
 
   258 sorry
 
   258 
   259 
   259 lemma nil_rsp2[quot_respect]: "(list_rel op \<approx> OO op \<approx> OO list_rel op \<approx>) [] []"
 
   260 lemma nil_rsp2[quot_respect]: "(list_rel op \<approx> OO op \<approx> OO list_rel op \<approx>) [] []"
 
   260 apply (metis FSet3.nil_rsp list_rel.simps(1) pred_comp.intros)
 
   261   apply (metis FSet3.nil_rsp list_rel.simps(1) pred_comp.intros)
 
   261 done
 
   262   done
 
   262 
   263 
   263 lemma set_in_eq: "(\<forall>e. ((e \<in> A) \<longleftrightarrow> (e \<in> B))) \<equiv> A = B"
 
   264 lemma set_in_eq: "(\<forall>e. ((e \<in> A) \<longleftrightarrow> (e \<in> B))) \<equiv> A = B"
 
   264   apply (rule eq_reflection)
 
   265   apply (rule eq_reflection)
 
   265   apply auto
 
   266   apply auto
 
   266   done
 
   267   done
 
   348 apply(simp add: comp_def)
 
   349 apply(simp add: comp_def)
 
   349 apply(fold fempty_def[simplified id_simps])
 
   350 apply(fold fempty_def[simplified id_simps])
 
   350 apply(rule refl)
 
   351 apply(rule refl)
 
   351 done
 
   352 done
 
   352 
   353 
       
   354 (* Should be true *)
 
       
   355 
       
   356 lemma insert_rsp2[quot_respect]:
 
       
   357   "(op \<approx> ===> list_rel op \<approx> OO op \<approx> OO list_rel op \<approx> ===> list_rel op \<approx> OO op \<approx> OO list_rel op \<approx>) op # op #"
 
       
   358 apply auto
 
       
   359 apply (simp add: set_in_eq)
 
       
   360 sorry
 
       
   361 
       
   362 lemma append_rsp[quot_respect]:
 
       
   363   "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
 
       
   364   by (auto)
 
       
   365 
   353 lemma fconcat_insert:
 
   366 lemma fconcat_insert:
 
   354   shows "fconcat (finsert x S) = x |\<union>| fconcat S"
 
   367   shows "fconcat (finsert x S) = x |\<union>| fconcat S"
 
   355 apply(lifting concat2)
 
   368 apply(lifting concat2)
 
   356 apply(injection)
 
       
   357 (* The Relation is wrong to apply rep_abs_rsp *)
 
       
   358 thm rep_abs_rsp[of "(op \<approx> ===> op =)"]
 
       
   359 defer
 
       
   360 apply (simp only: finsert_def[simplified id_simps])
 
       
   361 apply (simp only: fconcat_def[simplified id_simps])
 
       
   362 apply(cleaning)
 
   369 apply(cleaning)
 
   363 (* finsert_def doesn't get folded, since rep-abs types are incorrect *)
 
   370 apply (simp add: finsert_def fconcat_def comp_def)
 
   364 apply(simp add: comp_def)
 
       
   365 apply (simp add: fconcat_def[simplified id_simps])
 
       
   366 apply cleaning
 
   371 apply cleaning
 
   367 (* The Relation is wrong again. *)
 
   372 done
 
   368 sorry
 
       
   369 
   373 
   370 text {* raw section *}
 
   374 text {* raw section *}
 
   371 
   375 
   372 lemma map_rsp_aux:
 
   376 lemma map_rsp_aux:
 
   373   assumes a: "a \<approx> b"
 
   377   assumes a: "a \<approx> b"
 
   491 
   495 
   492 lemma mem_cons: 
   496 lemma mem_cons: 
   493   "a \<in> set A \<Longrightarrow> a # A \<approx> A"
 
   497   "a \<in> set A \<Longrightarrow> a # A \<approx> A"
 
   494 by auto
 
   498 by auto
 
   495 
   499 
   496 lemma cons_left_comm: 
   500 lemma cons_left_comm:
 
   497   "x #y # A \<approx> y # x # A"
 
   501   "x # y # A \<approx> y # x # A"
 
   498 by auto
 
   502 by (auto simp add: id_simps)
 
   499 
   503 
   500 lemma cons_left_idem: 
   504 lemma cons_left_idem:
 
   501   "x # x # A \<approx> x # A"
 
   505   "x # x # A \<approx> x # A"
 
   502 by auto
 
   506 by (auto simp add: id_simps)
 
   503 
   507 
   504 lemma finite_set_raw_strong_cases:
 
   508 lemma finite_set_raw_strong_cases:
 
   505   "(X = []) \<or> (\<exists>a Y. ((a \<notin> set Y) \<and> (X \<approx> a # Y)))"
 
   509   "(X = []) \<or> (\<exists>a Y. ((a \<notin> set Y) \<and> (X \<approx> a # Y)))"
 
   506   apply (induct X)
 
   510   apply (induct X)
 
   507   apply (simp)
 
   511   apply (simp)
 
   590 
   594 
   591 lemma fold_rsp[quot_respect]:
 
   595 lemma fold_rsp[quot_respect]:
 
   592   "(op = ===> op = ===> op \<approx> ===> op =) fold_raw fold_raw"
 
   596   "(op = ===> op = ===> op \<approx> ===> op =) fold_raw fold_raw"
 
   593 apply(auto)
 
   597 apply(auto)
 
   594 sorry
 
   598 sorry
 
   595 
       
   596 lemma append_rsp[quot_respect]:
 
       
   597   "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
 
       
   598 by auto
 
       
   599 
   599 
   600 primrec
 
   600 primrec
 
   601   inter_raw
 
   601   inter_raw
 
   602 where
 
   602 where
 
   603   "inter_raw [] B = []"
 
   603   "inter_raw [] B = []"
nominal2