src/CCL/ex/list.ML
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 290 37d580c16af5
permissions -rw-r--r--
tidying
     1 (*  Title: 	CCL/ex/list
     2     ID:         $Id$
     3     Author: 	Martin Coen, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 For list.thy.
     7 *)
     8 
     9 open List;
    10 
    11 val list_defs = [map_def,comp_def,append_def,filter_def,flat_def,
    12                  insert_def,isort_def,partition_def,qsort_def];
    13 
    14 (****)
    15 
    16 val listBs = map (fn s=>prove_goalw List.thy list_defs s (fn _ => [simp_tac term_ss 1]))
    17      ["(f o g) = (%a.f(g(a)))",
    18       "(f o g)(a) = f(g(a))",
    19       "map(f,[]) = []",
    20       "map(f,x$xs) = f(x)$map(f,xs)",
    21       "[] @ m = m",
    22       "x$xs @ m = x$(xs @ m)",
    23       "filter(f,[]) = []",
    24       "filter(f,x$xs) = if f`x then x$filter(f,xs) else filter(f,xs)",
    25       "flat([]) = []",
    26       "flat(x$xs) = x @ flat(xs)",
    27       "insert(f,a,[]) = a$[]",
    28       "insert(f,a,x$xs) = if f`a`x then a$x$xs else x$insert(f,a,xs)"];
    29 
    30 val list_ss = nat_ss addsimps listBs;
    31 
    32 (****)
    33 
    34 val [prem] = goal List.thy "n:Nat ==> map(f) ^ n ` [] = []";
    35 br (prem RS Nat_ind) 1;
    36 by (ALLGOALS (asm_simp_tac list_ss));
    37 val nmapBnil = result();
    38 
    39 val [prem] = goal List.thy "n:Nat ==> map(f)^n`(x$xs) = (f^n`x)$(map(f)^n`xs)";
    40 br (prem RS Nat_ind) 1;
    41 by (ALLGOALS (asm_simp_tac list_ss));
    42 val nmapBcons = result();
    43 
    44 (***)
    45 
    46 val prems = goalw List.thy [map_def]
    47   "[| !!x.x:A==>f(x):B;  l : List(A) |] ==> map(f,l) : List(B)";
    48 by (typechk_tac prems 1);
    49 val mapT = result();
    50 
    51 val prems = goalw List.thy [append_def]
    52   "[| l : List(A);  m : List(A) |] ==> l @ m : List(A)";
    53 by (typechk_tac prems 1);
    54 val appendT = result();
    55 
    56 val prems = goal List.thy
    57   "[| l : {l:List(A). m : {m:List(A).P(l @ m)}} |] ==> l @ m : {x:List(A). P(x)}";
    58 by (cut_facts_tac prems 1);
    59 by (fast_tac (set_cs addSIs [SubtypeI,appendT] addSEs [SubtypeE]) 1);
    60 val appendTS = result();
    61 
    62 val prems = goalw List.thy [filter_def]
    63   "[| f:A->Bool;   l : List(A) |] ==> filter(f,l) : List(A)";
    64 by (typechk_tac prems 1);
    65 val filterT = result();
    66 
    67 val prems = goalw List.thy [flat_def]
    68   "l : List(List(A)) ==> flat(l) : List(A)";
    69 by (typechk_tac (appendT::prems) 1);
    70 val flatT = result();
    71 
    72 val prems = goalw List.thy [insert_def]
    73   "[|  f : A->A->Bool; a:A; l : List(A) |] ==> insert(f,a,l) : List(A)";
    74 by (typechk_tac prems 1);
    75 val insertT = result();
    76 
    77 val prems = goal List.thy
    78   "[| f : {f:A->A->Bool. a : {a:A. l : {l:List(A).P(insert(f,a,l))}}} |] ==> \
    79 \  insert(f,a,l)  : {x:List(A). P(x)}";
    80 by (cut_facts_tac prems 1);
    81 by (fast_tac (set_cs addSIs [SubtypeI,insertT] addSEs [SubtypeE]) 1);
    82 val insertTS = result();
    83 
    84 val prems = goalw List.thy [partition_def]
    85   "[| f:A->Bool;  l : List(A) |] ==> partition(f,l) : List(A)*List(A)";
    86 by (typechk_tac prems 1);
    87 by clean_ccs_tac;
    88 br (ListPRI RS wfstI RS (ListPR_wf RS wmap_wf RS wfI)) 2;
    89 br (ListPRI RS wfstI RS (ListPR_wf RS wmap_wf RS wfI)) 1;
    90 by (REPEAT (atac 1));
    91 val partitionT = result();
    92 
    93 (*** Correctness Conditions for Insertion Sort ***)
    94 
    95 
    96 val prems = goalw List.thy [isort_def] 
    97     "f:A->A->Bool ==> isort(f) : PROD l:List(A).{x: List(A). Ord(f,x) & Perm(x,l)}";
    98 by (gen_ccs_tac  ([insertTS,insertT]@prems) 1);
    99 
   100 
   101 (*** Correctness Conditions for Quick Sort ***)
   102 
   103 val prems = goalw List.thy [qsort_def] 
   104     "f:A->A->Bool ==> qsort(f) : PROD l:List(A).{x: List(A). Ord(f,x) & Perm(x,l)}";
   105 by (gen_ccs_tac  ([partitionT,appendTS,appendT]@prems) 1);
   106