Added function upto to List.
authornipkow
Wed Sep 02 16:52:06 1998 +0200 (1998-09-02)
changeset 5425157c6663dedd
parent 5424 771a68a468cc
child 5426 566f47250bd0
Added function upto to List.
Had to rearrange loading sequence because now List uses Recdef.
src/HOL/List.ML
src/HOL/List.thy
src/HOL/ROOT.ML
     1.1 --- a/src/HOL/List.ML	Wed Sep 02 10:37:13 1998 +0200
     1.2 +++ b/src/HOL/List.ML	Wed Sep 02 16:52:06 1998 +0200
     1.3 @@ -825,6 +825,29 @@
     1.4  qed_spec_mp "sum_eq_0_conv";
     1.5  AddIffs [sum_eq_0_conv];
     1.6  
     1.7 +(** upto **)
     1.8 +
     1.9 +Goal "!i j. ~ j < i --> j - i < Suc j - i";
    1.10 +by(strip_tac 1);
    1.11 +br diff_less_Suc_diff 1;
    1.12 +be leI 1;
    1.13 +val lemma = result();
    1.14 +
    1.15 +Goalw [upto_def] "j<i ==> [i..j] = []";
    1.16 +br trans 1;
    1.17 +brs paired_upto.rules 1;
    1.18 +br lemma 1;
    1.19 +by(Asm_simp_tac 1);
    1.20 +qed "upto_conv_Nil";
    1.21 +
    1.22 +Goalw [upto_def] "i<=j ==> [i..j] = i#[Suc i..j]";
    1.23 +br trans 1;
    1.24 +brs paired_upto.rules 1;
    1.25 +br lemma 1;
    1.26 +by(asm_simp_tac (simpset() addsimps [leD]) 1);
    1.27 +qed "upto_conv_Cons";
    1.28 +
    1.29 +Addsimps [upto_conv_Nil,upto_conv_Cons];
    1.30  
    1.31  (** nodups & remdups **)
    1.32  section "nodups & remdups";
     2.1 --- a/src/HOL/List.thy	Wed Sep 02 10:37:13 1998 +0200
     2.2 +++ b/src/HOL/List.thy	Wed Sep 02 16:52:06 1998 +0200
     2.3 @@ -6,7 +6,7 @@
     2.4  The datatype of finite lists.
     2.5  *)
     2.6  
     2.7 -List = WF_Rel + Datatype +
     2.8 +List = Datatype + Recdef +
     2.9  
    2.10  datatype 'a list = "[]" ("[]") | "#" 'a ('a list) (infixr 65)
    2.11  
    2.12 @@ -28,6 +28,8 @@
    2.13    tl, butlast :: 'a list => 'a list
    2.14    rev         :: 'a list => 'a list
    2.15    zip	      :: "'a list => 'b list => ('a * 'b) list"
    2.16 +  upto        :: nat => nat => nat list                   ("(1[_../_])")
    2.17 +  paired_upto :: "nat * nat => nat list"
    2.18    remdups     :: 'a list => 'a list
    2.19    nodups      :: "'a list => bool"
    2.20    replicate   :: nat => 'a => 'a list
    2.21 @@ -135,6 +137,9 @@
    2.22  primrec
    2.23    "zip xs []     = []"
    2.24    "zip xs (y#ys) = (hd xs,y)#zip (tl xs) ys"
    2.25 +recdef paired_upto "measure(%(i,j). (Suc j)-i)"
    2.26 +  "paired_upto(i,j) = (if j<i then [] else i#paired_upto(Suc i,j))"
    2.27 +defs upto_def  "[i..j] == paired_upto(i,j)"
    2.28  primrec
    2.29    "nodups []     = True"
    2.30    "nodups (x#xs) = (x ~: set xs & nodups xs)"
     3.1 --- a/src/HOL/ROOT.ML	Wed Sep 02 10:37:13 1998 +0200
     3.2 +++ b/src/HOL/ROOT.ML	Wed Sep 02 16:52:06 1998 +0200
     3.3 @@ -52,22 +52,21 @@
     3.4  use "Tools/datatype_abs_proofs.ML";
     3.5  use "Tools/datatype_package.ML";
     3.6  use "Tools/primrec_package.ML";
     3.7 +use_thy"Datatype";
     3.8  
     3.9  use_thy "Arith";
    3.10  use "arith_data.ML";
    3.11  
    3.12 -use_thy "Finite";
    3.13 -use_thy "Map";
    3.14 +use_thy "Recdef";
    3.15 +(*TFL: recursive function definitions*)
    3.16 +cd "$ISABELLE_HOME/src/TFL";
    3.17 +use "sys.sml";
    3.18 +cd "$ISABELLE_HOME/src/HOL";
    3.19  
    3.20  cd "Integ";
    3.21  use_thy "Bin";
    3.22  cd "..";
    3.23  
    3.24 -(*TFL: recursive function definitions*)
    3.25 -cd "$ISABELLE_HOME/src/TFL";
    3.26 -use "sys.sml";
    3.27 -cd "$ISABELLE_HOME/src/HOL";
    3.28 -
    3.29  (*the all-in-one theory*)
    3.30  use_thy "Main";
    3.31