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