src/Pure/drule.ML
changeset 8129 29e239c7b8c2
parent 8086 78e254305ae6
child 8328 efbcec3eb02f
     1.1 --- a/src/Pure/drule.ML	Fri Jan 14 12:17:53 2000 +0100
     1.2 +++ b/src/Pure/drule.ML	Mon Jan 17 14:10:32 2000 +0100
     1.3 @@ -30,6 +30,8 @@
     1.4    val freeze_thaw	: thm -> thm * (thm -> thm)
     1.5    val implies_elim_list	: thm -> thm list -> thm
     1.6    val implies_intr_list	: cterm list -> thm -> thm
     1.7 +  val instantiate       :
     1.8 +    (indexname * ctyp) list * (cterm * cterm) list -> thm -> thm
     1.9    val zero_var_indexes	: thm -> thm
    1.10    val standard		: thm -> thm
    1.11    val rotate_prems      : int -> thm -> thm
    1.12 @@ -256,7 +258,7 @@
    1.13                      cterm_of sign (Var((b,0),T'))) :: varpairs(vars,bs)
    1.14                  end
    1.15            | varpairs _ = raise TERM("varpairs", []);
    1.16 -    in instantiate (ctye, varpairs(vars,rev bs)) th end;
    1.17 +    in Thm.instantiate (ctye, varpairs(vars,rev bs)) th end;
    1.18  
    1.19  
    1.20  (*Standard form of object-rule: no hypotheses, Frees, or outer quantifiers;
    1.21 @@ -293,7 +295,7 @@
    1.22  	     fun thaw th' = 
    1.23  		 th' |> forall_intr_list (map #2 insts)
    1.24  	             |> forall_elim_list (map #1 insts)
    1.25 -	 in  (instantiate ([],insts) fth, thaw)  end
    1.26 +	 in  (Thm.instantiate ([],insts) fth, thaw)  end
    1.27   end;
    1.28  
    1.29  
    1.30 @@ -359,42 +361,6 @@
    1.31          [th] => th
    1.32        | _ =>   raise THM("COMP", 1, [tha,thb]);
    1.33  
    1.34 -(*Instantiate theorem th, reading instantiations under signature sg*)
    1.35 -fun read_instantiate_sg sg sinsts th =
    1.36 -    let val ts = types_sorts th;
    1.37 -        val used = add_term_tvarnames(#prop(rep_thm th),[]);
    1.38 -    in  instantiate (read_insts sg ts ts used sinsts) th  end;
    1.39 -
    1.40 -(*Instantiate theorem th, reading instantiations under theory of th*)
    1.41 -fun read_instantiate sinsts th =
    1.42 -    read_instantiate_sg (#sign (rep_thm th)) sinsts th;
    1.43 -
    1.44 -
    1.45 -(*Left-to-right replacements: tpairs = [...,(vi,ti),...].
    1.46 -  Instantiates distinct Vars by terms, inferring type instantiations. *)
    1.47 -local
    1.48 -  fun add_types ((ct,cu), (sign,tye,maxidx)) =
    1.49 -    let val {sign=signt, t=t, T= T, maxidx=maxt,...} = rep_cterm ct
    1.50 -        and {sign=signu, t=u, T= U, maxidx=maxu,...} = rep_cterm cu;
    1.51 -        val maxi = Int.max(maxidx, Int.max(maxt, maxu));
    1.52 -        val sign' = Sign.merge(sign, Sign.merge(signt, signu))
    1.53 -        val (tye',maxi') = Type.unify (#tsig(Sign.rep_sg sign')) maxi tye (T,U)
    1.54 -          handle Type.TUNIFY => raise TYPE("add_types", [T,U], [t,u])
    1.55 -    in  (sign', tye', maxi')  end;
    1.56 -in
    1.57 -fun cterm_instantiate ctpairs0 th =
    1.58 -  let val (sign,tye,_) = foldr add_types (ctpairs0, (#sign(rep_thm th),[],0))
    1.59 -      val tsig = #tsig(Sign.rep_sg sign);
    1.60 -      fun instT(ct,cu) = let val inst = subst_TVars tye
    1.61 -                         in (cterm_fun inst ct, cterm_fun inst cu) end
    1.62 -      fun ctyp2 (ix,T) = (ix, ctyp_of sign T)
    1.63 -  in  instantiate (map ctyp2 tye, map instT ctpairs0) th  end
    1.64 -  handle TERM _ =>
    1.65 -           raise THM("cterm_instantiate: incompatible signatures",0,[th])
    1.66 -       | TYPE (msg, _, _) => raise THM(msg, 0, [th])
    1.67 -end;
    1.68 -
    1.69 -
    1.70  (** theorem equality **)
    1.71  
    1.72  (*Do the two theorems have the same signature?*)
    1.73 @@ -495,45 +461,6 @@
    1.74    else raise THM("rewrite_goal_rule",i,[thm]);
    1.75  
    1.76  
    1.77 -(** Derived rules mainly for METAHYPS **)
    1.78 -
    1.79 -(*Given the term "a", takes (%x.t)==(%x.u) to t[a/x]==u[a/x]*)
    1.80 -fun equal_abs_elim ca eqth =
    1.81 -  let val {sign=signa, t=a, ...} = rep_cterm ca
    1.82 -      and combth = combination eqth (reflexive ca)
    1.83 -      val {sign,prop,...} = rep_thm eqth
    1.84 -      val (abst,absu) = Logic.dest_equals prop
    1.85 -      val cterm = cterm_of (Sign.merge (sign,signa))
    1.86 -  in  transitive (symmetric (beta_conversion (cterm (abst$a))))
    1.87 -           (transitive combth (beta_conversion (cterm (absu$a))))
    1.88 -  end
    1.89 -  handle THM _ => raise THM("equal_abs_elim", 0, [eqth]);
    1.90 -
    1.91 -(*Calling equal_abs_elim with multiple terms*)
    1.92 -fun equal_abs_elim_list cts th = foldr (uncurry equal_abs_elim) (rev cts, th);
    1.93 -
    1.94 -local
    1.95 -  val alpha = TVar(("'a",0), [])     (*  type ?'a::{}  *)
    1.96 -  fun err th = raise THM("flexpair_inst: ", 0, [th])
    1.97 -  fun flexpair_inst def th =
    1.98 -    let val {prop = Const _ $ t $ u,  sign,...} = rep_thm th
    1.99 -        val cterm = cterm_of sign
   1.100 -        fun cvar a = cterm(Var((a,0),alpha))
   1.101 -        val def' = cterm_instantiate [(cvar"t", cterm t), (cvar"u", cterm u)]
   1.102 -                   def
   1.103 -    in  equal_elim def' th
   1.104 -    end
   1.105 -    handle THM _ => err th | Bind => err th
   1.106 -in
   1.107 -val flexpair_intr = flexpair_inst (symmetric ProtoPure.flexpair_def)
   1.108 -and flexpair_elim = flexpair_inst ProtoPure.flexpair_def
   1.109 -end;
   1.110 -
   1.111 -(*Version for flexflex pairs -- this supports lifting.*)
   1.112 -fun flexpair_abs_elim_list cts =
   1.113 -    flexpair_intr o equal_abs_elim_list cts o flexpair_elim;
   1.114 -
   1.115 -
   1.116  (*** Some useful meta-theorems ***)
   1.117  
   1.118  (*The rule V/V, obtains assumption solving for eresolve_tac*)
   1.119 @@ -602,7 +529,86 @@
   1.120    end;
   1.121  
   1.122  
   1.123 -(* GOAL (PROP A) <==> PROP A *)
   1.124 +(*** Instantiate theorem th, reading instantiations under signature sg ****)
   1.125 +
   1.126 +(*Version that normalizes the result: Thm.instantiate no longer does that*)
   1.127 +fun instantiate instpair th = Thm.instantiate instpair th  COMP   asm_rl;
   1.128 +
   1.129 +fun read_instantiate_sg sg sinsts th =
   1.130 +    let val ts = types_sorts th;
   1.131 +        val used = add_term_tvarnames(#prop(rep_thm th),[]);
   1.132 +    in  instantiate (read_insts sg ts ts used sinsts) th  end;
   1.133 +
   1.134 +(*Instantiate theorem th, reading instantiations under theory of th*)
   1.135 +fun read_instantiate sinsts th =
   1.136 +    read_instantiate_sg (#sign (rep_thm th)) sinsts th;
   1.137 +
   1.138 +
   1.139 +(*Left-to-right replacements: tpairs = [...,(vi,ti),...].
   1.140 +  Instantiates distinct Vars by terms, inferring type instantiations. *)
   1.141 +local
   1.142 +  fun add_types ((ct,cu), (sign,tye,maxidx)) =
   1.143 +    let val {sign=signt, t=t, T= T, maxidx=maxt,...} = rep_cterm ct
   1.144 +        and {sign=signu, t=u, T= U, maxidx=maxu,...} = rep_cterm cu;
   1.145 +        val maxi = Int.max(maxidx, Int.max(maxt, maxu));
   1.146 +        val sign' = Sign.merge(sign, Sign.merge(signt, signu))
   1.147 +        val (tye',maxi') = Type.unify (#tsig(Sign.rep_sg sign')) maxi tye (T,U)
   1.148 +          handle Type.TUNIFY => raise TYPE("add_types", [T,U], [t,u])
   1.149 +    in  (sign', tye', maxi')  end;
   1.150 +in
   1.151 +fun cterm_instantiate ctpairs0 th =
   1.152 +  let val (sign,tye,_) = foldr add_types (ctpairs0, (#sign(rep_thm th),[],0))
   1.153 +      val tsig = #tsig(Sign.rep_sg sign);
   1.154 +      fun instT(ct,cu) = let val inst = subst_TVars tye
   1.155 +                         in (cterm_fun inst ct, cterm_fun inst cu) end
   1.156 +      fun ctyp2 (ix,T) = (ix, ctyp_of sign T)
   1.157 +  in  instantiate (map ctyp2 tye, map instT ctpairs0) th  end
   1.158 +  handle TERM _ =>
   1.159 +           raise THM("cterm_instantiate: incompatible signatures",0,[th])
   1.160 +       | TYPE (msg, _, _) => raise THM(msg, 0, [th])
   1.161 +end;
   1.162 +
   1.163 +
   1.164 +(** Derived rules mainly for METAHYPS **)
   1.165 +
   1.166 +(*Given the term "a", takes (%x.t)==(%x.u) to t[a/x]==u[a/x]*)
   1.167 +fun equal_abs_elim ca eqth =
   1.168 +  let val {sign=signa, t=a, ...} = rep_cterm ca
   1.169 +      and combth = combination eqth (reflexive ca)
   1.170 +      val {sign,prop,...} = rep_thm eqth
   1.171 +      val (abst,absu) = Logic.dest_equals prop
   1.172 +      val cterm = cterm_of (Sign.merge (sign,signa))
   1.173 +  in  transitive (symmetric (beta_conversion (cterm (abst$a))))
   1.174 +           (transitive combth (beta_conversion (cterm (absu$a))))
   1.175 +  end
   1.176 +  handle THM _ => raise THM("equal_abs_elim", 0, [eqth]);
   1.177 +
   1.178 +(*Calling equal_abs_elim with multiple terms*)
   1.179 +fun equal_abs_elim_list cts th = foldr (uncurry equal_abs_elim) (rev cts, th);
   1.180 +
   1.181 +local
   1.182 +  val alpha = TVar(("'a",0), [])     (*  type ?'a::{}  *)
   1.183 +  fun err th = raise THM("flexpair_inst: ", 0, [th])
   1.184 +  fun flexpair_inst def th =
   1.185 +    let val {prop = Const _ $ t $ u,  sign,...} = rep_thm th
   1.186 +        val cterm = cterm_of sign
   1.187 +        fun cvar a = cterm(Var((a,0),alpha))
   1.188 +        val def' = cterm_instantiate [(cvar"t", cterm t), (cvar"u", cterm u)]
   1.189 +                   def
   1.190 +    in  equal_elim def' th
   1.191 +    end
   1.192 +    handle THM _ => err th | Bind => err th
   1.193 +in
   1.194 +val flexpair_intr = flexpair_inst (symmetric ProtoPure.flexpair_def)
   1.195 +and flexpair_elim = flexpair_inst ProtoPure.flexpair_def
   1.196 +end;
   1.197 +
   1.198 +(*Version for flexflex pairs -- this supports lifting.*)
   1.199 +fun flexpair_abs_elim_list cts =
   1.200 +    flexpair_intr o equal_abs_elim_list cts o flexpair_elim;
   1.201 +
   1.202 +
   1.203 +(*** GOAL (PROP A) <==> PROP A ***)
   1.204  
   1.205  local
   1.206    val A = read_prop "PROP A";