diff -r d9527f97246e -r 89669c58e506 List.ML --- a/List.ML Thu Aug 25 10:47:33 1994 +0200 +++ b/List.ML Thu Aug 25 11:01:45 1994 +0200 @@ -3,60 +3,43 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge -For List.thy. +Definition of type 'a list by a least fixed point *) open List; -(** the list functional **) - -goalw List.thy [List_Fun_def] "mono(List_Fun(A))"; -by (REPEAT (ares_tac [monoI, subset_refl, usum_mono, uprod_mono] 1)); -val List_Fun_mono = result(); +val list_con_defs = [NIL_def, CONS_def]; -goalw List.thy [List_Fun_def] - "!!A B. A<=B ==> List_Fun(A,Z) <= List_Fun(B,Z)"; -by (REPEAT (ares_tac [subset_refl, usum_mono, uprod_mono] 1)); -val List_Fun_mono2 = result(); - -(*This justifies using List in other recursive type definitions*) -goalw List.thy [List_def] "!!A B. A<=B ==> List(A) <= List(B)"; -by (rtac lfp_mono 1); -by (etac List_Fun_mono2 1); -val List_mono = result(); - -(** Type checking rules -- List creates well-founded sets **) +goal List.thy "list(A) = {Numb(0)} <+> (A <*> list(A))"; +let val rew = rewrite_rule list_con_defs in +by (fast_tac (univ_cs addSIs (equalityI :: map rew list.intrs) + addEs [rew list.elim]) 1) +end; +val list_unfold = result(); -val prems = goalw List.thy [List_def,List_Fun_def] "List(Sexp) <= Sexp"; -by (rtac lfp_lowerbound 1); -by (fast_tac (univ_cs addIs [Sexp_NumbI,Sexp_In0I,Sexp_In1I,Sexp_SconsI]) 1); -val List_Sexp = result(); - -(* A <= Sexp ==> List(A) <= Sexp *) -val List_subset_Sexp = standard - (List_mono RS (List_Sexp RSN (2,subset_trans))); - -(** Induction **) +(*This justifies using list in other recursive type definitions*) +goalw List.thy list.defs "!!A B. A<=B ==> list(A) <= list(B)"; +by (rtac lfp_mono 1); +by (REPEAT (ares_tac basic_monos 1)); +val list_mono = result(); -(*Induction for the set List(A) *) -val major::prems = goalw List.thy [NIL_def,CONS_def] - "[| M: List(A); P(NIL); \ -\ !!M N. [| M: A; N: List(A); P(N) |] ==> P(CONS(M,N)) |] \ -\ ==> P(M)"; -by (rtac (major RS (List_def RS def_induct)) 1); -by (rtac List_Fun_mono 1); -by (rewtac List_Fun_def); -by (fast_tac (set_cs addIs prems addEs [usumE,uprodE]) 1); -val List_induct = result(); +(*Type checking -- list creates well-founded sets*) +goalw List.thy (list_con_defs @ list.defs) "list(sexp) <= sexp"; +by (rtac lfp_lowerbound 1); +by (fast_tac (univ_cs addIs sexp.intrs@[sexp_In0I,sexp_In1I]) 1); +val list_sexp = result(); + +(* A <= sexp ==> list(A) <= sexp *) +val list_subset_sexp = standard ([list_mono, list_sexp] MRS subset_trans); (*Induction for the type 'a list *) val prems = goalw List.thy [Nil_def,Cons_def] "[| P(Nil); \ \ !!x xs. P(xs) ==> P(x # xs) |] ==> P(l)"; -by (rtac (Rep_List_inverse RS subst) 1); (*types force good instantiation*) -by (rtac (Rep_List RS List_induct) 1); +by (rtac (Rep_list_inverse RS subst) 1); (*types force good instantiation*) +by (rtac (Rep_list RS list.induct) 1); by (REPEAT (ares_tac prems 1 - ORELSE eresolve_tac [rangeE, ssubst, Abs_List_inverse RS subst] 1)); + ORELSE eresolve_tac [rangeE, ssubst, Abs_list_inverse RS subst] 1)); val list_induct = result(); (*Perform induction on xs. *) @@ -64,39 +47,21 @@ EVERY [res_inst_tac [("l",a)] list_induct M, rename_last_tac a ["1"] (M+1)]; -(** Introduction rules for List constructors **) - -val List_unfold = rewrite_rule [List_Fun_def] - (List_Fun_mono RS (List_def RS def_lfp_Tarski)); - -(* c : {Numb(0)} <+> A <*> List(A) ==> c : List(A) *) -val ListI = List_unfold RS equalityD2 RS subsetD; - -(* NIL is a List -- this also justifies the type definition*) -goalw List.thy [NIL_def] "NIL: List(A)"; -by (rtac (singletonI RS usum_In0I RS ListI) 1); -val NIL_I = result(); - -goalw List.thy [CONS_def] - "!!a A M. [| a: A; M: List(A) |] ==> CONS(a,M) : List(A)"; -by (REPEAT (ares_tac [uprodI RS usum_In1I RS ListI] 1)); -val CONS_I = result(); - (*** Isomorphisms ***) -goal List.thy "inj(Rep_List)"; +goal List.thy "inj(Rep_list)"; by (rtac inj_inverseI 1); -by (rtac Rep_List_inverse 1); -val inj_Rep_List = result(); +by (rtac Rep_list_inverse 1); +val inj_Rep_list = result(); -goal List.thy "inj_onto(Abs_List,List(range(Leaf)))"; +goal List.thy "inj_onto(Abs_list,list(range(Leaf)))"; by (rtac inj_onto_inverseI 1); -by (etac Abs_List_inverse 1); -val inj_onto_Abs_List = result(); +by (etac Abs_list_inverse 1); +val inj_onto_Abs_list = result(); (** Distinctness of constructors **) -goalw List.thy [NIL_def,CONS_def] "CONS(M,N) ~= NIL"; +goalw List.thy list_con_defs "CONS(M,N) ~= NIL"; by (rtac In1_not_In0 1); val CONS_not_NIL = result(); val NIL_not_CONS = standard (CONS_not_NIL RS not_sym); @@ -105,8 +70,8 @@ val NIL_neq_CONS = sym RS CONS_neq_NIL; goalw List.thy [Nil_def,Cons_def] "x # xs ~= Nil"; -by (rtac (CONS_not_NIL RS (inj_onto_Abs_List RS inj_onto_contraD)) 1); -by (REPEAT (resolve_tac [rangeI, NIL_I, CONS_I, Rep_List] 1)); +by (rtac (CONS_not_NIL RS (inj_onto_Abs_list RS inj_onto_contraD)) 1); +by (REPEAT (resolve_tac (list.intrs @ [rangeI, Rep_list]) 1)); val Cons_not_Nil = result(); val Nil_not_Cons = standard (Cons_not_Nil RS not_sym); @@ -123,37 +88,37 @@ val CONS_inject = standard (CONS_CONS_eq RS iffD1 RS conjE); (*For reasoning about abstract list constructors*) -val List_cs = set_cs addIs [Rep_List, NIL_I, CONS_I] +val list_cs = set_cs addIs [Rep_list] @ list.intrs addSEs [CONS_neq_NIL,NIL_neq_CONS,CONS_inject] - addSDs [inj_onto_Abs_List RS inj_ontoD, - inj_Rep_List RS injD, Leaf_inject]; + addSDs [inj_onto_Abs_list RS inj_ontoD, + inj_Rep_list RS injD, Leaf_inject]; goalw List.thy [Cons_def] "(x#xs=y#ys) = (x=y & xs=ys)"; -by (fast_tac List_cs 1); +by (fast_tac list_cs 1); val Cons_Cons_eq = result(); val Cons_inject = standard (Cons_Cons_eq RS iffD1 RS conjE); -val [major] = goal List.thy "CONS(M,N): List(A) ==> M: A & N: List(A)"; +val [major] = goal List.thy "CONS(M,N): list(A) ==> M: A & N: list(A)"; by (rtac (major RS setup_induction) 1); -by (etac List_induct 1); -by (ALLGOALS (fast_tac List_cs)); +by (etac list.induct 1); +by (ALLGOALS (fast_tac list_cs)); val CONS_D = result(); val prems = goalw List.thy [CONS_def,In1_def] - "CONS(M,N): Sexp ==> M: Sexp & N: Sexp"; + "CONS(M,N): sexp ==> M: sexp & N: sexp"; by (cut_facts_tac prems 1); by (fast_tac (set_cs addSDs [Scons_D]) 1); -val Sexp_CONS_D = result(); +val sexp_CONS_D = result(); (*Basic ss with constructors and their freeness*) val list_free_simps = [Cons_not_Nil, Nil_not_Cons, Cons_Cons_eq, - CONS_not_NIL, NIL_not_CONS, CONS_CONS_eq, - NIL_I, CONS_I]; + CONS_not_NIL, NIL_not_CONS, CONS_CONS_eq] + @ list.intrs; val list_free_ss = HOL_ss addsimps list_free_simps; -goal List.thy "!!N. N: List(A) ==> !M. N ~= CONS(M,N)"; -by (etac List_induct 1); +goal List.thy "!!N. N: list(A) ==> !M. N ~= CONS(M,N)"; +by (etac list.induct 1); by (ALLGOALS (asm_simp_tac list_free_ss)); val not_CONS_self = result(); @@ -180,34 +145,35 @@ by (simp_tac (HOL_ss addsimps [Split,Case_In1]) 1); val List_case_CONS = result(); -(*** List_rec -- by wf recursion on pred_Sexp ***) +(*** 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. *) -(* The trancl(pred_sexp) is essential because pred_Sexp_CONS_I1,2 would not - hold if pred_Sexp^+ were changed to pred_Sexp. *) +val List_rec_unfold = [List_rec_def, wf_pred_sexp RS wf_trancl] MRS def_wfrec + |> standard; -val List_rec_unfold = wf_pred_Sexp RS wf_trancl RS (List_rec_def RS def_wfrec); - -(** pred_Sexp lemmas **) +(** pred_sexp lemmas **) goalw List.thy [CONS_def,In1_def] - "!!M. [| M: Sexp; N: Sexp |] ==> : pred_Sexp^+"; -by (asm_simp_tac pred_Sexp_ss 1); -val pred_Sexp_CONS_I1 = result(); + "!!M. [| M: sexp; N: sexp |] ==> : pred_sexp^+"; +by (asm_simp_tac pred_sexp_ss 1); +val pred_sexp_CONS_I1 = result(); goalw List.thy [CONS_def,In1_def] - "!!M. [| M: Sexp; N: Sexp |] ==> : pred_Sexp^+"; -by (asm_simp_tac pred_Sexp_ss 1); -val pred_Sexp_CONS_I2 = result(); + "!!M. [| M: sexp; N: sexp |] ==> : pred_sexp^+"; +by (asm_simp_tac pred_sexp_ss 1); +val pred_sexp_CONS_I2 = result(); val [prem] = goal List.thy - " : pred_Sexp^+ ==> \ -\ : pred_Sexp^+ & : pred_Sexp^+"; -by (rtac (prem RS (pred_Sexp_subset_Sigma RS trancl_subset_Sigma RS + " : pred_sexp^+ ==> \ +\ : pred_sexp^+ & : pred_sexp^+"; +by (rtac (prem RS (pred_sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaE2)) 1); -by (etac (Sexp_CONS_D RS conjE) 1); -by (REPEAT (ares_tac [conjI, pred_Sexp_CONS_I1, pred_Sexp_CONS_I2, +by (etac (sexp_CONS_D RS conjE) 1); +by (REPEAT (ares_tac [conjI, pred_sexp_CONS_I1, pred_sexp_CONS_I2, prem RSN (2, trans_trancl RS transD)] 1)); -val pred_Sexp_CONS_D = result(); +val pred_sexp_CONS_D = result(); (** Conversion rules for List_rec **) @@ -216,24 +182,25 @@ by (simp_tac (HOL_ss addsimps [List_case_NIL]) 1); val List_rec_NIL = result(); -goal List.thy "!!M. [| M: Sexp; N: Sexp |] ==> \ +goal List.thy "!!M. [| M: sexp; N: sexp |] ==> \ \ List_rec(CONS(M,N), c, h) = h(M, N, List_rec(N,c,h))"; by (rtac (List_rec_unfold RS trans) 1); by (asm_simp_tac - (HOL_ss addsimps [List_case_CONS, CONS_I, pred_Sexp_CONS_I2, cut_apply])1); + (HOL_ss addsimps [List_case_CONS, list.CONS_I, pred_sexp_CONS_I2, + cut_apply])1); val List_rec_CONS = result(); (*** list_rec -- by List_rec ***) -val Rep_List_in_Sexp = - [range_Leaf_subset_Sexp RS List_subset_Sexp, Rep_List] MRS subsetD; +val Rep_list_in_sexp = + [range_Leaf_subset_sexp RS list_subset_sexp, Rep_list] MRS subsetD; local val list_rec_simps = list_free_simps @ [List_rec_NIL, List_rec_CONS, - Abs_List_inverse, Rep_List_inverse, - Rep_List, rangeI, inj_Leaf, Inv_f_f, - Sexp_LeafI, Rep_List_in_Sexp] + Abs_list_inverse, Rep_list_inverse, + Rep_list, rangeI, inj_Leaf, Inv_f_f, + sexp.LeafI, Rep_list_in_sexp] in val list_rec_Nil = prove_goalw List.thy [list_rec_def, Nil_def] "list_rec(Nil,c,h) = c" @@ -250,16 +217,16 @@ (*Type checking. Useful?*) -val major::A_subset_Sexp::prems = goal List.thy - "[| M: List(A); \ -\ A<=Sexp; \ +val major::A_subset_sexp::prems = goal List.thy + "[| 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 node set)"; -val Sexp_ListA_I = A_subset_Sexp RS List_subset_Sexp RS subsetD; -val Sexp_A_I = A_subset_Sexp RS subsetD; -by (rtac (major RS List_induct) 1); -by (ALLGOALS(asm_simp_tac (list_ss addsimps ([Sexp_A_I,Sexp_ListA_I]@prems)))); +\ !!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)"; +val sexp_ListA_I = A_subset_sexp RS list_subset_sexp RS subsetD; +val sexp_A_I = A_subset_sexp RS subsetD; +by (rtac (major RS list.induct) 1); +by (ALLGOALS(asm_simp_tac (list_ss addsimps ([sexp_A_I,sexp_ListA_I]@prems)))); val List_rec_type = result(); (** Generalized map functionals **) @@ -273,7 +240,7 @@ by (rtac list_rec_Cons 1); val Rep_map_Cons = result(); -goalw List.thy [Rep_map_def] "!!f. (!!x. f(x): A) ==> Rep_map(f,xs): List(A)"; +goalw List.thy [Rep_map_def] "!!f. (!!x. f(x): A) ==> Rep_map(f,xs): list(A)"; by (rtac list_induct 1); by(ALLGOALS(asm_simp_tac list_ss)); val Rep_map_type = result(); @@ -283,7 +250,7 @@ val Abs_map_NIL = result(); val prems = goalw List.thy [Abs_map_def] - "[| M: Sexp; N: Sexp |] ==> \ + "[| M: sexp; N: sexp |] ==> \ \ Abs_map(g, CONS(M,N)) = g(M) # Abs_map(g,N)"; by (REPEAT (resolve_tac (List_rec_CONS::prems) 1)); val Abs_map_CONS = result(); @@ -380,11 +347,11 @@ map_Nil, map_Cons]; val map_ss = list_free_ss addsimps map_simps; -val [major,A_subset_Sexp,minor] = goal List.thy - "[| M: List(A); A<=Sexp; !!z. z: A ==> f(g(z)) = z |] \ +val [major,A_subset_sexp,minor] = goal List.thy + "[| M: list(A); A<=sexp; !!z. z: A ==> f(g(z)) = z |] \ \ ==> Rep_map(f, Abs_map(g,M)) = M"; -by (rtac (major RS List_induct) 1); -by (ALLGOALS (asm_simp_tac(map_ss addsimps [Sexp_A_I,Sexp_ListA_I,minor]))); +by (rtac (major RS list.induct) 1); +by (ALLGOALS (asm_simp_tac(map_ss addsimps [sexp_A_I,sexp_ListA_I,minor]))); val Abs_map_inverse = result(); (*Rep_map_inverse is obtained via Abs_Rep_map and map_ident*) @@ -417,11 +384,11 @@ by (ALLGOALS (asm_simp_tac map_ss)); val map_compose = result(); -goal List.thy "!!f. (!!x. f(x): Sexp) ==> \ +goal List.thy "!!f. (!!x. f(x): sexp) ==> \ \ Abs_map(g, Rep_map(f,xs)) = map(%t. g(f(t)), xs)"; by (list_ind_tac "xs" 1); by(ALLGOALS(asm_simp_tac(map_ss addsimps - [Rep_map_type,List_Sexp RS subsetD]))); + [Rep_map_type,list_sexp RS subsetD]))); val Abs_Rep_map = result(); val list_ss = list_ss addsimps