314 mk_case_cong_tac ctxt exhaust_thm' case_thms), |
314 mk_case_cong_tac ctxt exhaust_thm' case_thms), |
315 Skip_Proof.prove lthy [] [] goal_weak (K (etac arg_cong 1))) |
315 Skip_Proof.prove lthy [] [] goal_weak (K (etac arg_cong 1))) |
316 |> pairself (singleton (Proof_Context.export names_lthy lthy)) |
316 |> pairself (singleton (Proof_Context.export names_lthy lthy)) |
317 end; |
317 end; |
318 |
318 |
319 val split_thm = |
319 val (split_thm, split_asm_thm) = |
320 let |
320 let |
321 fun mk_clause xctr xs f_xs = |
321 fun mk_conjunct xctr xs f_xs = |
322 list_all_free xs (HOLogic.mk_imp (HOLogic.mk_eq (v, xctr), q $ f_xs)); |
322 list_all_free xs (HOLogic.mk_imp (HOLogic.mk_eq (v, xctr), q $ f_xs)); |
|
323 fun mk_disjunct xctr xs f_xs = |
|
324 list_exists_free xs (HOLogic.mk_conj (HOLogic.mk_eq (v, xctr), |
|
325 HOLogic.mk_not (q $ f_xs))); |
|
326 |
|
327 val lhs = q $ (mk_caseofB_term eta_fs $ v); |
|
328 |
323 val goal = |
329 val goal = |
324 mk_Trueprop_eq (q $ (mk_caseofB_term eta_fs $ v), |
330 mk_Trueprop_eq (lhs, Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct xctrs xss xfs)); |
325 Library.foldr1 HOLogic.mk_conj (map3 mk_clause xctrs xss xfs)); |
331 val goal_asm = |
326 in |
332 mk_Trueprop_eq (lhs, HOLogic.mk_not (Library.foldr1 HOLogic.mk_disj |
327 Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => |
333 (map3 mk_disjunct xctrs xss xfs))); |
328 mk_split_tac ctxt exhaust_thm' case_thms inject_thms distinct_thms) |
334 |
329 |> singleton (Proof_Context.export names_lthy lthy) |
335 val split_thm = |
330 end; |
336 Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => |
331 |
337 mk_split_tac ctxt exhaust_thm' case_thms inject_thms distinct_thms) |
332 val split_asm_thm = TrueI; |
338 |> singleton (Proof_Context.export names_lthy lthy) |
|
339 val split_asm_thm = |
|
340 Skip_Proof.prove lthy [] [] goal_asm (fn {context = ctxt, ...} => |
|
341 mk_split_asm_tac ctxt split_thm) |
|
342 |> singleton (Proof_Context.export names_lthy lthy) |
|
343 in |
|
344 (split_thm, split_asm_thm) |
|
345 end; |
333 |
346 |
334 (* TODO: case syntax *) |
347 (* TODO: case syntax *) |
335 (* TODO: attributes (simp, case_names, etc.) *) |
348 (* TODO: attributes (simp, case_names, etc.) *) |
336 |
349 |
337 fun note thmN thms = |
350 fun note thmN thms = |