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