ProtoPure.thy;
authorwenzelm
Fri Oct 24 17:13:21 1997 +0200 (1997-10-24)
changeset 39914cb2f2422695
parent 3990 a8c80f5fdd16
child 3992 8b87ba92f7a1
ProtoPure.thy;
src/Pure/drule.ML
src/Pure/tactic.ML
src/Pure/tctical.ML
src/Pure/unify.ML
     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
     2.1 --- a/src/Pure/tactic.ML	Fri Oct 24 17:12:35 1997 +0200
     2.2 +++ b/src/Pure/tactic.ML	Fri Oct 24 17:13:21 1997 +0200
     2.3 @@ -310,7 +310,7 @@
     2.4    increment revcut_rl instead.*)
     2.5  fun make_elim_preserve rl = 
     2.6    let val {maxidx,...} = rep_thm rl
     2.7 -      fun cvar ixn = cterm_of Sign.proto_pure (Var(ixn,propT));
     2.8 +      fun cvar ixn = cterm_of (sign_of ProtoPure.thy) (Var(ixn,propT));
     2.9        val revcut_rl' = 
    2.10  	  instantiate ([],  [(cvar("V",0), cvar("V",maxidx+1)),
    2.11  			     (cvar("W",0), cvar("W",maxidx+1))]) revcut_rl
     3.1 --- a/src/Pure/tctical.ML	Fri Oct 24 17:12:35 1997 +0200
     3.2 +++ b/src/Pure/tctical.ML	Fri Oct 24 17:13:21 1997 +0200
     3.3 @@ -334,7 +334,7 @@
     3.4  (*SELECT_GOAL optimization: replace the conclusion by a variable X,
     3.5    to avoid copying.  Proof states have X==concl as an assuption.*)
     3.6  
     3.7 -val prop_equals = cterm_of Sign.proto_pure 
     3.8 +val prop_equals = cterm_of (sign_of ProtoPure.thy) 
     3.9                      (Const("==", propT-->propT-->propT));
    3.10  
    3.11  fun mk_prop_equals(t,u) = capply (capply prop_equals t) u;
    3.12 @@ -343,7 +343,7 @@
    3.13    It is paired with a function to undo the transformation.  If ct contains
    3.14    Vars then it returns ct==>ct.*)
    3.15  fun eq_trivial ct =
    3.16 -  let val xfree = cterm_of Sign.proto_pure (Free (gensym"EQ_TRIVIAL_", propT))
    3.17 +  let val xfree = cterm_of (sign_of ProtoPure.thy) (Free (gensym"EQ_TRIVIAL_", propT))
    3.18        val ct_eq_x = mk_prop_equals (ct, xfree)
    3.19        and refl_ct = reflexive ct
    3.20        fun restore th = 
    3.21 @@ -367,7 +367,7 @@
    3.22  
    3.23  (* (!!selct. PROP ?V) ==> PROP ?V ;  contains NO TYPE VARIABLES.*)
    3.24  val dummy_quant_rl = 
    3.25 -  read_cterm Sign.proto_pure ("!!selct::prop. PROP V",propT) |>
    3.26 +  read_cterm (sign_of ProtoPure.thy) ("!!selct::prop. PROP V",propT) |>
    3.27    assume |> forall_elim_var 0 |> standard;
    3.28  
    3.29  (* Prevent the subgoal's assumptions from becoming additional subgoals in the
     4.1 --- a/src/Pure/unify.ML	Fri Oct 24 17:12:35 1997 +0200
     4.2 +++ b/src/Pure/unify.ML	Fri Oct 24 17:13:21 1997 +0200
     4.3 @@ -41,7 +41,7 @@
     4.4  and trace_types = ref false	(*announce potential incompleteness
     4.5  				  of type unification*)
     4.6  
     4.7 -val sgr = ref(Sign.proto_pure);
     4.8 +val sgr = ref(Sign.pre_pure);
     4.9  
    4.10  type binderlist = (string*typ) list;
    4.11