summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | pusch |

Thu, 01 Apr 1999 18:42:48 +0200 | |

changeset 6408 | 5b443d6331ed |

parent 6407 | ec60d821f3f6 |

child 6409 | 41643761bef2 |

new definition for nth.
added warnings, if primrec definition is deleted from simpset.

src/HOL/List.ML | file | annotate | diff | comparison | revisions | |

src/HOL/List.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/List.ML Wed Mar 31 16:14:20 1999 +0200 +++ b/src/HOL/List.ML Thu Apr 01 18:42:48 1999 +0200 @@ -570,15 +570,23 @@ section "nth"; -Goal "(x#xs)!n = (case n of 0 => x | Suc m => xs!m)"; -by (simp_tac (simpset() addsplits [nat.split]) 1); -qed "nth_Cons"; +Goal "(x#xs)!0 = x"; +by Auto_tac; +qed "nth_Cons_0"; +Addsimps [nth_Cons_0]; -Goal "!xs. (xs@ys)!n = (if n < length xs then xs!n else ys!(n - length xs))"; -by (induct_tac "n" 1); +Goal "(x#xs)!(Suc n) = xs!n"; +by Auto_tac; +qed "nth_Cons_Suc"; +Addsimps [nth_Cons_Suc]; + +Delsimps (thms "nth.simps"); + +Goal "!n. (xs@ys)!n = (if n < length xs then xs!n else ys!(n - length xs))"; +by (induct_tac "xs" 1); by (Asm_simp_tac 1); by (rtac allI 1); - by (exhaust_tac "xs" 1); + by (exhaust_tac "n" 1); by Auto_tac; qed_spec_mp "nth_append";

--- a/src/HOL/List.thy Wed Mar 31 16:14:20 1999 +0200 +++ b/src/HOL/List.thy Thu Apr 01 18:42:48 1999 +0200 @@ -122,12 +122,17 @@ primrec drop_Nil "drop n [] = []" drop_Cons "drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)" + (* Warning: simpset does not contain this definition but separate theorems + for n=0 / n=Suc k*) primrec take_Nil "take n [] = []" take_Cons "take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)" -primrec - "xs!0 = hd xs" - "xs!(Suc n) = (tl xs)!n" + (* Warning: simpset does not contain this definition but separate theorems + for n=0 / n=Suc k*) +primrec + nth_Cons "(x#xs)!n = (case n of 0 => x | (Suc k) => xs!k)" + (* Warning: simpset does not contain this definition but separate theorems + for n=0 / n=Suc k*) primrec " [][i:=v] = []" "(x#xs)[i:=v] = (case i of 0 => v # xs @@ -141,6 +146,8 @@ primrec "zip xs [] = []" "zip xs (y#ys) = (case xs of [] => [] | z#zs => (z,y)#zip zs ys)" + (* Warning: simpset does not contain this definition but separate theorems + for xs=[] / xs=z#zs *) primrec "[i..0(] = []" "[i..(Suc j)(] = (if i <= j then [i..j(] @ [j] else [])" @@ -154,7 +161,7 @@ replicate_0 "replicate 0 x = []" replicate_Suc "replicate (Suc n) x = x # replicate n x" -(** Lexcicographic orderings on lists **) +(** Lexicographic orderings on lists **) consts lexn :: "('a * 'a)set => nat => ('a list * 'a list)set"