--- a/src/HOL/Library/FSet.thy Thu Apr 10 17:48:15 2014 +0200
+++ b/src/HOL/Library/FSet.thy Thu Apr 10 17:48:15 2014 +0200
@@ -810,15 +810,13 @@
apply (rule ext)+
by transfer (auto intro: finite_rel_set rel_set_OO[unfolded fun_eq_iff, rule_format, THEN iffD1])
-lemma Domainp_fset[relator_domain]:
- assumes "Domainp T = P"
- shows "Domainp (rel_fset T) = (\<lambda>A. fBall A P)"
+lemma Domainp_fset[relator_domain]: "Domainp (rel_fset T) = (\<lambda>A. fBall A (Domainp T))"
proof -
- from assms obtain f where f: "\<forall>x\<in>Collect P. T x (f x)"
+ obtain f where f: "\<forall>x\<in>Collect (Domainp T). T x (f x)"
unfolding Domainp_iff[abs_def]
apply atomize_elim
- by (subst bchoice_iff[symmetric]) auto
- from assms f show ?thesis
+ by (subst bchoice_iff[symmetric]) (auto iff: bchoice_iff[symmetric])
+ from f show ?thesis
unfolding fun_eq_iff rel_fset_alt_def Domainp_iff
apply clarify
apply (rule iffI)
--- a/src/HOL/Lifting_Option.thy Thu Apr 10 17:48:15 2014 +0200
+++ b/src/HOL/Lifting_Option.thy Thu Apr 10 17:48:15 2014 +0200
@@ -33,10 +33,9 @@
"(rel_option A) OO (rel_option B) = rel_option (A OO B)"
by (rule ext)+ (auto simp: rel_option_iff OO_def split: option.split)
-lemma Domainp_option[relator_domain]:
- assumes "Domainp A = P"
- shows "Domainp (rel_option A) = (pred_option P)"
-using assms unfolding Domainp_iff[abs_def] rel_option_iff[abs_def]
+lemma Domainp_option[relator_domain]:
+ "Domainp (rel_option A) = (pred_option (Domainp A))"
+unfolding Domainp_iff[abs_def] rel_option_iff[abs_def]
by (auto iff: fun_eq_iff split: option.split)
lemma left_total_rel_option[transfer_rule]:
--- a/src/HOL/Lifting_Product.thy Thu Apr 10 17:48:15 2014 +0200
+++ b/src/HOL/Lifting_Product.thy Thu Apr 10 17:48:15 2014 +0200
@@ -24,11 +24,9 @@
"(rel_prod A B) OO (rel_prod C D) = rel_prod (A OO C) (B OO D)"
by (rule ext)+ (auto simp: rel_prod_def OO_def)
-lemma Domainp_prod[relator_domain]:
- assumes "Domainp T1 = P1"
- assumes "Domainp T2 = P2"
- shows "Domainp (rel_prod T1 T2) = (pred_prod P1 P2)"
-using assms unfolding rel_prod_def pred_prod_def by blast
+lemma Domainp_prod[relator_domain]:
+ "Domainp (rel_prod T1 T2) = (pred_prod (Domainp T1) (Domainp T2))"
+unfolding rel_prod_def pred_prod_def by blast
lemma left_total_rel_prod [transfer_rule]:
assumes "left_total R1"
--- a/src/HOL/Lifting_Set.thy Thu Apr 10 17:48:15 2014 +0200
+++ b/src/HOL/Lifting_Set.thy Thu Apr 10 17:48:15 2014 +0200
@@ -45,9 +45,8 @@
done
lemma Domainp_set[relator_domain]:
- assumes "Domainp T = R"
- shows "Domainp (rel_set T) = (\<lambda>A. Ball A R)"
-using assms unfolding rel_set_def Domainp_iff[abs_def]
+ "Domainp (rel_set T) = (\<lambda>A. Ball A (Domainp T))"
+unfolding rel_set_def Domainp_iff[abs_def]
apply (intro ext)
apply (rule iffI)
apply blast
--- a/src/HOL/Lifting_Sum.thy Thu Apr 10 17:48:15 2014 +0200
+++ b/src/HOL/Lifting_Sum.thy Thu Apr 10 17:48:15 2014 +0200
@@ -20,10 +20,7 @@
by (rule ext)+ (auto simp add: rel_sum_def OO_def split_sum_ex split: sum.split)
lemma Domainp_sum[relator_domain]:
- assumes "Domainp R1 = P1"
- assumes "Domainp R2 = P2"
- shows "Domainp (rel_sum R1 R2) = (sum_pred P1 P2)"
-using assms
+ "Domainp (rel_sum R1 R2) = (sum_pred (Domainp R1) (Domainp R2))"
by (auto simp add: Domainp_iff split_sum_ex iff: fun_eq_iff split: sum.split)
lemma left_total_rel_sum[transfer_rule]:
--- a/src/HOL/List.thy Thu Apr 10 17:48:15 2014 +0200
+++ b/src/HOL/List.thy Thu Apr 10 17:48:15 2014 +0200
@@ -6605,13 +6605,12 @@
qed
lemma Domainp_list[relator_domain]:
- assumes "Domainp A = P"
- shows "Domainp (list_all2 A) = (list_all P)"
+ "Domainp (list_all2 A) = (list_all (Domainp A))"
proof -
{
fix x
- have *: "\<And>x. (\<exists>y. A x y) = P x" using assms unfolding Domainp_iff by blast
- have "(\<exists>y. (list_all2 A x y)) = list_all P x"
+ have *: "\<And>x. (\<exists>y. A x y) = Domainp A x" unfolding Domainp_iff by blast
+ have "(\<exists>y. (list_all2 A x y)) = list_all (Domainp A) x"
by (induction x) (simp_all add: * list_all2_Cons1)
}
then show ?thesis
--- a/src/HOL/Tools/transfer.ML Thu Apr 10 17:48:15 2014 +0200
+++ b/src/HOL/Tools/transfer.ML Thu Apr 10 17:48:15 2014 +0200
@@ -335,6 +335,21 @@
gen_abstract_domains ctxt dest thm
end
+fun abstract_domains_relator_domain ctxt thm =
+ let
+ fun dest prop =
+ let
+ val prems = Logic.strip_imp_prems prop
+ val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop)
+ val ((rel, x), y) = apfst Term.dest_comb (Term.dest_comb concl)
+ in
+ (y, fn y' =>
+ Logic.list_implies (prems, HOLogic.mk_Trueprop (rel $ x $ y')))
+ end
+ in
+ gen_abstract_domains ctxt dest thm
+ end
+
fun detect_transfer_rules thm =
let
fun is_transfer_rule tm = case (HOLogic.dest_Trueprop tm) of
@@ -779,10 +794,18 @@
val relator_domain_setup =
let
val name = @{binding relator_domain}
- fun add_thm thm = Data.map (map_relator_domain (Item_Net.update thm))
- #> add_transfer_domain_thm thm
- fun del_thm thm = Data.map (map_relator_domain (Item_Net.remove thm))
- #> del_transfer_domain_thm thm
+ fun add_thm thm context =
+ let
+ val thm = abstract_domains_relator_domain (Context.proof_of context) thm
+ in
+ context |> Data.map (map_relator_domain (Item_Net.update thm)) |> add_transfer_domain_thm thm
+ end
+ fun del_thm thm context =
+ let
+ val thm = abstract_domains_relator_domain (Context.proof_of context) thm
+ in
+ context |> Data.map (map_relator_domain (Item_Net.remove thm)) |> del_transfer_domain_thm thm
+ end
val add = Thm.declaration_attribute add_thm
val del = Thm.declaration_attribute del_thm
val text = "declaration of relator domain rule (used by transfer method)"
@@ -792,7 +815,6 @@
#> Global_Theory.add_thms_dynamic (name, content)
end
-
val setup =
relator_eq_setup
#> relator_domain_setup
--- a/src/HOL/Transfer.thy Thu Apr 10 17:48:15 2014 +0200
+++ b/src/HOL/Transfer.thy Thu Apr 10 17:48:15 2014 +0200
@@ -128,10 +128,9 @@
lemma Domaimp_refl[transfer_domain_rule]:
"Domainp T = Domainp T" ..
-lemma Domainp_prod_fun_eq[transfer_domain_rule]:
- assumes "Domainp T = P"
- shows "Domainp (op= ===> T) = (\<lambda>f. \<forall>x. P (f x))"
-by (auto intro: choice simp: assms[symmetric] Domainp_iff rel_fun_def fun_eq_iff)
+lemma Domainp_prod_fun_eq[relator_domain]:
+ "Domainp (op= ===> T) = (\<lambda>f. \<forall>x. (Domainp T) (f x))"
+by (auto intro: choice simp: Domainp_iff rel_fun_def fun_eq_iff)
subsection {* Predicates on relations, i.e. ``class constraints'' *}