--- 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{};
--- 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);
--- 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 [])"
--- 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
--- 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"
--- 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);
--- 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);
--- 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);
--- 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) )"
--- 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"
--- 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;