src/HOL/BNF_GFP.thy
changeset 55966 972f0aa7091b
parent 55945 e96383acecf9
child 57698 afef6616cbae
     1.1 --- a/src/HOL/BNF_GFP.thy	Thu Mar 06 22:15:01 2014 +0100
     1.2 +++ b/src/HOL/BNF_GFP.thy	Fri Mar 07 01:02:21 2014 +0100
     1.3 @@ -21,6 +21,12 @@
     1.4  Sign.const_alias @{binding proj} @{const_name Equiv_Relations.proj}
     1.5  *}
     1.6  
     1.7 +lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
     1.8 +by simp
     1.9 +
    1.10 +lemma obj_sumE: "\<lbrakk>\<forall>x. s = Inl x \<longrightarrow> P; \<forall>x. s = Inr x \<longrightarrow> P\<rbrakk> \<Longrightarrow> P"
    1.11 +by (cases s) auto
    1.12 +
    1.13  lemma not_TrueE: "\<not> True \<Longrightarrow> P"
    1.14  by (erule notE, rule TrueI)
    1.15