nipkow@35247: (*  Title:      HOL/Induct/SList.thy
nipkow@35247:     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
nipkow@35247: 
nipkow@35247: This theory is strictly of historical interest. It illustrates how
nipkow@35247: recursive datatypes can be constructed in higher-order logic from
nipkow@35247: first principles. Isabelle's datatype package automates a
nipkow@35247: construction of this sort.
nipkow@35247: 
nipkow@35247: Enriched theory of lists; mutual indirect recursive data-types.
nipkow@35247: 
nipkow@35247: Definition of type 'a list (strict lists) by a least fixed point
nipkow@35247: 
wenzelm@61943: We use          list(A) == lfp(%Z. {NUMB(0)} <+> A \<times> Z)
wenzelm@61943: and not         list    == lfp(%Z. {NUMB(0)} <+> range(Leaf) \<times> Z)
nipkow@35247: 
nipkow@35247: so that list can serve as a "functor" for defining other recursive types.
nipkow@35247: 
blanchet@58305: This enables the conservative construction of mutual recursive datatypes
nipkow@35247: such as
nipkow@35247: 
blanchet@58305: datatype 'a m = Node 'a * 'a m list
nipkow@35247: *)
nipkow@35247: 
wenzelm@60530: section \<open>Extended List Theory (old)\<close>
nipkow@35247: 
nipkow@35247: theory SList
nipkow@35247: imports Sexp
nipkow@35247: begin
nipkow@35247: 
nipkow@35247: (*Hilbert_Choice is needed for the function "inv"*)
nipkow@35247: 
nipkow@35247: (* *********************************************************************** *)
nipkow@35247: (*                                                                         *)
nipkow@35247: (* Building up data type                                                   *)
nipkow@35247: (*                                                                         *)
nipkow@35247: (* *********************************************************************** *)
nipkow@35247: 
nipkow@35247: 
nipkow@35247: (* Defining the Concrete Constructors *)
nipkow@35247: definition
nipkow@35247:   NIL  :: "'a item" where
nipkow@35247:   "NIL = In0(Numb(0))"
nipkow@35247: 
nipkow@35247: definition
nipkow@35247:   CONS :: "['a item, 'a item] => 'a item" where
nipkow@35247:   "CONS M N = In1(Scons M N)"
nipkow@35247: 
nipkow@35247: inductive_set
nipkow@35247:   list :: "'a item set => 'a item set"
nipkow@35247:   for A :: "'a item set"
nipkow@35247:   where
nipkow@35247:     NIL_I:  "NIL: list A"
nipkow@35247:   | CONS_I: "[| a: A;  M: list A |] ==> CONS a M : list A"
nipkow@35247: 
nipkow@35247: 
wenzelm@45694: definition "List = list (range Leaf)"
wenzelm@45694: 
wenzelm@49834: typedef 'a list = "List :: 'a item set"
wenzelm@45694:   morphisms Rep_List Abs_List
wenzelm@45694:   unfolding List_def by (blast intro: list.NIL_I)
nipkow@35247: 
blanchet@58112: abbreviation "Case == Old_Datatype.Case"
blanchet@58112: abbreviation "Split == Old_Datatype.Split"
nipkow@35247: 
nipkow@35247: definition
nipkow@35247:   List_case :: "['b, ['a item, 'a item]=>'b, 'a item] => 'b" where
nipkow@35247:   "List_case c d = Case(%x. c)(Split(d))"
nipkow@35247:   
nipkow@35247: definition
nipkow@35247:   List_rec  :: "['a item, 'b, ['a item, 'a item, 'b]=>'b] => 'b" where
nipkow@35247:   "List_rec M c d = wfrec (pred_sexp^+)
nipkow@35247:                            (%g. List_case c (%x y. d x y (g y))) M"
nipkow@35247: 
nipkow@35247: 
nipkow@35247: (* *********************************************************************** *)
nipkow@35247: (*                                                                         *)
nipkow@35247: (* Abstracting data type                                                   *)
nipkow@35247: (*                                                                         *)
nipkow@35247: (* *********************************************************************** *)
nipkow@35247: 
nipkow@35247: (*Declaring the abstract list constructors*)
nipkow@35247: 
nipkow@35247: no_translations
nipkow@35247:   "[x, xs]" == "x#[xs]"
nipkow@35247:   "[x]" == "x#[]"
nipkow@35247: no_notation
nipkow@35247:   Nil  ("[]") and
nipkow@35247:   Cons (infixr "#" 65)
nipkow@35247: 
nipkow@35247: definition
nipkow@35247:   Nil       :: "'a list"                               ("[]") where
nipkow@35247:    "Nil  = Abs_List(NIL)"
nipkow@35247: 
nipkow@35247: definition
nipkow@35247:   "Cons"       :: "['a, 'a list] => 'a list"           (infixr "#" 65) where
nipkow@35247:    "x#xs = Abs_List(CONS (Leaf x)(Rep_List xs))"
nipkow@35247: 
nipkow@35247: definition
nipkow@35247:   (* list Recursion -- the trancl is Essential; see list.ML *)
nipkow@35247:   list_rec  :: "['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b" where
nipkow@35247:    "list_rec l c d =
nipkow@35247:       List_rec(Rep_List l) c (%x y r. d(inv Leaf x)(Abs_List y) r)"
nipkow@35247: 
nipkow@35247: definition
nipkow@35247:   list_case :: "['b, ['a, 'a list]=>'b, 'a list] => 'b" where
nipkow@35247:    "list_case a f xs = list_rec xs a (%x xs r. f x xs)"
nipkow@35247: 
nipkow@35247: (* list Enumeration *)
nipkow@35247: translations
nipkow@35247:   "[x, xs]" == "x#[xs]"
nipkow@35247:   "[x]"     == "x#[]"
nipkow@35247: 
nipkow@35247:   "case xs of [] => a | y#ys => b" == "CONST list_case(a, %y ys. b, xs)"
nipkow@35247: 
nipkow@35247: 
nipkow@35247: (* *********************************************************************** *)
nipkow@35247: (*                                                                         *)
nipkow@35247: (* Generalized Map Functionals                                             *)
nipkow@35247: (*                                                                         *)
nipkow@35247: (* *********************************************************************** *)
nipkow@35247: 
nipkow@35247:   
nipkow@35247: (* Generalized Map Functionals *)
nipkow@35247: 
nipkow@35247: definition
nipkow@35247:   Rep_map   :: "('b => 'a item) => ('b list => 'a item)" where
nipkow@35247:    "Rep_map f xs = list_rec xs  NIL(%x l r. CONS(f x) r)"
nipkow@35247: 
nipkow@35247: definition
nipkow@35247:   Abs_map   :: "('a item => 'b) => 'a item => 'b list" where
nipkow@35247:    "Abs_map g M  = List_rec M Nil (%N L r. g(N)#r)"
nipkow@35247: 
nipkow@35247: 
nipkow@35247: definition
nipkow@35247:   map       :: "('a=>'b) => ('a list => 'b list)" where
nipkow@35247:   "map f xs = list_rec xs [] (%x l r. f(x)#r)"
nipkow@35247: 
haftmann@39246: primrec take :: "['a list,nat] => 'a list" where
nipkow@35247:   take_0:  "take xs 0 = []"
haftmann@39246: | take_Suc: "take xs (Suc n) = list_case [] (%x l. x # take l n) xs"
nipkow@35247: 
nipkow@35247: lemma ListI: "x : list (range Leaf) ==> x : List"
nipkow@35247: by (simp add: List_def)
nipkow@35247: 
nipkow@35247: lemma ListD: "x : List ==> x : list (range Leaf)"
nipkow@35247: by (simp add: List_def)
nipkow@35247: 
nipkow@35247: lemma list_unfold: "list(A) = usum {Numb(0)} (uprod A (list(A)))"
nipkow@35247:   by (fast intro!: list.intros [unfolded NIL_def CONS_def]
nipkow@35247:            elim: list.cases [unfolded NIL_def CONS_def])
nipkow@35247: 
nipkow@35247: (*This justifies using list in other recursive type definitions*)
nipkow@35247: lemma list_mono: "A<=B ==> list(A) <= list(B)"
nipkow@35247: apply (rule subsetI)
nipkow@35247: apply (erule list.induct)
nipkow@35247: apply (auto intro!: list.intros)
nipkow@35247: done
nipkow@35247: 
nipkow@35247: (*Type checking -- list creates well-founded sets*)
nipkow@35247: lemma list_sexp: "list(sexp) <= sexp"
nipkow@35247: apply (rule subsetI)
nipkow@35247: apply (erule list.induct)
nipkow@35247: apply (unfold NIL_def CONS_def)
nipkow@35247: apply (auto intro: sexp.intros sexp_In0I sexp_In1I)
nipkow@35247: done
nipkow@35247: 
nipkow@35247: (* A <= sexp ==> list(A) <= sexp *)
nipkow@35247: lemmas list_subset_sexp = subset_trans [OF list_mono list_sexp] 
nipkow@35247: 
nipkow@35247: 
nipkow@35247: (*Induction for the type 'a list *)
nipkow@35247: lemma list_induct:
nipkow@35247:     "[| P(Nil);    
nipkow@35247:         !!x xs. P(xs) ==> P(x # xs) |]  ==> P(l)"
nipkow@35247: apply (unfold Nil_def Cons_def) 
nipkow@35247: apply (rule Rep_List_inverse [THEN subst])
nipkow@35247: (*types force good instantiation*)
nipkow@35247: apply (rule Rep_List [unfolded List_def, THEN list.induct], simp)
nipkow@35247: apply (erule Abs_List_inverse [unfolded List_def, THEN subst], blast) 
nipkow@35247: done
nipkow@35247: 
nipkow@35247: 
nipkow@35247: (*** Isomorphisms ***)
nipkow@35247: 
nipkow@35247: lemma inj_on_Abs_list: "inj_on Abs_List (list(range Leaf))"
nipkow@35247: apply (rule inj_on_inverseI)
nipkow@35247: apply (erule Abs_List_inverse [unfolded List_def])
nipkow@35247: done
nipkow@35247: 
nipkow@35247: (** Distinctness of constructors **)
nipkow@35247: 
nipkow@35247: lemma CONS_not_NIL [iff]: "CONS M N ~= NIL"
nipkow@35247: by (simp add: NIL_def CONS_def)
nipkow@35247: 
nipkow@35247: lemmas NIL_not_CONS [iff] = CONS_not_NIL [THEN not_sym]
wenzelm@45605: lemmas CONS_neq_NIL = CONS_not_NIL [THEN notE]
nipkow@35247: lemmas NIL_neq_CONS = sym [THEN CONS_neq_NIL]
nipkow@35247: 
nipkow@35247: lemma Cons_not_Nil [iff]: "x # xs ~= Nil"
nipkow@35247: apply (unfold Nil_def Cons_def)
nipkow@35247: apply (rule CONS_not_NIL [THEN inj_on_Abs_list [THEN inj_on_contraD]])
nipkow@35247: apply (simp_all add: list.intros rangeI Rep_List [unfolded List_def])
nipkow@35247: done
nipkow@35247: 
wenzelm@45605: lemmas Nil_not_Cons = Cons_not_Nil [THEN not_sym]
wenzelm@45605: declare Nil_not_Cons [iff]
wenzelm@45605: lemmas Cons_neq_Nil = Cons_not_Nil [THEN notE]
nipkow@35247: lemmas Nil_neq_Cons = sym [THEN Cons_neq_Nil]
nipkow@35247: 
nipkow@35247: (** Injectiveness of CONS and Cons **)
nipkow@35247: 
nipkow@35247: lemma CONS_CONS_eq [iff]: "(CONS K M)=(CONS L N) = (K=L & M=N)"
nipkow@35247: by (simp add: CONS_def)
nipkow@35247: 
nipkow@35247: (*For reasoning about abstract list constructors*)
nipkow@35247: declare Rep_List [THEN ListD, intro] ListI [intro]
nipkow@35247: declare list.intros [intro,simp]
nipkow@35247: declare Leaf_inject [dest!]
nipkow@35247: 
nipkow@35247: lemma Cons_Cons_eq [iff]: "(x#xs=y#ys) = (x=y & xs=ys)"
nipkow@35247: apply (simp add: Cons_def)
nipkow@35247: apply (subst Abs_List_inject)
nipkow@35247: apply (auto simp add: Rep_List_inject)
nipkow@35247: done
nipkow@35247: 
wenzelm@45605: lemmas Cons_inject2 = Cons_Cons_eq [THEN iffD1, THEN conjE]
nipkow@35247: 
nipkow@35247: lemma CONS_D: "CONS M N: list(A) ==> M: A & N: list(A)"
wenzelm@45694:   by (induct L == "CONS M N" rule: list.induct) auto
nipkow@35247: 
nipkow@35247: lemma sexp_CONS_D: "CONS M N: sexp ==> M: sexp & N: sexp"
nipkow@35247: apply (simp add: CONS_def In1_def)
nipkow@35247: apply (fast dest!: Scons_D)
nipkow@35247: done
nipkow@35247: 
nipkow@35247: 
nipkow@35247: (*Reasoning about constructors and their freeness*)
nipkow@35247: 
nipkow@35247: 
nipkow@35247: lemma not_CONS_self: "N: list(A) ==> !M. N ~= CONS M N"
nipkow@35247: apply (erule list.induct) apply simp_all done
nipkow@35247: 
nipkow@35247: lemma not_Cons_self2: "\<forall>x. l ~= x#l"
nipkow@35247: by (induct l rule: list_induct) simp_all
nipkow@35247: 
nipkow@35247: 
nipkow@35247: lemma neq_Nil_conv2: "(xs ~= []) = (\<exists>y ys. xs = y#ys)"
nipkow@35247: by (induct xs rule: list_induct) auto
nipkow@35247: 
nipkow@35247: (** Conversion rules for List_case: case analysis operator **)
nipkow@35247: 
nipkow@35247: lemma List_case_NIL [simp]: "List_case c h NIL = c"
nipkow@35247: by (simp add: List_case_def NIL_def)
nipkow@35247: 
nipkow@35247: lemma List_case_CONS [simp]: "List_case c h (CONS M N) = h M N"
nipkow@35247: by (simp add: List_case_def CONS_def)
nipkow@35247: 
nipkow@35247: 
nipkow@35247: (*** List_rec -- by wf recursion on pred_sexp ***)
nipkow@35247: 
nipkow@35247: (* The trancl(pred_sexp) is essential because pred_sexp_CONS_I1,2 would not
nipkow@35247:    hold if pred_sexp^+ were changed to pred_sexp. *)
nipkow@35247: 
nipkow@35247: lemma List_rec_unfold_lemma:
nipkow@35247:      "(%M. List_rec M c d) == 
nipkow@35247:       wfrec (pred_sexp^+) (%g. List_case c (%x y. d x y (g y)))"
nipkow@35247: by (simp add: List_rec_def)
nipkow@35247: 
nipkow@35247: lemmas List_rec_unfold = 
wenzelm@45605:     def_wfrec [OF List_rec_unfold_lemma wf_pred_sexp [THEN wf_trancl]]
nipkow@35247: 
nipkow@35247: 
nipkow@35247: (** pred_sexp lemmas **)
nipkow@35247: 
nipkow@35247: lemma pred_sexp_CONS_I1: 
nipkow@35247:     "[| M: sexp;  N: sexp |] ==> (M, CONS M N) : pred_sexp^+"
nipkow@35247: by (simp add: CONS_def In1_def)
nipkow@35247: 
nipkow@35247: lemma pred_sexp_CONS_I2: 
nipkow@35247:     "[| M: sexp;  N: sexp |] ==> (N, CONS M N) : pred_sexp^+"
nipkow@35247: by (simp add: CONS_def In1_def)
nipkow@35247: 
nipkow@35247: lemma pred_sexp_CONS_D: 
nipkow@35247:     "(CONS M1 M2, N) : pred_sexp^+ ==>  
nipkow@35247:      (M1,N) : pred_sexp^+ & (M2,N) : pred_sexp^+"
nipkow@35247: apply (frule pred_sexp_subset_Sigma [THEN trancl_subset_Sigma, THEN subsetD])
nipkow@35247: apply (blast dest!: sexp_CONS_D intro: pred_sexp_CONS_I1 pred_sexp_CONS_I2 
nipkow@35247:                     trans_trancl [THEN transD])
nipkow@35247: done
nipkow@35247: 
nipkow@35247: 
nipkow@35247: (** Conversion rules for List_rec **)
nipkow@35247: 
nipkow@35247: lemma List_rec_NIL [simp]: "List_rec NIL c h = c"
nipkow@35247: apply (rule List_rec_unfold [THEN trans])
nipkow@35247: apply (simp add: List_case_NIL)
nipkow@35247: done
nipkow@35247: 
nipkow@35247: lemma List_rec_CONS [simp]:
nipkow@35247:      "[| M: sexp;  N: sexp |] 
nipkow@35247:       ==> List_rec (CONS M N) c h = h M N (List_rec N c h)"
nipkow@35247: apply (rule List_rec_unfold [THEN trans])
nipkow@35247: apply (simp add: pred_sexp_CONS_I2)
nipkow@35247: done
nipkow@35247: 
nipkow@35247: 
nipkow@35247: (*** list_rec -- by List_rec ***)
nipkow@35247: 
nipkow@35247: lemmas Rep_List_in_sexp =
nipkow@35247:     subsetD [OF range_Leaf_subset_sexp [THEN list_subset_sexp]
nipkow@35247:                 Rep_List [THEN ListD]] 
nipkow@35247: 
nipkow@35247: 
nipkow@35247: lemma list_rec_Nil [simp]: "list_rec Nil c h = c"
nipkow@35247: by (simp add: list_rec_def ListI [THEN Abs_List_inverse] Nil_def)
nipkow@35247: 
nipkow@35247: 
nipkow@35247: lemma list_rec_Cons [simp]: "list_rec (a#l) c h = h a l (list_rec l c h)"
nipkow@35247: by (simp add: list_rec_def ListI [THEN Abs_List_inverse] Cons_def
nipkow@35247:               Rep_List_inverse Rep_List [THEN ListD] inj_Leaf Rep_List_in_sexp)
nipkow@35247: 
nipkow@35247: 
nipkow@35247: (*Type checking.  Useful?*)
nipkow@35247: lemma List_rec_type:
nipkow@35247:      "[| M: list(A);      
nipkow@35247:          A<=sexp;         
nipkow@35247:          c: C(NIL);       
nipkow@35247:          !!x y r. [| x: A;  y: list(A);  r: C(y) |] ==> h x y r: C(CONS x y)  
nipkow@35247:       |] ==> List_rec M c h : C(M :: 'a item)"
nipkow@35247: apply (erule list.induct, simp) 
nipkow@35247: apply (insert list_subset_sexp) 
nipkow@35247: apply (subst List_rec_CONS, blast+)
nipkow@35247: done
nipkow@35247: 
nipkow@35247: 
nipkow@35247: 
nipkow@35247: (** Generalized map functionals **)
nipkow@35247: 
nipkow@35247: lemma Rep_map_Nil [simp]: "Rep_map f Nil = NIL"
nipkow@35247: by (simp add: Rep_map_def)
nipkow@35247: 
nipkow@35247: lemma Rep_map_Cons [simp]: 
nipkow@35247:     "Rep_map f(x#xs) = CONS(f x)(Rep_map f xs)"
nipkow@35247: by (simp add: Rep_map_def)
nipkow@35247: 
nipkow@35247: lemma Rep_map_type: "(!!x. f(x): A) ==> Rep_map f xs: list(A)"
nipkow@35247: apply (simp add: Rep_map_def)
nipkow@35247: apply (rule list_induct, auto)
nipkow@35247: done
nipkow@35247: 
nipkow@35247: lemma Abs_map_NIL [simp]: "Abs_map g NIL = Nil"
nipkow@35247: by (simp add: Abs_map_def)
nipkow@35247: 
nipkow@35247: lemma Abs_map_CONS [simp]: 
nipkow@35247:     "[| M: sexp;  N: sexp |] ==> Abs_map g (CONS M N) = g(M) # Abs_map g N"
nipkow@35247: by (simp add: Abs_map_def)
nipkow@35247: 
nipkow@35247: (*Eases the use of primitive recursion.*)
nipkow@35247: lemma def_list_rec_NilCons:
nipkow@35247:     "[| !!xs. f(xs) = list_rec xs c h  |] 
nipkow@35247:      ==> f [] = c & f(x#xs) = h x xs (f xs)"
nipkow@35247: by simp 
nipkow@35247: 
nipkow@35247: lemma Abs_map_inverse:
nipkow@35247:      "[| M: list(A);  A<=sexp;  !!z. z: A ==> f(g(z)) = z |]  
nipkow@35247:       ==> Rep_map f (Abs_map g M) = M"
nipkow@35247: apply (erule list.induct, simp_all)
nipkow@35247: apply (insert list_subset_sexp) 
nipkow@35247: apply (subst Abs_map_CONS, blast)
nipkow@35247: apply blast 
nipkow@35247: apply simp 
nipkow@35247: done
nipkow@35247: 
nipkow@35247: (*Rep_map_inverse is obtained via Abs_Rep_map and map_ident*)
nipkow@35247: 
nipkow@35247: (** list_case **)
nipkow@35247: 
nipkow@35247: (* setting up rewrite sets *)
nipkow@35247: 
wenzelm@60530: text\<open>Better to have a single theorem with a conjunctive conclusion.\<close>
nipkow@35247: declare def_list_rec_NilCons [OF list_case_def, simp]
nipkow@35247: 
nipkow@35247: (** list_case **)
nipkow@35247: 
nipkow@35247: lemma expand_list_case: 
nipkow@35247:  "P(list_case a f xs) = ((xs=[] --> P a ) & (!y ys. xs=y#ys --> P(f y ys)))"
nipkow@35247: by (induct xs rule: list_induct) simp_all
nipkow@35247: 
nipkow@35247: 
nipkow@35247: (**** Function definitions ****)
nipkow@35247: 
nipkow@35247: declare def_list_rec_NilCons [OF map_def, simp]
nipkow@35247: 
nipkow@35247: (** The functional "map" and the generalized functionals **)
nipkow@35247: 
nipkow@35247: lemma Abs_Rep_map: 
nipkow@35247:      "(!!x. f(x): sexp) ==>  
nipkow@35247:         Abs_map g (Rep_map f xs) = map (%t. g(f(t))) xs"
nipkow@35247: apply (induct xs rule: list_induct)
nipkow@35247: apply (simp_all add: Rep_map_type list_sexp [THEN subsetD])
nipkow@35247: done
nipkow@35247: 
nipkow@35247: 
nipkow@35247: (** Additional mapping lemmas **)
nipkow@35247: 
nipkow@35247: lemma map_ident [simp]: "map(%x. x)(xs) = xs"
nipkow@35247: by (induct xs rule: list_induct) simp_all
nipkow@35247: 
nipkow@35247: lemma map_compose: "map(f o g)(xs) = map f (map g xs)"
nipkow@35247: apply (simp add: o_def)
nipkow@35247: apply (induct xs rule: list_induct)
nipkow@35247: apply simp_all
nipkow@35247: done
nipkow@35247: 
nipkow@35247: 
nipkow@35247: (** take **)
nipkow@35247: 
nipkow@35247: lemma take_Suc1 [simp]: "take [] (Suc x) = []"
nipkow@35247: by simp
nipkow@35247: 
nipkow@35247: lemma take_Suc2 [simp]: "take(a#xs)(Suc x) = a#take xs x"
nipkow@35247: by simp
nipkow@35247: 
nipkow@35247: lemma take_Nil [simp]: "take [] n = []"
nipkow@35247: by (induct n) simp_all
nipkow@35247: 
nipkow@35247: lemma take_take_eq [simp]: "\<forall>n. take (take xs n) n = take xs n"
nipkow@35247: apply (induct xs rule: list_induct)
nipkow@35247: apply simp_all
nipkow@35247: apply (rule allI)
nipkow@35247: apply (induct_tac n)
nipkow@35247: apply auto
nipkow@35247: done
nipkow@35247: 
nipkow@35247: end