add transfer rule for constant List.lists
authorhuffman
Mon May 14 17:28:07 2012 +0200 (2012-05-14)
changeset 47923ba9df9685e7c
parent 47922 bba52dffab2b
child 47924 4e951258204b
add transfer rule for constant List.lists
src/HOL/Library/Quotient_List.thy
     1.1 --- a/src/HOL/Library/Quotient_List.thy	Mon May 14 17:09:11 2012 +0200
     1.2 +++ b/src/HOL/Library/Quotient_List.thy	Mon May 14 17:28:07 2012 +0200
     1.3 @@ -176,6 +176,15 @@
     1.4    "(list_all2 A ===> set_rel A) set set"
     1.5    unfolding set_def by transfer_prover
     1.6  
     1.7 +lemma lists_transfer [transfer_rule]:
     1.8 +  "(set_rel A ===> set_rel (list_all2 A)) lists lists"
     1.9 +  apply (rule fun_relI, rule set_relI)
    1.10 +  apply (erule lists.induct, simp)
    1.11 +  apply (simp only: set_rel_def list_all2_Cons1, metis lists.Cons)
    1.12 +  apply (erule lists.induct, simp)
    1.13 +  apply (simp only: set_rel_def list_all2_Cons2, metis lists.Cons)
    1.14 +  done
    1.15 +
    1.16  subsection {* Setup for lifting package *}
    1.17  
    1.18  lemma Quotient_list[quot_map]: