# HG changeset patch
# User kuncar
# Date 1397144895 -7200
# Node ID 3373f5d1e07480bfbb889358957a173e12ceba86
# Parent  c1048f5bbb4566310d4896fd9d8062bce041f3d5
abstract Domainp in relator_domain rules => more natural statement of the rule

diff -r c1048f5bbb45 -r 3373f5d1e074 src/HOL/Library/FSet.thy
--- 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)
diff -r c1048f5bbb45 -r 3373f5d1e074 src/HOL/Lifting_Option.thy
--- 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]:
diff -r c1048f5bbb45 -r 3373f5d1e074 src/HOL/Lifting_Product.thy
--- 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"
diff -r c1048f5bbb45 -r 3373f5d1e074 src/HOL/Lifting_Set.thy
--- 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
diff -r c1048f5bbb45 -r 3373f5d1e074 src/HOL/Lifting_Sum.thy
--- 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]:
diff -r c1048f5bbb45 -r 3373f5d1e074 src/HOL/List.thy
--- 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
diff -r c1048f5bbb45 -r 3373f5d1e074 src/HOL/Tools/transfer.ML
--- 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
diff -r c1048f5bbb45 -r 3373f5d1e074 src/HOL/Transfer.thy
--- 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'' *}