136 val derive_induct_recs_thms_for_types: (string -> bool) -> BNF_Def.bnf list -> |
136 val derive_induct_recs_thms_for_types: (string -> bool) -> BNF_Def.bnf list -> |
137 ('a * typ list list list list * term list list * 'b) option -> thm -> thm list -> |
137 ('a * typ list list list list * term list list * 'b) option -> thm -> thm list -> |
138 BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> typ list -> typ list -> |
138 BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> typ list -> typ list -> |
139 typ list list list -> thm list -> thm list -> thm list -> term list list -> thm list list -> |
139 typ list list list -> thm list -> thm list -> thm list -> term list list -> thm list list -> |
140 term list -> thm list -> Proof.context -> lfp_sugar_thms |
140 term list -> thm list -> Proof.context -> lfp_sugar_thms |
|
141 val derive_coinduct_thms_for_types: bool -> (term -> term) -> BNF_Def.bnf list -> thm -> |
|
142 thm list -> BNF_Def.bnf list -> typ list -> typ list -> typ list list list -> int list -> |
|
143 thm list -> thm list -> (thm -> thm) -> thm list list -> Ctr_Sugar.ctr_sugar list -> |
|
144 Proof.context -> (thm list * thm) list |
141 val derive_coinduct_corecs_thms_for_types: BNF_Def.bnf list -> |
145 val derive_coinduct_corecs_thms_for_types: BNF_Def.bnf list -> |
142 string * term list * term list list |
146 string * term list * term list list |
143 * (((term list list * term list list * term list list list list * term list list list list) |
147 * (((term list list * term list list * term list list list list * term list list list list) |
144 * term list list list) * typ list) -> |
148 * term list list list) * typ list) -> |
145 thm -> thm list -> thm list -> thm list -> BNF_Def.bnf list -> typ list -> typ list -> |
149 thm -> thm list -> thm list -> thm list -> BNF_Def.bnf list -> typ list -> typ list -> |
1803 in |
1806 in |
1804 Thm.instantiate ([], insts) coind |
1807 Thm.instantiate ([], insts) coind |
1805 |> unfold_thms ctxt unfolds |
1808 |> unfold_thms ctxt unfolds |
1806 end; |
1809 end; |
1807 |
1810 |
1808 fun derive_coinduct_corecs_thms_for_types pre_bnfs (x, cs, cpss, (((pgss, _, _, _), cqgsss), _)) |
1811 fun derive_coinduct_thms_for_types strong alter_r pre_bnfs dtor_coinduct dtor_ctors |
1809 dtor_coinduct dtor_injects dtor_ctors dtor_corec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss |
1812 live_nesting_bnfs fpTs Xs ctrXs_Tsss ns fp_abs_inverses abs_inverses mk_vimage2p ctr_defss |
1810 kss mss ns fp_abs_inverses abs_inverses mk_vimage2p ctr_defss (ctr_sugars : ctr_sugar list) |
1813 (ctr_sugars : ctr_sugar list) ctxt = |
1811 corecs corec_defs lthy = |
|
1812 let |
1814 let |
1813 fun mk_ctor_dtor_corec_thm dtor_inject dtor_ctor corec = |
|
1814 iffD1 OF [dtor_inject, trans OF [corec, dtor_ctor RS sym]]; |
|
1815 |
|
1816 val ctor_dtor_corec_thms = |
|
1817 @{map 3} mk_ctor_dtor_corec_thm dtor_injects dtor_ctors dtor_corec_thms; |
|
1818 |
|
1819 val nn = length pre_bnfs; |
1815 val nn = length pre_bnfs; |
1820 |
1816 |
1821 val pre_map_defs = map map_def_of_bnf pre_bnfs; |
|
1822 val pre_rel_defs = map rel_def_of_bnf pre_bnfs; |
1817 val pre_rel_defs = map rel_def_of_bnf pre_bnfs; |
1823 val live_nesting_map_ident0s = map map_ident0_of_bnf live_nesting_bnfs; |
|
1824 val live_nesting_rel_eqs = map rel_eq_of_bnf live_nesting_bnfs; |
1818 val live_nesting_rel_eqs = map rel_eq_of_bnf live_nesting_bnfs; |
1825 |
1819 |
1826 val fp_b_names = map base_name_of_typ fpTs; |
1820 val fp_b_names = map base_name_of_typ fpTs; |
1827 |
1821 |
1828 val ctrss = map #ctrs ctr_sugars; |
|
1829 val discss = map #discs ctr_sugars; |
1822 val discss = map #discs ctr_sugars; |
1830 val selsss = map #selss ctr_sugars; |
1823 val selsss = map #selss ctr_sugars; |
1831 val exhausts = map #exhaust ctr_sugars; |
1824 val exhausts = map #exhaust ctr_sugars; |
1832 val disc_thmsss = map #disc_thmss ctr_sugars; |
1825 val disc_thmsss = map #disc_thmss ctr_sugars; |
1833 val discIss = map #discIs ctr_sugars; |
|
1834 val sel_thmsss = map #sel_thmss ctr_sugars; |
1826 val sel_thmsss = map #sel_thmss ctr_sugars; |
1835 |
1827 |
1836 val (((rs, us'), vs'), _) = lthy |
1828 val (((rs, us'), vs'), _) = ctxt |
1837 |> mk_Frees "R" (map (fn T => mk_pred2T T T) fpTs) |
1829 |> mk_Frees "R" (map (fn T => mk_pred2T T T) fpTs) |
1838 ||>> Variable.variant_fixes fp_b_names |
1830 ||>> Variable.variant_fixes fp_b_names |
1839 ||>> Variable.variant_fixes (map (suffix "'") fp_b_names); |
1831 ||>> Variable.variant_fixes (map (suffix "'") fp_b_names); |
1840 |
1832 |
1841 val us = map2 (curry Free) us' fpTs; |
1833 val us = map2 (curry Free) us' fpTs; |
1844 |
1836 |
1845 val vs = map2 (curry Free) vs' fpTs; |
1837 val vs = map2 (curry Free) vs' fpTs; |
1846 val vdiscss = map2 (map o rapp) vs discss; |
1838 val vdiscss = map2 (map o rapp) vs discss; |
1847 val vselsss = map2 (map o map o rapp) vs selsss; |
1839 val vselsss = map2 (map o map o rapp) vs selsss; |
1848 |
1840 |
1849 val coinduct_thms_pairs = |
1841 val uvrs = @{map 3} (fn r => fn u => fn v => r $ u $ v) rs us vs; |
1850 let |
1842 val uv_eqs = map2 (curry HOLogic.mk_eq) us vs; |
1851 val uvrs = @{map 3} (fn r => fn u => fn v => r $ u $ v) rs us vs; |
1843 val strong_rs = |
1852 val uv_eqs = map2 (curry HOLogic.mk_eq) us vs; |
1844 @{map 4} (fn u => fn v => fn uvr => fn uv_eq => |
1853 val strong_rs = |
1845 fold_rev Term.lambda [u, v] (HOLogic.mk_disj (uvr, uv_eq))) us vs uvrs uv_eqs; |
1854 @{map 4} (fn u => fn v => fn uvr => fn uv_eq => |
1846 |
1855 fold_rev Term.lambda [u, v] (HOLogic.mk_disj (uvr, uv_eq))) us vs uvrs uv_eqs; |
1847 fun build_the_rel rs' T Xs_T = |
1856 |
1848 build_rel [] ctxt [] (fn (_, X) => nth rs' (find_index (curry (op =) X) Xs)) (T, Xs_T) |
1857 fun build_the_rel rs' T Xs_T = |
1849 |> Term.subst_atomic_types (Xs ~~ fpTs); |
1858 build_rel [] lthy [] (fn (_, X) => nth rs' (find_index (curry (op =) X) Xs)) (T, Xs_T) |
1850 |
1859 |> Term.subst_atomic_types (Xs ~~ fpTs); |
1851 fun build_rel_app rs' usel vsel Xs_T = |
1860 |
1852 fold rapp [usel, vsel] (build_the_rel rs' (fastype_of usel) Xs_T); |
1861 fun build_rel_app rs' usel vsel Xs_T = |
1853 |
1862 fold rapp [usel, vsel] (build_the_rel rs' (fastype_of usel) Xs_T); |
1854 fun mk_prem_ctr_concls rs' n k udisc usels vdisc vsels ctrXs_Ts = |
1863 |
1855 (if k = n then [] else [HOLogic.mk_eq (udisc, vdisc)]) @ |
1864 fun mk_prem_ctr_concls rs' n k udisc usels vdisc vsels ctrXs_Ts = |
1856 (if null usels then |
1865 (if k = n then [] else [HOLogic.mk_eq (udisc, vdisc)]) @ |
1857 [] |
1866 (if null usels then |
1858 else |
1867 [] |
1859 [Library.foldr HOLogic.mk_imp (if n = 1 then [] else [udisc, vdisc], |
1868 else |
1860 Library.foldr1 HOLogic.mk_conj (@{map 3} (build_rel_app rs') usels vsels ctrXs_Ts))]); |
1869 [Library.foldr HOLogic.mk_imp (if n = 1 then [] else [udisc, vdisc], |
1861 |
1870 Library.foldr1 HOLogic.mk_conj |
1862 fun mk_prem_concl rs' n udiscs uselss vdiscs vselss ctrXs_Tss = |
1871 (@{map 3} (build_rel_app rs') usels vsels ctrXs_Ts))]); |
1863 flat (@{map 6} (mk_prem_ctr_concls rs' n) (1 upto n) udiscs uselss vdiscs vselss ctrXs_Tss) |
1872 |
1864 |> Library.foldr1 HOLogic.mk_conj |
1873 fun mk_prem_concl rs' n udiscs uselss vdiscs vselss ctrXs_Tss = |
1865 handle List.Empty => @{term True}; |
1874 Library.foldr1 HOLogic.mk_conj (flat (@{map 6} (mk_prem_ctr_concls rs' n) |
1866 |
1875 (1 upto n) udiscs uselss vdiscs vselss ctrXs_Tss)) |
1867 fun mk_prem rs' uvr u v n udiscs uselss vdiscs vselss ctrXs_Tss = |
1876 handle List.Empty => @{term True}; |
1868 fold_rev Logic.all [u, v] (Logic.mk_implies (HOLogic.mk_Trueprop uvr, |
1877 |
1869 HOLogic.mk_Trueprop (mk_prem_concl rs' n udiscs uselss vdiscs vselss ctrXs_Tss))); |
1878 fun mk_prem rs' uvr u v n udiscs uselss vdiscs vselss ctrXs_Tss = |
1870 |
1879 fold_rev Logic.all [u, v] (Logic.mk_implies (HOLogic.mk_Trueprop uvr, |
1871 val concl = |
1880 HOLogic.mk_Trueprop (mk_prem_concl rs' n udiscs uselss vdiscs vselss ctrXs_Tss))); |
1872 HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj |
1881 |
1873 (@{map 3} (fn uvr => fn u => fn v => HOLogic.mk_imp (uvr, HOLogic.mk_eq (u, v))) |
1882 val concl = |
1874 uvrs us vs)); |
1883 HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj |
1875 |
1884 (@{map 3} (fn uvr => fn u => fn v => HOLogic.mk_imp (uvr, HOLogic.mk_eq (u, v))) |
1876 fun mk_goal rs0' = |
1885 uvrs us vs)); |
1877 Logic.list_implies (@{map 9} (mk_prem (map alter_r rs0')) uvrs us vs ns udiscss uselsss |
1886 |
1878 vdiscss vselsss ctrXs_Tsss, concl); |
1887 fun mk_goal rs' = |
1879 |
1888 Logic.list_implies (@{map 9} (mk_prem rs') uvrs us vs ns udiscss uselsss vdiscss vselsss |
1880 val goals = map mk_goal ([rs] @ (if strong then [strong_rs] else [])); |
1889 ctrXs_Tsss, concl); |
1881 |
1890 |
1882 fun prove dtor_coinduct' goal = |
1891 val goals = map mk_goal [rs, strong_rs]; |
1883 Variable.add_free_names ctxt goal [] |
1892 val varss = map (fn goal => Variable.add_free_names lthy goal []) goals; |
1884 |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, ...} => |
1893 |
1885 mk_coinduct_tac ctxt live_nesting_rel_eqs nn ns dtor_coinduct' pre_rel_defs fp_abs_inverses |
1894 fun prove dtor_coinduct' goal vars = |
1886 abs_inverses dtor_ctors exhausts ctr_defss disc_thmsss sel_thmsss)) |
1895 Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, ...} => |
1887 |> Thm.close_derivation; |
1896 mk_coinduct_tac ctxt live_nesting_rel_eqs nn ns dtor_coinduct' pre_rel_defs |
1888 |
1897 fp_abs_inverses abs_inverses dtor_ctors exhausts ctr_defss disc_thmsss sel_thmsss) |
1889 val rel_eqs = map rel_eq_of_bnf pre_bnfs; |
1898 |> Thm.close_derivation; |
1890 val rel_monos = map rel_mono_of_bnf pre_bnfs; |
1899 |
1891 val dtor_coinducts = |
1900 val rel_eqs = map rel_eq_of_bnf pre_bnfs; |
1892 [dtor_coinduct] @ |
1901 val rel_monos = map rel_mono_of_bnf pre_bnfs; |
1893 (if strong then [mk_coinduct_strong_thm dtor_coinduct rel_eqs rel_monos mk_vimage2p ctxt] |
1902 val dtor_coinducts = |
1894 else []); |
1903 [dtor_coinduct, mk_coinduct_strong_thm dtor_coinduct rel_eqs rel_monos mk_vimage2p lthy] |
1895 in |
1904 in |
1896 map2 (postproc_co_induct ctxt nn mp @{thm conj_commute[THEN iffD1]} oo prove) |
1905 @{map 3} (postproc_co_induct lthy nn mp @{thm conj_commute[THEN iffD1]} ooo prove) |
1897 dtor_coinducts goals |
1906 dtor_coinducts goals varss |
1898 end; |
1907 end; |
1899 |
|
1900 fun derive_coinduct_corecs_thms_for_types pre_bnfs (x, cs, cpss, (((pgss, _, _, _), cqgsss), _)) |
|
1901 dtor_coinduct dtor_injects dtor_ctors dtor_corec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss |
|
1902 kss mss ns fp_abs_inverses abs_inverses mk_vimage2p ctr_defss (ctr_sugars : ctr_sugar list) |
|
1903 corecs corec_defs ctxt = |
|
1904 let |
|
1905 fun mk_ctor_dtor_corec_thm dtor_inject dtor_ctor corec = |
|
1906 iffD1 OF [dtor_inject, trans OF [corec, dtor_ctor RS sym]]; |
|
1907 |
|
1908 val ctor_dtor_corec_thms = |
|
1909 @{map 3} mk_ctor_dtor_corec_thm dtor_injects dtor_ctors dtor_corec_thms; |
|
1910 |
|
1911 val pre_map_defs = map map_def_of_bnf pre_bnfs; |
|
1912 val live_nesting_map_ident0s = map map_ident0_of_bnf live_nesting_bnfs; |
|
1913 |
|
1914 val fp_b_names = map base_name_of_typ fpTs; |
|
1915 |
|
1916 val ctrss = map #ctrs ctr_sugars; |
|
1917 val discss = map #discs ctr_sugars; |
|
1918 val selsss = map #selss ctr_sugars; |
|
1919 val disc_thmsss = map #disc_thmss ctr_sugars; |
|
1920 val discIss = map #discIs ctr_sugars; |
|
1921 val sel_thmsss = map #sel_thmss ctr_sugars; |
|
1922 |
|
1923 val coinduct_thms_pairs = derive_coinduct_thms_for_types true I pre_bnfs dtor_coinduct |
|
1924 dtor_ctors live_nesting_bnfs fpTs Xs ctrXs_Tsss ns fp_abs_inverses abs_inverses mk_vimage2p |
|
1925 ctr_defss ctr_sugars ctxt; |
1908 |
1926 |
1909 fun mk_maybe_not pos = not pos ? HOLogic.mk_not; |
1927 fun mk_maybe_not pos = not pos ? HOLogic.mk_not; |
1910 |
1928 |
1911 val gcorecs = map (lists_bmoc pgss) corecs; |
1929 val gcorecs = map (lists_bmoc pgss) corecs; |
1912 |
1930 |
1913 val corec_thmss = |
1931 val corec_thmss = |
1914 let |
1932 let |
|
1933 val (us', _) = ctxt |
|
1934 |> Variable.variant_fixes fp_b_names; |
|
1935 |
|
1936 val us = map2 (curry Free) us' fpTs; |
|
1937 |
1915 fun mk_goal c cps gcorec n k ctr m cfs' = |
1938 fun mk_goal c cps gcorec n k ctr m cfs' = |
1916 fold_rev (fold_rev Logic.all) ([c] :: pgss) |
1939 fold_rev (fold_rev Logic.all) ([c] :: pgss) |
1917 (Logic.list_implies (seq_conds (HOLogic.mk_Trueprop oo mk_maybe_not) n k cps, |
1940 (Logic.list_implies (seq_conds (HOLogic.mk_Trueprop oo mk_maybe_not) n k cps, |
1918 mk_Trueprop_eq (gcorec $ c, Term.list_comb (ctr, take m cfs')))); |
1941 mk_Trueprop_eq (gcorec $ c, Term.list_comb (ctr, take m cfs')))); |
1919 |
1942 |