src/HOL/Induct/SList.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 45694 4a8743618257
child 49834 b27bbb021df1
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
35247
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
     1
(*  Title:      HOL/Induct/SList.thy
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
     3
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
     4
This theory is strictly of historical interest. It illustrates how
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
     5
recursive datatypes can be constructed in higher-order logic from
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
     6
first principles. Isabelle's datatype package automates a
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
     7
construction of this sort.
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
     8
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
     9
Enriched theory of lists; mutual indirect recursive data-types.
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    10
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    11
Definition of type 'a list (strict lists) by a least fixed point
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    12
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    13
We use          list(A) == lfp(%Z. {NUMB(0)} <+> A <*> Z)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    14
and not         list    == lfp(%Z. {NUMB(0)} <+> range(Leaf) <*> Z)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    15
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    16
so that list can serve as a "functor" for defining other recursive types.
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    17
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    18
This enables the conservative construction of mutual recursive data-types
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    19
such as
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    20
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    21
datatype 'a m = Node 'a * ('a m) list
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    22
*)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    23
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    24
header {* Extended List Theory (old) *}
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    25
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    26
theory SList
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    27
imports Sexp
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    28
begin
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    29
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    30
(*Hilbert_Choice is needed for the function "inv"*)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    31
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    32
(* *********************************************************************** *)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    33
(*                                                                         *)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    34
(* Building up data type                                                   *)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    35
(*                                                                         *)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    36
(* *********************************************************************** *)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    37
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    38
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    39
(* Defining the Concrete Constructors *)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    40
definition
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    41
  NIL  :: "'a item" where
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    42
  "NIL = In0(Numb(0))"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    43
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    44
definition
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    45
  CONS :: "['a item, 'a item] => 'a item" where
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    46
  "CONS M N = In1(Scons M N)"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    47
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    48
inductive_set
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    49
  list :: "'a item set => 'a item set"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    50
  for A :: "'a item set"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    51
  where
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    52
    NIL_I:  "NIL: list A"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    53
  | CONS_I: "[| a: A;  M: list A |] ==> CONS a M : list A"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    54
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    55
45694
4a8743618257 prefer typedef without extra definition and alternative name;
wenzelm
parents: 45605
diff changeset
    56
definition "List = list (range Leaf)"
4a8743618257 prefer typedef without extra definition and alternative name;
wenzelm
parents: 45605
diff changeset
    57
4a8743618257 prefer typedef without extra definition and alternative name;
wenzelm
parents: 45605
diff changeset
    58
typedef (open) 'a list = "List :: 'a item set"
4a8743618257 prefer typedef without extra definition and alternative name;
wenzelm
parents: 45605
diff changeset
    59
  morphisms Rep_List Abs_List
4a8743618257 prefer typedef without extra definition and alternative name;
wenzelm
parents: 45605
diff changeset
    60
  unfolding List_def by (blast intro: list.NIL_I)
35247
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    61
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    62
abbreviation "Case == Datatype.Case"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    63
abbreviation "Split == Datatype.Split"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    64
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    65
definition
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    66
  List_case :: "['b, ['a item, 'a item]=>'b, 'a item] => 'b" where
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    67
  "List_case c d = Case(%x. c)(Split(d))"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    68
  
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    69
definition
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    70
  List_rec  :: "['a item, 'b, ['a item, 'a item, 'b]=>'b] => 'b" where
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    71
  "List_rec M c d = wfrec (pred_sexp^+)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    72
                           (%g. List_case c (%x y. d x y (g y))) M"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    73
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    74
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    75
(* *********************************************************************** *)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    76
(*                                                                         *)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    77
(* Abstracting data type                                                   *)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    78
(*                                                                         *)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    79
(* *********************************************************************** *)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    80
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    81
(*Declaring the abstract list constructors*)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    82
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    83
no_translations
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    84
  "[x, xs]" == "x#[xs]"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    85
  "[x]" == "x#[]"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    86
no_notation
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    87
  Nil  ("[]") and
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    88
  Cons (infixr "#" 65)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    89
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    90
definition
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    91
  Nil       :: "'a list"                               ("[]") where
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    92
   "Nil  = Abs_List(NIL)"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    93
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    94
definition
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    95
  "Cons"       :: "['a, 'a list] => 'a list"           (infixr "#" 65) where
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    96
   "x#xs = Abs_List(CONS (Leaf x)(Rep_List xs))"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    97
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    98
definition
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
    99
  (* list Recursion -- the trancl is Essential; see list.ML *)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   100
  list_rec  :: "['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b" where
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   101
   "list_rec l c d =
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   102
      List_rec(Rep_List l) c (%x y r. d(inv Leaf x)(Abs_List y) r)"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   103
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   104
definition
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   105
  list_case :: "['b, ['a, 'a list]=>'b, 'a list] => 'b" where
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   106
   "list_case a f xs = list_rec xs a (%x xs r. f x xs)"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   107
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   108
(* list Enumeration *)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   109
translations
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   110
  "[x, xs]" == "x#[xs]"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   111
  "[x]"     == "x#[]"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   112
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   113
  "case xs of [] => a | y#ys => b" == "CONST list_case(a, %y ys. b, xs)"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   114
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   115
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   116
(* *********************************************************************** *)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   117
(*                                                                         *)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   118
(* Generalized Map Functionals                                             *)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   119
(*                                                                         *)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   120
(* *********************************************************************** *)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   121
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   122
  
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   123
(* Generalized Map Functionals *)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   124
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   125
definition
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   126
  Rep_map   :: "('b => 'a item) => ('b list => 'a item)" where
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   127
   "Rep_map f xs = list_rec xs  NIL(%x l r. CONS(f x) r)"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   128
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   129
definition
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   130
  Abs_map   :: "('a item => 'b) => 'a item => 'b list" where
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   131
   "Abs_map g M  = List_rec M Nil (%N L r. g(N)#r)"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   132
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   133
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   134
definition
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   135
  map       :: "('a=>'b) => ('a list => 'b list)" where
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   136
  "map f xs = list_rec xs [] (%x l r. f(x)#r)"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   137
39246
9e58f0499f57 modernized primrec
haftmann
parents: 35247
diff changeset
   138
primrec take :: "['a list,nat] => 'a list" where
35247
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   139
  take_0:  "take xs 0 = []"
39246
9e58f0499f57 modernized primrec
haftmann
parents: 35247
diff changeset
   140
| take_Suc: "take xs (Suc n) = list_case [] (%x l. x # take l n) xs"
35247
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   141
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   142
lemma ListI: "x : list (range Leaf) ==> x : List"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   143
by (simp add: List_def)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   144
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   145
lemma ListD: "x : List ==> x : list (range Leaf)"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   146
by (simp add: List_def)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   147
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   148
lemma list_unfold: "list(A) = usum {Numb(0)} (uprod A (list(A)))"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   149
  by (fast intro!: list.intros [unfolded NIL_def CONS_def]
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   150
           elim: list.cases [unfolded NIL_def CONS_def])
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   151
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   152
(*This justifies using list in other recursive type definitions*)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   153
lemma list_mono: "A<=B ==> list(A) <= list(B)"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   154
apply (rule subsetI)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   155
apply (erule list.induct)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   156
apply (auto intro!: list.intros)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   157
done
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   158
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   159
(*Type checking -- list creates well-founded sets*)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   160
lemma list_sexp: "list(sexp) <= sexp"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   161
apply (rule subsetI)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   162
apply (erule list.induct)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   163
apply (unfold NIL_def CONS_def)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   164
apply (auto intro: sexp.intros sexp_In0I sexp_In1I)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   165
done
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   166
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   167
(* A <= sexp ==> list(A) <= sexp *)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   168
lemmas list_subset_sexp = subset_trans [OF list_mono list_sexp] 
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   169
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   170
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   171
(*Induction for the type 'a list *)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   172
lemma list_induct:
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   173
    "[| P(Nil);    
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   174
        !!x xs. P(xs) ==> P(x # xs) |]  ==> P(l)"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   175
apply (unfold Nil_def Cons_def) 
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   176
apply (rule Rep_List_inverse [THEN subst])
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   177
(*types force good instantiation*)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   178
apply (rule Rep_List [unfolded List_def, THEN list.induct], simp)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   179
apply (erule Abs_List_inverse [unfolded List_def, THEN subst], blast) 
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   180
done
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   181
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   182
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   183
(*** Isomorphisms ***)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   184
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   185
lemma inj_on_Abs_list: "inj_on Abs_List (list(range Leaf))"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   186
apply (rule inj_on_inverseI)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   187
apply (erule Abs_List_inverse [unfolded List_def])
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   188
done
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   189
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   190
(** Distinctness of constructors **)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   191
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   192
lemma CONS_not_NIL [iff]: "CONS M N ~= NIL"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   193
by (simp add: NIL_def CONS_def)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   194
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   195
lemmas NIL_not_CONS [iff] = CONS_not_NIL [THEN not_sym]
45605
a89b4bc311a5 eliminated obsolete "standard";
wenzelm
parents: 39246
diff changeset
   196
lemmas CONS_neq_NIL = CONS_not_NIL [THEN notE]
35247
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   197
lemmas NIL_neq_CONS = sym [THEN CONS_neq_NIL]
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   198
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   199
lemma Cons_not_Nil [iff]: "x # xs ~= Nil"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   200
apply (unfold Nil_def Cons_def)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   201
apply (rule CONS_not_NIL [THEN inj_on_Abs_list [THEN inj_on_contraD]])
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   202
apply (simp_all add: list.intros rangeI Rep_List [unfolded List_def])
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   203
done
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   204
45605
a89b4bc311a5 eliminated obsolete "standard";
wenzelm
parents: 39246
diff changeset
   205
lemmas Nil_not_Cons = Cons_not_Nil [THEN not_sym]
a89b4bc311a5 eliminated obsolete "standard";
wenzelm
parents: 39246
diff changeset
   206
declare Nil_not_Cons [iff]
a89b4bc311a5 eliminated obsolete "standard";
wenzelm
parents: 39246
diff changeset
   207
lemmas Cons_neq_Nil = Cons_not_Nil [THEN notE]
35247
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   208
lemmas Nil_neq_Cons = sym [THEN Cons_neq_Nil]
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   209
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   210
(** Injectiveness of CONS and Cons **)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   211
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   212
lemma CONS_CONS_eq [iff]: "(CONS K M)=(CONS L N) = (K=L & M=N)"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   213
by (simp add: CONS_def)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   214
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   215
(*For reasoning about abstract list constructors*)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   216
declare Rep_List [THEN ListD, intro] ListI [intro]
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   217
declare list.intros [intro,simp]
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   218
declare Leaf_inject [dest!]
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   219
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   220
lemma Cons_Cons_eq [iff]: "(x#xs=y#ys) = (x=y & xs=ys)"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   221
apply (simp add: Cons_def)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   222
apply (subst Abs_List_inject)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   223
apply (auto simp add: Rep_List_inject)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   224
done
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   225
45605
a89b4bc311a5 eliminated obsolete "standard";
wenzelm
parents: 39246
diff changeset
   226
lemmas Cons_inject2 = Cons_Cons_eq [THEN iffD1, THEN conjE]
35247
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   227
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   228
lemma CONS_D: "CONS M N: list(A) ==> M: A & N: list(A)"
45694
4a8743618257 prefer typedef without extra definition and alternative name;
wenzelm
parents: 45605
diff changeset
   229
  by (induct L == "CONS M N" rule: list.induct) auto
35247
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   230
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   231
lemma sexp_CONS_D: "CONS M N: sexp ==> M: sexp & N: sexp"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   232
apply (simp add: CONS_def In1_def)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   233
apply (fast dest!: Scons_D)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   234
done
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   235
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   236
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   237
(*Reasoning about constructors and their freeness*)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   238
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   239
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   240
lemma not_CONS_self: "N: list(A) ==> !M. N ~= CONS M N"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   241
apply (erule list.induct) apply simp_all done
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   242
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   243
lemma not_Cons_self2: "\<forall>x. l ~= x#l"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   244
by (induct l rule: list_induct) simp_all
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   245
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   246
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   247
lemma neq_Nil_conv2: "(xs ~= []) = (\<exists>y ys. xs = y#ys)"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   248
by (induct xs rule: list_induct) auto
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   249
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   250
(** Conversion rules for List_case: case analysis operator **)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   251
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   252
lemma List_case_NIL [simp]: "List_case c h NIL = c"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   253
by (simp add: List_case_def NIL_def)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   254
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   255
lemma List_case_CONS [simp]: "List_case c h (CONS M N) = h M N"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   256
by (simp add: List_case_def CONS_def)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   257
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   258
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   259
(*** List_rec -- by wf recursion on pred_sexp ***)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   260
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   261
(* The trancl(pred_sexp) is essential because pred_sexp_CONS_I1,2 would not
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   262
   hold if pred_sexp^+ were changed to pred_sexp. *)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   263
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   264
lemma List_rec_unfold_lemma:
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   265
     "(%M. List_rec M c d) == 
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   266
      wfrec (pred_sexp^+) (%g. List_case c (%x y. d x y (g y)))"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   267
by (simp add: List_rec_def)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   268
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   269
lemmas List_rec_unfold = 
45605
a89b4bc311a5 eliminated obsolete "standard";
wenzelm
parents: 39246
diff changeset
   270
    def_wfrec [OF List_rec_unfold_lemma wf_pred_sexp [THEN wf_trancl]]
35247
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   271
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   272
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   273
(** pred_sexp lemmas **)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   274
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   275
lemma pred_sexp_CONS_I1: 
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   276
    "[| M: sexp;  N: sexp |] ==> (M, CONS M N) : pred_sexp^+"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   277
by (simp add: CONS_def In1_def)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   278
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   279
lemma pred_sexp_CONS_I2: 
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   280
    "[| M: sexp;  N: sexp |] ==> (N, CONS M N) : pred_sexp^+"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   281
by (simp add: CONS_def In1_def)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   282
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   283
lemma pred_sexp_CONS_D: 
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   284
    "(CONS M1 M2, N) : pred_sexp^+ ==>  
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   285
     (M1,N) : pred_sexp^+ & (M2,N) : pred_sexp^+"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   286
apply (frule pred_sexp_subset_Sigma [THEN trancl_subset_Sigma, THEN subsetD])
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   287
apply (blast dest!: sexp_CONS_D intro: pred_sexp_CONS_I1 pred_sexp_CONS_I2 
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   288
                    trans_trancl [THEN transD])
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   289
done
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   290
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   291
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   292
(** Conversion rules for List_rec **)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   293
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   294
lemma List_rec_NIL [simp]: "List_rec NIL c h = c"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   295
apply (rule List_rec_unfold [THEN trans])
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   296
apply (simp add: List_case_NIL)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   297
done
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   298
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   299
lemma List_rec_CONS [simp]:
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   300
     "[| M: sexp;  N: sexp |] 
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   301
      ==> List_rec (CONS M N) c h = h M N (List_rec N c h)"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   302
apply (rule List_rec_unfold [THEN trans])
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   303
apply (simp add: pred_sexp_CONS_I2)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   304
done
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   305
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   306
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   307
(*** list_rec -- by List_rec ***)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   308
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   309
lemmas Rep_List_in_sexp =
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   310
    subsetD [OF range_Leaf_subset_sexp [THEN list_subset_sexp]
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   311
                Rep_List [THEN ListD]] 
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   312
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   313
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   314
lemma list_rec_Nil [simp]: "list_rec Nil c h = c"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   315
by (simp add: list_rec_def ListI [THEN Abs_List_inverse] Nil_def)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   316
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   317
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   318
lemma list_rec_Cons [simp]: "list_rec (a#l) c h = h a l (list_rec l c h)"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   319
by (simp add: list_rec_def ListI [THEN Abs_List_inverse] Cons_def
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   320
              Rep_List_inverse Rep_List [THEN ListD] inj_Leaf Rep_List_in_sexp)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   321
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   322
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   323
(*Type checking.  Useful?*)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   324
lemma List_rec_type:
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   325
     "[| M: list(A);      
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   326
         A<=sexp;         
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   327
         c: C(NIL);       
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   328
         !!x y r. [| x: A;  y: list(A);  r: C(y) |] ==> h x y r: C(CONS x y)  
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   329
      |] ==> List_rec M c h : C(M :: 'a item)"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   330
apply (erule list.induct, simp) 
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   331
apply (insert list_subset_sexp) 
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   332
apply (subst List_rec_CONS, blast+)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   333
done
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   334
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   335
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   336
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   337
(** Generalized map functionals **)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   338
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   339
lemma Rep_map_Nil [simp]: "Rep_map f Nil = NIL"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   340
by (simp add: Rep_map_def)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   341
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   342
lemma Rep_map_Cons [simp]: 
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   343
    "Rep_map f(x#xs) = CONS(f x)(Rep_map f xs)"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   344
by (simp add: Rep_map_def)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   345
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   346
lemma Rep_map_type: "(!!x. f(x): A) ==> Rep_map f xs: list(A)"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   347
apply (simp add: Rep_map_def)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   348
apply (rule list_induct, auto)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   349
done
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   350
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   351
lemma Abs_map_NIL [simp]: "Abs_map g NIL = Nil"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   352
by (simp add: Abs_map_def)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   353
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   354
lemma Abs_map_CONS [simp]: 
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   355
    "[| M: sexp;  N: sexp |] ==> Abs_map g (CONS M N) = g(M) # Abs_map g N"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   356
by (simp add: Abs_map_def)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   357
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   358
(*Eases the use of primitive recursion.*)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   359
lemma def_list_rec_NilCons:
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   360
    "[| !!xs. f(xs) = list_rec xs c h  |] 
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   361
     ==> f [] = c & f(x#xs) = h x xs (f xs)"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   362
by simp 
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   363
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   364
lemma Abs_map_inverse:
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   365
     "[| M: list(A);  A<=sexp;  !!z. z: A ==> f(g(z)) = z |]  
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   366
      ==> Rep_map f (Abs_map g M) = M"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   367
apply (erule list.induct, simp_all)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   368
apply (insert list_subset_sexp) 
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   369
apply (subst Abs_map_CONS, blast)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   370
apply blast 
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   371
apply simp 
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   372
done
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   373
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   374
(*Rep_map_inverse is obtained via Abs_Rep_map and map_ident*)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   375
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   376
(** list_case **)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   377
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   378
(* setting up rewrite sets *)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   379
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   380
text{*Better to have a single theorem with a conjunctive conclusion.*}
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   381
declare def_list_rec_NilCons [OF list_case_def, simp]
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   382
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   383
(** list_case **)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   384
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   385
lemma expand_list_case: 
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   386
 "P(list_case a f xs) = ((xs=[] --> P a ) & (!y ys. xs=y#ys --> P(f y ys)))"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   387
by (induct xs rule: list_induct) simp_all
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   388
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   389
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   390
(**** Function definitions ****)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   391
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   392
declare def_list_rec_NilCons [OF map_def, simp]
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   393
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   394
(** The functional "map" and the generalized functionals **)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   395
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   396
lemma Abs_Rep_map: 
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   397
     "(!!x. f(x): sexp) ==>  
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   398
        Abs_map g (Rep_map f xs) = map (%t. g(f(t))) xs"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   399
apply (induct xs rule: list_induct)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   400
apply (simp_all add: Rep_map_type list_sexp [THEN subsetD])
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   401
done
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   402
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   403
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   404
(** Additional mapping lemmas **)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   405
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   406
lemma map_ident [simp]: "map(%x. x)(xs) = xs"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   407
by (induct xs rule: list_induct) simp_all
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   408
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   409
lemma map_compose: "map(f o g)(xs) = map f (map g xs)"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   410
apply (simp add: o_def)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   411
apply (induct xs rule: list_induct)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   412
apply simp_all
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   413
done
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   414
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   415
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   416
(** take **)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   417
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   418
lemma take_Suc1 [simp]: "take [] (Suc x) = []"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   419
by simp
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   420
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   421
lemma take_Suc2 [simp]: "take(a#xs)(Suc x) = a#take xs x"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   422
by simp
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   423
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   424
lemma take_Nil [simp]: "take [] n = []"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   425
by (induct n) simp_all
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   426
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   427
lemma take_take_eq [simp]: "\<forall>n. take (take xs n) n = take xs n"
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   428
apply (induct xs rule: list_induct)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   429
apply simp_all
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   430
apply (rule allI)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   431
apply (induct_tac n)
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   432
apply auto
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   433
done
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   434
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents:
diff changeset
   435
end