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.
Nominal/FSet.thy
changeset 2266 dcffc2f132c9
parent 2250 c3fd4e42bb4a
child 2278 337569f85398
equal deleted inserted replaced
2265:9c44db3eef95 2266:dcffc2f132c9 
    78        else f a (ffold_raw f z xs)
 
    78        else f a (ffold_raw f z xs)
 
    79      else z)"
 
    79      else z)"
 
    80 
    80 
    81 text {* Composition Quotient *}
 
    81 text {* Composition Quotient *}
 
    82 
    82 
    83 lemma list_rel_refl:
 
    83 lemma list_rel_refl1:
 
    84   shows "(list_rel op \<approx>) r r"
 
    84   shows "(list_rel op \<approx>) r r"
 
    85   by (rule list_rel_refl) (metis equivp_def fset_equivp)
 
    85   by (rule list_rel_refl) (metis equivp_def fset_equivp)
 
    86 
    86 
    87 lemma compose_list_refl:
 
    87 lemma compose_list_refl:
 
    88   shows "(list_rel op \<approx> OOO op \<approx>) r r"
 
    88   shows "(list_rel op \<approx> OOO op \<approx>) r r"
 
    89 proof
 
    89 proof
 
    90   have *: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp])
 
    90   have *: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp])
 
    91   show "list_rel op \<approx> r r" by (rule list_rel_refl)
 
    91   show "list_rel op \<approx> r r" by (rule list_rel_refl1)
 
    92   with * show "(op \<approx> OO list_rel op \<approx>) r r" ..
 
    92   with * show "(op \<approx> OO list_rel op \<approx>) r r" ..
 
    93 qed
 
    93 qed
 
    94 
    94 
    95 lemma Quotient_fset_list:
 
    95 lemma Quotient_fset_list:
 
    96   shows "Quotient (list_rel op \<approx>) (map abs_fset) (map rep_fset)"
 
    96   shows "Quotient (list_rel op \<approx>) (map abs_fset) (map rep_fset)"
 
   100   by (rule eq_reflection) auto
 
   100   by (rule eq_reflection) auto
 
   101 
   101 
   102 lemma map_rel_cong: "b \<approx> ba \<Longrightarrow> map f b \<approx> map f ba"
 
   102 lemma map_rel_cong: "b \<approx> ba \<Longrightarrow> map f b \<approx> map f ba"
 
   103   unfolding list_eq.simps
 
   103   unfolding list_eq.simps
 
   104   by (simp only: set_map set_in_eq)
 
   104   by (simp only: set_map set_in_eq)
 
       
   105 
   105 
   106 
   106 lemma quotient_compose_list[quot_thm]:
 
   107 lemma quotient_compose_list[quot_thm]:
 
   107   shows  "Quotient ((list_rel op \<approx>) OOO (op \<approx>))
 
   108   shows  "Quotient ((list_rel op \<approx>) OOO (op \<approx>))
 
   108     (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)"
 
   109     (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)"
 
   109   unfolding Quotient_def comp_def
 
   110   unfolding Quotient_def comp_def
 
   110 proof (intro conjI allI)
 
   111 proof (intro conjI allI)
 
   111   fix a r s
 
   112   fix a r s
 
   112   show "abs_fset (map abs_fset (map rep_fset (rep_fset a))) = a"
 
   113   show "abs_fset (map abs_fset (map rep_fset (rep_fset a))) = a"
 
   113     by (simp add: abs_o_rep[OF Quotient_fset] Quotient_abs_rep[OF Quotient_fset] map_id)
 
   114     by (simp add: abs_o_rep[OF Quotient_fset] Quotient_abs_rep[OF Quotient_fset] map_id)
 
   114   have b: "list_rel op \<approx> (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
 
   115   have b: "list_rel op \<approx> (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
 
   115     by (rule list_rel_refl)
 
   116     by (rule list_rel_refl1)
 
   116   have c: "(op \<approx> OO list_rel op \<approx>) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
 
   117   have c: "(op \<approx> OO list_rel op \<approx>) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
 
   117     by (rule, rule equivp_reflp[OF fset_equivp]) (rule b)
 
   118     by (rule, rule equivp_reflp[OF fset_equivp]) (rule b)
 
   118   show "(list_rel op \<approx> OOO op \<approx>) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
 
   119   show "(list_rel op \<approx> OOO op \<approx>) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
 
   119     by (rule, rule list_rel_refl) (rule c)
 
   120     by (rule, rule list_rel_refl1) (rule c)
 
   120   show "(list_rel op \<approx> OOO op \<approx>) r s = ((list_rel op \<approx> OOO op \<approx>) r r \<and>
 
   121   show "(list_rel op \<approx> OOO op \<approx>) r s = ((list_rel op \<approx> OOO op \<approx>) r r \<and>
 
   121         (list_rel op \<approx> OOO op \<approx>) s s \<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s))"
 
   122         (list_rel op \<approx> OOO op \<approx>) s s \<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s))"
 
   122   proof (intro iffI conjI)
 
   123   proof (intro iffI conjI)
 
   123     show "(list_rel op \<approx> OOO op \<approx>) r r" by (rule compose_list_refl)
 
   124     show "(list_rel op \<approx> OOO op \<approx>) r r" by (rule compose_list_refl)
 
   124     show "(list_rel op \<approx> OOO op \<approx>) s s" by (rule compose_list_refl)
 
   125     show "(list_rel op \<approx> OOO op \<approx>) s s" by (rule compose_list_refl)
 
   146     have d: "map abs_fset r \<approx> map abs_fset s"
 
   147     have d: "map abs_fset r \<approx> map abs_fset s"
 
   147       by (subst Quotient_rel[OF Quotient_fset]) (simp add: a)
 
   148       by (subst Quotient_rel[OF Quotient_fset]) (simp add: a)
 
   148     have b: "map rep_fset (map abs_fset r) \<approx> map rep_fset (map abs_fset s)"
 
   149     have b: "map rep_fset (map abs_fset r) \<approx> map rep_fset (map abs_fset s)"
 
   149       by (rule map_rel_cong[OF d])
 
   150       by (rule map_rel_cong[OF d])
 
   150     have y: "list_rel op \<approx> (map rep_fset (map abs_fset s)) s"
 
   151     have y: "list_rel op \<approx> (map rep_fset (map abs_fset s)) s"
 
   151       by (fact rep_abs_rsp_left[OF Quotient_fset_list, OF list_rel_refl[of s]])
 
   152       by (fact rep_abs_rsp_left[OF Quotient_fset_list, OF list_rel_refl1[of s]])
 
   152     have c: "(op \<approx> OO list_rel op \<approx>) (map rep_fset (map abs_fset r)) s"
 
   153     have c: "(op \<approx> OO list_rel op \<approx>) (map rep_fset (map abs_fset r)) s"
 
   153       by (rule pred_compI) (rule b, rule y)
 
   154       by (rule pred_compI) (rule b, rule y)
 
   154     have z: "list_rel op \<approx> r (map rep_fset (map abs_fset r))"
 
   155     have z: "list_rel op \<approx> r (map rep_fset (map abs_fset r))"
 
   155       by (fact rep_abs_rsp[OF Quotient_fset_list, OF list_rel_refl[of r]])
 
   156       by (fact rep_abs_rsp[OF Quotient_fset_list, OF list_rel_refl1[of r]])
 
   156     then show "(list_rel op \<approx> OOO op \<approx>) r s"
 
   157     then show "(list_rel op \<approx> OOO op \<approx>) r s"
 
   157       using a c pred_compI by simp
 
   158       using a c pred_compI by simp
 
   158   qed
 
   159   qed
 
   159 qed
 
   160 qed
 
   160 
   161 
   651 
   652 
   652 lemma append_rsp2_pre0:
 
   653 lemma append_rsp2_pre0:
 
   653   assumes a:"list_rel op \<approx> x x'"
 
   654   assumes a:"list_rel op \<approx> x x'"
 
   654   shows "list_rel op \<approx> (x @ z) (x' @ z)"
 
   655   shows "list_rel op \<approx> (x @ z) (x' @ z)"
 
   655   using a apply (induct x x' rule: list_induct2')
 
   656   using a apply (induct x x' rule: list_induct2')
 
   656   by simp_all (rule list_rel_refl)
 
   657   by simp_all (rule list_rel_refl1)
 
   657 
   658 
   658 lemma append_rsp2_pre1:
 
   659 lemma append_rsp2_pre1:
 
   659   assumes a:"list_rel op \<approx> x x'"
 
   660   assumes a:"list_rel op \<approx> x x'"
 
   660   shows "list_rel op \<approx> (z @ x) (z @ x')"
 
   661   shows "list_rel op \<approx> (z @ x) (z @ x')"
 
   661   using a apply (induct x x' arbitrary: z rule: list_induct2')
 
   662   using a apply (induct x x' arbitrary: z rule: list_induct2')
 
   662   apply (rule list_rel_refl)
 
   663   apply (rule list_rel_refl1)
 
   663   apply (simp_all del: list_eq.simps)
 
   664   apply (simp_all del: list_eq.simps)
 
   664   apply (rule list_rel_app_l)
 
   665   apply (rule list_rel_app_l)
 
   665   apply (simp_all add: reflp_def)
 
   666   apply (simp_all add: reflp_def)
 
   666   done
 
   667   done
 
   667 
   668 
   672   apply (rule list_rel_transp[OF fset_equivp])
 
   673   apply (rule list_rel_transp[OF fset_equivp])
 
   673   apply (rule append_rsp2_pre0)
 
   674   apply (rule append_rsp2_pre0)
 
   674   apply (rule a)
 
   675   apply (rule a)
 
   675   using b apply (induct z z' rule: list_induct2')
 
   676   using b apply (induct z z' rule: list_induct2')
 
   676   apply (simp_all only: append_Nil2)
 
   677   apply (simp_all only: append_Nil2)
 
   677   apply (rule list_rel_refl)
 
   678   apply (rule list_rel_refl1)
 
   678   apply simp_all
 
   679   apply simp_all
 
   679   apply (rule append_rsp2_pre1)
 
   680   apply (rule append_rsp2_pre1)
 
   680   apply simp
 
   681   apply simp
 
   681   done
 
   682   done
 
   682 
   683 
  1411 
  1412 
  1412 ML {*
 
  1413 ML {*
 
  1413 fun dest_fsetT (Type (@{type_name fset}, [T])) = T
 
  1414 fun dest_fsetT (Type (@{type_name fset}, [T])) = T
 
  1414   | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
 
  1415   | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
 
  1415 *}
 
  1416 *}
 
  1416 
       
  1417 no_notation
 
       
  1418   list_eq (infix "\<approx>" 50)
 
       
  1419 
  1417 
  1420 ML {*
 
  1418 ML {*
 
  1421 open Quotient_Info;
 
  1419 open Quotient_Info;
 
  1422 
  1420 
  1423 exception LIFT_MATCH of string
 
  1421 exception LIFT_MATCH of string
 
  1676 apply rule
 
  1674 apply rule
 
  1677 apply (rule ball_reg_right)
 
  1675 apply (rule ball_reg_right)
 
  1678 apply auto
 
  1676 apply auto
 
  1679 done
 
  1677 done
 
  1680 
  1678 
       
  1679 lemma list_rel_refl:
 
       
  1680   assumes q: "equivp R"
 
       
  1681   shows "(list_rel R) r r"
 
       
  1682   by (rule list_rel_refl) (metis equivp_def fset_equivp q)
 
       
  1683 
       
  1684 lemma compose_list_refl2:
 
       
  1685   assumes q: "equivp R"
 
       
  1686   shows "(list_rel R OOO op \<approx>) r r"
 
       
  1687 proof
 
       
  1688   have *: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp])
 
       
  1689   show "list_rel R r r" by (rule list_rel_refl[OF q])
 
       
  1690   with * show "(op \<approx> OO list_rel R) r r" ..
 
       
  1691 qed
 
       
  1692 
       
  1693 lemma quotient_compose_list_g[quot_thm]:
 
       
  1694   assumes q: "Quotient R Abs Rep"
 
       
  1695   and     e: "equivp R"
 
       
  1696   shows  "Quotient ((list_rel R) OOO (op \<approx>))
 
       
  1697     (abs_fset \<circ> (map Abs)) ((map Rep) \<circ> rep_fset)"
 
       
  1698   unfolding Quotient_def comp_def
 
       
  1699 proof (intro conjI allI)
 
       
  1700   fix a r s
 
       
  1701   show "abs_fset (map Abs (map Rep (rep_fset a))) = a"
 
       
  1702     by (simp add: abs_o_rep[OF q] Quotient_abs_rep[OF Quotient_fset] map_id)
 
       
  1703   have b: "list_rel R (map Rep (rep_fset a)) (map Rep (rep_fset a))"
 
       
  1704     by (rule list_rel_refl[OF e])
 
       
  1705   have c: "(op \<approx> OO list_rel R) (map Rep (rep_fset a)) (map Rep (rep_fset a))"
 
       
  1706     by (rule, rule equivp_reflp[OF fset_equivp]) (rule b)
 
       
  1707   show "(list_rel R OOO op \<approx>) (map Rep (rep_fset a)) (map Rep (rep_fset a))"
 
       
  1708     by (rule, rule list_rel_refl[OF e]) (rule c)
 
       
  1709   show "(list_rel R OOO op \<approx>) r s = ((list_rel R OOO op \<approx>) r r \<and>
 
       
  1710         (list_rel R OOO op \<approx>) s s \<and> abs_fset (map Abs r) = abs_fset (map Abs s))"
 
       
  1711   proof (intro iffI conjI)
 
       
  1712     show "(list_rel R OOO op \<approx>) r r" by (rule compose_list_refl2[OF e])
 
       
  1713     show "(list_rel R OOO op \<approx>) s s" by (rule compose_list_refl2[OF e])
 
       
  1714   next
 
       
  1715     assume a: "(list_rel R OOO op \<approx>) r s"
 
       
  1716     then have b: "map Abs r \<approx> map Abs s"
 
       
  1717     proof (elim pred_compE)
 
       
  1718       fix b ba
 
       
  1719       assume c: "list_rel R r b"
 
       
  1720       assume d: "b \<approx> ba"
 
       
  1721       assume e: "list_rel R ba s"
 
       
  1722       have f: "map Abs r = map Abs b"
 
       
  1723         using Quotient_rel[OF list_quotient[OF q]] c by blast
 
       
  1724       have "map Abs ba = map Abs s"
 
       
  1725         using Quotient_rel[OF list_quotient[OF q]] e by blast
 
       
  1726       then have g: "map Abs s = map Abs ba" by simp
 
       
  1727       then show "map Abs r \<approx> map Abs s" using d f map_rel_cong by simp
 
       
  1728     qed
 
       
  1729     then show "abs_fset (map Abs r) = abs_fset (map Abs s)"
 
       
  1730       using Quotient_rel[OF Quotient_fset] by blast
 
       
  1731   next
 
       
  1732     assume a: "(list_rel R OOO op \<approx>) r r \<and> (list_rel R OOO op \<approx>) s s
 
       
  1733       \<and> abs_fset (map Abs r) = abs_fset (map Abs s)"
 
       
  1734     then have s: "(list_rel R OOO op \<approx>) s s" by simp
 
       
  1735     have d: "map Abs r \<approx> map Abs s"
 
       
  1736       by (subst Quotient_rel[OF Quotient_fset]) (simp add: a)
 
       
  1737     have b: "map Rep (map Abs r) \<approx> map Rep (map Abs s)"
 
       
  1738       by (rule map_rel_cong[OF d])
 
       
  1739     have y: "list_rel R (map Rep (map Abs s)) s"
 
       
  1740       by (fact rep_abs_rsp_left[OF list_quotient[OF q], OF list_rel_refl[OF e, of s]])
 
       
  1741     have c: "(op \<approx> OO list_rel R) (map Rep (map Abs r)) s"
 
       
  1742       by (rule pred_compI) (rule b, rule y)
 
       
  1743     have z: "list_rel R r (map Rep (map Abs r))"
 
       
  1744       by (fact rep_abs_rsp[OF list_quotient[OF q], OF list_rel_refl[OF e, of r]])
 
       
  1745     then show "(list_rel R OOO op \<approx>) r s"
 
       
  1746       using a c pred_compI by simp
 
       
  1747   qed
 
       
  1748 qed
 
       
  1749 
       
  1750 no_notation
 
       
  1751   list_eq (infix "\<approx>" 50)
 
       
  1752 
       
  1753 
  1681 end
 
  1754 end
nominal2