# HG changeset patch
# User haftmann
# Date 1571846964 0
# Node ID 273fc913427b33a427bcbcf980607ebfa4b32df9
# Parent  cc204e10385ce9aa85aec10890f8bf1345de7fc8
more transfer rules

diff -r cc204e10385c -r 273fc913427b src/HOL/Groups_List.thy
--- a/src/HOL/Groups_List.thy	Wed Oct 23 16:09:23 2019 +0000
+++ b/src/HOL/Groups_List.thy	Wed Oct 23 16:09:24 2019 +0000
@@ -94,6 +94,18 @@
 translations \<comment> \<open>Beware of argument permutation!\<close>
   "\<Sum>x\<leftarrow>xs. b" == "CONST sum_list (CONST map (\<lambda>x. b) xs)"
 
+context
+  includes lifting_syntax
+begin
+
+lemma sum_list_transfer [transfer_rule]:
+  "(list_all2 A ===> A) sum_list sum_list"
+    if [transfer_rule]: "A 0 0" "(A ===> A ===> A) (+) (+)"
+  unfolding sum_list.eq_foldr [abs_def]
+  by transfer_prover
+
+end
+
 text \<open>TODO duplicates\<close>
 lemmas sum_list_simps = sum_list.Nil sum_list.Cons
 lemmas sum_list_append = sum_list.append
@@ -367,18 +379,6 @@
   "sum f (set [m..<n]) = sum_list (map f [m..<n])"
   by (simp add: interv_sum_list_conv_sum_set_nat)
 
-context
-  includes lifting_syntax
-begin
-
-lemma sum_list_transfer [transfer_rule]:
-  "(list_all2 A ===> A) sum_list sum_list"
-    if [transfer_rule]: "A 0 0" "(A ===> A ===> A) (+) (+)"
-  unfolding sum_list.eq_foldr [abs_def]
-  by transfer_prover
-
-end
-
 
 subsection \<open>List product\<close>
 
@@ -416,10 +416,6 @@
 
 end
 
-lemma prod_list_zero_iff:
-  "prod_list xs = 0 \<longleftrightarrow> (0 :: 'a :: {semiring_no_zero_divisors, semiring_1}) \<in> set xs"
-  by (induction xs) simp_all
-
 text \<open>Some syntactic sugar:\<close>
 
 syntax (ASCII)
@@ -429,4 +425,20 @@
 translations \<comment> \<open>Beware of argument permutation!\<close>
   "\<Prod>x\<leftarrow>xs. b" \<rightleftharpoons> "CONST prod_list (CONST map (\<lambda>x. b) xs)"
 
+context
+  includes lifting_syntax
+begin
+
+lemma prod_list_transfer [transfer_rule]:
+  "(list_all2 A ===> A) prod_list prod_list"
+    if [transfer_rule]: "A 1 1" "(A ===> A ===> A) (*) (*)"
+  unfolding prod_list.eq_foldr [abs_def]
+  by transfer_prover
+
 end
+
+lemma prod_list_zero_iff:
+  "prod_list xs = 0 \<longleftrightarrow> (0 :: 'a :: {semiring_no_zero_divisors, semiring_1}) \<in> set xs"
+  by (induction xs) simp_all
+
+end
diff -r cc204e10385c -r 273fc913427b src/HOL/Power.thy
--- a/src/HOL/Power.thy	Wed Oct 23 16:09:23 2019 +0000
+++ b/src/HOL/Power.thy	Wed Oct 23 16:09:24 2019 +0000
@@ -28,6 +28,19 @@
 
 end
 
+context
+  includes lifting_syntax
+begin
+
+lemma power_transfer [transfer_rule]:
+  \<open>(R ===> (=) ===> R) (^) (^)\<close>
+    if [transfer_rule]: \<open>R 1 1\<close>
+      \<open>(R ===> R ===> R) (*) (*)\<close>
+    for R :: \<open>'a::power \<Rightarrow> 'b::power \<Rightarrow> bool\<close>
+  by (simp only: power_def [abs_def]) transfer_prover
+
+end
+
 context monoid_mult
 begin