src/HOL/Library/Combine_PER.thy
 author haftmann Mon Jun 05 15:59:41 2017 +0200 (2017-06-05) changeset 66010 2f7d39285a1a parent 65366 10ca63a18e56 permissions -rw-r--r--
executable domain membership checks
```     1 (*  Author:     Florian Haftmann, TU Muenchen *)
```
```     2
```
```     3 section \<open>A combinator to build partial equivalence relations from a predicate and an equivalence relation\<close>
```
```     4
```
```     5 theory Combine_PER
```
```     6   imports Main Lattice_Syntax
```
```     7 begin
```
```     8
```
```     9 definition combine_per :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
```
```    10   where "combine_per P R = (\<lambda>x y. P x \<and> P y) \<sqinter> R"
```
```    11
```
```    12 lemma combine_per_simp [simp]:
```
```    13   "combine_per P R x y \<longleftrightarrow> P x \<and> P y \<and> x \<approx> y" for R (infixl "\<approx>" 50)
```
```    14   by (simp add: combine_per_def)
```
```    15
```
```    16 lemma combine_per_top [simp]: "combine_per \<top> R = R"
```
```    17   by (simp add: fun_eq_iff)
```
```    18
```
```    19 lemma combine_per_eq [simp]: "combine_per P HOL.eq = HOL.eq \<sqinter> (\<lambda>x y. P x)"
```
```    20   by (auto simp add: fun_eq_iff)
```
```    21
```
```    22 lemma symp_combine_per: "symp R \<Longrightarrow> symp (combine_per P R)"
```
```    23   by (auto simp add: symp_def sym_def combine_per_def)
```
```    24
```
```    25 lemma transp_combine_per: "transp R \<Longrightarrow> transp (combine_per P R)"
```
```    26   by (auto simp add: transp_def trans_def combine_per_def)
```
```    27
```
```    28 lemma combine_perI: "P x \<Longrightarrow> P y \<Longrightarrow> x \<approx> y \<Longrightarrow> combine_per P R x y" for R (infixl "\<approx>" 50)
```
```    29   by (simp add: combine_per_def)
```
```    30
```
```    31 lemma symp_combine_per_symp: "symp R \<Longrightarrow> symp (combine_per P R)"
```
```    32   by (auto intro!: sympI elim: sympE)
```
```    33
```
```    34 lemma transp_combine_per_transp: "transp R \<Longrightarrow> transp (combine_per P R)"
```
```    35   by (auto intro!: transpI elim: transpE)
```
```    36
```
```    37 lemma equivp_combine_per_part_equivp [intro?]:
```
```    38   fixes R (infixl "\<approx>" 50)
```
```    39   assumes "\<exists>x. P x" and "equivp R"
```
```    40   shows "part_equivp (combine_per P R)"
```
```    41 proof -
```
```    42   from \<open>\<exists>x. P x\<close> obtain x where "P x" ..
```
```    43   moreover from \<open>equivp R\<close> have "x \<approx> x"
```
```    44     by (rule equivp_reflp)
```
```    45   ultimately have "\<exists>x. P x \<and> x \<approx> x"
```
```    46     by blast
```
```    47   with \<open>equivp R\<close> show ?thesis
```
```    48     by (auto intro!: part_equivpI symp_combine_per_symp transp_combine_per_transp
```
```    49       elim: equivpE)
```
```    50 qed
```
```    51
```
```    52 end
```