114 fun future_result ctxt result prop = |
114 fun future_result ctxt result prop = |
115 let |
115 let |
116 val assms = Assumption.all_assms_of ctxt; |
116 val assms = Assumption.all_assms_of ctxt; |
117 val As = map Thm.term_of assms; |
117 val As = map Thm.term_of assms; |
118 |
118 |
119 val xs = map Free (fold Term.add_frees (prop :: As) []); |
119 val frees = Term_Subst.Frees.build (fold Term_Subst.add_frees (prop :: As)); |
120 val fixes = map (Thm.cterm_of ctxt) xs; |
120 val xs = Term_Subst.Frees.fold_rev (cons o Thm.cterm_of ctxt o Free o #1) frees []; |
121 |
121 |
122 val tfrees = fold Term.add_tfrees (prop :: As) []; |
122 val tfrees = Term_Subst.TFrees.build (fold Term_Subst.add_tfrees (prop :: As)); |
123 val tfrees_set = Symtab.build (fold (Symtab.insert_set o #1) tfrees); |
123 val Ts = Symtab.build (Term_Subst.TFrees.fold (Symtab.insert_set o #1 o #1) tfrees); |
124 val instT = map (fn (a, S) => (((a, 0), S), Thm.ctyp_of ctxt (TFree (a, S)))) tfrees; |
124 val instT = |
|
125 build (tfrees |> Term_Subst.TFrees.fold (fn ((a, S), ()) => |
|
126 cons (((a, 0), S), Thm.ctyp_of ctxt (TFree (a, S))))); |
125 |
127 |
126 val global_prop = |
128 val global_prop = |
127 Logic.varify_types_global (fold_rev Logic.all xs (Logic.list_implies (As, prop))) |
129 Logic.list_implies (As, prop) |
|
130 |> Term_Subst.Frees.fold_rev (Logic.all o Free o #1) frees |
|
131 |> Logic.varify_types_global |
128 |> Thm.cterm_of ctxt |
132 |> Thm.cterm_of ctxt |
129 |> Thm.weaken_sorts' ctxt; |
133 |> Thm.weaken_sorts' ctxt; |
130 val global_result = result |> Future.map |
134 val global_result = result |> Future.map |
131 (Drule.flexflex_unique (SOME ctxt) #> |
135 (Drule.flexflex_unique (SOME ctxt) #> |
132 Drule.implies_intr_list assms #> |
136 Drule.implies_intr_list assms #> |
133 Drule.forall_intr_list fixes #> |
137 Drule.forall_intr_list xs #> |
134 Thm.adjust_maxidx_thm ~1 #> |
138 Thm.adjust_maxidx_thm ~1 #> |
135 Thm.generalize (tfrees_set, Symtab.empty) 0 #> |
139 Thm.generalize (Ts, Symtab.empty) 0 #> |
136 Thm.strip_shyps #> |
140 Thm.strip_shyps #> |
137 Thm.solve_constraints); |
141 Thm.solve_constraints); |
138 val local_result = |
142 val local_result = |
139 Thm.future global_result global_prop |
143 Thm.future global_result global_prop |
140 |> Thm.close_derivation \<^here> |
144 |> Thm.close_derivation \<^here> |
141 |> Thm.instantiate (instT, []) |
145 |> Thm.instantiate (instT, []) |
142 |> Drule.forall_elim_list fixes |
146 |> Drule.forall_elim_list xs |
143 |> fold (Thm.elim_implies o Thm.assume) assms |
147 |> fold (Thm.elim_implies o Thm.assume) assms |
144 |> Thm.solve_constraints; |
148 |> Thm.solve_constraints; |
145 in local_result end; |
149 in local_result end; |
146 |
150 |
147 |
151 |