src/HOL/simpdata.ML
changeset 7357 d0e16da40ea2
parent 7213 08a354bbc34c
child 7369 2d2110cda81e
     1.1 --- a/src/HOL/simpdata.ML	Wed Aug 25 20:46:40 1999 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Wed Aug 25 20:49:02 1999 +0200
     1.3 @@ -89,14 +89,14 @@
     1.4  end;
     1.5  
     1.6  
     1.7 -val [prem] = goal HOL.thy "x==y ==> x=y";
     1.8 +val [prem] = goal (the_context ()) "x==y ==> x=y";
     1.9  by (rewtac prem);
    1.10  by (rtac refl 1);
    1.11  qed "meta_eq_to_obj_eq";
    1.12  
    1.13  local
    1.14  
    1.15 -  fun prover s = prove_goal HOL.thy s (fn _ => [(Blast_tac 1)]);
    1.16 +  fun prover s = prove_goal (the_context ()) s (fn _ => [(Blast_tac 1)]);
    1.17  
    1.18  in
    1.19  
    1.20 @@ -157,7 +157,7 @@
    1.21  
    1.22  
    1.23  val imp_cong = impI RSN
    1.24 -    (2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
    1.25 +    (2, prove_goal (the_context ()) "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
    1.26          (fn _=> [(Blast_tac 1)]) RS mp RS mp);
    1.27  
    1.28  (*Miniscoping: pushing in existential quantifiers*)
    1.29 @@ -182,10 +182,10 @@
    1.30  (* elimination of existential quantifiers in assumptions *)
    1.31  
    1.32  val ex_all_equiv =
    1.33 -  let val lemma1 = prove_goal HOL.thy
    1.34 +  let val lemma1 = prove_goal (the_context ())
    1.35          "(? x. P(x) ==> PROP Q) ==> (!!x. P(x) ==> PROP Q)"
    1.36          (fn prems => [resolve_tac prems 1, etac exI 1]);
    1.37 -      val lemma2 = prove_goalw HOL.thy [Ex_def]
    1.38 +      val lemma2 = prove_goalw (the_context ()) [Ex_def]
    1.39          "(!!x. P(x) ==> PROP Q) ==> (? x. P(x) ==> PROP Q)"
    1.40          (fn prems => [(REPEAT(resolve_tac prems 1))])
    1.41    in equal_intr lemma1 lemma2 end;
    1.42 @@ -194,13 +194,13 @@
    1.43  
    1.44  (* Elimination of True from asumptions: *)
    1.45  
    1.46 -val True_implies_equals = prove_goal HOL.thy
    1.47 +val True_implies_equals = prove_goal (the_context ())
    1.48   "(True ==> PROP P) == PROP P"
    1.49  (fn _ => [rtac equal_intr_rule 1, atac 2,
    1.50            METAHYPS (fn prems => resolve_tac prems 1) 1,
    1.51            rtac TrueI 1]);
    1.52  
    1.53 -fun prove nm thm  = qed_goal nm HOL.thy thm (fn _ => [(Blast_tac 1)]);
    1.54 +fun prove nm thm  = qed_goal nm (the_context ()) thm (fn _ => [(Blast_tac 1)]);
    1.55  
    1.56  prove "conj_commute" "(P&Q) = (Q&P)";
    1.57  prove "conj_left_commute" "(P&(Q&R)) = (Q&(P&R))";
    1.58 @@ -255,19 +255,19 @@
    1.59  (* '&' congruence rule: not included by default!
    1.60     May slow rewrite proofs down by as much as 50% *)
    1.61  
    1.62 -let val th = prove_goal HOL.thy 
    1.63 +let val th = prove_goal (the_context ()) 
    1.64                  "(P=P')--> (P'--> (Q=Q'))--> ((P&Q) = (P'&Q'))"
    1.65                  (fn _=> [(Blast_tac 1)])
    1.66  in  bind_thm("conj_cong",standard (impI RSN (2, th RS mp RS mp)))  end;
    1.67  
    1.68 -let val th = prove_goal HOL.thy 
    1.69 +let val th = prove_goal (the_context ()) 
    1.70                  "(Q=Q')--> (Q'--> (P=P'))--> ((P&Q) = (P'&Q'))"
    1.71                  (fn _=> [(Blast_tac 1)])
    1.72  in  bind_thm("rev_conj_cong",standard (impI RSN (2, th RS mp RS mp)))  end;
    1.73  
    1.74  (* '|' congruence rule: not included by default! *)
    1.75  
    1.76 -let val th = prove_goal HOL.thy 
    1.77 +let val th = prove_goal (the_context ()) 
    1.78                  "(P=P')--> (~P'--> (Q=Q'))--> ((P|Q) = (P'|Q'))"
    1.79                  (fn _=> [(Blast_tac 1)])
    1.80  in  bind_thm("disj_cong",standard (impI RSN (2, th RS mp RS mp)))  end;
    1.81 @@ -358,10 +358,10 @@
    1.82  
    1.83  local
    1.84  val ex_pattern =
    1.85 -  Thm.read_cterm (Theory.sign_of HOL.thy) ("EX x. P(x) & Q(x)",HOLogic.boolT)
    1.86 +  Thm.read_cterm (Theory.sign_of (the_context ())) ("EX x. P(x) & Q(x)",HOLogic.boolT)
    1.87  
    1.88  val all_pattern =
    1.89 -  Thm.read_cterm (Theory.sign_of HOL.thy) ("ALL x. P(x) & P'(x) --> Q(x)",HOLogic.boolT)
    1.90 +  Thm.read_cterm (Theory.sign_of (the_context ())) ("ALL x. P(x) & P'(x) --> Q(x)",HOLogic.boolT)
    1.91  
    1.92  in
    1.93  val defEX_regroup =
    1.94 @@ -478,7 +478,7 @@
    1.95  
    1.96  
    1.97  (*For expand_case_tac*)
    1.98 -val prems = goal HOL.thy "[| P ==> Q(True); ~P ==> Q(False) |] ==> Q(P)";
    1.99 +val prems = goal (the_context ()) "[| P ==> Q(True); ~P ==> Q(False) |] ==> Q(P)";
   1.100  by (case_tac "P" 1);
   1.101  by (ALLGOALS (asm_simp_tac (HOL_ss addsimps prems)));
   1.102  val expand_case = result();
   1.103 @@ -491,9 +491,8 @@
   1.104      Simp_tac i;
   1.105  
   1.106  
   1.107 -(* install implicit simpset *)
   1.108 -
   1.109 -simpset_ref() := HOL_ss addcongs [if_weak_cong];
   1.110 +(* default simpset *)
   1.111 +val simpsetup = [fn thy => (simpset_ref_of thy := HOL_ss addcongs [if_weak_cong]; thy)];
   1.112  
   1.113  
   1.114  (*** integration of simplifier with classical reasoner ***)