# HG changeset patch
# User blanchet
# Date 1390246963 -3600
# Node ID 8ee9aabb2bca8e4394e68a43c3e371129dfc45e6
# Parent  0a689157e3ce2471c868b1244ffb87c7c544f955
rationalized lemmas

diff -r 0a689157e3ce -r 8ee9aabb2bca src/HOL/BNF_LFP.thy
--- a/src/HOL/BNF_LFP.thy	Mon Jan 20 20:21:12 2014 +0100
+++ b/src/HOL/BNF_LFP.thy	Mon Jan 20 20:42:43 2014 +0100
@@ -222,7 +222,7 @@
 lemma meta_spec2:
   assumes "(\<And>x y. PROP P x y)"
   shows "PROP P x y"
-by (rule `(\<And>x y. PROP P x y)`)
+by (rule assms)
 
 lemma nchotomy_relcomppE:
   "\<lbrakk>\<And>y. \<exists>x. y = f x; (r OO s) a c; \<And>b. r a (f b) \<Longrightarrow> s (f b) c \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
@@ -234,10 +234,15 @@
 lemma predicate2D_vimage2p: "\<lbrakk>R \<le> vimage2p f g S; R x y\<rbrakk> \<Longrightarrow> S (f x) (g y)"
   unfolding vimage2p_def by auto
 
+lemma id_transfer: "fun_rel A A id id"
+unfolding fun_rel_def by simp
+
 ML_file "Tools/BNF/bnf_lfp_rec_sugar.ML"
 ML_file "Tools/BNF/bnf_lfp_util.ML"
 ML_file "Tools/BNF/bnf_lfp_tactics.ML"
 ML_file "Tools/BNF/bnf_lfp.ML"
 ML_file "Tools/BNF/bnf_lfp_compat.ML"
 
+hide_fact (open) id_transfer
+
 end
diff -r 0a689157e3ce -r 8ee9aabb2bca src/HOL/BNF_Util.thy
--- a/src/HOL/BNF_Util.thy	Mon Jan 20 20:21:12 2014 +0100
+++ b/src/HOL/BNF_Util.thy	Mon Jan 20 20:42:43 2014 +0100
@@ -10,9 +10,23 @@
 
 theory BNF_Util
 imports BNF_Cardinal_Arithmetic
-  Transfer (*FIXME: define fun_rel here, reuse in Transfer once this theory is in HOL*)
 begin
 
+definition
+  fun_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool"
+where
+  "fun_rel A B = (\<lambda>f g. \<forall>x y. A x y \<longrightarrow> B (f x) (g y))"
+
+lemma fun_relI [intro]:
+  assumes "\<And>x y. A x y \<Longrightarrow> B (f x) (g y)"
+  shows "fun_rel A B f g"
+  using assms by (simp add: fun_rel_def)
+
+lemma fun_relD:
+  assumes "fun_rel A B f g" and "A x y"
+  shows "B (f x) (g y)"
+  using assms by (simp add: fun_rel_def)
+
 definition collect where
 "collect F x = (\<Union>f \<in> F. f x)"
 
diff -r 0a689157e3ce -r 8ee9aabb2bca src/HOL/Basic_BNFs.thy
--- a/src/HOL/Basic_BNFs.thy	Mon Jan 20 20:21:12 2014 +0100
+++ b/src/HOL/Basic_BNFs.thy	Mon Jan 20 20:42:43 2014 +0100
@@ -11,7 +11,6 @@
 
 theory Basic_BNFs
 imports BNF_Def
-   (*FIXME: define relators here, reuse in Lifting_* once this theory is in HOL*)
 begin
 
 bnf ID: 'a
diff -r 0a689157e3ce -r 8ee9aabb2bca src/HOL/Lifting_Sum.thy
--- a/src/HOL/Lifting_Sum.thy	Mon Jan 20 20:21:12 2014 +0100
+++ b/src/HOL/Lifting_Sum.thy	Mon Jan 20 20:42:43 2014 +0100
@@ -12,19 +12,12 @@
 
 abbreviation (input) "sum_pred \<equiv> sum_case"
 
-lemma sum_rel_eq [relator_eq]:
-  "sum_rel (op =) (op =) = (op =)"
-  by (simp add: sum_rel_def fun_eq_iff split: sum.split)
-
-lemma sum_rel_mono[relator_mono]:
-  assumes "A \<le> C"
-  assumes "B \<le> D"
-  shows "(sum_rel A B) \<le> (sum_rel C D)"
-using assms by (auto simp: sum_rel_def split: sum.splits)
+lemmas sum_rel_eq[relator_eq] = sum.rel_eq
+lemmas sum_rel_mono[relator_mono] = sum.rel_mono
 
 lemma sum_rel_OO[relator_distr]:
   "(sum_rel A B) OO (sum_rel C D) = sum_rel (A OO C) (B OO D)"
-by (rule ext)+ (auto simp add: sum_rel_def OO_def split_sum_ex split: sum.split)
+  by (rule ext)+ (auto simp add: sum_rel_def OO_def split_sum_ex split: sum.split)
 
 lemma Domainp_sum[relator_domain]:
   assumes "Domainp R1 = P1"
@@ -94,4 +87,3 @@
 end
 
 end
-
diff -r 0a689157e3ce -r 8ee9aabb2bca src/HOL/Transfer.thy
--- a/src/HOL/Transfer.thy	Mon Jan 20 20:21:12 2014 +0100
+++ b/src/HOL/Transfer.thy	Mon Jan 20 20:42:43 2014 +0100
@@ -6,16 +6,11 @@
 header {* Generic theorem transfer using relations *}
 
 theory Transfer
-imports Hilbert_Choice
+imports Hilbert_Choice Basic_BNFs
 begin
 
 subsection {* Relator for function space *}
 
-definition
-  fun_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool"
-where
-  "fun_rel A B = (\<lambda>f g. \<forall>x y. A x y \<longrightarrow> B (f x) (g y))"
-
 locale lifting_syntax
 begin
   notation fun_rel (infixr "===>" 55)
@@ -26,32 +21,20 @@
 begin
 interpretation lifting_syntax .
 
-lemma fun_relI [intro]:
-  assumes "\<And>x y. A x y \<Longrightarrow> B (f x) (g y)"
-  shows "(A ===> B) f g"
-  using assms by (simp add: fun_rel_def)
-
-lemma fun_relD:
-  assumes "(A ===> B) f g" and "A x y"
-  shows "B (f x) (g y)"
-  using assms by (simp add: fun_rel_def)
-
 lemma fun_relD2:
-  assumes "(A ===> B) f g" and "A x x"
+  assumes "fun_rel A B f g" and "A x x"
   shows "B (f x) (g x)"
-  using assms unfolding fun_rel_def by auto
+  using assms by (rule fun_relD)
 
 lemma fun_relE:
-  assumes "(A ===> B) f g" and "A x y"
+  assumes "fun_rel A B f g" and "A x y"
   obtains "B (f x) (g y)"
   using assms by (simp add: fun_rel_def)
 
-lemma fun_rel_eq:
-  shows "((op =) ===> (op =)) = (op =)"
-  by (auto simp add: fun_eq_iff elim: fun_relE)
+lemmas fun_rel_eq = fun.rel_eq
 
 lemma fun_rel_eq_rel:
-  shows "((op =) ===> R) = (\<lambda>f g. \<forall>x. R (f x) (g x))"
+shows "fun_rel (op =) R = (\<lambda>f g. \<forall>x. R (f x) (g x))"
   by (simp add: fun_rel_def)