# HG changeset patch
# User kuncar
# Date 1370439181 -7200
# Node ID 299b35e3054bd4d7c2704a6c004b2e25df591f52
# Parent  32c433c38ddd3faf1fcd096e1aebd6f20ce23581
transfer rule for listsum

diff -r 32c433c38ddd -r 299b35e3054b src/HOL/Library/Quotient_List.thy
--- a/src/HOL/Library/Quotient_List.thy	Wed Jun 05 15:21:52 2013 +0200
+++ b/src/HOL/Library/Quotient_List.thy	Wed Jun 05 15:33:01 2013 +0200
@@ -333,6 +333,13 @@
   apply (erule_tac xs=x in list_all2_induct, simp, simp add: fun_rel_def)
   done
 
+lemma listsum_transfer[transfer_rule]:
+  assumes [transfer_rule]: "A 0 0"
+  assumes [transfer_rule]: "(A ===> A ===> A) op + op +"
+  shows "(list_all2 A ===> A) listsum listsum"
+  unfolding listsum_def[abs_def]
+  by transfer_prover
+
 subsection {* Setup for lifting package *}
 
 lemma Quotient_list[quot_map]: