fun_rel introduction and list_rel elimination for quotient package
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Thu Apr 22 11:55:19 2010 +0200 (2010-04-22)
changeset 3627692011cc923f5
parent 36275 c6ca9e258269
child 36277 9be4ab2acc13
child 36278 6b330b1fa0c0
fun_rel introduction and list_rel elimination for quotient package
src/HOL/Library/Quotient_List.thy
src/HOL/Quotient.thy
     1.1 --- a/src/HOL/Library/Quotient_List.thy	Thu Apr 22 09:30:39 2010 +0200
     1.2 +++ b/src/HOL/Library/Quotient_List.thy	Thu Apr 22 11:55:19 2010 +0200
     1.3 @@ -271,6 +271,15 @@
     1.4    apply(simp_all)
     1.5    done
     1.6  
     1.7 +lemma list_rel_find_element:
     1.8 +  assumes a: "x \<in> set a"
     1.9 +  and b: "list_rel R a b"
    1.10 +  shows "\<exists>y. (y \<in> set b \<and> R x y)"
    1.11 +proof -
    1.12 +  have "length a = length b" using b by (rule list_rel_len)
    1.13 +  then show ?thesis using a b by (induct a b rule: list_induct2) auto
    1.14 +qed
    1.15 +
    1.16  lemma list_rel_refl:
    1.17    assumes a: "\<And>x y. R x y = (R x = R y)"
    1.18    shows "list_rel R x x"
     2.1 --- a/src/HOL/Quotient.thy	Thu Apr 22 09:30:39 2010 +0200
     2.2 +++ b/src/HOL/Quotient.thy	Thu Apr 22 11:55:19 2010 +0200
     2.3 @@ -106,6 +106,10 @@
     2.4  where
     2.5  [simp]: "fun_rel E1 E2 f g = (\<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))"
     2.6  
     2.7 +lemma fun_relI [intro]:
     2.8 +  assumes "\<And>a b. P a b \<Longrightarrow> Q (x a) (y b)"
     2.9 +  shows "(P ===> Q) x y"
    2.10 +  using assms by (simp add: fun_rel_def)
    2.11  
    2.12  lemma fun_map_id:
    2.13    shows "(id ---> id) = id"