Nominal/FSet.thy
changeset 2532 22c37deb3dac
parent 2531 8054f4988672
child 2533 767161329839
equal deleted inserted replaced
2531:8054f4988672 2532:22c37deb3dac
   158 lemma set_fminus_raw[simp]: 
   158 lemma set_fminus_raw[simp]: 
   159   "set (fminus_raw xs ys) = (set xs - set ys)"
   159   "set (fminus_raw xs ys) = (set xs - set ys)"
   160   by (induct ys arbitrary: xs) (auto)
   160   by (induct ys arbitrary: xs) (auto)
   161 
   161 
   162 
   162 
   163 text {* Respectfullness *}
   163 text {* Respectfulness *}
   164 
   164 
   165 lemma append_rsp[quot_respect]:
   165 lemma append_rsp[quot_respect]:
   166   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) append append"
   166   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) append append"
   167   by (simp)
   167   by (simp)
   168 
   168 
   297   qed
   297   qed
   298   then show "concat a \<approx> concat b" by auto
   298   then show "concat a \<approx> concat b" by auto
   299 qed
   299 qed
   300 
   300 
   301 lemma [quot_respect]:
   301 lemma [quot_respect]:
   302   shows "((op =) ===> op \<approx> ===> op \<approx>) filter filter"
   302   shows "(op = ===> op \<approx> ===> op \<approx>) filter filter"
   303   by auto
   303   by auto
   304 
   304 
   305 text {* Distributive lattice with bot *}
   305 text {* Distributive lattice with bot *}
   306 
   306 
   307 lemma append_inter_distrib:
   307 lemma append_inter_distrib: