src/HOL/BNF_FP_Base.thy
changeset 55083 0a689157e3ce
parent 55079 ec08a67e993b
child 55414 eab03e9cee8a
     1.1 --- a/src/HOL/BNF_FP_Base.thy	Mon Jan 20 20:00:33 2014 +0100
     1.2 +++ b/src/HOL/BNF_FP_Base.thy	Mon Jan 20 20:21:12 2014 +0100
     1.3 @@ -10,7 +10,7 @@
     1.4  header {* Shared Fixed Point Operations on Bounded Natural Functors *}
     1.5  
     1.6  theory BNF_FP_Base
     1.7 -imports BNF_Comp Ctr_Sugar
     1.8 +imports BNF_Comp
     1.9  begin
    1.10  
    1.11  lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q"
    1.12 @@ -98,17 +98,6 @@
    1.13  "setr (Inr x) = {x}"
    1.14  unfolding sum_set_defs by simp+
    1.15  
    1.16 -lemma prod_rel_simp:
    1.17 -"prod_rel P Q (x, y) (x', y') \<longleftrightarrow> P x x' \<and> Q y y'"
    1.18 -unfolding prod_rel_def by simp
    1.19 -
    1.20 -lemma sum_rel_simps:
    1.21 -"sum_rel P Q (Inl x) (Inl x') \<longleftrightarrow> P x x'"
    1.22 -"sum_rel P Q (Inr y) (Inr y') \<longleftrightarrow> Q y y'"
    1.23 -"sum_rel P Q (Inl x) (Inr y') \<longleftrightarrow> False"
    1.24 -"sum_rel P Q (Inr y) (Inl x') \<longleftrightarrow> False"
    1.25 -unfolding sum_rel_def by simp+
    1.26 -
    1.27  lemma spec2: "\<forall>x y. P x y \<Longrightarrow> P x y"
    1.28  by blast
    1.29