227 fun zero_var_indexes_list [] = [] |
227 fun zero_var_indexes_list [] = [] |
228 | zero_var_indexes_list ths = |
228 | zero_var_indexes_list ths = |
229 let |
229 let |
230 val thy = Theory.merge_list (map Thm.theory_of_thm ths); |
230 val thy = Theory.merge_list (map Thm.theory_of_thm ths); |
231 val (instT, inst) = Term_Subst.zero_var_indexes_inst (map Thm.full_prop_of ths); |
231 val (instT, inst) = Term_Subst.zero_var_indexes_inst (map Thm.full_prop_of ths); |
232 val cinstT = map (fn (v, T) => (Thm.global_ctyp_of thy (TVar v), Thm.global_ctyp_of thy T)) instT; |
232 val cinstT = |
233 val cinst = map (fn (v, t) => (Thm.global_cterm_of thy (Var v), Thm.global_cterm_of thy t)) inst; |
233 map (fn (v, T) => (Thm.global_ctyp_of thy (TVar v), Thm.global_ctyp_of thy T)) instT; |
|
234 val cinst = |
|
235 map (fn (v, t) => (Thm.global_cterm_of thy (Var v), Thm.global_cterm_of thy t)) inst; |
234 in map (Thm.adjust_maxidx_thm ~1 o Thm.instantiate (cinstT, cinst)) ths end; |
236 in map (Thm.adjust_maxidx_thm ~1 o Thm.instantiate (cinstT, cinst)) ths end; |
235 |
237 |
236 val zero_var_indexes = singleton zero_var_indexes_list; |
238 val zero_var_indexes = singleton zero_var_indexes_list; |
237 |
239 |
238 |
240 |
244 fold Thm.implies_intr (#hyps (Thm.crep_thm th)) th; |
246 fold Thm.implies_intr (#hyps (Thm.crep_thm th)) th; |
245 |
247 |
246 (*Squash a theorem's flexflex constraints provided it can be done uniquely. |
248 (*Squash a theorem's flexflex constraints provided it can be done uniquely. |
247 This step can lose information.*) |
249 This step can lose information.*) |
248 fun flexflex_unique opt_ctxt th = |
250 fun flexflex_unique opt_ctxt th = |
249 if null (Thm.tpairs_of th) then th else |
251 if null (Thm.tpairs_of th) then th |
250 case distinct Thm.eq_thm (Seq.list_of (Thm.flexflex_rule opt_ctxt th)) of |
252 else |
|
253 (case distinct Thm.eq_thm (Seq.list_of (Thm.flexflex_rule opt_ctxt th)) of |
251 [th] => th |
254 [th] => th |
252 | [] => raise THM("flexflex_unique: impossible constraints", 0, [th]) |
255 | [] => raise THM ("flexflex_unique: impossible constraints", 0, [th]) |
253 | _ => raise THM("flexflex_unique: multiple unifiers", 0, [th]); |
256 | _ => raise THM ("flexflex_unique: multiple unifiers", 0, [th])); |
254 |
257 |
255 |
258 |
256 (* old-style export without context *) |
259 (* old-style export without context *) |
257 |
260 |
258 val export_without_context_open = |
261 val export_without_context_open = |
314 (*Resolution: P==>Q, Q==>R gives P==>R*) |
317 (*Resolution: P==>Q, Q==>R gives P==>R*) |
315 fun tha RS thb = tha RSN (1,thb); |
318 fun tha RS thb = tha RSN (1,thb); |
316 |
319 |
317 (*For joining lists of rules*) |
320 (*For joining lists of rules*) |
318 fun thas RLN (i, thbs) = |
321 fun thas RLN (i, thbs) = |
319 let val resolve = Thm.biresolution NONE false (map (pair false) thas) i |
322 let |
320 fun resb thb = Seq.list_of (resolve thb) handle THM _ => [] |
323 val resolve = Thm.biresolution NONE false (map (pair false) thas) i |
|
324 fun resb thb = Seq.list_of (resolve thb) handle THM _ => [] |
321 in maps resb thbs end; |
325 in maps resb thbs end; |
322 |
326 |
323 fun thas RL thbs = thas RLN (1, thbs); |
327 fun thas RL thbs = thas RLN (1, thbs); |
324 |
328 |
325 (*Isar-style multi-resolution*) |
329 (*Isar-style multi-resolution*) |
714 |
718 |
715 local |
719 local |
716 |
720 |
717 (*compose Q and [Q1,Q2,...,Qk]==>R to [Q2,...,Qk]==>R getting unique result*) |
721 (*compose Q and [Q1,Q2,...,Qk]==>R to [Q2,...,Qk]==>R getting unique result*) |
718 fun comp incremented th1 th2 = |
722 fun comp incremented th1 th2 = |
719 Thm.bicompose NONE {flatten = true, match = false, incremented = incremented} (false, th1, 0) 1 th2 |
723 Thm.bicompose NONE {flatten = true, match = false, incremented = incremented} |
|
724 (false, th1, 0) 1 th2 |
720 |> Seq.list_of |> distinct Thm.eq_thm |
725 |> Seq.list_of |> distinct Thm.eq_thm |
721 |> (fn [th] => th | _ => raise THM ("COMP", 1, [th1, th2])); |
726 |> (fn [th] => th | _ => raise THM ("COMP", 1, [th1, th2])); |
722 |
727 |
723 in |
728 in |
724 |
729 |
758 "\nof variable " ^ |
763 "\nof variable " ^ |
759 Syntax.string_of_term_global thy' (Term.map_types (Envir.norm_type tye) t) ^ |
764 Syntax.string_of_term_global thy' (Term.map_types (Envir.norm_type tye) t) ^ |
760 "\ncannot be unified with type\n" ^ |
765 "\ncannot be unified with type\n" ^ |
761 Syntax.string_of_typ_global thy' (Envir.norm_type tye U) ^ "\nof term " ^ |
766 Syntax.string_of_typ_global thy' (Envir.norm_type tye U) ^ "\nof term " ^ |
762 Syntax.string_of_term_global thy' (Term.map_types (Envir.norm_type tye) u), |
767 Syntax.string_of_term_global thy' (Term.map_types (Envir.norm_type tye) u), |
763 [T, U], [t, u]) |
768 [T, U], [t, u]); |
764 in (thy', tye', maxi') end; |
769 in (thy', tye', maxi') end; |
765 in |
770 in |
766 |
771 |
767 fun cterm_instantiate [] th = th |
772 fun cterm_instantiate [] th = th |
768 | cterm_instantiate ctpairs th = |
773 | cterm_instantiate ctpairs th = |
769 let |
774 let |
770 val (thy, tye, _) = fold_rev add_types ctpairs (Thm.theory_of_thm th, Vartab.empty, 0); |
775 val (thy, tye, _) = fold_rev add_types ctpairs (Thm.theory_of_thm th, Vartab.empty, 0); |
771 val instT = |
776 val instT = |
772 Vartab.fold (fn (xi, (S, T)) => |
777 Vartab.fold (fn (xi, (S, T)) => |
773 cons (Thm.global_ctyp_of thy (TVar (xi, S)), Thm.global_ctyp_of thy (Envir.norm_type tye T))) tye []; |
778 cons (apply2 (Thm.global_ctyp_of thy) (TVar (xi, S), Envir.norm_type tye T))) tye []; |
774 val inst = map (apply2 (Thm.instantiate_cterm (instT, []))) ctpairs; |
779 val inst = map (apply2 (Thm.instantiate_cterm (instT, []))) ctpairs; |
775 in instantiate_normalize (instT, inst) th end |
780 in instantiate_normalize (instT, inst) th end |
776 handle TERM (msg, _) => raise THM (msg, 0, [th]) |
781 handle TERM (msg, _) => raise THM (msg, 0, [th]) |
777 | TYPE (msg, _, _) => raise THM (msg, 0, [th]); |
782 | TYPE (msg, _, _) => raise THM (msg, 0, [th]); |
778 end; |
783 end; |