src/CCL/ex/List.thy
author blanchet
Mon, 15 Sep 2014 10:49:07 +0200
changeset 58335 a5a3b576fcfb
parent 45010 8a4db903039f
child 58889 5b7a9633cfa8
permissions -rw-r--r--
generate 'code' attribute only if 'code' plugin is enabled
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17456
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3837
diff changeset
     1
(*  Title:      CCL/ex/List.thy
1474
3f7d67927fe2 expanded tabs
clasohm
parents: 1149
diff changeset
     2
    Author:     Martin Coen, Cambridge University Computer Laboratory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Copyright   1993  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
17456
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3837
diff changeset
     6
header {* Programs defined over lists *}
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3837
diff changeset
     7
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3837
diff changeset
     8
theory List
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3837
diff changeset
     9
imports Nat
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3837
diff changeset
    10
begin
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
42155
ffe99b07c9c0 modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents: 35762
diff changeset
    12
definition map :: "[i=>i,i]=>i"
ffe99b07c9c0 modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents: 35762
diff changeset
    13
  where "map(f,l) == lrec(l,[],%x xs g. f(x)$g)"
ffe99b07c9c0 modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents: 35762
diff changeset
    14
ffe99b07c9c0 modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents: 35762
diff changeset
    15
definition comp :: "[i=>i,i=>i]=>i=>i"  (infixr "\<circ>" 55)
ffe99b07c9c0 modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents: 35762
diff changeset
    16
  where "f \<circ> g == (%x. f(g(x)))"
ffe99b07c9c0 modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents: 35762
diff changeset
    17
ffe99b07c9c0 modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents: 35762
diff changeset
    18
definition append :: "[i,i]=>i"  (infixr "@" 55)
ffe99b07c9c0 modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents: 35762
diff changeset
    19
  where "l @ m == lrec(l,m,%x xs g. x$g)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
42155
ffe99b07c9c0 modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents: 35762
diff changeset
    21
axiomatization member :: "[i,i]=>i"  (infixr "mem" 55)  (* FIXME dangling eq *)
45010
8a4db903039f proper fact binding;
wenzelm
parents: 42155
diff changeset
    22
  where member_ax: "a mem l == lrec(l,false,%h t g. if eq(a,h) then true else g)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
42155
ffe99b07c9c0 modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents: 35762
diff changeset
    24
definition filter :: "[i,i]=>i"
ffe99b07c9c0 modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents: 35762
diff changeset
    25
  where "filter(f,l) == lrec(l,[],%x xs g. if f`x then x$g else g)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
42155
ffe99b07c9c0 modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents: 35762
diff changeset
    27
definition flat :: "i=>i"
ffe99b07c9c0 modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents: 35762
diff changeset
    28
  where "flat(l) == lrec(l,[],%h t g. h @ g)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
42155
ffe99b07c9c0 modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents: 35762
diff changeset
    30
definition partition :: "[i,i]=>i" where
1149
5750eba8820d removed \...\ inside strings
clasohm
parents: 290
diff changeset
    31
  "partition(f,l) == letrec part l a b be lcase(l,<a,b>,%x xs.
17456
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3837
diff changeset
    32
                            if f`x then part(xs,x$a,b) else part(xs,a,x$b))
1149
5750eba8820d removed \...\ inside strings
clasohm
parents: 290
diff changeset
    33
                    in part(l,[],[])"
42155
ffe99b07c9c0 modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents: 35762
diff changeset
    34
ffe99b07c9c0 modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents: 35762
diff changeset
    35
definition insert :: "[i,i,i]=>i"
ffe99b07c9c0 modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents: 35762
diff changeset
    36
  where "insert(f,a,l) == lrec(l,a$[],%h t g. if f`a`h then a$h$t else h$g)"
ffe99b07c9c0 modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents: 35762
diff changeset
    37
ffe99b07c9c0 modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents: 35762
diff changeset
    38
definition isort :: "i=>i"
ffe99b07c9c0 modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents: 35762
diff changeset
    39
  where "isort(f) == lam l. lrec(l,[],%h t g. insert(f,h,g))"
ffe99b07c9c0 modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents: 35762
diff changeset
    40
ffe99b07c9c0 modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents: 35762
diff changeset
    41
definition qsort :: "i=>i" where
ffe99b07c9c0 modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents: 35762
diff changeset
    42
  "qsort(f) == lam l. letrec qsortx l be lcase(l,[],%h t.
17456
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3837
diff changeset
    43
                                   let p be partition(f`h,t)
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3837
diff changeset
    44
                                   in split(p,%x y. qsortx(x) @ h$qsortx(y)))
1149
5750eba8820d removed \...\ inside strings
clasohm
parents: 290
diff changeset
    45
                          in qsortx(l)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    47
lemmas list_defs = map_def comp_def append_def filter_def flat_def
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    48
  insert_def isort_def partition_def qsort_def
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    49
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    50
lemma listBs [simp]:
42155
ffe99b07c9c0 modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents: 35762
diff changeset
    51
  "!!f g. (f \<circ> g) = (%a. f(g(a)))"
