src/HOL/Library/Combine_PER.thy
author wenzelm
Wed, 08 Mar 2017 10:50:59 +0100
changeset 65151 a7394aa4d21c
parent 64267 b9a1486e79be
child 65366 10ca63a18e56
permissions -rw-r--r--
tuned proofs;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63415
diff changeset
     1
(*  Author:     Florian Haftmann, TU Muenchen *)
63377
64adf4ba9526 combinator to build partial equivalence relations from a predicate and an equivalenc relation
haftmann
parents:
diff changeset
     2
64adf4ba9526 combinator to build partial equivalence relations from a predicate and an equivalenc relation
haftmann
parents:
diff changeset
     3
section \<open>A combinator to build partial equivalence relations from a predicate and an equivalence relation\<close>
64adf4ba9526 combinator to build partial equivalence relations from a predicate and an equivalenc relation
haftmann
parents:
diff changeset
     4
64adf4ba9526 combinator to build partial equivalence relations from a predicate and an equivalenc relation
haftmann
parents:
diff changeset
     5
theory Combine_PER
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63415
diff changeset
     6
  imports Main "~~/src/HOL/Library/Lattice_Syntax"
63377
64adf4ba9526 combinator to build partial equivalence relations from a predicate and an equivalenc relation
haftmann
parents:
diff changeset
     7
begin
64adf4ba9526 combinator to build partial equivalence relations from a predicate and an equivalenc relation
haftmann
parents:
diff changeset
     8
64adf4ba9526 combinator to build partial equivalence relations from a predicate and an equivalenc relation
haftmann
parents:
diff changeset
     9
definition combine_per :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63415
diff changeset
    10
  where "combine_per P R = (\<lambda>x y. P x \<and> P y) \<sqinter> R"
63377
64adf4ba9526 combinator to build partial equivalence relations from a predicate and an equivalenc relation
haftmann
parents:
diff changeset
    11
64adf4ba9526 combinator to build partial equivalence relations from a predicate and an equivalenc relation
haftmann
parents:
diff changeset
    12
lemma combine_per_simp [simp]:
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63415
diff changeset
    13
  "combine_per P R x y \<longleftrightarrow> P x \<and> P y \<and> x \<approx> y" for R (infixl "\<approx>" 50)
63377
64adf4ba9526 combinator to build partial equivalence relations from a predicate and an equivalenc relation
haftmann
parents:
diff changeset
    14
  by (simp add: combine_per_def)
64adf4ba9526 combinator to build partial equivalence relations from a predicate and an equivalenc relation
haftmann
parents:
diff changeset
    15
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63415
diff changeset
    16
lemma combine_per_top [simp]: "combine_per \<top> R = R"
63377
64adf4ba9526 combinator to build partial equivalence relations from a predicate and an equivalenc relation
haftmann
parents:
diff changeset
    17
  by (simp add: fun_eq_iff)
64adf4ba9526 combinator to build partial equivalence relations from a predicate and an equivalenc relation
haftmann
parents:
diff changeset
    18
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63415
diff changeset
    19
lemma combine_per_eq [simp]: "combine_per P HOL.eq = HOL.eq \<sqinter> (\<lambda>x y. P x)"
63377
64adf4ba9526 combinator to build partial equivalence relations from a predicate and an equivalenc relation
haftmann
parents:
diff changeset
    20
  by (auto simp add: fun_eq_iff)
64adf4ba9526 combinator to build partial equivalence relations from a predicate and an equivalenc relation
haftmann
parents:
diff changeset
    21
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63415
diff changeset
    22
lemma symp_combine_per: "symp R \<Longrightarrow> symp (combine_per P R)"
63377
64adf4ba9526 combinator to build partial equivalence relations from a predicate and an equivalenc relation
haftmann
parents:
diff changeset
    23
  by (auto simp add: symp_def sym_def combine_per_def)
64adf4ba9526 combinator to build partial equivalence relations from a predicate and an equivalenc relation
haftmann
parents:
diff changeset
    24
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63415
diff changeset
    25
