re-added mem and list_all
authoroheimb
Mon Sep 21 23:03:11 1998 +0200 (1998-09-21)
changeset 5518654ead0ba4f7
parent 5517 863f56450888
child 5519 54e313ed22ba
re-added mem and list_all
src/HOL/List.ML
src/HOL/List.thy
src/HOL/MiniML/Generalize.thy
src/HOL/MiniML/Type.ML
src/HOL/W0/Type.ML
src/HOL/ex/Recdefs.ML
     1.1 --- a/src/HOL/List.ML	Mon Sep 21 22:58:43 1998 +0200
     1.2 +++ b/src/HOL/List.ML	Mon Sep 21 23:03:11 1998 +0200
     1.3 @@ -469,21 +469,31 @@
     1.4  bind_thm("in_listsI",in_lists_conv_set RS iffD2);
     1.5  AddSIs [in_listsI];
     1.6  
     1.7 +(** mem **)
     1.8 + 
     1.9 +section "mem";
    1.10 +
    1.11 +Goal "(x mem xs) = (x: set xs)";
    1.12 +by (induct_tac "xs" 1);
    1.13 +by Auto_tac;
    1.14 +qed "set_mem_eq";
    1.15 +
    1.16 +
    1.17  (** list_all **)
    1.18  
    1.19  section "list_all";
    1.20  
    1.21 +Goal "list_all P xs = (!x:set xs. P x)";
    1.22 +by (induct_tac "xs" 1);
    1.23 +by Auto_tac;
    1.24 +qed "list_all_conv";
    1.25 +
    1.26  Goal "list_all P (xs@ys) = (list_all P xs & list_all P ys)";
    1.27  by (induct_tac "xs" 1);
    1.28  by Auto_tac;
    1.29  qed "list_all_append";
    1.30  Addsimps [list_all_append];
    1.31  
    1.32 -Goal "list_all P xs = (!x. x mem xs --> P x)";
    1.33 -by (induct_tac "xs" 1);
    1.34 -by Auto_tac;
    1.35 -qed "list_all_conv";
    1.36 -
    1.37  
    1.38  (** filter **)
    1.39  
    1.40 @@ -583,7 +593,7 @@
    1.41  qed_spec_mp "nth_map";
    1.42  Addsimps [nth_map];
    1.43  
    1.44 -Goal "!n. n < length xs --> list_all P xs --> P(xs!n)";
    1.45 +Goal "!n. n < length xs --> Ball (set xs) P --> P(xs!n)";
    1.46  by (induct_tac "xs" 1);
    1.47  (* case [] *)
    1.48  by (Simp_tac 1);
    1.49 @@ -591,9 +601,9 @@
    1.50  by (rtac allI 1);
    1.51  by (induct_tac "n" 1);
    1.52  by Auto_tac;
    1.53 -qed_spec_mp "list_all_nth";
    1.54 +qed_spec_mp "list_ball_nth";
    1.55  
    1.56 -Goal "!n. n < length xs --> xs!n mem xs";
    1.57 +Goal "!n. n < length xs --> xs!n : set xs";
    1.58  by (induct_tac "xs" 1);
    1.59  (* case [] *)
    1.60  by (Simp_tac 1);
    1.61 @@ -607,6 +617,7 @@
    1.62  qed_spec_mp "nth_mem";
    1.63  Addsimps [nth_mem];
    1.64  
    1.65 +
    1.66  (** list update **)
    1.67  
    1.68  section "list update";
     2.1 --- a/src/HOL/List.thy	Mon Sep 21 22:58:43 1998 +0200
     2.2 +++ b/src/HOL/List.thy	Mon Sep 21 23:03:11 1998 +0200
     2.3 @@ -17,7 +17,9 @@
     2.4    foldl       :: [['b,'a] => 'b, 'b, 'a list] => 'b
     2.5    hd, last    :: 'a list => 'a
     2.6    set         :: 'a list => 'a set
     2.7 +  list_all    :: ('a => bool) => ('a list => bool)
     2.8    map         :: ('a=>'b) => ('a list => 'b list)
     2.9 +  mem         :: ['a, 'a list] => bool                    (infixl 55)
    2.10    nth         :: ['a list, nat] => 'a			  (infixl "!" 100)
    2.11    list_update :: 'a list => nat => 'a => 'a list
    2.12    take, drop  :: [nat, 'a list] => 'a list
    2.13 @@ -35,9 +37,6 @@
    2.14    lupdbinds  lupdbind
    2.15  
    2.16  syntax
    2.17 -  mem         :: ['a, 'a list] => bool                    (infixl 55)
    2.18 -  list_all    :: ('a => bool) => ('a list => bool)
    2.19 -
    2.20    (* list Enumeration *)
    2.21    "@list"     :: args => 'a list                          ("[(_)]")
    2.22  
    2.23 @@ -53,9 +52,6 @@
    2.24    upto        :: nat => nat => nat list                   ("(1[_../_])")
    2.25  
    2.26  translations
    2.27 -  "x mem xs"      == "x:set xs"
    2.28 -  "list_all P xs" == "Ball (set xs) P"
    2.29 -  
    2.30    "[x, xs]"     == "x#[xs]"
    2.31    "[x]"         == "x#[]"
    2.32    "[x:xs . P]"  == "filter (%x. P) xs"
    2.33 @@ -97,9 +93,15 @@
    2.34    "butlast [] = []"
    2.35    "butlast(x#xs) = (if xs=[] then [] else x#butlast xs)"
    2.36  primrec
    2.37 +  "x mem [] = False"
    2.38 +  "x mem (y#ys) = (if y=x then True else x mem ys)"
    2.39 +primrec
    2.40    "set [] = {}"
    2.41    "set (x#xs) = insert x (set xs)"
    2.42  primrec
    2.43 +  list_all_Nil  "list_all P [] = True"
    2.44 +  list_all_Cons "list_all P (x#xs) = (P(x) & list_all P xs)"
    2.45 +primrec
    2.46    "map f [] = []"
    2.47    "map f (x#xs) = f(x)#map f xs"
    2.48  primrec
     3.1 --- a/src/HOL/MiniML/Generalize.thy	Mon Sep 21 22:58:43 1998 +0200
     3.2 +++ b/src/HOL/MiniML/Generalize.thy	Mon Sep 21 23:03:11 1998 +0200
     3.3 @@ -26,7 +26,7 @@
     3.4    gen_ML_aux :: [nat list, typ] => type_scheme
     3.5  
     3.6  primrec
     3.7 -  "gen_ML_aux A (TVar n) = (if (n mem A) then (FVar n) else (BVar n))"
     3.8 +  "gen_ML_aux A (TVar n) = (if (n: set A) then (FVar n) else (BVar n))"
     3.9    "gen_ML_aux A (t1 -> t2) = (gen_ML_aux A t1) =-> (gen_ML_aux A t2)"
    3.10  
    3.11  consts
     4.1 --- a/src/HOL/MiniML/Type.ML	Mon Sep 21 22:58:43 1998 +0200
     4.2 +++ b/src/HOL/MiniML/Type.ML	Mon Sep 21 23:03:11 1998 +0200
     4.3 @@ -345,12 +345,12 @@
     4.4  
     4.5  Addsimps [free_tv_of_substitutions_extend_to_scheme_lists];
     4.6  
     4.7 -Goal "!!sch::type_scheme. (n : free_tv sch) = (n mem free_tv_ML sch)";
     4.8 +Goal "!!sch::type_scheme. (n : free_tv sch) = (n: set (free_tv_ML sch))";
     4.9  by (induct_tac "sch" 1);
    4.10  by (ALLGOALS Asm_simp_tac);
    4.11  qed "free_tv_ML_scheme";
    4.12  
    4.13 -Goal "!!A::type_scheme list. (n : free_tv A) = (n mem free_tv_ML A)";
    4.14 +Goal "!!A::type_scheme list. (n : free_tv A) = (n: set (free_tv_ML A))";
    4.15  by (induct_tac "A" 1);
    4.16  by (Simp_tac 1);
    4.17  by (asm_simp_tac (simpset() addsimps [free_tv_ML_scheme]) 1);
    4.18 @@ -405,7 +405,7 @@
    4.19  by (fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1);
    4.20  qed "new_tv_subst";
    4.21  
    4.22 -Goal "new_tv n x = list_all (new_tv n) x";
    4.23 +Goal "new_tv n x = (!y:set x. new_tv n y)";
    4.24  by (induct_tac "x" 1);
    4.25  by (ALLGOALS Asm_simp_tac);
    4.26  qed "new_tv_list";
    4.27 @@ -488,8 +488,7 @@
    4.28  qed_spec_mp "new_tv_subst_scheme_list";
    4.29  Addsimps [new_tv_subst_scheme_list];
    4.30  
    4.31 -Goal
    4.32 -  "new_tv n A --> new_tv (Suc n) ((TVar n)#A)";
    4.33 +Goal "new_tv n A --> new_tv (Suc n) ((TVar n)#A)";
    4.34  by (simp_tac (simpset() addsimps [new_tv_list]) 1);
    4.35  qed "new_tv_Suc_list";
    4.36  
     5.1 --- a/src/HOL/W0/Type.ML	Mon Sep 21 22:58:43 1998 +0200
     5.2 +++ b/src/HOL/W0/Type.ML	Mon Sep 21 23:03:11 1998 +0200
     5.3 @@ -146,7 +146,7 @@
     5.4  by (fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1);
     5.5  qed "new_tv_subst";
     5.6  
     5.7 -Goal "new_tv n x = list_all (new_tv n) x";
     5.8 +Goal "new_tv n x = (!y:set x. new_tv n y)";
     5.9  by (induct_tac "x" 1);
    5.10  by (ALLGOALS Asm_simp_tac);
    5.11  qed "new_tv_list";
    5.12 @@ -248,7 +248,7 @@
    5.13  Addsimps [new_tv_not_free_tv];
    5.14  
    5.15  Goal
    5.16 -  "(t::typ) mem ts --> free_tv t <= free_tv ts";
    5.17 +  "(t::typ): set ts --> free_tv t <= free_tv ts";
    5.18  by (induct_tac "ts" 1);
    5.19  (* case [] *)
    5.20  by (Simp_tac 1);
     6.1 --- a/src/HOL/ex/Recdefs.ML	Mon Sep 21 22:58:43 1998 +0200
     6.2 +++ b/src/HOL/ex/Recdefs.ML	Mon Sep 21 23:03:11 1998 +0200
     6.3 @@ -9,7 +9,7 @@
     6.4  
     6.5  Addsimps qsort.rules;
     6.6  
     6.7 -Goal "(x mem qsort (ord,l)) = (x mem l)";
     6.8 +Goal "(x: set (qsort (ord,l))) = (x: set l)";
     6.9  by (res_inst_tac [("u","ord"),("v","l")] qsort.induct 1);
    6.10  by (ALLGOALS Asm_simp_tac);
    6.11  by (Blast_tac 1);