# HG changeset patch # User wenzelm # Date 964475506 -7200 # Node ID 4b6bc2b347e5aa72bca892293a3a404956e5b46f # Parent d8dfa816a3686bce6a2934a3892a9d70f587f9fa avoid referencing thy value; diff -r d8dfa816a368 -r 4b6bc2b347e5 src/HOL/Fun.ML --- 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; diff -r d8dfa816a368 -r 4b6bc2b347e5 src/HOL/Gfp.ML --- 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)); diff -r d8dfa816a368 -r 4b6bc2b347e5 src/HOL/Integ/IntDiv.ML --- 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, diff -r d8dfa816a368 -r 4b6bc2b347e5 src/HOL/Lfp.ML --- 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"; diff -r d8dfa816a368 -r 4b6bc2b347e5 src/HOL/Ord.ML --- 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) P; x=y ==> P; y P |] ==> P"; by(cut_facts_tac [linorder_less_linear] 1); by(REPEAT(eresolve_tac (prems@[disjE]) 1)); diff -r d8dfa816a368 -r 4b6bc2b347e5 src/HOL/Real/Hyperreal/Filter.ML --- 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); diff -r d8dfa816a368 -r 4b6bc2b347e5 src/HOL/Real/PNat.ML --- 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 ~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, diff -r d8dfa816a368 -r 4b6bc2b347e5 src/HOL/Real/RealDef.ML --- 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); diff -r d8dfa816a368 -r 4b6bc2b347e5 src/HOL/Set.ML --- 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]); diff -r d8dfa816a368 -r 4b6bc2b347e5 src/HOL/Trancl.ML --- 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 \ diff -r d8dfa816a368 -r 4b6bc2b347e5 src/HOL/Univ.ML --- 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); diff -r d8dfa816a368 -r 4b6bc2b347e5 src/HOL/Vimage.ML --- 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])); diff -r d8dfa816a368 -r 4b6bc2b347e5 src/HOL/WF.ML --- 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)); diff -r d8dfa816a368 -r 4b6bc2b347e5 src/HOL/WF_Rel.ML --- 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); diff -r d8dfa816a368 -r 4b6bc2b347e5 src/HOL/equalities.ML --- 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)",