src/HOL/BNF_LFP.thy
changeset 57641 dc59f147b27d
parent 57493 554592fb795a
child 57698 afef6616cbae
     1.1 --- a/src/HOL/BNF_LFP.thy	Thu Jul 24 11:51:22 2014 +0200
     1.2 +++ b/src/HOL/BNF_LFP.thy	Thu Jul 24 11:54:15 2014 +0200
     1.3 @@ -41,23 +41,23 @@
     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 (<f, g> x) = f x"
     1.8 +lemma fst_convol': "fst (\<langle>f, g\<rangle> x) = f x"
     1.9  using fst_convol unfolding convol_def by simp
    1.10  
    1.11 -lemma snd_convol': "snd (<f, g> x) = g x"
    1.12 +lemma snd_convol': "snd (\<langle>f, g\<rangle> x) = g x"
    1.13  using snd_convol unfolding convol_def by simp
    1.14  
    1.15 -lemma convol_expand_snd: "fst o f = g \<Longrightarrow>  <g, snd o f> = f"
    1.16 +lemma convol_expand_snd: "fst o f = g \<Longrightarrow> \<langle>g, snd o f\<rangle> = f"
    1.17  unfolding convol_def by auto
    1.18  
    1.19  lemma convol_expand_snd':
    1.20    assumes "(fst o f = g)"
    1.21 -  shows "h = snd o f \<longleftrightarrow> <g, h> = f"
    1.22 +  shows "h = snd o f \<longleftrightarrow> \<langle>g, h\<rangle> = f"
    1.23  proof -
    1.24 -  from assms have *: "<g, snd o f> = f" by (rule convol_expand_snd)
    1.25 -  then have "h = snd o f \<longleftrightarrow> h = snd o <g, snd o f>" by simp
    1.26 +  from assms have *: "\<langle>g, snd o f\<rangle> = f" by (rule convol_expand_snd)
    1.27 +  then have "h = snd o f \<longleftrightarrow> h = snd o \<langle>g, snd o f\<rangle>" by simp
    1.28    moreover have "\<dots> \<longleftrightarrow> h = snd o f" by (simp add: snd_convol)
    1.29 -  moreover have "\<dots> \<longleftrightarrow> <g, h> = f" by (subst (2) *[symmetric]) (auto simp: convol_def fun_eq_iff)
    1.30 +  moreover have "\<dots> \<longleftrightarrow> \<langle>g, h\<rangle> = f" by (subst (2) *[symmetric]) (auto simp: convol_def fun_eq_iff)
    1.31    ultimately show ?thesis by simp
    1.32  qed
    1.33  lemma bij_betwE: "bij_betw f A B \<Longrightarrow> \<forall>a\<in>A. f a \<in> B"