src/ZF/List_ZF.thy
author wenzelm
Wed, 27 Mar 2013 16:38:25 +0100
changeset 51553 63327f679cff
parent 46953 2b6e55924af3
child 58860 fee7cfa69c50
permissions -rw-r--r--
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26056
diff changeset
     1
(*  Title:      ZF/List_ZF.thy
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
     3
    Copyright   1994  University of Cambridge
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
     4
*)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
     5
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
     6
header{*Lists in Zermelo-Fraenkel Set Theory*}
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
     7
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
     8
theory List_ZF imports Datatype_ZF ArithSimp begin
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
     9
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    10
consts
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    11
  list       :: "i=>i"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    12
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    13
datatype
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
    14
  "list(A)" = Nil | Cons ("a \<in> A", "l \<in> list(A)")
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    15
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    16
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    17
syntax
35425
d4e747d3a874 standard convention for syntax consts;
wenzelm
parents: 35112
diff changeset
    18
 "_Nil" :: i  ("[]")
d4e747d3a874 standard convention for syntax consts;
wenzelm
parents: 35112
diff changeset
    19
 "_List" :: "is => i"  ("[(_)]")
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    20
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    21
translations
35068
544867142ea4 modernized translations;
wenzelm
parents: 32960
diff changeset
    22
  "[x, xs]"     == "CONST Cons(x, [xs])"
544867142ea4 modernized translations;
wenzelm
parents: 32960
diff changeset
    23
  "[x]"         == "CONST Cons(x, [])"
