# HG changeset patch
# User nipkow
# Date 904747926 -7200
# Node ID 157c6663dedde8564253fd216d0c28261b5ce8c5
# Parent  771a68a468ccb97c778d935b931a33cb43bc7b8e
Added function upto to List.
Had to rearrange loading sequence because now List uses Recdef.

diff -r 771a68a468cc -r 157c6663dedd src/HOL/List.ML
--- a/src/HOL/List.ML	Wed Sep 02 10:37:13 1998 +0200
+++ b/src/HOL/List.ML	Wed Sep 02 16:52:06 1998 +0200
@@ -825,6 +825,29 @@
 qed_spec_mp "sum_eq_0_conv";
 AddIffs [sum_eq_0_conv];
 
+(** upto **)
+
+Goal "!i j. ~ j < i --> j - i < Suc j - i";
+by(strip_tac 1);
+br diff_less_Suc_diff 1;
+be leI 1;
+val lemma = result();
+
+Goalw [upto_def] "j<i ==> [i..j] = []";
+br trans 1;
+brs paired_upto.rules 1;
+br lemma 1;
+by(Asm_simp_tac 1);
+qed "upto_conv_Nil";
+
+Goalw [upto_def] "i<=j ==> [i..j] = i#[Suc i..j]";
+br trans 1;
+brs paired_upto.rules 1;
+br lemma 1;
+by(asm_simp_tac (simpset() addsimps [leD]) 1);
+qed "upto_conv_Cons";
+
+Addsimps [upto_conv_Nil,upto_conv_Cons];
 
 (** nodups & remdups **)
 section "nodups & remdups";
diff -r 771a68a468cc -r 157c6663dedd src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Sep 02 10:37:13 1998 +0200
+++ b/src/HOL/List.thy	Wed Sep 02 16:52:06 1998 +0200
@@ -6,7 +6,7 @@
 The datatype of finite lists.
 *)
 
-List = WF_Rel + Datatype +
+List = Datatype + Recdef +
 
 datatype 'a list = "[]" ("[]") | "#" 'a ('a list) (infixr 65)
 
@@ -28,6 +28,8 @@
   tl, butlast :: 'a list => 'a list
   rev         :: 'a list => 'a list
   zip	      :: "'a list => 'b list => ('a * 'b) list"
+  upto        :: nat => nat => nat list                   ("(1[_../_])")
+  paired_upto :: "nat * nat => nat list"
   remdups     :: 'a list => 'a list
   nodups      :: "'a list => bool"
   replicate   :: nat => 'a => 'a list
@@ -135,6 +137,9 @@
 primrec
   "zip xs []     = []"
   "zip xs (y#ys) = (hd xs,y)#zip (tl xs) ys"
+recdef paired_upto "measure(%(i,j). (Suc j)-i)"
+  "paired_upto(i,j) = (if j<i then [] else i#paired_upto(Suc i,j))"
+defs upto_def  "[i..j] == paired_upto(i,j)"
 primrec
   "nodups []     = True"
   "nodups (x#xs) = (x ~: set xs & nodups xs)"
diff -r 771a68a468cc -r 157c6663dedd src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Wed Sep 02 10:37:13 1998 +0200
+++ b/src/HOL/ROOT.ML	Wed Sep 02 16:52:06 1998 +0200
@@ -52,22 +52,21 @@
 use "Tools/datatype_abs_proofs.ML";
 use "Tools/datatype_package.ML";
 use "Tools/primrec_package.ML";
+use_thy"Datatype";
 
 use_thy "Arith";
 use "arith_data.ML";
 
-use_thy "Finite";
-use_thy "Map";
+use_thy "Recdef";
+(*TFL: recursive function definitions*)
+cd "$ISABELLE_HOME/src/TFL";
+use "sys.sml";
+cd "$ISABELLE_HOME/src/HOL";
 
 cd "Integ";
 use_thy "Bin";
 cd "..";
 
-(*TFL: recursive function definitions*)
-cd "$ISABELLE_HOME/src/TFL";
-use "sys.sml";
-cd "$ISABELLE_HOME/src/HOL";
-
 (*the all-in-one theory*)
 use_thy "Main";