nth -> !
authornipkow
Tue Dec 30 11:14:09 1997 +0100 (1997-12-30)
changeset 4502337c073de95e
parent 4501 5f629ee2502b
child 4503 5ed72705c201
nth -> !
NEWS
src/HOL/List.ML
src/HOL/List.thy
src/HOL/MiniML/Instance.thy
src/HOL/MiniML/MiniML.thy
src/HOL/MiniML/Type.ML
src/HOL/MiniML/W.ML
src/HOL/MiniML/W.thy
src/HOL/W0/I.thy
src/HOL/W0/MiniML.thy
src/HOL/W0/W.thy
     1.1 --- a/NEWS	Mon Dec 29 21:39:22 1997 +0100
     1.2 +++ b/NEWS	Tue Dec 30 11:14:09 1997 +0100
     1.3 @@ -182,8 +182,10 @@
     1.4      "n ~= 0". Theorems and proof tools have been modified towards this
     1.5      `standard'.
     1.6  
     1.7 -* HOL/Lists: the function "set_of_list" has been renamed "set"
     1.8 -  (and its theorems too);
     1.9 +* HOL/Lists:
    1.10 +  the function "set_of_list" has been renamed "set" (and its theorems too);
    1.11 +  the function "nth" now takes its arguments in the reverse order and
    1.12 +  has acquired the infix notation "!" as in "xs!n".
    1.13  
    1.14  * HOL/Set: UNIV is now a constant and is no longer translated to Compl{};
    1.15  
     2.1 --- a/src/HOL/List.ML	Mon Dec 29 21:39:22 1997 +0100
     2.2 +++ b/src/HOL/List.ML	Tue Dec 30 11:14:09 1997 +0100
     2.3 @@ -438,8 +438,7 @@
     2.4  section "nth";
     2.5  
     2.6  goal thy
     2.7 -  "!xs. nth n (xs@ys) = \
     2.8 -\          (if n < length xs then nth n xs else nth (n - length xs) ys)";
     2.9 +  "!xs. (xs@ys)!n = (if n < length xs then xs!n else ys!(n - length xs))";
    2.10  by (nat_ind_tac "n" 1);
    2.11   by (Asm_simp_tac 1);
    2.12   by (rtac allI 1);
    2.13 @@ -450,7 +449,7 @@
    2.14   by (ALLGOALS Asm_simp_tac);
    2.15  qed_spec_mp "nth_append";
    2.16  
    2.17 -goal thy "!n. n < length xs --> nth n (map f xs) = f (nth n xs)";
    2.18 +goal thy "!n. n < length xs --> (map f xs)!n = f(xs!n)";
    2.19  by (induct_tac "xs" 1);
    2.20  (* case [] *)
    2.21  by (Asm_full_simp_tac 1);
    2.22 @@ -461,7 +460,7 @@
    2.23  qed_spec_mp "nth_map";
    2.24  Addsimps [nth_map];
    2.25  
    2.26 -goal thy "!n. n < length xs --> list_all P xs --> P(nth n xs)";
    2.27 +goal thy "!n. n < length xs --> list_all P xs --> P(xs!n)";
    2.28  by (induct_tac "xs" 1);
    2.29  (* case [] *)
    2.30  by (Simp_tac 1);
    2.31 @@ -471,7 +470,7 @@
    2.32  by (ALLGOALS Asm_full_simp_tac);
    2.33  qed_spec_mp "list_all_nth";
    2.34  
    2.35 -goal thy "!n. n < length xs --> (nth n xs) mem xs";
    2.36 +goal thy "!n. n < length xs --> xs!n mem xs";
    2.37  by (induct_tac "xs" 1);
    2.38  (* case [] *)
    2.39  by (Simp_tac 1);
    2.40 @@ -643,7 +642,7 @@
    2.41  by (ALLGOALS Asm_simp_tac);
    2.42  qed_spec_mp "drop_map";
    2.43  
    2.44 -goal thy "!n i. i < n --> nth i (take n xs) = nth i xs";
    2.45 +goal thy "!n i. i < n --> (take n xs)!i = xs!i";
    2.46  by (induct_tac "xs" 1);
    2.47   by (ALLGOALS Asm_simp_tac);
    2.48  by (Clarify_tac 1);
    2.49 @@ -654,7 +653,7 @@
    2.50  qed_spec_mp "nth_take";
    2.51  Addsimps [nth_take];
    2.52  
    2.53 -goal thy  "!xs i. n + i <= length xs --> nth i (drop n xs) = nth (n + i) xs";
    2.54 +goal thy  "!xs i. n + i <= length xs --> (drop n xs)!i = xs!(n+i)";
    2.55  by (nat_ind_tac "n" 1);
    2.56   by (ALLGOALS Asm_simp_tac);
    2.57  by (rtac allI 1);
     3.1 --- a/src/HOL/List.thy	Mon Dec 29 21:39:22 1997 +0100
     3.2 +++ b/src/HOL/List.thy	Tue Dec 30 11:14:09 1997 +0100
     3.3 @@ -20,7 +20,7 @@
     3.4    list_all    :: ('a => bool) => ('a list => bool)
     3.5    map         :: ('a=>'b) => ('a list => 'b list)
     3.6    mem         :: ['a, 'a list] => bool                    (infixl 55)
     3.7 -  nth         :: [nat, 'a list] => 'a
     3.8 +  nth         :: ['a list, nat] => 'a			  (infixl "!" 100)
     3.9    take, drop  :: [nat, 'a list] => 'a list
    3.10    takeWhile,
    3.11    dropWhile   :: ('a => bool) => 'a list => 'a list
    3.12 @@ -106,8 +106,8 @@
    3.13    take_Nil  "take n [] = []"
    3.14    take_Cons "take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)"
    3.15  primrec nth nat
    3.16 -  "nth 0 xs = hd xs"
    3.17 -  "nth (Suc n) xs = nth n (tl xs)"
    3.18 +  "xs!0 = hd xs"
    3.19 +  "xs!(Suc n) = (tl xs)!n"
    3.20  primrec takeWhile list
    3.21    "takeWhile P [] = []"
    3.22    "takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])"
     4.1 --- a/src/HOL/MiniML/Instance.thy	Mon Dec 29 21:39:22 1997 +0100
     4.2 +++ b/src/HOL/MiniML/Instance.thy	Tue Dec 30 11:14:09 1997 +0100
     4.3 @@ -44,6 +44,6 @@
     4.4    
     4.5  instance list :: (ord)ord
     4.6  defs le_env_def
     4.7 -  "A <= B == length B = length A & (!i. i < length A --> nth i A <= nth i B)"
     4.8 +  "A <= B == length B = length A & (!i. i < length A --> A!i <= B!i)"
     4.9  
    4.10  end
     5.1 --- a/src/HOL/MiniML/MiniML.thy	Mon Dec 29 21:39:22 1997 +0100
     5.2 +++ b/src/HOL/MiniML/MiniML.thy	Tue Dec 30 11:14:09 1997 +0100
     5.3 @@ -23,7 +23,7 @@
     5.4  
     5.5  inductive has_type
     5.6  intrs
     5.7 -        VarI "[| n < length A; t <| (nth n A) |] ==> A |- Var n :: t"
     5.8 +        VarI "[| n < length A; t <| A!n |] ==> A |- Var n :: t"
     5.9          AbsI "[| (mk_scheme t1)#A |- e :: t2 |] ==> A |- Abs e :: t1 -> t2"
    5.10          AppI "[| A |- e1 :: t2 -> t1; A |- e2 :: t2 |] 
    5.11                ==> A |- App e1 e2 :: t1"
     6.1 --- a/src/HOL/MiniML/Type.ML	Mon Dec 29 21:39:22 1997 +0100
     6.2 +++ b/src/HOL/MiniML/Type.ML	Tue Dec 30 11:14:09 1997 +0100
     6.3 @@ -146,7 +146,7 @@
     6.4  qed "free_tv_id_subst";
     6.5  Addsimps [free_tv_id_subst];
     6.6  
     6.7 -goal thy "!!A. !n. n < length A --> x : free_tv (nth n A) --> x : free_tv A";
     6.8 +goal thy "!!A. !n. n < length A --> x : free_tv (A!n) --> x : free_tv A";
     6.9  by (list.induct_tac "A" 1);
    6.10  by (Asm_full_simp_tac 1);
    6.11  by (rtac allI 1);
    6.12 @@ -157,7 +157,7 @@
    6.13  
    6.14  Addsimps [free_tv_nth_A_impl_free_tv_A];
    6.15  
    6.16 -goal thy "!!A. !nat. nat < length A --> x : free_tv (nth nat A) --> x : free_tv A";
    6.17 +goal thy "!!A. !nat. nat < length A --> x : free_tv (A!nat) --> x : free_tv A";
    6.18  by (list.induct_tac "A" 1);
    6.19  by (Asm_full_simp_tac 1);
    6.20  by (rtac allI 1);
    6.21 @@ -512,7 +512,8 @@
    6.22  by (Asm_simp_tac 1);
    6.23  qed_spec_mp "new_tv_only_depends_on_free_tv_scheme_list";
    6.24  
    6.25 -goalw thy [new_tv_def] "!!A. !nat. nat < length A --> new_tv n A --> (new_tv n (nth nat A))";
    6.26 +goalw thy [new_tv_def]
    6.27 +  "!!A. !nat. nat < length A --> new_tv n A --> (new_tv n (A!nat))";
    6.28  by (list.induct_tac "A" 1);
    6.29  by (Asm_full_simp_tac 1);
    6.30  by (rtac allI 1);
    6.31 @@ -750,7 +751,7 @@
    6.32  by (Simp_tac 1);
    6.33  qed "subst_id_on_type_scheme_list";
    6.34  
    6.35 -goal thy "!!n. !n. n < length A --> nth n ($ S A) = $S (nth n A)";
    6.36 +goal thy "!n. n < length A --> ($ S A)!n = $S (A!n)";
    6.37  by (list.induct_tac "A" 1);
    6.38  by (Asm_full_simp_tac 1);
    6.39  by (rtac allI 1);
     7.1 --- a/src/HOL/MiniML/W.ML	Mon Dec 29 21:39:22 1997 +0100
     7.2 +++ b/src/HOL/MiniML/W.ML	Tue Dec 30 11:14:09 1997 +0100
     7.3 @@ -180,7 +180,7 @@
     7.4  by (simp_tac (simpset() addsimps
     7.5      [free_tv_subst] addsplits [split_option_bind,expand_if]) 1);
     7.6  by (strip_tac 1);
     7.7 -by (case_tac "v : free_tv (nth nat A)" 1);
     7.8 +by (case_tac "v : free_tv (A!nat)" 1);
     7.9  by (Asm_full_simp_tac 1);
    7.10  by (dtac free_tv_bound_typ_inst1 1);
    7.11  by (simp_tac (simpset() addsimps [o_def]) 1);
     8.1 --- a/src/HOL/MiniML/W.thy	Mon Dec 29 21:39:22 1997 +0100
     8.2 +++ b/src/HOL/MiniML/W.thy	Tue Dec 30 11:14:09 1997 +0100
     8.3 @@ -20,8 +20,8 @@
     8.4  primrec W expr
     8.5    "W (Var i) A n =  
     8.6       (if i < length A then Some( id_subst,   
     8.7 -	                         bound_typ_inst (%b. TVar(b+n)) (nth i A),   
     8.8 -	                         n + (min_new_bound_tv (nth i A)) )  
     8.9 +	                         bound_typ_inst (%b. TVar(b+n)) (A!i),   
    8.10 +	                         n + (min_new_bound_tv (A!i)) )  
    8.11  	              else None)"
    8.12    
    8.13    "W (Abs e) A n = ( (S,t,m) := W e ((FVar n)#A) (Suc n);
     9.1 --- a/src/HOL/W0/I.thy	Mon Dec 29 21:39:22 1997 +0100
     9.2 +++ b/src/HOL/W0/I.thy	Tue Dec 30 11:14:09 1997 +0100
     9.3 @@ -12,7 +12,7 @@
     9.4          I :: [expr, typ list, nat, subst] => result_W
     9.5  
     9.6  primrec I expr
     9.7 -        "I (Var i) a n s = (if i < length a then Ok(s, nth i a, n)
     9.8 +        "I (Var i) a n s = (if i < length a then Ok(s, a!i, n)
     9.9                                      else Fail)"
    9.10          "I (Abs e) a n s = ( (s,t,m) := I e ((TVar n)#a) (Suc n) s;
    9.11                                       Ok(s, TVar n -> t, m) )"
    10.1 --- a/src/HOL/W0/MiniML.thy	Mon Dec 29 21:39:22 1997 +0100
    10.2 +++ b/src/HOL/W0/MiniML.thy	Tue Dec 30 11:14:09 1997 +0100
    10.3 @@ -23,7 +23,7 @@
    10.4  
    10.5  inductive has_type
    10.6  intrs
    10.7 -        VarI "[| n < length a |] ==> a |- Var n :: nth n a"
    10.8 +        VarI "[| n < length a |] ==> a |- Var n :: a!n"
    10.9          AbsI "[| t1#a |- e :: t2 |] ==> a |- Abs e :: t1 -> t2"
   10.10          AppI "[| a |- e1 :: t2 -> t1; a |- e2 :: t2 |] 
   10.11                ==> a |- App e1 e2 :: t1"
    11.1 --- a/src/HOL/W0/W.thy	Mon Dec 29 21:39:22 1997 +0100
    11.2 +++ b/src/HOL/W0/W.thy	Tue Dec 30 11:14:09 1997 +0100
    11.3 @@ -16,10 +16,10 @@
    11.4          W :: [expr, typ list, nat] => result_W
    11.5  
    11.6  primrec W expr
    11.7 -  "W (Var i) a n = (if i < length a then Ok(id_subst, nth i a, n)
    11.8 -                          else Fail)"
    11.9 +  "W (Var i) a n = (if i < length a then Ok(id_subst, a!i, n)
   11.10 +                    else Fail)"
   11.11    "W (Abs e) a n = ( (s,t,m) := W e ((TVar n)#a) (Suc n);
   11.12 -                           Ok(s, (s n) -> t, m) )"
   11.13 +                     Ok(s, (s n) -> t, m) )"
   11.14    "W (App e1 e2) a n =
   11.15                   ( (s1,t1,m1) := W e1 a n;
   11.16                     (s2,t2,m2) := W e2 ($s1 a) m1;