--- a/src/HOL/BNF_FP_Base.thy Mon Jan 20 20:00:33 2014 +0100
+++ b/src/HOL/BNF_FP_Base.thy Mon Jan 20 20:21:12 2014 +0100
@@ -10,7 +10,7 @@
header {* Shared Fixed Point Operations on Bounded Natural Functors *}
theory BNF_FP_Base
-imports BNF_Comp Ctr_Sugar
+imports BNF_Comp
begin
lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q"
@@ -98,17 +98,6 @@
"setr (Inr x) = {x}"
unfolding sum_set_defs by simp+
-lemma prod_rel_simp:
-"prod_rel P Q (x, y) (x', y') \<longleftrightarrow> P x x' \<and> Q y y'"
-unfolding prod_rel_def by simp
-
-lemma sum_rel_simps:
-"sum_rel P Q (Inl x) (Inl x') \<longleftrightarrow> P x x'"
-"sum_rel P Q (Inr y) (Inr y') \<longleftrightarrow> Q y y'"
-"sum_rel P Q (Inl x) (Inr y') \<longleftrightarrow> False"
-"sum_rel P Q (Inr y) (Inl x') \<longleftrightarrow> False"
-unfolding sum_rel_def by simp+
-
lemma spec2: "\<forall>x y. P x y \<Longrightarrow> P x y"
by blast
--- a/src/HOL/Basic_BNFs.thy Mon Jan 20 20:00:33 2014 +0100
+++ b/src/HOL/Basic_BNFs.thy Mon Jan 20 20:21:12 2014 +0100
@@ -12,8 +12,6 @@
theory Basic_BNFs
imports BNF_Def
(*FIXME: define relators here, reuse in Lifting_* once this theory is in HOL*)
- Lifting_Sum
- Lifting_Product
begin
bnf ID: 'a
@@ -42,6 +40,21 @@
lemmas sum_set_defs = setl_def[abs_def] setr_def[abs_def]
+definition
+ sum_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd \<Rightarrow> bool"
+where
+ "sum_rel R1 R2 x y =
+ (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y
+ | (Inr x, Inr y) \<Rightarrow> R2 x y
+ | _ \<Rightarrow> False)"
+
+lemma sum_rel_simps[simp]:
+ "sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
+ "sum_rel R1 R2 (Inl a1) (Inr b2) = False"
+ "sum_rel R1 R2 (Inr a2) (Inl b1) = False"
+ "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
+ unfolding sum_rel_def by simp_all
+
bnf "'a + 'b"
map: sum_map
sets: setl setr
@@ -109,6 +122,15 @@
lemmas prod_set_defs = fsts_def[abs_def] snds_def[abs_def]
+definition
+ prod_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool"
+where
+ "prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
+
+lemma prod_rel_apply [simp]:
+ "prod_rel R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
+ by (simp add: prod_rel_def)
+
bnf "'a \<times> 'b"
map: map_pair
sets: fsts snds
--- a/src/HOL/Lifting.thy Mon Jan 20 20:00:33 2014 +0100
+++ b/src/HOL/Lifting.thy Mon Jan 20 20:21:12 2014 +0100
@@ -484,9 +484,6 @@
text {* Proving a parametrized correspondence relation *}
-lemma eq_OO: "op= OO R = R"
-unfolding OO_def by metis
-
definition POS :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where
"POS A B \<equiv> A \<le> B"
--- a/src/HOL/Lifting_Product.thy Mon Jan 20 20:00:33 2014 +0100
+++ b/src/HOL/Lifting_Product.thy Mon Jan 20 20:21:12 2014 +0100
@@ -5,23 +5,14 @@
header {* Setup for Lifting/Transfer for the product type *}
theory Lifting_Product
-imports Lifting
+imports Lifting Basic_BNFs
begin
subsection {* Relator and predicator properties *}
-definition
- prod_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool"
-where
- "prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
-
definition prod_pred :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
where "prod_pred R1 R2 = (\<lambda>(a, b). R1 a \<and> R2 b)"
-lemma prod_rel_apply [simp]:
- "prod_rel R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
- by (simp add: prod_rel_def)
-
lemma prod_pred_apply [simp]:
"prod_pred P1 P2 (a, b) \<longleftrightarrow> P1 a \<and> P2 b"
by (simp add: prod_pred_def)
--- a/src/HOL/Lifting_Sum.thy Mon Jan 20 20:00:33 2014 +0100
+++ b/src/HOL/Lifting_Sum.thy Mon Jan 20 20:21:12 2014 +0100
@@ -5,26 +5,11 @@
header {* Setup for Lifting/Transfer for the sum type *}
theory Lifting_Sum
-imports Lifting
+imports Lifting Basic_BNFs
begin
subsection {* Relator and predicator properties *}
-definition
- sum_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd \<Rightarrow> bool"
-where
- "sum_rel R1 R2 x y =
- (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y
- | (Inr x, Inr y) \<Rightarrow> R2 x y
- | _ \<Rightarrow> False)"
-
-lemma sum_rel_simps[simp]:
- "sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
- "sum_rel R1 R2 (Inl a1) (Inr b2) = False"
- "sum_rel R1 R2 (Inr a2) (Inl b1) = False"
- "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
- unfolding sum_rel_def by simp_all
-
abbreviation (input) "sum_pred \<equiv> sum_case"
lemma sum_rel_eq [relator_eq]:
--- a/src/HOL/Relation.thy Mon Jan 20 20:00:33 2014 +0100
+++ b/src/HOL/Relation.thy Mon Jan 20 20:21:12 2014 +0100
@@ -624,6 +624,9 @@
"r O s = {(x, z). \<exists>y. (x, y) \<in> r \<and> (y, z) \<in> s}"
by (auto simp add: set_eq_iff)
+lemma eq_OO: "op= OO R = R"
+by blast
+
subsubsection {* Converse *}
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Mon Jan 20 20:00:33 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Mon Jan 20 20:21:12 2014 +0100
@@ -41,7 +41,7 @@
Union_Un_distrib collect_def[abs_def] image_def o_apply map_pair_simp
mem_Collect_eq mem_UN_compreh_eq prod_set_simps sum_map.simps sum_set_simps};
val sum_prod_thms_set = @{thms UN_compreh_eq_eq} @ sum_prod_thms_set0;
-val sum_prod_thms_rel = @{thms prod_rel_simp sum_rel_simps id_apply};
+val sum_prod_thms_rel = @{thms prod_rel_apply sum_rel_simps id_apply};
fun hhf_concl_conv cv ctxt ct =
(case Thm.term_of ct of