# HG changeset patch
# User nipkow
# Date 883476849 -3600
# Node ID 337c073de95e772b2c73d618d7c2f9c9442f791d
# Parent  5f629ee2502bab7cdcb98743635bcd5d3935365b
nth -> !

diff -r 5f629ee2502b -r 337c073de95e NEWS
--- a/NEWS	Mon Dec 29 21:39:22 1997 +0100
+++ b/NEWS	Tue Dec 30 11:14:09 1997 +0100
@@ -182,8 +182,10 @@
     "n ~= 0". Theorems and proof tools have been modified towards this
     `standard'.
 
-* HOL/Lists: the function "set_of_list" has been renamed "set"
-  (and its theorems too);
+* HOL/Lists:
+  the function "set_of_list" has been renamed "set" (and its theorems too);
+  the function "nth" now takes its arguments in the reverse order and
+  has acquired the infix notation "!" as in "xs!n".
 
 * HOL/Set: UNIV is now a constant and is no longer translated to Compl{};
 
diff -r 5f629ee2502b -r 337c073de95e src/HOL/List.ML
--- a/src/HOL/List.ML	Mon Dec 29 21:39:22 1997 +0100
+++ b/src/HOL/List.ML	Tue Dec 30 11:14:09 1997 +0100
@@ -438,8 +438,7 @@
 section "nth";
 
 goal thy
-  "!xs. nth n (xs@ys) = \
-\          (if n < length xs then nth n xs else nth (n - length xs) ys)";
+  "!xs. (xs@ys)!n = (if n < length xs then xs!n else ys!(n - length xs))";
 by (nat_ind_tac "n" 1);
  by (Asm_simp_tac 1);
  by (rtac allI 1);
@@ -450,7 +449,7 @@
  by (ALLGOALS Asm_simp_tac);
 qed_spec_mp "nth_append";
 
-goal thy "!n. n < length xs --> nth n (map f xs) = f (nth n xs)";
+goal thy "!n. n < length xs --> (map f xs)!n = f(xs!n)";
 by (induct_tac "xs" 1);
 (* case [] *)
 by (Asm_full_simp_tac 1);
@@ -461,7 +460,7 @@
 qed_spec_mp "nth_map";
 Addsimps [nth_map];
 
-goal thy "!n. n < length xs --> list_all P xs --> P(nth n xs)";
+goal thy "!n. n < length xs --> list_all P xs --> P(xs!n)";
 by (induct_tac "xs" 1);
 (* case [] *)
 by (Simp_tac 1);
@@ -471,7 +470,7 @@
 by (ALLGOALS Asm_full_simp_tac);
 qed_spec_mp "list_all_nth";
 
-goal thy "!n. n < length xs --> (nth n xs) mem xs";
+goal thy "!n. n < length xs --> xs!n mem xs";
 by (induct_tac "xs" 1);
 (* case [] *)
 by (Simp_tac 1);
@@ -643,7 +642,7 @@
 by (ALLGOALS Asm_simp_tac);
 qed_spec_mp "drop_map";
 
-goal thy "!n i. i < n --> nth i (take n xs) = nth i xs";
+goal thy "!n i. i < n --> (take n xs)!i = xs!i";
 by (induct_tac "xs" 1);
  by (ALLGOALS Asm_simp_tac);
 by (Clarify_tac 1);
@@ -654,7 +653,7 @@
 qed_spec_mp "nth_take";
 Addsimps [nth_take];
 
-goal thy  "!xs i. n + i <= length xs --> nth i (drop n xs) = nth (n + i) xs";
+goal thy  "!xs i. n + i <= length xs --> (drop n xs)!i = xs!(n+i)";
 by (nat_ind_tac "n" 1);
  by (ALLGOALS Asm_simp_tac);
 by (rtac allI 1);
diff -r 5f629ee2502b -r 337c073de95e src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Dec 29 21:39:22 1997 +0100
+++ b/src/HOL/List.thy	Tue Dec 30 11:14:09 1997 +0100
@@ -20,7 +20,7 @@
   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
+  nth         :: ['a list, nat] => 'a			  (infixl "!" 100)
   take, drop  :: [nat, 'a list] => 'a list
   takeWhile,
   dropWhile   :: ('a => bool) => 'a list => 'a list
@@ -106,8 +106,8 @@
   take_Nil  "take n [] = []"
   take_Cons "take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)"
 primrec nth nat
-  "nth 0 xs = hd xs"
-  "nth (Suc n) xs = nth n (tl xs)"
+  "xs!0 = hd xs"
+  "xs!(Suc n) = (tl xs)!n"
 primrec takeWhile list
   "takeWhile P [] = []"
   "takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])"
diff -r 5f629ee2502b -r 337c073de95e src/HOL/MiniML/Instance.thy
--- a/src/HOL/MiniML/Instance.thy	Mon Dec 29 21:39:22 1997 +0100
+++ b/src/HOL/MiniML/Instance.thy	Tue Dec 30 11:14:09 1997 +0100
@@ -44,6 +44,6 @@
   
 instance list :: (ord)ord
 defs le_env_def
-  "A <= B == length B = length A & (!i. i < length A --> nth i A <= nth i B)"
+  "A <= B == length B = length A & (!i. i < length A --> A!i <= B!i)"
 
 end
diff -r 5f629ee2502b -r 337c073de95e src/HOL/MiniML/MiniML.thy
--- a/src/HOL/MiniML/MiniML.thy	Mon Dec 29 21:39:22 1997 +0100
+++ b/src/HOL/MiniML/MiniML.thy	Tue Dec 30 11:14:09 1997 +0100
@@ -23,7 +23,7 @@
 
 inductive has_type
 intrs
-        VarI "[| n < length A; t <| (nth n A) |] ==> A |- Var n :: t"
+        VarI "[| n < length A; t <| A!n |] ==> A |- Var n :: t"
         AbsI "[| (mk_scheme t1)#A |- e :: t2 |] ==> A |- Abs e :: t1 -> t2"
         AppI "[| A |- e1 :: t2 -> t1; A |- e2 :: t2 |] 
               ==> A |- App e1 e2 :: t1"
diff -r 5f629ee2502b -r 337c073de95e src/HOL/MiniML/Type.ML
--- a/src/HOL/MiniML/Type.ML	Mon Dec 29 21:39:22 1997 +0100
+++ b/src/HOL/MiniML/Type.ML	Tue Dec 30 11:14:09 1997 +0100
@@ -146,7 +146,7 @@
 qed "free_tv_id_subst";
 Addsimps [free_tv_id_subst];
 
-goal thy "!!A. !n. n < length A --> x : free_tv (nth n A) --> x : free_tv A";
+goal thy "!!A. !n. n < length A --> x : free_tv (A!n) --> x : free_tv A";
 by (list.induct_tac "A" 1);
 by (Asm_full_simp_tac 1);
 by (rtac allI 1);
@@ -157,7 +157,7 @@
 
 Addsimps [free_tv_nth_A_impl_free_tv_A];
 
-goal thy "!!A. !nat. nat < length A --> x : free_tv (nth nat A) --> x : free_tv A";
+goal thy "!!A. !nat. nat < length A --> x : free_tv (A!nat) --> x : free_tv A";
 by (list.induct_tac "A" 1);
 by (Asm_full_simp_tac 1);
 by (rtac allI 1);
@@ -512,7 +512,8 @@
 by (Asm_simp_tac 1);
 qed_spec_mp "new_tv_only_depends_on_free_tv_scheme_list";
 
-goalw thy [new_tv_def] "!!A. !nat. nat < length A --> new_tv n A --> (new_tv n (nth nat A))";
+goalw thy [new_tv_def]
+  "!!A. !nat. nat < length A --> new_tv n A --> (new_tv n (A!nat))";
 by (list.induct_tac "A" 1);
 by (Asm_full_simp_tac 1);
 by (rtac allI 1);
@@ -750,7 +751,7 @@
 by (Simp_tac 1);
 qed "subst_id_on_type_scheme_list";
 
-goal thy "!!n. !n. n < length A --> nth n ($ S A) = $S (nth n A)";
+goal thy "!n. n < length A --> ($ S A)!n = $S (A!n)";
 by (list.induct_tac "A" 1);
 by (Asm_full_simp_tac 1);
 by (rtac allI 1);
diff -r 5f629ee2502b -r 337c073de95e src/HOL/MiniML/W.ML
--- a/src/HOL/MiniML/W.ML	Mon Dec 29 21:39:22 1997 +0100
+++ b/src/HOL/MiniML/W.ML	Tue Dec 30 11:14:09 1997 +0100
@@ -180,7 +180,7 @@
 by (simp_tac (simpset() addsimps
     [free_tv_subst] addsplits [split_option_bind,expand_if]) 1);
 by (strip_tac 1);
-by (case_tac "v : free_tv (nth nat A)" 1);
+by (case_tac "v : free_tv (A!nat)" 1);
 by (Asm_full_simp_tac 1);
 by (dtac free_tv_bound_typ_inst1 1);
 by (simp_tac (simpset() addsimps [o_def]) 1);
diff -r 5f629ee2502b -r 337c073de95e src/HOL/MiniML/W.thy
--- a/src/HOL/MiniML/W.thy	Mon Dec 29 21:39:22 1997 +0100
+++ b/src/HOL/MiniML/W.thy	Tue Dec 30 11:14:09 1997 +0100
@@ -20,8 +20,8 @@
 primrec W expr
   "W (Var i) A n =  
      (if i < length A then Some( id_subst,   
-	                         bound_typ_inst (%b. TVar(b+n)) (nth i A),   
-	                         n + (min_new_bound_tv (nth i A)) )  
+	                         bound_typ_inst (%b. TVar(b+n)) (A!i),   
+	                         n + (min_new_bound_tv (A!i)) )  
 	              else None)"
   
   "W (Abs e) A n = ( (S,t,m) := W e ((FVar n)#A) (Suc n);
diff -r 5f629ee2502b -r 337c073de95e src/HOL/W0/I.thy
--- a/src/HOL/W0/I.thy	Mon Dec 29 21:39:22 1997 +0100
+++ b/src/HOL/W0/I.thy	Tue Dec 30 11:14:09 1997 +0100
@@ -12,7 +12,7 @@
         I :: [expr, typ list, nat, subst] => result_W
 
 primrec I expr
-        "I (Var i) a n s = (if i < length a then Ok(s, nth i a, n)
+        "I (Var i) a n s = (if i < length a then Ok(s, a!i, n)
                                     else Fail)"
         "I (Abs e) a n s = ( (s,t,m) := I e ((TVar n)#a) (Suc n) s;
                                      Ok(s, TVar n -> t, m) )"
diff -r 5f629ee2502b -r 337c073de95e src/HOL/W0/MiniML.thy
--- a/src/HOL/W0/MiniML.thy	Mon Dec 29 21:39:22 1997 +0100
+++ b/src/HOL/W0/MiniML.thy	Tue Dec 30 11:14:09 1997 +0100
@@ -23,7 +23,7 @@
 
 inductive has_type
 intrs
-        VarI "[| n < length a |] ==> a |- Var n :: nth n a"
+        VarI "[| n < length a |] ==> a |- Var n :: a!n"
         AbsI "[| t1#a |- e :: t2 |] ==> a |- Abs e :: t1 -> t2"
         AppI "[| a |- e1 :: t2 -> t1; a |- e2 :: t2 |] 
               ==> a |- App e1 e2 :: t1"
diff -r 5f629ee2502b -r 337c073de95e src/HOL/W0/W.thy
--- a/src/HOL/W0/W.thy	Mon Dec 29 21:39:22 1997 +0100
+++ b/src/HOL/W0/W.thy	Tue Dec 30 11:14:09 1997 +0100
@@ -16,10 +16,10 @@
         W :: [expr, typ list, nat] => result_W
 
 primrec W expr
-  "W (Var i) a n = (if i < length a then Ok(id_subst, nth i a, n)
-                          else Fail)"
+  "W (Var i) a n = (if i < length a then Ok(id_subst, a!i, n)
+                    else Fail)"
   "W (Abs e) a n = ( (s,t,m) := W e ((TVar n)#a) (Suc n);
-                           Ok(s, (s n) -> t, m) )"
+                     Ok(s, (s n) -> t, m) )"
   "W (App e1 e2) a n =
                  ( (s1,t1,m1) := W e1 a n;
                    (s2,t2,m2) := W e2 ($s1 a) m1;