src/Pure/drule.ML
changeset 3991 4cb2f2422695
parent 3766 8e1794c4e81b
child 4016 90aebb69c04e
     1.1 --- a/src/Pure/drule.ML	Fri Oct 24 17:12:35 1997 +0200
     1.2 +++ b/src/Pure/drule.ML	Fri Oct 24 17:13:21 1997 +0200
     1.3 @@ -68,10 +68,10 @@
     1.4    val zero_var_indexes	: thm -> thm
     1.5  end;
     1.6  
     1.7 -
     1.8  structure Drule : DRULE =
     1.9  struct
    1.10  
    1.11 +
    1.12  (** some cterm->cterm operations: much faster than calling cterm_of! **)
    1.13  
    1.14  (** SAME NAMES as in structure Logic: use compound identifiers! **)
    1.15 @@ -389,22 +389,22 @@
    1.16  (*** Meta-Rewriting Rules ***)
    1.17  
    1.18  val reflexive_thm =
    1.19 -  let val cx = cterm_of Sign.proto_pure (Var(("x",0),TVar(("'a",0),logicS)))
    1.20 +  let val cx = cterm_of (sign_of ProtoPure.thy) (Var(("x",0),TVar(("'a",0),logicS)))
    1.21    in Thm.reflexive cx end;
    1.22  
    1.23  val symmetric_thm =
    1.24 -  let val xy = read_cterm Sign.proto_pure ("x::'a::logic == y",propT)
    1.25 +  let val xy = read_cterm (sign_of ProtoPure.thy) ("x::'a::logic == y",propT)
    1.26    in standard(Thm.implies_intr_hyps(Thm.symmetric(Thm.assume xy))) end;
    1.27  
    1.28  val transitive_thm =
    1.29 -  let val xy = read_cterm Sign.proto_pure ("x::'a::logic == y",propT)
    1.30 -      val yz = read_cterm Sign.proto_pure ("y::'a::logic == z",propT)
    1.31 +  let val xy = read_cterm (sign_of ProtoPure.thy) ("x::'a::logic == y",propT)
    1.32 +      val yz = read_cterm (sign_of ProtoPure.thy) ("y::'a::logic == z",propT)
    1.33        val xythm = Thm.assume xy and yzthm = Thm.assume yz
    1.34    in standard(Thm.implies_intr yz (Thm.transitive xythm yzthm)) end;
    1.35  
    1.36  (** Below, a "conversion" has type cterm -> thm **)
    1.37  
    1.38 -val refl_implies = reflexive (cterm_of Sign.proto_pure implies);
    1.39 +val refl_implies = reflexive (cterm_of (sign_of ProtoPure.thy) implies);
    1.40  
    1.41  (*In [A1,...,An]==>B, rewrite the selected A's only -- for rewrite_goals_tac*)
    1.42  (*Do not rewrite flex-flex pairs*)
    1.43 @@ -474,8 +474,8 @@
    1.44      end
    1.45      handle THM _ => err th | bind => err th
    1.46  in
    1.47 -val flexpair_intr = flexpair_inst (symmetric flexpair_def)
    1.48 -and flexpair_elim = flexpair_inst flexpair_def
    1.49 +val flexpair_intr = flexpair_inst (symmetric ProtoPure.flexpair_def)
    1.50 +and flexpair_elim = flexpair_inst ProtoPure.flexpair_def
    1.51  end;
    1.52  
    1.53  (*Version for flexflex pairs -- this supports lifting.*)
    1.54 @@ -486,17 +486,17 @@
    1.55  (*** Some useful meta-theorems ***)
    1.56  
    1.57  (*The rule V/V, obtains assumption solving for eresolve_tac*)
    1.58 -val asm_rl = trivial(read_cterm Sign.proto_pure ("PROP ?psi",propT));
    1.59 +val asm_rl = trivial(read_cterm (sign_of ProtoPure.thy) ("PROP ?psi",propT));
    1.60  
    1.61  (*Meta-level cut rule: [| V==>W; V |] ==> W *)
    1.62 -val cut_rl = trivial(read_cterm Sign.proto_pure
    1.63 +val cut_rl = trivial(read_cterm (sign_of ProtoPure.thy)
    1.64          ("PROP ?psi ==> PROP ?theta", propT));
    1.65  
    1.66  (*Generalized elim rule for one conclusion; cut_rl with reversed premises:
    1.67       [| PROP V;  PROP V ==> PROP W |] ==> PROP W *)
    1.68  val revcut_rl =
    1.69 -  let val V = read_cterm Sign.proto_pure ("PROP V", propT)
    1.70 -      and VW = read_cterm Sign.proto_pure ("PROP V ==> PROP W", propT);
    1.71 +  let val V = read_cterm (sign_of ProtoPure.thy) ("PROP V", propT)
    1.72 +      and VW = read_cterm (sign_of ProtoPure.thy) ("PROP V ==> PROP W", propT);
    1.73    in  standard (implies_intr V
    1.74                  (implies_intr VW
    1.75                   (implies_elim (assume VW) (assume V))))
    1.76 @@ -504,16 +504,16 @@
    1.77  
    1.78  (*for deleting an unwanted assumption*)
    1.79  val thin_rl =
    1.80 -  let val V = read_cterm Sign.proto_pure ("PROP V", propT)
    1.81 -      and W = read_cterm Sign.proto_pure ("PROP W", propT);
    1.82 +  let val V = read_cterm (sign_of ProtoPure.thy) ("PROP V", propT)
    1.83 +      and W = read_cterm (sign_of ProtoPure.thy) ("PROP W", propT);
    1.84    in  standard (implies_intr V (implies_intr W (assume W)))
    1.85    end;
    1.86  
    1.87  (* (!!x. PROP ?V) == PROP ?V       Allows removal of redundant parameters*)
    1.88  val triv_forall_equality =
    1.89 -  let val V  = read_cterm Sign.proto_pure ("PROP V", propT)
    1.90 -      and QV = read_cterm Sign.proto_pure ("!!x::'a. PROP V", propT)
    1.91 -      and x  = read_cterm Sign.proto_pure ("x", TFree("'a",logicS));
    1.92 +  let val V  = read_cterm (sign_of ProtoPure.thy) ("PROP V", propT)
    1.93 +      and QV = read_cterm (sign_of ProtoPure.thy) ("!!x::'a. PROP V", propT)
    1.94 +      and x  = read_cterm (sign_of ProtoPure.thy) ("x", TFree("'a",logicS));
    1.95    in  standard (equal_intr (implies_intr QV (forall_elim x (assume QV)))
    1.96                             (implies_intr V  (forall_intr x (assume V))))
    1.97    end;
    1.98 @@ -523,12 +523,12 @@
    1.99     `thm COMP swap_prems_rl' swaps the first two premises of `thm'
   1.100  *)
   1.101  val swap_prems_rl =
   1.102 -  let val cmajor = read_cterm Sign.proto_pure
   1.103 +  let val cmajor = read_cterm (sign_of ProtoPure.thy)
   1.104              ("PROP PhiA ==> PROP PhiB ==> PROP Psi", propT);
   1.105        val major = assume cmajor;
   1.106 -      val cminor1 = read_cterm Sign.proto_pure  ("PROP PhiA", propT);
   1.107 +      val cminor1 = read_cterm (sign_of ProtoPure.thy)  ("PROP PhiA", propT);
   1.108        val minor1 = assume cminor1;
   1.109 -      val cminor2 = read_cterm Sign.proto_pure  ("PROP PhiB", propT);
   1.110 +      val cminor2 = read_cterm (sign_of ProtoPure.thy)  ("PROP PhiB", propT);
   1.111        val minor2 = assume cminor2;
   1.112    in standard
   1.113         (implies_intr cmajor (implies_intr cminor2 (implies_intr cminor1
   1.114 @@ -540,8 +540,8 @@
   1.115     Introduction rule for == using ==> not meta-hyps.
   1.116  *)
   1.117  val equal_intr_rule =
   1.118 -  let val PQ = read_cterm Sign.proto_pure ("PROP phi ==> PROP psi", propT)
   1.119 -      and QP = read_cterm Sign.proto_pure ("PROP psi ==> PROP phi", propT)
   1.120 +  let val PQ = read_cterm (sign_of ProtoPure.thy) ("PROP phi ==> PROP psi", propT)
   1.121 +      and QP = read_cterm (sign_of ProtoPure.thy) ("PROP psi ==> PROP phi", propT)
   1.122    in  equal_intr (assume PQ) (assume QP)
   1.123        |> implies_intr QP
   1.124        |> implies_intr PQ