--- 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
--- 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)"
--- 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
--- 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
-
--- 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)