diff -r 3a8d722fd3ff -r 16c4ea954511 List.ML --- a/List.ML Fri Nov 11 10:35:03 1994 +0100 +++ b/List.ML Mon Nov 21 17:50:34 1994 +0100 @@ -15,19 +15,19 @@ by (fast_tac (univ_cs addSIs (equalityI :: map rew list.intrs) addEs [rew list.elim]) 1) end; -val list_unfold = result(); +qed "list_unfold"; (*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(); +qed "list_mono"; (*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(); +qed "list_sexp"; (* A <= sexp ==> list(A) <= sexp *) val list_subset_sexp = standard ([list_mono, list_sexp] MRS subset_trans); @@ -40,7 +40,7 @@ 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)); -val list_induct = result(); +qed "list_induct"; (*Perform induction on xs. *) fun list_ind_tac a M = @@ -52,18 +52,18 @@ goal List.thy "inj(Rep_list)"; by (rtac inj_inverseI 1); by (rtac Rep_list_inverse 1); -val inj_Rep_list = result(); +qed "inj_Rep_list"; 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(); +qed "inj_onto_Abs_list"; (** Distinctness of constructors **) goalw List.thy list_con_defs "CONS(M,N) ~= NIL"; by (rtac In1_not_In0 1); -val CONS_not_NIL = result(); +qed "CONS_not_NIL"; val NIL_not_CONS = standard (CONS_not_NIL RS not_sym); val CONS_neq_NIL = standard (CONS_not_NIL RS notE); @@ -72,7 +72,7 @@ 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 (list.intrs @ [rangeI, Rep_list]) 1)); -val Cons_not_Nil = result(); +qed "Cons_not_Nil"; val Nil_not_Cons = standard (Cons_not_Nil RS not_sym); @@ -83,7 +83,7 @@ goalw List.thy [CONS_def] "(CONS(K,M)=CONS(L,N)) = (K=L & M=N)"; by (fast_tac (HOL_cs addSEs [Scons_inject, make_elim In1_inject]) 1); -val CONS_CONS_eq = result(); +qed "CONS_CONS_eq"; val CONS_inject = standard (CONS_CONS_eq RS iffD1 RS conjE); @@ -95,20 +95,20 @@ goalw List.thy [Cons_def] "(x#xs=y#ys) = (x=y & xs=ys)"; by (fast_tac list_cs 1); -val Cons_Cons_eq = result(); +qed "Cons_Cons_eq"; 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)"; by (rtac (major RS setup_induction) 1); by (etac list.induct 1); by (ALLGOALS (fast_tac list_cs)); -val CONS_D = result(); +qed "CONS_D"; val prems = goalw List.thy [CONS_def,In1_def] "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(); +qed "sexp_CONS_D"; (*Basic ss with constructors and their freeness*) @@ -120,12 +120,12 @@ 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(); +qed "not_CONS_self"; goal List.thy "!x. l ~= x#l"; by (list_ind_tac "l" 1); by (ALLGOALS (asm_simp_tac list_free_ss)); -val not_Cons_self = result(); +qed "not_Cons_self"; goal List.thy "(xs ~= []) = (? y ys. xs = y#ys)"; @@ -133,17 +133,17 @@ by(simp_tac list_free_ss 1); by(asm_simp_tac list_free_ss 1); by(REPEAT(resolve_tac [exI,refl,conjI] 1)); -val neq_Nil_conv = result(); +qed "neq_Nil_conv"; (** Conversion rules for List_case: case analysis operator **) goalw List.thy [List_case_def,NIL_def] "List_case(c, h, NIL) = c"; by (rtac Case_In0 1); -val List_case_NIL = result(); +qed "List_case_NIL"; goalw List.thy [List_case_def,CONS_def] "List_case(c, h, CONS(M,N)) = h(M,N)"; by (simp_tac (HOL_ss addsimps [Split,Case_In1]) 1); -val List_case_CONS = result(); +qed "List_case_CONS"; (*** List_rec -- by wf recursion on pred_sexp ***) @@ -158,12 +158,12 @@ 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(); +qed "pred_sexp_CONS_I1"; 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(); +qed "pred_sexp_CONS_I2"; val [prem] = goal List.thy " : pred_sexp^+ ==> \ @@ -173,14 +173,14 @@ 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(); +qed "pred_sexp_CONS_D"; (** Conversion rules for List_rec **) goal List.thy "List_rec(NIL,c,h) = c"; by (rtac (List_rec_unfold RS trans) 1); by (simp_tac (HOL_ss addsimps [List_case_NIL]) 1); -val List_rec_NIL = result(); +qed "List_rec_NIL"; goal List.thy "!!M. [| M: sexp; N: sexp |] ==> \ \ List_rec(CONS(M,N), c, h) = h(M, N, List_rec(N,c,h))"; @@ -188,7 +188,7 @@ by (asm_simp_tac (HOL_ss addsimps [List_case_CONS, list.CONS_I, pred_sexp_CONS_I2, cut_apply])1); -val List_rec_CONS = result(); +qed "List_rec_CONS"; (*** list_rec -- by List_rec ***) @@ -227,46 +227,46 @@ 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(); +qed "List_rec_type"; (** Generalized map functionals **) goalw List.thy [Rep_map_def] "Rep_map(f,Nil) = NIL"; by (rtac list_rec_Nil 1); -val Rep_map_Nil = result(); +qed "Rep_map_Nil"; goalw List.thy [Rep_map_def] "Rep_map(f, x#xs) = CONS(f(x), Rep_map(f,xs))"; by (rtac list_rec_Cons 1); -val Rep_map_Cons = result(); +qed "Rep_map_Cons"; 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(); +qed "Rep_map_type"; goalw List.thy [Abs_map_def] "Abs_map(g,NIL) = Nil"; by (rtac List_rec_NIL 1); -val Abs_map_NIL = result(); +qed "Abs_map_NIL"; val prems = goalw List.thy [Abs_map_def] "[| 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(); +qed "Abs_map_CONS"; (*These 2 rules ease the use of primitive recursion. NOTE USE OF == *) val [rew] = goal List.thy "[| !!xs. f(xs) == list_rec(xs,c,h) |] ==> f([]) = c"; by (rewtac rew); by (rtac list_rec_Nil 1); -val def_list_rec_Nil = result(); +qed "def_list_rec_Nil"; val [rew] = goal List.thy "[| !!xs. f(xs) == list_rec(xs,c,h) |] ==> f(x#xs) = h(x,xs,f(xs))"; by (rewtac rew); by (rtac list_rec_Cons 1); -val def_list_rec_Cons = result(); +qed "def_list_rec_Cons"; fun list_recs def = [standard (def RS def_list_rec_Nil), @@ -302,42 +302,42 @@ goal List.thy "(xs@ys)@zs = xs@(ys@zs)"; by(list_ind_tac "xs" 1); by(ALLGOALS(asm_simp_tac list_ss)); -val append_assoc = result(); +qed "append_assoc"; goal List.thy "xs @ [] = xs"; by(list_ind_tac "xs" 1); by(ALLGOALS(asm_simp_tac list_ss)); -val append_Nil2 = result(); +qed "append_Nil2"; (** mem **) goal List.thy "x mem (xs@ys) = (x mem xs | x mem ys)"; by(list_ind_tac "xs" 1); by(ALLGOALS(asm_simp_tac (list_ss setloop (split_tac [expand_if])))); -val mem_append = result(); +qed "mem_append"; goal List.thy "x mem [x:xs.P(x)] = (x mem xs & P(x))"; by(list_ind_tac "xs" 1); by(ALLGOALS(asm_simp_tac (list_ss setloop (split_tac [expand_if])))); -val mem_filter = result(); +qed "mem_filter"; (** list_all **) goal List.thy "(Alls x:xs.True) = True"; by(list_ind_tac "xs" 1); by(ALLGOALS(asm_simp_tac list_ss)); -val list_all_True = result(); +qed "list_all_True"; goal List.thy "list_all(p,xs@ys) = (list_all(p,xs) & list_all(p,ys))"; by(list_ind_tac "xs" 1); by(ALLGOALS(asm_simp_tac list_ss)); -val list_all_conj = result(); +qed "list_all_conj"; goal List.thy "(Alls x:xs.P(x)) = (!x. x mem xs --> P(x))"; by(list_ind_tac "xs" 1); by(ALLGOALS(asm_simp_tac (list_ss setloop (split_tac [expand_if])))); by(fast_tac HOL_cs 1); -val list_all_mem_conv = result(); +qed "list_all_mem_conv"; (** The functional "map" **) @@ -352,7 +352,7 @@ \ ==> 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]))); -val Abs_map_inverse = result(); +qed "Abs_map_inverse"; (*Rep_map_inverse is obtained via Abs_Rep_map and map_ident*) @@ -364,7 +364,7 @@ by(list_ind_tac "xs" 1); by(ALLGOALS(asm_simp_tac list_ss)); by(fast_tac HOL_cs 1); -val expand_list_case = result(); +qed "expand_list_case"; (** Additional mapping lemmas **) @@ -372,24 +372,24 @@ goal List.thy "map(%x.x, xs) = xs"; by (list_ind_tac "xs" 1); by (ALLGOALS (asm_simp_tac map_ss)); -val map_ident = result(); +qed "map_ident"; goal List.thy "map(f, xs@ys) = map(f,xs) @ map(f,ys)"; by (list_ind_tac "xs" 1); by (ALLGOALS (asm_simp_tac (map_ss addsimps [append_Nil,append_Cons]))); -val map_append = result(); +qed "map_append"; goalw List.thy [o_def] "map(f o g, xs) = map(f, map(g, xs))"; by (list_ind_tac "xs" 1); by (ALLGOALS (asm_simp_tac map_ss)); -val map_compose = result(); +qed "map_compose"; 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]))); -val Abs_Rep_map = result(); +qed "Abs_Rep_map"; val list_ss = list_ss addsimps [mem_append, mem_filter, append_assoc, append_Nil2, map_ident,