src/HOL/Library/Combine_PER.thy
 author haftmann Fri Mar 22 19:18:08 2019 +0000 (4 months ago) changeset 69946 494934c30f38 parent 65366 10ca63a18e56 permissions -rw-r--r--
improved code equations taken over from AFP
 wenzelm@63462 ` 1` ```(* Author: Florian Haftmann, TU Muenchen *) ``` haftmann@63377 ` 2` haftmann@63377 ` 3` ```section \A combinator to build partial equivalence relations from a predicate and an equivalence relation\ ``` haftmann@63377 ` 4` haftmann@63377 ` 5` ```theory Combine_PER ``` wenzelm@65366 ` 6` ``` imports Main Lattice_Syntax ``` haftmann@63377 ` 7` ```begin ``` haftmann@63377 ` 8` haftmann@63377 ` 9` ```definition combine_per :: "('a \ bool) \ ('a \ 'a \ bool) \ 'a \ 'a \ bool" ``` wenzelm@63462 ` 10` ``` where "combine_per P R = (\x y. P x \ P y) \ R" ``` haftmann@63377 ` 11` haftmann@63377 ` 12` ```lemma combine_per_simp [simp]: ``` wenzelm@63462 ` 13` ``` "combine_per P R x y \ P x \ P y \ x \ y" for R (infixl "\" 50) ``` haftmann@63377 ` 14` ``` by (simp add: combine_per_def) ``` haftmann@63377 ` 15` wenzelm@63462 ` 16` ```lemma combine_per_top [simp]: "combine_per \ R = R" ``` haftmann@63377 ` 17` ``` by (simp add: fun_eq_iff) ``` haftmann@63377 ` 18` wenzelm@63462 ` 19` ```lemma combine_per_eq [simp]: "combine_per P HOL.eq = HOL.eq \ (\x y. P x)" ``` haftmann@63377 ` 20` ``` by (auto simp add: fun_eq_iff) ``` haftmann@63377 ` 21` wenzelm@63462 ` 22` ```lemma symp_combine_per: "symp R \ symp (combine_per P R)" ``` haftmann@63377 ` 23` ``` by (auto simp add: symp_def sym_def combine_per_def) ``` haftmann@63377 ` 24` wenzelm@63462 ` 25` ```lemma transp_combine_per: "transp R \ transp (combine_per P R)" ``` haftmann@63377 ` 26` ``` by (auto simp add: transp_def trans_def combine_per_def) ``` haftmann@63377 ` 27` wenzelm@63462 ` 28` ```lemma combine_perI: "P x \ P y \ x \ y \ combine_per P R x y" for R (infixl "\" 50) ``` haftmann@63377 ` 29` ``` by (simp add: combine_per_def) ``` haftmann@63377 ` 30` wenzelm@63462 ` 31` ```lemma symp_combine_per_symp: "symp R \ symp (combine_per P R)" ``` haftmann@63377 ` 32` ``` by (auto intro!: sympI elim: sympE) ``` haftmann@63377 ` 33` wenzelm@63462 ` 34` ```lemma transp_combine_per_transp: "transp R \ transp (combine_per P R)" ``` haftmann@63377 ` 35` ``` by (auto intro!: transpI elim: transpE) ``` haftmann@63377 ` 36` haftmann@63415 ` 37` ```lemma equivp_combine_per_part_equivp [intro?]: ``` haftmann@63377 ` 38` ``` fixes R (infixl "\" 50) ``` haftmann@63377 ` 39` ``` assumes "\x. P x" and "equivp R" ``` haftmann@63377 ` 40` ``` shows "part_equivp (combine_per P R)" ``` haftmann@63377 ` 41` ```proof - ``` haftmann@63377 ` 42` ``` from \\x. P x\ obtain x where "P x" .. ``` wenzelm@63462 ` 43` ``` moreover from \equivp R\ have "x \ x" ``` wenzelm@63462 ` 44` ``` by (rule equivp_reflp) ``` wenzelm@63462 ` 45` ``` ultimately have "\x. P x \ x \ x" ``` wenzelm@63462 ` 46` ``` by blast ``` haftmann@63377 ` 47` ``` with \equivp R\ show ?thesis ``` haftmann@63377 ` 48` ``` by (auto intro!: part_equivpI symp_combine_per_symp transp_combine_per_transp ``` haftmann@63377 ` 49` ``` elim: equivpE) ``` haftmann@63377 ` 50` ```qed ``` haftmann@63377 ` 51` nipkow@64267 ` 52` ```end ```