equal
deleted
inserted
replaced
271 val (xs, names_lthy2) = mk_Frees "x" (binder_types (fastype_of size)) lthy2; |
271 val (xs, names_lthy2) = mk_Frees "x" (binder_types (fastype_of size)) lthy2; |
272 val goal = |
272 val goal = |
273 HOLogic.mk_Trueprop (BNF_LFP_Util.mk_not_eq (list_comb (size, xs)) HOLogic.zero); |
273 HOLogic.mk_Trueprop (BNF_LFP_Util.mk_not_eq (list_comb (size, xs)) HOLogic.zero); |
274 val thm = |
274 val thm = |
275 Goal.prove_sorry lthy2 [] [] goal (fn {context = ctxt, ...} => |
275 Goal.prove_sorry lthy2 [] [] goal (fn {context = ctxt, ...} => |
276 mk_size_neq ctxt (map (Proof_Context.cterm_of lthy2) xs) |
276 mk_size_neq ctxt (map (Thm.cterm_of lthy2) xs) |
277 (#exhaust (#ctr_sugar (#fp_ctr_sugar fp_sugar))) size_thms) |
277 (#exhaust (#ctr_sugar (#fp_ctr_sugar fp_sugar))) size_thms) |
278 |> single |
278 |> single |
279 |> Proof_Context.export names_lthy2 lthy2 |
279 |> Proof_Context.export names_lthy2 lthy2 |
280 |> map Thm.close_derivation; |
280 |> map Thm.close_derivation; |
281 in thm end) fp_sugars overloaded_size_consts overloaded_size_simpss |
281 in thm end) fp_sugars overloaded_size_consts overloaded_size_simpss |