equal
deleted
inserted
replaced
23 | mk_un_N _ l suf = un_N ^ suf ^ string_of_int l; |
23 | mk_un_N _ l suf = un_N ^ suf ^ string_of_int l; |
24 |
24 |
25 val case_congN = "case_cong"; |
25 val case_congN = "case_cong"; |
26 val case_eqN = "case_eq"; |
26 val case_eqN = "case_eq"; |
27 val casesN = "cases"; |
27 val casesN = "cases"; |
28 val ctr_selsN = "ctr_sels"; |
28 val collapseN = "collapse"; |
29 val disc_exclusN = "disc_exclus"; |
29 val disc_exclusN = "disc_exclus"; |
30 val disc_exhaustN = "disc_exhaust"; |
30 val disc_exhaustN = "disc_exhaust"; |
31 val discsN = "discs"; |
31 val discsN = "discs"; |
32 val distinctN = "distinct"; |
32 val distinctN = "distinct"; |
33 val exhaustN = "exhaust"; |
33 val exhaustN = "exhaust"; |
348 in |
348 in |
349 [Skip_Proof.prove lthy [] [] goal (fn _ => |
349 [Skip_Proof.prove lthy [] [] goal (fn _ => |
350 mk_disc_exhaust_tac n exhaust_thm discI_thms)] |
350 mk_disc_exhaust_tac n exhaust_thm discI_thms)] |
351 end; |
351 end; |
352 |
352 |
353 val ctr_sel_thms = |
353 val collapse_thms = |
354 let |
354 let |
355 fun mk_goal ctr disc sels = |
355 fun mk_goal ctr disc sels = |
356 let |
356 let |
357 val prem = HOLogic.mk_Trueprop (betapply (disc, v)); |
357 val prem = HOLogic.mk_Trueprop (betapply (disc, v)); |
358 val concl = |
358 val concl = |
364 end; |
364 end; |
365 val goals = map3 mk_goal ctrs discs selss; |
365 val goals = map3 mk_goal ctrs discs selss; |
366 in |
366 in |
367 map4 (fn m => fn discD => fn sel_thms => Option.map (fn goal => |
367 map4 (fn m => fn discD => fn sel_thms => Option.map (fn goal => |
368 Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => |
368 Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => |
369 mk_ctr_sel_tac ctxt m discD sel_thms))) ms discD_thms sel_thmss goals |
369 mk_collapse_tac ctxt m discD sel_thms))) ms discD_thms sel_thmss goals |
370 |> map_filter I |
370 |> map_filter I |
371 end; |
371 end; |
372 |
372 |
373 val case_eq_thm = |
373 val case_eq_thm = |
374 let |
374 let |
435 |
435 |
436 val notes = |
436 val notes = |
437 [(case_congN, [case_cong_thm]), |
437 [(case_congN, [case_cong_thm]), |
438 (case_eqN, [case_eq_thm]), |
438 (case_eqN, [case_eq_thm]), |
439 (casesN, case_thms), |
439 (casesN, case_thms), |
440 (ctr_selsN, ctr_sel_thms), |
440 (collapseN, collapse_thms), |
441 (discsN, disc_thms), |
441 (discsN, disc_thms), |
442 (disc_exclusN, disc_exclus_thms), |
442 (disc_exclusN, disc_exclus_thms), |
443 (disc_exhaustN, disc_exhaust_thms), |
443 (disc_exhaustN, disc_exhaust_thms), |
444 (distinctN, distinct_thms), |
444 (distinctN, distinct_thms), |
445 (exhaustN, [exhaust_thm]), |
445 (exhaustN, [exhaust_thm]), |