equal
deleted
inserted
replaced
258 |
258 |
259 val mono_goal = apply_inst lthy mono (lambda f_uc (F_uc $ f_uc $ x_uc)) |
259 val mono_goal = apply_inst lthy mono (lambda f_uc (F_uc $ f_uc $ x_uc)) |
260 |> HOLogic.mk_Trueprop |
260 |> HOLogic.mk_Trueprop |
261 |> Logic.all x_uc; |
261 |> Logic.all x_uc; |
262 |
262 |
263 val mono_thm = Goal.prove_internal lthy [] (Thm.cterm_of lthy mono_goal) |
263 val mono_thm = |
264 (K (mono_tac lthy 1)) |
264 Goal.prove_internal lthy [] (Thm.cterm_of lthy mono_goal) |
|
265 (fn {context = goal_ctxt, ...} => mono_tac goal_ctxt 1) |
265 val inst_mono_thm = Thm.forall_elim (Thm.cterm_of lthy x_uc) mono_thm |
266 val inst_mono_thm = Thm.forall_elim (Thm.cterm_of lthy x_uc) mono_thm |
266 |
267 |
267 val f_def_rhs = curry_n arity (apply_inst lthy fixp F_uc); |
268 val f_def_rhs = curry_n arity (apply_inst lthy fixp F_uc); |
268 val f_def_binding = |
269 val f_def_binding = |
269 Thm.make_def_binding (Config.get lthy Function_Lib.function_internals) f_binding |
270 Thm.make_def_binding (Config.get lthy Function_Lib.function_internals) f_binding |