--- a/src/ZF/Cardinal.ML Wed Dec 14 10:26:30 1994 +0100
+++ b/src/ZF/Cardinal.ML Wed Dec 14 11:41:49 1994 +0100
@@ -219,7 +219,7 @@
goal Cardinal.thy "!!K. Card(K) ==> K le |K|";
by (asm_simp_tac (ZF_ss addsimps [le_refl, Card_is_Ord, Card_cardinal_eq]) 1);
-val Card_cardinal_le = result();
+qed "Card_cardinal_le";
goalw Cardinal.thy [cardinal_def] "Ord(|A|)";
by (rtac Ord_Least 1);
--- a/src/ZF/CardinalArith.ML Wed Dec 14 10:26:30 1994 +0100
+++ b/src/ZF/CardinalArith.ML Wed Dec 14 11:41:49 1994 +0100
@@ -96,7 +96,7 @@
goalw CardinalArith.thy [lepoll_def, inj_def] "A lepoll A+B";
by (res_inst_tac [("x", "lam x:A. Inl(x)")] exI 1);
by (asm_simp_tac (sum_ss addsimps [lam_type]) 1);
-val sum_lepoll_self = result();
+qed "sum_lepoll_self";
(*Could probably weaken the premises to well_ord(K,r), or removing using AC*)
goalw CardinalArith.thy [cadd_def]
@@ -104,7 +104,7 @@
by (rtac ([Card_cardinal_le, well_ord_lepoll_imp_Card_le] MRS le_trans) 1);
by (rtac sum_lepoll_self 3);
by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel, Card_is_Ord] 1));
-val cadd_le_self = result();
+qed "cadd_le_self";
(** Monotonicity of addition **)
@@ -119,7 +119,7 @@
by (typechk_tac ([inj_is_fun,case_type, InlI, InrI] @ ZF_typechecks));
by (eresolve_tac [sumE] 1);
by (ALLGOALS (asm_simp_tac (sum_ss addsimps [left_inverse])));
-val sum_lepoll_mono = result();
+qed "sum_lepoll_mono";
goalw CardinalArith.thy [cadd_def]
"!!K. [| K' le K; L' le L |] ==> (K' |+| L') le (K |+| L)";
@@ -127,7 +127,7 @@
by (resolve_tac [well_ord_lepoll_imp_Card_le] 1);
by (REPEAT (ares_tac [sum_lepoll_mono, subset_imp_lepoll] 2));
by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel] 1));
-val cadd_le_mono = result();
+qed "cadd_le_mono";
(** Addition of finite cardinals is "ordinary" addition **)
@@ -262,7 +262,7 @@
goalw CardinalArith.thy [lepoll_def, inj_def] "!!b. b: B ==> A lepoll A*B";
by (res_inst_tac [("x", "lam x:A. <x,b>")] exI 1);
by (asm_simp_tac (ZF_ss addsimps [lam_type]) 1);
-val prod_lepoll_self = result();
+qed "prod_lepoll_self";
(*Could probably weaken the premises to well_ord(K,r), or removing using AC*)
goalw CardinalArith.thy [cmult_def]
@@ -270,7 +270,7 @@
by (rtac ([Card_cardinal_le, well_ord_lepoll_imp_Card_le] MRS le_trans) 1);
by (rtac prod_lepoll_self 3);
by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel, Card_is_Ord, ltD] 1));
-val cmult_le_self = result();
+qed "cmult_le_self";
(** Monotonicity of multiplication **)
@@ -284,7 +284,7 @@
by (typechk_tac (inj_is_fun::ZF_typechecks));
by (eresolve_tac [SigmaE] 1);
by (asm_simp_tac (ZF_ss addsimps [left_inverse]) 1);
-val prod_lepoll_mono = result();
+qed "prod_lepoll_mono";
goalw CardinalArith.thy [cmult_def]
"!!K. [| K' le K; L' le L |] ==> (K' |*| L') le (K |*| L)";
@@ -292,7 +292,7 @@
by (resolve_tac [well_ord_lepoll_imp_Card_le] 1);
by (REPEAT (ares_tac [prod_lepoll_mono, subset_imp_lepoll] 2));
by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel] 1));
-val cmult_le_mono = result();
+qed "cmult_le_mono";
(*** Multiplication of finite cardinals is "ordinary" multiplication ***)
@@ -329,7 +329,7 @@
by (asm_simp_tac
(ZF_ss addsimps [Ord_0, Ord_succ, cmult_0, cmult_succ_lemma, Card_is_Ord,
read_instantiate [("j","0")] cadd_commute, cadd_0]) 1);
-val cmult_2 = result();
+qed "cmult_2";
(*** Infinite Cardinals are Limit Ordinals ***)
@@ -591,7 +591,7 @@
by (forward_tac [InfCard_is_Card RS Card_is_Ord RS le_refl] 1);
by (resolve_tac [cmult_le_mono RS le_trans] 1 THEN REPEAT (assume_tac 1));
by (asm_simp_tac (ZF_ss addsimps [InfCard_csquare_eq]) 1);
-val InfCard_le_cmult_eq = result();
+qed "InfCard_le_cmult_eq";
(*Corollary 10.13 (1), for cardinal multiplication*)
goal CardinalArith.thy
@@ -604,7 +604,7 @@
(asm_simp_tac
(ZF_ss addsimps [InfCard_is_Limit RS Limit_has_0, InfCard_le_cmult_eq,
subset_Un_iff2 RS iffD1, le_imp_subset])));
-val InfCard_cmult_eq = result();
+qed "InfCard_cmult_eq";
(*This proof appear to be the simplest!*)
goal CardinalArith.thy "!!K. InfCard(K) ==> K |+| K = K";
@@ -613,7 +613,7 @@
by (resolve_tac [InfCard_le_cmult_eq] 1);
by (typechk_tac [Ord_0, le_refl, leI]);
by (typechk_tac [InfCard_is_Limit, Limit_has_0, Limit_has_succ]);
-val InfCard_cdouble_eq = result();
+qed "InfCard_cdouble_eq";
(*Corollary 10.13 (1), for cardinal addition*)
goal CardinalArith.thy "!!K. [| InfCard(K); L le K |] ==> K |+| L = K";
@@ -623,7 +623,7 @@
by (forward_tac [InfCard_is_Card RS Card_is_Ord RS le_refl] 1);
by (resolve_tac [cadd_le_mono RS le_trans] 1 THEN REPEAT (assume_tac 1));
by (asm_simp_tac (ZF_ss addsimps [InfCard_cdouble_eq]) 1);
-val InfCard_le_cadd_eq = result();
+qed "InfCard_le_cadd_eq";
goal CardinalArith.thy
"!!K. [| InfCard(K); InfCard(L) |] ==> K |+| L = K Un L";
@@ -635,7 +635,7 @@
(asm_simp_tac
(ZF_ss addsimps [InfCard_le_cadd_eq,
subset_Un_iff2 RS iffD1, le_imp_subset])));
-val InfCard_cadd_eq = result();
+qed "InfCard_cadd_eq";
(*The other part, Corollary 10.13 (2), refers to the cardinality of the set
of all n-tuples of elements of K. A better version for the Isabelle theory
--- a/src/ZF/Epsilon.ML Wed Dec 14 10:26:30 1994 +0100
+++ b/src/ZF/Epsilon.ML Wed Dec 14 11:41:49 1994 +0100
@@ -28,11 +28,11 @@
qed "Transset_eclose";
(* x : eclose(A) ==> x <= eclose(A) *)
-val eclose_subset =
- standard (rewrite_rule [Transset_def] Transset_eclose RS bspec);
+bind_thm ("eclose_subset",
+ rewrite_rule [Transset_def] Transset_eclose RS bspec);
(* [| A : eclose(B); c : A |] ==> c : eclose(B) *)
-val ecloseD = standard (eclose_subset RS subsetD);
+bind_thm ("ecloseD", eclose_subset RS subsetD);
val arg_in_eclose_sing = arg_subset_eclose RS singleton_subsetD;
val arg_into_eclose_sing = arg_in_eclose_sing RS ecloseD;
@@ -41,7 +41,7 @@
[| a: eclose(A); !!x. [| x: eclose(A); ALL y:x. P(y) |] ==> P(x)
|] ==> P(a)
*)
-val eclose_induct = standard (Transset_eclose RSN (2, Transset_induct));
+bind_thm ("eclose_induct", Transset_eclose RSN (2, Transset_induct));
(*Epsilon induction*)
val prems = goal Epsilon.thy
@@ -118,7 +118,7 @@
(* j : eclose(A) ==> Memrel(eclose(A)) -`` j = j *)
val under_Memrel_eclose = Transset_eclose RS under_Memrel;
-val wfrec_ssubst = standard (wf_Memrel RS wfrec RS ssubst);
+bind_thm ("wfrec_ssubst", wf_Memrel RS wfrec RS ssubst);
val [kmemj,jmemi] = goal Epsilon.thy
"[| k:eclose({j}); j:eclose({i}) |] ==> \
--- a/src/ZF/List.ML Wed Dec 14 10:26:30 1994 +0100
+++ b/src/ZF/List.ML Wed Dec 14 11:41:49 1994 +0100
@@ -47,7 +47,7 @@
qed "list_univ";
(*These two theorems are unused -- useful??*)
-val list_subset_univ = standard ([list_mono, list_univ] MRS subset_trans);
+bind_thm ("list_subset_univ", ([list_mono, list_univ] MRS subset_trans));
goal List.thy "!!l A B. [| l: list(A); A <= univ(B) |] ==> l: univ(B)";
by (REPEAT (ares_tac [list_subset_univ RS subsetD] 1));
@@ -272,7 +272,7 @@
(** theorems about list(Collect(A,P)) -- used in ex/term.ML **)
(* c : list(Collect(B,P)) ==> c : list(B) *)
-val list_CollectD = standard (Collect_subset RS list_mono RS subsetD);
+bind_thm ("list_CollectD", (Collect_subset RS list_mono RS subsetD));
val prems = goal List.thy
"l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)";
@@ -320,7 +320,7 @@
by (ALLGOALS (asm_simp_tac (list_ss addsimps [drop_0,drop_succ_Cons])));
by (fast_tac ZF_cs 1);
qed "drop_length_Cons_lemma";
-val drop_length_Cons = standard (drop_length_Cons_lemma RS spec);
+bind_thm ("drop_length_Cons", (drop_length_Cons_lemma RS spec));
goal List.thy
"!!l. l: list(A) ==> ALL i: length(l). EX z zs. drop(i,l) = Cons(z,zs)";
@@ -339,7 +339,7 @@
by (fast_tac ZF_cs 2);
by (fast_tac (ZF_cs addEs [succ_in_naturalD,length_type]) 1);
qed "drop_length_lemma";
-val drop_length = standard (drop_length_lemma RS bspec);
+bind_thm ("drop_length", (drop_length_lemma RS bspec));
(*** theorems about app ***)
--- a/src/ZF/Order.ML Wed Dec 14 10:26:30 1994 +0100
+++ b/src/ZF/Order.ML Wed Dec 14 11:41:49 1994 +0100
@@ -83,7 +83,7 @@
"!!f. f: ord_iso(A,r,B,s) ==> converse(f): ord_iso(B,s,A,r)";
by (safe_tac ZF_cs);
by (ALLGOALS (asm_full_simp_tac bij_ss));
-val ord_iso_sym = result();
+qed "ord_iso_sym";
val major::premx::premy::prems = goalw Order.thy [linear_def]
"[| linear(A,r); x:A; y:A; \
--- a/src/ZF/OrderArith.ML Wed Dec 14 10:26:30 1994 +0100
+++ b/src/ZF/OrderArith.ML Wed Dec 14 11:41:49 1994 +0100
@@ -58,7 +58,7 @@
by (rtac Collect_subset 1);
qed "radd_type";
-val field_radd = standard (radd_type RS field_rel_subset);
+bind_thm ("field_radd", (radd_type RS field_rel_subset));
(** Linearity **)
@@ -137,7 +137,7 @@
by (rtac Collect_subset 1);
qed "rmult_type";
-val field_rmult = standard (rmult_type RS field_rel_subset);
+bind_thm ("field_rmult", (rmult_type RS field_rel_subset));
(** Linearity **)
@@ -202,7 +202,7 @@
by (rtac Collect_subset 1);
qed "rvimage_type";
-val field_rvimage = standard (rvimage_type RS field_rel_subset);
+bind_thm ("field_rvimage", (rvimage_type RS field_rel_subset));
(** Linearity **)
--- a/src/ZF/OrderType.ML Wed Dec 14 10:26:30 1994 +0100
+++ b/src/ZF/OrderType.ML Wed Dec 14 11:41:49 1994 +0100
@@ -224,7 +224,7 @@
"!!i j. j<i ==> j = pred(i, j, Memrel(i))";
by (asm_simp_tac (ZF_ss addsimps [Memrel_iff]) 1);
by (fast_tac (eq_cs addEs [Ord_trans]) 1);
-val lt_eq_pred = result();
+qed "lt_eq_pred";
goal OrderType.thy
"!!i. [| j<i; f: ord_iso(i,Memrel(i),j,Memrel(j)) \
@@ -239,7 +239,7 @@
by (asm_simp_tac (ZF_ss addsimps [Memrel_iff]) 1);
by (fast_tac (ZF_cs addSEs [bij_is_fun RS apply_type]
addEs [Ord_trans]) 1);
-val Ord_iso_implies_eq_lemma = result();
+qed "Ord_iso_implies_eq_lemma";
(*Kunen's Theorem 7.3 (ii), page 16. Isomorphic ordinals are equal*)
goal OrderType.thy
@@ -247,4 +247,4 @@
\ |] ==> i=j";
by (res_inst_tac [("i","i"),("j","j")] Ord_linear_lt 1);
by (REPEAT (eresolve_tac [asm_rl, ord_iso_sym, Ord_iso_implies_eq_lemma] 1));
-val Ord_iso_implies_eq = result();
+qed "Ord_iso_implies_eq";
--- a/src/ZF/Ordinal.ML Wed Dec 14 10:26:30 1994 +0100
+++ b/src/ZF/Ordinal.ML Wed Dec 14 11:41:49 1994 +0100
@@ -216,7 +216,7 @@
qed "not_lt0";
(* i<0 ==> R *)
-val lt0E = standard (not_lt0 RS notE);
+bind_thm ("lt0E", not_lt0 RS notE);
goal Ordinal.thy "!!i j k. [| i<j; j<k |] ==> i<k";
by (fast_tac (ZF_cs addSIs [ltI] addSEs [ltE, Ord_trans]) 1);
@@ -269,7 +269,7 @@
by (fast_tac (ZF_cs addSIs [Ord_0 RS le_refl] addSEs [leE, lt0E]) 1);
qed "le0_iff";
-val le0D = standard (le0_iff RS iffD1);
+bind_thm ("le0D", le0_iff RS iffD1);
val lt_cs =
ZF_cs addSIs [le_refl, leCI]
@@ -372,7 +372,7 @@
by (trans_ind_tac "j" [] 1);
by (DEPTH_SOLVE (step_tac eq_cs 1 ORELSE Ord_trans_tac 1));
qed "Ord_linear_lemma";
-val Ord_linear = standard (Ord_linear_lemma RS spec RS mp);
+bind_thm ("Ord_linear", Ord_linear_lemma RS spec RS mp);
(*The trichotomy law for ordinals!*)
val ordi::ordj::prems = goalw Ordinal.thy [lt_def]
--- a/src/ZF/Perm.ML Wed Dec 14 10:26:30 1994 +0100
+++ b/src/ZF/Perm.ML Wed Dec 14 11:41:49 1994 +0100
@@ -92,7 +92,7 @@
qed "bij_is_surj";
(* f: bij(A,B) ==> f: A->B *)
-val bij_is_fun = standard (bij_is_inj RS inj_is_fun);
+bind_thm ("bij_is_fun", (bij_is_inj RS inj_is_fun));
val prems = goalw Perm.thy [bij_def]
"[| !!x. x:A ==> c(x): B; \
--- a/src/ZF/QPair.ML Wed Dec 14 10:26:30 1994 +0100
+++ b/src/ZF/QPair.ML Wed Dec 14 11:41:49 1994 +0100
@@ -29,7 +29,7 @@
"<a;b> = <c;d> <-> a=c & b=d"
(fn _=> [rtac sum_equal_iff 1]);
-val QPair_inject = standard (QPair_iff RS iffD1 RS conjE);
+bind_thm ("QPair_inject", (QPair_iff RS iffD1 RS conjE));
qed_goal "QPair_inject1" QPair.thy "<a;b> = <c;d> ==> a=c"
(fn [major]=>
@@ -203,10 +203,10 @@
(*Injection and freeness rules*)
-val QInl_inject = standard (QInl_iff RS iffD1);
-val QInr_inject = standard (QInr_iff RS iffD1);
-val QInl_neq_QInr = standard (QInl_QInr_iff RS iffD1 RS FalseE);
-val QInr_neq_QInl = standard (QInr_QInl_iff RS iffD1 RS FalseE);
+bind_thm ("QInl_inject", (QInl_iff RS iffD1));
+bind_thm ("QInr_inject", (QInr_iff RS iffD1));
+bind_thm ("QInl_neq_QInr", (QInl_QInr_iff RS iffD1 RS FalseE));
+bind_thm ("QInr_neq_QInl", (QInr_QInl_iff RS iffD1 RS FalseE));
val qsum_cs =
qpair_cs addSIs [PartI, QInlI, QInrI]
--- a/src/ZF/QUniv.ML Wed Dec 14 10:26:30 1994 +0100
+++ b/src/ZF/QUniv.ML Wed Dec 14 11:41:49 1994 +0100
@@ -37,7 +37,7 @@
by (rtac univ_eclose_subset_quniv 1);
qed "univ_subset_quniv";
-val univ_into_quniv = standard (univ_subset_quniv RS subsetD);
+bind_thm ("univ_into_quniv", (univ_subset_quniv RS subsetD));
goalw QUniv.thy [quniv_def] "Pow(univ(A)) <= quniv(A)";
by (rtac (arg_subset_eclose RS univ_mono RS Pow_mono) 1);
@@ -46,9 +46,9 @@
val univ_subset_into_quniv = standard
(PowI RS (Pow_univ_subset_quniv RS subsetD));
-val zero_in_quniv = standard (zero_in_univ RS univ_into_quniv);
-val one_in_quniv = standard (one_in_univ RS univ_into_quniv);
-val two_in_quniv = standard (two_in_univ RS univ_into_quniv);
+bind_thm ("zero_in_quniv", (zero_in_univ RS univ_into_quniv));
+bind_thm ("one_in_quniv", (one_in_univ RS univ_into_quniv));
+bind_thm ("two_in_quniv", (two_in_univ RS univ_into_quniv));
val A_subset_quniv = standard
([A_subset_univ, univ_subset_quniv] MRS subset_trans);
@@ -105,7 +105,7 @@
by (REPEAT (ares_tac [conjI,PowI] 1));
qed "quniv_QPair_D";
-val quniv_QPair_E = standard (quniv_QPair_D RS conjE);
+bind_thm ("quniv_QPair_E", (quniv_QPair_D RS conjE));
goal QUniv.thy "<a;b> : quniv(A) <-> a: quniv(A) & b: quniv(A)";
by (REPEAT (ares_tac [iffI, QPair_in_quniv, quniv_QPair_D] 1
@@ -137,12 +137,12 @@
([nat_subset_univ, univ_subset_quniv] MRS subset_trans);
(* n:nat ==> n:quniv(A) *)
-val nat_into_quniv = standard (nat_subset_quniv RS subsetD);
+bind_thm ("nat_into_quniv", (nat_subset_quniv RS subsetD));
val bool_subset_quniv = standard
([bool_subset_univ, univ_subset_quniv] MRS subset_trans);
-val bool_into_quniv = standard (bool_subset_quniv RS subsetD);
+bind_thm ("bool_into_quniv", (bool_subset_quniv RS subsetD));
(**** Properties of Vfrom analogous to the "take-lemma" ****)
@@ -159,7 +159,7 @@
qed "doubleton_in_Vfrom_D";
(*This weaker version says a, b exist at the same level*)
-val Vfrom_doubleton_D = standard (Transset_Vfrom RS Transset_doubleton_D);
+bind_thm ("Vfrom_doubleton_D", (Transset_Vfrom RS Transset_doubleton_D));
(** Using only the weaker theorem would prove <a,b> : Vfrom(X,i)
implies a, b : Vfrom(X,i), which is useless for induction.
--- a/src/ZF/Sum.ML Wed Dec 14 10:26:30 1994 +0100
+++ b/src/ZF/Sum.ML Wed Dec 14 11:41:49 1994 +0100
@@ -85,10 +85,10 @@
(*Injection and freeness rules*)
-val Inl_inject = standard (Inl_iff RS iffD1);
-val Inr_inject = standard (Inr_iff RS iffD1);
-val Inl_neq_Inr = standard (Inl_Inr_iff RS iffD1 RS FalseE);
-val Inr_neq_Inl = standard (Inr_Inl_iff RS iffD1 RS FalseE);
+bind_thm ("Inl_inject", (Inl_iff RS iffD1));
+bind_thm ("Inr_inject", (Inr_iff RS iffD1));
+bind_thm ("Inl_neq_Inr", (Inl_Inr_iff RS iffD1 RS FalseE));
+bind_thm ("Inr_neq_Inl", (Inr_Inl_iff RS iffD1 RS FalseE));
val sum_cs = ZF_cs addSIs [PartI, InlI, InrI]
addSEs [PartE, sumE, Inl_neq_Inr, Inr_neq_Inl]
--- a/src/ZF/Trancl.ML Wed Dec 14 10:26:30 1994 +0100
+++ b/src/ZF/Trancl.ML Wed Dec 14 11:41:49 1994 +0100
@@ -25,7 +25,7 @@
(** The relation rtrancl **)
-val rtrancl_type = standard (rtrancl_def RS def_lfp_subset);
+bind_thm ("rtrancl_type", (rtrancl_def RS def_lfp_subset));
(*Reflexivity of rtrancl*)
val [prem] = goal Trancl.thy "[| a: field(r) |] ==> <a,a> : r^*";
--- a/src/ZF/Univ.ML Wed Dec 14 10:26:30 1994 +0100
+++ b/src/ZF/Univ.ML Wed Dec 14 11:41:49 1994 +0100
@@ -31,7 +31,7 @@
qed "Vfrom_mono_lemma";
(* [| A<=B; i<=x |] ==> Vfrom(A,i) <= Vfrom(B,x) *)
-val Vfrom_mono = standard (Vfrom_mono_lemma RS spec RS mp);
+bind_thm ("Vfrom_mono", (Vfrom_mono_lemma RS spec RS mp));
(** A fundamental equality: Vfrom does not require ordinals! **)
@@ -424,7 +424,7 @@
qed "Vset_rank_imp1";
(* [| Ord(i); x : Vset(i) |] ==> rank(x) < i *)
-val VsetD = standard (Vset_rank_imp1 RS spec RS mp);
+bind_thm ("VsetD", (Vset_rank_imp1 RS spec RS mp));
val [ordi] = goal Univ.thy "Ord(i) ==> ALL b. rank(b) : i --> b : Vset(i)";
by (rtac (ordi RS trans_induct) 1);
@@ -584,7 +584,7 @@
qed "nat_subset_univ";
(* n:nat ==> n:univ(A) *)
-val nat_into_univ = standard (nat_subset_univ RS subsetD);
+bind_thm ("nat_into_univ", (nat_subset_univ RS subsetD));
(** instances for 1 and 2 **)
@@ -601,7 +601,7 @@
by (fast_tac (ZF_cs addSIs [zero_in_univ,one_in_univ]) 1);
qed "bool_subset_univ";
-val bool_into_univ = standard (bool_subset_univ RS subsetD);
+bind_thm ("bool_into_univ", (bool_subset_univ RS subsetD));
(** Closure under disjoint union **)
--- a/src/ZF/WF.ML Wed Dec 14 10:26:30 1994 +0100
+++ b/src/ZF/WF.ML Wed Dec 14 11:41:49 1994 +0100
@@ -200,8 +200,8 @@
(** r-``{a} is the set of everything under a in r **)
-val underI = standard (vimage_singleton_iff RS iffD2);
-val underD = standard (vimage_singleton_iff RS iffD1);
+bind_thm ("underI", (vimage_singleton_iff RS iffD2));
+bind_thm ("underD", (vimage_singleton_iff RS iffD1));
(** is_recfun **)
@@ -238,7 +238,7 @@
by (rewtac restrict_def);
by (asm_simp_tac (wf_super_ss addsimps [vimage_singleton_iff]) 1);
qed "is_recfun_equal_lemma";
-val is_recfun_equal = standard (is_recfun_equal_lemma RS mp RS mp);
+bind_thm ("is_recfun_equal", (is_recfun_equal_lemma RS mp RS mp));
val prems as [wfr,transr,recf,recg,_] = goal WF.thy
"[| wf(r); trans(r); \
--- a/src/ZF/ex/Acc.ML Wed Dec 14 10:26:30 1994 +0100
+++ b/src/ZF/ex/Acc.ML Wed Dec 14 11:41:49 1994 +0100
@@ -18,12 +18,12 @@
val prems = goal Acc.thy
"[| !!b. <b,a>:r ==> b: acc(r); a: field(r) |] ==> a: acc(r)";
by (fast_tac (ZF_cs addIs (prems@acc.intrs)) 1);
-val accI = result();
+qed "accI";
goal Acc.thy "!!a b r. [| b: acc(r); <a,b>: r |] ==> a: acc(r)";
by (etac acc.elim 1);
by (fast_tac ZF_cs 1);
-val acc_downward = result();
+qed "acc_downward";
val [major,indhyp] = goal Acc.thy
"[| a : acc(r); \
@@ -35,13 +35,13 @@
by (resolve_tac acc.intrs 1);
by (assume_tac 2);
be (Collect_subset RS Pow_mono RS subsetD) 1;
-val acc_induct = result();
+qed "acc_induct";
goal Acc.thy "wf[acc(r)](r)";
by (rtac wf_onI2 1);
by (etac acc_induct 1);
by (fast_tac ZF_cs 1);
-val wf_on_acc = result();
+qed "wf_on_acc";
(* field(r) <= acc(r) ==> wf(r) *)
val acc_wfI = wf_on_acc RS wf_on_subset_A RS wf_on_field_imp_wf;
@@ -53,8 +53,8 @@
by (resolve_tac [accI] 1);
by (assume_tac 2);
by (fast_tac ZF_cs 1);
-val acc_wfD = result();
+qed "acc_wfD";
goal Acc.thy "wf(r) <-> field(r) <= acc(r)";
by (EVERY1 [rtac iffI, etac acc_wfD, etac acc_wfI]);
-val wf_acc_iff = result();
+qed "wf_acc_iff";
--- a/src/ZF/ex/BT.ML Wed Dec 14 10:26:30 1994 +0100
+++ b/src/ZF/ex/BT.ML Wed Dec 14 11:41:49 1994 +0100
@@ -21,27 +21,27 @@
by (rtac lfp_mono 1);
by (REPEAT (rtac bt.bnd_mono 1));
by (REPEAT (ares_tac (univ_mono::basic_monos) 1));
-val bt_mono = result();
+qed "bt_mono";
goalw BT.thy (bt.defs@bt.con_defs) "bt(univ(A)) <= univ(A)";
by (rtac lfp_lowerbound 1);
by (rtac (A_subset_univ RS univ_mono) 2);
by (fast_tac (ZF_cs addSIs [zero_in_univ, Inl_in_univ, Inr_in_univ,
Pair_in_univ]) 1);
-val bt_univ = result();
+qed "bt_univ";
-val bt_subset_univ = standard ([bt_mono, bt_univ] MRS subset_trans);
+bind_thm ("bt_subset_univ", ([bt_mono, bt_univ] MRS subset_trans));
(** bt_rec -- by Vset recursion **)
goalw BT.thy bt.con_defs "rank(l) < rank(Br(a,l,r))";
by (simp_tac rank_ss 1);
-val rank_Br1 = result();
+qed "rank_Br1";
goalw BT.thy bt.con_defs "rank(r) < rank(Br(a,l,r))";
by (simp_tac rank_ss 1);
-val rank_Br2 = result();
+qed "rank_Br2";
goal BT.thy "bt_rec(Lf,c,h) = c";
by (rtac (bt_rec_def RS def_Vrec RS trans) 1);
@@ -71,13 +71,13 @@
val [rew] = goal BT.thy "[| !!t. j(t)==bt_rec(t, c, h) |] ==> j(Lf) = c";
by (rewtac rew);
by (rtac bt_rec_Lf 1);
-val def_bt_rec_Lf = result();
+qed "def_bt_rec_Lf";
val [rew] = goal BT.thy
"[| !!t. j(t)==bt_rec(t, c, h) |] ==> j(Br(a,l,r)) = h(a,l,r,j(l),j(r))";
by (rewtac rew);
by (rtac bt_rec_Br 1);
-val def_bt_rec_Br = result();
+qed "def_bt_rec_Br";
fun bt_recs def = map standard ([def] RL [def_bt_rec_Lf, def_bt_rec_Br]);
@@ -88,7 +88,7 @@
val prems = goalw BT.thy [n_nodes_def]
"xs: bt(A) ==> n_nodes(xs) : nat";
by (REPEAT (ares_tac (prems @ [bt_rec_type, nat_0I, nat_succI, add_type]) 1));
-val n_nodes_type = result();
+qed "n_nodes_type";
(** n_leaves **)
@@ -106,7 +106,7 @@
goalw BT.thy [bt_reflect_def] "!!xs. xs: bt(A) ==> bt_reflect(xs) : bt(A)";
by (REPEAT (ares_tac (bt.intrs @ [bt_rec_type]) 1));
-val bt_reflect_type = result();
+qed "bt_reflect_type";
(** BT simplification **)
@@ -131,13 +131,13 @@
by (bt_ind_tac "t" prems 1);
by (ALLGOALS (asm_simp_tac bt_ss));
by (REPEAT (ares_tac [add_commute, n_leaves_type] 1));
-val n_leaves_reflect = result();
+qed "n_leaves_reflect";
val prems = goal BT.thy
"t: bt(A) ==> n_leaves(t) = succ(n_nodes(t))";
by (bt_ind_tac "t" prems 1);
by (ALLGOALS (asm_simp_tac (bt_ss addsimps [add_succ_right])));
-val n_leaves_nodes = result();
+qed "n_leaves_nodes";
(*** theorems about bt_reflect ***)
@@ -145,6 +145,6 @@
"t: bt(A) ==> bt_reflect(bt_reflect(t))=t";
by (bt_ind_tac "t" prems 1);
by (ALLGOALS (asm_simp_tac bt_ss));
-val bt_reflect_bt_reflect_ident = result();
+qed "bt_reflect_bt_reflect_ident";
--- a/src/ZF/ex/Bin.ML Wed Dec 14 10:26:30 1994 +0100
+++ b/src/ZF/ex/Bin.ML Wed Dec 14 11:41:49 1994 +0100
@@ -45,7 +45,7 @@
by (ALLGOALS
(asm_simp_tac (ZF_ss addsimps (prems@[bin_rec_Plus,bin_rec_Minus,
bin_rec_Bcons]))));
-val bin_rec_type = result();
+qed "bin_rec_type";
(** Versions for use with definitions **)
@@ -53,19 +53,19 @@
"[| !!w. j(w)==bin_rec(w,a,b,h) |] ==> j(Plus) = a";
by (rewtac rew);
by (rtac bin_rec_Plus 1);
-val def_bin_rec_Plus = result();
+qed "def_bin_rec_Plus";
val [rew] = goal Bin.thy
"[| !!w. j(w)==bin_rec(w,a,b,h) |] ==> j(Minus) = b";
by (rewtac rew);
by (rtac bin_rec_Minus 1);
-val def_bin_rec_Minus = result();
+qed "def_bin_rec_Minus";
val [rew] = goal Bin.thy
"[| !!w. j(w)==bin_rec(w,a,b,h) |] ==> j(w$$x) = h(w,x,j(w))";
by (rewtac rew);
by (rtac bin_rec_Bcons 1);
-val def_bin_rec_Bcons = result();
+qed "def_bin_rec_Bcons";
fun bin_recs def = map standard
([def] RL [def_bin_rec_Plus, def_bin_rec_Minus, def_bin_rec_Bcons]);
@@ -78,7 +78,7 @@
"!!w. w: bin ==> integ_of_bin(w) : integ";
by (typechk_tac (bin_typechecks0@integ_typechecks@
nat_typechecks@[bool_into_nat]));
-val integ_of_bin_type = result();
+qed "integ_of_bin_type";
goalw Bin.thy [bin_succ_def]
"!!w. w: bin ==> bin_succ(w) : bin";
@@ -105,7 +105,7 @@
"!!v w. [| v: bin; w: bin |] ==> bin_mult(v,w) : bin";
by (typechk_tac ([bin_minus_type,bin_add_type]@bin_typechecks0@
bool_typechecks));
-val bin_mult_type = result();
+qed "bin_mult_type";
val bin_typechecks = bin_typechecks0 @
[integ_of_bin_type, bin_succ_type, bin_pred_type,
@@ -128,7 +128,7 @@
\ z: integ; z': integ; v: integ; v': integ; w: integ |] \
\ ==> z $+ (v $+ w) = z' $+ (v' $+ w)";
by (asm_simp_tac (integ_ss addsimps ([zadd_assoc RS sym])) 1);
-val zadd_assoc_cong = result();
+qed "zadd_assoc_cong";
goal Integ.thy
"!!z v w. [| z: integ; v: integ; w: integ |] \
@@ -143,7 +143,7 @@
val zadd_assoc_swap_kill = zadd_kill RSN (4, zadd_assoc_swap RS trans);
(*Pushes 'constants' of the form $#m to the right -- LOOPS if two!*)
-val zadd_assoc_znat = standard (znat_type RS zadd_assoc_swap);
+bind_thm ("zadd_assoc_znat", (znat_type RS zadd_assoc_swap));
goal Integ.thy
"!!z w. [| z: integ; w: integ |] \
@@ -195,7 +195,7 @@
by (etac boolE 1);
by (ALLGOALS
(asm_simp_tac (bin_minus_ss addsimps [zminus_zadd_distrib, zadd_assoc])));
-val integ_of_bin_minus = result();
+qed "integ_of_bin_minus";
(*** bin_add: binary addition ***)
@@ -221,7 +221,7 @@
\ bin_add(v$$x, w$$y) = \
\ bin_add(v, cond(x and y, bin_succ(w), w)) $$ (x xor y)";
by (asm_simp_tac bin_ss 1);
-val bin_add_Bcons_Bcons = result();
+qed "bin_add_Bcons_Bcons";
val bin_add_rews = [bin_add_Plus, bin_add_Minus, bin_add_Bcons_Plus,
bin_add_Bcons_Minus, bin_add_Bcons_Bcons,
@@ -248,7 +248,7 @@
by (ALLGOALS (asm_simp_tac (bin_add_ss addsimps [zadd_assoc,zadd_swap_pairs])));
by (REPEAT (ares_tac ([refl, zadd_kill, zadd_assoc_swap_kill RS sym]@
typechecks) 1));
-val integ_of_bin_add_lemma = result();
+qed "integ_of_bin_add_lemma";
val integ_of_bin_add = integ_of_bin_add_lemma RS bspec;
@@ -274,7 +274,7 @@
(bin_mult_ss addsimps [zadd_zmult_distrib, zmult_1, zadd_assoc]) 1);
by (REPEAT (ares_tac ([zadd_commute, zadd_assoc_swap_kill RS sym]@
typechecks) 1));
-val integ_of_bin_mult = result();
+qed "integ_of_bin_mult";
(**** Computations ****)
@@ -285,19 +285,19 @@
goal Bin.thy "bin_succ(w$$1) = bin_succ(w) $$ 0";
by (simp_tac carry_ss 1);
-val bin_succ_Bcons1 = result();
+qed "bin_succ_Bcons1";
goal Bin.thy "bin_succ(w$$0) = w$$1";
by (simp_tac carry_ss 1);
-val bin_succ_Bcons0 = result();
+qed "bin_succ_Bcons0";
goal Bin.thy "bin_pred(w$$1) = w$$0";
by (simp_tac carry_ss 1);
-val bin_pred_Bcons1 = result();
+qed "bin_pred_Bcons1";
goal Bin.thy "bin_pred(w$$0) = bin_pred(w) $$ 1";
by (simp_tac carry_ss 1);
-val bin_pred_Bcons0 = result();
+qed "bin_pred_Bcons0";
(** extra rules for bin_minus **)
@@ -305,28 +305,28 @@
goal Bin.thy "bin_minus(w$$1) = bin_pred(bin_minus(w) $$ 0)";
by (simp_tac bin_minus_ss 1);
-val bin_minus_Bcons1 = result();
+qed "bin_minus_Bcons1";
goal Bin.thy "bin_minus(w$$0) = bin_minus(w) $$ 0";
by (simp_tac bin_minus_ss 1);
-val bin_minus_Bcons0 = result();
+qed "bin_minus_Bcons0";
(** extra rules for bin_add **)
goal Bin.thy
"!!w. w: bin ==> bin_add(v$$1, w$$1) = bin_add(v, bin_succ(w)) $$ 0";
by (asm_simp_tac bin_add_ss 1);
-val bin_add_Bcons_Bcons11 = result();
+qed "bin_add_Bcons_Bcons11";
goal Bin.thy
"!!w. w: bin ==> bin_add(v$$1, w$$0) = bin_add(v,w) $$ 1";
by (asm_simp_tac bin_add_ss 1);
-val bin_add_Bcons_Bcons10 = result();
+qed "bin_add_Bcons_Bcons10";
goal Bin.thy
"!!w y.[| w: bin; y: bool |] ==> bin_add(v$$0, w$$y) = bin_add(v,w) $$ y";
by (asm_simp_tac bin_add_ss 1);
-val bin_add_Bcons_Bcons0 = result();
+qed "bin_add_Bcons_Bcons0";
(** extra rules for bin_mult **)
@@ -334,11 +334,11 @@
goal Bin.thy "bin_mult(v$$1, w) = bin_add(bin_mult(v,w)$$0, w)";
by (simp_tac bin_mult_ss 1);
-val bin_mult_Bcons1 = result();
+qed "bin_mult_Bcons1";
goal Bin.thy "bin_mult(v$$0, w) = bin_mult(v,w)$$0";
by (simp_tac bin_mult_ss 1);
-val bin_mult_Bcons0 = result();
+qed "bin_mult_Bcons0";
(*** The computation simpset ***)
--- a/src/ZF/ex/Brouwer.ML Wed Dec 14 10:26:30 1994 +0100
+++ b/src/ZF/ex/Brouwer.ML Wed Dec 14 11:41:49 1994 +0100
@@ -17,7 +17,7 @@
by (fast_tac (sum_cs addSIs (equalityI :: map rew intrs)
addEs [rew elim]) 1)
end;
-val brouwer_unfold = result();
+qed "brouwer_unfold";
(*A nicer induction rule than the standard one*)
val major::prems = goal Brouwer.thy
@@ -31,7 +31,7 @@
by (REPEAT_SOME (ares_tac prems));
by (fast_tac (ZF_cs addEs [fun_weaken_type]) 1);
by (fast_tac (ZF_cs addDs [apply_type]) 1);
-val brouwer_induct2 = result();
+qed "brouwer_induct2";
(** The Martin-Löf wellordering type **)
@@ -41,7 +41,7 @@
by (fast_tac (sum_cs addSIs (equalityI :: map rew intrs)
addEs [rew elim]) 1)
end;
-val Well_unfold = result();
+qed "Well_unfold";
(*A nicer induction rule than the standard one*)
val major::prems = goal Brouwer.thy
@@ -53,7 +53,7 @@
by (REPEAT_SOME (ares_tac prems));
by (fast_tac (ZF_cs addEs [fun_weaken_type]) 1);
by (fast_tac (ZF_cs addDs [apply_type]) 1);
-val Well_induct2 = result();
+qed "Well_induct2";
(*In fact it's isomorphic to nat, but we need a recursion operator for
@@ -61,4 +61,4 @@
goal Brouwer.thy "Well(bool, %x.x) = 1 + (1 -> Well(bool, %x.x))";
by (resolve_tac [Well_unfold RS trans] 1);
by (simp_tac (ZF_ss addsimps [Sigma_bool, Pi_empty1, succ_def]) 1);
-val Well_bool_unfold = result();
+qed "Well_bool_unfold";
--- a/src/ZF/ex/CoUnit.ML Wed Dec 14 10:26:30 1994 +0100
+++ b/src/ZF/ex/CoUnit.ML Wed Dec 14 11:41:49 1994 +0100
@@ -26,7 +26,7 @@
by (rtac subset_refl 1);
by (rewrite_goals_tac counit.con_defs);
by (fast_tac ZF_cs 1);
-val counit_eq_univ = result();
+qed "counit_eq_univ";
(*A similar example, but the constructor is non-degenerate and it works!
@@ -41,7 +41,7 @@
goalw CoUnit.thy counit2.con_defs "bnd_mono(univ(0), %x. Con2(x,x))";
by (rtac bnd_monoI 1);
by (REPEAT (ares_tac [subset_refl, QPair_subset_univ, QPair_mono] 1));
-val Con2_bnd_mono = result();
+qed "Con2_bnd_mono";
goal CoUnit.thy "lfp(univ(0), %x. Con2(x,x)) : counit2";
by (rtac (singletonI RS counit2.coinduct) 1);
@@ -62,7 +62,7 @@
addSIs [QPair_Int_Vset_subset_UN RS subset_trans, QPair_mono]
addSEs [Ord_in_Ord, Pair_inject];
by (fast_tac lleq_cs 1);
-val counit2_Int_Vset_subset_lemma = result();
+qed "counit2_Int_Vset_subset_lemma";
val counit2_Int_Vset_subset = standard
(counit2_Int_Vset_subset_lemma RS spec RS spec RS mp);
@@ -70,7 +70,7 @@
goal CoUnit.thy "!!x y. [| x: counit2; y: counit2 |] ==> x=y";
by (rtac equalityI 1);
by (REPEAT (ares_tac [conjI, counit2_Int_Vset_subset RS Int_Vset_subset] 1));
-val counit2_implies_equal = result();
+qed "counit2_implies_equal";
goal CoUnit.thy "counit2 = {lfp(univ(0), %x. Con2(x,x))}";
by (rtac equalityI 1);
@@ -79,4 +79,4 @@
by (dtac (lfp_Con2_in_counit2 RS counit2_implies_equal) 1);
by (etac subst 1);
by (rtac singletonI 1);
-val counit2_eq_univ = result();
+qed "counit2_eq_univ";
--- a/src/ZF/ex/Comb.ML Wed Dec 14 10:26:30 1994 +0100
+++ b/src/ZF/ex/Comb.ML Wed Dec 14 11:41:49 1994 +0100
@@ -23,8 +23,8 @@
(*** Results about Contraction ***)
-val contract_induct = standard
- (contract.mutual_induct RS spec RS spec RSN (2,rev_mp));
+bind_thm ("contract_induct",
+ (contract.mutual_induct RS spec RS spec RSN (2,rev_mp)));
(*For type checking: replaces a-1->b by a,b:comb *)
val contract_combE2 = contract.dom_subset RS subsetD RS SigmaE2;
@@ -35,11 +35,11 @@
by (fast_tac (ZF_cs addIs [equalityI,contract.K] addSEs [contract_combE2]) 1);
qed "field_contract_eq";
-val reduction_refl = standard
- (field_contract_eq RS equalityD2 RS subsetD RS rtrancl_refl);
+bind_thm ("reduction_refl",
+ (field_contract_eq RS equalityD2 RS subsetD RS rtrancl_refl));
-val rtrancl_into_rtrancl2 = standard
- (r_into_rtrancl RS (trans_rtrancl RS transD));
+bind_thm ("rtrancl_into_rtrancl2",
+ (r_into_rtrancl RS (trans_rtrancl RS transD)));
val reduction_rls = [reduction_refl, contract.K, contract.S,
contract.K RS rtrancl_into_rtrancl2,
@@ -50,7 +50,7 @@
(*Example only: not used*)
goalw Comb.thy [I_def] "!!p. p:comb ==> I#p ---> p";
by (REPEAT (ares_tac (comb.intrs @ reduction_rls) 1));
-val reduce_I = result();
+qed "reduce_I";
goalw Comb.thy [I_def] "I: comb";
by (REPEAT (ares_tac comb.intrs 1));
@@ -72,11 +72,11 @@
goalw Comb.thy [I_def] "!!r. I -1-> r ==> P";
by (fast_tac contract_cs 1);
-val I_contract_E = result();
+qed "I_contract_E";
goal Comb.thy "!!p r. K#p -1-> r ==> (EX q. r = K#q & p -1-> q)";
by (fast_tac contract_cs 1);
-val K1_contractD = result();
+qed "K1_contractD";
goal Comb.thy "!!p r. [| p ---> q; r: comb |] ==> p#r ---> q#r";
by (forward_tac [rtrancl_type RS subsetD RS SigmaD1] 1);
@@ -85,7 +85,7 @@
by (fast_tac (contract_cs addIs reduction_rls) 1);
by (etac (trans_rtrancl RS transD) 1);
by (fast_tac (contract_cs addIs reduction_rls) 1);
-val Ap_reduce1 = result();
+qed "Ap_reduce1";
goal Comb.thy "!!p r. [| p ---> q; r: comb |] ==> r#p ---> r#q";
by (forward_tac [rtrancl_type RS subsetD RS SigmaD1] 1);
@@ -94,33 +94,33 @@
by (fast_tac (contract_cs addIs reduction_rls) 1);
by (etac (trans_rtrancl RS transD) 1);
by (fast_tac (contract_cs addIs reduction_rls) 1);
-val Ap_reduce2 = result();
+qed "Ap_reduce2";
(** Counterexample to the diamond property for -1-> **)
goal Comb.thy "K#I#(I#I) -1-> I";
by (REPEAT (ares_tac [contract.K, comb_I, comb_Ap] 1));
-val KIII_contract1 = result();
+qed "KIII_contract1";
goalw Comb.thy [I_def] "K#I#(I#I) -1-> K#I#((K#I)#(K#I))";
by (DEPTH_SOLVE (resolve_tac (comb.intrs @ contract.intrs) 1));
-val KIII_contract2 = result();
+qed "KIII_contract2";
goal Comb.thy "K#I#((K#I)#(K#I)) -1-> I";
by (REPEAT (ares_tac (comb.intrs @ [contract.K, comb_I]) 1));
-val KIII_contract3 = result();
+qed "KIII_contract3";
goalw Comb.thy [diamond_def] "~ diamond(contract)";
by (fast_tac (ZF_cs addIs [KIII_contract1,KIII_contract2,KIII_contract3]
addSEs [I_contract_E]) 1);
-val not_diamond_contract = result();
+qed "not_diamond_contract";
(*** Results about Parallel Contraction ***)
-val parcontract_induct = standard
- (parcontract.mutual_induct RS spec RS spec RSN (2,rev_mp));
+bind_thm ("parcontract_induct",
+ (parcontract.mutual_induct RS spec RS spec RSN (2,rev_mp)));
(*For type checking: replaces a=1=>b by a,b:comb *)
val parcontract_combE2 = parcontract.dom_subset RS subsetD RS SigmaE2;
@@ -130,7 +130,7 @@
goal Comb.thy "field(parcontract) = comb";
by (fast_tac (ZF_cs addIs [equalityI, parcontract.K]
addSEs [parcontract_combE2]) 1);
-val field_parcontract_eq = result();
+qed "field_parcontract_eq";
(*Derive a case for each combinator constructor*)
val K_parcontractE = parcontract.mk_cases comb.con_defs "K =1=> r";
@@ -149,16 +149,16 @@
goal Comb.thy "!!p r. K#p =1=> r ==> (EX p'. r = K#p' & p =1=> p')";
by (fast_tac parcontract_cs 1);
-val K1_parcontractD = result();
+qed "K1_parcontractD";
goal Comb.thy "!!p r. S#p =1=> r ==> (EX p'. r = S#p' & p =1=> p')";
by (fast_tac parcontract_cs 1);
-val S1_parcontractD = result();
+qed "S1_parcontractD";
goal Comb.thy
"!!p q r. S#p#q =1=> r ==> (EX p' q'. r = S#p'#q' & p =1=> p' & q =1=> q')";
by (fast_tac (parcontract_cs addSDs [S1_parcontractD]) 1);
-val S2_parcontractD = result();
+qed "S2_parcontractD";
(*Church-Rosser property for parallel contraction*)
goalw Comb.thy [diamond_def] "diamond(parcontract)";
@@ -166,7 +166,7 @@
by (etac parcontract_induct 1);
by (ALLGOALS
(fast_tac (parcontract_cs addSDs [K1_parcontractD,S2_parcontractD])));
-val diamond_parcontract = result();
+qed "diamond_parcontract";
(*** Transitive closure preserves the Church-Rosser property ***)
@@ -177,7 +177,7 @@
by (fast_tac (ZF_cs addIs [r_into_trancl]) 1);
by (slow_best_tac (ZF_cs addSDs [spec RS mp]
addIs [r_into_trancl, trans_trancl RS transD]) 1);
-val diamond_trancl_lemma = result();
+qed "diamond_trancl_lemma";
val diamond_lemmaE = diamond_trancl_lemma RS spec RS mp RS exE;
@@ -188,7 +188,7 @@
by (ALLGOALS
(slow_best_tac (ZF_cs addIs [r_into_trancl, trans_trancl RS transD]
addEs [major RS diamond_lemmaE])));
-val diamond_trancl = result();
+qed "diamond_trancl";
(*** Equivalence of p--->q and p===>q ***)
@@ -196,7 +196,7 @@
goal Comb.thy "!!p q. p-1->q ==> p=1=>q";
by (etac contract_induct 1);
by (ALLGOALS (fast_tac (parcontract_cs)));
-val contract_imp_parcontract = result();
+qed "contract_imp_parcontract";
goal Comb.thy "!!p q. p--->q ==> p===>q";
by (forward_tac [rtrancl_type RS subsetD RS SigmaD1] 1);
@@ -205,7 +205,7 @@
by (fast_tac (parcontract_cs addIs [r_into_trancl]) 1);
by (fast_tac (ZF_cs addIs [contract_imp_parcontract,
r_into_trancl, trans_trancl RS transD]) 1);
-val reduce_imp_parreduce = result();
+qed "reduce_imp_parreduce";
goal Comb.thy "!!p q. p=1=>q ==> p--->q";
@@ -227,10 +227,10 @@
by (etac parcontract_imp_reduce 1);
by (etac (trans_rtrancl RS transD) 1);
by (etac parcontract_imp_reduce 1);
-val parreduce_imp_reduce = result();
+qed "parreduce_imp_reduce";
goal Comb.thy "p===>q <-> p--->q";
by (REPEAT (ares_tac [iffI, parreduce_imp_reduce, reduce_imp_parreduce] 1));
-val parreduce_iff_reduce = result();
+qed "parreduce_iff_reduce";
writeln"Reached end of file.";
--- a/src/ZF/ex/Data.ML Wed Dec 14 10:26:30 1994 +0100
+++ b/src/ZF/ex/Data.ML Wed Dec 14 11:41:49 1994 +0100
@@ -14,7 +14,7 @@
by (fast_tac (sum_cs addSIs (equalityI :: map rew intrs)
addEs [rew elim]) 1)
end;
-val data_unfold = result();
+qed "data_unfold";
(** Lemmas to justify using "data" in other recursive type definitions **)
@@ -22,15 +22,15 @@
by (rtac lfp_mono 1);
by (REPEAT (rtac data.bnd_mono 1));
by (REPEAT (ares_tac (univ_mono::Un_mono::basic_monos) 1));
-val data_mono = result();
+qed "data_mono";
goalw Data.thy (data.defs@data.con_defs) "data(univ(A),univ(A)) <= univ(A)";
by (rtac lfp_lowerbound 1);
by (rtac ([A_subset_univ, Un_upper1] MRS subset_trans RS univ_mono) 2);
by (fast_tac (ZF_cs addSIs [zero_in_univ, Inl_in_univ, Inr_in_univ,
Pair_in_univ]) 1);
-val data_univ = result();
+qed "data_univ";
-val data_subset_univ = standard ([data_mono, data_univ] MRS subset_trans);
+bind_thm ("data_subset_univ", ([data_mono, data_univ] MRS subset_trans));
--- a/src/ZF/ex/Integ.ML Wed Dec 14 10:26:30 1994 +0100
+++ b/src/ZF/ex/Integ.ML Wed Dec 14 11:41:49 1994 +0100
@@ -35,7 +35,7 @@
by (rtac (add_left_commute RS trans) 1 THEN typechk_tac prems);
by (rtac (eqa RS ssubst) 1);
by (rtac (add_left_commute) 1 THEN typechk_tac prems);
-val integ_trans_lemma = result();
+qed "integ_trans_lemma";
(** Natural deduction for intrel **)
@@ -57,7 +57,7 @@
\ p = <<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1 & \
\ x1: nat & y1: nat & x2: nat & y2: nat)";
by (fast_tac ZF_cs 1);
-val intrelE_lemma = result();
+qed "intrelE_lemma";
val [major,minor] = goal Integ.thy
"[| p: intrel; \
@@ -95,7 +95,7 @@
by (dtac eq_intrelD 1);
by (typechk_tac [nat_0I, SigmaI]);
by (asm_full_simp_tac intrel_ss 1);
-val znat_inject = result();
+qed "znat_inject";
(**** zminus: unary negation on integ ****)
@@ -104,7 +104,7 @@
"congruent(intrel, split(%x y. intrel``{<y,x>}))";
by (safe_tac intrel_cs);
by (asm_full_simp_tac (intrel_ss addsimps add_ac) 1);
-val zminus_congruent = result();
+qed "zminus_congruent";
(*Resolve th against the corresponding facts for zminus*)
val zminus_ize = RSLIST [equiv_intrel, zminus_congruent];
@@ -122,7 +122,7 @@
(*The setloop is only needed because assumptions are in the wrong order!*)
by (asm_full_simp_tac (intrel_ss addsimps add_ac
setloop dtac eq_intrelD) 1);
-val zminus_inject = result();
+qed "zminus_inject";
goalw Integ.thy [zminus_def]
"!!x y.[| x: nat; y: nat |] ==> $~ (intrel``{<x,y>}) = intrel `` {<y,x>}";
@@ -132,11 +132,11 @@
goalw Integ.thy [integ_def] "!!z. z : integ ==> $~ ($~ z) = z";
by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
by (asm_simp_tac (ZF_ss addsimps [zminus]) 1);
-val zminus_zminus = result();
+qed "zminus_zminus";
goalw Integ.thy [integ_def, znat_def] "$~ ($#0) = $#0";
by (simp_tac (arith_ss addsimps [zminus]) 1);
-val zminus_0 = result();
+qed "zminus_0";
(**** znegative: the test for negative integers ****)
@@ -145,7 +145,7 @@
by (asm_full_simp_tac (intrel_ss setloop K(safe_tac intrel_cs)) 1);
be rev_mp 1;
by (asm_simp_tac (arith_ss addsimps [add_le_self2 RS le_imp_not_lt]) 1);
-val not_znegative_znat = result();
+qed "not_znegative_znat";
goalw Integ.thy [znegative_def, znat_def]
"!!n. n: nat ==> znegative($~ $# succ(n))";
@@ -153,7 +153,7 @@
by (REPEAT
(ares_tac [refl, exI, conjI, nat_0_le,
refl RS intrelI RS imageI, consI1, nat_0I, nat_succI] 1));
-val znegative_zminus_znat = result();
+qed "znegative_zminus_znat";
(**** zmagnitude: magnitide of an integer, as a natural number ****)
@@ -174,7 +174,7 @@
by (res_inst_tac [("m1","x")] (add_commute RS ssubst) 1 THEN
REPEAT (assume_tac 1));
by (asm_simp_tac (arith_ss addsimps [diff_add_inverse, diff_add_0]) 1);
-val zmagnitude_congruent = result();
+qed "zmagnitude_congruent";
(*Resolve th against the corresponding facts for zmagnitude*)
@@ -184,7 +184,7 @@
"!!z. z : integ ==> zmagnitude(z) : nat";
by (typechk_tac [split_type, zmagnitude_ize UN_equiv_class_type,
add_type, diff_type]);
-val zmagnitude_type = result();
+qed "zmagnitude_type";
goalw Integ.thy [zmagnitude_def]
"!!x y. [| x: nat; y: nat |] ==> \
@@ -195,12 +195,12 @@
goalw Integ.thy [znat_def]
"!!n. n: nat ==> zmagnitude($# n) = n";
by (asm_simp_tac (intrel_ss addsimps [zmagnitude]) 1);
-val zmagnitude_znat = result();
+qed "zmagnitude_znat";
goalw Integ.thy [znat_def]
"!!n. n: nat ==> zmagnitude($~ $# n) = n";
by (asm_simp_tac (intrel_ss addsimps [zmagnitude, zminus]) 1);
-val zmagnitude_zminus_znat = result();
+qed "zmagnitude_zminus_znat";
(**** zadd: addition on integ ****)
@@ -219,7 +219,7 @@
by (res_inst_tac [("m1","x2a")] (add_left_commute RS ssubst) 3);
by (typechk_tac [add_type]);
by (asm_simp_tac (arith_ss addsimps [add_assoc RS sym]) 1);
-val zadd_congruent2 = result();
+qed "zadd_congruent2";
(*Resolve th against the corresponding facts for zadd*)
@@ -229,7 +229,7 @@
"!!z w. [| z: integ; w: integ |] ==> z $+ w : integ";
by (REPEAT (ares_tac [zadd_ize UN_equiv_class_type2,
split_type, add_type, quotientI, SigmaI] 1));
-val zadd_type = result();
+qed "zadd_type";
goalw Integ.thy [zadd_def]
"!!x1 y1. [| x1: nat; y1: nat; x2: nat; y2: nat |] ==> \
@@ -247,7 +247,7 @@
"!!z w. [| z: integ; w: integ |] ==> $~ (z $+ w) = $~ z $+ $~ w";
by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
by (asm_simp_tac (arith_ss addsimps [zminus,zadd]) 1);
-val zminus_zadd_distrib = result();
+qed "zminus_zadd_distrib";
goalw Integ.thy [integ_def]
"!!z w. [| z: integ; w: integ |] ==> z $+ w = w $+ z";
@@ -266,7 +266,7 @@
goalw Integ.thy [znat_def]
"!!m n. [| m: nat; n: nat |] ==> $# (m #+ n) = ($#m) $+ ($#n)";
by (asm_simp_tac (arith_ss addsimps [zadd]) 1);
-val znat_add = result();
+qed "znat_add";
goalw Integ.thy [integ_def,znat_def] "!!z. z : integ ==> z $+ ($~ z) = $#0";
by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
@@ -276,7 +276,7 @@
goal Integ.thy "!!z. z : integ ==> ($~ z) $+ z = $#0";
by (asm_simp_tac
(ZF_ss addsimps [zadd_commute, zminus_type, zadd_zminus_inverse]) 1);
-val zadd_zminus_inverse2 = result();
+qed "zadd_zminus_inverse2";
goal Integ.thy "!!z. z:integ ==> z $+ $#0 = z";
by (rtac (zadd_commute RS trans) 1);
@@ -306,7 +306,7 @@
(arith_ss addsimps ([add_assoc RS sym, add_mult_distrib_left RS sym])) 2);
(*Proof that zmult is commutative on representatives*)
by (asm_simp_tac (arith_ss addsimps (mult_ac@add_ac)) 1);
-val zmult_congruent2 = result();
+qed "zmult_congruent2";
(*Resolve th against the corresponding facts for zmult*)
@@ -317,7 +317,7 @@
by (REPEAT (ares_tac [zmult_ize UN_equiv_class_type2,
split_type, add_type, mult_type,
quotientI, SigmaI] 1));
-val zmult_type = result();
+qed "zmult_type";
goalw Integ.thy [zmult_def]
"!!x1 x2. [| x1: nat; y1: nat; x2: nat; y2: nat |] ==> \
@@ -329,7 +329,7 @@
goalw Integ.thy [integ_def,znat_def] "!!z. z : integ ==> $#0 $* z = $#0";
by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
by (asm_simp_tac (arith_ss addsimps [zmult]) 1);
-val zmult_0 = result();
+qed "zmult_0";
goalw Integ.thy [integ_def,znat_def]
"!!z. z : integ ==> $#1 $* z = z";
@@ -341,19 +341,19 @@
"!!z w. [| z: integ; w: integ |] ==> ($~ z) $* w = $~ (z $* w)";
by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
by (asm_simp_tac (intrel_ss addsimps ([zminus, zmult] @ add_ac)) 1);
-val zmult_zminus = result();
+qed "zmult_zminus";
goalw Integ.thy [integ_def]
"!!z w. [| z: integ; w: integ |] ==> ($~ z) $* ($~ w) = (z $* w)";
by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
by (asm_simp_tac (intrel_ss addsimps ([zminus, zmult] @ add_ac)) 1);
-val zmult_zminus_zminus = result();
+qed "zmult_zminus_zminus";
goalw Integ.thy [integ_def]
"!!z w. [| z: integ; w: integ |] ==> z $* w = w $* z";
by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
by (asm_simp_tac (intrel_ss addsimps ([zmult] @ add_ac @ mult_ac)) 1);
-val zmult_commute = result();
+qed "zmult_commute";
goalw Integ.thy [integ_def]
"!!z1 z2 z3. [| z1: integ; z2: integ; z3: integ |] ==> \
@@ -362,7 +362,7 @@
by (asm_simp_tac
(intrel_ss addsimps ([zmult, add_mult_distrib_left,
add_mult_distrib] @ add_ac @ mult_ac)) 1);
-val zmult_assoc = result();
+qed "zmult_assoc";
goalw Integ.thy [integ_def]
"!!z1 z2 z3. [| z1: integ; z2: integ; w: integ |] ==> \
--- a/src/ZF/ex/LList.ML Wed Dec 14 10:26:30 1994 +0100
+++ b/src/ZF/ex/LList.ML Wed Dec 14 11:41:49 1994 +0100
@@ -20,7 +20,7 @@
by (fast_tac (qsum_cs addSIs (equalityI :: map rew intrs)
addEs [rew elim]) 1)
end;
-val llist_unfold = result();
+qed "llist_unfold";
(*** Lemmas to justify using "llist" in other recursive type definitions ***)
@@ -28,7 +28,7 @@
by (rtac gfp_mono 1);
by (REPEAT (rtac llist.bnd_mono 1));
by (REPEAT (ares_tac (quniv_mono::basic_monos) 1));
-val llist_mono = result();
+qed "llist_mono";
(** Closure of quniv(A) under llist -- why so complex? Its a gfp... **)
@@ -50,16 +50,16 @@
(*LCons case*)
by (safe_tac quniv_cs);
by (ALLGOALS (fast_tac (quniv_cs addSEs [Ord_trans, make_elim bspec])));
-val llist_quniv_lemma = result();
+qed "llist_quniv_lemma";
goal LList.thy "llist(quniv(A)) <= quniv(A)";
by (rtac (qunivI RS subsetI) 1);
by (rtac Int_Vset_subset 1);
by (REPEAT (ares_tac [llist_quniv_lemma RS bspec] 1));
-val llist_quniv = result();
+qed "llist_quniv";
-val llist_subset_quniv = standard
- (llist_mono RS (llist_quniv RSN (2,subset_trans)));
+bind_thm ("llist_subset_quniv",
+ (llist_mono RS (llist_quniv RSN (2,subset_trans))));
(*** Lazy List Equality: lleq ***)
@@ -77,10 +77,10 @@
by (rewrite_goals_tac (QInr_def::llist.con_defs));
by (safe_tac lleq_cs);
by (fast_tac (subset_cs addSEs [Ord_trans, make_elim bspec]) 1);
-val lleq_Int_Vset_subset_lemma = result();
+qed "lleq_Int_Vset_subset_lemma";
-val lleq_Int_Vset_subset = standard
- (lleq_Int_Vset_subset_lemma RS spec RS spec RS mp);
+bind_thm ("lleq_Int_Vset_subset",
+ (lleq_Int_Vset_subset_lemma RS spec RS spec RS mp));
(*lleq(A) is a symmetric relation because qconverse(lleq(A)) is a fixedpoint*)
@@ -90,13 +90,13 @@
by (safe_tac converse_cs);
by (etac lleq.elim 1);
by (ALLGOALS (fast_tac qconverse_cs));
-val lleq_symmetric = result();
+qed "lleq_symmetric";
goal LList.thy "!!l l'. <l,l'> : lleq(A) ==> l=l'";
by (rtac equalityI 1);
by (REPEAT (ares_tac [lleq_Int_Vset_subset RS Int_Vset_subset] 1
ORELSE etac lleq_symmetric 1));
-val lleq_implies_equal = result();
+qed "lleq_implies_equal";
val [eqprem,lprem] = goal LList.thy
"[| l=l'; l: llist(A) |] ==> <l,l'> : lleq(A)";
@@ -105,7 +105,7 @@
by (safe_tac qpair_cs);
by (etac llist.elim 1);
by (ALLGOALS (fast_tac pair_cs));
-val equal_llist_implies_leq = result();
+qed "equal_llist_implies_leq";
(*** Lazy List Functions ***)
@@ -119,26 +119,26 @@
by (REPEAT (ares_tac [subset_refl, QInr_mono, QPair_mono] 2));
by (REPEAT (ares_tac [subset_refl, A_subset_univ,
QInr_subset_univ, QPair_subset_univ] 1));
-val lconst_fun_bnd_mono = result();
+qed "lconst_fun_bnd_mono";
(* lconst(a) = LCons(a,lconst(a)) *)
-val lconst = standard
- ([lconst_def, lconst_fun_bnd_mono] MRS def_lfp_Tarski);
+bind_thm ("lconst",
+ ([lconst_def, lconst_fun_bnd_mono] MRS def_lfp_Tarski));
val lconst_subset = lconst_def RS def_lfp_subset;
-val member_subset_Union_eclose = standard (arg_into_eclose RS Union_upper);
+bind_thm ("member_subset_Union_eclose", (arg_into_eclose RS Union_upper));
goal LList.thy "!!a A. a : A ==> lconst(a) : quniv(A)";
by (rtac (lconst_subset RS subset_trans RS qunivI) 1);
by (etac (arg_into_eclose RS eclose_subset RS univ_mono) 1);
-val lconst_in_quniv = result();
+qed "lconst_in_quniv";
goal LList.thy "!!a A. a:A ==> lconst(a): llist(A)";
by (rtac (singletonI RS llist.coinduct) 1);
by (etac (lconst_in_quniv RS singleton_subsetI) 1);
by (fast_tac (ZF_cs addSIs [lconst]) 1);
-val lconst_type = result();
+qed "lconst_type";
(*** flip --- equations merely assumed; certain consequences proved ***)
@@ -146,7 +146,7 @@
goal QUniv.thy "!!b. b:bool ==> b Int X <= univ(eclose(A))";
by (fast_tac (quniv_cs addSEs [boolE]) 1);
-val bool_Int_subset_univ = result();
+qed "bool_Int_subset_univ";
val flip_cs = quniv_cs addSIs [not_type]
addIs [bool_Int_subset_univ];
@@ -167,12 +167,12 @@
(*LCons case*)
by (safe_tac flip_cs);
by (ALLGOALS (fast_tac (flip_cs addSEs [Ord_trans, make_elim bspec])));
-val flip_llist_quniv_lemma = result();
+qed "flip_llist_quniv_lemma";
goal LList.thy "!!l. l: llist(bool) ==> flip(l) : quniv(bool)";
by (rtac (flip_llist_quniv_lemma RS bspec RS Int_Vset_subset RS qunivI) 1);
by (REPEAT (assume_tac 1));
-val flip_in_quniv = result();
+qed "flip_in_quniv";
val [prem] = goal LList.thy "l : llist(bool) ==> flip(l): llist(bool)";
by (res_inst_tac [("X", "{flip(l) . l:llist(bool)}")]
@@ -197,4 +197,4 @@
by (asm_simp_tac flip_ss 1);
by (asm_simp_tac (flip_ss addsimps [flip_type, not_not]) 1);
by (fast_tac (ZF_cs addSIs [not_type]) 1);
-val flip_flip = result();
+qed "flip_flip";
--- a/src/ZF/ex/ListN.ML Wed Dec 14 10:26:30 1994 +0100
+++ b/src/ZF/ex/ListN.ML Wed Dec 14 11:41:49 1994 +0100
@@ -18,32 +18,32 @@
by (etac list.induct 1);
by (ALLGOALS (asm_simp_tac list_ss));
by (REPEAT (ares_tac listn.intrs 1));
-val list_into_listn = result();
+qed "list_into_listn";
goal ListN.thy "<n,l> : listn(A) <-> l:list(A) & length(l)=n";
by (rtac iffI 1);
by (etac listn_induct 1);
by (safe_tac (ZF_cs addSIs (list_typechecks @
[length_Nil, length_Cons, list_into_listn])));
-val listn_iff = result();
+qed "listn_iff";
goal ListN.thy "listn(A)``{n} = {l:list(A). length(l)=n}";
by (rtac equality_iffI 1);
by (simp_tac (list_ss addsimps [listn_iff,separation,image_singleton_iff]) 1);
-val listn_image_eq = result();
+qed "listn_image_eq";
goalw ListN.thy listn.defs "!!A B. A<=B ==> listn(A) <= listn(B)";
by (rtac lfp_mono 1);
by (REPEAT (rtac listn.bnd_mono 1));
by (REPEAT (ares_tac ([univ_mono,Sigma_mono,list_mono] @ basic_monos) 1));
-val listn_mono = result();
+qed "listn_mono";
goal ListN.thy
"!!n l. [| <n,l> : listn(A); <n',l'> : listn(A) |] ==> \
\ <n#+n', l@l'> : listn(A)";
by (etac listn_induct 1);
by (ALLGOALS (asm_simp_tac (list_ss addsimps listn.intrs)));
-val listn_append = result();
+qed "listn_append";
val Nil_listn_case = listn.mk_cases list.con_defs "<i,Nil> : listn(A)"
and Cons_listn_case = listn.mk_cases list.con_defs "<i,Cons(x,l)> : listn(A)";
--- a/src/ZF/ex/Ntree.ML Wed Dec 14 10:26:30 1994 +0100
+++ b/src/ZF/ex/Ntree.ML Wed Dec 14 11:41:49 1994 +0100
@@ -18,7 +18,7 @@
by (fast_tac (sum_cs addSIs (equalityI :: map rew intrs)
addEs [rew elim]) 1)
end;
-val ntree_unfold = result();
+qed "ntree_unfold";
(*A nicer induction rule than the standard one*)
val major::prems = goal Ntree.thy
@@ -31,7 +31,7 @@
by (REPEAT_SOME (ares_tac prems));
by (fast_tac (ZF_cs addEs [fun_weaken_type]) 1);
by (fast_tac (ZF_cs addDs [apply_type]) 1);
-val ntree_induct = result();
+qed "ntree_induct";
(*Induction on ntree(A) to prove an equation*)
val major::prems = goal Ntree.thy
@@ -45,7 +45,7 @@
br fun_extension 1;
by (REPEAT_SOME (ares_tac [comp_fun]));
by (asm_simp_tac (ZF_ss addsimps [comp_fun_apply]) 1);
-val ntree_induct_eqn = result();
+qed "ntree_induct_eqn";
(** Lemmas to justify using "Ntree" in other recursive type definitions **)
@@ -53,7 +53,7 @@
by (rtac lfp_mono 1);
by (REPEAT (rtac ntree.bnd_mono 1));
by (REPEAT (ares_tac (univ_mono::basic_monos) 1));
-val ntree_mono = result();
+qed "ntree_mono";
(*Easily provable by induction also*)
goalw Ntree.thy (ntree.defs@ntree.con_defs) "ntree(univ(A)) <= univ(A)";
@@ -61,7 +61,7 @@
by (rtac (A_subset_univ RS univ_mono) 2);
by (safe_tac ZF_cs);
by (REPEAT (ares_tac [Pair_in_univ, nat_fun_univ RS subsetD] 1));
-val ntree_univ = result();
+qed "ntree_univ";
val ntree_subset_univ = [ntree_mono, ntree_univ] MRS subset_trans |> standard;
@@ -73,7 +73,7 @@
by (fast_tac (sum_cs addSIs (equalityI :: map rew intrs)
addEs [rew elim]) 1)
end;
-val maptree_unfold = result();
+qed "maptree_unfold";
(*A nicer induction rule than the standard one*)
val major::prems = goal Ntree.thy
@@ -88,7 +88,7 @@
by (dresolve_tac [FiniteFun.dom_subset RS subsetD] 1);
by (dresolve_tac [Fin.dom_subset RS subsetD] 1);
by (fast_tac ZF_cs 1);
-val maptree_induct = result();
+qed "maptree_induct";
(** maptree2 **)
@@ -98,7 +98,7 @@
by (fast_tac (sum_cs addSIs (equalityI :: map rew intrs)
addEs [rew elim]) 1)
end;
-val maptree2_unfold = result();
+qed "maptree2_unfold";
(*A nicer induction rule than the standard one*)
val major::prems = goal Ntree.thy
@@ -113,5 +113,5 @@
by (dresolve_tac [FiniteFun.dom_subset RS subsetD] 1);
by (dresolve_tac [Fin.dom_subset RS subsetD] 1);
by (fast_tac ZF_cs 1);
-val maptree2_induct = result();
+qed "maptree2_induct";
--- a/src/ZF/ex/Primrec.ML Wed Dec 14 10:26:30 1994 +0100
+++ b/src/ZF/ex/Primrec.ML Wed Dec 14 11:41:49 1994 +0100
@@ -42,24 +42,24 @@
goalw Primrec.thy [PROJ_def]
"!!l. [| x: nat; l: list(nat) |] ==> PROJ(0) ` (Cons(x,l)) = x";
by (asm_simp_tac pr_ss 1);
-val PROJ_0 = result();
+qed "PROJ_0";
goalw Primrec.thy [COMP_def]
"!!l. [| l: list(nat) |] ==> COMP(g,[f]) ` l = g` [f`l]";
by (asm_simp_tac pr_ss 1);
-val COMP_1 = result();
+qed "COMP_1";
goalw Primrec.thy [PREC_def]
"!!l. l: list(nat) ==> PREC(f,g) ` (Cons(0,l)) = f`l";
by (asm_simp_tac pr_ss 1);
-val PREC_0 = result();
+qed "PREC_0";
goalw Primrec.thy [PREC_def]
"!!l. [| x:nat; l: list(nat) |] ==> \
\ PREC(f,g) ` (Cons(succ(x),l)) = \
\ g ` Cons(PREC(f,g)`(Cons(x,l)), Cons(x,l))";
by (asm_simp_tac pr_ss 1);
-val PREC_succ = result();
+qed "PREC_succ";
(*** Inductive definition of the PR functions ***)
@@ -73,7 +73,7 @@
goalw Primrec.thy [ACK_def] "!!i. i:nat ==> ACK(i): primrec";
by (etac nat_induct 1);
by (ALLGOALS (asm_simp_tac pr_ss));
-val ACK_in_primrec = result();
+qed "ACK_in_primrec";
val ack_typechecks =
[ACK_in_primrec, primrec_into_fun RS apply_type,
@@ -94,12 +94,12 @@
(*PROPERTY A 1*)
goalw Primrec.thy [ACK_def] "!!j. j:nat ==> ack(0,j) = succ(j)";
by (asm_simp_tac (pr_ss addsimps [SC]) 1);
-val ack_0 = result();
+qed "ack_0";
(*PROPERTY A 2*)
goalw Primrec.thy [ACK_def] "ack(succ(i), 0) = ack(i,1)";
by (asm_simp_tac (pr_ss addsimps [CONST,PREC_0]) 1);
-val ack_succ_0 = result();
+qed "ack_succ_0";
(*PROPERTY A 3*)
(*Could be proved in Primrec0, like the previous two cases, but using
@@ -108,7 +108,7 @@
"!!i j. [| i:nat; j:nat |] ==> \
\ ack(succ(i), succ(j)) = ack(i, ack(succ(i), j))";
by (asm_simp_tac (pr_ss addsimps [CONST,PREC_succ,COMP_1,PROJ_0]) 1);
-val ack_succ_succ = result();
+qed "ack_succ_succ";
val ack_ss =
pr_ss addsimps [ack_0, ack_succ_0, ack_succ_succ,
@@ -124,14 +124,14 @@
asm_simp_tac ack_ss] 1);
by (DO_GOAL [etac (succ_leI RS lt_trans1),
asm_simp_tac ack_ss] 1);
-val lt_ack2_lemma = result();
-val lt_ack2 = standard (lt_ack2_lemma RS bspec);
+qed "lt_ack2_lemma";
+bind_thm ("lt_ack2", (lt_ack2_lemma RS bspec));
(*PROPERTY A 5-, the single-step lemma*)
goal Primrec.thy "!!i j. [| i:nat; j:nat |] ==> ack(i,j) < ack(i, succ(j))";
by (etac nat_induct 1);
by (ALLGOALS (asm_simp_tac (ack_ss addsimps [lt_ack2])));
-val ack_lt_ack_succ2 = result();
+qed "ack_lt_ack_succ2";
(*PROPERTY A 5, monotonicity for < *)
goal Primrec.thy "!!i j k. [| j<k; i:nat; k:nat |] ==> ack(i,j) < ack(i,k)";
@@ -147,7 +147,7 @@
"!!i j k. [| j le k; i: nat; k:nat |] ==> ack(i,j) le ack(i,k)";
by (res_inst_tac [("f", "%j.ack(i,j)")] Ord_lt_mono_imp_le_mono 1);
by (REPEAT (ares_tac [ack_lt_mono2, ack_type RS nat_into_Ord] 1));
-val ack_le_mono2 = result();
+qed "ack_le_mono2";
(*PROPERTY A 6*)
goal Primrec.thy
@@ -192,7 +192,7 @@
goal Primrec.thy "!!j. j:nat ==> ack(succ(1),j) = succ(succ(succ(j#+j)))";
by (etac nat_induct 1);
by (ALLGOALS (asm_simp_tac (ack_ss addsimps [ack_1, add_succ_right])));
-val ack_2 = result();
+qed "ack_2";
(*PROPERTY A 10*)
goal Primrec.thy
@@ -227,7 +227,7 @@
by (rtac (ack_add_bound RS lt_trans2) 2);
by (asm_simp_tac (ack_ss addsimps [add_0_right]) 5);
by (REPEAT (ares_tac ([add_lt_mono, lt_ack2] @ ack_typechecks) 1));
-val ack_add_bound2 = result();
+qed "ack_add_bound2";
(*** MAIN RESULT ***)
@@ -239,7 +239,7 @@
by (etac list.elim 1);
by (asm_simp_tac (ack2_ss addsimps [succ_iff]) 1);
by (asm_simp_tac (ack2_ss addsimps [ack_1, add_le_self]) 1);
-val SC_case = result();
+qed "SC_case";
(*PROPERTY A 4'? Extra lemma needed for CONST case, constant functions*)
goal Primrec.thy "!!j. [| i:nat; j:nat |] ==> i < ack(i,j)";
@@ -252,7 +252,7 @@
goalw Primrec.thy [CONST_def]
"!!l. [| l: list(nat); k: nat |] ==> CONST(k) ` l < ack(k, list_add(l))";
by (asm_simp_tac (ack2_ss addsimps [lt_ack1]) 1);
-val CONST_case = result();
+qed "CONST_case";
goalw Primrec.thy [PROJ_def]
"!!l. l: list(nat) ==> ALL i:nat. PROJ(i) ` l < ack(0, list_add(l))";
@@ -267,7 +267,7 @@
by (etac (bspec RS lt_trans2) 1);
by (rtac (add_le_self2 RS succ_leI) 2);
by (tc_tac []);
-val PROJ_case_lemma = result();
+qed "PROJ_case_lemma";
val PROJ_case = PROJ_case_lemma RS bspec;
(** COMP case **)
@@ -289,7 +289,7 @@
by (REPEAT (FIRSTGOAL (etac bspec)));
by (rtac ack_add_bound 5);
by (tc_tac []);
-val COMP_map_lemma = result();
+qed "COMP_map_lemma";
goalw Primrec.thy [COMP_def]
"!!g. [| g: primrec; kg: nat; \
@@ -307,7 +307,7 @@
by (rtac ack_nest_bound 3);
by (etac (bspec RS ack_lt_mono2) 2);
by (tc_tac [map_type]);
-val COMP_case = result();
+qed "COMP_case";
(** PREC case **)
@@ -340,7 +340,7 @@
by (rtac (add_le_self2 RS ack_le_mono1 RS lt_trans1) 1);
by (etac ack_lt_mono2 5);
by (tc_tac []);
-val PREC_case_lemma = result();
+qed "PREC_case_lemma";
goal Primrec.thy
"!!f g. [| f: primrec; kf: nat; \
@@ -356,7 +356,7 @@
(FIRST' [test_assume_tac,
match_tac (ack_typechecks),
rtac (ack_add_bound2 RS ballI) THEN' etac bspec])));
-val PREC_case = result();
+qed "PREC_case";
goal Primrec.thy
"!!f. f:primrec ==> EX k:nat. ALL l:list(nat). f`l < ack(k, list_add(l))";
@@ -365,7 +365,7 @@
by (DEPTH_SOLVE
(ares_tac ([SC_case, CONST_case, PROJ_case, COMP_case, PREC_case,
bexI, ballI] @ nat_typechecks) 1));
-val ack_bounds_primrec = result();
+qed "ack_bounds_primrec";
goal Primrec.thy
"~ (lam l:list(nat). list_case(0, %x xs. ack(x,x), l)) : primrec";
@@ -375,5 +375,5 @@
by (dres_inst_tac [("x", "[x]")] bspec 1);
by (asm_simp_tac ack2_ss 1);
by (asm_full_simp_tac (ack2_ss addsimps [add_0_right]) 1);
-val ack_not_primrec = result();
+qed "ack_not_primrec";
--- a/src/ZF/ex/PropLog.ML Wed Dec 14 10:26:30 1994 +0100
+++ b/src/ZF/ex/PropLog.ML Wed Dec 14 11:41:49 1994 +0100
@@ -19,20 +19,20 @@
by (rtac (prop_rec_def RS def_Vrec RS trans) 1);
by (rewrite_goals_tac prop.con_defs);
by (simp_tac rank_ss 1);
-val prop_rec_Fls = result();
+qed "prop_rec_Fls";
goal PropLog.thy "prop_rec(#v,b,c,d) = c(v)";
by (rtac (prop_rec_def RS def_Vrec RS trans) 1);
by (rewrite_goals_tac prop.con_defs);
by (simp_tac rank_ss 1);
-val prop_rec_Var = result();
+qed "prop_rec_Var";
goal PropLog.thy "prop_rec(p=>q,b,c,d) = \
\ d(p, q, prop_rec(p,b,c,d), prop_rec(q,b,c,d))";
by (rtac (prop_rec_def RS def_Vrec RS trans) 1);
by (rewrite_goals_tac prop.con_defs);
by (simp_tac rank_ss 1);
-val prop_rec_Imp = result();
+qed "prop_rec_Imp";
val prop_rec_ss =
arith_ss addsimps [prop_rec_Fls, prop_rec_Var, prop_rec_Imp];
@@ -43,12 +43,12 @@
goalw PropLog.thy [is_true_def] "is_true(Fls,t) <-> False";
by (simp_tac (prop_rec_ss addsimps [one_not_0 RS not_sym]) 1);
-val is_true_Fls = result();
+qed "is_true_Fls";
goalw PropLog.thy [is_true_def] "is_true(#v,t) <-> v:t";
by (simp_tac (prop_rec_ss addsimps [one_not_0 RS not_sym]
setloop (split_tac [expand_if])) 1);
-val is_true_Var = result();
+qed "is_true_Var";
goalw PropLog.thy [is_true_def]
"is_true(p=>q,t) <-> (is_true(p,t)-->is_true(q,t))";
@@ -59,15 +59,15 @@
goalw PropLog.thy [hyps_def] "hyps(Fls,t) = 0";
by (simp_tac prop_rec_ss 1);
-val hyps_Fls = result();
+qed "hyps_Fls";
goalw PropLog.thy [hyps_def] "hyps(#v,t) = {if(v:t, #v, #v=>Fls)}";
by (simp_tac prop_rec_ss 1);
-val hyps_Var = result();
+qed "hyps_Var";
goalw PropLog.thy [hyps_def] "hyps(p=>q,t) = hyps(p,t) Un hyps(q,t)";
by (simp_tac prop_rec_ss 1);
-val hyps_Imp = result();
+qed "hyps_Imp";
val prop_ss = prop_rec_ss
addsimps prop.intrs
@@ -80,7 +80,7 @@
by (rtac lfp_mono 1);
by (REPEAT (rtac thms.bnd_mono 1));
by (REPEAT (ares_tac (univ_mono::basic_monos) 1));
-val thms_mono = result();
+qed "thms_mono";
val thms_in_pl = thms.dom_subset RS subsetD;
@@ -103,7 +103,7 @@
(** Weakening, left and right **)
(* [| G<=H; G|-p |] ==> H|-p Order of premises is convenient with RS*)
-val weaken_left = standard (thms_mono RS subsetD);
+bind_thm ("weaken_left", (thms_mono RS subsetD));
(* H |- p ==> cons(a,H) |- p *)
val weaken_left_cons = subset_consI RS weaken_left;
@@ -131,23 +131,23 @@
goal PropLog.thy "!!H p q. [| H|-p; cons(p,H) |- q |] ==> H |- q";
by (rtac (deduction RS thms_MP) 1);
by (REPEAT (ares_tac [thms_in_pl] 1));
-val cut = result();
+qed "cut";
goal PropLog.thy "!!H p. [| H |- Fls; p:prop |] ==> H |- p";
by (rtac (thms.DN RS thms_MP) 1);
by (rtac weaken_right 2);
by (REPEAT (ares_tac (prop.intrs@[consI1]) 1));
-val thms_FlsE = result();
+qed "thms_FlsE";
(* [| H |- p=>Fls; H |- p; q: prop |] ==> H |- q *)
-val thms_notE = standard (thms_MP RS thms_FlsE);
+bind_thm ("thms_notE", (thms_MP RS thms_FlsE));
(*Soundness of the rules wrt truth-table semantics*)
goalw PropLog.thy [logcon_def] "!!H. H |- p ==> H |= p";
by (etac thms.induct 1);
by (fast_tac (ZF_cs addSDs [is_true_Imp RS iffD1 RS mp]) 5);
by (ALLGOALS (asm_simp_tac prop_ss));
-val soundness = result();
+qed "soundness";
(*** Towards the completeness proof ***)
@@ -168,7 +168,7 @@
by (rtac (consI1 RS thms.H RS thms_MP) 1);
by (rtac (premp RS weaken_left_cons) 2);
by (REPEAT (ares_tac prop.intrs 1));
-val Imp_Fls = result();
+qed "Imp_Fls";
(*Typical example of strengthening the induction formula*)
val [major] = goal PropLog.thy
@@ -180,7 +180,7 @@
Fls_Imp RS weaken_left_Un2]));
by (ALLGOALS (fast_tac (ZF_cs addIs [weaken_left_Un1, weaken_left_Un2,
weaken_right, Imp_Fls])));
-val hyps_thms_if = result();
+qed "hyps_thms_if";
(*Key lemma for completeness; yields a set of assumptions satisfying p*)
val [premp,sat] = goalw PropLog.thy [logcon_def]
@@ -188,7 +188,7 @@
by (rtac (sat RS spec RS mp RS if_P RS subst) 1 THEN
rtac (premp RS hyps_thms_if) 2);
by (fast_tac ZF_cs 1);
-val logcon_thms_p = result();
+qed "logcon_thms_p";
(*For proving certain theorems in our new propositional logic*)
val thms_cs =
@@ -201,7 +201,7 @@
by (rtac (deduction RS deduction) 1);
by (rtac (thms.DN RS thms_MP) 1);
by (ALLGOALS (best_tac (thms_cs addSIs prems)));
-val thms_excluded_middle = result();
+qed "thms_excluded_middle";
(*Hard to prove directly because it requires cuts*)
val prems = goal PropLog.thy
@@ -222,7 +222,7 @@
by (fast_tac (ZF_cs addSEs prop.free_SEs) 1);
by (asm_simp_tac prop_ss 1);
by (fast_tac ZF_cs 1);
-val hyps_Diff = result();
+qed "hyps_Diff";
(*For the case hyps(p,t)-cons(#v => Fls,Y) |- p;
we also have hyps(p,t)-{#v=>Fls} <= hyps(p, cons(v,t)) *)
@@ -234,7 +234,7 @@
by (fast_tac (ZF_cs addSEs prop.free_SEs) 1);
by (asm_simp_tac prop_ss 1);
by (fast_tac ZF_cs 1);
-val hyps_cons = result();
+qed "hyps_cons";
(** Two lemmas for use with weaken_left **)
@@ -254,7 +254,7 @@
by (asm_simp_tac (prop_ss addsimps (Fin.intrs @ [UN_I, cons_iff])
setloop (split_tac [expand_if])) 2);
by (ALLGOALS (asm_simp_tac (prop_ss addsimps [Un_0, Fin.emptyI, Fin_UnI])));
-val hyps_finite = result();
+qed "hyps_finite";
val Diff_weaken_left = subset_refl RSN (2, Diff_mono) RS weaken_left;
@@ -281,19 +281,19 @@
by (rtac (cons_Diff_subset2 RS weaken_left) 1);
by (rtac (premp RS hyps_cons RS Diff_weaken_left) 1);
by (etac spec 1);
-val completeness_0_lemma = result();
+qed "completeness_0_lemma";
(*The base case for completeness*)
val [premp,sat] = goal PropLog.thy "[| p: prop; 0 |= p |] ==> 0 |- p";
by (rtac (Diff_cancel RS subst) 1);
by (rtac (sat RS (premp RS completeness_0_lemma RS spec)) 1);
-val completeness_0 = result();
+qed "completeness_0";
(*A semantic analogue of the Deduction Theorem*)
goalw PropLog.thy [logcon_def] "!!H p q. [| cons(p,H) |= q |] ==> H |= p=>q";
by (simp_tac prop_ss 1);
by (fast_tac ZF_cs 1);
-val logcon_Imp = result();
+qed "logcon_Imp";
goal PropLog.thy "!!H. H: Fin(prop) ==> ALL p:prop. H |= p --> H |- p";
by (etac Fin_induct 1);
@@ -301,13 +301,13 @@
by (rtac (weaken_left_cons RS thms_MP) 1);
by (fast_tac (ZF_cs addSIs (logcon_Imp::prop.intrs)) 1);
by (fast_tac thms_cs 1);
-val completeness_lemma = result();
+qed "completeness_lemma";
val completeness = completeness_lemma RS bspec RS mp;
val [finite] = goal PropLog.thy "H: Fin(prop) ==> H |- p <-> H |= p & p:prop";
by (fast_tac (ZF_cs addSEs [soundness, finite RS completeness,
thms_in_pl]) 1);
-val thms_iff = result();
+qed "thms_iff";
writeln"Reached end of file.";
--- a/src/ZF/ex/Ramsey.ML Wed Dec 14 10:26:30 1994 +0100
+++ b/src/ZF/ex/Ramsey.ML Wed Dec 14 11:41:49 1994 +0100
@@ -24,21 +24,21 @@
goalw Ramsey.thy [Clique_def] "Clique(0,V,E)";
by (fast_tac ZF_cs 1);
-val Clique0 = result();
+qed "Clique0";
goalw Ramsey.thy [Clique_def]
"!!C V E. [| Clique(C,V',E); V'<=V |] ==> Clique(C,V,E)";
by (fast_tac ZF_cs 1);
-val Clique_superset = result();
+qed "Clique_superset";
goalw Ramsey.thy [Indept_def] "Indept(0,V,E)";
by (fast_tac ZF_cs 1);
-val Indept0 = result();
+qed "Indept0";
val prems = goalw Ramsey.thy [Indept_def]
"!!I V E. [| Indept(I,V',E); V'<=V |] ==> Indept(I,V,E)";
by (fast_tac ZF_cs 1);
-val Indept_superset = result();
+qed "Indept_superset";
(*** Atleast ***)
@@ -118,11 +118,11 @@
(*proving the condition*)
by (asm_simp_tac (arith_ss addsimps [add_succ_right]) 1);
by (etac Atleast_superset 1 THEN fast_tac ZF_cs 1);
-val pigeon2_lemma = result();
+qed "pigeon2_lemma";
(* [| m:nat; n:nat; Atleast(m #+ n #- succ(0), A Un B) |] ==>
Atleast(m,A) | Atleast(n,B) *)
-val pigeon2 = standard (pigeon2_lemma RS bspec RS spec RS spec RS mp);
+bind_thm ("pigeon2", (pigeon2_lemma RS bspec RS spec RS spec RS mp));
(**** Ramsey's Theorem ****)
@@ -131,11 +131,11 @@
goalw Ramsey.thy [Ramsey_def] "Ramsey(n,0,j)";
by (fast_tac (ZF_cs addIs [Clique0,Atleast0]) 1);
-val Ramsey0j = result();
+qed "Ramsey0j";
goalw Ramsey.thy [Ramsey_def] "Ramsey(n,i,0)";
by (fast_tac (ZF_cs addIs [Indept0,Atleast0]) 1);
-val Ramseyi0 = result();
+qed "Ramseyi0";
(** Lemmas for induction step **)
@@ -149,7 +149,7 @@
by (rtac Atleast_superset 3);
by (REPEAT (resolve_tac prems 1));
by (fast_tac ZF_cs 1);
-val Atleast_partition = result();
+qed "Atleast_partition";
(*For the Atleast part, proves ~(a:I) from the second premise!*)
val prems = goalw Ramsey.thy [Symmetric_def,Indept_def]
@@ -158,7 +158,7 @@
\ Indept(cons(a,I), V, E) & Atleast(succ(j), cons(a,I))";
by (cut_facts_tac prems 1);
by (fast_tac (ZF_cs addSEs [Atleast_succI]) 1); (*34 secs*)
-val Indept_succ = result();
+qed "Indept_succ";
val prems = goalw Ramsey.thy [Symmetric_def,Clique_def]
"[| Symmetric(E); Clique(C, {z: V-{a}. <a,z>:E}, E); a: V; \
@@ -166,7 +166,7 @@
\ Clique(cons(a,C), V, E) & Atleast(succ(j), cons(a,C))";
by (cut_facts_tac prems 1);
by (fast_tac (ZF_cs addSEs [Atleast_succI]) 1); (*41 secs*)
-val Clique_succ = result();
+qed "Clique_succ";
(** Induction step **)
@@ -193,7 +193,7 @@
by (rtac exI 1);
by (REPEAT (ares_tac [Clique_succ] 1)); (*make a bigger Clique*)
by (fast_tac (ZF_cs addEs [Indept_superset]) 1); (*easy -- given an Indept*)
-val Ramsey_step_lemma = result();
+qed "Ramsey_step_lemma";
(** The actual proof **)
@@ -211,7 +211,7 @@
by (rtac bexI 1);
by (rtac Ramsey_step_lemma 1);
by (REPEAT (ares_tac [nat_succI,add_type] 1));
-val ramsey_lemma = result();
+qed "ramsey_lemma";
(*Final statement in a tidy form, without succ(...) *)
val prems = goal Ramsey.thy
@@ -219,7 +219,7 @@
by (rtac (ramsey_lemma RS bspec RS bexE) 1);
by (etac bexI 3);
by (REPEAT (ares_tac (prems@[nat_succI]) 1));
-val ramsey = result();
+qed "ramsey";
(*Compute Ramsey numbers according to proof above -- which, actually,
does not constrain the base case values at all!*)
--- a/src/ZF/ex/Rmap.ML Wed Dec 14 10:26:30 1994 +0100
+++ b/src/ZF/ex/Rmap.ML Wed Dec 14 11:41:49 1994 +0100
@@ -13,10 +13,10 @@
by (REPEAT (rtac rmap.bnd_mono 1));
by (REPEAT (ares_tac ([Sigma_mono, list_mono, domain_mono, range_mono] @
basic_monos) 1));
-val rmap_mono = result();
+qed "rmap_mono";
-val rmap_induct = standard
- (rmap.mutual_induct RS spec RS spec RSN (2,rev_mp));
+bind_thm ("rmap_induct",
+ (rmap.mutual_induct RS spec RS spec RSN (2,rev_mp)));
val Nil_rmap_case = rmap.mk_cases list.con_defs "<Nil,zs> : rmap(r)"
and Cons_rmap_case = rmap.mk_cases list.con_defs "<Cons(x,xs),zs> : rmap(r)";
@@ -28,20 +28,20 @@
by (rtac (rmap.dom_subset RS subset_trans) 1);
by (REPEAT (ares_tac [domain_rel_subset, range_rel_subset,
Sigma_mono, list_mono] 1));
-val rmap_rel_type = result();
+qed "rmap_rel_type";
goal Rmap.thy
"!!r. A <= domain(r) ==> list(A) <= domain(rmap(r))";
by (resolve_tac [subsetI] 1);
by (etac list.induct 1);
by (ALLGOALS (fast_tac rmap_cs));
-val rmap_total = result();
+qed "rmap_total";
goalw Rmap.thy [function_def] "!!r. function(r) ==> function(rmap(r))";
by (rtac (impI RS allI RS allI) 1);
by (etac rmap_induct 1);
by (ALLGOALS (fast_tac rmap_cs));
-val rmap_functional = result();
+qed "rmap_functional";
(** If f is a function then rmap(f) behaves as expected. **)
@@ -49,14 +49,14 @@
goal Rmap.thy "!!f. f: A->B ==> rmap(f): list(A)->list(B)";
by (asm_full_simp_tac
(ZF_ss addsimps [Pi_iff, rmap_rel_type, rmap_functional, rmap_total]) 1);
-val rmap_fun_type = result();
+qed "rmap_fun_type";
goalw Rmap.thy [apply_def] "rmap(f)`Nil = Nil";
by (fast_tac (rmap_cs addIs [the_equality]) 1);
-val rmap_Nil = result();
+qed "rmap_Nil";
goal Rmap.thy "!!f. [| f: A->B; x: A; xs: list(A) |] ==> \
\ rmap(f) ` Cons(x,xs) = Cons(f`x, rmap(f)`xs)";
by (rtac apply_equality 1);
by (REPEAT (ares_tac ([apply_Pair, rmap_fun_type] @ rmap.intrs) 1));
-val rmap_Cons = result();
+qed "rmap_Cons";
--- a/src/ZF/ex/TF.ML Wed Dec 14 10:26:30 1994 +0100
+++ b/src/ZF/ex/TF.ML Wed Dec 14 11:41:49 1994 +0100
@@ -21,16 +21,16 @@
goalw TF.thy [tree_def] "tree(A) <= tree_forest(A)";
by (rtac Part_subset 1);
-val tree_subset_TF = result();
+qed "tree_subset_TF";
goalw TF.thy [forest_def] "forest(A) <= tree_forest(A)";
by (rtac Part_subset 1);
-val forest_subset_TF = result();
+qed "forest_subset_TF";
goal TF.thy "tree(A) Un forest(A) = tree_forest(A)";
by (safe_tac (subset_cs addSIs [equalityI, tree_subset_TF, forest_subset_TF]));
by (fast_tac (ZF_cs addSIs tree_forest.intrs addEs [tree_forest.elim]) 1);
-val TF_equals_Un = result();
+qed "TF_equals_Un";
(** NOT useful, but interesting... **)
@@ -50,13 +50,13 @@
"tree(A) = {Inl(x). x: A*forest(A)}";
by (rtac (Part_Inl RS subst) 1);
by (rtac (tree_forest_unfold' RS subst_context) 1);
-val tree_unfold = result();
+qed "tree_unfold";
goalw TF.thy [tree_def, forest_def]
"forest(A) = {Inr(x). x: {0} + tree(A)*forest(A)}";
by (rtac (Part_Inr RS subst) 1);
by (rtac (tree_forest_unfold' RS subst_context) 1);
-val forest_unfold = result();
+qed "forest_unfold";
(*** TF_rec -- by Vset recursion ***)
@@ -112,7 +112,7 @@
by (rewtac Ball_def);
by (rtac tree_forest.mutual_induct 1);
by (ALLGOALS (asm_simp_tac (TF_rec_ss addsimps prems)));
-val tree_forest_rec_type = result();
+qed "tree_forest_rec_type";
(** Versions for use with definitions **)
@@ -121,19 +121,19 @@
"[| !!z. j(z)==TF_rec(z,b,c,d) |] ==> j(Tcons(a,f)) = b(a,f,j(f))";
by (rewtac rew);
by (rtac TF_rec_Tcons 1);
-val def_TF_rec_Tcons = result();
+qed "def_TF_rec_Tcons";
val [rew] = goal TF.thy
"[| !!z. j(z)==TF_rec(z,b,c,d) |] ==> j(Fnil) = c";
by (rewtac rew);
by (rtac TF_rec_Fnil 1);
-val def_TF_rec_Fnil = result();
+qed "def_TF_rec_Fnil";
val [rew] = goal TF.thy
"[| !!z. j(z)==TF_rec(z,b,c,d) |] ==> j(Fcons(t,f)) = d(t,f,j(t),j(f))";
by (rewtac rew);
by (rtac TF_rec_Fcons 1);
-val def_TF_rec_Fcons = result();
+qed "def_TF_rec_Fcons";
fun TF_recs def = map standard
([def] RL [def_TF_rec_Tcons, def_TF_rec_Fnil, def_TF_rec_Fcons]);
@@ -147,14 +147,14 @@
goalw TF.thy [list_of_TF_def]
"!!z A. z: tree_forest(A) ==> list_of_TF(z) : list(tree(A))";
by (REPEAT (ares_tac ([TF_rec_type,TconsI] @ list_typechecks) 1));
-val list_of_TF_type = result();
+qed "list_of_TF_type";
val [TF_of_list_Nil,TF_of_list_Cons] = list_recs TF_of_list_def;
goalw TF.thy [TF_of_list_def]
"!!l A. l: list(tree(A)) ==> TF_of_list(l) : forest(A)";
by (REPEAT (ares_tac [list_rec_type, FnilI, FconsI] 1));
-val TF_of_list_type = result();
+qed "TF_of_list_type";
(** TF_map **)
@@ -167,7 +167,7 @@
\ (ALL f: forest(A). TF_map(h,f) : forest(B))";
by (REPEAT
(ares_tac ([tree_forest_rec_type, TconsI, FnilI, FconsI] @ prems) 1));
-val TF_map_type = result();
+qed "TF_map_type";
(** TF_size **)
@@ -177,7 +177,7 @@
goalw TF.thy [TF_size_def]
"!!z A. z: tree_forest(A) ==> TF_size(z) : nat";
by (REPEAT (ares_tac [TF_rec_type, add_type, nat_0I, nat_succI] 1));
-val TF_size_type = result();
+qed "TF_size_type";
(** TF_preorder **)
@@ -188,7 +188,7 @@
goalw TF.thy [TF_preorder_def]
"!!z A. z: tree_forest(A) ==> TF_preorder(z) : list(A)";
by (REPEAT (ares_tac ([TF_rec_type, app_type] @ list.intrs) 1));
-val TF_preorder_type = result();
+qed "TF_preorder_type";
(** Term simplification **)
@@ -221,31 +221,31 @@
\ |] ==> R(f)";
by (rtac (major RS (tree_forest.mutual_induct RS conjunct2 RS spec RSN (2,rev_mp))) 1);
by (REPEAT (ares_tac (TrueI::prems) 1));
-val forest_induct = result();
+qed "forest_induct";
goal TF.thy "!!f A. f: forest(A) ==> TF_of_list(list_of_TF(f)) = f";
by (etac forest_induct 1);
by (ALLGOALS (asm_simp_tac TF_ss));
-val forest_iso = result();
+qed "forest_iso";
goal TF.thy
"!!ts. ts: list(tree(A)) ==> list_of_TF(TF_of_list(ts)) = ts";
by (etac list.induct 1);
by (ALLGOALS (asm_simp_tac TF_ss));
-val tree_list_iso = result();
+qed "tree_list_iso";
(** theorems about TF_map **)
goal TF.thy "!!z A. z: tree_forest(A) ==> TF_map(%u.u, z) = z";
by (etac tree_forest.induct 1);
by (ALLGOALS (asm_simp_tac TF_ss));
-val TF_map_ident = result();
+qed "TF_map_ident";
goal TF.thy
"!!z A. z: tree_forest(A) ==> TF_map(h, TF_map(j,z)) = TF_map(%u.h(j(u)), z)";
by (etac tree_forest.induct 1);
by (ALLGOALS (asm_simp_tac TF_ss));
-val TF_map_compose = result();
+qed "TF_map_compose";
(** theorems about TF_size **)
@@ -253,13 +253,13 @@
"!!z A. z: tree_forest(A) ==> TF_size(TF_map(h,z)) = TF_size(z)";
by (etac tree_forest.induct 1);
by (ALLGOALS (asm_simp_tac TF_ss));
-val TF_size_TF_map = result();
+qed "TF_size_TF_map";
goal TF.thy
"!!z A. z: tree_forest(A) ==> TF_size(z) = length(TF_preorder(z))";
by (etac tree_forest.induct 1);
by (ALLGOALS (asm_simp_tac (TF_ss addsimps [length_app])));
-val TF_size_length = result();
+qed "TF_size_length";
(** theorems about TF_preorder **)
@@ -267,4 +267,4 @@
\ TF_preorder(TF_map(h,z)) = map(h, TF_preorder(z))";
by (etac tree_forest.induct 1);
by (ALLGOALS (asm_simp_tac (TF_ss addsimps [map_app_distrib])));
-val TF_preorder_TF_map = result();
+qed "TF_preorder_TF_map";
--- a/src/ZF/ex/Term.ML Wed Dec 14 10:26:30 1994 +0100
+++ b/src/ZF/ex/Term.ML Wed Dec 14 11:41:49 1994 +0100
@@ -14,7 +14,7 @@
by (fast_tac (sum_cs addSIs (equalityI :: map rew intrs)
addEs [rew elim]) 1)
end;
-val term_unfold = result();
+qed "term_unfold";
(*Induction on term(A) followed by induction on List *)
val major::prems = goal Term.thy
@@ -27,7 +27,7 @@
by (etac list.induct 1);
by (etac CollectE 2);
by (REPEAT (ares_tac (prems@[list_CollectD]) 1));
-val term_induct2 = result();
+qed "term_induct2";
(*Induction on term(A) to prove an equation*)
val major::prems = goal Term.thy
@@ -46,7 +46,7 @@
by (rtac lfp_mono 1);
by (REPEAT (rtac term.bnd_mono 1));
by (REPEAT (ares_tac (univ_mono::basic_monos) 1));
-val term_mono = result();
+qed "term_mono";
(*Easily provable by induction also*)
goalw Term.thy (term.defs@term.con_defs) "term(univ(A)) <= univ(A)";
@@ -54,14 +54,14 @@
by (rtac (A_subset_univ RS univ_mono) 2);
by (safe_tac ZF_cs);
by (REPEAT (ares_tac [Pair_in_univ, list_univ RS subsetD] 1));
-val term_univ = result();
+qed "term_univ";
val term_subset_univ =
term_mono RS (term_univ RSN (2,subset_trans)) |> standard;
goal Term.thy "!!t A B. [| t: term(A); A <= univ(B) |] ==> t: univ(B)";
by (REPEAT (ares_tac [term_subset_univ RS subsetD] 1));
-val term_into_univ = result();
+qed "term_into_univ";
(*** term_rec -- by Vset recursion ***)
@@ -76,7 +76,7 @@
by (forward_tac [rank_Cons1 RS lt_trans] 1);
by (dtac (rank_Cons2 RS lt_trans) 1);
by (asm_simp_tac (list_ss addsimps [ordi, VsetI]) 1);
-val map_lemma = result();
+qed "map_lemma";
(*Typing premise is necessary to invoke map_lemma*)
val [prem] = goal Term.thy
@@ -103,7 +103,7 @@
by (ALLGOALS (asm_simp_tac (list_ss addsimps [term_rec])));
by (etac CollectE 1);
by (REPEAT (ares_tac [list.Cons_I, UN_I] 1));
-val term_rec_type = result();
+qed "term_rec_type";
val [rew,tslist] = goal Term.thy
"[| !!t. j(t)==term_rec(t,d); ts: list(A) |] ==> \
@@ -124,7 +124,7 @@
(** term_map **)
-val term_map = standard (term_map_def RS def_term_rec);
+bind_thm ("term_map", (term_map_def RS def_term_rec));
val prems = goalw Term.thy [term_map_def]
"[| t: term(A); !!x. x: A ==> f(x): B |] ==> term_map(f,t) : term(B)";
@@ -140,29 +140,29 @@
(** term_size **)
-val term_size = standard (term_size_def RS def_term_rec);
+bind_thm ("term_size", (term_size_def RS def_term_rec));
goalw Term.thy [term_size_def] "!!t A. t: term(A) ==> term_size(t) : nat";
by (REPEAT (ares_tac [term_rec_simple_type, list_add_type, nat_succI] 1));
-val term_size_type = result();
+qed "term_size_type";
(** reflect **)
-val reflect = standard (reflect_def RS def_term_rec);
+bind_thm ("reflect", (reflect_def RS def_term_rec));
goalw Term.thy [reflect_def] "!!t A. t: term(A) ==> reflect(t) : term(A)";
by (REPEAT (ares_tac [term_rec_simple_type, rev_type, term.Apply_I] 1));
-val reflect_type = result();
+qed "reflect_type";
(** preorder **)
-val preorder = standard (preorder_def RS def_term_rec);
+bind_thm ("preorder", (preorder_def RS def_term_rec));
goalw Term.thy [preorder_def]
"!!t A. t: term(A) ==> preorder(t) : list(A)";
by (REPEAT (ares_tac [term_rec_simple_type, list.Cons_I, flat_type] 1));
-val preorder_type = result();
+qed "preorder_type";
(** Term simplification **)
@@ -182,19 +182,19 @@
goal Term.thy "!!t A. t: term(A) ==> term_map(%u.u, t) = t";
by (etac term_induct_eqn 1);
by (asm_simp_tac (term_ss addsimps [map_ident]) 1);
-val term_map_ident = result();
+qed "term_map_ident";
goal Term.thy
"!!t A. t: term(A) ==> term_map(f, term_map(g,t)) = term_map(%u.f(g(u)), t)";
by (etac term_induct_eqn 1);
by (asm_simp_tac (term_ss addsimps [map_compose]) 1);
-val term_map_compose = result();
+qed "term_map_compose";
goal Term.thy
"!!t A. t: term(A) ==> term_map(f, reflect(t)) = reflect(term_map(f,t))";
by (etac term_induct_eqn 1);
by (asm_simp_tac (term_ss addsimps [rev_map_distrib RS sym, map_compose]) 1);
-val term_map_reflect = result();
+qed "term_map_reflect";
(** theorems about term_size **)
@@ -203,18 +203,18 @@
"!!t A. t: term(A) ==> term_size(term_map(f,t)) = term_size(t)";
by (etac term_induct_eqn 1);
by (asm_simp_tac (term_ss addsimps [map_compose]) 1);
-val term_size_term_map = result();
+qed "term_size_term_map";
goal Term.thy "!!t A. t: term(A) ==> term_size(reflect(t)) = term_size(t)";
by (etac term_induct_eqn 1);
by (asm_simp_tac (term_ss addsimps [rev_map_distrib RS sym, map_compose,
list_add_rev]) 1);
-val term_size_reflect = result();
+qed "term_size_reflect";
goal Term.thy "!!t A. t: term(A) ==> term_size(t) = length(preorder(t))";
by (etac term_induct_eqn 1);
by (asm_simp_tac (term_ss addsimps [length_flat, map_compose]) 1);
-val term_size_length = result();
+qed "term_size_length";
(** theorems about reflect **)
@@ -223,7 +223,7 @@
by (etac term_induct_eqn 1);
by (asm_simp_tac (term_ss addsimps [rev_map_distrib, map_compose,
map_ident, rev_rev_ident]) 1);
-val reflect_reflect_ident = result();
+qed "reflect_reflect_ident";
(** theorems about preorder **)
@@ -232,7 +232,7 @@
"!!t A. t: term(A) ==> preorder(term_map(f,t)) = map(f, preorder(t))";
by (etac term_induct_eqn 1);
by (asm_simp_tac (term_ss addsimps [map_compose, map_flat]) 1);
-val preorder_term_map = result();
+qed "preorder_term_map";
(** preorder(reflect(t)) = rev(postorder(t)) **)
--- a/src/ZF/ex/misc.ML Wed Dec 14 10:26:30 1994 +0100
+++ b/src/ZF/ex/misc.ML Wed Dec 14 11:41:49 1994 +0100
@@ -53,7 +53,7 @@
by (safe_tac ZF_cs);
by (asm_simp_tac hom_ss 1);
by (asm_simp_tac hom_ss 1);
-val comp_homs = result();
+qed "comp_homs";
(** A characterization of functions, suggested by Tobias Nipkow **)
@@ -98,7 +98,7 @@
\ (g O f O h): surj(C,C); \
\ f: A->B; g: B->C; h: C->A |] ==> h: bij(C,A)";
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1));
-val pastre1 = result();
+qed "pastre1";
val prems = goalw Perm.thy [bij_def]
"[| (h O g O f): surj(A,A); \
@@ -106,7 +106,7 @@
\ (g O f O h): surj(C,C); \
\ f: A->B; g: B->C; h: C->A |] ==> h: bij(C,A)";
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1));
-val pastre2 = result();
+qed "pastre2";
val prems = goalw Perm.thy [bij_def]
"[| (h O g O f): surj(A,A); \
@@ -114,7 +114,7 @@
\ (g O f O h): inj(C,C); \
\ f: A->B; g: B->C; h: C->A |] ==> h: bij(C,A)";
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1));
-val pastre3 = result();
+qed "pastre3";
val prems = goalw Perm.thy [bij_def]
"[| (h O g O f): surj(A,A); \
@@ -122,7 +122,7 @@
\ (g O f O h): inj(C,C); \
\ f: A->B; g: B->C; h: C->A |] ==> h: bij(C,A)";
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1));
-val pastre4 = result();
+qed "pastre4";
val prems = goalw Perm.thy [bij_def]
"[| (h O g O f): inj(A,A); \
@@ -130,7 +130,7 @@
\ (g O f O h): inj(C,C); \
\ f: A->B; g: B->C; h: C->A |] ==> h: bij(C,A)";
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1));
-val pastre5 = result();
+qed "pastre5";
val prems = goalw Perm.thy [bij_def]
"[| (h O g O f): inj(A,A); \
@@ -138,7 +138,7 @@
\ (g O f O h): surj(C,C); \
\ f: A->B; g: B->C; h: C->A |] ==> h: bij(C,A)";
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1));
-val pastre6 = result();
+qed "pastre6";
(** Yet another example... **)
--- a/src/ZF/pair.ML Wed Dec 14 10:26:30 1994 +0100
+++ b/src/ZF/pair.ML Wed Dec 14 11:41:49 1994 +0100
@@ -18,7 +18,7 @@
(fn _=> [ (simp_tac (FOL_ss addsimps [doubleton_iff]) 1),
(fast_tac FOL_cs 1) ]);
-val Pair_inject = standard (Pair_iff RS iffD1 RS conjE);
+bind_thm ("Pair_inject", (Pair_iff RS iffD1 RS conjE));
qed_goal "Pair_inject1" ZF.thy "<a,b> = <c,d> ==> a=c"
(fn [major]=>
--- a/src/ZF/subset.ML Wed Dec 14 10:26:30 1994 +0100
+++ b/src/ZF/subset.ML Wed Dec 14 11:41:49 1994 +0100
@@ -24,7 +24,7 @@
(*A safe special case of subset elimination, adding no new variables
[| cons(a,B) <= C; [| a : C; B <= C |] ==> R |] ==> R *)
-val cons_subsetE = standard (cons_subset_iff RS iffD1 RS conjE);
+bind_thm ("cons_subsetE", (cons_subset_iff RS iffD1 RS conjE));
qed_goal "subset_empty_iff" ZF.thy "A<=0 <-> A=0"
(fn _=> [ (fast_tac (upair_cs addIs [equalityI]) 1) ]);