98 |
98 |
99 val EqN = "Eq_"; |
99 val EqN = "Eq_"; |
100 |
100 |
101 val case_transferN = "case_transfer"; |
101 val case_transferN = "case_transfer"; |
102 val ctr_transferN = "ctr_transfer"; |
102 val ctr_transferN = "ctr_transfer"; |
|
103 val disc_transferN = "disc_transfer"; |
103 val corec_codeN = "corec_code"; |
104 val corec_codeN = "corec_code"; |
104 val map_disc_iffN = "map_disc_iff"; |
105 val map_disc_iffN = "map_disc_iff"; |
105 val map_selN = "map_sel"; |
106 val map_selN = "map_sel"; |
106 val set_casesN = "set_cases"; |
107 val set_casesN = "set_cases"; |
107 val set_introsN = "set_intros"; |
108 val set_introsN = "set_intros"; |
1368 free_constructors tacss ((((discs_sels, no_code), standard_binding), ctr_specs), |
1369 free_constructors tacss ((((discs_sels, no_code), standard_binding), ctr_specs), |
1369 sel_default_eqs) lthy |
1370 sel_default_eqs) lthy |
1370 end; |
1371 end; |
1371 |
1372 |
1372 fun derive_maps_sets_rels (ctr_sugar as {casex, case_cong, case_thms, discs, selss, ctrs, |
1373 fun derive_maps_sets_rels (ctr_sugar as {casex, case_cong, case_thms, discs, selss, ctrs, |
1373 exhaust, disc_thmss, sel_thmss, injects, distincts, ...} : ctr_sugar, lthy) = |
1374 exhaust, exhaust_discs, disc_thmss, sel_thmss, injects, distincts, distinct_discsss, |
|
1375 ...} : ctr_sugar, lthy) = |
1374 if live = 0 then |
1376 if live = 0 then |
1375 ((([], [], [], []), ctr_sugar), lthy) |
1377 ((([], [], [], []), ctr_sugar), lthy) |
1376 else |
1378 else |
1377 let |
1379 let |
1378 val rel_flip = rel_flip_of_bnf fp_bnf; |
1380 val rel_flip = rel_flip_of_bnf fp_bnf; |
1468 map (fn th => th RS @{thm eq_False[THEN iffD2]}) rel_distinct_thms @ |
1470 map (fn th => th RS @{thm eq_False[THEN iffD2]}) rel_distinct_thms @ |
1469 map2 (fn th => fn 0 => th RS @{thm eq_True[THEN iffD2]} | _ => th) |
1471 map2 (fn th => fn 0 => th RS @{thm eq_True[THEN iffD2]} | _ => th) |
1470 rel_inject_thms ms; |
1472 rel_inject_thms ms; |
1471 |
1473 |
1472 val (map_disc_iff_thms, map_sel_thms, set_sel_thms, rel_sel_thms, set_intros_thms, |
1474 val (map_disc_iff_thms, map_sel_thms, set_sel_thms, rel_sel_thms, set_intros_thms, |
1473 case_transfer_thms, ctr_transfer_thms, (set_cases_thms, set_cases_attrss), |
1475 case_transfer_thms, ctr_transfer_thms, disc_transfer_thms, |
1474 (rel_cases_thm, rel_cases_attrs)) = |
1476 (set_cases_thms, set_cases_attrss), (rel_cases_thm, rel_cases_attrs)) = |
1475 let |
1477 let |
1476 val live_AsBs = filter (op <>) (As ~~ Bs); |
1478 val live_AsBs = filter (op <>) (As ~~ Bs); |
1477 val fTs = map (op -->) live_AsBs; |
1479 val fTs = map (op -->) live_AsBs; |
1478 val (((((fs, Rs), ta), tb), thesis), names_lthy) = names_lthy |
1480 val (((((fs, Rs), ta), tb), thesis), names_lthy) = names_lthy |
1479 |> mk_Frees "f" fTs |
1481 |> mk_Frees "f" fTs |
1486 val ctrAs = map (mk_ctr As) ctrs; |
1488 val ctrAs = map (mk_ctr As) ctrs; |
1487 val ctrBs = map (mk_ctr Bs) ctrs; |
1489 val ctrBs = map (mk_ctr Bs) ctrs; |
1488 val relAsBs = mk_rel live As Bs (rel_of_bnf fp_bnf); |
1490 val relAsBs = mk_rel live As Bs (rel_of_bnf fp_bnf); |
1489 val setAs = map (mk_set As) (sets_of_bnf fp_bnf); |
1491 val setAs = map (mk_set As) (sets_of_bnf fp_bnf); |
1490 val discAs = map (mk_disc_or_sel As) discs; |
1492 val discAs = map (mk_disc_or_sel As) discs; |
|
1493 val discBs = map (mk_disc_or_sel Bs) discs; |
1491 val selAss = map (map (mk_disc_or_sel As)) selss; |
1494 val selAss = map (map (mk_disc_or_sel As)) selss; |
1492 val discAs_selAss = flat (map2 (map o pair) discAs selAss); |
1495 val discAs_selAss = flat (map2 (map o pair) discAs selAss); |
1493 |
1496 |
1494 val ctr_transfer_thms = |
1497 val ctr_transfer_thms = |
1495 let |
1498 let |
1702 Goal.prove_sorry lthy [] [] goal |
1704 Goal.prove_sorry lthy [] [] goal |
1703 (fn {context = ctxt, prems = _} => |
1705 (fn {context = ctxt, prems = _} => |
1704 mk_case_transfer_tac ctxt rel_cases_thm case_thms) |
1706 mk_case_transfer_tac ctxt rel_cases_thm case_thms) |
1705 |> singleton (Proof_Context.export names_lthy lthy) |
1707 |> singleton (Proof_Context.export names_lthy lthy) |
1706 |> Thm.close_derivation |
1708 |> Thm.close_derivation |
|
1709 end; |
|
1710 |
|
1711 val disc_transfer_thms = |
|
1712 let |
|
1713 val goals = map2 (mk_parametricity_goal names_lthy Rs) discAs discBs; |
|
1714 in |
|
1715 if null goals then [] |
|
1716 else |
|
1717 Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals) |
|
1718 (fn {context = ctxt, prems = _} => |
|
1719 mk_disc_transfer_tac ctxt (the_single rel_sel_thms) |
|
1720 (the_single exhaust_discs) (flat (flat distinct_discsss))) |
|
1721 |> Conjunction.elim_balanced (length goals) |
|
1722 |> Proof_Context.export names_lthy lthy |
|
1723 |> map Thm.close_derivation |
1707 end; |
1724 end; |
1708 |
1725 |
1709 val map_disc_iff_thms = |
1726 val map_disc_iff_thms = |
1710 let |
1727 let |
1711 val discsB = map (mk_disc_or_sel Bs) discs; |
1728 val discsB = map (mk_disc_or_sel Bs) discs; |
1830 |> Proof_Context.export names_lthy lthy |
1847 |> Proof_Context.export names_lthy lthy |
1831 |> map Thm.close_derivation |
1848 |> map Thm.close_derivation |
1832 end; |
1849 end; |
1833 in |
1850 in |
1834 (map_disc_iff_thms, map_sel_thms, set_sel_thms, rel_sel_thms, set_intros_thms, |
1851 (map_disc_iff_thms, map_sel_thms, set_sel_thms, rel_sel_thms, set_intros_thms, |
1835 case_transfer_thms, ctr_transfer_thms, (set_cases_thms, set_cases_attrss), |
1852 case_transfer_thms, ctr_transfer_thms, disc_transfer_thms, |
1836 (rel_cases_thm, rel_cases_attrs)) |
1853 (set_cases_thms, set_cases_attrss), (rel_cases_thm, rel_cases_attrs)) |
1837 end; |
1854 end; |
1838 |
1855 |
1839 val anonymous_notes = |
1856 val anonymous_notes = |
1840 [([case_cong], fundefcong_attrs), |
1857 [([case_cong], fundefcong_attrs), |
1841 (rel_eq_thms, code_nitpicksimp_attrs)] |
1858 (rel_eq_thms, code_nitpicksimp_attrs)] |
1842 |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])])); |
1859 |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])])); |
1843 |
1860 |
1844 val notes = |
1861 val notes = |
1845 [(case_transferN, [case_transfer_thms], K []), |
1862 [(case_transferN, [case_transfer_thms], K []), |
1846 (ctr_transferN, ctr_transfer_thms, K []), |
1863 (ctr_transferN, ctr_transfer_thms, K []), |
|
1864 (disc_transferN, disc_transfer_thms, K []), |
1847 (mapN, map_thms, K (code_nitpicksimp_attrs @ simp_attrs)), |
1865 (mapN, map_thms, K (code_nitpicksimp_attrs @ simp_attrs)), |
1848 (map_disc_iffN, map_disc_iff_thms, K simp_attrs), |
1866 (map_disc_iffN, map_disc_iff_thms, K simp_attrs), |
1849 (map_selN, map_sel_thms, K []), |
1867 (map_selN, map_sel_thms, K []), |
1850 (rel_casesN, [rel_cases_thm], K rel_cases_attrs), |
1868 (rel_casesN, [rel_cases_thm], K rel_cases_attrs), |
1851 (rel_distinctN, rel_distinct_thms, K simp_attrs), |
1869 (rel_distinctN, rel_distinct_thms, K simp_attrs), |