--- a/src/HOL/Induct/SList.thy Thu Apr 04 16:48:00 2002 +0200
+++ b/src/HOL/Induct/SList.thy Thu Apr 04 17:32:52 2002 +0200
@@ -1,7 +1,7 @@
(* *********************************************************************** *)
(* *)
(* Title: SList.thy (Extended List Theory) *)
-(* Based on: $Id$ *)
+(* Based on: $Id$ *)
(* Author: Lawrence C Paulson, Cambridge University Computer Laboratory*)
(* Author: B. Wolff, University of Bremen *)
(* Purpose: Enriched theory of lists *)
@@ -24,40 +24,42 @@
Tidied by lcp. Still needs removal of nat_rec.
*)
-SList = NatArith + Sexp + Hilbert_Choice (*gives us "inv"*) +
+theory SList = NatArith + Sexp + Hilbert_Choice:
+
+(*Hilbert_Choice is needed for the function "inv"*)
+
(* *********************************************************************** *)
(* *)
(* Building up data type *)
(* *)
(* *********************************************************************** *)
-consts
- list :: "'a item set => 'a item set"
-
- NIL :: "'a item"
- CONS :: "['a item, 'a item] => 'a item"
- List_case :: "['b, ['a item, 'a item]=>'b, 'a item] => 'b"
- List_rec :: "['a item, 'b, ['a item, 'a item, 'b]=>'b] => 'b"
+(* Defining the Concrete Constructors *)
+constdefs
+ NIL :: "'a item"
+ "NIL == In0(Numb(0))"
-defs
- (* Defining the Concrete Constructors *)
- NIL_def "NIL == In0(Numb(0))"
- CONS_def "CONS M N == In1(Scons M N)"
+ CONS :: "['a item, 'a item] => 'a item"
+ "CONS M N == In1(Scons M N)"
+consts
+ list :: "'a item set => 'a item set"
inductive "list(A)"
- intrs
- NIL_I "NIL: list A"
- CONS_I "[| a: A; M: list A |] ==> CONS a M : list A"
+ intros
+ NIL_I: "NIL: list A"
+ CONS_I: "[| a: A; M: list A |] ==> CONS a M : list A"
typedef (List)
- 'a list = "list(range Leaf) :: 'a item set" (list.NIL_I)
+ 'a list = "list(range Leaf) :: 'a item set"
+ by (blast intro: list.NIL_I)
-defs
- List_case_def "List_case c d == Case(%x. c)(Split(d))"
+constdefs
+ List_case :: "['b, ['a item, 'a item]=>'b, 'a item] => 'b"
+ "List_case c d == Case(%x. c)(Split(d))"
- List_rec_def
+ List_rec :: "['a item, 'b, ['a item, 'a item, 'b]=>'b] => 'b"
"List_rec M c d == wfrec (trancl pred_sexp)
(%g. List_case c (%x y. d x y (g y))) M"
@@ -69,15 +71,26 @@
(* *********************************************************************** *)
(*Declaring the abstract list constructors*)
-consts
+
+constdefs
Nil :: "'a list"
- "#" :: "['a, 'a list] => 'a list" (infixr 65)
+ "Nil == Abs_List(NIL)"
+
+ "Cons" :: "['a, 'a list] => 'a list" (infixr "#" 65)
+ "x#xs == Abs_List(CONS (Leaf x)(Rep_List xs))"
+
list_case :: "['b, ['a, 'a list]=>'b, 'a list] => 'b"
- list_rec :: "['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b"
+ "list_case a f xs == list_rec xs a (%x xs r. f x xs)"
+
+ (* list Recursion -- the trancl is Essential; see list.ML *)
+ list_rec :: "['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b"
+ "list_rec l c d ==
+ List_rec(Rep_List l) c (%x y r. d(inv Leaf x)(Abs_List y) r)"
+
(* list Enumeration *)
-
+consts
"[]" :: "'a list" ("[]")
"@list" :: "args => 'a list" ("[(_)]")
@@ -88,22 +101,6 @@
"case xs of Nil => a | y#ys => b" == "list_case(a, %y ys. b, xs)"
-
-
-defs
- (* Defining the Abstract Constructors *)
- Nil_def "Nil == Abs_List(NIL)"
- Cons_def "x#xs == Abs_List(CONS (Leaf x)(Rep_List xs))"
-
- list_case_def "list_case a f xs == list_rec xs a (%x xs r. f x xs)"
-
- (* list Recursion -- the trancl is Essential; see list.ML *)
-
- list_rec_def
- "list_rec l c d == \
- \ List_rec(Rep_List l) c (%x y r. d(inv Leaf x)(Abs_List y) r)"
-
-
(* *********************************************************************** *)
(* *)
@@ -114,13 +111,12 @@
(* Generalized Map Functionals *)
-consts
+constdefs
Rep_map :: "('b => 'a item) => ('b list => 'a item)"
- Abs_map :: "('a item => 'b) => 'a item => 'b list"
+ "Rep_map f xs == list_rec xs NIL(%x l r. CONS(f x) r)"
-defs
- Rep_map_def "Rep_map f xs == list_rec xs NIL(%x l r. CONS(f x) r)"
- Abs_map_def "Abs_map g M == List_rec M Nil (%N L r. g(N)#r)"
+ Abs_map :: "('a item => 'b) => 'a item => 'b list"
+ "Abs_map g M == List_rec M Nil (%N L r. g(N)#r)"
(**** Function definitions ****)
@@ -140,7 +136,7 @@
ttl :: "'a list => 'a list"
"ttl xs == list_rec xs [] (%x xs r. xs)"
- mem :: "['a, 'a list] => bool" (infixl 55)
+ member :: "['a, 'a list] => bool" (infixl "mem" 55)
"x mem xs == list_rec xs False (%y ys r. if y=x then True else r)"
list_all :: "('a => bool) => ('a list => bool)"
@@ -150,13 +146,10 @@
"map f xs == list_rec xs [] (%x l r. f(x)#r)"
-consts
- "@" :: ['a list, 'a list] => 'a list (infixr 65)
-defs
- append_def"xs@ys == list_rec xs ys (%x l r. x#r)"
+constdefs
+ append :: "['a list, 'a list] => 'a list" (infixr "@" 65)
+ "xs@ys == list_rec xs ys (%x l r. x#r)"
-
-constdefs
filter :: "['a => bool, 'a list] => 'a list"
"filter P xs == list_rec xs [] (%x xs r. if P(x)then x#r else r)"
@@ -184,7 +177,6 @@
rev :: "'a list => 'a list"
"rev xs == list_rec xs [] (%x xs xsa. xsa @ [x])"
-
(* miscellaneous definitions *)
zip :: "'a list * 'b list => ('a*'b) list"
"zip == zipWith (%s. s)"
@@ -200,23 +192,793 @@
consts take :: "['a list,nat] => 'a list"
primrec
- take_0 "take xs 0 = []"
- take_Suc "take xs (Suc n) = list_case [] (%x l. x # take l n) xs"
+ take_0: "take xs 0 = []"
+ take_Suc: "take xs (Suc n) = list_case [] (%x l. x # take l n) xs"
consts enum :: "[nat,nat] => nat list"
primrec
- enum_0 "enum i 0 = []"
- enum_Suc "enum i (Suc j) = (if i <= j then enum i j @ [j] else [])"
+ enum_0: "enum i 0 = []"
+ enum_Suc: "enum i (Suc j) = (if i <= j then enum i j @ [j] else [])"
syntax
(* Special syntax for list_all and filter *)
"@Alls" :: "[idt, 'a list, bool] => bool" ("(2Alls _:_./ _)" 10)
- "@filter" :: "[idt, 'a list, bool] => 'a list" ("(1[_:_ ./ _])")
+ "@filter" :: "[idt, 'a list, bool] => 'a list" ("(1[_:_ ./ _])")
translations
"[x:xs. P]" == "filter(%x. P) xs"
"Alls x:xs. P"== "list_all(%x. P)xs"
+lemma ListI: "x : list (range Leaf) ==> x : List"
+by (simp add: List_def)
+
+lemma ListD: "x : List ==> x : list (range Leaf)"
+by (simp add: List_def)
+
+lemma list_unfold: "list(A) = usum {Numb(0)} (uprod A (list(A)))"
+ by (fast intro!: list.intros [unfolded NIL_def CONS_def]
+ elim: list.cases [unfolded NIL_def CONS_def])
+
+(*This justifies using list in other recursive type definitions*)
+lemma list_mono: "A<=B ==> list(A) <= list(B)"
+apply (unfold list.defs )
+apply (rule lfp_mono)
+apply (assumption | rule basic_monos)+
+done
+
+(*Type checking -- list creates well-founded sets*)
+lemma list_sexp: "list(sexp) <= sexp"
+apply (unfold NIL_def CONS_def list.defs)
+apply (rule lfp_lowerbound)
+apply (fast intro: sexp.intros sexp_In0I sexp_In1I)
+done
+
+(* A <= sexp ==> list(A) <= sexp *)
+lemmas list_subset_sexp = subset_trans [OF list_mono list_sexp]
+
+
+(*Induction for the type 'a list *)
+lemma list_induct:
+ "[| P(Nil);
+ !!x xs. P(xs) ==> P(x # xs) |] ==> P(l)"
+apply (unfold Nil_def Cons_def)
+apply (rule Rep_List_inverse [THEN subst])
+ (*types force good instantiation*)
+apply (rule Rep_List [unfolded List_def, THEN list.induct], simp)
+apply (erule Abs_List_inverse [unfolded List_def, THEN subst], blast)
+done
+
+
+(*** Isomorphisms ***)
+
+lemma inj_on_Abs_list: "inj_on Abs_List (list(range Leaf))"
+apply (rule inj_on_inverseI)
+apply (erule Abs_List_inverse [unfolded List_def])
+done
+
+(** Distinctness of constructors **)
+
+lemma CONS_not_NIL [iff]: "CONS M N ~= NIL"
+by (simp add: NIL_def CONS_def)
+
+lemmas NIL_not_CONS [iff] = CONS_not_NIL [THEN not_sym]
+lemmas CONS_neq_NIL = CONS_not_NIL [THEN notE, standard]
+lemmas NIL_neq_CONS = sym [THEN CONS_neq_NIL]
+
+lemma Cons_not_Nil [iff]: "x # xs ~= Nil"
+apply (unfold Nil_def Cons_def)
+apply (rule CONS_not_NIL [THEN inj_on_Abs_list [THEN inj_on_contraD]])
+apply (simp_all add: list.intros rangeI Rep_List [unfolded List_def])
+done
+
+lemmas Nil_not_Cons [iff] = Cons_not_Nil [THEN not_sym, standard]
+lemmas Cons_neq_Nil = Cons_not_Nil [THEN notE, standard]
+lemmas Nil_neq_Cons = sym [THEN Cons_neq_Nil]
+
+(** Injectiveness of CONS and Cons **)
+
+lemma CONS_CONS_eq [iff]: "(CONS K M)=(CONS L N) = (K=L & M=N)"
+by (simp add: CONS_def)
+
+(*For reasoning about abstract list constructors*)
+declare Rep_List [THEN ListD, intro] ListI [intro]
+declare list.intros [intro,simp]
+declare Leaf_inject [dest!]
+
+lemma Cons_Cons_eq [iff]: "(x#xs=y#ys) = (x=y & xs=ys)"
+apply (simp add: Cons_def)
+apply (subst Abs_List_inject)
+apply (auto simp add: Rep_List_inject)
+done
+
+lemmas Cons_inject2 = Cons_Cons_eq [THEN iffD1, THEN conjE, standard]
+
+lemma CONS_D: "CONS M N: list(A) ==> M: A & N: list(A)"
+apply (erule setup_induction)
+apply (erule list.induct, blast+)
+done
+
+lemma sexp_CONS_D: "CONS M N: sexp ==> M: sexp & N: sexp"
+apply (simp add: CONS_def In1_def)
+apply (fast dest!: Scons_D)
+done
+
+
+(*Reasoning about constructors and their freeness*)
+
+
+lemma not_CONS_self: "N: list(A) ==> !M. N ~= CONS M N"
+by (erule list.induct, simp_all)
+
+lemma not_Cons_self2: "\<forall>x. l ~= x#l"
+by (induct_tac "l" rule: list_induct, simp_all)
+
+
+lemma neq_Nil_conv2: "(xs ~= []) = (\<exists>y ys. xs = y#ys)"
+by (induct_tac "xs" rule: list_induct, auto)
+
+(** Conversion rules for List_case: case analysis operator **)
+
+lemma List_case_NIL [simp]: "List_case c h NIL = c"
+by (simp add: List_case_def NIL_def)
+
+lemma List_case_CONS [simp]: "List_case c h (CONS M N) = h M N"
+by (simp add: List_case_def CONS_def)
+
+
+(*** List_rec -- by wf recursion on pred_sexp ***)
+
+(* The trancl(pred_sexp) is essential because pred_sexp_CONS_I1,2 would not
+ hold if pred_sexp^+ were changed to pred_sexp. *)
+
+lemma List_rec_unfold_lemma:
+ "(%M. List_rec M c d) ==
+ wfrec (trancl pred_sexp) (%g. List_case c (%x y. d x y (g y)))"
+by (simp add: List_rec_def)
+
+lemmas List_rec_unfold =
+ def_wfrec [OF List_rec_unfold_lemma wf_pred_sexp [THEN wf_trancl],
+ standard]
+
+
+(** pred_sexp lemmas **)
+
+lemma pred_sexp_CONS_I1:
+ "[| M: sexp; N: sexp |] ==> (M, CONS M N) : pred_sexp^+"
+by (simp add: CONS_def In1_def)
+
+lemma pred_sexp_CONS_I2:
+ "[| M: sexp; N: sexp |] ==> (N, CONS M N) : pred_sexp^+"
+by (simp add: CONS_def In1_def)
+
+lemma pred_sexp_CONS_D:
+ "(CONS M1 M2, N) : pred_sexp^+ ==>
+ (M1,N) : pred_sexp^+ & (M2,N) : pred_sexp^+"
+apply (frule pred_sexp_subset_Sigma [THEN trancl_subset_Sigma, THEN subsetD])
+apply (blast dest!: sexp_CONS_D intro: pred_sexp_CONS_I1 pred_sexp_CONS_I2
+ trans_trancl [THEN transD])
+done
+
+
+(** Conversion rules for List_rec **)
+
+lemma List_rec_NIL [simp]: "List_rec NIL c h = c"
+apply (rule List_rec_unfold [THEN trans])
+apply (simp add: List_case_NIL)
+done
+
+lemma List_rec_CONS [simp]:
+ "[| M: sexp; N: sexp |]
+ ==> List_rec (CONS M N) c h = h M N (List_rec N c h)"
+apply (rule List_rec_unfold [THEN trans])
+apply (simp add: pred_sexp_CONS_I2)
+done
+
+
+(*** list_rec -- by List_rec ***)
+
+lemmas Rep_List_in_sexp =
+ subsetD [OF range_Leaf_subset_sexp [THEN list_subset_sexp]
+ Rep_List [THEN ListD]]
+
+
+lemma list_rec_Nil [simp]: "list_rec Nil c h = c"
+by (simp add: list_rec_def ListI [THEN Abs_List_inverse] Nil_def)
+
+
+lemma list_rec_Cons [simp]: "list_rec (a#l) c h = h a l (list_rec l c h)"
+by (simp add: list_rec_def ListI [THEN Abs_List_inverse] Cons_def
+ Rep_List_inverse Rep_List [THEN ListD] inj_Leaf Rep_List_in_sexp)
+
+
+(*Type checking. Useful?*)
+lemma List_rec_type:
+ "[| M: list(A);
+ A<=sexp;
+ c: C(NIL);
+ !!x y r. [| x: A; y: list(A); r: C(y) |] ==> h x y r: C(CONS x y)
+ |] ==> List_rec M c h : C(M :: 'a item)"
+apply (erule list.induct, simp)
+apply (insert list_subset_sexp)
+apply (subst List_rec_CONS, blast+)
+done
+
+
+
+(** Generalized map functionals **)
+
+lemma Rep_map_Nil [simp]: "Rep_map f Nil = NIL"
+by (simp add: Rep_map_def)
+
+lemma Rep_map_Cons [simp]:
+ "Rep_map f(x#xs) = CONS(f x)(Rep_map f xs)"
+by (simp add: Rep_map_def)
+
+lemma Rep_map_type: "(!!x. f(x): A) ==> Rep_map f xs: list(A)"
+apply (simp add: Rep_map_def)
+apply (rule list_induct, auto)
+done
+
+lemma Abs_map_NIL [simp]: "Abs_map g NIL = Nil"
+by (simp add: Abs_map_def)
+
+lemma Abs_map_CONS [simp]:
+ "[| M: sexp; N: sexp |] ==> Abs_map g (CONS M N) = g(M) # Abs_map g N"
+by (simp add: Abs_map_def)
+
+(*Eases the use of primitive recursion. NOTE USE OF == *)
+lemma def_list_rec_NilCons:
+ "[| !!xs. f(xs) == list_rec xs c h |]
+ ==> f [] = c & f(x#xs) = h x xs (f xs)"
+by simp
+
+
+
+lemma Abs_map_inverse:
+ "[| M: list(A); A<=sexp; !!z. z: A ==> f(g(z)) = z |]
+ ==> Rep_map f (Abs_map g M) = M"
+apply (erule list.induct, simp_all)
+apply (insert list_subset_sexp)
+apply (subst Abs_map_CONS, blast)
+apply blast
+apply simp
+done
+
+(*Rep_map_inverse is obtained via Abs_Rep_map and map_ident*)
+
+(** list_case **)
+
+(* setting up rewrite sets *)
+
+text{*Better to have a single theorem with a conjunctive conclusion.*}
+declare def_list_rec_NilCons [OF list_case_def, simp]
+
+(** list_case **)
+
+lemma expand_list_case:
+ "P(list_case a f xs) = ((xs=[] --> P a ) & (!y ys. xs=y#ys --> P(f y ys)))"
+by (induct_tac "xs" rule: list_induct, simp_all)
+
+
+(**** Function definitions ****)
+
+declare def_list_rec_NilCons [OF null_def, simp]
+declare def_list_rec_NilCons [OF hd_def, simp]
+declare def_list_rec_NilCons [OF tl_def, simp]
+declare def_list_rec_NilCons [OF ttl_def, simp]
+declare def_list_rec_NilCons [OF append_def, simp]
+declare def_list_rec_NilCons [OF member_def, simp]
+declare def_list_rec_NilCons [OF map_def, simp]
+declare def_list_rec_NilCons [OF filter_def, simp]
+declare def_list_rec_NilCons [OF list_all_def, simp]
+
+
+(** nth **)
+
+lemma def_nat_rec_0_eta:
+ "[| !!n. f == nat_rec c h |] ==> f(0) = c"
+by simp
+
+lemma def_nat_rec_Suc_eta:
+ "[| !!n. f == nat_rec c h |] ==> f(Suc(n)) = h n (f n)"
+by simp
+
+declare def_nat_rec_0_eta [OF nth_def, simp]
+declare def_nat_rec_Suc_eta [OF nth_def, simp]
+
+
+(** length **)
+
+lemma length_Nil [simp]: "length([]) = 0"
+by (simp add: length_def)
+
+lemma length_Cons [simp]: "length(a#xs) = Suc(length(xs))"
+by (simp add: length_def)
+
+
+(** @ - append **)
+
+lemma append_assoc [simp]: "(xs@ys)@zs = xs@(ys@zs)"
+by (induct_tac "xs" rule: list_induct, simp_all)
+
+lemma append_Nil2 [simp]: "xs @ [] = xs"
+by (induct_tac "xs" rule: list_induct, simp_all)
+
+(** mem **)
+
+lemma mem_append [simp]: "x mem (xs@ys) = (x mem xs | x mem ys)"
+by (induct_tac "xs" rule: list_induct, simp_all)
+
+lemma mem_filter [simp]: "x mem [x:xs. P x ] = (x mem xs & P(x))"
+by (induct_tac "xs" rule: list_induct, simp_all)
+
+(** list_all **)
+
+lemma list_all_True [simp]: "(Alls x:xs. True) = True"
+by (induct_tac "xs" rule: list_induct, simp_all)
+
+lemma list_all_conj [simp]:
+ "list_all p (xs@ys) = ((list_all p xs) & (list_all p ys))"
+by (induct_tac "xs" rule: list_induct, simp_all)
+
+lemma list_all_mem_conv: "(Alls x:xs. P(x)) = (!x. x mem xs --> P(x))"
+apply (induct_tac "xs" rule: list_induct, simp_all)
+apply blast
+done
+
+lemma nat_case_dist : "(! n. P n) = (P 0 & (! n. P (Suc n)))"
+apply auto
+apply (induct_tac "n", auto)
+done
+
+
+lemma alls_P_eq_P_nth: "(Alls u:A. P u) = (!n. n < length A --> P(nth n A))"
+apply (induct_tac "A" rule: list_induct, simp_all)
+apply (rule trans)
+apply (rule_tac [2] nat_case_dist [symmetric], simp_all)
+done
+
+
+lemma list_all_imp:
+ "[| !x. P x --> Q x; (Alls x:xs. P(x)) |] ==> (Alls x:xs. Q(x))"
+by (simp add: list_all_mem_conv)
+
+
+(** The functional "map" and the generalized functionals **)
+
+lemma Abs_Rep_map:
+ "(!!x. f(x): sexp) ==>
+ Abs_map g (Rep_map f xs) = map (%t. g(f(t))) xs"
+apply (induct_tac "xs" rule: list_induct)
+apply (simp_all add: Rep_map_type list_sexp [THEN subsetD])
+done
+
+
+(** Additional mapping lemmas **)
+
+lemma map_ident [simp]: "map(%x. x)(xs) = xs"
+by (induct_tac "xs" rule: list_induct, simp_all)
+
+lemma map_append [simp]: "map f (xs@ys) = map f xs @ map f ys"
+by (induct_tac "xs" rule: list_induct, simp_all)
+
+lemma map_compose: "map(f o g)(xs) = map f (map g xs)"
+apply (simp add: o_def)
+apply (induct_tac "xs" rule: list_induct, simp_all)
+done
+
+
+lemma mem_map_aux1 [rule_format]:
+ "x mem (map f q) --> (\<exists>y. y mem q & x = f y)"
+by (induct_tac "q" rule: list_induct, simp_all, blast)
+
+lemma mem_map_aux2 [rule_format]:
+ "(\<exists>y. y mem q & x = f y) --> x mem (map f q)"
+by (induct_tac "q" rule: list_induct, auto)
+
+lemma mem_map: "x mem (map f q) = (\<exists>y. y mem q & x = f y)"
+apply (rule iffI)
+apply (erule mem_map_aux1)
+apply (erule mem_map_aux2)
+done
+
+lemma hd_append [rule_format]: "A ~= [] --> hd(A @ B) = hd(A)"
+by (induct_tac "A" rule: list_induct, auto)
+
+lemma tl_append [rule_format]: "A ~= [] --> tl(A @ B) = tl(A) @ B"
+by (induct_tac "A" rule: list_induct, auto)
+
+
+(** take **)
+
+lemma take_Suc1 [simp]: "take [] (Suc x) = []"
+by simp
+
+lemma take_Suc2 [simp]: "take(a#xs)(Suc x) = a#take xs x"
+by simp
+
+
+(** drop **)
+
+lemma drop_0 [simp]: "drop xs 0 = xs"
+by (simp add: drop_def)
+
+lemma drop_Suc1 [simp]: "drop [] (Suc x) = []"
+apply (simp add: drop_def)
+apply (induct_tac "x", auto)
+done
+
+lemma drop_Suc2 [simp]: "drop(a#xs)(Suc x) = drop xs x"
+by (simp add: drop_def)
+
+
+(** copy **)
+
+lemma copy_0 [simp]: "copy x 0 = []"
+by (simp add: copy_def)
+
+lemma copy_Suc [simp]: "copy x (Suc y) = x # copy x y"
+by (simp add: copy_def)
+
+
+(** fold **)
+
+lemma foldl_Nil [simp]: "foldl f a [] = a"
+by (simp add: foldl_def)
+
+lemma foldl_Cons [simp]: "foldl f a(x#xs) = foldl f (f a x) xs"
+by (simp add: foldl_def)
+
+lemma foldr_Nil [simp]: "foldr f a [] = a"
+by (simp add: foldr_def)
+
+lemma foldr_Cons [simp]: "foldr f z(x#xs) = f x (foldr f z xs)"
+by (simp add: foldr_def)
+
+
+(** flat **)
+
+lemma flat_Nil [simp]: "flat [] = []"
+by (simp add: flat_def)
+
+lemma flat_Cons [simp]: "flat (x # xs) = x @ flat xs"
+by (simp add: flat_def)
+
+(** rev **)
+
+lemma rev_Nil [simp]: "rev [] = []"
+by (simp add: rev_def)
+
+lemma rev_Cons [simp]: "rev (x # xs) = rev xs @ [x]"
+by (simp add: rev_def)
+
+
+(** zip **)
+
+lemma zipWith_Cons_Cons [simp]:
+ "zipWith f (a#as,b#bs) = f(a,b) # zipWith f (as,bs)"
+by (simp add: zipWith_def)
+
+lemma zipWith_Nil_Nil [simp]: "zipWith f ([],[]) = []"
+by (simp add: zipWith_def)
+
+
+lemma zipWith_Cons_Nil [simp]: "zipWith f (x,[]) = []"
+apply (simp add: zipWith_def)
+apply (induct_tac "x" rule: list_induct, simp_all)
+done
+
+
+lemma zipWith_Nil_Cons [simp]: "zipWith f ([],x) = []"
+by (simp add: zipWith_def)
+
+lemma unzip_Nil [simp]: "unzip [] = ([],[])"
+by (simp add: unzip_def)
+
+
+
+(** SOME LIST THEOREMS **)
+
+(* SQUIGGOL LEMMAS *)
+
+lemma map_compose_ext: "map(f o g) = ((map f) o (map g))"
+apply (simp add: o_def)
+apply (rule ext)
+apply (simp add: map_compose [symmetric] o_def)
+done
+
+lemma map_flat: "map f (flat S) = flat(map (map f) S)"
+by (induct_tac "S" rule: list_induct, simp_all)
+
+lemma list_all_map_eq: "(Alls u:xs. f(u) = g(u)) --> map f xs = map g xs"
+by (induct_tac "xs" rule: list_induct, simp_all)
+
+lemma filter_map_d: "filter p (map f xs) = map f (filter(p o f)(xs))"
+by (induct_tac "xs" rule: list_induct, simp_all)
+
+lemma filter_compose: "filter p (filter q xs) = filter(%x. p x & q x) xs"
+by (induct_tac "xs" rule: list_induct, simp_all)
+
+(* "filter(p, filter(q,xs)) = filter(q, filter(p,xs))",
+ "filter(p, filter(p,xs)) = filter(p,xs)" BIRD's thms.*)
+
+lemma filter_append [rule_format, simp]:
+ "\<forall>B. filter p (A @ B) = (filter p A @ filter p B)"
+by (induct_tac "A" rule: list_induct, simp_all)
+
+
+(* inits(xs) == map(fst,splits(xs)),
+
+ splits([]) = []
+ splits(a # xs) = <[],xs> @ map(%x. <a # fst(x),snd(x)>, splits(xs))
+ (x @ y = z) = <x,y> mem splits(z)
+ x mem xs & y mem ys = <x,y> mem diag(xs,ys) *)
+
+lemma length_append: "length(xs@ys) = length(xs)+length(ys)"
+by (induct_tac "xs" rule: list_induct, simp_all)
+
+lemma length_map: "length(map f xs) = length(xs)"
+by (induct_tac "xs" rule: list_induct, simp_all)
+
+
+lemma take_Nil [simp]: "take [] n = []"
+by (induct_tac "n", simp_all)
+
+lemma take_take_eq [simp]: "\<forall>n. take (take xs n) n = take xs n"
+apply (induct_tac "xs" rule: list_induct, simp_all)
+apply (rule allI)
+apply (induct_tac "n", auto)
+done
+
+lemma take_take_Suc_eq1 [rule_format]:
+ "\<forall>n. take (take xs(Suc(n+m))) n = take xs n"
+apply (induct_tac "xs" rule: list_induct, simp_all)
+apply (rule allI)
+apply (induct_tac "n", auto)
+done
+
+declare take_Suc [simp del]
+
+lemma take_take_1: "take (take xs (n+m)) n = take xs n"
+apply (induct_tac "m")
+apply (simp_all add: take_take_Suc_eq1)
+done
+
+lemma take_take_Suc_eq2 [rule_format]:
+ "\<forall>n. take (take xs n)(Suc(n+m)) = take xs n"
+apply (induct_tac "xs" rule: list_induct, simp_all)
+apply (rule allI)
+apply (induct_tac "n", auto)
+done
+
+lemma take_take_2: "take(take xs n)(n+m) = take xs n"
+apply (induct_tac "m")
+apply (simp_all add: take_take_Suc_eq2)
+done
+
+(* length(take(xs,n)) = min(n, length(xs)) *)
+(* length(drop(xs,n)) = length(xs) - n *)
+
+lemma drop_Nil [simp]: "drop [] n = []"
+by (induct_tac "n", auto)
+
+lemma drop_drop [rule_format]: "\<forall>xs. drop (drop xs m) n = drop xs(m+n)"
+apply (induct_tac "m", auto)
+apply (induct_tac "xs" rule: list_induct, auto)
+done
+
+lemma take_drop [rule_format]: "\<forall>xs. (take xs n) @ (drop xs n) = xs"
+apply (induct_tac "n", auto)
+apply (induct_tac "xs" rule: list_induct, auto)
+done
+
+lemma copy_copy: "copy x n @ copy x m = copy x (n+m)"
+by (induct_tac "n", auto)
+
+lemma length_copy: "length(copy x n) = n"
+by (induct_tac "n", auto)
+
+lemma length_take [rule_format, simp]:
+ "\<forall>xs. length(take xs n) = min (length xs) n"
+apply (induct_tac "n")
+ apply auto
+apply (induct_tac "xs" rule: list_induct)
+ apply auto
+done
+
+lemma length_take_drop: "length(take A k) + length(drop A k) = length(A)"
+by (simp only: length_append [symmetric] take_drop)
+
+lemma take_append [rule_format]: "\<forall>A. length(A) = n --> take(A@B) n = A"
+apply (induct_tac "n")
+apply (rule allI)
+apply (rule_tac [2] allI)
+apply (induct_tac "A" rule: list_induct)
+apply (induct_tac [3] "A" rule: list_induct, simp_all)
+done
+
+lemma take_append2 [rule_format]:
+ "\<forall>A. length(A) = n --> take(A@B) (n+k) = A @ take B k"
+apply (induct_tac "n")
+apply (rule allI)
+apply (rule_tac [2] allI)
+apply (induct_tac "A" rule: list_induct)
+apply (induct_tac [3] "A" rule: list_induct, simp_all)
+done
+
+lemma take_map [rule_format]: "\<forall>n. take (map f A) n = map f (take A n)"
+apply (induct_tac "A" rule: list_induct, simp_all)
+apply (rule allI)
+apply (induct_tac "n", simp_all)
+done
+
+lemma drop_append [rule_format]: "\<forall>A. length(A) = n --> drop(A@B)n = B"
+apply (induct_tac "n")
+apply (rule allI)
+apply (rule_tac [2] allI)
+apply (induct_tac "A" rule: list_induct)
+apply (induct_tac [3] "A" rule: list_induct, simp_all)
+done
+
+lemma drop_append2 [rule_format]:
+ "\<forall>A. length(A) = n --> drop(A@B)(n+k) = drop B k"
+apply (induct_tac "n")
+apply (rule allI)
+apply (rule_tac [2] allI)
+apply (induct_tac "A" rule: list_induct)
+apply (induct_tac [3] "A" rule: list_induct, simp_all)
+done
+
+
+lemma drop_all [rule_format]: "\<forall>A. length(A) = n --> drop A n = []"
+apply (induct_tac "n")
+apply (rule allI)
+apply (rule_tac [2] allI)
+apply (induct_tac "A" rule: list_induct)
+apply (induct_tac [3] "A" rule: list_induct, auto)
+done
+
+lemma drop_map [rule_format]: "\<forall>n. drop (map f A) n = map f (drop A n)"
+apply (induct_tac "A" rule: list_induct, simp_all)
+apply (rule allI)
+apply (induct_tac "n", simp_all)
+done
+
+lemma take_all [rule_format]: "\<forall>A. length(A) = n --> take A n = A"
+apply (induct_tac "n")
+apply (rule allI)
+apply (rule_tac [2] allI)
+apply (induct_tac "A" rule: list_induct)
+apply (induct_tac [3] "A" rule: list_induct, auto)
+done
+
+lemma foldl_single: "foldl f a [b] = f a b"
+by simp_all
+
+lemma foldl_append [rule_format, simp]:
+ "\<forall>a. foldl f a (A @ B) = foldl f (foldl f a A) B"
+by (induct_tac "A" rule: list_induct, simp_all)
+
+lemma foldl_map [rule_format]:
+ "\<forall>e. foldl f e (map g S) = foldl (%x y. f x (g y)) e S"
+by (induct_tac "S" rule: list_induct, simp_all)
+
+lemma foldl_neutr_distr [rule_format]:
+ assumes r_neutr: "\<forall>a. f a e = a"
+ and r_neutl: "\<forall>a. f e a = a"
+ and assoc: "\<forall>a b c. f a (f b c) = f(f a b) c"
+ shows "\<forall>y. f y (foldl f e A) = foldl f y A"
+apply (induct_tac "A" rule: list_induct)
+apply (simp_all add: r_neutr r_neutl, clarify)
+apply (erule all_dupE)
+apply (rule trans)
+prefer 2 apply assumption
+apply (simp add: assoc [THEN spec, THEN spec, THEN spec, THEN sym])
+done
+
+lemma foldl_append_sym:
+"[| !a. f a e = a; !a. f e a = a;
+ !a b c. f a (f b c) = f(f a b) c |]
+ ==> foldl f e (A @ B) = f(foldl f e A)(foldl f e B)"
+apply (rule trans)
+apply (rule foldl_append)
+apply (rule sym)
+apply (rule foldl_neutr_distr, auto)
+done
+
+lemma foldr_append [rule_format, simp]:
+ "\<forall>a. foldr f a (A @ B) = foldr f (foldr f a B) A"
+apply (induct_tac "A" rule: list_induct, simp_all)
+done
+
+
+lemma foldr_map [rule_format]: "\<forall>e. foldr f e (map g S) = foldr (f o g) e S"
+apply (simp add: o_def)
+apply (induct_tac "S" rule: list_induct, simp_all)
+done
+
+lemma foldr_Un_eq_UN: "foldr op Un {} S = (UN X: {t. t mem S}.X)"
+by (induct_tac "S" rule: list_induct, auto)
+
+lemma foldr_neutr_distr:
+ "[| !a. f e a = a; !a b c. f a (f b c) = f(f a b) c |]
+ ==> foldr f y S = f (foldr f e S) y"
+by (induct_tac "S" rule: list_induct, auto)
+
+lemma foldr_append2:
+ "[| !a. f e a = a; !a b c. f a (f b c) = f(f a b) c |]
+ ==> foldr f e (A @ B) = f (foldr f e A) (foldr f e B)"
+apply auto
+apply (rule foldr_neutr_distr, auto)
+done
+
+lemma foldr_flat:
+ "[| !a. f e a = a; !a b c. f a (f b c) = f(f a b) c |] ==>
+ foldr f e (flat S) = (foldr f e)(map (foldr f e) S)"
+apply (induct_tac "S" rule: list_induct)
+apply (simp_all del: foldr_append add: foldr_append2)
+done
+
+
+lemma list_all_map: "(Alls x:map f xs .P(x)) = (Alls x:xs.(P o f)(x))"
+by (induct_tac "xs" rule: list_induct, auto)
+
+lemma list_all_and:
+ "(Alls x:xs. P(x)&Q(x)) = ((Alls x:xs. P(x))&(Alls x:xs. Q(x)))"
+by (induct_tac "xs" rule: list_induct, auto)
+
+
+lemma nth_map [rule_format]:
+ "\<forall>i. i < length(A) --> nth i (map f A) = f(nth i A)"
+apply (induct_tac "A" rule: list_induct, simp_all)
+apply (rule allI)
+apply (induct_tac "i", auto)
+done
+
+lemma nth_app_cancel_right [rule_format]:
+ "\<forall>i. i < length(A) --> nth i(A@B) = nth i A"
+apply (induct_tac "A" rule: list_induct, simp_all)
+apply (rule allI)
+apply (induct_tac "i", simp_all)
+done
+
+lemma nth_app_cancel_left [rule_format]:
+ "\<forall>n. n = length(A) --> nth(n+i)(A@B) = nth i B"
+by (induct_tac "A" rule: list_induct, simp_all)
+
+
+(** flat **)
+
+lemma flat_append [simp]: "flat(xs@ys) = flat(xs) @ flat(ys)"
+by (induct_tac "xs" rule: list_induct, auto)
+
+lemma filter_flat: "filter p (flat S) = flat(map (filter p) S)"
+by (induct_tac "S" rule: list_induct, auto)
+
+
+(** rev **)
+
+lemma rev_append [simp]: "rev(xs@ys) = rev(ys) @ rev(xs)"
+by (induct_tac "xs" rule: list_induct, auto)
+
+lemma rev_rev_ident [simp]: "rev(rev l) = l"
+by (induct_tac "l" rule: list_induct, auto)
+
+lemma rev_flat: "rev(flat ls) = flat (map rev (rev ls))"
+by (induct_tac "ls" rule: list_induct, auto)
+
+lemma rev_map_distrib: "rev(map f l) = map f (rev l)"
+by (induct_tac "l" rule: list_induct, auto)
+
+lemma foldl_rev: "foldl f b (rev l) = foldr (%x y. f y x) b l"
+by (induct_tac "l" rule: list_induct, auto)
+
+lemma foldr_rev: "foldr f b (rev l) = foldl (%x y. f y x) b l"
+apply (rule sym)
+apply (rule trans)
+apply (rule_tac [2] foldl_rev, simp)
+done
+
end
--- a/src/HOL/Induct/Sexp.thy Thu Apr 04 16:48:00 2002 +0200
+++ b/src/HOL/Induct/Sexp.thy Thu Apr 04 17:32:52 2002 +0200
@@ -7,35 +7,145 @@
structures by hand.
*)
-Sexp = Datatype_Universe + Inductive +
+theory Sexp = Datatype_Universe + Inductive:
consts
- sexp :: 'a item set
+ sexp :: "'a item set"
+
+inductive sexp
+ intros
+ LeafI: "Leaf(a) \<in> sexp"
+ NumbI: "Numb(i) \<in> sexp"
+ SconsI: "[| M \<in> sexp; N \<in> sexp |] ==> Scons M N \<in> sexp"
+
+constdefs
sexp_case :: "['a=>'b, nat=>'b, ['a item, 'a item]=>'b,
'a item] => 'b"
-
- sexp_rec :: "['a item, 'a=>'b, nat=>'b,
- ['a item, 'a item, 'b, 'b]=>'b] => 'b"
-
- pred_sexp :: "('a item * 'a item)set"
-
-inductive sexp
- intrs
- LeafI "Leaf(a): sexp"
- NumbI "Numb(i): sexp"
- SconsI "[| M: sexp; N: sexp |] ==> Scons M N : sexp"
-
-defs
-
- sexp_case_def
"sexp_case c d e M == THE z. (EX x. M=Leaf(x) & z=c(x))
| (EX k. M=Numb(k) & z=d(k))
| (EX N1 N2. M = Scons N1 N2 & z=e N1 N2)"
- pred_sexp_def
- "pred_sexp == UN M: sexp. UN N: sexp. {(M, Scons M N), (N, Scons M N)}"
+ pred_sexp :: "('a item * 'a item)set"
+ "pred_sexp == \<Union>M \<in> sexp. \<Union>N \<in> sexp. {(M, Scons M N), (N, Scons M N)}"
- sexp_rec_def
+ sexp_rec :: "['a item, 'a=>'b, nat=>'b,
+ ['a item, 'a item, 'b, 'b]=>'b] => 'b"
"sexp_rec M c d e == wfrec pred_sexp
(%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2))) M"
+
+
+(** sexp_case **)
+
+lemma sexp_case_Leaf [simp]: "sexp_case c d e (Leaf a) = c(a)"
+by (simp add: sexp_case_def, blast)
+
+lemma sexp_case_Numb [simp]: "sexp_case c d e (Numb k) = d(k)"
+by (simp add: sexp_case_def, blast)
+
+lemma sexp_case_Scons [simp]: "sexp_case c d e (Scons M N) = e M N"
+by (simp add: sexp_case_def)
+
+
+
+(** Introduction rules for sexp constructors **)
+
+lemma sexp_In0I: "M \<in> sexp ==> In0(M) \<in> sexp"
+apply (simp add: In0_def)
+apply (erule sexp.NumbI [THEN sexp.SconsI])
+done
+
+lemma sexp_In1I: "M \<in> sexp ==> In1(M) \<in> sexp"
+apply (simp add: In1_def)
+apply (erule sexp.NumbI [THEN sexp.SconsI])
+done
+
+declare sexp.intros [intro,simp]
+
+lemma range_Leaf_subset_sexp: "range(Leaf) <= sexp"
+by blast
+
+lemma Scons_D: "Scons M N \<in> sexp ==> M \<in> sexp & N \<in> sexp"
+apply (erule setup_induction)
+apply (erule sexp.induct, blast+)
+done
+
+(** Introduction rules for 'pred_sexp' **)
+
+lemma pred_sexp_subset_Sigma: "pred_sexp <= sexp <*> sexp"
+by (simp add: pred_sexp_def, blast)
+
+(* (a,b) \<in> pred_sexp^+ ==> a \<in> sexp *)
+lemmas trancl_pred_sexpD1 =
+ pred_sexp_subset_Sigma
+ [THEN trancl_subset_Sigma, THEN subsetD, THEN SigmaD1]
+and trancl_pred_sexpD2 =
+ pred_sexp_subset_Sigma
+ [THEN trancl_subset_Sigma, THEN subsetD, THEN SigmaD2]
+
+lemma pred_sexpI1:
+ "[| M \<in> sexp; N \<in> sexp |] ==> (M, Scons M N) \<in> pred_sexp"
+by (simp add: pred_sexp_def, blast)
+
+lemma pred_sexpI2:
+ "[| M \<in> sexp; N \<in> sexp |] ==> (N, Scons M N) \<in> pred_sexp"
+by (simp add: pred_sexp_def, blast)
+
+(*Combinations involving transitivity and the rules above*)
+lemmas pred_sexp_t1 [simp] = pred_sexpI1 [THEN r_into_trancl]
+and pred_sexp_t2 [simp] = pred_sexpI2 [THEN r_into_trancl]
+
+lemmas pred_sexp_trans1 [simp] = trans_trancl [THEN transD, OF _ pred_sexp_t1]
+and pred_sexp_trans2 [simp] = trans_trancl [THEN transD, OF _ pred_sexp_t2]
+
+(*Proves goals of the form (M,N):pred_sexp^+ provided M,N:sexp*)
+declare cut_apply [simp]
+
+lemma pred_sexpE:
+ "[| p \<in> pred_sexp;
+ !!M N. [| p = (M, Scons M N); M \<in> sexp; N \<in> sexp |] ==> R;
+ !!M N. [| p = (N, Scons M N); M \<in> sexp; N \<in> sexp |] ==> R
+ |] ==> R"
+by (simp add: pred_sexp_def, blast)
+
+lemma wf_pred_sexp: "wf(pred_sexp)"
+apply (rule pred_sexp_subset_Sigma [THEN wfI])
+apply (erule sexp.induct)
+apply (blast elim!: pred_sexpE)+
+done
+
+
+(*** sexp_rec -- by wf recursion on pred_sexp ***)
+
+lemma sexp_rec_unfold_lemma:
+ "(%M. sexp_rec M c d e) ==
+ wfrec pred_sexp (%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2)))"
+by (simp add: sexp_rec_def)
+
+lemmas sexp_rec_unfold = def_wfrec [OF sexp_rec_unfold_lemma wf_pred_sexp]
+
+(* sexp_rec a c d e =
+ sexp_case c d
+ (%N1 N2.
+ e N1 N2 (cut (%M. sexp_rec M c d e) pred_sexp a N1)
+ (cut (%M. sexp_rec M c d e) pred_sexp a N2)) a
+*)
+
+(** conversion rules **)
+
+lemma sexp_rec_Leaf: "sexp_rec (Leaf a) c d h = c(a)"
+apply (subst sexp_rec_unfold)
+apply (rule sexp_case_Leaf)
+done
+
+lemma sexp_rec_Numb: "sexp_rec (Numb k) c d h = d(k)"
+apply (subst sexp_rec_unfold)
+apply (rule sexp_case_Numb)
+done
+
+lemma sexp_rec_Scons: "[| M \<in> sexp; N \<in> sexp |] ==>
+ sexp_rec (Scons M N) c d h = h M N (sexp_rec M c d h) (sexp_rec N c d h)"
+apply (rule sexp_rec_unfold [THEN trans])
+apply (simp add: pred_sexpI1 pred_sexpI2)
+done
+
end