--- a/src/HOL/Transfer.thy Mon May 13 12:13:24 2013 +0200
+++ b/src/HOL/Transfer.thy Mon May 13 13:59:04 2013 +0200
@@ -1,5 +1,6 @@
(* Title: HOL/Transfer.thy
Author: Brian Huffman, TU Muenchen
+ Author: Ondrej Kuncar, TU Muenchen
*)
header {* Generic theorem transfer using relations *}
@@ -103,10 +104,6 @@
shows "Rel (A ===> B) (\<lambda>x. f x) (\<lambda>y. g y)"
using assms unfolding Rel_def fun_rel_def by fast
-text {* Handling of domains *}
-
-definition DOM :: "('a => 'b => bool) => ('a => bool) => bool" where "DOM T R \<equiv> Domainp T = R"
-
ML_file "Tools/transfer.ML"
setup Transfer.setup
@@ -116,6 +113,10 @@
hide_const (open) Rel
+text {* Handling of domains *}
+
+lemma Domaimp_refl[transfer_domain_rule]:
+ "Domainp T = Domainp T" ..
subsection {* Predicates on relations, i.e. ``class constraints'' *}
@@ -264,6 +265,21 @@
shows "(A ===> A ===> op =) (op =) (op =)"
using assms unfolding bi_unique_def fun_rel_def by auto
+lemma Domainp_iff: "Domainp T x \<longleftrightarrow> (\<exists>y. T x y)"
+ by auto
+
+lemma right_total_Ex_transfer[transfer_rule]:
+ assumes "right_total A"
+ shows "((A ===> op=) ===> op=) (Bex (Collect (Domainp A))) Ex"
+using assms unfolding right_total_def Bex_def fun_rel_def Domainp_iff[abs_def]
+by blast
+
+lemma right_total_All_transfer[transfer_rule]:
+ assumes "right_total A"
+ shows "((A ===> op =) ===> op =) (Ball (Collect (Domainp A))) All"
+using assms unfolding right_total_def Ball_def fun_rel_def Domainp_iff[abs_def]
+by blast
+
lemma All_transfer [transfer_rule]:
assumes "bi_total A"
shows "((A ===> op =) ===> op =) All All"
@@ -304,13 +320,6 @@
"(op = ===> (A ===> A) ===> (A ===> A)) compow compow"
unfolding funpow_def by transfer_prover
-text {* Fallback rule for transferring universal quantifiers over
- correspondence relations that are not bi-total, and do not have
- custom transfer rules (e.g. relations between function types). *}
-
-lemma Domainp_iff: "Domainp T x \<longleftrightarrow> (\<exists>y. T x y)"
- by auto
-
lemma Domainp_forall_transfer [transfer_rule]:
assumes "right_total A"
shows "((A ===> op =) ===> op =)
@@ -319,9 +328,6 @@
unfolding transfer_forall_def transfer_bforall_def fun_rel_def Domainp_iff
by metis
-text {* Preferred rule for transferring universal quantifiers over
- bi-total correspondence relations (later rules are tried first). *}
-
lemma forall_transfer [transfer_rule]:
"bi_total A \<Longrightarrow> ((A ===> op =) ===> op =) transfer_forall transfer_forall"
unfolding transfer_forall_def by (rule All_transfer)