# HG changeset patch
# User traytel
# Date 1455705566 -3600
# Node ID 532ad8de5d6159ef98ea4bbd23336c106d73e471
# Parent  112eefe85ff03a829190f2487c4f95c5b32ac1bf
call the predicator of list list_all

diff -r 112eefe85ff0 -r 532ad8de5d61 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Wed Feb 17 12:07:49 2016 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Wed Feb 17 11:39:26 2016 +0100
@@ -359,7 +359,7 @@
       Cons (infixr "#" 65)
 
     hide_type list
-    hide_const Nil Cons case_list hd tl set map list_all2 rec_list size_list pred_list
+    hide_const Nil Cons case_list hd tl set map list_all2 rec_list size_list list_all
 
     context early
     begin
@@ -370,6 +370,7 @@
     for
       map: map
       rel: list_all2
+      pred: list_all
     where
       "tl Nil = Nil"
 
@@ -439,6 +440,7 @@
     for
       map: map
       rel: list_all2
+      pred: list_all
 
 text \<open>
 \noindent
@@ -2889,7 +2891,7 @@
 
     lift_bnf (*<*)(no_warn_wits) (*>*)'a nonempty_list
     proof -
-      fix f and xs :: "'a list"
+      fix f(*<*):: "'a \<Rightarrow> 'c"(*>*) and xs :: "'a list"
       assume "xs \<in> {xs. xs \<noteq> []}"
       then show "map f xs \<in> {xs. xs \<noteq> []}"
         by (cases xs(*<*) rule: list.exhaust(*>*)) auto
diff -r 112eefe85ff0 -r 532ad8de5d61 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Feb 17 12:07:49 2016 +0100
+++ b/src/HOL/List.thy	Wed Feb 17 11:39:26 2016 +0100
@@ -14,6 +14,7 @@
 for
   map: map
   rel: list_all2
+  pred: list_all
 where
   "tl [] = []"
 
@@ -6241,10 +6242,7 @@
   "x \<in> set xs \<longleftrightarrow> member xs x"
   by (simp add: member_def)
 
-abbreviation "list_all == pred_list"
-
-lemma list_all_iff [code_abbrev]: "list_all P xs \<longleftrightarrow> Ball (set xs) P"
-unfolding pred_list_def ..
+lemmas list_all_iff [code_abbrev] = fun_cong[OF list.pred_set]
 
 definition list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
 list_ex_iff [code_abbrev]: "list_ex P xs \<longleftrightarrow> Bex (set xs) P"
@@ -6305,9 +6303,7 @@
   "list_ex P xs \<longleftrightarrow> (\<exists>n < length xs. P (xs ! n))"
   by (auto simp add: list_ex_iff set_conv_nth)
 
-lemma list_all_cong [fundef_cong]:
-  "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> list_all f xs = list_all g ys"
-  by (simp add: list_all_iff)
+lemmas list_all_cong [fundef_cong] = list.pred_cong
 
 lemma list_ex_cong [fundef_cong]:
   "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> list_ex f xs = list_ex g ys"