# HG changeset patch # User clasohm # Date 787401709 -3600 # Node ID 200a16083201b198acf3f11a0169eff761616173 # Parent 9ab8873bf9b3c0bb62417d9791b4812bf704ccf2 added bind_thm for theorems defined by "standard ..." diff -r 9ab8873bf9b3 -r 200a16083201 src/ZF/Cardinal.ML --- 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); diff -r 9ab8873bf9b3 -r 200a16083201 src/ZF/CardinalArith.ML --- 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. ")] 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 diff -r 9ab8873bf9b3 -r 200a16083201 src/ZF/Epsilon.ML --- 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}) |] ==> \ diff -r 9ab8873bf9b3 -r 200a16083201 src/ZF/List.ML --- 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 ***) diff -r 9ab8873bf9b3 -r 200a16083201 src/ZF/Order.ML --- 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; \ diff -r 9ab8873bf9b3 -r 200a16083201 src/ZF/OrderArith.ML --- 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 **) diff -r 9ab8873bf9b3 -r 200a16083201 src/ZF/OrderType.ML --- 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 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=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"; diff -r 9ab8873bf9b3 -r 200a16083201 src/ZF/Ordinal.ML --- 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 i 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; \ diff -r 9ab8873bf9b3 -r 200a16083201 src/ZF/QPair.ML --- 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=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=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] diff -r 9ab8873bf9b3 -r 200a16083201 src/ZF/QUniv.ML --- 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 " : 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 : Vfrom(X,i) implies a, b : Vfrom(X,i), which is useless for induction. diff -r 9ab8873bf9b3 -r 200a16083201 src/ZF/Sum.ML --- 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] diff -r 9ab8873bf9b3 -r 200a16083201 src/ZF/Trancl.ML --- 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) |] ==> : r^*"; diff -r 9ab8873bf9b3 -r 200a16083201 src/ZF/Univ.ML --- 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 **) diff -r 9ab8873bf9b3 -r 200a16083201 src/ZF/WF.ML --- 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); \ diff -r 9ab8873bf9b3 -r 200a16083201 src/ZF/ex/Acc.ML --- 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. :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); : 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"; diff -r 9ab8873bf9b3 -r 200a16083201 src/ZF/ex/BT.ML --- 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"; diff -r 9ab8873bf9b3 -r 200a16083201 src/ZF/ex/Bin.ML --- 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 ***) diff -r 9ab8873bf9b3 -r 200a16083201 src/ZF/ex/Brouwer.ML --- 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"; diff -r 9ab8873bf9b3 -r 200a16083201 src/ZF/ex/CoUnit.ML --- 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"; diff -r 9ab8873bf9b3 -r 200a16083201 src/ZF/ex/Comb.ML --- 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."; diff -r 9ab8873bf9b3 -r 200a16083201 src/ZF/ex/Data.ML --- 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)); diff -r 9ab8873bf9b3 -r 200a16083201 src/ZF/ex/Integ.ML --- 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#+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``{}))"; 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``{}) = intrel `` {}"; @@ -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 |] ==> \ diff -r 9ab8873bf9b3 -r 200a16083201 src/ZF/ex/LList.ML --- 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'. : 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) |] ==> : 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"; diff -r 9ab8873bf9b3 -r 200a16083201 src/ZF/ex/ListN.ML --- 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 " : 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. [| : listn(A); : listn(A) |] ==> \ \ : 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 " : listn(A)" and Cons_listn_case = listn.mk_cases list.con_defs " : listn(A)"; diff -r 9ab8873bf9b3 -r 200a16083201 src/ZF/ex/Ntree.ML --- 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"; diff -r 9ab8873bf9b3 -r 200a16083201 src/ZF/ex/Primrec.ML --- 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 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"; diff -r 9ab8873bf9b3 -r 200a16083201 src/ZF/ex/PropLog.ML --- 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."; diff -r 9ab8873bf9b3 -r 200a16083201 src/ZF/ex/Ramsey.ML --- 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}. :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!*) diff -r 9ab8873bf9b3 -r 200a16083201 src/ZF/ex/Rmap.ML --- 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 " : rmap(r)" and Cons_rmap_case = rmap.mk_cases list.con_defs " : 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"; diff -r 9ab8873bf9b3 -r 200a16083201 src/ZF/ex/TF.ML --- 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"; diff -r 9ab8873bf9b3 -r 200a16083201 src/ZF/ex/Term.ML --- 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)) **) diff -r 9ab8873bf9b3 -r 200a16083201 src/ZF/ex/misc.ML --- 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... **) diff -r 9ab8873bf9b3 -r 200a16083201 src/ZF/pair.ML --- 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=c" (fn [major]=> diff -r 9ab8873bf9b3 -r 200a16083201 src/ZF/subset.ML --- 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) ]);