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 2544 3b24b5d2b68c
parent 2543 8537493c039f
child 2546 3a7155fce1da
equal deleted inserted replaced
2543:8537493c039f 2544:3b24b5d2b68c 
    67 
    67 
    68 
    68 
    69 section {* Quotient composition lemmas *}
 
    69 section {* Quotient composition lemmas *}
 
    70 
    70 
    71 lemma list_all2_refl':
 
    71 lemma list_all2_refl':
 
    72   shows "(list_all2 op \<approx>) r r"
 
    72   assumes q: "equivp R"
 
    73   by (rule list_all2_refl) (metis equivp_def fset_equivp)
 
    73   shows "(list_all2 R) r r"
 
       
    74   by (rule list_all2_refl) (metis equivp_def q)
 
    74 
    75 
    75 lemma compose_list_refl:
 
    76 lemma compose_list_refl:
 
    76   shows "(list_all2 op \<approx> OOO op \<approx>) r r"
 
    77   assumes q: "equivp R"
 
       
    78   shows "(list_all2 R OOO op \<approx>) r r"
 
    77 proof
 
    79 proof
 
    78   have *: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp])
 
    80   have *: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp])
 
    79   show "list_all2 op \<approx> r r" by (rule list_all2_refl')
 
    81   show "list_all2 R r r" by (rule list_all2_refl'[OF q])
 
    80   with * show "(op \<approx> OO list_all2 op \<approx>) r r" ..
 
    82   with * show "(op \<approx> OO list_all2 R) r r" ..
 
    81 qed
 
    83 qed
 
    82 
       
    83 lemma Quotient_fset_list:
 
       
    84   shows "Quotient (list_all2 op \<approx>) (map abs_fset) (map rep_fset)"
 
       
    85   by (fact list_quotient[OF Quotient_fset])
 
       
    86 
    84 
    87 lemma map_list_eq_cong: "b \<approx> ba \<Longrightarrow> map f b \<approx> map f ba"
 
    85 lemma map_list_eq_cong: "b \<approx> ba \<Longrightarrow> map f b \<approx> map f ba"
 
    88   unfolding list_eq.simps
 
    86   unfolding list_eq.simps
 
    89   by (simp only: set_map)
 
    87   by (simp only: set_map)
 
    90 
    88 
       
    89 lemma quotient_compose_list_g:
 
       
    90   assumes q: "Quotient R Abs Rep"
 
       
    91   and     e: "equivp R"
 
       
    92   shows  "Quotient ((list_all2 R) OOO (op \<approx>))
 
       
    93     (abs_fset \<circ> (map Abs)) ((map Rep) \<circ> rep_fset)"
 
       
    94   unfolding Quotient_def comp_def
 
       
    95 proof (intro conjI allI)
 
       
    96   fix a r s
 
       
    97   show "abs_fset (map Abs (map Rep (rep_fset a))) = a"
 
       
    98     by (simp add: abs_o_rep[OF q] Quotient_abs_rep[OF Quotient_fset] map_id)
 
       
    99   have b: "list_all2 R (map Rep (rep_fset a)) (map Rep (rep_fset a))"
 
       
   100     by (rule list_all2_refl'[OF e])
 
       
   101   have c: "(op \<approx> OO list_all2 R) (map Rep (rep_fset a)) (map Rep (rep_fset a))"
 
       
   102     by (rule, rule equivp_reflp[OF fset_equivp]) (rule b)
 
       
   103   show "(list_all2 R OOO op \<approx>) (map Rep (rep_fset a)) (map Rep (rep_fset a))"
 
       
   104     by (rule, rule list_all2_refl'[OF e]) (rule c)
 
       
   105   show "(list_all2 R OOO op \<approx>) r s = ((list_all2 R OOO op \<approx>) r r \<and>
 
       
   106         (list_all2 R OOO op \<approx>) s s \<and> abs_fset (map Abs r) = abs_fset (map Abs s))"
 
       
   107   proof (intro iffI conjI)
 
       
   108     show "(list_all2 R OOO op \<approx>) r r" by (rule compose_list_refl[OF e])
 
       
   109     show "(list_all2 R OOO op \<approx>) s s" by (rule compose_list_refl[OF e])
 
       
   110   next
 
       
   111     assume a: "(list_all2 R OOO op \<approx>) r s"
 
       
   112     then have b: "map Abs r \<approx> map Abs s"
 
       
   113     proof (elim pred_compE)
 
       
   114       fix b ba
 
       
   115       assume c: "list_all2 R r b"
 
       
   116       assume d: "b \<approx> ba"
 
       
   117       assume e: "list_all2 R ba s"
 
       
   118       have f: "map Abs r = map Abs b"
 
       
   119         using Quotient_rel[OF list_quotient[OF q]] c by blast
 
       
   120       have "map Abs ba = map Abs s"
 
       
   121         using Quotient_rel[OF list_quotient[OF q]] e by blast
 
       
   122       then have g: "map Abs s = map Abs ba" by simp
 
       
   123       then show "map Abs r \<approx> map Abs s" using d f map_list_eq_cong by simp
 
       
   124     qed
 
       
   125     then show "abs_fset (map Abs r) = abs_fset (map Abs s)"
 
       
   126       using Quotient_rel[OF Quotient_fset] by blast
 
       
   127   next
 
       
   128     assume a: "(list_all2 R OOO op \<approx>) r r \<and> (list_all2 R OOO op \<approx>) s s
 
       
   129       \<and> abs_fset (map Abs r) = abs_fset (map Abs s)"
 
       
   130     then have s: "(list_all2 R OOO op \<approx>) s s" by simp
 
       
   131     have d: "map Abs r \<approx> map Abs s"
 
       
   132       by (subst Quotient_rel[OF Quotient_fset]) (simp add: a)
 
       
   133     have b: "map Rep (map Abs r) \<approx> map Rep (map Abs s)"
 
       
   134       by (rule map_list_eq_cong[OF d])
 
       
   135     have y: "list_all2 R (map Rep (map Abs s)) s"
 
       
   136       by (fact rep_abs_rsp_left[OF list_quotient[OF q], OF list_all2_refl'[OF e, of s]])
 
       
   137     have c: "(op \<approx> OO list_all2 R) (map Rep (map Abs r)) s"
 
       
   138       by (rule pred_compI) (rule b, rule y)
 
       
   139     have z: "list_all2 R r (map Rep (map Abs r))"
 
       
   140       by (fact rep_abs_rsp[OF list_quotient[OF q], OF list_all2_refl'[OF e, of r]])
 
       
   141     then show "(list_all2 R OOO op \<approx>) r s"
 
       
   142       using a c pred_compI by simp
 
       
   143   qed
 
       
   144 qed
 
       
   145 
    91 lemma quotient_compose_list[quot_thm]:
 
   146 lemma quotient_compose_list[quot_thm]:
 
    92   shows  "Quotient ((list_all2 op \<approx>) OOO (op \<approx>))
 
   147   shows  "Quotient ((list_all2 op \<approx>) OOO (op \<approx>))
 
    93     (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)"
 
   148     (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)"
 
    94   unfolding Quotient_def comp_def
 
   149   by (rule quotient_compose_list_g, rule Quotient_fset, rule list_eq_equivp)
 
    95 proof (intro conjI allI)
 
       
    96   fix a r s
 
       
    97   show "abs_fset (map abs_fset (map rep_fset (rep_fset a))) = a"
 
       
    98     by (simp add: abs_o_rep[OF Quotient_fset] Quotient_abs_rep[OF Quotient_fset] map_id)
 
       
    99   have b: "list_all2 op \<approx> (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
 
       
   100     by (rule list_all2_refl')
 
       
   101   have c: "(op \<approx> OO list_all2 op \<approx>) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
 
       
   102     by (rule, rule equivp_reflp[OF fset_equivp]) (rule b)
 
       
   103   show "(list_all2 op \<approx> OOO op \<approx>) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
 
       
   104     by (rule, rule list_all2_refl') (rule c)
 
       
   105   show "(list_all2 op \<approx> OOO op \<approx>) r s = ((list_all2 op \<approx> OOO op \<approx>) r r \<and>
 
       
   106         (list_all2 op \<approx> OOO op \<approx>) s s \<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s))"
 
       
   107   proof (intro iffI conjI)
 
       
   108     show "(list_all2 op \<approx> OOO op \<approx>) r r" by (rule compose_list_refl)
 
       
   109     show "(list_all2 op \<approx> OOO op \<approx>) s s" by (rule compose_list_refl)
 
       
   110   next
 
       
   111     assume a: "(list_all2 op \<approx> OOO op \<approx>) r s"
 
       
   112     then have b: "map abs_fset r \<approx> map abs_fset s"
 
       
   113     proof (elim pred_compE)
 
       
   114       fix b ba
 
       
   115       assume c: "list_all2 op \<approx> r b"
 
       
   116       assume d: "b \<approx> ba"
 
       
   117       assume e: "list_all2 op \<approx> ba s"
 
       
   118       have f: "map abs_fset r = map abs_fset b"
 
       
   119         using Quotient_rel[OF Quotient_fset_list] c by blast
 
       
   120       have "map abs_fset ba = map abs_fset s"
 
       
   121         using Quotient_rel[OF Quotient_fset_list] e by blast
 
       
   122       then have g: "map abs_fset s = map abs_fset ba" by simp
 
       
   123       then show "map abs_fset r \<approx> map abs_fset s" using d f map_list_eq_cong by simp
 
       
   124     qed
 
       
   125     then show "abs_fset (map abs_fset r) = abs_fset (map abs_fset s)"
 
       
   126       using Quotient_rel[OF Quotient_fset] by blast
 
       
   127   next
 
       
   128     assume a: "(list_all2 op \<approx> OOO op \<approx>) r r \<and> (list_all2 op \<approx> OOO op \<approx>) s s
 
       
   129       \<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s)"
 
       
   130     then have s: "(list_all2 op \<approx> OOO op \<approx>) s s" by simp
 
       
   131     have d: "map abs_fset r \<approx> map abs_fset s"
 
       
   132       by (subst Quotient_rel[OF Quotient_fset]) (simp add: a)
 
       
   133     have b: "map rep_fset (map abs_fset r) \<approx> map rep_fset (map abs_fset s)"
 
       
   134       by (rule map_list_eq_cong[OF d])
 
       
   135     have y: "list_all2 op \<approx> (map rep_fset (map abs_fset s)) s"
 
       
   136       by (fact rep_abs_rsp_left[OF Quotient_fset_list, OF list_all2_refl'[of s]])
 
       
   137     have c: "(op \<approx> OO list_all2 op \<approx>) (map rep_fset (map abs_fset r)) s"
 
       
   138       by (rule pred_compI) (rule b, rule y)
 
       
   139     have z: "list_all2 op \<approx> r (map rep_fset (map abs_fset r))"
 
       
   140       by (fact rep_abs_rsp[OF Quotient_fset_list, OF list_all2_refl'[of r]])
 
       
   141     then show "(list_all2 op \<approx> OOO op \<approx>) r s"
 
       
   142       using a c pred_compI by simp
 
       
   143   qed
 
       
   144 qed
 
       
   145 
       
   146 
   150 
   147 subsection {* Respectfulness lemmas for list operations *}
 
   151 subsection {* Respectfulness lemmas for list operations *}
 
   148 
   152 
   149 lemma list_equiv_rsp [quot_respect]:
 
   153 lemma list_equiv_rsp [quot_respect]:
 
   150   shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
 
   154   shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
 
   432 
   436 
   433 subsection {* Compositional respectfulness and preservation lemmas *}
 
   437 subsection {* Compositional respectfulness and preservation lemmas *}
 
   434 
   438 
   435 lemma Nil_rsp2 [quot_respect]: 
   439 lemma Nil_rsp2 [quot_respect]: 
   436   shows "(list_all2 op \<approx> OOO op \<approx>) Nil Nil"
 
   440   shows "(list_all2 op \<approx> OOO op \<approx>) Nil Nil"
 
   437   by (fact compose_list_refl)
 
   441   by (rule compose_list_refl, rule list_eq_equivp)
 
   438 
   442 
   439 lemma Cons_rsp2 [quot_respect]:
 
   443 lemma Cons_rsp2 [quot_respect]:
 
   440   shows "(op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) Cons Cons"
 
   444   shows "(op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) Cons Cons"
 
   441   apply auto
 
   445   apply auto
 
   442   apply (rule_tac b="x # b" in pred_compI)
 
   446   apply (rule_tac b="x # b" in pred_compI)
 
   468 
   472 
   469 lemma append_rsp2_pre0:
 
   473 lemma append_rsp2_pre0:
 
   470   assumes a:"list_all2 op \<approx> x x'"
 
   474   assumes a:"list_all2 op \<approx> x x'"
 
   471   shows "list_all2 op \<approx> (x @ z) (x' @ z)"
 
   475   shows "list_all2 op \<approx> (x @ z) (x' @ z)"
 
   472   using a apply (induct x x' rule: list_induct2')
 
   476   using a apply (induct x x' rule: list_induct2')
 
   473   by simp_all (rule list_all2_refl')
 
   477   by simp_all (rule list_all2_refl'[OF list_eq_equivp])
 
   474 
   478 
   475 lemma append_rsp2_pre1:
 
   479 lemma append_rsp2_pre1:
 
   476   assumes a:"list_all2 op \<approx> x x'"
 
   480   assumes a:"list_all2 op \<approx> x x'"
 
   477   shows "list_all2 op \<approx> (z @ x) (z @ x')"
 
   481   shows "list_all2 op \<approx> (z @ x) (z @ x')"
 
   478   using a apply (induct x x' arbitrary: z rule: list_induct2')
 
   482   using a apply (induct x x' arbitrary: z rule: list_induct2')
 
   479   apply (rule list_all2_refl')
 
   483   apply (rule list_all2_refl'[OF list_eq_equivp])
 
   480   apply (simp_all del: list_eq.simps)
 
   484   apply (simp_all del: list_eq.simps)
 
   481   apply (rule list_all2_app_l)
 
   485   apply (rule list_all2_app_l)
 
   482   apply (simp_all add: reflp_def)
 
   486   apply (simp_all add: reflp_def)
 
   483   done
 
   487   done
 
   484 
   488 
   489   apply (rule list_all2_transp[OF fset_equivp])
 
   493   apply (rule list_all2_transp[OF fset_equivp])
 
   490   apply (rule append_rsp2_pre0)
 
   494   apply (rule append_rsp2_pre0)
 
   491   apply (rule a)
 
   495   apply (rule a)
 
   492   using b apply (induct z z' rule: list_induct2')
 
   496   using b apply (induct z z' rule: list_induct2')
 
   493   apply (simp_all only: append_Nil2)
 
   497   apply (simp_all only: append_Nil2)
 
   494   apply (rule list_all2_refl')
 
   498   apply (rule list_all2_refl'[OF list_eq_equivp])
 
   495   apply simp_all
 
   499   apply simp_all
 
   496   apply (rule append_rsp2_pre1)
 
   500   apply (rule append_rsp2_pre1)
 
   497   apply simp
 
   501   apply simp
 
   498   done
 
   502   done
 
   499 
   503 
  1138   and "\<And>xs1 xs2 xs3. \<lbrakk>xs1 = xs2; P xs1 xs2; xs2 = xs3; P xs2 xs3\<rbrakk> \<Longrightarrow> P xs1 xs3"
 
  1142   and "\<And>xs1 xs2 xs3. \<lbrakk>xs1 = xs2; P xs1 xs2; xs2 = xs3; P xs2 xs3\<rbrakk> \<Longrightarrow> P xs1 xs3"
 
  1139   shows "P x1 x2"
 
  1143   shows "P x1 x2"
 
  1140   using assms
 
  1144   using assms
 
  1141   by (lifting list_eq2.induct[simplified list_eq2_equiv[symmetric]])
 
  1145   by (lifting list_eq2.induct[simplified list_eq2_equiv[symmetric]])
 
  1142 
  1146 
  1143 lemma list_all2_refl'':
 
       
  1144   assumes q: "equivp R"
 
       
  1145   shows "(list_all2 R) r r"
 
       
  1146   by (rule list_all2_refl) (metis equivp_def q)
 
       
  1147 
       
  1148 lemma compose_list_refl2:
 
       
  1149   assumes q: "equivp R"
 
       
  1150   shows "(list_all2 R OOO op \<approx>) r r"
 
       
  1151 proof
 
       
  1152   have *: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp])
 
       
  1153   show "list_all2 R r r" by (rule list_all2_refl''[OF q])
 
       
  1154   with * show "(op \<approx> OO list_all2 R) r r" ..
 
       
  1155 qed
 
       
  1156 
       
  1157 lemma quotient_compose_list_g:
 
       
  1158   assumes q: "Quotient R Abs Rep"
 
       
  1159   and     e: "equivp R"
 
       
  1160   shows  "Quotient ((list_all2 R) OOO (op \<approx>))
 
       
  1161     (abs_fset \<circ> (map Abs)) ((map Rep) \<circ> rep_fset)"
 
       
  1162   unfolding Quotient_def comp_def
 
       
  1163 proof (intro conjI allI)
 
       
  1164   fix a r s
 
       
  1165   show "abs_fset (map Abs (map Rep (rep_fset a))) = a"
 
       
  1166     by (simp add: abs_o_rep[OF q] Quotient_abs_rep[OF Quotient_fset] map_id)
 
       
  1167   have b: "list_all2 R (map Rep (rep_fset a)) (map Rep (rep_fset a))"
 
       
  1168     by (rule list_all2_refl''[OF e])
 
       
  1169   have c: "(op \<approx> OO list_all2 R) (map Rep (rep_fset a)) (map Rep (rep_fset a))"
 
       
  1170     by (rule, rule equivp_reflp[OF fset_equivp]) (rule b)
 
       
  1171   show "(list_all2 R OOO op \<approx>) (map Rep (rep_fset a)) (map Rep (rep_fset a))"
 
       
  1172     by (rule, rule list_all2_refl''[OF e]) (rule c)
 
       
  1173   show "(list_all2 R OOO op \<approx>) r s = ((list_all2 R OOO op \<approx>) r r \<and>
 
       
  1174         (list_all2 R OOO op \<approx>) s s \<and> abs_fset (map Abs r) = abs_fset (map Abs s))"
 
       
  1175   proof (intro iffI conjI)
 
       
  1176     show "(list_all2 R OOO op \<approx>) r r" by (rule compose_list_refl2[OF e])
 
       
  1177     show "(list_all2 R OOO op \<approx>) s s" by (rule compose_list_refl2[OF e])
 
       
  1178   next
 
       
  1179     assume a: "(list_all2 R OOO op \<approx>) r s"
 
       
  1180     then have b: "map Abs r \<approx> map Abs s"
 
       
  1181     proof (elim pred_compE)
 
       
  1182       fix b ba
 
       
  1183       assume c: "list_all2 R r b"
 
       
  1184       assume d: "b \<approx> ba"
 
       
  1185       assume e: "list_all2 R ba s"
 
       
  1186       have f: "map Abs r = map Abs b"
 
       
  1187         using Quotient_rel[OF list_quotient[OF q]] c by blast
 
       
  1188       have "map Abs ba = map Abs s"
 
       
  1189         using Quotient_rel[OF list_quotient[OF q]] e by blast
 
       
  1190       then have g: "map Abs s = map Abs ba" by simp
 
       
  1191       then show "map Abs r \<approx> map Abs s" using d f map_list_eq_cong by simp
 
       
  1192     qed
 
       
  1193     then show "abs_fset (map Abs r) = abs_fset (map Abs s)"
 
       
  1194       using Quotient_rel[OF Quotient_fset] by blast
 
       
  1195   next
 
       
  1196     assume a: "(list_all2 R OOO op \<approx>) r r \<and> (list_all2 R OOO op \<approx>) s s
 
       
  1197       \<and> abs_fset (map Abs r) = abs_fset (map Abs s)"
 
       
  1198     then have s: "(list_all2 R OOO op \<approx>) s s" by simp
 
       
  1199     have d: "map Abs r \<approx> map Abs s"
 
       
  1200       by (subst Quotient_rel[OF Quotient_fset]) (simp add: a)
 
       
  1201     have b: "map Rep (map Abs r) \<approx> map Rep (map Abs s)"
 
       
  1202       by (rule map_list_eq_cong[OF d])
 
       
  1203     have y: "list_all2 R (map Rep (map Abs s)) s"
 
       
  1204       by (fact rep_abs_rsp_left[OF list_quotient[OF q], OF list_all2_refl''[OF e, of s]])
 
       
  1205     have c: "(op \<approx> OO list_all2 R) (map Rep (map Abs r)) s"
 
       
  1206       by (rule pred_compI) (rule b, rule y)
 
       
  1207     have z: "list_all2 R r (map Rep (map Abs r))"
 
       
  1208       by (fact rep_abs_rsp[OF list_quotient[OF q], OF list_all2_refl''[OF e, of r]])
 
       
  1209     then show "(list_all2 R OOO op \<approx>) r s"
 
       
  1210       using a c pred_compI by simp
 
       
  1211   qed
 
       
  1212 qed
 
       
  1213 
       
  1214 
       
  1215 ML {*
 
  1147 ML {*
 
  1216 fun dest_fsetT (Type (@{type_name fset}, [T])) = T
 
  1148 fun dest_fsetT (Type (@{type_name fset}, [T])) = T
 
  1217   | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
 
  1149   | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
 
  1218 *}
 
  1150 *}
 
  1219 
  1151
nominal2