# HG changeset patch # User paulson # Date 840445958 -7200 # Node ID 55d8e38262a87f421022d89bda5933b924ecc674 # Parent d069f23e941f714fbc8eaf284cee63a9d0963feb Renamed setOfList to set_of_list diff -r d069f23e941f -r 55d8e38262a8 src/HOL/List.ML --- 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 **) diff -r d069f23e941f -r 55d8e38262a8 src/HOL/List.thy --- 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)" diff -r d069f23e941f -r 55d8e38262a8 src/HOL/ex/SList.ML --- 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]; diff -r d069f23e941f -r 55d8e38262a8 src/HOL/ex/SList.thy --- 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)" diff -r d069f23e941f -r 55d8e38262a8 src/HOL/ex/Term.ML --- 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);