544867142ea4 modernized translations;
wenzelm
parents: 32960
diff changeset
    24
  "[]"          == "CONST Nil"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    25
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    26
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    27
consts
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    28
  length :: "i=>i"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    29
  hd     :: "i=>i"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    30
  tl     :: "i=>i"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    31
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    32
primrec
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    33
  "length([]) = 0"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    34
  "length(Cons(a,l)) = succ(length(l))"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    35
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    36
primrec
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    37
  "hd([]) = 0"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    38
  "hd(Cons(a,l)) = a"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    39
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    40
primrec
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    41
  "tl([]) = []"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    42
  "tl(Cons(a,l)) = l"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    43
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    44
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    45
consts
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    46
  map         :: "[i=>i, i] => i"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    47
  set_of_list :: "i=>i"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    48
  app         :: "[i,i]=>i"                        (infixr "@" 60)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    49
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    50
(*map is a binding operator -- it applies to meta-level functions, not
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    51
object-level functions.  This simplifies the final form of term_rec_conv,
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    52
although complicating its derivation.*)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    53
primrec
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    54
  "map(f,[]) = []"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    55
  "map(f,Cons(a,l)) = Cons(f(a), map(f,l))"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    56
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    57
primrec
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    58
  "set_of_list([]) = 0"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    59
  "set_of_list(Cons(a,l)) = cons(a, set_of_list(l))"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    60
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    61
primrec
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    62
  app_Nil:  "[] @ ys = ys"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    63
  app_Cons: "(Cons(a,l)) @ ys = Cons(a, l @ ys)"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    64
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    65
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    66
consts
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    67
  rev :: "i=>i"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    68
  flat       :: "i=>i"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    69
  list_add   :: "i=>i"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    70
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    71
primrec
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    72
  "rev([]) = []"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    73
  "rev(Cons(a,l)) = rev(l) @ [a]"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    74
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    75
primrec
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    76
  "flat([]) = []"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    77
  "flat(Cons(l,ls)) = l @ flat(ls)"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    78
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    79
primrec
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    80
  "list_add([]) = 0"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    81
  "list_add(Cons(a,l)) = a #+ list_add(l)"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    82
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    83
consts
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    84
  drop       :: "[i,i]=>i"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    85
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    86
primrec
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    87
  drop_0:    "drop(0,l) = l"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    88
  drop_succ: "drop(succ(i), l) = tl (drop(i,l))"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    89
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    90
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    91
(*** Thanks to Sidi Ehmety for the following ***)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    92
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    93
definition
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    94
(* Function `take' returns the first n elements of a list *)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    95
  take     :: "[i,i]=>i"  where
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
    96
  "take(n, as) == list_rec(\<lambda>n\<in>nat. [],
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
    97
                %a l r. \<lambda>n\<in>nat. nat_case([], %m. Cons(a, r`m), n), as)`n"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    98
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    99
definition
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   100
  nth :: "[i, i]=>i"  where
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   101
  --{*returns the (n+1)th element of a list, or 0 if the
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   102
   list is too short.*}
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   103
  "nth(n, as) == list_rec(\<lambda>n\<in>nat. 0,
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   104
                          %a l r. \<lambda>n\<in>nat. nat_case(a, %m. r`m, n), as) ` n"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   105
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   106
definition
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   107
  list_update :: "[i, i, i]=>i"  where
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   108
  "list_update(xs, i, v) == list_rec(\<lambda>n\<in>nat. Nil,
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   109
      %u us vs. \<lambda>n\<in>nat. nat_case(Cons(v, us), %m. Cons(u, vs`m), n), xs)`i"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   110
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   111
consts
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   112
  filter :: "[i=>o, i] => i"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   113
  upt :: "[i, i] =>i"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   114
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   115
primrec
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   116
  "filter(P, Nil) = Nil"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   117
  "filter(P, Cons(x, xs)) =
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   118
     (if P(x) then Cons(x, filter(P, xs)) else filter(P, xs))"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   119
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   120
primrec
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   121
  "upt(i, 0) = Nil"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   122
  "upt(i, succ(j)) = (if i \<le> j then upt(i, j)@[j] else Nil)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   123
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   124
definition
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   125
  min :: "[i,i] =>i"  where
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   126
    "min(x, y) == (if x \<le> y then x else y)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   127
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   128
definition
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   129
  max :: "[i, i] =>i"  where
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   130
    "max(x, y) == (if x \<le> y then y else x)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   131
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   132
(*** Aspects of the datatype definition ***)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   133
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   134
declare list.intros [simp,TC]
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   135
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   136
(*An elimination rule, for type-checking*)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   137
inductive_cases ConsE: "Cons(a,l) \<in> list(A)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   138
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   139
lemma Cons_type_iff [simp]: "Cons(a,l) \<in> list(A) \<longleftrightarrow> a \<in> A & l \<in> list(A)"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   140
by (blast elim: ConsE)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   141
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   142
(*Proving freeness results*)
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   143
lemma Cons_iff: "Cons(a,l)=Cons(a',l') \<longleftrightarrow> a=a' & l=l'"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   144
by auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   145
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   146
lemma Nil_Cons_iff: "~ Nil=Cons(a,l)"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   147
by auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   148
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   149
lemma list_unfold: "list(A) = {0} + (A * list(A))"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   150
by (blast intro!: list.intros [unfolded list.con_defs]
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   151
          elim: list.cases [unfolded list.con_defs])
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   152
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   153
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   154
(**  Lemmas to justify using "list" in other recursive type definitions **)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   155
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   156
lemma list_mono: "A<=B ==> list(A) \<subseteq> list(B)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   157
apply (unfold list.defs )
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   158
apply (rule lfp_mono)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   159
apply (simp_all add: list.bnd_mono)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   160
apply (assumption | rule univ_mono basic_monos)+
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   161
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   162
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   163
(*There is a similar proof by list induction.*)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   164
lemma list_univ: "list(univ(A)) \<subseteq> univ(A)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   165
apply (unfold list.defs list.con_defs)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   166
apply (rule lfp_lowerbound)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   167
apply (rule_tac [2] A_subset_univ [THEN univ_mono])
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   168
apply (blast intro!: zero_in_univ Inl_in_univ Inr_in_univ Pair_in_univ)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   169
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   170
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   171
(*These two theorems justify datatypes involving list(nat), list(A), ...*)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   172
lemmas list_subset_univ = subset_trans [OF list_mono list_univ]
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   173
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   174
lemma list_into_univ: "[| l \<in> list(A);  A \<subseteq> univ(B) |] ==> l \<in> univ(B)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   175
by (blast intro: list_subset_univ [THEN subsetD])
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   176
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   177
lemma list_case_type:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   178
    "[| l \<in> list(A);
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   179
        c \<in> C(Nil);
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   180
        !!x y. [| x \<in> A;  y \<in> list(A) |] ==> h(x,y): C(Cons(x,y))
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   181
     |] ==> list_case(c,h,l) \<in> C(l)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   182
by (erule list.induct, auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   183
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   184
lemma list_0_triv: "list(0) = {Nil}"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   185
apply (rule equalityI, auto)
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   186
apply (induct_tac x, auto)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   187
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   188
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   189
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   190
(*** List functions ***)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   191
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   192
lemma tl_type: "l \<in> list(A) ==> tl(l) \<in> list(A)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   193
apply (induct_tac "l")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   194
apply (simp_all (no_asm_simp) add: list.intros)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   195
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   196
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   197
(** drop **)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   198
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   199
lemma drop_Nil [simp]: "i \<in> nat ==> drop(i, Nil) = Nil"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   200
apply (induct_tac "i")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   201
apply (simp_all (no_asm_simp))
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   202
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   203
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   204
lemma drop_succ_Cons [simp]: "i \<in> nat ==> drop(succ(i), Cons(a,l)) = drop(i,l)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   205
apply (rule sym)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   206
apply (induct_tac "i")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   207
apply (simp (no_asm))
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   208
apply (simp (no_asm_simp))
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   209
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   210
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   211
lemma drop_type [simp,TC]: "[| i \<in> nat; l \<in> list(A) |] ==> drop(i,l) \<in> list(A)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   212
apply (induct_tac "i")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   213
apply (simp_all (no_asm_simp) add: tl_type)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   214
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   215
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   216
declare drop_succ [simp del]
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   217
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   218
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   219
(** Type checking -- proved by induction, as usual **)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   220
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   221
lemma list_rec_type [TC]:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   222
    "[| l \<in> list(A);
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   223
        c \<in> C(Nil);
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   224
        !!x y r. [| x \<in> A;  y \<in> list(A);  r \<in> C(y) |] ==> h(x,y,r): C(Cons(x,y))
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   225
     |] ==> list_rec(c,h,l) \<in> C(l)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   226
by (induct_tac "l", auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   227
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   228
(** map **)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   229
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   230
lemma map_type [TC]:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   231
    "[| l \<in> list(A);  !!x. x \<in> A ==> h(x): B |] ==> map(h,l) \<in> list(B)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   232
apply (simp add: map_list_def)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   233
apply (typecheck add: list.intros list_rec_type, blast)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   234
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   235
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   236
lemma map_type2 [TC]: "l \<in> list(A) ==> map(h,l) \<in> list({h(u). u \<in> A})"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   237
apply (erule map_type)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   238
apply (erule RepFunI)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   239
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   240
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   241
(** length **)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   242
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   243
lemma length_type [TC]: "l \<in> list(A) ==> length(l) \<in> nat"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   244
by (simp add: length_list_def)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   245
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   246
lemma lt_length_in_nat:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   247
   "[|x < length(xs); xs \<in> list(A)|] ==> x \<in> nat"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   248
by (frule lt_nat_in_nat, typecheck)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   249
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   250
(** app **)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   251
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   252
lemma app_type [TC]: "[| xs: list(A);  ys: list(A) |] ==> xs@ys \<in> list(A)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   253
by (simp add: app_list_def)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   254
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   255
(** rev **)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   256
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   257
lemma rev_type [TC]: "xs: list(A) ==> rev(xs) \<in> list(A)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   258
by (simp add: rev_list_def)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   259
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   260
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   261
(** flat **)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   262
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   263
lemma flat_type [TC]: "ls: list(list(A)) ==> flat(ls) \<in> list(A)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   264
by (simp add: flat_list_def)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   265
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   266
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   267
(** set_of_list **)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   268
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   269
lemma set_of_list_type [TC]: "l \<in> list(A) ==> set_of_list(l) \<in> Pow(A)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   270
apply (unfold set_of_list_list_def)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   271
apply (erule list_rec_type, auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   272
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   273
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   274
lemma set_of_list_append:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   275
     "xs: list(A) ==> set_of_list (xs@ys) = set_of_list(xs) \<union> set_of_list(ys)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   276
apply (erule list.induct)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   277
apply (simp_all (no_asm_simp) add: Un_cons)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   278
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   279
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   280
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   281
(** list_add **)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   282
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   283
lemma list_add_type [TC]: "xs: list(nat) ==> list_add(xs) \<in> nat"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   284
by (simp add: list_add_list_def)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   285
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   286
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   287
(*** theorems about map ***)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   288
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   289
lemma map_ident [simp]: "l \<in> list(A) ==> map(%u. u, l) = l"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   290
apply (induct_tac "l")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   291
apply (simp_all (no_asm_simp))
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   292
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   293
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   294
lemma map_compose: "l \<in> list(A) ==> map(h, map(j,l)) = map(%u. h(j(u)), l)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   295
apply (induct_tac "l")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   296
apply (simp_all (no_asm_simp))
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   297
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   298
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   299
lemma map_app_distrib: "xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   300
apply (induct_tac "xs")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   301
apply (simp_all (no_asm_simp))
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   302
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   303
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   304
lemma map_flat: "ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   305
apply (induct_tac "ls")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   306
apply (simp_all (no_asm_simp) add: map_app_distrib)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   307
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   308
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   309
lemma list_rec_map:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   310
     "l \<in> list(A) ==>
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   311
      list_rec(c, d, map(h,l)) =
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   312
      list_rec(c, %x xs r. d(h(x), map(h,xs), r), l)"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   313
apply (induct_tac "l")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   314
apply (simp_all (no_asm_simp))
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   315
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   316
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   317
(** theorems about list(Collect(A,P)) -- used in Induct/Term.thy **)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   318
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   319
(* @{term"c \<in> list(Collect(B,P)) ==> c \<in> list"} *)
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 35425
diff changeset
   320
lemmas list_CollectD = Collect_subset [THEN list_mono, THEN subsetD]
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   321
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   322
lemma map_list_Collect: "l \<in> list({x \<in> A. h(x)=j(x)}) ==> map(h,l) = map(j,l)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   323
apply (induct_tac "l")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   324
apply (simp_all (no_asm_simp))
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   325
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   326
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   327
(*** theorems about length ***)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   328
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   329
lemma length_map [simp]: "xs: list(A) ==> length(map(h,xs)) = length(xs)"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   330
by (induct_tac "xs", simp_all)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   331
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   332
lemma length_app [simp]:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   333
     "[| xs: list(A); ys: list(A) |]
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   334
      ==> length(xs@ys) = length(xs) #+ length(ys)"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   335
by (induct_tac "xs", simp_all)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   336
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   337
lemma length_rev [simp]: "xs: list(A) ==> length(rev(xs)) = length(xs)"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   338
apply (induct_tac "xs")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   339
apply (simp_all (no_asm_simp) add: length_app)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   340
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   341
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   342
lemma length_flat:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   343
     "ls: list(list(A)) ==> length(flat(ls)) = list_add(map(length,ls))"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   344
apply (induct_tac "ls")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   345
apply (simp_all (no_asm_simp) add: length_app)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   346
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   347
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   348
(** Length and drop **)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   349
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   350
(*Lemma for the inductive step of drop_length*)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   351
lemma drop_length_Cons [rule_format]:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   352
     "xs: list(A) ==>
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   353
           \<forall>x.  \<exists>z zs. drop(length(xs), Cons(x,xs)) = Cons(z,zs)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   354
by (erule list.induct, simp_all)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   355
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   356
lemma drop_length [rule_format]:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   357
     "l \<in> list(A) ==> \<forall>i \<in> length(l). (\<exists>z zs. drop(i,l) = Cons(z,zs))"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   358
apply (erule list.induct, simp_all, safe)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   359
apply (erule drop_length_Cons)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   360
apply (rule natE)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   361
apply (erule Ord_trans [OF asm_rl length_type Ord_nat], assumption, simp_all)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   362
apply (blast intro: succ_in_naturalD length_type)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   363
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   364
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   365
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   366
(*** theorems about app ***)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   367
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   368
lemma app_right_Nil [simp]: "xs: list(A) ==> xs@Nil=xs"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   369
by (erule list.induct, simp_all)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   370
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   371
lemma app_assoc: "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   372
by (induct_tac "xs", simp_all)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   373
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   374
lemma flat_app_distrib: "ls: list(list(A)) ==> flat(ls@ms) = flat(ls)@flat(ms)"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   375
apply (induct_tac "ls")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   376
apply (simp_all (no_asm_simp) add: app_assoc)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   377
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   378
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   379
(*** theorems about rev ***)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   380
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   381
lemma rev_map_distrib: "l \<in> list(A) ==> rev(map(h,l)) = map(h,rev(l))"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   382
apply (induct_tac "l")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   383
apply (simp_all (no_asm_simp) add: map_app_distrib)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   384
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   385
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   386
(*Simplifier needs the premises as assumptions because rewriting will not
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   387
  instantiate the variable ?A in the rules' typing conditions; note that
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   388
  rev_type does not instantiate ?A.  Only the premises do.
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   389
*)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   390
lemma rev_app_distrib:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   391
     "[| xs: list(A);  ys: list(A) |] ==> rev(xs@ys) = rev(ys)@rev(xs)"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   392
apply (erule list.induct)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   393
apply (simp_all add: app_assoc)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   394
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   395
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   396
lemma rev_rev_ident [simp]: "l \<in> list(A) ==> rev(rev(l))=l"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   397
apply (induct_tac "l")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   398
apply (simp_all (no_asm_simp) add: rev_app_distrib)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   399
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   400
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   401
lemma rev_flat: "ls: list(list(A)) ==> rev(flat(ls)) = flat(map(rev,rev(ls)))"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   402
apply (induct_tac "ls")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   403
apply (simp_all add: map_app_distrib flat_app_distrib rev_app_distrib)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   404
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   405
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   406
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   407
(*** theorems about list_add ***)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   408
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   409
lemma list_add_app:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   410
     "[| xs: list(nat);  ys: list(nat) |]
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   411
      ==> list_add(xs@ys) = list_add(ys) #+ list_add(xs)"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   412
apply (induct_tac "xs", simp_all)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   413
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   414
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   415
lemma list_add_rev: "l \<in> list(nat) ==> list_add(rev(l)) = list_add(l)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   416
apply (induct_tac "l")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   417
apply (simp_all (no_asm_simp) add: list_add_app)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   418
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   419
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   420
lemma list_add_flat:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   421
     "ls: list(list(nat)) ==> list_add(flat(ls)) = list_add(map(list_add,ls))"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   422
apply (induct_tac "ls")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   423
apply (simp_all (no_asm_simp) add: list_add_app)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   424
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   425
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   426
(** New induction rules **)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   427
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   428
lemma list_append_induct [case_names Nil snoc, consumes 1]:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   429
    "[| l \<in> list(A);
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   430
        P(Nil);
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   431
        !!x y. [| x \<in> A;  y \<in> list(A);  P(y) |] ==> P(y @ [x])
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   432
     |] ==> P(l)"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   433
apply (subgoal_tac "P(rev(rev(l)))", simp)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   434
apply (erule rev_type [THEN list.induct], simp_all)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   435
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   436
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   437
lemma list_complete_induct_lemma [rule_format]:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   438
 assumes ih:
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   439
    "\<And>l. [| l \<in> list(A);
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   440
             \<forall>l' \<in> list(A). length(l') < length(l) \<longrightarrow> P(l')|]
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   441
          ==> P(l)"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   442
  shows "n \<in> nat ==> \<forall>l \<in> list(A). length(l) < n \<longrightarrow> P(l)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   443
apply (induct_tac n, simp)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   444
apply (blast intro: ih elim!: leE)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   445
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   446
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   447
theorem list_complete_induct:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   448
      "[| l \<in> list(A);
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   449
          \<And>l. [| l \<in> list(A);
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   450
                  \<forall>l' \<in> list(A). length(l') < length(l) \<longrightarrow> P(l')|]
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   451
               ==> P(l)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   452
       |] ==> P(l)"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   453
apply (rule list_complete_induct_lemma [of A])
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   454
   prefer 4 apply (rule le_refl, simp)
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   455
  apply blast
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   456
 apply simp
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   457
apply assumption
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   458
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   459
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   460
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   461
(*** Thanks to Sidi Ehmety for these results about min, take, etc. ***)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   462
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   463
(** min FIXME: replace by Int! **)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   464
(* Min theorems are also true for i, j ordinals *)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   465
lemma min_sym: "[| i \<in> nat; j \<in> nat |] ==> min(i,j)=min(j,i)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   466
apply (unfold min_def)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   467
apply (auto dest!: not_lt_imp_le dest: lt_not_sym intro: le_anti_sym)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   468
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   469
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   470
lemma min_type [simp,TC]: "[| i \<in> nat; j \<in> nat |] ==> min(i,j):nat"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   471
by (unfold min_def, auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   472
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   473
lemma min_0 [simp]: "i \<in> nat ==> min(0,i) = 0"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   474
apply (unfold min_def)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   475
apply (auto dest: not_lt_imp_le)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   476
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   477
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   478
lemma min_02 [simp]: "i \<in> nat ==> min(i, 0) = 0"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   479
apply (unfold min_def)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   480
apply (auto dest: not_lt_imp_le)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   481
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   482
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   483
lemma lt_min_iff: "[| i \<in> nat; j \<in> nat; k \<in> nat |] ==> i<min(j,k) \<longleftrightarrow> i<j & i<k"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   484
apply (unfold min_def)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   485
apply (auto dest!: not_lt_imp_le intro: lt_trans2 lt_trans)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   486
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   487
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   488
lemma min_succ_succ [simp]:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   489
     "[| i \<in> nat; j \<in> nat |] ==>  min(succ(i), succ(j))= succ(min(i, j))"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   490
apply (unfold min_def, auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   491
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   492
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   493
(*** more theorems about lists ***)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   494
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   495
(** filter **)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   496
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   497
lemma filter_append [simp]:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   498
     "xs:list(A) ==> filter(P, xs@ys) = filter(P, xs) @ filter(P, ys)"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   499
by (induct_tac "xs", auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   500
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   501
lemma filter_type [simp,TC]: "xs:list(A) ==> filter(P, xs):list(A)"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   502
by (induct_tac "xs", auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   503
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   504
lemma length_filter: "xs:list(A) ==> length(filter(P, xs)) \<le> length(xs)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   505
apply (induct_tac "xs", auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   506
apply (rule_tac j = "length (l) " in le_trans)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   507
apply (auto simp add: le_iff)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   508
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   509
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   510
lemma filter_is_subset: "xs:list(A) ==> set_of_list(filter(P,xs)) \<subseteq> set_of_list(xs)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   511
by (induct_tac "xs", auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   512
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   513
lemma filter_False [simp]: "xs:list(A) ==> filter(%p. False, xs) = Nil"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   514
by (induct_tac "xs", auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   515
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   516
lemma filter_True [simp]: "xs:list(A) ==> filter(%p. True, xs) = xs"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   517
by (induct_tac "xs", auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   518
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   519
(** length **)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   520
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   521
lemma length_is_0_iff [simp]: "xs:list(A) ==> length(xs)=0 \<longleftrightarrow> xs=Nil"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   522
by (erule list.induct, auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   523
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   524
lemma length_is_0_iff2 [simp]: "xs:list(A) ==> 0 = length(xs) \<longleftrightarrow> xs=Nil"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   525
by (erule list.induct, auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   526
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   527
lemma length_tl [simp]: "xs:list(A) ==> length(tl(xs)) = length(xs) #- 1"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   528
by (erule list.induct, auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   529
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   530
lemma length_greater_0_iff: "xs:list(A) ==> 0<length(xs) \<longleftrightarrow> xs \<noteq> Nil"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   531
by (erule list.induct, auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   532
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   533
lemma length_succ_iff: "xs:list(A) ==> length(xs)=succ(n) \<longleftrightarrow> (\<exists>y ys. xs=Cons(y, ys) & length(ys)=n)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   534
by (erule list.induct, auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   535
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   536
(** more theorems about append **)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   537
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   538
lemma append_is_Nil_iff [simp]:
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   539
     "xs:list(A) ==> (xs@ys = Nil) \<longleftrightarrow> (xs=Nil & ys = Nil)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   540
by (erule list.induct, auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   541
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   542
lemma append_is_Nil_iff2 [simp]:
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   543
     "xs:list(A) ==> (Nil = xs@ys) \<longleftrightarrow> (xs=Nil & ys = Nil)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   544
by (erule list.induct, auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   545
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   546
lemma append_left_is_self_iff [simp]:
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   547
     "xs:list(A) ==> (xs@ys = xs) \<longleftrightarrow> (ys = Nil)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   548
by (erule list.induct, auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   549
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   550
lemma append_left_is_self_iff2 [simp]:
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   551
     "xs:list(A) ==> (xs = xs@ys) \<longleftrightarrow> (ys = Nil)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   552
by (erule list.induct, auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   553
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   554
(*TOO SLOW as a default simprule!*)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   555
lemma append_left_is_Nil_iff [rule_format]:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   556
     "[| xs:list(A); ys:list(A); zs:list(A) |] ==>
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   557
   length(ys)=length(zs) \<longrightarrow> (xs@ys=zs \<longleftrightarrow> (xs=Nil & ys=zs))"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   558
apply (erule list.induct)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   559
apply (auto simp add: length_app)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   560
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   561
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   562
(*TOO SLOW as a default simprule!*)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   563
lemma append_left_is_Nil_iff2 [rule_format]:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   564
     "[| xs:list(A); ys:list(A); zs:list(A) |] ==>
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   565
   length(ys)=length(zs) \<longrightarrow> (zs=ys@xs \<longleftrightarrow> (xs=Nil & ys=zs))"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   566
apply (erule list.induct)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   567
apply (auto simp add: length_app)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   568
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   569
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   570
lemma append_eq_append_iff [rule_format,simp]:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   571
     "xs:list(A) ==> \<forall>ys \<in> list(A).
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   572
      length(xs)=length(ys) \<longrightarrow> (xs@us = ys@vs) \<longleftrightarrow> (xs=ys & us=vs)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   573
apply (erule list.induct)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   574
apply (simp (no_asm_simp))
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   575
apply clarify
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   576
apply (erule_tac a = ys in list.cases, auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   577
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   578
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   579
lemma append_eq_append [rule_format]:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   580
  "xs:list(A) ==>
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   581
   \<forall>ys \<in> list(A). \<forall>us \<in> list(A). \<forall>vs \<in> list(A).
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   582
   length(us) = length(vs) \<longrightarrow> (xs@us = ys@vs) \<longrightarrow> (xs=ys & us=vs)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   583
apply (induct_tac "xs")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   584
apply (force simp add: length_app, clarify)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   585
apply (erule_tac a = ys in list.cases, simp)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   586
apply (subgoal_tac "Cons (a, l) @ us =vs")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   587
 apply (drule rev_iffD1 [OF _ append_left_is_Nil_iff], simp_all, blast)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   588
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   589
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   590
lemma append_eq_append_iff2 [simp]:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   591
 "[| xs:list(A); ys:list(A); us:list(A); vs:list(A); length(us)=length(vs) |]
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   592
  ==>  xs@us = ys@vs \<longleftrightarrow> (xs=ys & us=vs)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   593
apply (rule iffI)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   594
apply (rule append_eq_append, auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   595
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   596
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   597
lemma append_self_iff [simp]:
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   598
     "[| xs:list(A); ys:list(A); zs:list(A) |] ==> xs@ys=xs@zs \<longleftrightarrow> ys=zs"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   599
by simp
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   600
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   601
lemma append_self_iff2 [simp]:
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   602
     "[| xs:list(A); ys:list(A); zs:list(A) |] ==> ys@xs=zs@xs \<longleftrightarrow> ys=zs"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   603
by simp
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   604
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   605
(* Can also be proved from append_eq_append_iff2,
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   606
but the proof requires two more hypotheses: x \<in> A and y \<in> A *)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   607
lemma append1_eq_iff [rule_format,simp]:
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   608
     "xs:list(A) ==> \<forall>ys \<in> list(A). xs@[x] = ys@[y] \<longleftrightarrow> (xs = ys & x=y)"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   609
apply (erule list.induct)
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   610
 apply clarify
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   611
 apply (erule list.cases)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   612
 apply simp_all
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   613
txt{*Inductive step*}
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   614
apply clarify
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   615
apply (erule_tac a=ys in list.cases, simp_all)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   616
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   617
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   618
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   619
lemma append_right_is_self_iff [simp]:
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   620
     "[| xs:list(A); ys:list(A) |] ==> (xs@ys = ys) \<longleftrightarrow> (xs=Nil)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   621
by (simp (no_asm_simp) add: append_left_is_Nil_iff)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   622
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   623
lemma append_right_is_self_iff2 [simp]:
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   624
     "[| xs:list(A); ys:list(A) |] ==> (ys = xs@ys) \<longleftrightarrow> (xs=Nil)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   625
apply (rule iffI)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   626
apply (drule sym, auto)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   627
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   628
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   629
lemma hd_append [rule_format,simp]:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   630
     "xs:list(A) ==> xs \<noteq> Nil \<longrightarrow> hd(xs @ ys) = hd(xs)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   631
by (induct_tac "xs", auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   632
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   633
lemma tl_append [rule_format,simp]:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   634
     "xs:list(A) ==> xs\<noteq>Nil \<longrightarrow> tl(xs @ ys) = tl(xs)@ys"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   635
by (induct_tac "xs", auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   636
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   637
(** rev **)
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   638
lemma rev_is_Nil_iff [simp]: "xs:list(A) ==> (rev(xs) = Nil \<longleftrightarrow> xs = Nil)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   639
by (erule list.induct, auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   640
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   641
lemma Nil_is_rev_iff [simp]: "xs:list(A) ==> (Nil = rev(xs) \<longleftrightarrow> xs = Nil)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   642
by (erule list.induct, auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   643
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   644
lemma rev_is_rev_iff [rule_format,simp]:
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   645
     "xs:list(A) ==> \<forall>ys \<in> list(A). rev(xs)=rev(ys) \<longleftrightarrow> xs=ys"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   646
apply (erule list.induct, force, clarify)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   647
apply (erule_tac a = ys in list.cases, auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   648
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   649
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   650
lemma rev_list_elim [rule_format]:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   651
     "xs:list(A) ==>
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   652
      (xs=Nil \<longrightarrow> P) \<longrightarrow> (\<forall>ys \<in> list(A). \<forall>y \<in> A. xs =ys@[y] \<longrightarrow>P)\<longrightarrow>P"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   653
by (erule list_append_induct, auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   654
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   655
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   656
(** more theorems about drop **)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   657
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   658
lemma length_drop [rule_format,simp]:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   659
     "n \<in> nat ==> \<forall>xs \<in> list(A). length(drop(n, xs)) = length(xs) #- n"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   660
apply (erule nat_induct)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   661
apply (auto elim: list.cases)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   662
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   663
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   664
lemma drop_all [rule_format,simp]:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   665
     "n \<in> nat ==> \<forall>xs \<in> list(A). length(xs) \<le> n \<longrightarrow> drop(n, xs)=Nil"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   666
apply (erule nat_induct)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   667
apply (auto elim: list.cases)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   668
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   669
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   670
lemma drop_append [rule_format]:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   671
     "n \<in> nat ==>
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   672
      \<forall>xs \<in> list(A). drop(n, xs@ys) = drop(n,xs) @ drop(n #- length(xs), ys)"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   673
apply (induct_tac "n")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   674
apply (auto elim: list.cases)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   675
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   676
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   677
lemma drop_drop:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   678
    "m \<in> nat ==> \<forall>xs \<in> list(A). \<forall>n \<in> nat. drop(n, drop(m, xs))=drop(n #+ m, xs)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   679
apply (induct_tac "m")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   680
apply (auto elim: list.cases)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   681
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   682
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   683
(** take **)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   684
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   685
lemma take_0 [simp]: "xs:list(A) ==> take(0, xs) =  Nil"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   686
apply (unfold take_def)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   687
apply (erule list.induct, auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   688
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   689
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   690
lemma take_succ_Cons [simp]:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   691
    "n \<in> nat ==> take(succ(n), Cons(a, xs)) = Cons(a, take(n, xs))"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   692
by (simp add: take_def)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   693
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   694
(* Needed for proving take_all *)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   695
lemma take_Nil [simp]: "n \<in> nat ==> take(n, Nil) = Nil"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   696
by (unfold take_def, auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   697
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   698
lemma take_all [rule_format,simp]:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   699
     "n \<in> nat ==> \<forall>xs \<in> list(A). length(xs) \<le> n  \<longrightarrow> take(n, xs) = xs"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   700
apply (erule nat_induct)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   701
apply (auto elim: list.cases)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   702
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   703
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   704
lemma take_type [rule_format,simp,TC]:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   705
     "xs:list(A) ==> \<forall>n \<in> nat. take(n, xs):list(A)"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   706
apply (erule list.induct, simp, clarify)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   707
apply (erule natE, auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   708
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   709
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   710
lemma take_append [rule_format,simp]:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   711
 "xs:list(A) ==>
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   712
  \<forall>ys \<in> list(A). \<forall>n \<in> nat. take(n, xs @ ys) =
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   713
                            take(n, xs) @ take(n #- length(xs), ys)"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   714
apply (erule list.induct, simp, clarify)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   715
apply (erule natE, auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   716
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   717
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   718
lemma take_take [rule_format]:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   719
   "m \<in> nat ==>
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   720
    \<forall>xs \<in> list(A). \<forall>n \<in> nat. take(n, take(m,xs))= take(min(n, m), xs)"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   721
apply (induct_tac "m", auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   722
apply (erule_tac a = xs in list.cases)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   723
apply (auto simp add: take_Nil)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   724
apply (erule_tac n=n in natE)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   725
apply (auto intro: take_0 take_type)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   726
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   727
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   728
(** nth **)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   729
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   730
lemma nth_0 [simp]: "nth(0, Cons(a, l)) = a"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   731
by (simp add: nth_def)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   732
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   733
lemma nth_Cons [simp]: "n \<in> nat ==> nth(succ(n), Cons(a,l)) = nth(n,l)"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   734
by (simp add: nth_def)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   735
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   736
lemma nth_empty [simp]: "nth(n, Nil) = 0"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   737
by (simp add: nth_def)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   738
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   739
lemma nth_type [rule_format,simp,TC]:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   740
     "xs:list(A) ==> \<forall>n. n < length(xs) \<longrightarrow> nth(n,xs) \<in> A"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   741
apply (erule list.induct, simp, clarify)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   742
apply (subgoal_tac "n \<in> nat")
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   743
 apply (erule natE, auto dest!: le_in_nat)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   744
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   745
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   746
lemma nth_eq_0 [rule_format]:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   747
     "xs:list(A) ==> \<forall>n \<in> nat. length(xs) \<le> n \<longrightarrow> nth(n,xs) = 0"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   748
apply (erule list.induct, simp, clarify)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   749
apply (erule natE, auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   750
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   751
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   752
lemma nth_append [rule_format]:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   753
  "xs:list(A) ==>
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   754
   \<forall>n \<in> nat. nth(n, xs @ ys) = (if n < length(xs) then nth(n,xs)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   755
                                else nth(n #- length(xs), ys))"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   756
apply (induct_tac "xs", simp, clarify)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   757
apply (erule natE, auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   758
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   759
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   760
lemma set_of_list_conv_nth:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   761
    "xs:list(A)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   762
     ==> set_of_list(xs) = {x \<in> A. \<exists>i\<in>nat. i<length(xs) & x = nth(i,xs)}"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   763
apply (induct_tac "xs", simp_all)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   764
apply (rule equalityI, auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   765
apply (rule_tac x = 0 in bexI, auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   766
apply (erule natE, auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   767
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   768
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   769
(* Other theorems about lists *)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   770
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   771
lemma nth_take_lemma [rule_format]:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   772
 "k \<in> nat ==>
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   773
  \<forall>xs \<in> list(A). (\<forall>ys \<in> list(A). k \<le> length(xs) \<longrightarrow> k \<le> length(ys) \<longrightarrow>
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   774
      (\<forall>i \<in> nat. i<k \<longrightarrow> nth(i,xs) = nth(i,ys))\<longrightarrow> take(k,xs) = take(k,ys))"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   775
apply (induct_tac "k")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   776
apply (simp_all (no_asm_simp) add: lt_succ_eq_0_disj all_conj_distrib)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   777
apply clarify
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   778
(*Both lists are non-empty*)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   779
apply (erule_tac a=xs in list.cases, simp)
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   780
apply (erule_tac a=ys in list.cases, clarify)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   781
apply (simp (no_asm_use) )
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   782
apply clarify
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   783
apply (simp (no_asm_simp))
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   784
apply (rule conjI, force)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   785
apply (rename_tac y ys z zs)
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   786
apply (drule_tac x = zs and x1 = ys in bspec [THEN bspec], auto)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   787
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   788
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   789
lemma nth_equalityI [rule_format]:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   790
     "[| xs:list(A); ys:list(A); length(xs) = length(ys);
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   791
         \<forall>i \<in> nat. i < length(xs) \<longrightarrow> nth(i,xs) = nth(i,ys) |]
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   792
      ==> xs = ys"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   793
apply (subgoal_tac "length (xs) \<le> length (ys) ")
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   794
apply (cut_tac k="length(xs)" and xs=xs and ys=ys in nth_take_lemma)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   795
apply (simp_all add: take_all)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   796
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   797
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   798
(*The famous take-lemma*)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   799
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   800
lemma take_equalityI [rule_format]:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   801
    "[| xs:list(A); ys:list(A); (\<forall>i \<in> nat. take(i, xs) = take(i,ys)) |]
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   802
     ==> xs = ys"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   803
apply (case_tac "length (xs) \<le> length (ys) ")
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   804
apply (drule_tac x = "length (ys) " in bspec)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   805
apply (drule_tac [3] not_lt_imp_le)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   806
apply (subgoal_tac [5] "length (ys) \<le> length (xs) ")
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   807
apply (rule_tac [6] j = "succ (length (ys))" in le_trans)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   808
apply (rule_tac [6] leI)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   809
apply (drule_tac [5] x = "length (xs) " in bspec)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   810
apply (simp_all add: take_all)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   811
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   812
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   813
lemma nth_drop [rule_format]:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   814
  "n \<in> nat ==> \<forall>i \<in> nat. \<forall>xs \<in> list(A). nth(i, drop(n, xs)) = nth(n #+ i, xs)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   815
apply (induct_tac "n", simp_all, clarify)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   816
apply (erule list.cases, auto)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   817
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   818
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   819
lemma take_succ [rule_format]:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   820
  "xs\<in>list(A)
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   821
   ==> \<forall>i. i < length(xs) \<longrightarrow> take(succ(i), xs) = take(i,xs) @ [nth(i, xs)]"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   822
apply (induct_tac "xs", auto)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   823
apply (subgoal_tac "i\<in>nat")
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   824
apply (erule natE)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   825
apply (auto simp add: le_in_nat)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   826
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   827
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   828
lemma take_add [rule_format]:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   829
     "[|xs\<in>list(A); j\<in>nat|]
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   830
      ==> \<forall>i\<in>nat. take(i #+ j, xs) = take(i,xs) @ take(j, drop(i,xs))"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   831
apply (induct_tac "xs", simp_all, clarify)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   832
apply (erule_tac n = i in natE, simp_all)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   833
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   834
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   835
lemma length_take:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   836
     "l\<in>list(A) ==> \<forall>n\<in>nat. length(take(n,l)) = min(n, length(l))"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   837
apply (induct_tac "l", safe, simp_all)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   838
apply (erule natE, simp_all)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   839
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   840
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   841
subsection{*The function zip*}
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   842
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   843
text{*Crafty definition to eliminate a type argument*}
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   844
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   845
consts
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   846
  zip_aux        :: "[i,i]=>i"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   847
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   848
primrec (*explicit lambda is required because both arguments of "un" vary*)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   849
  "zip_aux(B,[]) =
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   850
     (\<lambda>ys \<in> list(B). list_case([], %y l. [], ys))"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   851
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   852
  "zip_aux(B,Cons(x,l)) =
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   853
     (\<lambda>ys \<in> list(B).
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   854
        list_case(Nil, %y zs. Cons(<x,y>, zip_aux(B,l)`zs), ys))"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   855
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   856
definition
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   857
  zip :: "[i, i]=>i"  where
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   858
   "zip(xs, ys) == zip_aux(set_of_list(ys),xs)`ys"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   859
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   860
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   861
(* zip equations *)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   862
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   863
lemma list_on_set_of_list: "xs \<in> list(A) ==> xs \<in> list(set_of_list(xs))"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   864
apply (induct_tac xs, simp_all)
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   865
apply (blast intro: list_mono [THEN subsetD])
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   866
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   867
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   868
lemma zip_Nil [simp]: "ys:list(A) ==> zip(Nil, ys)=Nil"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   869
apply (simp add: zip_def list_on_set_of_list [of _ A])
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   870
apply (erule list.cases, simp_all)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   871
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   872
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   873
lemma zip_Nil2 [simp]: "xs:list(A) ==> zip(xs, Nil)=Nil"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   874
apply (simp add: zip_def list_on_set_of_list [of _ A])
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   875
apply (erule list.cases, simp_all)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   876
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   877
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   878
lemma zip_aux_unique [rule_format]:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   879
     "[|B<=C;  xs \<in> list(A)|]
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   880
      ==> \<forall>ys \<in> list(B). zip_aux(C,xs) ` ys = zip_aux(B,xs) ` ys"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   881
