src/HOL/BNF_Least_Fixpoint.thy
changeset 62905 52c5a25e0c96
parent 60758 d8d85a8172b5
child 62906 75ca185db27f
     1.1 --- a/src/HOL/BNF_Least_Fixpoint.thy	Thu Apr 07 17:26:22 2016 +0200
     1.2 +++ b/src/HOL/BNF_Least_Fixpoint.thy	Thu Apr 07 17:56:22 2016 +0200
     1.3 @@ -40,26 +40,6 @@
     1.4  lemma FieldI2: "(i, j) \<in> R \<Longrightarrow> j \<in> Field R"
     1.5    unfolding Field_def by auto
     1.6  
     1.7 -lemma fst_convol': "fst (\<langle>f, g\<rangle> x) = f x"
     1.8 -  using fst_convol unfolding convol_def by simp
     1.9 -
    1.10 -lemma snd_convol': "snd (\<langle>f, g\<rangle> x) = g x"
    1.11 -  using snd_convol unfolding convol_def by simp
    1.12 -
    1.13 -lemma convol_expand_snd: "fst o f = g \<Longrightarrow> \<langle>g, snd o f\<rangle> = f"
    1.14 -  unfolding convol_def by auto
    1.15 -
    1.16 -lemma convol_expand_snd':
    1.17 -  assumes "(fst o f = g)"
    1.18 -  shows "h = snd o f \<longleftrightarrow> \<langle>g, h\<rangle> = f"
    1.19 -proof -
    1.20 -  from assms have *: "\<langle>g, snd o f\<rangle> = f" by (rule convol_expand_snd)
    1.21 -  then have "h = snd o f \<longleftrightarrow> h = snd o \<langle>g, snd o f\<rangle>" by simp
    1.22 -  moreover have "\<dots> \<longleftrightarrow> h = snd o f" by (simp add: snd_convol)
    1.23 -  moreover have "\<dots> \<longleftrightarrow> \<langle>g, h\<rangle> = f" by (subst (2) *[symmetric]) (auto simp: convol_def fun_eq_iff)
    1.24 -  ultimately show ?thesis by simp
    1.25 -qed
    1.26 -
    1.27  lemma bij_betwE: "bij_betw f A B \<Longrightarrow> \<forall>a\<in>A. f a \<in> B"
    1.28    unfolding bij_betw_def by auto
    1.29  
    1.30 @@ -172,19 +152,6 @@
    1.31  lemma predicate2D_vimage2p: "\<lbrakk>R \<le> vimage2p f g S; R x y\<rbrakk> \<Longrightarrow> S (f x) (g y)"
    1.32    unfolding vimage2p_def by auto
    1.33  
    1.34 -lemma id_transfer: "rel_fun A A id id"
    1.35 -  unfolding rel_fun_def by simp
    1.36 -
    1.37 -lemma fst_transfer: "rel_fun (rel_prod A B) A fst fst"
    1.38 -  unfolding rel_fun_def by simp
    1.39 -
    1.40 -lemma snd_transfer: "rel_fun (rel_prod A B) B snd snd"
    1.41 -  unfolding rel_fun_def by simp
    1.42 -
    1.43 -lemma convol_transfer:
    1.44 -  "rel_fun (rel_fun R S) (rel_fun (rel_fun R T) (rel_fun R (rel_prod S T))) BNF_Def.convol BNF_Def.convol"
    1.45 -  unfolding rel_fun_def convol_def by auto
    1.46 -
    1.47  lemma ssubst_Pair_rhs: "\<lbrakk>(r, s) \<in> R; s' = s\<rbrakk> \<Longrightarrow> (r, s') \<in> R"
    1.48    by (rule ssubst)
    1.49