author  wenzelm 
Wed, 08 Mar 2017 10:50:59 +0100  
changeset 65151  a7394aa4d21c 
parent 64267  b9a1486e79be 
child 65366  10ca63a18e56 
permissions  rwrr 
63462  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  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  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  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  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  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  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  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  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  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  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  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  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 

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  52 
end 