src/HOL/List.thy
changeset 55938 f20d1db5aa3c
parent 55932 68c5104d2204
child 55944 7ab8f003fe41
     1.1 --- a/src/HOL/List.thy	Thu Mar 06 14:25:55 2014 +0100
     1.2 +++ b/src/HOL/List.thy	Thu Mar 06 14:57:14 2014 +0100
     1.3 @@ -6734,7 +6734,7 @@
     1.4    by (rule fun_relI, erule list_all2_induct, auto)
     1.5  
     1.6  lemma set_transfer [transfer_rule]:
     1.7 -  "(list_all2 A ===> set_rel A) set set"
     1.8 +  "(list_all2 A ===> rel_set A) set set"
     1.9    unfolding set_rec[abs_def] by transfer_prover
    1.10  
    1.11  lemma map_rec: "map f xs = rec_list Nil (%x _ y. Cons (f x) y) xs"
    1.12 @@ -6864,7 +6864,7 @@
    1.13    done
    1.14  
    1.15  lemma sublist_transfer [transfer_rule]:
    1.16 -  "(list_all2 A ===> set_rel (op =) ===> list_all2 A) sublist sublist"
    1.17 +  "(list_all2 A ===> rel_set (op =) ===> list_all2 A) sublist sublist"
    1.18    unfolding sublist_def [abs_def] by transfer_prover
    1.19  
    1.20  lemma partition_transfer [transfer_rule]:
    1.21 @@ -6873,25 +6873,25 @@
    1.22    unfolding partition_def by transfer_prover
    1.23  
    1.24  lemma lists_transfer [transfer_rule]:
    1.25 -  "(set_rel A ===> set_rel (list_all2 A)) lists lists"
    1.26 -  apply (rule fun_relI, rule set_relI)
    1.27 +  "(rel_set A ===> rel_set (list_all2 A)) lists lists"
    1.28 +  apply (rule fun_relI, rule rel_setI)
    1.29    apply (erule lists.induct, simp)
    1.30 -  apply (simp only: set_rel_def list_all2_Cons1, metis lists.Cons)
    1.31 +  apply (simp only: rel_set_def list_all2_Cons1, metis lists.Cons)
    1.32    apply (erule lists.induct, simp)
    1.33 -  apply (simp only: set_rel_def list_all2_Cons2, metis lists.Cons)
    1.34 +  apply (simp only: rel_set_def list_all2_Cons2, metis lists.Cons)
    1.35    done
    1.36  
    1.37  lemma set_Cons_transfer [transfer_rule]:
    1.38 -  "(set_rel A ===> set_rel (list_all2 A) ===> set_rel (list_all2 A))
    1.39 +  "(rel_set A ===> rel_set (list_all2 A) ===> rel_set (list_all2 A))
    1.40      set_Cons set_Cons"
    1.41 -  unfolding fun_rel_def set_rel_def set_Cons_def
    1.42 +  unfolding fun_rel_def rel_set_def set_Cons_def
    1.43    apply safe
    1.44    apply (simp add: list_all2_Cons1, fast)
    1.45    apply (simp add: list_all2_Cons2, fast)
    1.46    done
    1.47  
    1.48  lemma listset_transfer [transfer_rule]:
    1.49 -  "(list_all2 (set_rel A) ===> set_rel (list_all2 A)) listset listset"
    1.50 +  "(list_all2 (rel_set A) ===> rel_set (list_all2 A)) listset listset"
    1.51    unfolding listset_def by transfer_prover
    1.52  
    1.53  lemma null_transfer [transfer_rule]: