1.1 --- a/src/Pure/drule.ML Thu Mar 02 10:29:29 2000 +0100
1.2 +++ b/src/Pure/drule.ML Thu Mar 02 18:18:10 2000 +0100
1.3 @@ -11,97 +11,98 @@
1.4 signature BASIC_DRULE =
1.5 sig
1.6 val dest_implies : cterm -> cterm * cterm
1.7 - val skip_flexpairs : cterm -> cterm
1.8 - val strip_imp_prems : cterm -> cterm list
1.9 - val cprems_of : thm -> cterm list
1.10 - val read_insts :
1.11 + val skip_flexpairs : cterm -> cterm
1.12 + val strip_imp_prems : cterm -> cterm list
1.13 + val cprems_of : thm -> cterm list
1.14 + val read_insts :
1.15 Sign.sg -> (indexname -> typ option) * (indexname -> sort option)
1.16 -> (indexname -> typ option) * (indexname -> sort option)
1.17 -> string list -> (string*string)list
1.18 -> (indexname*ctyp)list * (cterm*cterm)list
1.19 val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option)
1.20 val strip_shyps_warning : thm -> thm
1.21 - val forall_intr_list : cterm list -> thm -> thm
1.22 - val forall_intr_frees : thm -> thm
1.23 - val forall_intr_vars : thm -> thm
1.24 - val forall_elim_list : cterm list -> thm -> thm
1.25 - val forall_elim_var : int -> thm -> thm
1.26 - val forall_elim_vars : int -> thm -> thm
1.27 - val freeze_thaw : thm -> thm * (thm -> thm)
1.28 - val implies_elim_list : thm -> thm list -> thm
1.29 - val implies_intr_list : cterm list -> thm -> thm
1.30 + val forall_intr_list : cterm list -> thm -> thm
1.31 + val forall_intr_frees : thm -> thm
1.32 + val forall_intr_vars : thm -> thm
1.33 + val forall_elim_list : cterm list -> thm -> thm
1.34 + val forall_elim_var : int -> thm -> thm
1.35 + val forall_elim_vars : int -> thm -> thm
1.36 + val freeze_thaw : thm -> thm * (thm -> thm)
1.37 + val implies_elim_list : thm -> thm list -> thm
1.38 + val implies_intr_list : cterm list -> thm -> thm
1.39 val instantiate :
1.40 (indexname * ctyp) list * (cterm * cterm) list -> thm -> thm
1.41 - val zero_var_indexes : thm -> thm
1.42 - val standard : thm -> thm
1.43 + val zero_var_indexes : thm -> thm
1.44 + val standard : thm -> thm
1.45 val rotate_prems : int -> thm -> thm
1.46 - val assume_ax : theory -> string -> thm
1.47 - val RSN : thm * (int * thm) -> thm
1.48 - val RS : thm * thm -> thm
1.49 - val RLN : thm list * (int * thm list) -> thm list
1.50 - val RL : thm list * thm list -> thm list
1.51 - val MRS : thm list * thm -> thm
1.52 - val MRL : thm list list * thm list -> thm list
1.53 - val compose : thm * int * thm -> thm list
1.54 - val COMP : thm * thm -> thm
1.55 + val assume_ax : theory -> string -> thm
1.56 + val RSN : thm * (int * thm) -> thm
1.57 + val RS : thm * thm -> thm
1.58 + val RLN : thm list * (int * thm list) -> thm list
1.59 + val RL : thm list * thm list -> thm list
1.60 + val MRS : thm list * thm -> thm
1.61 + val MRL : thm list list * thm list -> thm list
1.62 + val compose : thm * int * thm -> thm list
1.63 + val COMP : thm * thm -> thm
1.64 val read_instantiate_sg: Sign.sg -> (string*string)list -> thm -> thm
1.65 - val read_instantiate : (string*string)list -> thm -> thm
1.66 - val cterm_instantiate : (cterm*cterm)list -> thm -> thm
1.67 - val weak_eq_thm : thm * thm -> bool
1.68 - val eq_thm_sg : thm * thm -> bool
1.69 - val size_of_thm : thm -> int
1.70 - val reflexive_thm : thm
1.71 - val symmetric_thm : thm
1.72 - val transitive_thm : thm
1.73 + val read_instantiate : (string*string)list -> thm -> thm
1.74 + val cterm_instantiate : (cterm*cterm)list -> thm -> thm
1.75 + val weak_eq_thm : thm * thm -> bool
1.76 + val eq_thm_sg : thm * thm -> bool
1.77 + val size_of_thm : thm -> int
1.78 + val reflexive_thm : thm
1.79 + val symmetric_thm : thm
1.80 + val transitive_thm : thm
1.81 val refl_implies : thm
1.82 val symmetric_fun : thm -> thm
1.83 - val rewrite_rule_aux : (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm
1.84 - val rewrite_thm : bool * bool * bool
1.85 + val rewrite_rule_aux : (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm
1.86 + val rewrite_thm : bool * bool * bool
1.87 -> (meta_simpset -> thm -> thm option)
1.88 -> meta_simpset -> thm -> thm
1.89 - val rewrite_cterm : bool * bool * bool
1.90 + val rewrite_cterm : bool * bool * bool
1.91 -> (meta_simpset -> thm -> thm option)
1.92 -> meta_simpset -> cterm -> thm
1.93 val rewrite_goals_rule_aux: (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm
1.94 - val rewrite_goal_rule : bool* bool * bool
1.95 + val rewrite_goal_rule : bool* bool * bool
1.96 -> (meta_simpset -> thm -> thm option)
1.97 -> meta_simpset -> int -> thm -> thm
1.98 - val equal_abs_elim : cterm -> thm -> thm
1.99 + val equal_abs_elim : cterm -> thm -> thm
1.100 val equal_abs_elim_list: cterm list -> thm -> thm
1.101 val flexpair_abs_elim_list: cterm list -> thm -> thm
1.102 - val asm_rl : thm
1.103 - val cut_rl : thm
1.104 - val revcut_rl : thm
1.105 - val thin_rl : thm
1.106 + val asm_rl : thm
1.107 + val cut_rl : thm
1.108 + val revcut_rl : thm
1.109 + val thin_rl : thm
1.110 val triv_forall_equality: thm
1.111 val swap_prems_rl : thm
1.112 val equal_intr_rule : thm
1.113 - val instantiate' : ctyp option list -> cterm option list -> thm -> thm
1.114 - val incr_indexes : int -> thm -> thm
1.115 - val incr_indexes_wrt : int list -> ctyp list -> cterm list -> thm list -> thm -> thm
1.116 + val instantiate' : ctyp option list -> cterm option list -> thm -> thm
1.117 + val incr_indexes : int -> thm -> thm
1.118 + val incr_indexes_wrt : int list -> ctyp list -> cterm list -> thm list -> thm -> thm
1.119 end;
1.120
1.121 signature DRULE =
1.122 sig
1.123 include BASIC_DRULE
1.124 - val compose_single : thm * int * thm -> thm
1.125 - val triv_goal : thm
1.126 - val rev_triv_goal : thm
1.127 + val compose_single : thm * int * thm -> thm
1.128 + val triv_goal : thm
1.129 + val rev_triv_goal : thm
1.130 + val freeze_all : thm -> thm
1.131 val mk_triv_goal : cterm -> thm
1.132 - val mk_cgoal : cterm -> cterm
1.133 - val assume_goal : cterm -> thm
1.134 - val tvars_of_terms : term list -> (indexname * sort) list
1.135 - val vars_of_terms : term list -> (indexname * typ) list
1.136 - val tvars_of : thm -> (indexname * sort) list
1.137 - val vars_of : thm -> (indexname * typ) list
1.138 - val unvarifyT : thm -> thm
1.139 - val unvarify : thm -> thm
1.140 - val rule_attribute : ('a -> thm -> thm) -> 'a attribute
1.141 - val tag : tag -> 'a attribute
1.142 - val untag : tag -> 'a attribute
1.143 - val tag_lemma : 'a attribute
1.144 - val tag_assumption : 'a attribute
1.145 - val tag_internal : 'a attribute
1.146 + val mk_cgoal : cterm -> cterm
1.147 + val assume_goal : cterm -> thm
1.148 + val tvars_of_terms : term list -> (indexname * sort) list
1.149 + val vars_of_terms : term list -> (indexname * typ) list
1.150 + val tvars_of : thm -> (indexname * sort) list
1.151 + val vars_of : thm -> (indexname * typ) list
1.152 + val unvarifyT : thm -> thm
1.153 + val unvarify : thm -> thm
1.154 + val rule_attribute : ('a -> thm -> thm) -> 'a attribute
1.155 + val tag : tag -> 'a attribute
1.156 + val untag : tag -> 'a attribute
1.157 + val tag_lemma : 'a attribute
1.158 + val tag_assumption : 'a attribute
1.159 + val tag_internal : 'a attribute
1.160 end;
1.161
1.162 structure Drule: DRULE =
1.163 @@ -114,18 +115,18 @@
1.164
1.165 (*dest_implies for cterms. Note T=prop below*)
1.166 fun dest_implies ct =
1.167 - case term_of ct of
1.168 - (Const("==>", _) $ _ $ _) =>
1.169 - let val (ct1,ct2) = dest_comb ct
1.170 - in (#2 (dest_comb ct1), ct2) end
1.171 + case term_of ct of
1.172 + (Const("==>", _) $ _ $ _) =>
1.173 + let val (ct1,ct2) = dest_comb ct
1.174 + in (#2 (dest_comb ct1), ct2) end
1.175 | _ => raise TERM ("dest_implies", [term_of ct]) ;
1.176
1.177
1.178 (*Discard flexflex pairs; return a cterm*)
1.179 fun skip_flexpairs ct =
1.180 case term_of ct of
1.181 - (Const("==>", _) $ (Const("=?=",_)$_$_) $ _) =>
1.182 - skip_flexpairs (#2 (dest_implies ct))
1.183 + (Const("==>", _) $ (Const("=?=",_)$_$_) $ _) =>
1.184 + skip_flexpairs (#2 (dest_implies ct))
1.185 | _ => ct;
1.186
1.187 (* A1==>...An==>B goes to [A1,...,An], where B is not an implication *)
1.188 @@ -136,8 +137,8 @@
1.189
1.190 (* A1==>...An==>B goes to B, where B is not an implication *)
1.191 fun strip_imp_concl ct =
1.192 - case term_of ct of (Const("==>", _) $ _ $ _) =>
1.193 - strip_imp_concl (#2 (dest_comb ct))
1.194 + case term_of ct of (Const("==>", _) $ _ $ _) =>
1.195 + strip_imp_concl (#2 (dest_comb ct))
1.196 | _ => ct;
1.197
1.198 (*The premises of a theorem, as a cterm list*)
1.199 @@ -249,7 +250,7 @@
1.200 val inrs = add_term_tvars(prop,[]);
1.201 val nms' = rev(foldl add_new_id ([], map (#1 o #1) inrs));
1.202 val tye = ListPair.map (fn ((v,rs),a) => (v, TVar((a,0),rs)))
1.203 - (inrs, nms')
1.204 + (inrs, nms')
1.205 val ctye = map (fn (v,T) => (v,ctyp_of sign T)) tye;
1.206 fun varpairs([],[]) = []
1.207 | varpairs((var as Var(v,T)) :: vars, b::bs) =
1.208 @@ -273,7 +274,7 @@
1.209 end;
1.210
1.211
1.212 -(*Convert all Vars in a theorem to Frees. Also return a function for
1.213 +(*Convert all Vars in a theorem to Frees. Also return a function for
1.214 reversing that operation. DOES NOT WORK FOR TYPE VARIABLES.
1.215 Similar code in type/freeze_thaw*)
1.216 fun freeze_thaw th =
1.217 @@ -283,19 +284,19 @@
1.218 case term_vars prop of
1.219 [] => (fth, fn x => x)
1.220 | vars =>
1.221 - let fun newName (Var(ix,_), (pairs,used)) =
1.222 - let val v = variant used (string_of_indexname ix)
1.223 - in ((ix,v)::pairs, v::used) end;
1.224 - val (alist, _) = foldr newName
1.225 - (vars, ([], add_term_names (prop, [])))
1.226 - fun mk_inst (Var(v,T)) =
1.227 - (cterm_of sign (Var(v,T)),
1.228 - cterm_of sign (Free(the (assoc(alist,v)), T)))
1.229 - val insts = map mk_inst vars
1.230 - fun thaw th' =
1.231 - th' |> forall_intr_list (map #2 insts)
1.232 - |> forall_elim_list (map #1 insts)
1.233 - in (Thm.instantiate ([],insts) fth, thaw) end
1.234 + let fun newName (Var(ix,_), (pairs,used)) =
1.235 + let val v = variant used (string_of_indexname ix)
1.236 + in ((ix,v)::pairs, v::used) end;
1.237 + val (alist, _) = foldr newName
1.238 + (vars, ([], add_term_names (prop, [])))
1.239 + fun mk_inst (Var(v,T)) =
1.240 + (cterm_of sign (Var(v,T)),
1.241 + cterm_of sign (Free(the (assoc(alist,v)), T)))
1.242 + val insts = map mk_inst vars
1.243 + fun thaw th' =
1.244 + th' |> forall_intr_list (map #2 insts)
1.245 + |> forall_elim_list (map #1 insts)
1.246 + in (Thm.instantiate ([],insts) fth, thaw) end
1.247 end;
1.248
1.249
1.250 @@ -405,7 +406,7 @@
1.251
1.252 val symmetric_thm =
1.253 let val xy = read_prop "x::'a::logic == y"
1.254 - in store_thm "symmetric"
1.255 + in store_thm "symmetric"
1.256 (Thm.implies_intr_hyps(Thm.symmetric(Thm.assume xy)))
1.257 end;
1.258
1.259 @@ -518,7 +519,7 @@
1.260
1.261 (* [| PROP ?phi ==> PROP ?psi; PROP ?psi ==> PROP ?phi |]
1.262 ==> PROP ?phi == PROP ?psi
1.263 - Introduction rule for == as a meta-theorem.
1.264 + Introduction rule for == as a meta-theorem.
1.265 *)
1.266 val equal_intr_rule =
1.267 let val PQ = read_prop "PROP phi ==> PROP psi"
1.268 @@ -708,6 +709,27 @@
1.269 in incr_indexes (maxidx + 1) end;
1.270
1.271
1.272 +(* freeze_all *)
1.273 +
1.274 +(*freeze all (T)Vars; assumes thm in standard form*)
1.275 +
1.276 +fun freeze_all_TVars thm =
1.277 + (case tvars_of thm of
1.278 + [] => thm
1.279 + | tvars =>
1.280 + let val cert = Thm.ctyp_of (Thm.sign_of_thm thm)
1.281 + in instantiate' (map (fn ((x, _), S) => Some (cert (TFree (x, S)))) tvars) [] thm end);
1.282 +
1.283 +fun freeze_all_Vars thm =
1.284 + (case vars_of thm of
1.285 + [] => thm
1.286 + | vars =>
1.287 + let val cert = Thm.cterm_of (Thm.sign_of_thm thm)
1.288 + in instantiate' [] (map (fn ((x, _), T) => Some (cert (Free (x, T)))) vars) thm end);
1.289 +
1.290 +val freeze_all = freeze_all_Vars o freeze_all_TVars;
1.291 +
1.292 +
1.293 (* mk_triv_goal *)
1.294
1.295 (*make an initial proof state, "PROP A ==> (PROP A)" *)