src/HOL/BNF/BNF_Def.thy
changeset 52731 dacd47a0633f
parent 52730 6bf02eb4ddf7
child 52749 ed416f4ac34e
     1.1 --- a/src/HOL/BNF/BNF_Def.thy	Thu Jul 25 12:25:07 2013 +0200
     1.2 +++ b/src/HOL/BNF/BNF_Def.thy	Thu Jul 25 16:46:53 2013 +0200
     1.3 @@ -193,20 +193,20 @@
     1.4    ((\<lambda>i. if i \<in> g ` C then the_inv_into C g i else x) o g) i = id i"
     1.5  unfolding Func_def by (auto elim: the_inv_into_f_f)
     1.6  
     1.7 -definition vimagep where
     1.8 -  "vimagep f g R = (\<lambda>x y. R (f x) (g y))"
     1.9 +definition vimage2p where
    1.10 +  "vimage2p f g R = (\<lambda>x y. R (f x) (g y))"
    1.11  
    1.12 -lemma vimagepI: "R (f x) (g y) \<Longrightarrow> vimagep f g R x y"
    1.13 -  unfolding vimagep_def by -
    1.14 +lemma vimage2pI: "R (f x) (g y) \<Longrightarrow> vimage2p f g R x y"
    1.15 +  unfolding vimage2p_def by -
    1.16  
    1.17 -lemma vimagepD: "vimagep f g R x y \<Longrightarrow> R (f x) (g y)"
    1.18 -  unfolding vimagep_def by -
    1.19 +lemma vimage2pD: "vimage2p f g R x y \<Longrightarrow> R (f x) (g y)"
    1.20 +  unfolding vimage2p_def by -
    1.21  
    1.22 -lemma fun_rel_iff_leq_vimagep: "(fun_rel R S) f g = (R \<le> vimagep f g S)"
    1.23 -  unfolding fun_rel_def vimagep_def by auto
    1.24 +lemma fun_rel_iff_leq_vimage2p: "(fun_rel R S) f g = (R \<le> vimage2p f g S)"
    1.25 +  unfolding fun_rel_def vimage2p_def by auto
    1.26  
    1.27 -lemma convol_image_vimagep: "<f o fst, g o snd> ` Collect (split (vimagep f g R)) \<subseteq> Collect (split R)"
    1.28 -  unfolding vimagep_def convol_def by auto
    1.29 +lemma convol_image_vimage2p: "<f o fst, g o snd> ` Collect (split (vimage2p f g R)) \<subseteq> Collect (split R)"
    1.30 +  unfolding vimage2p_def convol_def by auto
    1.31  
    1.32  ML_file "Tools/bnf_def_tactics.ML"
    1.33  ML_file "Tools/bnf_def.ML"