equal
deleted
inserted
replaced
106 val premts = Thm.prems_of th; |
106 val premts = Thm.prems_of th; |
107 |
107 |
108 fun allify_prem_var (vt as (n,ty),t) = |
108 fun allify_prem_var (vt as (n,ty),t) = |
109 (Term.all ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t))) |
109 (Term.all ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t))) |
110 |
110 |
111 fun allify_prem Ts p = Library.foldr allify_prem_var (Ts, p) |
111 fun allify_prem Ts p = foldr allify_prem_var p Ts |
112 |
112 |
113 val cTs = map (ctermify o Free) Ts |
113 val cTs = map (ctermify o Free) Ts |
114 val cterm_asms = map (ctermify o allify_prem Ts) premts |
114 val cterm_asms = map (ctermify o allify_prem Ts) premts |
115 val allifyied_asm_thms = map (Drule.forall_elim_list cTs o Thm.assume) cterm_asms |
115 val allifyied_asm_thms = map (Drule.forall_elim_list cTs o Thm.assume) cterm_asms |
116 in |
116 in |
165 let val vt = #t (Thm.rep_cterm v) |
165 let val vt = #t (Thm.rep_cterm v) |
166 val (n,ty) = Term.dest_Free vt |
166 val (n,ty) = Term.dest_Free vt |
167 in (Term.all ty) $ (Abs(n,ty,Term.abstract_over (vt, t))) end; |
167 in (Term.all ty) $ (Abs(n,ty,Term.abstract_over (vt, t))) end; |
168 |
168 |
169 fun allify_for_sg_term ctermify vs t = |
169 fun allify_for_sg_term ctermify vs t = |
170 let val t_alls = Library.foldr allify_term (vs,t); |
170 let val t_alls = foldr allify_term t vs; |
171 val ct_alls = ctermify t_alls; |
171 val ct_alls = ctermify t_alls; |
172 in |
172 in |
173 (ct_alls, Drule.forall_elim_list vs (Thm.assume ct_alls)) |
173 (ct_alls, Drule.forall_elim_list vs (Thm.assume ct_alls)) |
174 end; |
174 end; |
175 (* lookup type of a free var name from a list *) |
175 (* lookup type of a free var name from a list *) |
254 val solth' = |
254 val solth' = |
255 solth |> Drule.implies_intr_list hcprems |
255 solth |> Drule.implies_intr_list hcprems |
256 |> Drule.forall_intr_list cfvs |
256 |> Drule.forall_intr_list cfvs |
257 in Drule.compose_single (solth', i, gth) end; |
257 in Drule.compose_single (solth', i, gth) end; |
258 |
258 |
259 val export_solutions = Library.foldr (uncurry export_solution); |
259 fun export_solutions (xs,th) = foldr (uncurry export_solution) th xs; |
260 |
260 |
261 |
261 |
262 (* fix parameters of a subgoal "i", as free variables, and create an |
262 (* fix parameters of a subgoal "i", as free variables, and create an |
263 exporting function that will use the result of this proved goal to |
263 exporting function that will use the result of this proved goal to |
264 show the goal in the original theorem. |
264 show the goal in the original theorem. |