src/HOL/BNF/BNF_Def.thy
changeset 52635 4f84b730c489
parent 51917 f964a9887713
child 52659 58b87aa4dc3b
     1.1 --- a/src/HOL/BNF/BNF_Def.thy	Thu Jul 11 11:16:23 2013 +0200
     1.2 +++ b/src/HOL/BNF/BNF_Def.thy	Sat Jul 13 13:03:21 2013 +0200
     1.3 @@ -185,6 +185,25 @@
     1.4  lemma predicate2_eqD: "A = B \<Longrightarrow> A a b \<longleftrightarrow> B a b"
     1.5  by metis
     1.6  
     1.7 +lemma sum_case_o_inj:
     1.8 +"sum_case f g \<circ> Inl = f"
     1.9 +"sum_case f g \<circ> Inr = g"
    1.10 +by auto
    1.11 +
    1.12 +lemma card_order_csum_cone_cexp_def:
    1.13 +  "card_order r \<Longrightarrow> ( |A1| +c cone) ^c r = |Func UNIV (Inl ` A1 \<union> {Inr ()})|"
    1.14 +  unfolding cexp_def cone_def Field_csum Field_card_of by (auto dest: Field_card_order)
    1.15 +
    1.16 +lemma If_the_inv_into_in_Func:
    1.17 +  "\<lbrakk>inj_on g C; C \<subseteq> B \<union> {x}\<rbrakk> \<Longrightarrow>
    1.18 +  (\<lambda>i. if i \<in> g ` C then the_inv_into C g i else x) \<in> Func UNIV (B \<union> {x})"
    1.19 +unfolding Func_def by (auto dest: the_inv_into_into)
    1.20 +
    1.21 +lemma If_the_inv_into_f_f:
    1.22 +  "\<lbrakk>i \<in> C; inj_on g C\<rbrakk> \<Longrightarrow>
    1.23 +  ((\<lambda>i. if i \<in> g ` C then the_inv_into C g i else x) o g) i = id i"
    1.24 +unfolding Func_def by (auto elim: the_inv_into_f_f)
    1.25 +
    1.26  ML_file "Tools/bnf_def_tactics.ML"
    1.27  ML_file "Tools/bnf_def.ML"
    1.28