src/HOL/BNF_FP_Base.thy
changeset 55803 74d3fe9031d8
parent 55702 63c80031d8dd
child 55811 aa1acc25126b
     1.1 --- a/src/HOL/BNF_FP_Base.thy	Fri Feb 28 12:04:40 2014 +0100
     1.2 +++ b/src/HOL/BNF_FP_Base.thy	Tue Feb 25 18:14:26 2014 +0100
     1.3 @@ -64,6 +64,11 @@
     1.4  lemma obj_one_pointE: "\<forall>x. s = x \<longrightarrow> P \<Longrightarrow> P"
     1.5  by blast
     1.6  
     1.7 +lemma type_copy_obj_one_point_absE:
     1.8 +  assumes "type_definition Rep Abs UNIV"
     1.9 +  shows "\<forall>x. s = Abs x \<longrightarrow> P \<Longrightarrow> P"
    1.10 +  using type_definition.Rep_inverse[OF assms] by metis
    1.11 +
    1.12  lemma obj_sumE_f:
    1.13  "\<lbrakk>\<forall>x. s = f (Inl x) \<longrightarrow> P; \<forall>x. s = f (Inr x) \<longrightarrow> P\<rbrakk> \<Longrightarrow> \<forall>x. s = f x \<longrightarrow> P"
    1.14  by (rule allI) (metis sumE)
    1.15 @@ -132,7 +137,7 @@
    1.16    unfolding case_sum_o_sum_map id_comp comp_id ..
    1.17  
    1.18  lemma fun_rel_def_butlast:
    1.19 -  "(fun_rel R (fun_rel S T)) f g = (\<forall>x y. R x y \<longrightarrow> (fun_rel S T) (f x) (g y))"
    1.20 +  "fun_rel R (fun_rel S T) f g = (\<forall>x y. R x y \<longrightarrow> (fun_rel S T) (f x) (g y))"
    1.21    unfolding fun_rel_def ..
    1.22  
    1.23  lemma subst_eq_imp: "(\<forall>a b. a = b \<longrightarrow> P a b) \<equiv> (\<forall>a. P a a)"
    1.24 @@ -148,6 +153,30 @@
    1.25     (\<And>x. x \<in> P \<Longrightarrow> f x \<in> Q)"
    1.26    unfolding Grp_def by rule auto
    1.27  
    1.28 +lemma vimage2p_mono: "vimage2p f g R x y \<Longrightarrow> R \<le> S \<Longrightarrow> vimage2p f g S x y"
    1.29 +  unfolding vimage2p_def by blast
    1.30 +
    1.31 +lemma vimage2p_refl: "(\<And>x. R x x) \<Longrightarrow> vimage2p f f R x x"
    1.32 +  unfolding vimage2p_def by auto
    1.33 +
    1.34 +lemma
    1.35 +  assumes "type_definition Rep Abs UNIV"
    1.36 +  shows type_copy_Rep_o_Abs: "Rep \<circ> Abs = id" and type_copy_Abs_o_Rep: "Abs o Rep = id"
    1.37 +  unfolding fun_eq_iff comp_apply id_apply
    1.38 +    type_definition.Abs_inverse[OF assms UNIV_I] type_definition.Rep_inverse[OF assms] by simp_all
    1.39 +
    1.40 +lemma type_copy_map_comp0_undo:
    1.41 +  assumes "type_definition Rep Abs UNIV"
    1.42 +          "type_definition Rep' Abs' UNIV"
    1.43 +          "type_definition Rep'' Abs'' UNIV"
    1.44 +  shows "Abs' o M o Rep'' = (Abs' o M1 o Rep) o (Abs o M2 o Rep'') \<Longrightarrow> M1 o M2 = M"
    1.45 +  by (rule sym) (auto simp: fun_eq_iff type_definition.Abs_inject[OF assms(2) UNIV_I UNIV_I]
    1.46 +    type_definition.Abs_inverse[OF assms(1) UNIV_I]
    1.47 +    type_definition.Abs_inverse[OF assms(3) UNIV_I] dest: spec[of _ "Abs'' x" for x])
    1.48 +
    1.49 +lemma vimage2p_comp: "vimage2p (f1 o f2) (g1 o g2) = vimage2p f2 g2 o vimage2p f1 g1"
    1.50 +  unfolding fun_eq_iff vimage2p_def o_apply by simp
    1.51 +
    1.52  ML_file "Tools/BNF/bnf_fp_util.ML"
    1.53  ML_file "Tools/BNF/bnf_fp_def_sugar_tactics.ML"
    1.54  ML_file "Tools/BNF/bnf_fp_def_sugar.ML"