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
```