apply (induct_tac xs)
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   882
 apply simp_all
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   883
 apply (blast intro: list_mono [THEN subsetD], clarify)
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   884
apply (erule_tac a=ys in list.cases, auto)
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   885
apply (blast intro: list_mono [THEN subsetD])
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   886
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   887
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   888
lemma zip_Cons_Cons [simp]:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   889
     "[| xs:list(A); ys:list(B); x \<in> A; y \<in> B |] ==>
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   890
      zip(Cons(x,xs), Cons(y, ys)) = Cons(<x,y>, zip(xs, ys))"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   891
apply (simp add: zip_def, auto)
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   892
apply (rule zip_aux_unique, auto)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   893
apply (simp add: list_on_set_of_list [of _ B])
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   894
apply (blast intro: list_on_set_of_list list_mono [THEN subsetD])
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   895
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   896
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   897
lemma zip_type [rule_format,simp,TC]:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   898
     "xs:list(A) ==> \<forall>ys \<in> list(B). zip(xs, ys):list(A*B)"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   899
apply (induct_tac "xs")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   900
apply (simp (no_asm))
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   901
apply clarify
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   902
apply (erule_tac a = ys in list.cases, auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   903
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   904
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   905
(* zip length *)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   906
lemma length_zip [rule_format,simp]:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   907
     "xs:list(A) ==> \<forall>ys \<in> list(B). length(zip(xs,ys)) =
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   908
                                     min(length(xs), length(ys))"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   909
apply (unfold min_def)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   910
apply (induct_tac "xs", simp_all, clarify)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   911
apply (erule_tac a = ys in list.cases, auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   912
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   913
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   914
lemma zip_append1 [rule_format]:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   915
 "[| ys:list(A); zs:list(B) |] ==>
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   916
  \<forall>xs \<in> list(A). zip(xs @ ys, zs) =
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   917
                 zip(xs, take(length(xs), zs)) @ zip(ys, drop(length(xs),zs))"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   918
apply (induct_tac "zs", force, clarify)
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   919
apply (erule_tac a = xs in list.cases, simp_all)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   920
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   921
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   922
lemma zip_append2 [rule_format]:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   923
 "[| xs:list(A); zs:list(B) |] ==> \<forall>ys \<in> list(B). zip(xs, ys@zs) =
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   924
       zip(take(length(ys), xs), ys) @ zip(drop(length(ys), xs), zs)"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   925
apply (induct_tac "xs", force, clarify)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   926
apply (erule_tac a = ys in list.cases, auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   927
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   928
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   929
lemma zip_append [simp]:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   930
 "[| length(xs) = length(us); length(ys) = length(vs);
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   931
     xs:list(A); us:list(B); ys:list(A); vs:list(B) |]
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   932
  ==> zip(xs@ys,us@vs) = zip(xs, us) @ zip(ys, vs)"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   933
by (simp (no_asm_simp) add: zip_append1 drop_append diff_self_eq_0)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   934
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   935
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   936
lemma zip_rev [rule_format,simp]:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   937
 "ys:list(B) ==> \<forall>xs \<in> list(A).
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   938
    length(xs) = length(ys) \<longrightarrow> zip(rev(xs), rev(ys)) = rev(zip(xs, ys))"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   939
apply (induct_tac "ys", force, clarify)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   940
apply (erule_tac a = xs in list.cases)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   941
apply (auto simp add: length_rev)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   942
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   943
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   944
lemma nth_zip [rule_format,simp]:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   945
   "ys:list(B) ==> \<forall>i \<in> nat. \<forall>xs \<in> list(A).
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   946
                    i < length(xs) \<longrightarrow> i < length(ys) \<longrightarrow>
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   947
                    nth(i,zip(xs, ys)) = <nth(i,xs),nth(i, ys)>"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   948
apply (induct_tac "ys", force, clarify)
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   949
apply (erule_tac a = xs in list.cases, simp)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   950
apply (auto elim: natE)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   951
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   952
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   953
lemma set_of_list_zip [rule_format]:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   954
     "[| xs:list(A); ys:list(B); i \<in> nat |]
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   955
      ==> set_of_list(zip(xs, ys)) =
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   956
          {<x, y>:A*B. \<exists>i\<in>nat. i < min(length(xs), length(ys))
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   957
          & x = nth(i, xs) & y = nth(i, ys)}"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   958
by (force intro!: Collect_cong simp add: lt_min_iff set_of_list_conv_nth)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   959
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   960
(** list_update **)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   961
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   962
lemma list_update_Nil [simp]: "i \<in> nat ==>list_update(Nil, i, v) = Nil"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   963
by (unfold list_update_def, auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   964
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   965
lemma list_update_Cons_0 [simp]: "list_update(Cons(x, xs), 0, v)= Cons(v, xs)"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   966
by (unfold list_update_def, auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   967
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   968
lemma list_update_Cons_succ [simp]:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   969
  "n \<in> nat ==>
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   970
    list_update(Cons(x, xs), succ(n), v)= Cons(x, list_update(xs, n, v))"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   971
apply (unfold list_update_def, auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   972
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   973
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   974
lemma list_update_type [rule_format,simp,TC]:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   975
     "[| xs:list(A); v \<in> A |] ==> \<forall>n \<in> nat. list_update(xs, n, v):list(A)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   976
apply (induct_tac "xs")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   977
apply (simp (no_asm))
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   978
apply clarify
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   979
apply (erule natE, auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   980
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   981
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   982
lemma length_list_update [rule_format,simp]:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   983
     "xs:list(A) ==> \<forall>i \<in> nat. length(list_update(xs, i, v))=length(xs)"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   984
apply (induct_tac "xs")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   985
apply (simp (no_asm))
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   986
apply clarify
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   987
apply (erule natE, auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   988
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   989
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   990
lemma nth_list_update [rule_format]:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   991
     "[| xs:list(A) |] ==> \<forall>i \<in> nat. \<forall>j \<in> nat. i < length(xs)  \<longrightarrow>
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   992
         nth(j, list_update(xs, i, x)) = (if i=j then x else nth(j, xs))"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   993
apply (induct_tac "xs")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   994
 apply simp_all
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   995
apply clarify
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   996
apply (rename_tac i j)
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   997
apply (erule_tac n=i in natE)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   998
apply (erule_tac [2] n=j in natE)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   999
apply (erule_tac n=j in natE, simp_all, force)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1000
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1001
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1002
lemma nth_list_update_eq [simp]:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1003
     "[| i < length(xs); xs:list(A) |] ==> nth(i, list_update(xs, i,x)) = x"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1004
by (simp (no_asm_simp) add: lt_length_in_nat nth_list_update)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1005
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1006
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1007
lemma nth_list_update_neq [rule_format,simp]:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1008
  "xs:list(A) ==>
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1009
     \<forall>i \<in> nat. \<forall>j \<in> nat. i \<noteq> j \<longrightarrow> nth(j, list_update(xs,i,x)) = nth(j,xs)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1010
apply (induct_tac "xs")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1011
 apply (simp (no_asm))
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1012
apply clarify
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1013
apply (erule natE)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1014
apply (erule_tac [2] natE, simp_all)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1015
apply (erule natE, simp_all)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1016
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1017
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1018
lemma list_update_overwrite [rule_format,simp]:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1019
     "xs:list(A) ==> \<forall>i \<in> nat. i < length(xs)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1020
   \<longrightarrow> list_update(list_update(xs, i, x), i, y) = list_update(xs, i,y)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1021
apply (induct_tac "xs")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1022
 apply (simp (no_asm))
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1023
apply clarify
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1024
apply (erule natE, auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1025
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1026
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1027
lemma list_update_same_conv [rule_format]:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1028
     "xs:list(A) ==>
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1029
      \<forall>i \<in> nat. i < length(xs) \<longrightarrow>
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
  1030
                 (list_update(xs, i, x) = xs) \<longleftrightarrow> (nth(i, xs) = x)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1031
apply (induct_tac "xs")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1032
 apply (simp (no_asm))
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1033
apply clarify
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1034
apply (erule natE, auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1035
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1036
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1037
lemma update_zip [rule_format]:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1038
     "ys:list(B) ==>
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1039
      \<forall>i \<in> nat. \<forall>xy \<in> A*B. \<forall>xs \<in> list(A).
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1040
        length(xs) = length(ys) \<longrightarrow>
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1041
        list_update(zip(xs, ys), i, xy) = zip(list_update(xs, i, fst(xy)),
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1042
                                              list_update(ys, i, snd(xy)))"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1043
apply (induct_tac "ys")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1044
 apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1045
apply (erule_tac a = xs in list.cases)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1046
apply (auto elim: natE)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1047
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1048
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1049
lemma set_update_subset_cons [rule_format]:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1050
  "xs:list(A) ==>
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1051
   \<forall>i \<in> nat. set_of_list(list_update(xs, i, x)) \<subseteq> cons(x, set_of_list(xs))"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1052
apply (induct_tac "xs")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1053
 apply simp
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1054
apply (rule ballI)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1055
apply (erule natE, simp_all, auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1056
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1057
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1058
lemma set_of_list_update_subsetI:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
  1059
     "[| set_of_list(xs) \<subseteq> A; xs:list(A); x \<in> A; i \<in> nat|]
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1060
   ==> set_of_list(list_update(xs, i,x)) \<subseteq> A"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1061
apply (rule subset_trans)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1062
apply (rule set_update_subset_cons, auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1063
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1064
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1065
(** upt **)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1066
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1067
lemma upt_rec:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
  1068
     "j \<in> nat ==> upt(i,j) = (if i<j then Cons(i, upt(succ(i), j)) else Nil)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1069
apply (induct_tac "j", auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1070
apply (drule not_lt_imp_le)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1071
apply (auto simp: lt_Ord intro: le_anti_sym)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1072
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1073
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
  1074
lemma upt_conv_Nil [simp]: "[| j \<le> i; j \<in> nat |] ==> upt(i,j) = Nil"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1075
apply (subst upt_rec, auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1076
apply (auto simp add: le_iff)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1077
apply (drule lt_asym [THEN notE], auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1078
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1079
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1080
(*Only needed if upt_Suc is deleted from the simpset*)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1081
lemma upt_succ_append:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
  1082
     "[| i \<le> j; j \<in> nat |] ==> upt(i,succ(j)) = upt(i, j)@[j]"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1083
by simp
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1084
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1085
lemma upt_conv_Cons:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
  1086
     "[| i<j; j \<in> nat |]  ==> upt(i,j) = Cons(i,upt(succ(i),j))"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1087
apply (rule trans)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1088
apply (rule upt_rec, auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1089
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1090
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
  1091
lemma upt_type [simp,TC]: "j \<in> nat ==> upt(i,j):list(nat)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1092
by (induct_tac "j", auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1093
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1094
(*LOOPS as a simprule, since j<=j*)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1095
lemma upt_add_eq_append:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
  1096
     "[| i \<le> j; j \<in> nat; k \<in> nat |] ==> upt(i, j #+k) = upt(i,j)@upt(j,j#+k)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1097
apply (induct_tac "k")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1098
apply (auto simp add: app_assoc app_type)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1099
apply (rule_tac j = j in le_trans, auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1100
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1101
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
  1102
lemma length_upt [simp]: "[| i \<in> nat; j \<in> nat |] ==>length(upt(i,j)) = j #- i"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1103
apply (induct_tac "j")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1104
apply (rule_tac [2] sym)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1105
apply (auto dest!: not_lt_imp_le simp add: diff_succ diff_is_0_iff)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1106
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1107
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1108
lemma nth_upt [rule_format,simp]:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
  1109
     "[| i \<in> nat; j \<in> nat; k \<in> nat |] ==> i #+ k < j \<longrightarrow> nth(k, upt(i,j)) = i #+ k"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1110
apply (induct_tac "j", simp)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1111
apply (simp add: nth_append le_iff)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1112
apply (auto dest!: not_lt_imp_le
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1113
            simp add: nth_append less_diff_conv add_commute)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1114
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1115
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1116
lemma take_upt [rule_format,simp]:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
  1117
     "[| m \<in> nat; n \<in> nat |] ==>
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1118
         \<forall>i \<in> nat. i #+ m \<le> n \<longrightarrow> take(m, upt(i,n)) = upt(i,i#+m)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1119
apply (induct_tac "m")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1120
apply (simp (no_asm_simp) add: take_0)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1121
apply clarify
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1122
apply (subst upt_rec, simp)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1123
apply (rule sym)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1124
apply (subst upt_rec, simp)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1125
apply (simp_all del: upt.simps)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1126
apply (rule_tac j = "succ (i #+ x) " in lt_trans2)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1127
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1128
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1129
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1130
lemma map_succ_upt:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
  1131
     "[| m \<in> nat; n \<in> nat |] ==> map(succ, upt(m,n))= upt(succ(m), succ(n))"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1132
apply (induct_tac "n")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1133
apply (auto simp add: map_app_distrib)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1134
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1135
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1136
lemma nth_map [rule_format,simp]:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1137
     "xs:list(A) ==>
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1138
      \<forall>n \<in> nat. n < length(xs) \<longrightarrow> nth(n, map(f, xs)) = f(nth(n, xs))"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1139
apply (induct_tac "xs", simp)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1140
apply (rule ballI)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1141
apply (induct_tac "n", auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1142
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1143
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1144
lemma nth_map_upt [rule_format]:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
  1145
     "[| m \<in> nat; n \<in> nat |] ==>
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1146
      \<forall>i \<in> nat. i < n #- m \<longrightarrow> nth(i, map(f, upt(m,n))) = f(m #+ i)"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1147
apply (rule_tac n = m and m = n in diff_induct, typecheck, simp, simp)
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1148
apply (subst map_succ_upt [symmetric], simp_all, clarify)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1149
apply (subgoal_tac "i < length (upt (0, x))")
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1150
 prefer 2
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1151
 apply (simp add: less_diff_conv)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1152
 apply (rule_tac j = "succ (i #+ y) " in lt_trans2)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1153
  apply simp
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1154
 apply simp
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1155
apply (subgoal_tac "i < length (upt (y, x))")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1156
 apply (simp_all add: add_commute less_diff_conv)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1157
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1158
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1159
(** sublist (a generalization of nth to sets) **)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1160
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1161
definition
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1162
  sublist :: "[i, i] => i"  where
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1163
    "sublist(xs, A)==
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1164
     map(fst, (filter(%p. snd(p): A, zip(xs, upt(0,length(xs))))))"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1165
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1166
lemma sublist_0 [simp]: "xs:list(A) ==>sublist(xs, 0) =Nil"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1167
by (unfold sublist_def, auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1168
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1169
lemma sublist_Nil [simp]: "sublist(Nil, A) = Nil"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1170
by (unfold sublist_def, auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1171
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1172
lemma sublist_shift_lemma:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
  1173
 "[| xs:list(B); i \<in> nat |] ==>
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1174
  map(fst, filter(%p. snd(p):A, zip(xs, upt(i,i #+ length(xs))))) =
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
  1175
  map(fst, filter(%p. snd(p):nat & snd(p) #+ i \<in> A, zip(xs,upt(0,length(xs)))))"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1176
apply (erule list_append_induct)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1177
apply (simp (no_asm_simp))
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1178
apply (auto simp add: add_commute length_app filter_append map_app_distrib)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1179
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1180
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1181
lemma sublist_type [simp,TC]:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1182
     "xs:list(B) ==> sublist(xs, A):list(B)"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1183
apply (unfold sublist_def)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1184
apply (induct_tac "xs")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1185
apply (auto simp add: filter_append map_app_distrib)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1186
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1187
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1188
lemma upt_add_eq_append2:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
  1189
     "[| i \<in> nat; j \<in> nat |] ==> upt(0, i #+ j) = upt(0, i) @ upt(i, i #+ j)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1190
by (simp add: upt_add_eq_append [of 0] nat_0_le)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1191
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1192
lemma sublist_append:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1193
 "[| xs:list(B); ys:list(B)  |] ==>
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
  1194
  sublist(xs@ys, A) = sublist(xs, A) @ sublist(ys, {j \<in> nat. j #+ length(xs): A})"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1195
apply (unfold sublist_def)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1196
apply (erule_tac l = ys in list_append_induct, simp)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1197
apply (simp (no_asm_simp) add: upt_add_eq_append2 app_assoc [symmetric])
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1198
apply (auto simp add: sublist_shift_lemma length_type map_app_distrib app_assoc)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1199
apply (simp_all add: add_commute)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1200
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1201
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1202
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1203
lemma sublist_Cons:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
  1204
     "[| xs:list(B); x \<in> B |] ==>
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1205
      sublist(Cons(x, xs), A) =
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
  1206
      (if 0 \<in> A then [x] else []) @ sublist(xs, {j \<in> nat. succ(j) \<in> A})"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1207
apply (erule_tac l = xs in list_append_induct)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1208
apply (simp (no_asm_simp) add: sublist_def)
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1209
apply (simp del: app_Cons add: app_Cons [symmetric] sublist_append, simp)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1210
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1211
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1212
lemma sublist_singleton [simp]:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1213
     "sublist([x], A) = (if 0 \<in> A then [x] else [])"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1214
by (simp add: sublist_Cons)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1215
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1216
lemma sublist_upt_eq_take [rule_format, simp]:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1217
    "xs:list(A) ==> \<forall>n\<in>nat. sublist(xs,n) = take(n,xs)"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1218
apply (erule list.induct, simp)
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1219
apply (clarify );
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1220
apply (erule natE)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1221
apply (simp_all add: nat_eq_Collect_lt Ord_mem_iff_lt sublist_Cons)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1222
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1223
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1224
lemma sublist_Int_eq:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1225
     "xs \<in> list(B) ==> sublist(xs, A \<inter> nat) = sublist(xs, A)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1226
apply (erule list.induct)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1227
apply (simp_all add: sublist_Cons)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1228
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1229
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1230
text{*Repetition of a List Element*}
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1231
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1232
consts   repeat :: "[i,i]=>i"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1233
primrec
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1234
  "repeat(a,0) = []"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1235
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1236
  "repeat(a,succ(n)) = Cons(a,repeat(a,n))"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1237
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1238
lemma length_repeat: "n \<in> nat ==> length(repeat(a,n)) = n"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1239
by (induct_tac n, auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1240
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1241
lemma repeat_succ_app: "n \<in> nat ==> repeat(a,succ(n)) = repeat(a,n) @ [a]"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1242
apply (induct_tac n)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1243
apply (simp_all del: app_Cons add: app_Cons [symmetric])
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1244
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1245
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1246
lemma repeat_type [TC]: "[|a \<in> A; n \<in> nat|] ==> repeat(a,n) \<in> list(A)"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1247
by (induct_tac n, auto)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1248
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1249
end