add transfer rule for List.set
authorhuffman
Sat Apr 21 11:21:23 2012 +0200 (2012-04-21)
changeset 4765033ecf14d5ee9
parent 47649 df687f0797fb
child 47651 8e4f50afd21a
add transfer rule for List.set
src/HOL/Library/Quotient_List.thy
     1.1 --- a/src/HOL/Library/Quotient_List.thy	Sat Apr 21 11:04:21 2012 +0200
     1.2 +++ b/src/HOL/Library/Quotient_List.thy	Sat Apr 21 11:21:23 2012 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Quotient infrastructure for the list type *}
     1.5  
     1.6  theory Quotient_List
     1.7 -imports Main Quotient_Syntax
     1.8 +imports Main Quotient_Set
     1.9  begin
    1.10  
    1.11  subsection {* Relator for list type *}
    1.12 @@ -157,6 +157,10 @@
    1.13    apply (simp, simp add: fun_rel_def)
    1.14    done
    1.15  
    1.16 +lemma set_transfer [transfer_rule]:
    1.17 +  "(list_all2 A ===> set_rel A) set set"
    1.18 +  unfolding set_def by transfer_prover
    1.19 +
    1.20  subsection {* Setup for lifting package *}
    1.21  
    1.22  lemma Quotient_list: