65 val warn_extra_tfrees: context -> context -> context |
65 val warn_extra_tfrees: context -> context -> context |
66 val generalize: context -> context -> term list -> term list |
66 val generalize: context -> context -> term list -> term list |
67 val find_free: term -> string -> term option |
67 val find_free: term -> string -> term option |
68 val export: bool -> context -> context -> thm -> thm Seq.seq |
68 val export: bool -> context -> context -> thm -> thm Seq.seq |
69 val export_standard: cterm list -> context -> context -> thm -> thm |
69 val export_standard: cterm list -> context -> context -> thm -> thm |
|
70 val export_plain: cterm list -> context -> context -> thm -> thm |
70 val drop_schematic: indexname * term option -> indexname * term option |
71 val drop_schematic: indexname * term option -> indexname * term option |
71 val add_binds: (indexname * string option) list -> context -> context |
72 val add_binds: (indexname * string option) list -> context -> context |
72 val add_binds_i: (indexname * term option) list -> context -> context |
73 val add_binds_i: (indexname * term option) list -> context -> context |
73 val auto_bind_goal: term list -> context -> context |
74 val auto_bind_goal: term list -> context -> context |
74 val auto_bind_facts: term list -> context -> context |
75 val auto_bind_facts: term list -> context -> context |
101 val put_thm: string * thm -> context -> context |
102 val put_thm: string * thm -> context -> context |
102 val put_thms: string * thm list -> context -> context |
103 val put_thms: string * thm list -> context -> context |
103 val put_thmss: (string * thm list) list -> context -> context |
104 val put_thmss: (string * thm list) list -> context -> context |
104 val reset_thms: string -> context -> context |
105 val reset_thms: string -> context -> context |
105 val note_thmss: |
106 val note_thmss: |
106 ((bstring * context attribute list) * (thmref * context attribute list) list) list -> |
107 ((bstring * context attribute list) * |
107 context -> context * (bstring * thm list) list |
108 (thmref * context attribute list) list) list -> |
|
109 context -> context * (bstring * thm list) list |
108 val note_thmss_i: |
110 val note_thmss_i: |
109 ((bstring * context attribute list) * (thm list * context attribute list) list) list -> |
111 ((bstring * context attribute list) * |
110 context -> context * (bstring * thm list) list |
112 (thm list * context attribute list) list) list -> |
|
113 context -> context * (bstring * thm list) list |
|
114 val note_thmss_accesses: |
|
115 (string -> string list) -> |
|
116 ((bstring * context attribute list) * |
|
117 (thmref * context attribute list) list) list -> |
|
118 context -> context * (bstring * thm list) list |
|
119 val note_thmss_accesses_i: |
|
120 (string -> string list) -> |
|
121 ((bstring * context attribute list) * |
|
122 (thm list * context attribute list) list) list -> |
|
123 context -> context * (bstring * thm list) list |
111 val export_assume: exporter |
124 val export_assume: exporter |
112 val export_presume: exporter |
125 val export_presume: exporter |
113 val cert_def: context -> term -> string * term |
126 val cert_def: context -> term -> string * term |
114 val export_def: exporter |
127 val export_def: exporter |
115 val assume: exporter |
128 val assume: exporter |
810 |> Tactic.norm_hhf_rule |
823 |> Tactic.norm_hhf_rule |
811 |> (#1 o Drule.tvars_intr_list tfrees) |
824 |> (#1 o Drule.tvars_intr_list tfrees) |
812 end) |
825 end) |
813 end; |
826 end; |
814 |
827 |
|
828 (* without varification *) |
|
829 |
|
830 fun export_view' view is_goal inner outer = |
|
831 let |
|
832 val asms = Library.drop (length (assumptions_of outer), assumptions_of inner); |
|
833 val exp_asms = map (fn (cprops, exp) => exp is_goal cprops) asms; |
|
834 in fn thm =>thm |
|
835 |> Tactic.norm_hhf_plain |
|
836 |> Seq.EVERY (rev exp_asms) |
|
837 |> Seq.map (Drule.implies_intr_list view) |
|
838 |> Seq.map Tactic.norm_hhf_plain |
|
839 end; |
|
840 |
815 val export = export_view []; |
841 val export = export_view []; |
816 |
842 |
817 fun export_standard view inner outer = |
843 fun gen_export_std exp_view view inner outer = |
818 let val exp = export_view view false inner outer in |
844 let val exp = exp_view view false inner outer in |
819 fn th => |
845 fn th => |
820 (case Seq.pull (exp th) of |
846 (case Seq.pull (exp th) of |
821 SOME (th', _) => th' |> Drule.local_standard |
847 SOME (th', _) => th' |> Drule.local_standard |
822 | NONE => raise CONTEXT ("Internal failure while exporting theorem", inner)) |
848 | NONE => raise CONTEXT ("Internal failure while exporting theorem", inner)) |
823 end; |
849 end; |
824 |
850 |
|
851 val export_standard = gen_export_std export_view; |
|
852 val export_plain = gen_export_std export_view'; |
825 |
853 |
826 |
854 |
827 (** bindings **) |
855 (** bindings **) |
828 |
856 |
829 (* update_binds *) |
857 (* update_binds *) |
1020 cases, defs, delta, delta_count)); |
1048 cases, defs, delta, delta_count)); |
1021 |
1049 |
1022 |
1050 |
1023 (* put_thm(s) *) |
1051 (* put_thm(s) *) |
1024 |
1052 |
1025 fun put_thms ("", _) ctxt = ctxt |
1053 fun gen_put_thms _ _ ("", _) ctxt = ctxt |
1026 | put_thms (name, ths) ctxt = ctxt |> map_context |
1054 | gen_put_thms override_q acc (name, ths) ctxt = ctxt |> map_context |
1027 (fn (thy, syntax, data, asms, binds, (q, space, tab, index), cases, defs, delta, delta_count) => |
1055 (fn (thy, syntax, data, asms, binds, (q, space, tab, index), cases, defs, delta, delta_count) => |
1028 if not q andalso NameSpace.is_qualified name then |
1056 if not override_q andalso not q andalso NameSpace.is_qualified name then |
1029 raise CONTEXT ("Attempt to declare qualified name " ^ quote name, ctxt) |
1057 raise CONTEXT ("Attempt to declare qualified name " ^ quote name, ctxt) |
1030 else (thy, syntax, data, asms, binds, (q, NameSpace.extend (space, [name]), |
1058 else (thy, syntax, data, asms, binds, (q, NameSpace.extend' acc (space, [name]), |
1031 Symtab.update ((name, SOME ths), tab), |
1059 Symtab.update ((name, SOME ths), tab), |
1032 FactIndex.add (is_known ctxt) (index, (name, ths))), cases, defs, delta, delta_count)); |
1060 FactIndex.add (is_known ctxt) (index, (name, ths))), cases, defs, delta, delta_count)); |
1033 |
1061 |
1034 fun put_thm (name, th) = put_thms (name, [th]); |
1062 fun gen_put_thm q acc (name, th) = gen_put_thms q acc (name, [th]); |
1035 |
1063 |
1036 fun put_thmss [] ctxt = ctxt |
1064 fun gen_put_thmss q acc [] ctxt = ctxt |
1037 | put_thmss (th :: ths) ctxt = ctxt |> put_thms th |> put_thmss ths; |
1065 | gen_put_thmss q acc (th :: ths) ctxt = |
1038 |
1066 ctxt |> gen_put_thms q acc th |> gen_put_thmss q acc ths; |
|
1067 |
|
1068 val put_thm = gen_put_thm false NameSpace.accesses; |
|
1069 val put_thms = gen_put_thms false NameSpace.accesses; |
|
1070 val put_thmss = gen_put_thmss false NameSpace.accesses; |
1039 |
1071 |
1040 (* reset_thms *) |
1072 (* reset_thms *) |
1041 |
1073 |
1042 fun reset_thms name = |
1074 fun reset_thms name = |
1043 map_context (fn (thy, syntax, data, asms, binds, (q, space, tab, index), cases, defs, delta, delta_count) => |
1075 map_context (fn (thy, syntax, data, asms, binds, (q, space, tab, index), cases, defs, delta, delta_count) => |
1047 |
1079 |
1048 (* note_thmss *) |
1080 (* note_thmss *) |
1049 |
1081 |
1050 local |
1082 local |
1051 |
1083 |
1052 fun gen_note_thss get (ctxt, ((name, more_attrs), ths_attrs)) = |
1084 fun gen_note_thss get acc (ctxt, ((name, more_attrs), ths_attrs)) = |
1053 let |
1085 let |
1054 fun app ((ct, ths), (th, attrs)) = |
1086 fun app ((ct, ths), (th, attrs)) = |
1055 let val (ct', th') = Thm.applys_attributes ((ct, get ctxt th), attrs @ more_attrs) |
1087 let val (ct', th') = Thm.applys_attributes ((ct, get ctxt th), attrs @ more_attrs) |
1056 in (ct', th' :: ths) end; |
1088 in (ct', th' :: ths) end; |
1057 val (ctxt', rev_thms) = Library.foldl app ((ctxt, []), ths_attrs); |
1089 val (ctxt', rev_thms) = Library.foldl app ((ctxt, []), ths_attrs); |
1058 val thms = List.concat (rev rev_thms); |
1090 val thms = List.concat (rev rev_thms); |
1059 in (ctxt' |> put_thms (name, thms), (name, thms)) end; |
1091 in (ctxt' |> gen_put_thms true acc (name, thms), (name, thms)) end; |
1060 |
1092 |
1061 fun gen_note_thmss get args ctxt = foldl_map (gen_note_thss get) (ctxt, args); |
1093 fun gen_note_thmss get acc args ctxt = |
|
1094 foldl_map (gen_note_thss get acc) (ctxt, args); |
1062 |
1095 |
1063 in |
1096 in |
1064 |
1097 |
1065 val note_thmss = gen_note_thmss get_thms; |
1098 val note_thmss = gen_note_thmss get_thms NameSpace.accesses; |
1066 val note_thmss_i = gen_note_thmss (K I); |
1099 val note_thmss_i = gen_note_thmss (K I) NameSpace.accesses; |
|
1100 |
|
1101 val note_thmss_accesses = gen_note_thmss get_thms; |
|
1102 val note_thmss_accesses_i = gen_note_thmss (K I); |
1067 |
1103 |
1068 end; |
1104 end; |
1069 |
1105 |
1070 |
1106 |
1071 |
1107 |