ffe99b07c9c0 modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents: 35762
diff changeset
    52
  "!!a f g. (f \<circ> g)(a) = f(g(a))"
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    53
  "!!f. map(f,[]) = []"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    54
  "!!f x xs. map(f,x$xs) = f(x)$map(f,xs)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    55
  "!!m. [] @ m = m"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    56
  "!!x xs m. x$xs @ m = x$(xs @ m)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    57
  "!!f. filter(f,[]) = []"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    58
  "!!f x xs. filter(f,x$xs) = if f`x then x$filter(f,xs) else filter(f,xs)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    59
  "flat([]) = []"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    60
  "!!x xs. flat(x$xs) = x @ flat(xs)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    61
  "!!a f. insert(f,a,[]) = a$[]"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    62
  "!!a f xs. insert(f,a,x$xs) = if f`a`x then a$x$xs else x$insert(f,a,xs)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    63
  by (simp_all add: list_defs)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    64
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    65
lemma nmapBnil: "n:Nat ==> map(f) ^ n ` [] = []"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    66
  apply (erule Nat_ind)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    67
   apply simp_all
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    68
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    69
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    70
lemma nmapBcons: "n:Nat ==> map(f)^n`(x$xs) = (f^n`x)$(map(f)^n`xs)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    71
  apply (erule Nat_ind)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    72
   apply simp_all
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    73
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    74
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    75
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    76
lemma mapT: "[| !!x. x:A==>f(x):B;  l : List(A) |] ==> map(f,l) : List(B)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    77
  apply (unfold map_def)
27221
31328dc30196 proper context for tactics derived from res_inst_tac;
wenzelm
parents: 24825
diff changeset
    78
  apply (tactic "typechk_tac @{context} [] 1")
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    79
  apply blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    80
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    81
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    82
lemma appendT: "[| l : List(A);  m : List(A) |] ==> l @ m : List(A)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    83
  apply (unfold append_def)
27221
31328dc30196 proper context for tactics derived from res_inst_tac;
wenzelm
parents: 24825
diff changeset
    84
  apply (tactic "typechk_tac @{context} [] 1")
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    85
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    86
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    87
lemma appendTS:
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    88
  "[| l : {l:List(A). m : {m:List(A).P(l @ m)}} |] ==> l @ m : {x:List(A). P(x)}"
42155
ffe99b07c9c0 modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents: 35762
diff changeset
    89
  by (blast intro!: appendT)
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    90
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    91
lemma filterT: "[| f:A->Bool;   l : List(A) |] ==> filter(f,l) : List(A)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    92
  apply (unfold filter_def)
27221
31328dc30196 proper context for tactics derived from res_inst_tac;
wenzelm
parents: 24825
diff changeset
    93
  apply (tactic "typechk_tac @{context} [] 1")
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    94
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    95
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    96
lemma flatT: "l : List(List(A)) ==> flat(l) : List(A)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    97
  apply (unfold flat_def)
27221
31328dc30196 proper context for tactics derived from res_inst_tac;
wenzelm
parents: 24825
diff changeset
    98
  apply (tactic {* typechk_tac @{context} @{thms appendT} 1 *})
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    99
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   100
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   101
lemma insertT: "[|  f : A->A->Bool; a:A; l : List(A) |] ==> insert(f,a,l) : List(A)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   102
  apply (unfold insert_def)
27221
31328dc30196 proper context for tactics derived from res_inst_tac;
wenzelm
parents: 24825
diff changeset
   103
  apply (tactic "typechk_tac @{context} [] 1")
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   104
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   105
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   106
lemma insertTS:
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   107
  "[| f : {f:A->A->Bool. a : {a:A. l : {l:List(A).P(insert(f,a,l))}}} |] ==>  
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   108
   insert(f,a,l)  : {x:List(A). P(x)}"
42155
ffe99b07c9c0 modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents: 35762
diff changeset
   109
  by (blast intro!: insertT)
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   110
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   111
lemma partitionT:
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   112
  "[| f:A->Bool;  l : List(A) |] ==> partition(f,l) : List(A)*List(A)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   113
  apply (unfold partition_def)
27221
31328dc30196 proper context for tactics derived from res_inst_tac;
wenzelm
parents: 24825
diff changeset
   114
  apply (tactic "typechk_tac @{context} [] 1")
31328dc30196 proper context for tactics derived from res_inst_tac;
wenzelm
parents: 24825
diff changeset
   115
  apply (tactic "clean_ccs_tac @{context}")
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   116
  apply (rule ListPRI [THEN wfstI, THEN ListPR_wf [THEN wmap_wf, THEN wfI]])
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   117
    apply assumption+
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   118
  apply (rule ListPRI [THEN wfstI, THEN ListPR_wf [THEN wmap_wf, THEN wfI]])
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   119
   apply assumption+
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   120
  done
17456
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3837
diff changeset
   121
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
end