--- a/src/HOL/Fun.ML Mon Jul 24 23:51:11 2000 +0200
+++ b/src/HOL/Fun.ML Mon Jul 24 23:51:46 2000 +0200
@@ -460,12 +460,13 @@
if v aconv x then Some g else gen_fun_upd (find g) T v w
| find t = None
in (dest_fun_T1 T, gen_fun_upd (find f) T x y) end
+ val ss = simpset ();
val fun_upd_prover = K [rtac eq_reflection 1, rtac ext 1,
- simp_tac (simpset_of Fun.thy) 1]
+ simp_tac ss 1]
fun mk_eq_cterm sg T l r = Thm.cterm_of sg (equals T $ l $ r)
in
val fun_upd2_simproc = Simplifier.mk_simproc "fun_upd2"
- [Thm.read_cterm (sign_of Fun.thy) ("f(v:=w,x:=y)", HOLogic.termT)]
+ [Thm.read_cterm (sign_of (the_context ())) ("f(v:=w,x:=y)", HOLogic.termT)]
(fn sg => (K (fn t => case find_double t of (T,None)=> None | (T,Some rhs)=>
Some (prove_goalw_cterm [] (mk_eq_cterm sg T t rhs) fun_upd_prover))))
end;
--- a/src/HOL/Gfp.ML Mon Jul 24 23:51:11 2000 +0200
+++ b/src/HOL/Gfp.ML Mon Jul 24 23:51:46 2000 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/gfp
+(* Title: HOL/Gfp.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
@@ -6,8 +6,6 @@
The Knaster-Tarski Theorem for greatest fixed points.
*)
-open Gfp;
-
(*** Proof of Knaster-Tarski Theorem using gfp ***)
(* gfp(f) is the least upper bound of {u. u <= f(u)} *)
@@ -16,7 +14,7 @@
by (etac (CollectI RS Union_upper) 1);
qed "gfp_upperbound";
-val prems = goalw Gfp.thy [gfp_def]
+val prems = goalw (the_context ()) [gfp_def]
"[| !!u. u <= f(u) ==> u<=X |] ==> gfp(f) <= X";
by (REPEAT (ares_tac ([Union_least]@prems) 1));
by (etac CollectD 1);
@@ -44,7 +42,7 @@
by Auto_tac;
qed "weak_coinduct";
-val [prem,mono] = goal Gfp.thy
+val [prem,mono] = goal (the_context ())
"[| X <= f(X Un gfp(f)); mono(f) |] ==> \
\ X Un gfp(f) <= f(X Un gfp(f))";
by (rtac (prem RS Un_least) 1);
@@ -59,7 +57,7 @@
by (REPEAT (ares_tac [UnI1, Un_least] 1));
qed "coinduct";
-val [mono,prem] = goal Gfp.thy
+val [mono,prem] = goal (the_context ())
"[| mono(f); a: gfp(f) |] ==> a: f(X Un gfp(f))";
by (rtac (mono RS mono_Un RS subsetD) 1);
by (rtac (mono RS gfp_lemma2 RS subsetD RS UnI2) 1);
@@ -74,7 +72,7 @@
by (REPEAT (ares_tac [subset_refl, monoI, Un_mono] 1 ORELSE etac monoD 1));
qed "coinduct3_mono_lemma";
-val [prem,mono] = goal Gfp.thy
+val [prem,mono] = goal (the_context ())
"[| X <= f(lfp(%x. f(x) Un X Un gfp(f))); mono(f) |] ==> \
\ lfp(%x. f(x) Un X Un gfp(f)) <= f(lfp(%x. f(x) Un X Un gfp(f)))";
by (rtac subset_trans 1);
@@ -98,12 +96,12 @@
(** Definition forms of gfp_Tarski and coinduct, to control unfolding **)
-val [rew,mono] = goal Gfp.thy "[| A==gfp(f); mono(f) |] ==> A = f(A)";
+val [rew,mono] = goal (the_context ()) "[| A==gfp(f); mono(f) |] ==> A = f(A)";
by (rewtac rew);
by (rtac (mono RS gfp_Tarski) 1);
qed "def_gfp_Tarski";
-val rew::prems = goal Gfp.thy
+val rew::prems = goal (the_context ())
"[| A==gfp(f); mono(f); a:X; X <= f(X Un A) |] ==> a: A";
by (rewtac rew);
by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems @ [coinduct]) 1));
@@ -118,7 +116,7 @@
by (REPEAT (ares_tac (prems @ [subsetI,CollectI]) 1));
qed "def_Collect_coinduct";
-val rew::prems = goal Gfp.thy
+val rew::prems = goal (the_context ())
"[| A==gfp(f); mono(f); a:X; X <= f(lfp(%x. f(x) Un X Un A)) |] ==> a: A";
by (rewtac rew);
by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems @ [coinduct3]) 1));
--- a/src/HOL/Integ/IntDiv.ML Mon Jul 24 23:51:11 2000 +0200
+++ b/src/HOL/Integ/IntDiv.ML Mon Jul 24 23:51:46 2000 +0200
@@ -130,7 +130,7 @@
(*Proving negDivAlg's termination condition*)
val [tc] = negDivAlg.tcs;
-goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop tc));
+goalw_cterm [] (cterm_of (sign_of (the_context ())) (HOLogic.mk_Trueprop tc));
by Auto_tac;
val lemma = result();
@@ -425,7 +425,7 @@
by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1);
qed "mod_neg_neg";
-Addsimps (map (read_instantiate_sg (sign_of IntDiv.thy)
+Addsimps (map (read_instantiate_sg (sign_of (the_context ()))
[("a", "number_of ?v"), ("b", "number_of ?w")])
[div_pos_pos, div_neg_pos, div_pos_neg, div_neg_neg,
mod_pos_pos, mod_neg_pos, mod_pos_neg, mod_neg_neg,
@@ -835,8 +835,7 @@
\ (if ~b | (#0::int) <= number_of w \
\ then number_of v div (number_of w) \
\ else (number_of v + (#1::int)) div (number_of w))";
-by (simp_tac (simpset_of Int.thy
- addsimps [zadd_assoc, number_of_BIT]) 1);
+by (simp_tac (simpset_of Int.thy addsimps [zadd_assoc, number_of_BIT]) 1);
by (asm_simp_tac (simpset()
delsimps bin_arith_extra_simps@bin_rel_simps
addsimps [zdiv_zmult_zmult1,
@@ -895,8 +894,7 @@
\ then #2 * (number_of v mod number_of w) + #1 \
\ else #2 * ((number_of v + (#1::int)) mod number_of w) - #1 \
\ else #2 * (number_of v mod number_of w))";
-by (simp_tac (simpset_of Int.thy
- addsimps [zadd_assoc, number_of_BIT]) 1);
+by (simp_tac (simpset_of Int.thy addsimps [zadd_assoc, number_of_BIT]) 1);
by (asm_simp_tac (simpset()
delsimps bin_arith_extra_simps@bin_rel_simps
addsimps [zmod_zmult_zmult1,
--- a/src/HOL/Lfp.ML Mon Jul 24 23:51:11 2000 +0200
+++ b/src/HOL/Lfp.ML Mon Jul 24 23:51:46 2000 +0200
@@ -1,13 +1,11 @@
-(* Title: HOL/lfp.ML
+(* Title: HOL/Lfp.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
-The Knaster-Tarski Theorem
+The Knaster-Tarski Theorem.
*)
-open Lfp;
-
(*** Proof of Knaster-Tarski Theorem ***)
(* lfp(f) is the greatest lower bound of {u. f(u) <= u} *)
@@ -57,7 +55,7 @@
(** Definition forms of lfp_Tarski and induct, to control unfolding **)
-val [rew,mono] = goal Lfp.thy "[| h==lfp(f); mono(f) |] ==> h = f(h)";
+val [rew,mono] = goal (the_context ()) "[| h==lfp(f); mono(f) |] ==> h = f(h)";
by (rewtac rew);
by (rtac (mono RS lfp_Tarski) 1);
qed "def_lfp_Tarski";
--- a/src/HOL/Ord.ML Mon Jul 24 23:51:11 2000 +0200
+++ b/src/HOL/Ord.ML Mon Jul 24 23:51:46 2000 +0200
@@ -120,7 +120,7 @@
by (Blast_tac 1);
qed "linorder_less_linear";
-val prems = goal thy
+val prems = goal (the_context ())
"[| (x::'a::linorder)<y ==> P; x=y ==> P; y<x ==> P |] ==> P";
by(cut_facts_tac [linorder_less_linear] 1);
by(REPEAT(eresolve_tac (prems@[disjE]) 1));
--- a/src/HOL/Real/Hyperreal/Filter.ML Mon Jul 24 23:51:11 2000 +0200
+++ b/src/HOL/Real/Hyperreal/Filter.ML Mon Jul 24 23:51:46 2000 +0200
@@ -342,7 +342,7 @@
Addsimps [Compl_empty_eq];
-val [prem] = goal thy "~ finite (UNIV:: 'a set) ==> \
+val [prem] = goal (the_context ()) "~ finite (UNIV:: 'a set) ==> \
\ {A:: 'a set. finite (- A)} : Filter UNIV";
by (cut_facts_tac [prem] 1);
by (rtac mem_FiltersetI2 1);
@@ -365,13 +365,13 @@
by (Blast_tac 1);
qed "not_finite_UNIV_Compl";
-val [prem] = goal thy "~ finite (UNIV:: 'a set) ==> \
+val [prem] = goal (the_context ()) "~ finite (UNIV:: 'a set) ==> \
\ !X: {A:: 'a set. finite (- A)}. ~ finite X";
by (cut_facts_tac [prem] 1);
by (auto_tac (claset() addDs [not_finite_UNIV_disjI],simpset()));
qed "mem_cofinite_Filter_not_finite";
-val [prem] = goal thy "~ finite (UNIV:: 'a set) ==> \
+val [prem] = goal (the_context ()) "~ finite (UNIV:: 'a set) ==> \
\ {A:: 'a set. finite (- A)} : Freefilter UNIV";
by (cut_facts_tac [prem] 1);
by (rtac mem_FreefiltersetI2 1);
--- a/src/HOL/Real/PNat.ML Mon Jul 24 23:51:11 2000 +0200
+++ b/src/HOL/Real/PNat.ML Mon Jul 24 23:51:46 2000 +0200
@@ -1,9 +1,9 @@
-(* Title : PNat.ML
+(* Title : HOL/Real/PNat.ML
ID : $Id$
Author : Jacques D. Fleuriot
Copyright : 1998 University of Cambridge
- Description : The positive naturals -- proofs
- : mainly as in Nat.thy
+
+The positive naturals -- proofs mainly as in theory Nat.
*)
Goal "mono(%X. {1} Un (Suc``X))";
@@ -30,14 +30,14 @@
(*** Induction ***)
-val major::prems = goal thy
+val major::prems = goal (the_context ())
"[| i: pnat; P(1); \
\ !!j. [| j: pnat; P(j) |] ==> P(Suc(j)) |] ==> P(i)";
by (rtac ([pnat_def, pnat_fun_mono, major] MRS def_induct) 1);
by (blast_tac (claset() addIs prems) 1);
qed "PNat_induct";
-val prems = goalw thy [pnat_one_def,pnat_Suc_def]
+val prems = goalw (the_context ()) [pnat_one_def,pnat_Suc_def]
"[| P(1p); \
\ !!n. P(n) ==> P(pSuc n) |] ==> P(n)";
by (rtac (Rep_pnat_inverse RS subst) 1);
@@ -50,7 +50,7 @@
fun pnat_ind_tac a i =
res_inst_tac [("n",a)] pnat_induct i THEN rename_last_tac a [""] (i+1);
-val prems = goal thy
+val prems = goal (the_context ())
"[| !!x. P x 1p; \
\ !!y. P 1p (pSuc y); \
\ !!x y. [| P x y |] ==> P (pSuc x) (pSuc y) \
@@ -63,7 +63,7 @@
qed "pnat_diff_induct";
(*Case analysis on the natural numbers*)
-val prems = goal thy
+val prems = goal (the_context ())
"[| n=1p ==> P; !!x. n = pSuc(x) ==> P |] ==> P";
by (subgoal_tac "n=1p | (EX x. n = pSuc(x))" 1);
by (fast_tac (claset() addSEs prems) 1);
@@ -340,7 +340,7 @@
by (simp_tac (simpset() addsimps [pnat_le_eq_less_or_eq]) 1);
qed "pnat_le_refl";
-val prems = goal thy "!!i. [| i <= j; j < k |] ==> i < (k::pnat)";
+val prems = goal (the_context ()) "!!i. [| i <= j; j < k |] ==> i < (k::pnat)";
by (dtac pnat_le_imp_less_or_eq 1);
by (blast_tac (claset() addIs [pnat_less_trans]) 1);
qed "pnat_le_less_trans";
@@ -384,7 +384,7 @@
by (simp_tac (simpset() addsimps [lemma]) 1);
qed "Least_pnat_def";
-val [prem1,prem2] = goalw thy [Least_pnat_def]
+val [prem1,prem2] = goalw (the_context ()) [Least_pnat_def]
"[| P(k::pnat); !!x. x<k ==> ~P(x) |] ==> (LEAST x. P(x)) = k";
by (rtac select_equality 1);
by (blast_tac (claset() addSIs [prem1,prem2]) 1);
@@ -647,7 +647,7 @@
simpset() addsimps [pnat_mult_left_commute]));
qed "pnat_same_multI2";
-val [prem] = goal thy
+val [prem] = goal (the_context ())
"(!!u. z = Abs_pnat(u) ==> P) ==> P";
by (cut_inst_tac [("x1","z")]
(rewrite_rule [pnat_def] (Rep_pnat RS Abs_pnat_inverse)) 1);
@@ -706,7 +706,7 @@
qed "pnat_of_nat_less_iff";
Addsimps [pnat_of_nat_less_iff RS sym];
-goalw PNat.thy [pnat_mult_def,pnat_of_nat_def]
+Goalw [pnat_mult_def,pnat_of_nat_def]
"pnat_of_nat n1 * pnat_of_nat n2 = \
\ pnat_of_nat (n1 * n2 + n1 + n2)";
by (auto_tac (claset(),simpset() addsimps [mult_Rep_pnat_mult,
--- a/src/HOL/Real/RealDef.ML Mon Jul 24 23:51:11 2000 +0200
+++ b/src/HOL/Real/RealDef.ML Mon Jul 24 23:51:46 2000 +0200
@@ -35,7 +35,7 @@
by (Blast_tac 1);
qed "realrelE_lemma";
-val [major,minor] = goal thy
+val [major,minor] = goal (the_context ())
"[| p: realrel; \
\ !!x1 y1 x2 y2. [| p = ((x1,y1),(x2,y2)); x1+y2 = x2+y1 \
\ |] ==> Q |] ==> Q";
@@ -94,7 +94,7 @@
by (Asm_full_simp_tac 1);
qed "inj_real_of_preal";
-val [prem] = goal thy
+val [prem] = goal (the_context ())
"(!!x y. z = Abs_real(realrel^^{(x,y)}) ==> P) ==> P";
by (res_inst_tac [("x1","z")]
(rewrite_rule [real_def] Rep_real RS quotientE) 1);
--- a/src/HOL/Set.ML Mon Jul 24 23:51:11 2000 +0200
+++ b/src/HOL/Set.ML Mon Jul 24 23:51:46 2000 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/set
+(* Title: HOL/Set.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
@@ -719,9 +719,9 @@
(*Split ifs on either side of the membership relation.
Not for Addsimps -- can cause goals to blow up!*)
bind_thm ("split_if_mem1",
- read_instantiate_sg (Theory.sign_of Set.thy) [("P", "%x. x : ?b")] split_if);
+ read_instantiate_sg (Theory.sign_of (the_context ())) [("P", "%x. x : ?b")] split_if);
bind_thm ("split_if_mem2",
- read_instantiate_sg (Theory.sign_of Set.thy) [("P", "%x. ?a : x")] split_if);
+ read_instantiate_sg (Theory.sign_of (the_context ())) [("P", "%x. ?a : x")] split_if);
bind_thms ("split_ifs", [if_bool_eq_conj, split_if_eq1, split_if_eq2,
split_if_mem1, split_if_mem2]);
--- a/src/HOL/Trancl.ML Mon Jul 24 23:51:11 2000 +0200
+++ b/src/HOL/Trancl.ML Mon Jul 24 23:51:46 2000 +0200
@@ -254,7 +254,7 @@
qed "trancl_induct";
(*Another induction rule for trancl, incorporating transitivity.*)
-val major::prems = goal thy
+val major::prems = goal (the_context ())
"[| (x,y) : r^+; \
\ !!x y. (x,y) : r ==> P x y; \
\ !!x y z. [| (x,y) : r^+; P x y; (y,z) : r^+; P y z |] ==> P x z \
--- a/src/HOL/Univ.ML Mon Jul 24 23:51:11 2000 +0200
+++ b/src/HOL/Univ.ML Mon Jul 24 23:51:46 2000 +0200
@@ -387,7 +387,7 @@
by (Blast_tac 1);
qed "Funs_mono";
-val [p] = goalw thy [Funs_def] "(!!x. f x : S) ==> f : Funs S";
+val [p] = goalw (the_context ()) [Funs_def] "(!!x. f x : S) ==> f : Funs S";
by (rtac CollectI 1);
by (rtac subsetI 1);
by (etac rangeE 1);
@@ -401,7 +401,7 @@
by (rtac rangeI 1);
qed "FunsD";
-val [p1, p2] = goalw thy [o_def]
+val [p1, p2] = goalw (the_context ()) [o_def]
"[| f : Funs R; !!x. x : R ==> r (a x) = x |] ==> r o (a o f) = f";
by (rtac (p2 RS ext) 1);
by (rtac (p1 RS FunsD) 1);
--- a/src/HOL/Vimage.ML Mon Jul 24 23:51:11 2000 +0200
+++ b/src/HOL/Vimage.ML Mon Jul 24 23:51:46 2000 +0200
@@ -79,7 +79,7 @@
(*A strange result used in Tools/inductive_package*)
bind_thm ("vimage_Collect",
allI RS
- prove_goalw thy [vimage_def]
+ prove_goalw (the_context ()) [vimage_def]
"! x. P (f x) = Q x ==> f -`` (Collect P) = Collect Q"
(fn prems => [cut_facts_tac prems 1, Fast_tac 1]));
--- a/src/HOL/WF.ML Mon Jul 24 23:51:11 2000 +0200
+++ b/src/HOL/WF.ML Mon Jul 24 23:51:46 2000 +0200
@@ -275,7 +275,7 @@
qed_spec_mp "is_recfun_equal";
-val prems as [wfr,transr,recfa,recgb,_] = goalw WF.thy [cut_def]
+val prems as [wfr,transr,recfa,recgb,_] = goalw (the_context ()) [cut_def]
"[| wf(r); trans(r); \
\ is_recfun r H a f; is_recfun r H b g; (b,a):r |] ==> \
\ cut f r b = g";
@@ -342,7 +342,7 @@
(*---------------------------------------------------------------------------
* This form avoids giant explosions in proofs. NOTE USE OF ==
*---------------------------------------------------------------------------*)
-val rew::prems = goal thy
+val rew::prems = goal (the_context ())
"[| f==wfrec r H; wf(r) |] ==> f(a) = H (cut f r a) a";
by (rewtac rew);
by (REPEAT (resolve_tac (prems@[wfrec]) 1));
--- a/src/HOL/WF_Rel.ML Mon Jul 24 23:51:11 2000 +0200
+++ b/src/HOL/WF_Rel.ML Mon Jul 24 23:51:46 2000 +0200
@@ -72,7 +72,7 @@
* Wellfoundedness of lexicographic combinations
*---------------------------------------------------------------------------*)
-val [wfa,wfb] = goalw thy [wf_def,lex_prod_def]
+val [wfa,wfb] = goalw (the_context ()) [wf_def,lex_prod_def]
"[| wf(ra); wf(rb) |] ==> wf(ra <*lex*> rb)";
by (EVERY1 [rtac allI,rtac impI]);
by (simp_tac (HOL_basic_ss addsimps [split_paired_All]) 1);
--- a/src/HOL/equalities.ML Mon Jul 24 23:51:11 2000 +0200
+++ b/src/HOL/equalities.ML Mon Jul 24 23:51:46 2000 +0200
@@ -104,7 +104,7 @@
by (Blast_tac 1);
qed "mk_disjoint_insert";
-bind_thm ("insert_Collect", prove_goal thy
+bind_thm ("insert_Collect", prove_goal (the_context ())
"insert a (Collect P) = {u. u ~= a --> P u}" (K [Auto_tac]));
Goal "u: A ==> (UN x:A. insert a (B x)) = insert a (UN x:A. B x)";
@@ -900,7 +900,7 @@
(** Miniscoping: pushing in big Unions and Intersections **)
local
- fun prover s = prove_goal thy s (fn _ => [Blast_tac 1])
+ fun prover s = prove_goal (the_context ()) s (fn _ => [Blast_tac 1])
in
val UN_simps = map prover
["!!C. c: C ==> (UN x:C. insert a (B x)) = insert a (UN x:C. B x)",