src/HOL/BNF/BNF_Def.thy
changeset 52719 480a3479fa47
parent 52660 7f7311d04727
child 52730 6bf02eb4ddf7
     1.1 --- a/src/HOL/BNF/BNF_Def.thy	Sun Jul 21 14:02:33 2013 +0200
     1.2 +++ b/src/HOL/BNF/BNF_Def.thy	Mon Jul 22 21:12:15 2013 +0200
     1.3 @@ -197,6 +197,21 @@
     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 +
    1.10 +lemma vimagepI: "R (f x) (g y) \<Longrightarrow> vimagep f g R x y"
    1.11 +  unfolding vimagep_def by -
    1.12 +
    1.13 +lemma vimagepD: "vimagep f g R x y \<Longrightarrow> R (f x) (g y)"
    1.14 +  unfolding vimagep_def by -
    1.15 +
    1.16 +lemma fun_rel_iff_leq_vimagep: "(fun_rel R S) f g = (R \<le> vimagep f g S)"
    1.17 +  unfolding fun_rel_def vimagep_def by auto
    1.18 +
    1.19 +lemma convol_image_vimagep: "<f o fst, g o snd> ` Collect (split (vimagep f g R)) \<subseteq> Collect (split R)"
    1.20 +  unfolding vimagep_def convol_def by auto
    1.21 +
    1.22  ML_file "Tools/bnf_def_tactics.ML"
    1.23  ML_file "Tools/bnf_def.ML"
    1.24