src/HOL/Library/Combine_PER.thy
author haftmann
Wed Jul 18 20:51:21 2018 +0200 (11 months ago)
changeset 68658 16cc1161ad7f
parent 65366 10ca63a18e56
permissions -rw-r--r--
tuned equation
wenzelm@63462
     1
(*  Author:     Florian Haftmann, TU Muenchen *)
haftmann@63377
     2
haftmann@63377
     3
section \<open>A combinator to build partial equivalence relations from a predicate and an equivalence relation\<close>
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 \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
wenzelm@63462
    10
  where "combine_per P R = (\<lambda>x y. P x \<and> P y) \<sqinter> R"
haftmann@63377
    11
haftmann@63377
    12
lemma combine_per_simp [simp]:
wenzelm@63462
    13
  "combine_per P R x y \<longleftrightarrow> P x \<and> P y \<and> x \<approx> y" for R (infixl "\<approx>" 50)
haftmann@63377
    14
  by (simp add: combine_per_def)
haftmann@63377
    15
wenzelm@63462
    16
lemma combine_per_top [simp]: "combine_per \<top> 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 \<sqinter> (\<lambda>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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> P y \<Longrightarrow> x \<approx> y \<Longrightarrow> combine_per P R x y" for R (infixl "\<approx>" 50)
haftmann@63377
    29
  by (simp add: combine_per_def)
haftmann@63377
    30
wenzelm@63462
    31
lemma symp_combine_per_symp: "symp R \<Longrightarrow> 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 \<Longrightarrow> 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 "\<approx>" 50)
haftmann@63377
    39
  assumes "\<exists>x. P x" and "equivp R"
haftmann@63377
    40
  shows "part_equivp (combine_per P R)"
haftmann@63377
    41
proof -
haftmann@63377
    42
  from \<open>\<exists>x. P x\<close> obtain x where "P x" ..
wenzelm@63462
    43
  moreover from \<open>equivp R\<close> have "x \<approx> x"
wenzelm@63462
    44
    by (rule equivp_reflp)
wenzelm@63462
    45
  ultimately have "\<exists>x. P x \<and> x \<approx> x"
wenzelm@63462
    46
    by blast
haftmann@63377
    47
  with \<open>equivp R\<close> 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