lemma transp_combine_per: "transp R \<Longrightarrow> transp (combine_per P R)"
63377
64adf4ba9526 combinator to build partial equivalence relations from a predicate and an equivalenc relation
haftmann
parents:
diff changeset
    26
  by (auto simp add: transp_def trans_def combine_per_def)
64adf4ba9526 combinator to build partial equivalence relations from a predicate and an equivalenc relation
haftmann
parents:
diff changeset
    27
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63415
diff changeset
    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)
63377
64adf4ba9526 combinator to build partial equivalence relations from a predicate and an equivalenc relation
haftmann
parents:
diff changeset
    29
  by (simp add: combine_per_def)
64adf4ba9526 combinator to build partial equivalence relations from a predicate and an equivalenc relation
haftmann
parents:
diff changeset
    30
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63415
diff changeset
    31
lemma symp_combine_per_symp: "symp R \<Longrightarrow> symp (combine_per P R)"
63377
64adf4ba9526 combinator to build partial equivalence relations from a predicate and an equivalenc relation
haftmann
parents:
diff changeset
    32
  by (auto intro!: sympI elim: sympE)
64adf4ba9526 combinator to build partial equivalence relations from a predicate and an equivalenc relation
haftmann
parents:
diff changeset
    33
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63415
diff changeset
    34
lemma transp_combine_per_transp: "transp R \<Longrightarrow> transp (combine_per P R)"
63377
64adf4ba9526 combinator to build partial equivalence relations from a predicate and an equivalenc relation
haftmann
parents:
diff changeset
    35
  by (auto intro!: transpI elim: transpE)
64adf4ba9526 combinator to build partial equivalence relations from a predicate and an equivalenc relation
haftmann
parents:
diff changeset
    36
63415
8f91c2f447a0 default rule for single-step reasoning
haftmann
parents: 63377
diff changeset
    37
lemma equivp_combine_per_part_equivp [intro?]:
63377
64adf4ba9526 combinator to build partial equivalence relations from a predicate and an equivalenc relation
haftmann
parents:
diff changeset
    38
  fixes R (infixl "\<approx>" 50)
64adf4ba9526 combinator to build partial equivalence relations from a predicate and an equivalenc relation
haftmann
parents:
diff changeset
    39
  assumes "\<exists>x. P x" and "equivp R"
64adf4ba9526 combinator to build partial equivalence relations from a predicate and an equivalenc relation
haftmann
parents:
diff changeset
    40
  shows "part_equivp (combine_per P R)"
64adf4ba9526 combinator to build partial equivalence relations from a predicate and an equivalenc relation
haftmann
parents:
diff changeset
    41
proof -
64adf4ba9526 combinator to build partial equivalence relations from a predicate and an equivalenc relation
haftmann
parents:
diff changeset
    42
  from \<open>\<exists>x. P x\<close> obtain x where "P x" ..
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63415
diff changeset
    43
  moreover from \<open>equivp R\<close> have "x \<approx> x"
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63415
diff changeset
    44
    by (rule equivp_reflp)
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63415
diff changeset
    45
  ultimately have "\<exists>x. P x \<and> x \<approx> x"
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63415
diff changeset
    46
    by blast
63377
64adf4ba9526 combinator to build partial equivalence relations from a predicate and an equivalenc relation
haftmann
parents:
diff changeset
    47
  with \<open>equivp R\<close> show ?thesis
64adf4ba9526 combinator to build partial equivalence relations from a predicate and an equivalenc relation
haftmann
parents:
diff changeset
    48
    by (auto intro!: part_equivpI symp_combine_per_symp transp_combine_per_transp
64adf4ba9526 combinator to build partial equivalence relations from a predicate and an equivalenc relation
haftmann
parents:
diff changeset
    49
      elim: equivpE)
64adf4ba9526 combinator to build partial equivalence relations from a predicate and an equivalenc relation
haftmann
parents:
diff changeset
    50
qed
64adf4ba9526 combinator to build partial equivalence relations from a predicate and an equivalenc relation
haftmann
parents:
diff changeset
    51
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63462
diff changeset
    52
end