--- a/src/ZF/AC.ML Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/AC.ML Thu Sep 07 21:12:49 2000 +0200
@@ -7,7 +7,7 @@
*)
(*The same as AC, but no premise a:A*)
-val [nonempty] = goal AC.thy
+val [nonempty] = goal (the_context ())
"[| !!x. x:A ==> (EX y. y:B(x)) |] ==> EX z. z : Pi(A,B)";
by (excluded_middle_tac "A=0" 1);
by (asm_simp_tac (simpset() addsimps [Pi_empty1]) 2 THEN Blast_tac 2);
@@ -28,7 +28,7 @@
by (Blast_tac 1);
qed "AC_Pi_Pow";
-val [nonempty] = goal AC.thy
+val [nonempty] = goal (the_context ())
"[| !!x. x:A ==> (EX y. y:x) \
\ |] ==> EX f: A->Union(A). ALL x:A. f`x : x";
by (res_inst_tac [("B1", "%x. x")] (AC_Pi RS exE) 1);
--- a/src/ZF/Arith.ML Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/Arith.ML Thu Sep 07 21:12:49 2000 +0200
@@ -15,7 +15,7 @@
*)
Addsimps [rec_type, nat_0_le];
-val nat_typechecks = [rec_type, nat_0I, nat_1I, nat_succI, Ord_nat];
+bind_thms ("nat_typechecks", [rec_type, nat_0I, nat_1I, nat_succI, Ord_nat]);
Goal "[| 0<k; k: nat |] ==> EX j: nat. k = succ(j)";
by (etac rev_mp 1);
@@ -261,7 +261,7 @@
qed "add_left_commute";
(*Addition is an AC-operator*)
-val add_ac = [add_assoc, add_commute, add_left_commute];
+bind_thms ("add_ac", [add_assoc, add_commute, add_left_commute]);
(*Cancellation law on the left*)
Goal "[| raw_add(k, m) = raw_add(k, n); k:nat |] ==> m=n";
@@ -496,6 +496,4 @@
by (rtac (mult_commute RS subst_context) 1);
qed "mult_left_commute";
-val mult_ac = [mult_assoc,mult_commute,mult_left_commute];
-
-
+bind_thms ("mult_ac", [mult_assoc,mult_commute,mult_left_commute]);
--- a/src/ZF/ArithSimp.ML Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/ArithSimp.ML Thu Sep 07 21:12:49 2000 +0200
@@ -75,10 +75,10 @@
by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_le_self])));
qed "div_termination";
-val div_rls = (*for mod and div*)
+bind_thms ("div_rls", (*for mod and div*)
nat_typechecks @
[Ord_transrec_type, apply_funtype, div_termination RS ltD,
- nat_into_Ord, not_lt_iff_le RS iffD1];
+ nat_into_Ord, not_lt_iff_le RS iffD1]);
val div_ss = simpset() addsimps [div_termination RS ltD,
not_lt_iff_le RS iffD2];
--- a/src/ZF/Bool.ML Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/Bool.ML Thu Sep 07 21:12:49 2000 +0200
@@ -6,7 +6,7 @@
Booleans in Zermelo-Fraenkel Set Theory
*)
-val bool_defs = [bool_def,cond_def];
+bind_thms ("bool_defs", [bool_def,cond_def]);
Goalw [succ_def] "{0} = 1";
by (rtac refl 1);
@@ -30,7 +30,7 @@
qed "one_not_0";
(** 1=0 ==> R **)
-val one_neq_0 = one_not_0 RS notE;
+bind_thm ("one_neq_0", one_not_0 RS notE);
val major::prems = Goalw bool_defs
"[| c: bool; c=1 ==> P; c=0 ==> P |] ==> P";
@@ -77,10 +77,19 @@
fun conds def = [standard (def RS def_cond_1), standard (def RS def_cond_0)];
-val [not_1,not_0] = conds not_def;
-val [and_1,and_0] = conds and_def;
-val [or_1,or_0] = conds or_def;
-val [xor_1,xor_0] = conds xor_def;
+val [not_1, not_0] = conds not_def;
+val [and_1, and_0] = conds and_def;
+val [or_1, or_0] = conds or_def;
+val [xor_1, xor_0] = conds xor_def;
+
+bind_thm ("not_1", not_1);
+bind_thm ("not_0", not_0);
+bind_thm ("and_1", and_1);
+bind_thm ("and_0", and_0);
+bind_thm ("or_1", or_1);
+bind_thm ("or_0", or_0);
+bind_thm ("xor_1", xor_1);
+bind_thm ("xor_0", xor_0);
Addsimps [not_1,not_0,and_1,and_0,or_1,or_0,xor_1,xor_0];
@@ -104,8 +113,8 @@
AddTCs [xor_type];
-val bool_typechecks = [bool_1I, bool_0I, cond_type, not_type, and_type,
- or_type, xor_type];
+bind_thms ("bool_typechecks",
+ [bool_1I, bool_0I, cond_type, not_type, and_type, or_type, xor_type]);
(*** Laws for 'not' ***)
--- a/src/ZF/Cardinal.ML Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/Cardinal.ML Thu Sep 07 21:12:49 2000 +0200
@@ -17,7 +17,7 @@
by (REPEAT (ares_tac [Diff_subset, subset_refl, Diff_mono, image_mono] 1));
qed "decomp_bnd_mono";
-val [gfun] = goal Cardinal.thy
+val [gfun] = goal (the_context ())
"g: Y->X ==> \
\ g``(Y - f`` lfp(X, %W. X - g``(Y - f``W))) = \
\ X - lfp(X, %W. X - g``(Y - f``W)) ";
@@ -38,7 +38,7 @@
by (REPEAT (ares_tac [fun_is_rel, image_subset, lfp_subset] 1));
qed "decomposition";
-val prems = goal Cardinal.thy
+val prems = goal (the_context ())
"[| f: inj(X,Y); g: inj(Y,X) |] ==> EX h. h: bij(X,Y)";
by (cut_facts_tac prems 1);
by (cut_facts_tac [(prems RL [inj_is_fun]) MRS decomposition] 1);
@@ -219,7 +219,7 @@
qed "less_LeastE";
(*Easier to apply than LeastI: conclusion has only one occurrence of P*)
-val prems = goal Cardinal.thy
+val prems = goal (the_context ())
"[| P(i); Ord(i); !!j. P(j) ==> Q(j) |] ==> Q(LEAST j. P(j))";
by (resolve_tac prems 1);
by (rtac LeastI 1);
@@ -333,7 +333,7 @@
by (blast_tac (claset() addSEs [ltE]) 1);
qed "Card_0";
-val [premK,premL] = goal Cardinal.thy
+val [premK,premL] = goal (the_context ())
"[| Card(K); Card(L) |] ==> Card(K Un L)";
by (rtac ([premK RS Card_is_Ord, premL RS Card_is_Ord] MRS Ord_linear_le) 1);
by (asm_simp_tac
@@ -780,7 +780,7 @@
qed "nat_wf_on_converse_Memrel";
Goal "n:nat ==> well_ord(n,converse(Memrel(n)))";
-by (forward_tac [transfer thy Ord_nat RS Ord_in_Ord RS well_ord_Memrel] 1);
+by (forward_tac [transfer (the_context ()) Ord_nat RS Ord_in_Ord RS well_ord_Memrel] 1);
by (rewtac well_ord_def);
by (blast_tac (claset() addSIs [tot_ord_converse,
nat_wf_on_converse_Memrel]) 1);
--- a/src/ZF/CardinalArith.ML Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/CardinalArith.ML Thu Sep 07 21:12:49 2000 +0200
@@ -295,9 +295,9 @@
qed "cmult_2";
-val sum_lepoll_prod = [sum_eq_2_times RS equalityD1 RS subset_imp_lepoll,
+bind_thm ("sum_lepoll_prod", [sum_eq_2_times RS equalityD1 RS subset_imp_lepoll,
asm_rl, lepoll_refl] MRS (prod_lepoll_mono RSN (2, lepoll_trans))
- |> standard;
+ |> standard);
Goal "[| A lepoll B; 2 lepoll A |] ==> A+B lepoll A*B";
by (REPEAT (ares_tac [[sum_lepoll_mono, sum_lepoll_prod]
@@ -791,8 +791,8 @@
(** Theorems by Krzysztof Grabczewski, proofs by lcp **)
-val nat_implies_well_ord =
- (transfer CardinalArith.thy nat_into_Ord) RS well_ord_Memrel;
+bind_thm ("nat_implies_well_ord",
+ (transfer (the_context ()) nat_into_Ord) RS well_ord_Memrel);
Goal "[| m:nat; n:nat |] ==> m + n eqpoll m #+ n";
by (rtac eqpoll_trans 1);
--- a/src/ZF/Cardinal_AC.ML Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/Cardinal_AC.ML Thu Sep 07 21:12:49 2000 +0200
@@ -15,7 +15,7 @@
by (etac well_ord_cardinal_eqpoll 1);
qed "cardinal_eqpoll";
-val cardinal_idem = cardinal_eqpoll RS cardinal_cong;
+bind_thm ("cardinal_idem", cardinal_eqpoll RS cardinal_cong);
Goal "|X| = |Y| ==> X eqpoll Y";
by (resolve_tac [AC_well_ord RS exE] 1);
@@ -160,7 +160,7 @@
by (res_inst_tac [("x1", "f`x")] (UN_upper RSN (2,subset_trans)) 1);
by (eresolve_tac [inj_is_fun RS apply_type] 2 THEN assume_tac 2);
by (asm_simp_tac (simpset() addsimps [inj_is_fun RS apply_rangeI]) 1);
-val inj_UN_subset = result();
+qed "inj_UN_subset";
(*Simpler to require |W|=K; we'd have a bijection; but the theorem would
be weaker.*)
--- a/src/ZF/Epsilon.ML Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/Epsilon.ML Thu Sep 07 21:12:49 2000 +0200
@@ -13,7 +13,7 @@
by (rtac (nat_0I RS UN_upper) 1);
qed "arg_subset_eclose";
-val arg_into_eclose = arg_subset_eclose RS subsetD;
+bind_thm ("arg_into_eclose", arg_subset_eclose RS subsetD);
Goalw [eclose_def,Transset_def] "Transset(eclose(A))";
by (rtac (subsetI RS ballI) 1);
@@ -32,8 +32,8 @@
(* [| A : eclose(B); c : A |] ==> c : eclose(B) *)
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;
+bind_thm ("arg_in_eclose_sing", arg_subset_eclose RS singleton_subsetD);
+bind_thm ("arg_into_eclose_sing", arg_in_eclose_sing RS ecloseD);
(* This is epsilon-induction for eclose(A); see also eclose_induct_down...
[| a: eclose(A); !!x. [| x: eclose(A); ALL y:x. P(y) |] ==> P(x)
@@ -112,11 +112,11 @@
qed "under_Memrel";
(* j : eclose(A) ==> Memrel(eclose(A)) -`` j = j *)
-val under_Memrel_eclose = Transset_eclose RS under_Memrel;
+bind_thm ("under_Memrel_eclose", Transset_eclose RS under_Memrel);
-val wfrec_ssubst = standard (wf_Memrel RS wfrec RS ssubst);
+bind_thm ("wfrec_ssubst", standard (wf_Memrel RS wfrec RS ssubst));
-val [kmemj,jmemi] = goal Epsilon.thy
+val [kmemj,jmemi] = goal (the_context ())
"[| k:eclose({j}); j:eclose({i}) |] ==> \
\ wfrec(Memrel(eclose({i})), k, H) = wfrec(Memrel(eclose({j})), k, H)";
by (rtac (kmemj RS eclose_induct) 1);
--- a/src/ZF/Finite.ML Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/Finite.ML Thu Sep 07 21:12:49 2000 +0200
@@ -19,7 +19,7 @@
qed "Fin_mono";
(* A : Fin(B) ==> A <= B *)
-val FinD = Fin.dom_subset RS subsetD RS PowD;
+bind_thm ("FinD", Fin.dom_subset RS subsetD RS PowD);
(** Induction on finite sets **)
--- a/src/ZF/Fixedpt.ML Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/Fixedpt.ML Thu Sep 07 21:12:49 2000 +0200
@@ -8,8 +8,6 @@
Proved in the lattice of subsets of D, namely Pow(D), with Inter as glb
*)
-open Fixedpt;
-
(*** Monotone operators ***)
val prems = Goalw [bnd_mono_def]
@@ -28,7 +26,7 @@
by (Blast_tac 1);
qed "bnd_monoD2";
-val [major,minor] = goal Fixedpt.thy
+val [major,minor] = goal (the_context ())
"[| bnd_mono(D,h); X<=D |] ==> h(X) <= D";
by (rtac (major RS bnd_monoD2 RS subset_trans) 1);
by (rtac (major RS bnd_monoD1) 3);
@@ -64,7 +62,7 @@
qed "lfp_subset";
(*Used in datatype package*)
-val [rew] = goal Fixedpt.thy "A==lfp(D,h) ==> A <= D";
+val [rew] = goal (the_context ()) "A==lfp(D,h) ==> A <= D";
by (rewtac rew);
by (rtac lfp_subset 1);
qed "def_lfp_subset";
@@ -76,7 +74,7 @@
by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [CollectE,PowD] 1));
qed "lfp_greatest";
-val hmono::prems = goal Fixedpt.thy
+val hmono::prems = goal (the_context ())
"[| bnd_mono(D,h); h(A)<=A; A<=D |] ==> h(lfp(D,h)) <= A";
by (rtac (hmono RS bnd_monoD2 RS subset_trans) 1);
by (rtac lfp_lowerbound 1);
@@ -89,7 +87,7 @@
by (REPEAT (assume_tac 1));
qed "lfp_lemma2";
-val [hmono] = goal Fixedpt.thy
+val [hmono] = goal (the_context ())
"bnd_mono(D,h) ==> lfp(D,h) <= h(lfp(D,h))";
by (rtac lfp_lowerbound 1);
by (rtac (hmono RS bnd_monoD2) 1);
@@ -103,7 +101,7 @@
qed "lfp_Tarski";
(*Definition form, to control unfolding*)
-val [rew,mono] = goal Fixedpt.thy
+val [rew,mono] = goal (the_context ())
"[| A==lfp(D,h); bnd_mono(D,h) |] ==> A = h(A)";
by (rewtac rew);
by (rtac (mono RS lfp_Tarski) 1);
@@ -144,7 +142,7 @@
(*This version is useful when "A" is not a subset of D;
second premise could simply be h(D Int A) <= D or !!X. X<=D ==> h(X)<=D *)
-val [hsub,hmono] = goal Fixedpt.thy
+val [hsub,hmono] = goal (the_context ())
"[| h(D Int A) <= A; bnd_mono(D,h) |] ==> lfp(D,h) <= A";
by (rtac (lfp_lowerbound RS subset_trans) 1);
by (rtac (hmono RS bnd_mono_subset RS Int_greatest) 1);
@@ -189,7 +187,7 @@
qed "gfp_subset";
(*Used in datatype package*)
-val [rew] = goal Fixedpt.thy "A==gfp(D,h) ==> A <= D";
+val [rew] = goal (the_context ()) "A==gfp(D,h) ==> A <= D";
by (rewtac rew);
by (rtac gfp_subset 1);
qed "def_gfp_subset";
@@ -200,7 +198,7 @@
by (fast_tac (subset_cs addIs ((hmono RS bnd_monoD1)::prems)) 1);
qed "gfp_least";
-val hmono::prems = goal Fixedpt.thy
+val hmono::prems = goal (the_context ())
"[| bnd_mono(D,h); A<=h(A); A<=D |] ==> A <= h(gfp(D,h))";
by (rtac (hmono RS bnd_monoD2 RSN (2,subset_trans)) 1);
by (rtac gfp_subset 3);
@@ -214,7 +212,7 @@
by (REPEAT (assume_tac 1));
qed "gfp_lemma2";
-val [hmono] = goal Fixedpt.thy
+val [hmono] = goal (the_context ())
"bnd_mono(D,h) ==> h(gfp(D,h)) <= gfp(D,h)";
by (rtac gfp_upperbound 1);
by (rtac (hmono RS bnd_monoD2) 1);
@@ -227,7 +225,7 @@
qed "gfp_Tarski";
(*Definition form, to control unfolding*)
-val [rew,mono] = goal Fixedpt.thy
+val [rew,mono] = goal (the_context ())
"[| A==gfp(D,h); bnd_mono(D,h) |] ==> A = h(A)";
by (rewtac rew);
by (rtac (mono RS gfp_Tarski) 1);
@@ -241,7 +239,7 @@
by (REPEAT (ares_tac [gfp_upperbound RS subsetD] 1));
qed "weak_coinduct";
-val [subs_h,subs_D,mono] = goal Fixedpt.thy
+val [subs_h,subs_D,mono] = goal (the_context ())
"[| X <= h(X Un gfp(D,h)); X <= D; bnd_mono(D,h) |] ==> \
\ X Un gfp(D,h) <= h(X Un gfp(D,h))";
by (rtac (subs_h RS Un_least) 1);
@@ -259,7 +257,7 @@
qed "coinduct";
(*Definition form, to control unfolding*)
-val rew::prems = goal Fixedpt.thy
+val rew::prems = goal (the_context ())
"[| A == gfp(D,h); bnd_mono(D,h); a: X; X <= h(X Un A); X <= D |] ==> \
\ a : A";
by (rewtac rew);
--- a/src/ZF/InfDatatype.ML Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/InfDatatype.ML Thu Sep 07 21:12:49 2000 +0200
@@ -6,10 +6,10 @@
Infinite-branching datatype definitions
*)
-val fun_Limit_VfromE =
+bind_thm ("fun_Limit_VfromE",
[apply_funtype, InfCard_csucc RS InfCard_is_Limit] MRS
- transfer InfDatatype.thy Limit_VfromE
- |> standard;
+ transfer (the_context ()) Limit_VfromE
+ |> standard);
Goal "[| f: D -> Vfrom(A,csucc(K)); |D| le K; InfCard(K) |] \
\ ==> EX j. f: D -> Vfrom(A,j) & j < csucc(K)";
@@ -54,7 +54,7 @@
qed "fun_in_Vcsucc";
(*Remove <= from the rule above*)
-val fun_in_Vcsucc' = subsetI RSN (4, fun_in_Vcsucc);
+bind_thm ("fun_in_Vcsucc'", subsetI RSN (4, fun_in_Vcsucc));
(** Version where K itself is the index set **)
@@ -93,8 +93,8 @@
UN_upper RS subset_imp_lepoll RS lepoll_imp_Card_le);
(*For most K-branching datatypes with domain Vfrom(A, csucc(K)) *)
-val inf_datatype_intrs =
+bind_thms ("inf_datatype_intrs",
[InfCard_nat, InfCard_nat_Un_cardinal,
Pair_in_Vcsucc, Inl_in_Vcsucc, Inr_in_Vcsucc,
zero_in_Vcsucc, A_into_Vfrom, nat_into_Vcsucc,
- Card_fun_in_Vcsucc, fun_in_Vcsucc', UN_I] @ Data_Arg.intrs;
+ Card_fun_in_Vcsucc, fun_in_Vcsucc', UN_I] @ Data_Arg.intrs);
--- a/src/ZF/Let.ML Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/Let.ML Thu Sep 07 21:12:49 2000 +0200
@@ -6,9 +6,7 @@
Let expressions -- borrowed from HOL
*)
-open Let;
-
-val [prem] = goalw thy
+val [prem] = goalw (the_context ())
[Let_def] "(!!x. x=t ==> P(u(x))) ==> P(let x=t in u(x))";
by (rtac (refl RS prem) 1);
qed "LetI";
--- a/src/ZF/List.ML Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/List.ML Thu Sep 07 21:12:49 2000 +0200
@@ -9,11 +9,11 @@
(*** Aspects of the datatype definition ***)
(*An elimination rule, for type-checking*)
-val ConsE = list.mk_cases "Cons(a,l) : list(A)";
+bind_thm ("ConsE", list.mk_cases "Cons(a,l) : list(A)");
(*Proving freeness results*)
-val Cons_iff = list.mk_free "Cons(a,l)=Cons(a',l') <-> a=a' & l=l'";
-val Nil_Cons_iff = list.mk_free "~ Nil=Cons(a,l)";
+bind_thm ("Cons_iff", list.mk_free "Cons(a,l)=Cons(a',l') <-> a=a' & l=l'");
+bind_thm ("Nil_Cons_iff", list.mk_free "~ Nil=Cons(a,l)");
Goal "list(A) = {0} + (A * list(A))";
let open list; val rew = rewrite_rule con_defs in
@@ -99,7 +99,7 @@
(** map **)
-val prems = Goalw [get_def thy "map_list"]
+val prems = Goalw [get_def (the_context ()) "map_list"]
"[| l: list(A); !!x. x: A ==> h(x): B |] ==> map(h,l) : list(B)";
by (REPEAT (ares_tac (prems @ list.intrs @ [list_rec_type]) 1));
qed "map_type";
@@ -111,21 +111,21 @@
(** length **)
-Goalw [get_def thy "length_list"]
+Goalw [get_def (the_context ()) "length_list"]
"l: list(A) ==> length(l) : nat";
by (REPEAT (ares_tac [list_rec_type, nat_0I, nat_succI] 1));
qed "length_type";
(** app **)
-Goalw [get_def thy "op @_list"]
+Goalw [get_def (the_context ()) "op @_list"]
"[| xs: list(A); ys: list(A) |] ==> xs@ys : list(A)";
by (REPEAT (ares_tac [list_rec_type, list.Cons_I] 1));
qed "app_type";
(** rev **)
-Goalw [get_def thy "rev_list"]
+Goalw [get_def (the_context ()) "rev_list"]
"xs: list(A) ==> rev(xs) : list(A)";
by (REPEAT (ares_tac (list.intrs @ [list_rec_type, app_type]) 1));
qed "rev_type";
@@ -133,7 +133,7 @@
(** flat **)
-Goalw [get_def thy "flat_list"]
+Goalw [get_def (the_context ()) "flat_list"]
"ls: list(list(A)) ==> flat(ls) : list(A)";
by (REPEAT (ares_tac (list.intrs @ [list_rec_type, app_type]) 1));
qed "flat_type";
@@ -141,7 +141,7 @@
(** set_of_list **)
-Goalw [get_def thy "set_of_list_list"]
+Goalw [get_def (the_context ()) "set_of_list_list"]
"l: list(A) ==> set_of_list(l) : Pow(A)";
by (etac list_rec_type 1);
by (ALLGOALS (Blast_tac));
@@ -156,15 +156,15 @@
(** list_add **)
-Goalw [get_def thy "list_add_list"]
+Goalw [get_def (the_context ()) "list_add_list"]
"xs: list(nat) ==> list_add(xs) : nat";
by (REPEAT (ares_tac [list_rec_type, nat_0I, add_type] 1));
qed "list_add_type";
-val list_typechecks =
+bind_thms ("list_typechecks",
list.intrs @
[list_rec_type, map_type, map_type2, app_type, length_type,
- rev_type, flat_type, list_add_type];
+ rev_type, flat_type, list_add_type]);
AddTCs list_typechecks;
--- a/src/ZF/Nat.ML Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/Nat.ML Thu Sep 07 21:12:49 2000 +0200
@@ -14,7 +14,7 @@
qed "nat_bnd_mono";
(* nat = {0} Un {succ(x). x:nat} *)
-val nat_unfold = nat_bnd_mono RS (nat_def RS def_lfp_Tarski);
+bind_thm ("nat_unfold", nat_bnd_mono RS (nat_def RS def_lfp_Tarski));
(** Type checking of 0 and successor **)
@@ -44,7 +44,7 @@
by (blast_tac (claset() addSEs [boolE]) 1);
qed "bool_subset_nat";
-val bool_into_nat = bool_subset_nat RS subsetD;
+bind_thm ("bool_into_nat", bool_subset_nat RS subsetD);
(** Injectivity properties and induction **)
@@ -97,7 +97,7 @@
qed "Limit_nat";
(* succ(i): nat ==> i: nat *)
-val succ_natD = [succI1, asm_rl, Ord_nat] MRS Ord_trans;
+bind_thm ("succ_natD", [succI1, asm_rl, Ord_nat] MRS Ord_trans);
AddSDs [succ_natD];
Goal "succ(n): nat <-> n: nat";
@@ -115,7 +115,7 @@
qed "nat_le_Limit";
(* [| succ(i): k; k: nat |] ==> i: k *)
-val succ_in_naturalD = [succI1, asm_rl, nat_into_Ord] MRS Ord_trans;
+bind_thm ("succ_in_naturalD", [succI1, asm_rl, nat_into_Ord] MRS Ord_trans);
Goal "[| m<n; n: nat |] ==> m: nat";
by (etac ltE 1);
@@ -131,7 +131,7 @@
(** Variations on mathematical induction **)
(*complete induction*)
-val complete_induct = Ord_nat RSN (2, Ord_induct);
+bind_thm ("complete_induct", Ord_nat RSN (2, Ord_induct));
val prems = Goal
"[| m: nat; n: nat; \
--- a/src/ZF/OrdQuant.ML Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/OrdQuant.ML Thu Sep 07 21:12:49 2000 +0200
@@ -1,4 +1,4 @@
-(* Title: ZF/AC/OrdQuant.thy
+(* Title: ZF/OrdQuant.ML
ID: $Id$
Authors: Krzysztof Grabczewski and L C Paulson
@@ -97,8 +97,7 @@
AddSEs [oexE, OUN_E];
AddEs [rev_oallE];
-val Ord_atomize = atomize (("OrdQuant.oall", [ospec])::ZF_conn_pairs,
- ZF_mem_pairs);
+val Ord_atomize = atomize (("OrdQuant.oall", [ospec])::ZF_conn_pairs, ZF_mem_pairs);
simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all)
addsimps [oall_simp, ltD RS beta]
@@ -111,4 +110,3 @@
by (etac Ord_induct 1 THEN assume_tac 1);
by (fast_tac (claset() addIs prems) 1);
qed "lt_induct";
-
--- a/src/ZF/OrderArith.ML Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/OrderArith.ML Thu Sep 07 21:12:49 2000 +0200
@@ -182,7 +182,7 @@
(** Linearity **)
-val [lina,linb] = goal OrderArith.thy
+val [lina,linb] = goal (the_context ())
"[| linear(A,r); linear(B,s) |] ==> linear(A*B,rmult(A,r,B,s))";
by (rewtac linear_def); (*Note! the premises are NOT rewritten*)
by (REPEAT_FIRST (ares_tac [ballI] ORELSE' etac SigmaE));
@@ -354,7 +354,7 @@
(** Linearity **)
-val [finj,lin] = goalw OrderArith.thy [inj_def]
+val [finj,lin] = goalw (the_context ()) [inj_def]
"[| f: inj(A,B); linear(B,r) |] ==> linear(A,rvimage(A,f,r))";
by (rewtac linear_def); (*Note! the premises are NOT rewritten*)
by (REPEAT_FIRST (ares_tac [ballI]));
--- a/src/ZF/OrderType.ML Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/OrderType.ML Thu Sep 07 21:12:49 2000 +0200
@@ -12,7 +12,7 @@
(**** Proofs needing the combination of Ordinal.thy and Order.thy ****)
-val [prem] = goal OrderType.thy "j le i ==> well_ord(j, Memrel(i))";
+val [prem] = goal (the_context ()) "j le i ==> well_ord(j, Memrel(i))";
by (rtac well_ordI 1);
by (rtac (wf_Memrel RS wf_imp_wf_on) 1);
by (resolve_tac [prem RS ltE] 1);
@@ -87,7 +87,7 @@
qed "ordermap_pred_unfold";
(*pred-unfolded version. NOT suitable for rewriting -- loops!*)
-val ordermap_unfold = rewrite_rule [pred_def] ordermap_pred_unfold;
+bind_thm ("ordermap_unfold", rewrite_rule [pred_def] ordermap_pred_unfold);
(*** Showing that ordermap, ordertype yield ordinals ***)
@@ -614,7 +614,7 @@
by (asm_simp_tac (simpset() addsimps [oadd_odiff_inverse, oadd_le_self]) 1);
qed "odiff_oadd_inverse";
-val [i_lt_j, k_le_i] = goal OrderType.thy
+val [i_lt_j, k_le_i] = goal (the_context ())
"[| i<j; k le i |] ==> i--k < j--k";
by (rtac (k_le_i RS lt_Ord RSN (2,oadd_lt_cancel2)) 1);
by (simp_tac
--- a/src/ZF/Ordinal.ML Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/Ordinal.ML Thu Sep 07 21:12:49 2000 +0200
@@ -1,4 +1,4 @@
-(* Title: ZF/Ordinal.thy
+(* Title: ZF/Ordinal.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
@@ -25,19 +25,19 @@
by (Blast_tac 1);
qed "Transset_doubleton_D";
-val [prem1,prem2] = goalw Ordinal.thy [Pair_def]
+val [prem1,prem2] = goalw (the_context ()) [Pair_def]
"[| Transset(C); <a,b>: C |] ==> a:C & b: C";
by (cut_facts_tac [prem2] 1);
by (blast_tac (claset() addSDs [prem1 RS Transset_doubleton_D]) 1);
qed "Transset_Pair_D";
-val prem1::prems = goal Ordinal.thy
+val prem1::prems = goal (the_context ())
"[| Transset(C); A*B <= C; b: B |] ==> A <= C";
by (cut_facts_tac prems 1);
by (blast_tac (claset() addSDs [prem1 RS Transset_Pair_D]) 1);
qed "Transset_includes_domain";
-val prem1::prems = goal Ordinal.thy
+val prem1::prems = goal (the_context ())
"[| Transset(C); A*B <= C; a: A |] ==> B <= C";
by (cut_facts_tac prems 1);
by (blast_tac (claset() addSDs [prem1 RS Transset_Pair_D]) 1);
@@ -105,7 +105,7 @@
qed "Ord_in_Ord";
(* Ord(succ(j)) ==> Ord(j) *)
-val Ord_succD = succI1 RSN (2, Ord_in_Ord);
+bind_thm ("Ord_succD", succI1 RSN (2, Ord_in_Ord));
AddSDs [Ord_succD];
@@ -235,7 +235,7 @@
(* [| i<j; ~P ==> j<i |] ==> P *)
bind_thm ("lt_asym", lt_not_sym RS swap);
-val [major]= goal Ordinal.thy "i<i ==> P";
+val [major]= goal (the_context ()) "i<i ==> P";
by (rtac (major RS (major RS lt_asym)) 1) ;
qed "lt_irrefl";
@@ -261,7 +261,7 @@
by (asm_simp_tac (simpset() addsimps [le_iff]) 1);
qed "le_eqI";
-val le_refl = refl RS le_eqI;
+bind_thm ("le_refl", refl RS le_eqI);
Goal "i le i <-> Ord(i)";
by (asm_simp_tac (simpset() addsimps [lt_not_refl, le_iff]) 1);
@@ -381,7 +381,7 @@
qed "Transset_induct";
(*Induction over an ordinal*)
-val Ord_induct = Ord_is_Transset RSN (2, Transset_induct);
+bind_thm ("Ord_induct", Ord_is_Transset RSN (2, Transset_induct));
(*Induction over the class of ordinals -- a useful corollary of Ord_induct*)
val [major,indhyp] = Goal
@@ -584,7 +584,7 @@
by (REPEAT_SOME assume_tac);
qed "Un_least_lt_iff";
-val [ordi,ordj,ordk] = goal Ordinal.thy
+val [ordi,ordj,ordk] = goal (the_context ())
"[| Ord(i); Ord(j); Ord(k) |] ==> i Un j : k <-> i:k & j:k";
by (cut_inst_tac [("k","k")] ([ordi,ordj] MRS Un_least_lt_iff) 1);
by (asm_full_simp_tac (simpset() addsimps [lt_def,ordi,ordj,ordk]) 1);
--- a/src/ZF/Perm.ML Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/Perm.ML Thu Sep 07 21:12:49 2000 +0200
@@ -62,7 +62,7 @@
Goalw [inj_def] "[| f:inj(A,B); a:A; b:A; f`a=f`b |] ==> a=b";
by (Blast_tac 1);
-val inj_apply_equality = result();
+qed "inj_apply_equality";
(** A function with a left inverse is an injection **)
@@ -143,7 +143,7 @@
by (Simp_tac 1);
qed "id_subset_inj";
-val id_inj = subset_refl RS id_subset_inj;
+bind_thm ("id_inj", subset_refl RS id_subset_inj);
Goalw [id_def,surj_def] "id(A): surj(A,A)";
by (blast_tac (claset() addIs [lam_type, beta]) 1);
@@ -180,7 +180,7 @@
inj_is_fun]) 1);
qed "left_inverse";
-val left_inverse_bij = bij_is_inj RS left_inverse;
+bind_thm ("left_inverse_bij", bij_is_inj RS left_inverse);
Goal "[| f: A->B; converse(f): C->A; b: C |] ==> f`(converse(f)`b) = b";
by (rtac (apply_Pair RS (converseD RS apply_equality)) 1);
@@ -421,7 +421,7 @@
(*right inverse of composition; one inclusion is
f: A->B ==> f O converse(f) <= id(B)
*)
-val [prem] = goalw Perm.thy [surj_def]
+val [prem] = goalw (the_context ()) [surj_def]
"f: surj(A,B) ==> f O converse(f) = id(B)";
val appfD = (prem RS CollectD1) RSN (3,apply_equality2);
by (cut_facts_tac [prem] 1);
@@ -489,7 +489,7 @@
(** Restrictions as surjections and bijections *)
-val prems = goalw Perm.thy [surj_def]
+val prems = goalw (the_context ()) [surj_def]
"f: Pi(A,B) ==> f: surj(A, f``A)";
val rls = apply_equality :: (prems RL [apply_Pair,Pi_type]);
by (fast_tac (claset() addIs rls) 1);
--- a/src/ZF/QPair.ML Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/QPair.ML Thu Sep 07 21:12:49 2000 +0200
@@ -62,10 +62,10 @@
(** Elimination rules for <a;b>:A*B -- introducing no eigenvariables **)
-val QSigmaE2 =
+bind_thm ("QSigmaE2",
rule_by_tactic (REPEAT_FIRST (etac QPair_inject ORELSE' bound_hyp_subst_tac)
THEN prune_params_tac)
- (inst "c" "<a;b>" QSigmaE);
+ (inst "c" "<a;b>" QSigmaE));
AddSEs [QSigmaE2, QSigmaE];
@@ -205,7 +205,7 @@
(**** The Quine-inspired notion of disjoint sum ****)
-val qsum_defs = [qsum_def,QInl_def,QInr_def,qcase_def];
+bind_thms ("qsum_defs", [qsum_def,QInl_def,QInr_def,qcase_def]);
(** Introduction rules for the injections **)
--- a/src/ZF/QUniv.ML Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/QUniv.ML Thu Sep 07 21:12:49 2000 +0200
@@ -63,7 +63,7 @@
bind_thm ("A_subset_quniv",
[A_subset_univ, univ_subset_quniv] MRS subset_trans);
-val A_into_quniv = A_subset_quniv RS subsetD;
+bind_thm ("A_into_quniv", A_subset_quniv RS subsetD);
(*** univ(A) closure for Quine-inspired pairs and injections ***)
@@ -79,12 +79,12 @@
by (etac (empty_subsetI RS QPair_subset_univ) 1);
qed "QInl_subset_univ";
-val naturals_subset_nat =
+bind_thm ("naturals_subset_nat",
rewrite_rule [Transset_def] (Ord_nat RS Ord_is_Transset)
- RS bspec;
+ RS bspec);
-val naturals_subset_univ =
- [naturals_subset_nat, nat_subset_univ] MRS subset_trans;
+bind_thm ("naturals_subset_univ",
+ [naturals_subset_nat, nat_subset_univ] MRS subset_trans);
Goalw [QInr_def] "a <= univ(A) ==> QInr(a) <= univ(A)";
by (etac (nat_1I RS naturals_subset_univ RS QPair_subset_univ) 1);
--- a/src/ZF/Rel.ML Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/Rel.ML Thu Sep 07 21:12:49 2000 +0200
@@ -6,8 +6,6 @@
Relations in Zermelo-Fraenkel Set Theory
*)
-open Rel;
-
(*** Some properties of relations -- useful? ***)
(* irreflexivity *)
--- a/src/ZF/Sum.ML Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/Sum.ML Thu Sep 07 21:12:49 2000 +0200
@@ -18,7 +18,7 @@
by (Blast_tac 1);
qed "Part_eqI";
-val PartI = refl RSN (2,Part_eqI);
+bind_thm ("PartI", refl RSN (2,Part_eqI));
val major::prems = Goalw [Part_def]
"[| a : Part(A,h); !!z. [| a : A; a=h(z) |] ==> P \
@@ -38,7 +38,7 @@
(*** Rules for Disjoint Sums ***)
-val sum_defs = [sum_def,Inl_def,Inr_def,case_def];
+bind_thms ("sum_defs", [sum_def,Inl_def,Inr_def,case_def]);
Goalw (bool_def::sum_defs) "Sigma(bool,C) = C(0) + C(1)";
by (Blast_tac 1);
--- a/src/ZF/Trancl.ML Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/Trancl.ML Thu Sep 07 21:12:49 2000 +0200
@@ -19,7 +19,7 @@
qed "rtrancl_mono";
(* r^* = id(field(r)) Un ( r O r^* ) *)
-val rtrancl_unfold = rtrancl_bnd_mono RS (rtrancl_def RS def_lfp_Tarski);
+bind_thm ("rtrancl_unfold", rtrancl_bnd_mono RS (rtrancl_def RS def_lfp_Tarski));
(** The relation rtrancl **)
@@ -138,7 +138,7 @@
qed "rtrancl_into_trancl1";
(*intro rule from r and r^* *)
-val prems = goal Trancl.thy
+val prems = goal (the_context ())
"[| <a,b> : r; <b,c> : r^* |] ==> <a,c> : r^+";
by (resolve_tac (prems RL [rtrancl_induct]) 1);
by (resolve_tac (prems RL [r_into_trancl]) 1);
--- a/src/ZF/Univ.ML Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/Univ.ML Thu Sep 07 21:12:49 2000 +0200
@@ -156,7 +156,7 @@
by (Blast_tac 1);
qed "Vfrom_Union";
-val [prem] = goal Univ.thy "y:X ==> Vfrom(A,Union(X)) = (UN y:X. Vfrom(A,y))";
+val [prem] = goal (the_context ()) "y:X ==> Vfrom(A,Union(X)) = (UN y:X. Vfrom(A,y))";
by (stac Vfrom 1);
by (rtac equalityI 1);
(*first inclusion*)
@@ -180,7 +180,7 @@
(*NB. limit ordinals are non-empty;
Vfrom(A,0) = A = A Un (UN y:0. Vfrom(A,y)) *)
-val [limiti] = goal Univ.thy
+val [limiti] = goal (the_context ())
"Limit(i) ==> Vfrom(A,i) = (UN y:i. Vfrom(A,y))";
by (rtac (limiti RS (Limit_has_0 RS ltD) RS Vfrom_Union RS subst) 1);
by (stac (limiti RS Limit_Union_eq) 1);
@@ -201,9 +201,9 @@
by (REPEAT (ares_tac (prems @ [ltI, Limit_is_Ord]) 1));
qed "Limit_VfromE";
-val zero_in_VLimit = Limit_has_0 RS ltD RS zero_in_Vfrom;
+bind_thm ("zero_in_VLimit", Limit_has_0 RS ltD RS zero_in_Vfrom);
-val [major,limiti] = goal Univ.thy
+val [major,limiti] = goal (the_context ())
"[| a: Vfrom(A,i); Limit(i) |] ==> {a} : Vfrom(A,i)";
by (rtac ([major,limiti] MRS Limit_VfromE) 1);
by (etac ([singleton_in_Vfrom, limiti] MRS Limit_VfromI) 1);
@@ -214,7 +214,7 @@
bind_thm ("Vfrom_UnI2", Un_upper2 RS (subset_refl RS Vfrom_mono RS subsetD));
(*Hard work is finding a single j:i such that {a,b}<=Vfrom(A,j)*)
-val [aprem,bprem,limiti] = goal Univ.thy
+val [aprem,bprem,limiti] = goal (the_context ())
"[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i) |] ==> \
\ {a,b} : Vfrom(A,i)";
by (rtac ([aprem,limiti] MRS Limit_VfromE) 1);
@@ -225,7 +225,7 @@
by (REPEAT (ares_tac [limiti, Limit_has_succ, Un_least_lt] 1));
qed "doubleton_in_VLimit";
-val [aprem,bprem,limiti] = goal Univ.thy
+val [aprem,bprem,limiti] = goal (the_context ())
"[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i) |] ==> \
\ <a,b> : Vfrom(A,i)";
(*Infer that a, b occur at ordinals x,xa < i.*)
@@ -340,7 +340,7 @@
by (blast_tac (claset() addIs [Pair_in_Vfrom]) 1);
qed "prod_in_Vfrom";
-val [aprem,bprem,limiti,transset] = goal Univ.thy
+val [aprem,bprem,limiti,transset] = goal (the_context ())
"[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i); Transset(A) |] ==> \
\ a*b : Vfrom(A,i)";
by (rtac ([aprem,bprem,limiti] MRS in_VLimit) 1);
@@ -360,7 +360,7 @@
i_subset_Vfrom RS subsetD]) 1);
qed "sum_in_Vfrom";
-val [aprem,bprem,limiti,transset] = goal Univ.thy
+val [aprem,bprem,limiti,transset] = goal (the_context ())
"[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i); Transset(A) |] ==> \
\ a+b : Vfrom(A,i)";
by (rtac ([aprem,bprem,limiti] MRS in_VLimit) 1);
@@ -385,7 +385,7 @@
by (blast_tac (claset() addIs [Pair_in_Vfrom]) 1);
qed "fun_in_Vfrom";
-val [aprem,bprem,limiti,transset] = goal Univ.thy
+val [aprem,bprem,limiti,transset] = goal (the_context ())
"[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i); Transset(A) |] ==> \
\ a->b : Vfrom(A,i)";
by (rtac ([aprem,bprem,limiti] MRS in_VLimit) 1);
@@ -415,9 +415,9 @@
by (Blast_tac 1);
qed "Vset";
-val Vset_succ = Transset_0 RS Transset_Vfrom_succ;
+bind_thm ("Vset_succ", Transset_0 RS Transset_Vfrom_succ);
-val Transset_Vset = Transset_0 RS Transset_Vfrom;
+bind_thm ("Transset_Vset", Transset_0 RS Transset_Vfrom);
(** Characterisation of the elements of Vset(i) **)
@@ -495,8 +495,8 @@
by (rtac rank_pair2 1);
qed "rank_Inr";
-val rank_rls = [rank_Inl, rank_Inr, rank_pair1, rank_pair2];
-val rank_trans_rls = rank_rls @ (rank_rls RLN (2, [lt_trans]));
+bind_thms ("rank_rls", [rank_Inl, rank_Inr, rank_pair1, rank_pair2]);
+bind_thms ("rank_trans_rls", rank_rls @ (rank_rls RLN (2, [lt_trans])));
val rank_ss = simpset() addsimps [VsetI] addsimps rank_trans_rls;
@@ -586,7 +586,7 @@
by (rtac A_subset_Vfrom 1);
qed "A_subset_univ";
-val A_into_univ = A_subset_univ RS subsetD;
+bind_thm ("A_into_univ", A_subset_univ RS subsetD);
(** Closure under unordered and ordered pairs **)
@@ -669,7 +669,7 @@
by (etac Limit_VfromE 1);
by (assume_tac 1);
by (blast_tac (claset() addSIs [Un_least_lt] addIs [Vfrom_UnI1, Vfrom_UnI2]) 1);
-val Fin_Vfrom_lemma = result();
+qed "Fin_Vfrom_lemma";
Goal "Limit(i) ==> Fin(Vfrom(A,i)) <= Vfrom(A,i)";
by (rtac subsetI 1);
@@ -677,13 +677,13 @@
by Safe_tac;
by (resolve_tac [Vfrom RS ssubst] 1);
by (blast_tac (claset() addSDs [ltD]) 1);
-val Fin_VLimit = result();
+qed "Fin_VLimit";
bind_thm ("Fin_subset_VLimit", [Fin_mono, Fin_VLimit] MRS subset_trans);
Goalw [univ_def] "Fin(univ(A)) <= univ(A)";
by (rtac (Limit_nat RS Fin_VLimit) 1);
-val Fin_univ = result();
+qed "Fin_univ";
(** Closure under finite powers (functions from a fixed natural number) **)
@@ -691,13 +691,13 @@
by (eresolve_tac [nat_fun_subset_Fin RS subset_trans] 1);
by (REPEAT (ares_tac [Fin_subset_VLimit, Sigma_subset_VLimit,
nat_subset_VLimit, subset_refl] 1));
-val nat_fun_VLimit = result();
+qed "nat_fun_VLimit";
bind_thm ("nat_fun_subset_VLimit", [Pi_mono, nat_fun_VLimit] MRS subset_trans);
Goalw [univ_def] "n: nat ==> n -> univ(A) <= univ(A)";
by (etac (Limit_nat RSN (2,nat_fun_VLimit)) 1);
-val nat_fun_univ = result();
+qed "nat_fun_univ";
(** Closure under finite function space **)
@@ -706,30 +706,30 @@
Goal "Limit(i) ==> Vfrom(A,i) -||> Vfrom(A,i) <= Vfrom(A,i)";
by (resolve_tac [FiniteFun.dom_subset RS subset_trans] 1);
by (REPEAT (ares_tac [Fin_subset_VLimit, Sigma_subset_VLimit, subset_refl] 1));
-val FiniteFun_VLimit1 = result();
+qed "FiniteFun_VLimit1";
Goalw [univ_def] "univ(A) -||> univ(A) <= univ(A)";
by (rtac (Limit_nat RS FiniteFun_VLimit1) 1);
-val FiniteFun_univ1 = result();
+qed "FiniteFun_univ1";
(*Version for a fixed domain*)
Goal "[| W <= Vfrom(A,i); Limit(i) |] ==> W -||> Vfrom(A,i) <= Vfrom(A,i)";
by (eresolve_tac [subset_refl RSN (2, FiniteFun_mono) RS subset_trans] 1);
by (etac FiniteFun_VLimit1 1);
-val FiniteFun_VLimit = result();
+qed "FiniteFun_VLimit";
Goalw [univ_def]
"W <= univ(A) ==> W -||> univ(A) <= univ(A)";
by (etac (Limit_nat RSN (2, FiniteFun_VLimit)) 1);
-val FiniteFun_univ = result();
+qed "FiniteFun_univ";
Goal "[| f: W -||> univ(A); W <= univ(A) |] ==> f : univ(A)";
by (eresolve_tac [FiniteFun_univ RS subsetD] 1);
by (assume_tac 1);
-val FiniteFun_in_univ = result();
+qed "FiniteFun_in_univ";
(*Remove <= from the rule above*)
-val FiniteFun_in_univ' = subsetI RSN (2, FiniteFun_in_univ);
+bind_thm ("FiniteFun_in_univ'", subsetI RSN (2, FiniteFun_in_univ));
(**** For QUniv. Properties of Vfrom analogous to the "take-lemma" ****)
--- a/src/ZF/Update.ML Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/Update.ML Thu Sep 07 21:12:49 2000 +0200
@@ -1,4 +1,4 @@
-(* Title: ZF/Update.thy
+(* Title: ZF/Update.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
@@ -6,8 +6,6 @@
Function updates: like theory Map, but for ordinary functions
*)
-open Update;
-
Goal "f(x:=y) ` z = (if z=x then y else f`z)";
by (simp_tac (simpset() addsimps [update_def]) 1);
by (case_tac "z : domain(f)" 1);
--- a/src/ZF/WF.ML Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/WF.ML Thu Sep 07 21:12:49 2000 +0200
@@ -1,4 +1,4 @@
-(* Title: ZF/wf.ML
+(* Title: ZF/WF.ML
ID: $Id$
Author: Tobias Nipkow and Lawrence C Paulson
Copyright 1998 University of Cambridge
@@ -175,7 +175,7 @@
val bchain_tac = EVERY' [rtac (bspec RS mp), assume_tac, assume_tac ];
(*transitive closure of a WF relation is WF provided A is downwards closed*)
-val [wfr,subs] = goal WF.thy
+val [wfr,subs] = goal (the_context ())
"[| wf[A](r); r-``A <= A |] ==> wf[A](r^+)";
by (rtac wf_onI2 1);
by (bchain_tac 1);
@@ -206,7 +206,7 @@
by (assume_tac 1);
qed "is_recfun_type";
-val [isrec,rel] = goalw WF.thy [is_recfun_def]
+val [isrec,rel] = goalw (the_context ()) [is_recfun_def]
"[| is_recfun(r,a,H,f); <x,a>:r |] ==> f`x = H(x, restrict(f,r-``{x}))";
by (res_inst_tac [("P", "%x.?t(x) = (?u::i)")] (isrec RS ssubst) 1);
by (rtac (rel RS underI RS beta) 1);
@@ -232,7 +232,7 @@
by (asm_simp_tac (wf_super_ss addsimps [vimage_singleton_iff]) 1);
qed_spec_mp "is_recfun_equal";
-val prems as [wfr,transr,recf,recg,_] = goal WF.thy
+val prems as [wfr,transr,recf,recg,_] = goal (the_context ())
"[| wf(r); trans(r); \
\ is_recfun(r,a,H,f); is_recfun(r,b,H,g); <b,a>:r |] ==> \
\ restrict(f, r-``{b}) = g";
@@ -296,7 +296,7 @@
(** Removal of the premise trans(r) **)
(*NOT SUITABLE FOR REWRITING: it is recursive!*)
-val [wfr] = goalw WF.thy [wfrec_def]
+val [wfr] = goalw (the_context ()) [wfrec_def]
"wf(r) ==> wfrec(r,a,H) = H(a, lam x:r-``{a}. wfrec(r,x,H))";
by (stac (wfr RS wf_trancl RS wftrec) 1);
by (rtac trans_trancl 1);
--- a/src/ZF/ZF.ML Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/ZF.ML Thu Sep 07 21:12:49 2000 +0200
@@ -10,7 +10,7 @@
Goal "[| b:A; a=b |] ==> a:A";
by (etac ssubst 1);
by (assume_tac 1);
-val subst_elem = result();
+qed "subst_elem";
(*** Bounded universal quantifier ***)
@@ -505,50 +505,28 @@
by (best_tac cantor_cs 1);
qed "cantor";
-(*Lemma for the inductive definition in Zorn.thy*)
+(*Lemma for the inductive definition in theory Zorn*)
Goal "Y : Pow(Pow(A)) ==> Union(Y) : Pow(A)";
by (Blast_tac 1);
qed "Union_in_Pow";
+(* update rulify setup -- include bounded All *)
+
+Goal "(!!x. x:A ==> P(x)) == Trueprop (ALL x:A. P(x))";
+by (simp_tac (simpset () addsimps (Ball_def :: thms "atomize")) 1);
+qed "ball_eq";
+
local
-val (bspecT, bspec') = make_new_spec bspec
+ val ss = FOL_basic_ss addsimps
+ (Drule.norm_hhf_eq :: map Thm.symmetric (ball_eq :: thms "atomize"));
in
-fun RSbspec th =
- (case concl_of th of
- _ $ (Const("Ball",_) $ _ $ Abs(a,_,_)) =>
- let val ca = cterm_of (#sign(rep_thm th)) (Var((a,0),bspecT))
- in th RS forall_elim ca bspec' end
- | _ => raise THM("RSbspec",0,[th]));
-
-val normalize_thm_ZF = normalize_thm [RSspec,RSbspec,RSmp];
+structure Rulify = RulifyFun
+ (val make_meta = Simplifier.simplify ss
+ val full_make_meta = Simplifier.full_simplify ss);
-fun qed_spec_mp name =
- let val thm = normalize_thm_ZF (result())
- in bind_thm(name, thm) end;
-
-fun qed_goal_spec_mp name thy s p =
- bind_thm (name, normalize_thm_ZF (prove_goal thy s p));
-
-fun qed_goalw_spec_mp name thy defs s p =
- bind_thm (name, normalize_thm_ZF (prove_goalw thy defs s p));
+structure BasicRulify: BASIC_RULIFY = Rulify;
+open BasicRulify;
end;
-
-
-(* attributes *)
-
-local
-
-fun gen_rulify x =
- Attrib.no_args (Drule.rule_attribute (K (normalize_thm_ZF))) x;
-
-in
-
-val attrib_setup =
- [Attrib.add_attributes
- [("rulify", (gen_rulify, gen_rulify),
- "put theorem into standard rule form")]];
-
-end;
--- a/src/ZF/Zorn.ML Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/Zorn.ML Thu Sep 07 21:12:49 2000 +0200
@@ -33,9 +33,11 @@
(*Introduction rules*)
val [TFin_nextI, Pow_TFin_UnionI] = TFin.intrs;
-val TFin_UnionI = PowI RS Pow_TFin_UnionI;
+bind_thm ("TFin_nextI", TFin_nextI);
+bind_thm ("Pow_TFin_UnionI", Pow_TFin_UnionI);
+bind_thm ("TFin_UnionI", PowI RS Pow_TFin_UnionI);
-val TFin_is_subset = TFin.dom_subset RS subsetD RS PowD;
+bind_thm ("TFin_is_subset", TFin.dom_subset RS subsetD RS PowD);
(** Structural induction on TFin(S,next) **)
@@ -66,7 +68,7 @@
(*Lemma 2 of section 3.2. Interesting in its own right!
Requires next: increasing(S) in the second induction step. *)
-val [major,ninc] = goal Zorn.thy
+val [major,ninc] = goal (the_context ())
"[| m: TFin(S,next); next: increasing(S) \
\ |] ==> ALL n: TFin(S,next) . n<=m --> n=m | next`n<=m";
by (rtac (major RS TFin_induct) 1);
--- a/src/ZF/equalities.ML Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/equalities.ML Thu Sep 07 21:12:49 2000 +0200
@@ -29,7 +29,7 @@
Goal "[| a: C; ALL y:C. y=b |] ==> C = {b}";
by (Blast_tac 1);
qed "equal_singleton_lemma";
-val equal_singleton = ballI RSN (2,equal_singleton_lemma);
+bind_thm ("equal_singleton", ballI RSN (2,equal_singleton_lemma));
(** Binary Intersection **)
--- a/src/ZF/func.ML Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/func.ML Thu Sep 07 21:12:49 2000 +0200
@@ -364,9 +364,9 @@
(** The Union of 2 disjoint functions is a function **)
-val Un_rls = [Un_subset_iff, SUM_Un_distrib1, prod_Un_distrib2,
+bind_thms ("Un_rls", [Un_subset_iff, SUM_Un_distrib1, prod_Un_distrib2,
Un_upper1 RSN (2, subset_trans),
- Un_upper2 RSN (2, subset_trans)];
+ Un_upper2 RSN (2, subset_trans)]);
Goal "[| f: A->B; g: C->D; A Int C = 0 |] \
\ ==> (f Un g) : (A Un C) -> (B Un D)";
--- a/src/ZF/mono.ML Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/mono.ML Thu Sep 07 21:12:49 2000 +0200
@@ -58,7 +58,7 @@
Goal "[| A<=C; ALL x:A. B(x) <= D(x) |] ==> Sigma(A,B) <= Sigma(C,D)";
by (Blast_tac 1);
qed "Sigma_mono_lemma";
-val Sigma_mono = ballI RSN (2,Sigma_mono_lemma);
+bind_thm ("Sigma_mono", ballI RSN (2,Sigma_mono_lemma));
Goalw sum_defs "[| A<=C; B<=D |] ==> A+B <= C+D";
by (REPEAT (ares_tac [subset_refl,Un_mono,Sigma_mono] 1));
@@ -83,7 +83,7 @@
\ QSigma(A,B) <= QSigma(C,D)";
by (Blast_tac 1);
qed "QSigma_mono_lemma";
-val QSigma_mono = ballI RSN (2,QSigma_mono_lemma);
+bind_thm ("QSigma_mono", ballI RSN (2,QSigma_mono_lemma));
Goalw [QInl_def] "a<=b ==> QInl(a) <= QInl(b)";
by (REPEAT (ares_tac [subset_refl RS QPair_mono] 1));
@@ -187,6 +187,5 @@
qed "all_mono";
(*Used in intr_elim.ML and in individual datatype definitions*)
-val basic_monos = [subset_refl, imp_refl, disj_mono, conj_mono,
- ex_mono, Collect_mono, Part_mono, in_mono];
-
+bind_thms ("basic_monos",
+ [subset_refl, imp_refl, disj_mono, conj_mono, ex_mono, Collect_mono, Part_mono, in_mono]);
--- a/src/ZF/simpdata.ML Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/simpdata.ML Thu Sep 07 21:12:49 2000 +0200
@@ -63,6 +63,13 @@
end;
+bind_thms ("ball_simps", ball_simps);
+bind_thm ("ball_conj_distrib", ball_conj_distrib);
+bind_thms ("bex_simps", bex_simps);
+bind_thm ("bex_disj_distrib", bex_disj_distrib);
+bind_thms ("Rep_simps", Rep_simps);
+bind_thms ("misc_simps", misc_simps);
+
Addsimps (ball_simps @ bex_simps @ Rep_simps @ misc_simps);
--- a/src/ZF/subset.ML Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/subset.ML Thu Sep 07 21:12:49 2000 +0200
@@ -196,11 +196,11 @@
by (blast_tac (claset() addIs prems) 1);
qed "RepFun_subset";
-val subset_SIs =
+bind_thms ("subset_SIs",
[subset_refl, cons_subsetI, subset_consI,
Union_least, UN_least, Un_least,
Inter_greatest, Int_greatest, RepFun_subset,
- Un_upper1, Un_upper2, Int_lower1, Int_lower2];
+ Un_upper1, Un_upper2, Int_lower1, Int_lower2]);
(*A claset for subset reasoning*)
--- a/src/ZF/upair.ML Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/upair.ML Thu Sep 07 21:12:49 2000 +0200
@@ -14,8 +14,8 @@
(*** Lemmas about power sets ***)
-val Pow_bottom = empty_subsetI RS PowI; (* 0 : Pow(B) *)
-val Pow_top = subset_refl RS PowI; (* A : Pow(A) *)
+bind_thm ("Pow_bottom", empty_subsetI RS PowI); (* 0 : Pow(B) *)
+bind_thm ("Pow_top", subset_refl RS PowI); (* A : Pow(A) *)
(*** Unordered pairs - Upair ***)
@@ -303,8 +303,7 @@
bind_thm ("split_if_mem1", inst "P" "%x. x : ?b" split_if);
bind_thm ("split_if_mem2", inst "P" "%x. ?a : x" split_if);
-val split_ifs = [split_if_eq1, split_if_eq2,
- split_if_mem1, split_if_mem2];
+bind_thms ("split_ifs", [split_if_eq1, split_if_eq2, split_if_mem1, split_if_mem2]);
(*Logically equivalent to split_if_mem2*)
Goal "a: (if P then x else y) <-> P & a:x | ~P & a:y";
@@ -387,7 +386,7 @@
(* succ(c) <= B ==> c : B *)
-val succ_subsetD = succI1 RSN (2,subsetD);
+bind_thm ("succ_subsetD", succI1 RSN (2,subsetD));
(* succ(b) ~= b *)
bind_thm ("succ_neq_self", succI1 RS mem_imp_not_eq RS not_sym);
@@ -403,4 +402,3 @@
(*Not needed now that cons is available. Deletion reduces the search space.*)
Delrules [UpairI1,UpairI2,UpairE];
-
--- a/src/ZF/upair.thy Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/upair.thy Thu Sep 07 21:12:49 2000 +0200
@@ -2,15 +2,12 @@
ID: $Id$
Author: Lawrence C Paulson and Martin D Coen, CU Computer Laboratory
Copyright 1993 University of Cambridge
-
-Dummy theory, but holds the standard ZF simpset.
*)
theory upair = ZF
files "Tools/typechk":
-setup
- TypeCheck.setup
+setup TypeCheck.setup
+setup Rulify.setup
end
-