Got rid of Alls in List.
authornipkow
Fri Jan 17 10:09:46 1997 +0100 (1997-01-17)
changeset 25120231e4f467f2
parent 2511 282e9a9eae9d
child 2513 d708d8cdc8e8
Got rid of Alls in List.
Added Ball_insert and Ball_Un in equalities.ML.
src/HOL/List.ML
src/HOL/List.thy
src/HOL/equalities.ML
     1.1 --- a/src/HOL/List.ML	Fri Jan 17 10:04:28 1997 +0100
     1.2 +++ b/src/HOL/List.ML	Fri Jan 17 10:09:46 1997 +0100
     1.3 @@ -17,6 +17,7 @@
     1.4  by (list.induct_tac "xs" 1);
     1.5  by (ALLGOALS Asm_simp_tac);
     1.6  qed "not_Cons_self";
     1.7 +Addsimps [not_Cons_self];
     1.8  
     1.9  goal List.thy "(xs ~= []) = (? y ys. xs = y#ys)";
    1.10  by (list.induct_tac "xs" 1);
    1.11 @@ -32,21 +33,25 @@
    1.12  by (list.induct_tac "xs" 1);
    1.13  by (ALLGOALS Asm_simp_tac);
    1.14  qed "append_assoc";
    1.15 +Addsimps [append_assoc];
    1.16  
    1.17  goal List.thy "xs @ [] = xs";
    1.18  by (list.induct_tac "xs" 1);
    1.19  by (ALLGOALS Asm_simp_tac);
    1.20  qed "append_Nil2";
    1.21 +Addsimps [append_Nil2];
    1.22  
    1.23  goal List.thy "(xs@ys = []) = (xs=[] & ys=[])";
    1.24  by (list.induct_tac "xs" 1);
    1.25  by (ALLGOALS Asm_simp_tac);
    1.26  qed "append_is_Nil";
    1.27 +Addsimps [append_is_Nil];
    1.28  
    1.29  goal List.thy "(xs @ ys = xs @ zs) = (ys=zs)";
    1.30  by (list.induct_tac "xs" 1);
    1.31  by (ALLGOALS Asm_simp_tac);
    1.32  qed "same_append_eq";
    1.33 +Addsimps [same_append_eq];
    1.34  
    1.35  goal List.thy "hd(xs@ys) = (if xs=[] then hd ys else hd xs)";
    1.36  by (list.induct_tac "xs" 1);
    1.37 @@ -57,14 +62,15 @@
    1.38  
    1.39  goal List.thy "rev(xs@ys) = rev(ys) @ rev(xs)";
    1.40  by (list.induct_tac "xs" 1);
    1.41 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [append_Nil2,append_assoc])));
    1.42 +by (ALLGOALS Asm_simp_tac);
    1.43  qed "rev_append";
    1.44 +Addsimps[rev_append];
    1.45  
    1.46  goal List.thy "rev(rev l) = l";
    1.47  by (list.induct_tac "l" 1);
    1.48 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [rev_append])));
    1.49 +by (ALLGOALS Asm_simp_tac);
    1.50  qed "rev_rev_ident";
    1.51 -
    1.52 +Addsimps[rev_rev_ident];
    1.53  
    1.54  (** mem **)
    1.55  
    1.56 @@ -72,11 +78,13 @@
    1.57  by (list.induct_tac "xs" 1);
    1.58  by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
    1.59  qed "mem_append";
    1.60 +Addsimps[mem_append];
    1.61  
    1.62  goal List.thy "x mem [x:xs.P(x)] = (x mem xs & P(x))";
    1.63  by (list.induct_tac "xs" 1);
    1.64  by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
    1.65  qed "mem_filter";
    1.66 +Addsimps[mem_filter];
    1.67  
    1.68  (** set_of_list **)
    1.69  
    1.70 @@ -85,6 +93,7 @@
    1.71  by (ALLGOALS Asm_simp_tac);
    1.72  by (Fast_tac 1);
    1.73  qed "set_of_list_append";
    1.74 +Addsimps[set_of_list_append];
    1.75  
    1.76  goal thy "(x mem xs) = (x: set_of_list xs)";
    1.77  by (list.induct_tac "xs" 1);
    1.78 @@ -100,17 +109,19 @@
    1.79  
    1.80  (** list_all **)
    1.81  
    1.82 -goal List.thy "(Alls x:xs.True) = True";
    1.83 +goal List.thy "list_all (%x.True) xs = True";
    1.84  by (list.induct_tac "xs" 1);
    1.85  by (ALLGOALS Asm_simp_tac);
    1.86  qed "list_all_True";
    1.87 +Addsimps [list_all_True];
    1.88  
    1.89  goal List.thy "list_all p (xs@ys) = (list_all p xs & list_all p ys)";
    1.90  by (list.induct_tac "xs" 1);
    1.91  by (ALLGOALS Asm_simp_tac);
    1.92 -qed "list_all_conj";
    1.93 +qed "list_all_append";
    1.94 +Addsimps [list_all_append];
    1.95  
    1.96 -goal List.thy "(Alls x:xs.P(x)) = (!x. x mem xs --> P(x))";
    1.97 +goal List.thy "list_all P xs = (!x. x mem xs --> P(x))";
    1.98  by (list.induct_tac "xs" 1);
    1.99  by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   1.100  by (Fast_tac 1);
   1.101 @@ -127,6 +138,11 @@
   1.102  by (Fast_tac 1);
   1.103  qed "expand_list_case";
   1.104  
   1.105 +val prems = goal List.thy "[| P([]); !!x xs. P(x#xs) |] ==> P(xs)";
   1.106 +by(list.induct_tac "xs" 1);
   1.107 +by(REPEAT(resolve_tac prems 1));
   1.108 +qed "list_cases";
   1.109 +
   1.110  goal List.thy  "(xs=[] --> P([])) & (!y ys. xs=y#ys --> P(y#ys)) --> P(xs)";
   1.111  by (list.induct_tac "xs" 1);
   1.112  by (Fast_tac 1);
   1.113 @@ -138,8 +154,9 @@
   1.114  
   1.115  goal List.thy  "flat(xs@ys) = flat(xs)@flat(ys)";
   1.116  by (list.induct_tac "xs" 1);
   1.117 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [append_assoc])));
   1.118 +by (ALLGOALS Asm_simp_tac);
   1.119  qed"flat_append";
   1.120 +Addsimps [flat_append];
   1.121  
   1.122  (** length **)
   1.123  
   1.124 @@ -238,32 +255,26 @@
   1.125  by (list.induct_tac "xs" 1);
   1.126  by (ALLGOALS Asm_simp_tac);
   1.127  qed "map_ident";
   1.128 +Addsimps[map_ident];
   1.129  
   1.130  goal List.thy "map f (xs@ys) = map f xs @ map f ys";
   1.131  by (list.induct_tac "xs" 1);
   1.132  by (ALLGOALS Asm_simp_tac);
   1.133  qed "map_append";
   1.134 +Addsimps[map_append];
   1.135  
   1.136  goalw List.thy [o_def] "map (f o g) xs = map f (map g xs)";
   1.137  by (list.induct_tac "xs" 1);
   1.138  by (ALLGOALS Asm_simp_tac);
   1.139  qed "map_compose";
   1.140 +Addsimps[map_compose];
   1.141  
   1.142  goal List.thy "rev(map f l) = map f (rev l)";
   1.143  by (list.induct_tac "l" 1);
   1.144 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [map_append])));
   1.145 +by (ALLGOALS Asm_simp_tac);
   1.146  qed "rev_map_distrib";
   1.147  
   1.148  goal List.thy "rev(flat ls) = flat (map rev (rev ls))";
   1.149  by (list.induct_tac "ls" 1);
   1.150 -by (ALLGOALS (asm_simp_tac (!simpset addsimps 
   1.151 -       [map_append, flat_append, rev_append, append_Nil2])));
   1.152 +by (ALLGOALS Asm_simp_tac);
   1.153  qed "rev_flat";
   1.154 -
   1.155 -Addsimps
   1.156 -  [not_Cons_self, append_assoc, append_Nil2, append_is_Nil, same_append_eq,
   1.157 -   mem_append, mem_filter,
   1.158 -   rev_append, rev_rev_ident,
   1.159 -   map_ident, map_append, map_compose,
   1.160 -   flat_append, list_all_True, list_all_conj];
   1.161 -
     2.1 --- a/src/HOL/List.thy	Fri Jan 17 10:04:28 1997 +0100
     2.2 +++ b/src/HOL/List.thy	Fri Jan 17 10:09:46 1997 +0100
     2.3 @@ -3,10 +3,7 @@
     2.4      Author:     Tobias Nipkow
     2.5      Copyright   1994 TU Muenchen
     2.6  
     2.7 -Definition of type 'a list as a datatype. This allows primrec to work.
     2.8 -
     2.9 -TODO: delete list_all from this theory and from ex/Sorting, etc.
    2.10 -      use set_of_list instead
    2.11 +The datatype of finite lists.
    2.12  *)
    2.13  
    2.14  List = Arith +
    2.15 @@ -35,18 +32,15 @@
    2.16    (* list Enumeration *)
    2.17    "@list"     :: args => 'a list                          ("[(_)]")
    2.18  
    2.19 -  (* Special syntax for list_all and filter *)
    2.20 -  "@Alls"     :: [idt, 'a list, bool] => bool             ("(2Alls _:_./ _)" 10)
    2.21 +  (* Special syntax for filter *)
    2.22    "@filter"   :: [idt, 'a list, bool] => 'a list          ("(1[_:_ ./ _])")
    2.23  
    2.24  translations
    2.25    "[x, xs]"     == "x#[xs]"
    2.26    "[x]"         == "x#[]"
    2.27    "[x:xs . P]"  == "filter (%x.P) xs"
    2.28 -  "Alls x:xs.P" == "list_all (%x.P) xs"
    2.29  
    2.30  syntax (symbols)
    2.31 -  "op #"      :: ['a, 'a list] => 'a list                 (infixr "\\<bullet>" 65)
    2.32    "@filter"   :: [idt, 'a list, bool] => 'a list          ("(1[_\\<in>_ ./ _])")
    2.33  
    2.34  
     3.1 --- a/src/HOL/equalities.ML	Fri Jan 17 10:04:28 1997 +0100
     3.2 +++ b/src/HOL/equalities.ML	Fri Jan 17 10:09:46 1997 +0100
     3.3 @@ -455,6 +455,18 @@
     3.4  by (Fast_tac 1);
     3.5  qed "Un_INT_distrib2";
     3.6  
     3.7 +
     3.8 +section"Bounded quantifiers";
     3.9 +
    3.10 +goal Set.thy "(!x:insert a A.P x) = (P a & (!x:A.P x))";
    3.11 +by (Fast_tac 1);
    3.12 +qed "Ball_insert";
    3.13 +
    3.14 +goal Set.thy "(!x:A Un B.P x) = ((!x:A.P x) & (!x:B.P x))";
    3.15 +by (Fast_tac 1);
    3.16 +qed "Ball_Un";
    3.17 +
    3.18 +
    3.19  section "-";
    3.20  
    3.21  goal Set.thy "A-A = {}";