equal
deleted
inserted
replaced
64 val declare_term: term -> context -> context |
64 val declare_term: term -> context -> context |
65 val read_tyname: context -> string -> typ |
65 val read_tyname: context -> string -> typ |
66 val read_const: context -> string -> term |
66 val read_const: context -> string -> term |
67 val warn_extra_tfrees: context -> context -> context |
67 val warn_extra_tfrees: context -> context -> context |
68 val generalize: context -> context -> term list -> term list |
68 val generalize: context -> context -> term list -> term list |
69 val find_free: term -> string -> term option |
|
70 val export: context -> context -> thm -> thm |
69 val export: context -> context -> thm -> thm |
71 val exports: context -> context -> thm -> thm Seq.seq |
70 val exports: context -> context -> thm -> thm Seq.seq |
72 val goal_exports: context -> context -> thm -> thm Seq.seq |
71 val goal_exports: context -> context -> thm -> thm Seq.seq |
73 val drop_schematic: indexname * term option -> indexname * term option |
72 val drop_schematic: indexname * term option -> indexname * term option |
74 val add_binds: (indexname * string option) list -> context -> context |
73 val add_binds: (indexname * string option) list -> context -> context |
706 |
705 |
707 |
706 |
708 |
707 |
709 (** export theorems **) |
708 (** export theorems **) |
710 |
709 |
711 fun get_free x (t as Free (y, _)) NONE = if x = y then SOME t else NONE |
|
712 | get_free _ _ opt = opt; |
|
713 |
|
714 fun find_free t x = fold_aterms (get_free x) t NONE; |
|
715 |
|
716 fun common_exports is_goal inner outer = |
710 fun common_exports is_goal inner outer = |
717 let |
711 let |
718 val gen = generalize_tfrees inner outer; |
712 val gen = generalize_tfrees inner outer; |
719 val fixes = fixed_names_of inner \\ fixed_names_of outer; |
713 val fixes = fixed_names_of inner \\ fixed_names_of outer; |
720 val asms = Library.drop (length (assumptions_of outer), assumptions_of inner); |
714 val asms = Library.drop (length (assumptions_of outer), assumptions_of inner); |
724 #> Seq.EVERY (rev exp_asms) |
718 #> Seq.EVERY (rev exp_asms) |
725 #> Seq.map (fn rule => |
719 #> Seq.map (fn rule => |
726 let |
720 let |
727 val thy = Thm.theory_of_thm rule; |
721 val thy = Thm.theory_of_thm rule; |
728 val prop = Thm.full_prop_of rule; |
722 val prop = Thm.full_prop_of rule; |
729 val frees = map (Thm.cterm_of thy) (List.mapPartial (find_free prop) fixes); |
723 val frees = map (Thm.cterm_of thy) (List.mapPartial (Term.find_free prop) fixes); |
730 val tfrees = gen (Term.add_term_tfree_names (prop, [])); |
724 val tfrees = gen (Term.add_term_tfree_names (prop, [])); |
731 in |
725 in |
732 rule |
726 rule |
733 |> Drule.forall_intr_list frees |
727 |> Drule.forall_intr_list frees |
734 |> Goal.norm_hhf |
728 |> Goal.norm_hhf |