src/HOL/BNF_Fixpoint_Base.thy
changeset 62905 52c5a25e0c96
parent 62335 e85c42f4f30a
child 63046 8053ef5a0174
     1.1 --- a/src/HOL/BNF_Fixpoint_Base.thy	Thu Apr 07 17:26:22 2016 +0200
     1.2 +++ b/src/HOL/BNF_Fixpoint_Base.thy	Thu Apr 07 17:56:22 2016 +0200
     1.3 @@ -242,6 +242,49 @@
     1.4  lemma top_conj: "top x \<and> P \<longleftrightarrow> P" "P \<and> top x \<longleftrightarrow> P"
     1.5    by blast+
     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 case_sum_expand_Inr_pointfree: "f o Inl = g \<Longrightarrow> case_sum g (f o Inr) = f"
    1.28 +  by (auto split: sum.splits)
    1.29 +
    1.30 +lemma case_sum_expand_Inr': "f o Inl = g \<Longrightarrow> h = f o Inr \<longleftrightarrow> case_sum g h = f"
    1.31 +  by (rule iffI) (auto simp add: fun_eq_iff split: sum.splits)
    1.32 +
    1.33 +lemma case_sum_expand_Inr: "f o Inl = g \<Longrightarrow> f x = case_sum g (f o Inr) x"
    1.34 +  by (auto split: sum.splits)
    1.35 +
    1.36 +lemma id_transfer: "rel_fun A A id id"
    1.37 +  unfolding rel_fun_def by simp
    1.38 +
    1.39 +lemma fst_transfer: "rel_fun (rel_prod A B) A fst fst"
    1.40 +  unfolding rel_fun_def by simp
    1.41 +
    1.42 +lemma snd_transfer: "rel_fun (rel_prod A B) B snd snd"
    1.43 +  unfolding rel_fun_def by simp
    1.44 +
    1.45 +lemma convol_transfer:
    1.46 +  "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.47 +  unfolding rel_fun_def convol_def by auto
    1.48 +
    1.49 +ML_file "Tools/BNF/bnf_fp_util_tactics.ML"
    1.50  ML_file "Tools/BNF/bnf_fp_util.ML"
    1.51  ML_file "Tools/BNF/bnf_fp_def_sugar_tactics.ML"
    1.52  ML_file "Tools/BNF/bnf_fp_def_sugar.ML"