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 |] ==> <M, CONS(M,N)> : 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 |] ==> <N, CONS(M,N)> : 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
     "<CONS(M1,M2), N> : 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,