--- a/src/HOL/List.ML Fri Aug 16 11:27:10 1996 +0200
+++ b/src/HOL/List.ML Mon Aug 19 11:12:38 1996 +0200
@@ -80,19 +80,19 @@
by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
qed "mem_filter";
-(** setOfList **)
+(** set_of_list **)
-goal thy "setOfList (xs@ys) = (setOfList xs Un setOfList ys)";
+goal thy "set_of_list (xs@ys) = (set_of_list xs Un set_of_list ys)";
by (list.induct_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
by (Fast_tac 1);
-qed "setOfList_append";
+qed "set_of_list_append";
-goal thy "(x mem xs) = (x: setOfList xs)";
+goal thy "(x mem xs) = (x: set_of_list xs)";
by (list.induct_tac "xs" 1);
by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
by (Fast_tac 1);
-qed "setOfList_mem_eq";
+qed "set_of_list_mem_eq";
(** list_all **)
--- a/src/HOL/List.thy Fri Aug 16 11:27:10 1996 +0200
+++ b/src/HOL/List.thy Mon Aug 19 11:12:38 1996 +0200
@@ -6,7 +6,7 @@
Definition of type 'a list as a datatype. This allows primrec to work.
TODO: delete list_all from this theory and from ex/Sorting, etc.
- use setOfList instead
+ use set_of_list instead
*)
List = Arith +
@@ -15,29 +15,29 @@
consts
- "@" :: ['a list, 'a list] => 'a list (infixr 65)
- drop :: [nat, 'a list] => 'a list
- filter :: ['a => bool, 'a list] => 'a list
- flat :: 'a list list => 'a list
- foldl :: [['b,'a] => 'b, 'b, 'a list] => 'b
- hd :: 'a list => 'a
- length :: 'a list => nat
- setOfList :: ('a list => 'a set)
- list_all :: ('a => bool) => ('a list => bool)
- map :: ('a=>'b) => ('a list => 'b list)
- mem :: ['a, 'a list] => bool (infixl 55)
- nth :: [nat, 'a list] => 'a
- take :: [nat, 'a list] => 'a list
- tl,ttl :: 'a list => 'a list
- rev :: 'a list => 'a list
+ "@" :: ['a list, 'a list] => 'a list (infixr 65)
+ drop :: [nat, 'a list] => 'a list
+ filter :: ['a => bool, 'a list] => 'a list
+ flat :: 'a list list => 'a list
+ foldl :: [['b,'a] => 'b, 'b, 'a list] => 'b
+ hd :: 'a list => 'a
+ length :: 'a list => nat
+ set_of_list :: ('a list => 'a set)
+ list_all :: ('a => bool) => ('a list => bool)
+ map :: ('a=>'b) => ('a list => 'b list)
+ mem :: ['a, 'a list] => bool (infixl 55)
+ nth :: [nat, 'a list] => 'a
+ take :: [nat, 'a list] => 'a list
+ tl,ttl :: 'a list => 'a list
+ rev :: 'a list => 'a list
syntax
(* list Enumeration *)
- "@list" :: args => 'a list ("[(_)]")
+ "@list" :: args => 'a list ("[(_)]")
(* Special syntax for list_all and filter *)
- "@Alls" :: [idt, 'a list, bool] => bool ("(2Alls _:_./ _)" 10)
- "@filter" :: [idt, 'a list, bool] => 'a list ("(1[_:_ ./ _])")
+ "@Alls" :: [idt, 'a list, bool] => bool ("(2Alls _:_./ _)" 10)
+ "@filter" :: [idt, 'a list, bool] => 'a list ("(1[_:_ ./ _])")
translations
"[x, xs]" == "x#[xs]"
@@ -59,9 +59,9 @@
primrec "op mem" list
"x mem [] = False"
"x mem (y#ys) = (if y=x then True else x mem ys)"
-primrec setOfList list
- "setOfList [] = {}"
- "setOfList (x#xs) = insert x (setOfList xs)"
+primrec set_of_list list
+ "set_of_list [] = {}"
+ "set_of_list (x#xs) = insert x (set_of_list xs)"
primrec list_all list
list_all_Nil "list_all P [] = True"
list_all_Cons "list_all P (x#xs) = (P(x) & list_all P xs)"
--- a/src/HOL/ex/SList.ML Fri Aug 16 11:27:10 1996 +0200
+++ b/src/HOL/ex/SList.ML Mon Aug 19 11:12:38 1996 +0200
@@ -277,23 +277,23 @@
(*** Unfolding the basic combinators ***)
-val [null_Nil,null_Cons] = list_recs null_def;
-val [_,hd_Cons] = list_recs hd_def;
-val [_,tl_Cons] = list_recs tl_def;
-val [ttl_Nil,ttl_Cons] = list_recs ttl_def;
-val [append_Nil3,append_Cons] = list_recs append_def;
-val [mem_Nil, mem_Cons] = list_recs mem_def;
-val [setOfList_Nil,setOfList_Cons] = list_recs setOfList_def;
-val [map_Nil,map_Cons] = list_recs map_def;
-val [list_case_Nil,list_case_Cons] = list_recs list_case_def;
-val [filter_Nil,filter_Cons] = list_recs filter_def;
+val [null_Nil, null_Cons] = list_recs null_def;
+val [_, hd_Cons] = list_recs hd_def;
+val [_, tl_Cons] = list_recs tl_def;
+val [ttl_Nil, ttl_Cons] = list_recs ttl_def;
+val [append_Nil3, append_Cons] = list_recs append_def;
+val [mem_Nil, mem_Cons] = list_recs mem_def;
+val [set_of_list_Nil, set_of_list_Cons] = list_recs set_of_list_def;
+val [map_Nil, map_Cons] = list_recs map_def;
+val [list_case_Nil, list_case_Cons] = list_recs list_case_def;
+val [filter_Nil, filter_Cons] = list_recs filter_def;
Addsimps
[null_Nil, ttl_Nil,
mem_Nil, mem_Cons,
list_case_Nil, list_case_Cons,
append_Nil3, append_Cons,
- setOfList_Nil, setOfList_Cons,
+ set_of_list_Nil, set_of_list_Cons,
map_Nil, map_Cons,
filter_Nil, filter_Cons];
--- a/src/HOL/ex/SList.thy Fri Aug 16 11:27:10 1996 +0200
+++ b/src/HOL/ex/SList.thy Mon Aug 19 11:12:38 1996 +0200
@@ -21,35 +21,35 @@
consts
- list :: 'a item set => 'a item set
- Rep_list :: 'a list => 'a item
- Abs_list :: 'a item => 'a list
- NIL :: 'a item
- CONS :: ['a item, 'a item] => 'a item
- Nil :: 'a list
- "#" :: ['a, 'a list] => 'a list (infixr 65)
- List_case :: ['b, ['a item, 'a item]=>'b, 'a item] => 'b
- List_rec :: ['a item, 'b, ['a item, 'a item, 'b]=>'b] => 'b
- list_case :: ['b, ['a, 'a list]=>'b, 'a list] => 'b
- list_rec :: ['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b
- Rep_map :: ('b => 'a item) => ('b list => 'a item)
- Abs_map :: ('a item => 'b) => 'a item => 'b list
- null :: 'a list => bool
- hd :: 'a list => 'a
- tl,ttl :: 'a list => 'a list
- setOfList :: ('a list => 'a set)
- mem :: ['a, 'a list] => bool (infixl 55)
- map :: ('a=>'b) => ('a list => 'b list)
- "@" :: ['a list, 'a list] => 'a list (infixr 65)
- filter :: ['a => bool, 'a list] => 'a list
+ list :: 'a item set => 'a item set
+ Rep_list :: 'a list => 'a item
+ Abs_list :: 'a item => 'a list
+ NIL :: 'a item
+ CONS :: ['a item, 'a item] => 'a item
+ Nil :: 'a list
+ "#" :: ['a, 'a list] => 'a list (infixr 65)
+ List_case :: ['b, ['a item, 'a item]=>'b, 'a item] => 'b
+ List_rec :: ['a item, 'b, ['a item, 'a item, 'b]=>'b] => 'b
+ list_case :: ['b, ['a, 'a list]=>'b, 'a list] => 'b
+ list_rec :: ['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b
+ Rep_map :: ('b => 'a item) => ('b list => 'a item)
+ Abs_map :: ('a item => 'b) => 'a item => 'b list
+ null :: 'a list => bool
+ hd :: 'a list => 'a
+ tl,ttl :: 'a list => 'a list
+ set_of_list :: ('a list => 'a set)
+ mem :: ['a, 'a list] => bool (infixl 55)
+ map :: ('a=>'b) => ('a list => 'b list)
+ "@" :: ['a list, 'a list] => 'a list (infixr 65)
+ filter :: ['a => bool, 'a list] => 'a list
(* list Enumeration *)
- "[]" :: 'a list ("[]")
- "@list" :: args => 'a list ("[(_)]")
+ "[]" :: 'a list ("[]")
+ "@list" :: args => 'a list ("[(_)]")
(* Special syntax for filter *)
- "@filter" :: [idt, 'a list, bool] => 'a list ("(1[_:_ ./ _])")
+ "@filter" :: [idt, 'a list, bool] => 'a list ("(1[_:_ ./ _])")
translations
"[x, xs]" == "x#[xs]"
@@ -105,7 +105,7 @@
(* a total version of tl: *)
ttl_def "ttl(xs) == list_rec xs [] (%x xs r.xs)"
- setOfList_def "setOfList xs == list_rec xs {} (%x l r. insert x r)"
+ set_of_list_def "set_of_list xs == list_rec xs {} (%x l r. insert x r)"
mem_def "x mem xs ==
list_rec xs False (%y ys r. if y=x then True else r)"
--- a/src/HOL/ex/Term.ML Fri Aug 16 11:27:10 1996 +0200
+++ b/src/HOL/ex/Term.ML Mon Aug 19 11:12:38 1996 +0200
@@ -65,7 +65,7 @@
(*Induction for the abstract type 'a term*)
val prems = goalw Term.thy [App_def,Rep_Tlist_def,Abs_Tlist_def]
- "[| !!x ts. (ALL t: setOfList ts. R t) ==> R(App x ts) \
+ "[| !!x ts. (ALL t: set_of_list ts. R t) ==> R(App x ts) \
\ |] ==> R(t)";
by (rtac (Rep_term_inverse RS subst) 1); (*types force good instantiation*)
by (res_inst_tac [("P","Rep_term(t) : sexp")] conjunct2 1);