166 val Zeros = map (fn empty => |
163 val Zeros = map (fn empty => |
167 HOLogic.mk_tuple (map (fn U => absdummy U empty) activeAs)) emptys; |
164 HOLogic.mk_tuple (map (fn U => absdummy U empty) activeAs)) emptys; |
168 val hrecTs = map fastype_of Zeros; |
165 val hrecTs = map fastype_of Zeros; |
169 val hsetTs = map (fn hrecT => Library.foldr (op -->) (sTs, HOLogic.natT --> hrecT)) hrecTs; |
166 val hsetTs = map (fn hrecT => Library.foldr (op -->) (sTs, HOLogic.natT --> hrecT)) hrecTs; |
170 |
167 |
171 val ((((((((((((((((((((((((((((((((((zs, zs'), zs_copy), zs_copy2), |
168 val (((((((((((((((((((((((((((((((((((zs, zs'), zs_copy), zs_copy2), z's), (ys, ys')), |
172 z's), As), Bs), Bs_copy), B's), B''s), ss), sum_ss), s's), s''s), fs), fs_copy), |
169 As), Bs), Bs_copy), B's), B''s), ss), sum_ss), s's), s''s), fs), fs_copy), |
173 self_fs), gs), all_gs), xFs), yFs), yFs_copy), RFs), (Rtuple, Rtuple')), (hrecs, hrecs')), |
170 self_fs), gs), all_gs), xFs), yFs), yFs_copy), RFs), (Rtuple, Rtuple')), (hrecs, hrecs')), |
174 (nat, nat')), Rs), Rs_copy), R's), sRs), (idx, idx')), Idx), Ris), Kss), names_lthy) = lthy |
171 (nat, nat')), Rs), Rs_copy), R's), sRs), (idx, idx')), Idx), Ris), Kss), names_lthy) = lthy |
175 |> mk_Frees' "b" activeAs |
172 |> mk_Frees' "b" activeAs |
176 ||>> mk_Frees "b" activeAs |
173 ||>> mk_Frees "b" activeAs |
177 ||>> mk_Frees "b" activeAs |
174 ||>> mk_Frees "b" activeAs |
178 ||>> mk_Frees "b" activeBs |
175 ||>> mk_Frees "b" activeBs |
|
176 ||>> mk_Frees' "y" passiveAs |
179 ||>> mk_Frees "A" ATs |
177 ||>> mk_Frees "A" ATs |
180 ||>> mk_Frees "B" BTs |
178 ||>> mk_Frees "B" BTs |
181 ||>> mk_Frees "B" BTs |
179 ||>> mk_Frees "B" BTs |
182 ||>> mk_Frees "B'" B'Ts |
180 ||>> mk_Frees "B'" B'Ts |
183 ||>> mk_Frees "B''" B''Ts |
181 ||>> mk_Frees "B''" B''Ts |
2084 (dtor_map_coinduct, rev (Term.add_tfrees dtor_map_coinduct_goal []), dtor_coinduct) |
2042 (dtor_map_coinduct, rev (Term.add_tfrees dtor_map_coinduct_goal []), dtor_coinduct) |
2085 end; |
2043 end; |
2086 |
2044 |
2087 val timer = time (timer "coinduction"); |
2045 val timer = time (timer "coinduction"); |
2088 |
2046 |
|
2047 val setss_by_bnf = map (fn i => map2 (mk_hset dtors i) ls passiveAs) ks; |
|
2048 val setss_by_range = transpose setss_by_bnf; |
|
2049 |
|
2050 val (hset_dtor_incl_thmss, hset_hset_dtor_incl_thmsss, dtor_hset_induct_thms) = |
|
2051 let |
|
2052 fun tinst_of dtor = |
|
2053 map (SOME o certify lthy) (dtor :: remove (op =) dtor dtors); |
|
2054 fun tinst_of' dtor = case tinst_of dtor of t :: ts => t :: NONE :: ts; |
|
2055 val Tinst = map (pairself (certifyT lthy)) |
|
2056 (map Logic.varifyT_global (deads @ allAs) ~~ (deads @ passiveAs @ Ts)); |
|
2057 val set_incl_thmss = |
|
2058 map2 (fn dtor => map (singleton (Proof_Context.export names_lthy lthy) o |
|
2059 Drule.instantiate' [] (tinst_of' dtor) o |
|
2060 Thm.instantiate (Tinst, []) o Drule.zero_var_indexes)) |
|
2061 dtors set_incl_hset_thmss; |
|
2062 |
|
2063 val tinst = splice (map (SOME o certify lthy) dtors) (replicate n NONE) |
|
2064 val set_minimal_thms = |
|
2065 map (Drule.instantiate' [] tinst o Thm.instantiate (Tinst, []) o |
|
2066 Drule.zero_var_indexes) |
|
2067 hset_minimal_thms; |
|
2068 |
|
2069 val set_set_incl_thmsss = |
|
2070 map2 (fn dtor => map (map (singleton (Proof_Context.export names_lthy lthy) o |
|
2071 Drule.instantiate' [] (NONE :: tinst_of' dtor) o |
|
2072 Thm.instantiate (Tinst, []) o Drule.zero_var_indexes))) |
|
2073 dtors set_hset_incl_hset_thmsss; |
|
2074 |
|
2075 val set_set_incl_thmsss' = transpose (map transpose set_set_incl_thmsss); |
|
2076 |
|
2077 val incls = |
|
2078 maps (map (fn thm => thm RS @{thm subset_Collect_iff})) set_incl_thmss @ |
|
2079 @{thms subset_Collect_iff[OF subset_refl]}; |
|
2080 |
|
2081 fun mk_induct_tinst phis jsets y y' = |
|
2082 map4 (fn phi => fn jset => fn Jz => fn Jz' => |
|
2083 SOME (certify lthy (Term.absfree Jz' (HOLogic.mk_Collect (fst y', snd y', |
|
2084 HOLogic.mk_conj (HOLogic.mk_mem (y, jset $ Jz), phi $ y $ Jz)))))) |
|
2085 phis jsets Jzs Jzs'; |
|
2086 val dtor_set_induct_thms = |
|
2087 map6 (fn set_minimal => fn set_set_inclss => fn jsets => fn y => fn y' => fn phis => |
|
2088 ((set_minimal |
|
2089 |> Drule.instantiate' [] (mk_induct_tinst phis jsets y y') |
|
2090 |> unfold_thms lthy incls) OF |
|
2091 (replicate n ballI @ |
|
2092 maps (map (fn thm => thm RS @{thm subset_CollectI})) set_set_inclss)) |
|
2093 |> singleton (Proof_Context.export names_lthy lthy) |
|
2094 |> rule_by_tactic lthy (ALLGOALS (TRY o etac asm_rl))) |
|
2095 set_minimal_thms set_set_incl_thmsss' setss_by_range ys ys' dtor_set_induct_phiss |
|
2096 in |
|
2097 (set_incl_thmss, set_set_incl_thmsss, dtor_set_induct_thms) |
|
2098 end; |
|
2099 |
2089 fun mk_dtor_map_DEADID_thm dtor_inject map_id0 = |
2100 fun mk_dtor_map_DEADID_thm dtor_inject map_id0 = |
2090 trans OF [iffD2 OF [dtor_inject, id_apply], map_id0 RS sym]; |
2101 trans OF [iffD2 OF [dtor_inject, id_apply], map_id0 RS sym]; |
2091 |
2102 |
2092 fun mk_dtor_Jrel_DEADID_thm dtor_inject bnf = |
2103 fun mk_dtor_Jrel_DEADID_thm dtor_inject bnf = |
2093 trans OF [rel_eq_of_bnf bnf RS @{thm predicate2_eqD}, dtor_inject] RS sym; |
2104 trans OF [rel_eq_of_bnf bnf RS @{thm predicate2_eqD}, dtor_inject] RS sym; |
2094 |
2105 |
2095 val JphiTs = map2 mk_pred2T passiveAs passiveBs; |
2106 val JphiTs = map2 mk_pred2T passiveAs passiveBs; |
|
2107 val Jpsi1Ts = map2 mk_pred2T passiveAs passiveCs; |
|
2108 val Jpsi2Ts = map2 mk_pred2T passiveCs passiveBs; |
2096 val prodTsTs' = map2 (curry HOLogic.mk_prodT) Ts Ts'; |
2109 val prodTsTs' = map2 (curry HOLogic.mk_prodT) Ts Ts'; |
2097 val fstsTsTs' = map fst_const prodTsTs'; |
2110 val fstsTsTs' = map fst_const prodTsTs'; |
2098 val sndsTsTs' = map snd_const prodTsTs'; |
2111 val sndsTsTs' = map snd_const prodTsTs'; |
2099 val activephiTs = map2 mk_pred2T activeAs activeBs; |
2112 val activephiTs = map2 mk_pred2T activeAs activeBs; |
2100 val activeJphiTs = map2 mk_pred2T Ts Ts'; |
2113 val activeJphiTs = map2 mk_pred2T Ts Ts'; |
2101 val (((Jphis, activephis), activeJphis), names_lthy) = names_lthy |
2114 val (((((Jphis, Jpsi1s), Jpsi2s), activephis), activeJphis), names_lthy) = names_lthy |
2102 |> mk_Frees "R" JphiTs |
2115 |> mk_Frees "R" JphiTs |
|
2116 ||>> mk_Frees "R" Jpsi1Ts |
|
2117 ||>> mk_Frees "Q" Jpsi2Ts |
2103 ||>> mk_Frees "S" activephiTs |
2118 ||>> mk_Frees "S" activephiTs |
2104 ||>> mk_Frees "JR" activeJphiTs; |
2119 ||>> mk_Frees "JR" activeJphiTs; |
2105 val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs; |
2120 val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs; |
2106 val in_rels = map in_rel_of_bnf bnfs; |
2121 val in_rels = map in_rel_of_bnf bnfs; |
2107 |
2122 |
|
2123 fun mk_Jrel_DEADID_coinduct_thm () = |
|
2124 mk_rel_xtor_co_induct_thm Greatest_FP rels activeJphis (map HOLogic.eq_const Ts) Jphis |
|
2125 Jzs Jz's dtors dtor's (fn {context = ctxt, prems} => |
|
2126 (unfold_thms_tac ctxt @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} THEN |
|
2127 REPEAT_DETERM (rtac allI 1) THEN rtac (dtor_coinduct_thm OF prems) 1)) lthy; |
|
2128 |
2108 (*register new codatatypes as BNFs*) |
2129 (*register new codatatypes as BNFs*) |
2109 val (timer, Jbnfs, (folded_dtor_map_o_thms, folded_dtor_map_thms), folded_dtor_set_thmss', |
2130 val (timer, Jbnfs, (dtor_Jmap_o_thms, dtor_Jmap_thms), dtor_Jset_thmss', |
2110 dtor_set_induct_thms, dtor_Jrel_thms, Jbnf_notes, lthy) = |
2131 dtor_Jrel_thms, Jrel_coinduct_thm, Jbnf_notes, lthy) = |
2111 if m = 0 then |
2132 if m = 0 then |
2112 (timer, replicate n DEADID_bnf, |
2133 (timer, replicate n DEADID_bnf, |
2113 map_split (`(mk_pointfree lthy)) (map2 mk_dtor_map_DEADID_thm dtor_inject_thms map_ids), |
2134 map_split (`(mk_pointfree lthy)) (map2 mk_dtor_map_DEADID_thm dtor_inject_thms map_ids), |
2114 replicate n [], [], map2 mk_dtor_Jrel_DEADID_thm dtor_inject_thms bnfs, [], lthy) |
2135 replicate n [], map2 mk_dtor_Jrel_DEADID_thm dtor_inject_thms bnfs, |
|
2136 mk_Jrel_DEADID_coinduct_thm (), [], lthy) |
2115 else let |
2137 else let |
2116 val fTs = map2 (curry op -->) passiveAs passiveBs; |
2138 val fTs = map2 (curry op -->) passiveAs passiveBs; |
2117 val gTs = map2 (curry op -->) passiveBs passiveCs; |
2139 val gTs = map2 (curry op -->) passiveBs passiveCs; |
2118 val f1Ts = map2 (curry op -->) passiveAs passiveYs; |
|
2119 val f2Ts = map2 (curry op -->) passiveBs passiveYs; |
|
2120 val p1Ts = map2 (curry op -->) passiveXs passiveAs; |
|
2121 val p2Ts = map2 (curry op -->) passiveXs passiveBs; |
|
2122 val pTs = map2 (curry op -->) passiveXs passiveCs; |
|
2123 val uTs = map2 (curry op -->) Ts Ts'; |
2140 val uTs = map2 (curry op -->) Ts Ts'; |
2124 val B1Ts = map HOLogic.mk_setT passiveAs; |
2141 |
2125 val B2Ts = map HOLogic.mk_setT passiveBs; |
2142 val ((((((((fs, fs'), fs_copy), gs), us), (Jys, Jys')), (Jys_copy, Jys'_copy)), |
2126 val AXTs = map HOLogic.mk_setT passiveXs; |
2143 (ys_copy, ys'_copy)), names_lthy) = names_lthy |
2127 val XTs = mk_Ts passiveXs; |
|
2128 val YTs = mk_Ts passiveYs; |
|
2129 |
|
2130 val ((((((((((((((((((fs, fs'), fs_copy), gs), us), |
|
2131 (Jys, Jys')), (Jys_copy, Jys'_copy)), dtor_set_induct_phiss), |
|
2132 B1s), B2s), AXs), f1s), f2s), p1s), p2s), ps), (ys, ys')), (ys_copy, ys'_copy)), |
|
2133 names_lthy) = names_lthy |
|
2134 |> mk_Frees' "f" fTs |
2144 |> mk_Frees' "f" fTs |
2135 ||>> mk_Frees "f" fTs |
2145 ||>> mk_Frees "f" fTs |
2136 ||>> mk_Frees "g" gTs |
2146 ||>> mk_Frees "g" gTs |
2137 ||>> mk_Frees "u" uTs |
2147 ||>> mk_Frees "u" uTs |
2138 ||>> mk_Frees' "b" Ts' |
2148 ||>> mk_Frees' "b" Ts' |
2139 ||>> mk_Frees' "b" Ts' |
2149 ||>> mk_Frees' "b" Ts' |
2140 ||>> mk_Freess "P" (map (fn A => map (mk_pred2T A) Ts) passiveAs) |
|
2141 ||>> mk_Frees "B1" B1Ts |
|
2142 ||>> mk_Frees "B2" B2Ts |
|
2143 ||>> mk_Frees "A" AXTs |
|
2144 ||>> mk_Frees "f1" f1Ts |
|
2145 ||>> mk_Frees "f2" f2Ts |
|
2146 ||>> mk_Frees "p1" p1Ts |
|
2147 ||>> mk_Frees "p2" p2Ts |
|
2148 ||>> mk_Frees "p" pTs |
|
2149 ||>> mk_Frees' "y" passiveAs |
|
2150 ||>> mk_Frees' "y" passiveAs; |
2150 ||>> mk_Frees' "y" passiveAs; |
2151 |
2151 |
2152 val map_FTFT's = map2 (fn Ds => |
2152 val map_FTFT's = map2 (fn Ds => |
2153 mk_map_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs; |
2153 mk_map_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs; |
2154 |
2154 |
2158 fun mk_map mk_const mk_T Ts fs Ts' dtors mk_maps = |
2158 fun mk_map mk_const mk_T Ts fs Ts' dtors mk_maps = |
2159 mk_unfold Ts' (map2 (fn dtor => fn Fmap => |
2159 mk_unfold Ts' (map2 (fn dtor => fn Fmap => |
2160 HOLogic.mk_comp (mk_Fmap mk_const fs Ts Fmap, dtor)) dtors (mk_maps Ts mk_T)); |
2160 HOLogic.mk_comp (mk_Fmap mk_const fs Ts Fmap, dtor)) dtors (mk_maps Ts mk_T)); |
2161 val mk_map_id = mk_map HOLogic.id_const I; |
2161 val mk_map_id = mk_map HOLogic.id_const I; |
2162 val mk_mapsAB = mk_maps passiveAs passiveBs; |
2162 val mk_mapsAB = mk_maps passiveAs passiveBs; |
2163 val mk_mapsBC = mk_maps passiveBs passiveCs; |
|
2164 val mk_mapsAC = mk_maps passiveAs passiveCs; |
|
2165 val mk_mapsAY = mk_maps passiveAs passiveYs; |
|
2166 val mk_mapsBY = mk_maps passiveBs passiveYs; |
|
2167 val mk_mapsXA = mk_maps passiveXs passiveAs; |
|
2168 val mk_mapsXB = mk_maps passiveXs passiveBs; |
|
2169 val mk_mapsXC = mk_maps passiveXs passiveCs; |
|
2170 val fs_maps = map (mk_map_id Ts fs Ts' dtors mk_mapsAB) ks; |
2163 val fs_maps = map (mk_map_id Ts fs Ts' dtors mk_mapsAB) ks; |
2171 val fs_copy_maps = map (mk_map_id Ts fs_copy Ts' dtors mk_mapsAB) ks; |
2164 |
2172 val gs_maps = map (mk_map_id Ts' gs Ts'' dtor's mk_mapsBC) ks; |
2165 val set_bss = |
2173 val fgs_maps = |
2166 map (flat o map2 (fn B => fn b => |
2174 map (mk_map_id Ts (map2 (curry HOLogic.mk_comp) gs fs) Ts'' dtors mk_mapsAC) ks; |
2167 if member (op =) resDs (TFree B) then [] else [b]) resBs) set_bss0; |
2175 val Xdtors = mk_dtors passiveXs; |
|
2176 val UNIV's = map HOLogic.mk_UNIV Ts'; |
|
2177 val CUNIVs = map HOLogic.mk_UNIV passiveCs; |
|
2178 val UNIV''s = map HOLogic.mk_UNIV Ts''; |
|
2179 val dtor''s = mk_dtors passiveCs; |
|
2180 val f1s_maps = map (mk_map_id Ts f1s YTs dtors mk_mapsAY) ks; |
|
2181 val f2s_maps = map (mk_map_id Ts' f2s YTs dtor's mk_mapsBY) ks; |
|
2182 val pid_maps = map (mk_map_id XTs ps Ts'' Xdtors mk_mapsXC) ks; |
|
2183 val pfst_Fmaps = |
|
2184 map (mk_Fmap fst_const p1s prodTsTs') (mk_mapsXA prodTsTs' (fst o HOLogic.dest_prodT)); |
|
2185 val psnd_Fmaps = |
|
2186 map (mk_Fmap snd_const p2s prodTsTs') (mk_mapsXB prodTsTs' (snd o HOLogic.dest_prodT)); |
|
2187 val p1id_Fmaps = map (mk_Fmap HOLogic.id_const p1s prodTsTs') (mk_mapsXA prodTsTs' I); |
|
2188 val p2id_Fmaps = map (mk_Fmap HOLogic.id_const p2s prodTsTs') (mk_mapsXB prodTsTs' I); |
|
2189 val pid_Fmaps = map (mk_Fmap HOLogic.id_const ps prodTsTs') (mk_mapsXC prodTsTs' I); |
|
2190 |
|
2191 val (dtor_map_thms, map_thms) = |
|
2192 let |
|
2193 fun mk_goal fs_map map dtor dtor' = fold_rev Logic.all fs |
|
2194 (mk_Trueprop_eq (HOLogic.mk_comp (dtor', fs_map), |
|
2195 HOLogic.mk_comp (Term.list_comb (map, fs @ fs_maps), dtor))); |
|
2196 val goals = map4 mk_goal fs_maps map_FTFT's dtors dtor's; |
|
2197 val cTs = map (SOME o certifyT lthy) FTs'; |
|
2198 val maps = |
|
2199 map5 (fn goal => fn cT => fn unfold => fn map_comp => fn map_cong0 => |
|
2200 Goal.prove_sorry lthy [] [] goal |
|
2201 (K (mk_map_tac m n cT unfold map_comp map_cong0)) |
|
2202 |> Thm.close_derivation) |
|
2203 goals cTs dtor_unfold_thms map_comps map_cong0s; |
|
2204 in |
|
2205 map_split (fn thm => (thm RS @{thm comp_eq_dest}, thm)) maps |
|
2206 end; |
|
2207 |
|
2208 val map_comp0_thms = |
|
2209 let |
|
2210 val goal = fold_rev Logic.all (fs @ gs) |
|
2211 (HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj |
|
2212 (map3 (fn fmap => fn gmap => fn fgmap => |
|
2213 HOLogic.mk_eq (HOLogic.mk_comp (gmap, fmap), fgmap)) |
|
2214 fs_maps gs_maps fgs_maps))) |
|
2215 in |
|
2216 split_conj_thm (Goal.prove_sorry lthy [] [] goal |
|
2217 (K (mk_map_comp0_tac m n map_thms map_comp0s map_cong0s dtor_unfold_unique_thm)) |
|
2218 |> Thm.close_derivation) |
|
2219 end; |
|
2220 |
|
2221 val dtor_map_unique_thm = |
|
2222 let |
|
2223 fun mk_prem u map dtor dtor' = |
|
2224 mk_Trueprop_eq (HOLogic.mk_comp (dtor', u), |
|
2225 HOLogic.mk_comp (Term.list_comb (map, fs @ us), dtor)); |
|
2226 val prems = map4 mk_prem us map_FTFT's dtors dtor's; |
|
2227 val goal = |
|
2228 HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj |
|
2229 (map2 (curry HOLogic.mk_eq) us fs_maps)); |
|
2230 in |
|
2231 Goal.prove_sorry lthy [] [] |
|
2232 (fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal))) |
|
2233 (mk_dtor_map_unique_tac dtor_unfold_unique_thm sym_map_comps) |
|
2234 |> Thm.close_derivation |
|
2235 end; |
|
2236 |
|
2237 val timer = time (timer "map functions for the new codatatypes"); |
|
2238 |
|
2239 val setss_by_bnf = map (fn i => map2 (mk_hset dtors i) ls passiveAs) ks; |
|
2240 val setss_by_bnf' = map (fn i => map2 (mk_hset dtor's i) ls passiveBs) ks; |
|
2241 val setss_by_range = transpose setss_by_bnf; |
|
2242 |
|
2243 val dtor_set_thmss = |
|
2244 let |
|
2245 fun mk_simp_goal relate pas_set act_sets sets dtor z set = |
|
2246 relate (set $ z, mk_union (pas_set $ (dtor $ z), |
|
2247 Library.foldl1 mk_union |
|
2248 (map2 (fn X => mk_UNION (X $ (dtor $ z))) act_sets sets))); |
|
2249 fun mk_goals eq = |
|
2250 map2 (fn i => fn sets => |
|
2251 map4 (fn Fsets => |
|
2252 mk_simp_goal eq (nth Fsets (i - 1)) (drop m Fsets) sets) |
|
2253 FTs_setss dtors Jzs sets) |
|
2254 ls setss_by_range; |
|
2255 |
|
2256 val le_goals = map |
|
2257 (fold_rev Logic.all Jzs o HOLogic.mk_Trueprop o Library.foldr1 HOLogic.mk_conj) |
|
2258 (mk_goals (uncurry mk_leq)); |
|
2259 val set_le_thmss = map split_conj_thm |
|
2260 (map4 (fn goal => fn hset_minimal => fn set_hsets => fn set_hset_hsetss => |
|
2261 Goal.prove_sorry lthy [] [] goal |
|
2262 (K (mk_set_le_tac n hset_minimal set_hsets set_hset_hsetss)) |
|
2263 |> Thm.close_derivation) |
|
2264 le_goals hset_minimal_thms set_hset_thmss' set_hset_hset_thmsss'); |
|
2265 |
|
2266 val simp_goalss = map (map2 (fn z => fn goal => |
|
2267 Logic.all z (HOLogic.mk_Trueprop goal)) Jzs) |
|
2268 (mk_goals HOLogic.mk_eq); |
|
2269 in |
|
2270 map4 (map4 (fn goal => fn set_le => fn set_incl_hset => fn set_hset_incl_hsets => |
|
2271 Goal.prove_sorry lthy [] [] goal |
|
2272 (K (mk_dtor_set_tac n set_le set_incl_hset set_hset_incl_hsets)) |
|
2273 |> Thm.close_derivation)) |
|
2274 simp_goalss set_le_thmss set_incl_hset_thmss' set_hset_incl_hset_thmsss' |
|
2275 end; |
|
2276 |
|
2277 val timer = time (timer "set functions for the new codatatypes"); |
|
2278 |
|
2279 val colss = map2 (fn j => fn T => |
|
2280 map (fn i => mk_hset_rec dtors nat i j T) ks) ls passiveAs; |
|
2281 val colss' = map2 (fn j => fn T => |
|
2282 map (fn i => mk_hset_rec dtor's nat i j T) ks) ls passiveBs; |
|
2283 val Xcolss = map2 (fn j => fn T => |
|
2284 map (fn i => mk_hset_rec Xdtors nat i j T) ks) ls passiveXs; |
|
2285 |
|
2286 val col_natural_thmss = |
|
2287 let |
|
2288 fun mk_col_natural f map z col col' = |
|
2289 HOLogic.mk_eq (mk_image f $ (col $ z), col' $ (map $ z)); |
|
2290 |
|
2291 fun mk_goal f cols cols' = list_all_free Jzs (Library.foldr1 HOLogic.mk_conj |
|
2292 (map4 (mk_col_natural f) fs_maps Jzs cols cols')); |
|
2293 |
|
2294 val goals = map3 mk_goal fs colss colss'; |
|
2295 |
|
2296 val ctss = |
|
2297 map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat]) goals; |
|
2298 |
|
2299 val thms = |
|
2300 map4 (fn goal => fn cts => fn rec_0s => fn rec_Sucs => |
|
2301 singleton (Proof_Context.export names_lthy lthy) |
|
2302 (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal) |
|
2303 (mk_col_natural_tac cts rec_0s rec_Sucs dtor_map_thms set_mapss)) |
|
2304 |> Thm.close_derivation) |
|
2305 goals ctss hset_rec_0ss' hset_rec_Sucss'; |
|
2306 in |
|
2307 map (split_conj_thm o mk_specN n) thms |
|
2308 end; |
|
2309 |
|
2310 val col_bd_thmss = |
|
2311 let |
|
2312 fun mk_col_bd z col = mk_ordLeq (mk_card_of (col $ z)) sbd; |
|
2313 |
|
2314 fun mk_goal cols = list_all_free Jzs (Library.foldr1 HOLogic.mk_conj |
|
2315 (map2 mk_col_bd Jzs cols)); |
|
2316 |
|
2317 val goals = map mk_goal colss; |
|
2318 |
|
2319 val ctss = |
|
2320 map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat]) goals; |
|
2321 |
|
2322 val thms = |
|
2323 map5 (fn j => fn goal => fn cts => fn rec_0s => fn rec_Sucs => |
|
2324 singleton (Proof_Context.export names_lthy lthy) |
|
2325 (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal) |
|
2326 (K (mk_col_bd_tac m j cts rec_0s rec_Sucs |
|
2327 sbd_Card_order sbd_Cinfinite set_sbdss))) |
|
2328 |> Thm.close_derivation) |
|
2329 ls goals ctss hset_rec_0ss' hset_rec_Sucss'; |
|
2330 in |
|
2331 map (split_conj_thm o mk_specN n) thms |
|
2332 end; |
|
2333 |
|
2334 val map_cong0_thms = |
|
2335 let |
|
2336 val cTs = map (SOME o certifyT lthy o |
|
2337 Term.typ_subst_atomic (passiveAs ~~ passiveBs) o TFree) coinduct_params; |
|
2338 |
|
2339 fun mk_prem z set f g y y' = |
|
2340 mk_Ball (set $ z) (Term.absfree y' (HOLogic.mk_eq (f $ y, g $ y))); |
|
2341 |
|
2342 fun mk_prems sets z = |
|
2343 Library.foldr1 HOLogic.mk_conj (map5 (mk_prem z) sets fs fs_copy ys ys') |
|
2344 |
|
2345 fun mk_map_cong0 sets z fmap gmap = |
|
2346 HOLogic.mk_imp (mk_prems sets z, HOLogic.mk_eq (fmap $ z, gmap $ z)); |
|
2347 |
|
2348 fun mk_coind_body sets (x, T) z fmap gmap y y_copy = |
|
2349 HOLogic.mk_conj |
|
2350 (HOLogic.mk_mem (z, HOLogic.mk_Collect (x, T, mk_prems sets z)), |
|
2351 HOLogic.mk_conj (HOLogic.mk_eq (y, fmap $ z), |
|
2352 HOLogic.mk_eq (y_copy, gmap $ z))) |
|
2353 |
|
2354 fun mk_cphi sets (z' as (x, T)) z fmap gmap y' y y'_copy y_copy = |
|
2355 HOLogic.mk_exists (x, T, mk_coind_body sets z' z fmap gmap y y_copy) |
|
2356 |> Term.absfree y'_copy |
|
2357 |> Term.absfree y' |
|
2358 |> certify lthy; |
|
2359 |
|
2360 val cphis = |
|
2361 map9 mk_cphi setss_by_bnf Jzs' Jzs fs_maps fs_copy_maps Jys' Jys Jys'_copy Jys_copy; |
|
2362 |
|
2363 val coinduct = Drule.instantiate' cTs (map SOME cphis) dtor_map_coinduct_thm; |
|
2364 |
|
2365 val goal = |
|
2366 HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj |
|
2367 (map4 mk_map_cong0 setss_by_bnf Jzs fs_maps fs_copy_maps)); |
|
2368 |
|
2369 val thm = singleton (Proof_Context.export names_lthy lthy) |
|
2370 (Goal.prove_sorry lthy [] [] goal |
|
2371 (K (mk_mcong_tac lthy m (rtac coinduct) map_comps dtor_map_thms map_cong0s set_mapss |
|
2372 set_hset_thmss set_hset_hset_thmsss))) |
|
2373 |> Thm.close_derivation |
|
2374 in |
|
2375 split_conj_thm thm |
|
2376 end; |
|
2377 |
|
2378 val B1_ins = map2 (mk_in B1s) setss_by_bnf Ts; |
|
2379 val B2_ins = map2 (mk_in B2s) setss_by_bnf' Ts'; |
|
2380 val thePulls = map4 mk_thePull B1_ins B2_ins f1s_maps f2s_maps; |
|
2381 val thePullTs = passiveXs @ map2 (curry HOLogic.mk_prodT) Ts Ts'; |
|
2382 val thePull_ins = map2 (mk_in (AXs @ thePulls)) (mk_setss thePullTs) (mk_FTs thePullTs); |
|
2383 val pickFs = map5 mk_pickWP thePull_ins pfst_Fmaps psnd_Fmaps |
|
2384 (map2 (curry op $) dtors Jzs) (map2 (curry op $) dtor's Jz's); |
|
2385 val pickF_ss = map3 (fn pickF => fn z => fn z' => |
|
2386 HOLogic.mk_split (Term.absfree z (Term.absfree z' pickF))) pickFs Jzs' Jz's'; |
|
2387 val picks = map (mk_unfold XTs pickF_ss) ks; |
|
2388 |
|
2389 val wpull_prem = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj |
|
2390 (map8 mk_wpull AXs B1s B2s f1s f2s (replicate m NONE) p1s p2s)); |
|
2391 |
|
2392 val map_eq_thms = map2 (fn simp => fn diff => box_equals OF [diff RS iffD2, simp, simp]) |
|
2393 dtor_map_thms dtor_inject_thms; |
|
2394 val map_wpull_thms = map (fn thm => thm OF |
|
2395 (replicate m asm_rl @ replicate n @{thm wpull_thePull})) map_wpulls; |
|
2396 val pickWP_assms_tacs = |
|
2397 map3 mk_pickWP_assms_tac set_incl_hset_thmss set_incl_hin_thmss map_eq_thms; |
|
2398 |
|
2399 val coalg_thePull_thm = |
|
2400 let |
|
2401 val coalg = HOLogic.mk_Trueprop |
|
2402 (mk_coalg CUNIVs thePulls (map2 (curry HOLogic.mk_comp) pid_Fmaps pickF_ss)); |
|
2403 val goal = fold_rev Logic.all (AXs @ B1s @ B2s @ f1s @ f2s @ p1s @ p2s @ ps) |
|
2404 (Logic.mk_implies (wpull_prem, coalg)); |
|
2405 in |
|
2406 Goal.prove_sorry lthy [] [] goal (mk_coalg_thePull_tac m coalg_def map_wpull_thms |
|
2407 set_mapss pickWP_assms_tacs) |
|
2408 |> Thm.close_derivation |
|
2409 end; |
|
2410 |
|
2411 val (mor_thePull_fst_thm, mor_thePull_snd_thm, mor_thePull_pick_thm) = |
|
2412 let |
|
2413 val mor_fst = HOLogic.mk_Trueprop |
|
2414 (mk_mor thePulls (map2 (curry HOLogic.mk_comp) p1id_Fmaps pickF_ss) |
|
2415 UNIVs dtors fstsTsTs'); |
|
2416 val mor_snd = HOLogic.mk_Trueprop |
|
2417 (mk_mor thePulls (map2 (curry HOLogic.mk_comp) p2id_Fmaps pickF_ss) |
|
2418 UNIV's dtor's sndsTsTs'); |
|
2419 val mor_pick = HOLogic.mk_Trueprop |
|
2420 (mk_mor thePulls (map2 (curry HOLogic.mk_comp) pid_Fmaps pickF_ss) |
|
2421 UNIV''s dtor''s (map2 (curry HOLogic.mk_comp) pid_maps picks)); |
|
2422 |
|
2423 val fst_goal = fold_rev Logic.all (AXs @ B1s @ B2s @ f1s @ f2s @ p1s @ p2s) |
|
2424 (Logic.mk_implies (wpull_prem, mor_fst)); |
|
2425 val snd_goal = fold_rev Logic.all (AXs @ B1s @ B2s @ f1s @ f2s @ p1s @ p2s) |
|
2426 (Logic.mk_implies (wpull_prem, mor_snd)); |
|
2427 val pick_goal = fold_rev Logic.all (AXs @ B1s @ B2s @ f1s @ f2s @ p1s @ p2s @ ps) |
|
2428 (Logic.mk_implies (wpull_prem, mor_pick)); |
|
2429 in |
|
2430 (Goal.prove_sorry lthy [] [] fst_goal (mk_mor_thePull_fst_tac m mor_def map_wpull_thms |
|
2431 map_comps pickWP_assms_tacs) |> Thm.close_derivation, |
|
2432 Goal.prove_sorry lthy [] [] snd_goal (mk_mor_thePull_snd_tac m mor_def map_wpull_thms |
|
2433 map_comps pickWP_assms_tacs) |> Thm.close_derivation, |
|
2434 Goal.prove_sorry lthy [] [] pick_goal (mk_mor_thePull_pick_tac mor_def dtor_unfold_thms |
|
2435 map_comps) |> Thm.close_derivation) |
|
2436 end; |
|
2437 |
|
2438 val pick_col_thmss = |
|
2439 let |
|
2440 fun mk_conjunct AX Jpair pick thePull col = |
|
2441 HOLogic.mk_imp (HOLogic.mk_mem (Jpair, thePull), mk_leq (col $ (pick $ Jpair)) AX); |
|
2442 |
|
2443 fun mk_concl AX cols = |
|
2444 list_all_free Jpairs (Library.foldr1 HOLogic.mk_conj |
|
2445 (map4 (mk_conjunct AX) Jpairs picks thePulls cols)); |
|
2446 |
|
2447 val concls = map2 mk_concl AXs Xcolss; |
|
2448 |
|
2449 val ctss = |
|
2450 map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat]) concls; |
|
2451 |
|
2452 val goals = |
|
2453 map (fn concl => Logic.mk_implies (wpull_prem, HOLogic.mk_Trueprop concl)) concls; |
|
2454 |
|
2455 val thms = |
|
2456 map5 (fn j => fn goal => fn cts => fn rec_0s => fn rec_Sucs => |
|
2457 singleton (Proof_Context.export names_lthy lthy) (Goal.prove_sorry lthy [] [] goal |
|
2458 (mk_pick_col_tac m j cts rec_0s rec_Sucs dtor_unfold_thms set_mapss |
|
2459 map_wpull_thms pickWP_assms_tacs)) |
|
2460 |> Thm.close_derivation) |
|
2461 ls goals ctss hset_rec_0ss' hset_rec_Sucss'; |
|
2462 in |
|
2463 map (map (fn thm => thm RS mp) o split_conj_thm o mk_specN n) thms |
|
2464 end; |
|
2465 |
|
2466 val timer = time (timer "helpers for BNF properties"); |
|
2467 |
|
2468 val map_id0_tacs = |
|
2469 map2 (K oo mk_map_id0_tac map_thms) dtor_unfold_unique_thms unfold_dtor_thms; |
|
2470 val map_comp0_tacs = map (fn thm => K (rtac (thm RS sym) 1)) map_comp0_thms; |
|
2471 val map_cong0_tacs = map (mk_map_cong0_tac m) map_cong0_thms; |
|
2472 val set_nat_tacss = |
|
2473 map2 (map2 (K oo mk_set_map0_tac)) hset_defss (transpose col_natural_thmss); |
|
2474 |
|
2475 val bd_co_tacs = replicate n (K (rtac sbd_card_order 1)); |
|
2476 val bd_cinf_tacs = replicate n (K (rtac (sbd_Cinfinite RS conjunct1) 1)); |
|
2477 |
|
2478 val set_bd_tacss = |
|
2479 map2 (map2 (K oo mk_set_bd_tac sbd_Cinfinite)) hset_defss (transpose col_bd_thmss); |
|
2480 |
|
2481 val map_wpull_tacs = |
|
2482 map3 (K ooo mk_wpull_tac m coalg_thePull_thm mor_thePull_fst_thm mor_thePull_snd_thm |
|
2483 mor_thePull_pick_thm) unique_mor_thms (transpose pick_col_thmss) hset_defss; |
|
2484 |
|
2485 val rel_OO_Grp_tacs = replicate n (K (rtac refl 1)); |
|
2486 |
|
2487 val tacss = map9 zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_nat_tacss |
|
2488 bd_co_tacs bd_cinf_tacs set_bd_tacss map_wpull_tacs rel_OO_Grp_tacs; |
|
2489 |
|
2490 val (hset_dtor_incl_thmss, hset_hset_dtor_incl_thmsss, dtor_hset_induct_thms) = |
|
2491 let |
|
2492 fun tinst_of dtor = |
|
2493 map (SOME o certify lthy) (dtor :: remove (op =) dtor dtors); |
|
2494 fun tinst_of' dtor = case tinst_of dtor of t :: ts => t :: NONE :: ts; |
|
2495 val Tinst = map (pairself (certifyT lthy)) |
|
2496 (map Logic.varifyT_global (deads @ allAs) ~~ (deads @ passiveAs @ Ts)); |
|
2497 val set_incl_thmss = |
|
2498 map2 (fn dtor => map (singleton (Proof_Context.export names_lthy lthy) o |
|
2499 Drule.instantiate' [] (tinst_of' dtor) o |
|
2500 Thm.instantiate (Tinst, []) o Drule.zero_var_indexes)) |
|
2501 dtors set_incl_hset_thmss; |
|
2502 |
|
2503 val tinst = splice (map (SOME o certify lthy) dtors) (replicate n NONE) |
|
2504 val set_minimal_thms = |
|
2505 map (Drule.instantiate' [] tinst o Thm.instantiate (Tinst, []) o |
|
2506 Drule.zero_var_indexes) |
|
2507 hset_minimal_thms; |
|
2508 |
|
2509 val set_set_incl_thmsss = |
|
2510 map2 (fn dtor => map (map (singleton (Proof_Context.export names_lthy lthy) o |
|
2511 Drule.instantiate' [] (NONE :: tinst_of' dtor) o |
|
2512 Thm.instantiate (Tinst, []) o Drule.zero_var_indexes))) |
|
2513 dtors set_hset_incl_hset_thmsss; |
|
2514 |
|
2515 val set_set_incl_thmsss' = transpose (map transpose set_set_incl_thmsss); |
|
2516 |
|
2517 val incls = |
|
2518 maps (map (fn thm => thm RS @{thm subset_Collect_iff})) set_incl_thmss @ |
|
2519 @{thms subset_Collect_iff[OF subset_refl]}; |
|
2520 |
|
2521 fun mk_induct_tinst phis jsets y y' = |
|
2522 map4 (fn phi => fn jset => fn Jz => fn Jz' => |
|
2523 SOME (certify lthy (Term.absfree Jz' (HOLogic.mk_Collect (fst y', snd y', |
|
2524 HOLogic.mk_conj (HOLogic.mk_mem (y, jset $ Jz), phi $ y $ Jz)))))) |
|
2525 phis jsets Jzs Jzs'; |
|
2526 val dtor_set_induct_thms = |
|
2527 map6 (fn set_minimal => fn set_set_inclss => fn jsets => fn y => fn y' => fn phis => |
|
2528 ((set_minimal |
|
2529 |> Drule.instantiate' [] (mk_induct_tinst phis jsets y y') |
|
2530 |> unfold_thms lthy incls) OF |
|
2531 (replicate n ballI @ |
|
2532 maps (map (fn thm => thm RS @{thm subset_CollectI})) set_set_inclss)) |
|
2533 |> singleton (Proof_Context.export names_lthy lthy) |
|
2534 |> rule_by_tactic lthy (ALLGOALS (TRY o etac asm_rl))) |
|
2535 set_minimal_thms set_set_incl_thmsss' setss_by_range ys ys' dtor_set_induct_phiss |
|
2536 in |
|
2537 (set_incl_thmss, set_set_incl_thmsss, dtor_set_induct_thms) |
|
2538 end; |
|
2539 |
2168 |
2540 fun close_wit I wit = (I, fold_rev Term.absfree (map (nth ys') I) wit); |
2169 fun close_wit I wit = (I, fold_rev Term.absfree (map (nth ys') I) wit); |
2541 |
2170 |
2542 val all_unitTs = replicate live HOLogic.unitT; |
2171 val all_unitTs = replicate live HOLogic.unitT; |
2543 val unitTs = replicate n HOLogic.unitT; |
2172 val unitTs = replicate n HOLogic.unitT; |
2651 |> filter (fn (_, thms) => length thms = m) |
2288 |> filter (fn (_, thms) => length thms = m) |
2652 end; |
2289 end; |
2653 |
2290 |
2654 val coind_wit_thms = maps mk_coind_wit_thms coind_witss; |
2291 val coind_wit_thms = maps mk_coind_wit_thms coind_witss; |
2655 |
2292 |
2656 val witss = map2 (fn Ds => fn bnf => mk_wits_of_bnf |
2293 val (wit_thmss, all_witss) = |
2657 (replicate (nwits_of_bnf bnf) Ds) |
|
2658 (replicate (nwits_of_bnf bnf) (passiveAs @ Ts)) bnf) Dss bnfs; |
|
2659 |
|
2660 val ctor_witss = |
|
2661 map (map (uncurry close_wit o tree_to_ctor_wit ys ctors witss o snd o snd) o |
|
2662 filter_out (fst o snd)) wit_treess; |
|
2663 |
|
2664 val all_witss = |
|
2665 fold (fn ((i, wit), thms) => fn witss => |
2294 fold (fn ((i, wit), thms) => fn witss => |
2666 nth_map i (fn (thms', wits) => (thms @ thms', wit :: wits)) witss) |
2295 nth_map i (fn (thms', wits) => (thms @ thms', wit :: wits)) witss) |
2667 coind_wit_thms (map (pair []) ctor_witss) |
2296 coind_wit_thms (map (pair []) ctor_witss) |
2668 |> map (apsnd (map snd o minimize_wits)); |
2297 |> map (apsnd (map snd o minimize_wits)) |
2669 |
2298 |> split_list; |
2670 val wit_tac = mk_wit_tac n dtor_ctor_thms (flat dtor_set_thmss) (maps wit_thms_of_bnf bnfs); |
2299 |
2671 |
2300 val (Jbnf_consts, lthy) = |
2672 val set_bss = |
2301 fold_map8 (fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets => fn wits => |
2673 map (flat o map2 (fn B => fn b => |
2302 fn T => fn lthy => |
2674 if member (op =) resDs (TFree B) then [] else [b]) resBs) set_bss0; |
2303 define_bnf_consts Dont_Inline (user_policy Note_Some lthy) (SOME deads) |
2675 |
2304 map_b rel_b set_bs |
2676 val (Jbnfs, lthy) = |
2305 ((((((b, T), fold_rev Term.absfree fs' mapx), sets), sbd), wits), NONE) lthy) |
2677 fold_map9 (fn tacs => fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets => |
2306 bs map_bs rel_bs set_bss fs_maps setss_by_bnf all_witss Ts lthy; |
2678 fn T => fn (thms, wits) => fn lthy => |
2307 |
2679 bnf_def Dont_Inline (user_policy Note_Some) I tacs (wit_tac thms) (SOME deads) map_b |
2308 val (_, Jconsts, Jconst_defs, mk_Jconsts) = split_list4 Jbnf_consts; |
2680 rel_b set_bs |
2309 val (_, Jsetss, Jbds_Ds, Jwitss_Ds, _) = split_list5 Jconsts; |
2681 ((((((b, T), fold_rev Term.absfree fs' mapx), sets), sbd), wits), NONE) lthy |
2310 val (Jmap_defs, Jset_defss, Jbd_defs, Jwit_defss, Jrel_defs) = split_list5 Jconst_defs; |
2682 |> register_bnf (Local_Theory.full_name lthy b)) |
2311 val (mk_Jmaps_Ds, mk_Jt_Ds, _, mk_Jrels_Ds, _) = split_list5 mk_Jconsts; |
2683 tacss bs map_bs rel_bs set_bss fs_maps setss_by_bnf Ts all_witss lthy; |
2312 |
2684 |
2313 val Jrel_unabs_defs = map (fn def => mk_unabs_def m (def RS meta_eq_to_obj_eq)) Jrel_defs; |
2685 val fold_maps = fold_thms lthy (map (fn bnf => |
2314 val Jset_defs = flat Jset_defss; |
2686 mk_unabs_def m (map_def_of_bnf bnf RS meta_eq_to_obj_eq)) Jbnfs); |
2315 val Jset_unabs_defs = map (fn def => def RS meta_eq_to_obj_eq RS fun_cong) Jset_defs; |
2687 |
2316 |
2688 val fold_sets = fold_thms lthy (maps (fn bnf => |
2317 fun mk_Jmaps As Bs = map (fn mk => mk deads As Bs) mk_Jmaps_Ds; |
2689 map (fn thm => thm RS meta_eq_to_obj_eq) (set_defs_of_bnf bnf)) Jbnfs); |
2318 fun mk_Jsetss As = map2 (fn mk => fn Jsets => map (mk deads As) Jsets) mk_Jt_Ds Jsetss; |
2690 |
2319 val Jbds = map2 (fn mk => mk deads passiveAs) mk_Jt_Ds Jbds_Ds; |
2691 val timer = time (timer "registered new codatatypes as BNFs"); |
2320 val Jwitss = |
2692 |
2321 map2 (fn mk => fn Jwits => map (mk deads passiveAs o snd) Jwits) mk_Jt_Ds Jwitss_Ds; |
2693 val dtor_set_incl_thmss = map (map fold_sets) hset_dtor_incl_thmss; |
2322 fun mk_Jrels As Bs = map (fn mk => mk deads As Bs) mk_Jrels_Ds; |
2694 val dtor_set_set_incl_thmsss = map (map (map fold_sets)) hset_hset_dtor_incl_thmsss; |
2323 |
2695 val dtor_set_induct_thms = map fold_sets dtor_hset_induct_thms; |
2324 val Jmaps = mk_Jmaps passiveAs passiveBs; |
2696 |
2325 val fs_Jmaps = map (fn m => Term.list_comb (m, fs)) Jmaps; |
2697 val Jrels = map (mk_rel_of_bnf deads passiveAs passiveBs) Jbnfs; |
2326 val fs_copy_Jmaps = map (fn m => Term.list_comb (m, fs_copy)) Jmaps; |
2698 |
2327 val gs_Jmaps = map (fn m => Term.list_comb (m, gs)) (mk_Jmaps passiveBs passiveCs); |
2699 val Jrelphis = map (fn Jrel => Term.list_comb (Jrel, Jphis)) Jrels; |
2328 val fgs_Jmaps = map (fn m => Term.list_comb (m, map2 (curry HOLogic.mk_comp) gs fs)) |
|
2329 (mk_Jmaps passiveAs passiveCs); |
|
2330 val (Jsetss_by_range, Jsetss_by_bnf) = `transpose (mk_Jsetss passiveAs); |
|
2331 |
|
2332 val timer = time (timer "bnf constants for the new datatypes"); |
|
2333 |
|
2334 val (dtor_Jmap_thms, Jmap_thms) = |
|
2335 let |
|
2336 fun mk_goal fs_Jmap map dtor dtor' = fold_rev Logic.all fs |
|
2337 (mk_Trueprop_eq (HOLogic.mk_comp (dtor', fs_Jmap), |
|
2338 HOLogic.mk_comp (Term.list_comb (map, fs @ fs_Jmaps), dtor))); |
|
2339 val goals = map4 mk_goal fs_Jmaps map_FTFT's dtors dtor's; |
|
2340 val cTs = map (SOME o certifyT lthy) FTs'; |
|
2341 val maps = |
|
2342 map5 (fn goal => fn cT => fn unfold => fn map_comp => fn map_cong0 => |
|
2343 Goal.prove_sorry lthy [] [] goal |
|
2344 (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jmap_defs THEN |
|
2345 mk_map_tac m n cT unfold map_comp map_cong0) |
|
2346 |> Thm.close_derivation) |
|
2347 goals cTs dtor_unfold_thms map_comps map_cong0s; |
|
2348 in |
|
2349 map_split (fn thm => (thm RS @{thm comp_eq_dest}, thm)) maps |
|
2350 end; |
|
2351 |
|
2352 val dtor_Jmap_unique_thm = |
|
2353 let |
|
2354 fun mk_prem u map dtor dtor' = |
|
2355 mk_Trueprop_eq (HOLogic.mk_comp (dtor', u), |
|
2356 HOLogic.mk_comp (Term.list_comb (map, fs @ us), dtor)); |
|
2357 val prems = map4 mk_prem us map_FTFT's dtors dtor's; |
|
2358 val goal = |
|
2359 HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj |
|
2360 (map2 (curry HOLogic.mk_eq) us fs_Jmaps)); |
|
2361 in |
|
2362 Goal.prove_sorry lthy [] [] |
|
2363 (fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal))) |
|
2364 (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jmap_defs THEN |
|
2365 mk_dtor_map_unique_tac dtor_unfold_unique_thm sym_map_comps ctxt) |
|
2366 |> Thm.close_derivation |
|
2367 end; |
|
2368 |
|
2369 val Jmap_comp0_thms = |
|
2370 let |
|
2371 val goal = fold_rev Logic.all (fs @ gs) |
|
2372 (HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj |
|
2373 (map3 (fn fmap => fn gmap => fn fgmap => |
|
2374 HOLogic.mk_eq (HOLogic.mk_comp (gmap, fmap), fgmap)) |
|
2375 fs_Jmaps gs_Jmaps fgs_Jmaps))) |
|
2376 in |
|
2377 split_conj_thm (Goal.prove_sorry lthy [] [] goal |
|
2378 (K (mk_map_comp0_tac Jmap_thms map_comp0s dtor_Jmap_unique_thm)) |
|
2379 |> Thm.close_derivation) |
|
2380 end; |
|
2381 |
|
2382 val timer = time (timer "map functions for the new codatatypes"); |
|
2383 |
|
2384 val (dtor_Jset_thmss', dtor_Jset_thmss) = |
|
2385 let |
|
2386 fun mk_simp_goal relate pas_set act_sets sets dtor z set = |
|
2387 relate (set $ z, mk_union (pas_set $ (dtor $ z), |
|
2388 Library.foldl1 mk_union |
|
2389 (map2 (fn X => mk_UNION (X $ (dtor $ z))) act_sets sets))); |
|
2390 fun mk_goals eq = |
|
2391 map2 (fn i => fn sets => |
|
2392 map4 (fn Fsets => |
|
2393 mk_simp_goal eq (nth Fsets (i - 1)) (drop m Fsets) sets) |
|
2394 FTs_setss dtors Jzs sets) |
|
2395 ls Jsetss_by_range; |
|
2396 |
|
2397 val le_goals = map |
|
2398 (fold_rev Logic.all Jzs o HOLogic.mk_Trueprop o Library.foldr1 HOLogic.mk_conj) |
|
2399 (mk_goals (uncurry mk_leq)); |
|
2400 val set_le_thmss = map split_conj_thm |
|
2401 (map4 (fn goal => fn hset_minimal => fn set_hsets => fn set_hset_hsetss => |
|
2402 Goal.prove_sorry lthy [] [] goal |
|
2403 (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN |
|
2404 mk_set_le_tac n hset_minimal set_hsets set_hset_hsetss) |
|
2405 |> Thm.close_derivation) |
|
2406 le_goals hset_minimal_thms set_hset_thmss' set_hset_hset_thmsss'); |
|
2407 |
|
2408 val ge_goalss = map (map2 (fn z => fn goal => |
|
2409 Logic.all z (HOLogic.mk_Trueprop goal)) Jzs) |
|
2410 (mk_goals (uncurry mk_leq o swap)); |
|
2411 val set_ge_thmss = |
|
2412 map3 (map3 (fn goal => fn set_incl_hset => fn set_hset_incl_hsets => |
|
2413 Goal.prove_sorry lthy [] [] goal |
|
2414 (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN |
|
2415 mk_set_ge_tac n set_incl_hset set_hset_incl_hsets) |
|
2416 |> Thm.close_derivation)) |
|
2417 ge_goalss set_incl_hset_thmss' set_hset_incl_hset_thmsss' |
|
2418 in |
|
2419 map2 (map2 (fn le => fn ge => equalityI OF [le, ge])) set_le_thmss set_ge_thmss |
|
2420 |> `transpose |
|
2421 end; |
|
2422 |
|
2423 val timer = time (timer "set functions for the new codatatypes"); |
|
2424 |
|
2425 val colss = map2 (fn j => fn T => |
|
2426 map (fn i => mk_hset_rec dtors nat i j T) ks) ls passiveAs; |
|
2427 val colss' = map2 (fn j => fn T => |
|
2428 map (fn i => mk_hset_rec dtor's nat i j T) ks) ls passiveBs; |
|
2429 |
|
2430 val col_natural_thmss = |
|
2431 let |
|
2432 fun mk_col_natural f map z col col' = |
|
2433 HOLogic.mk_eq (mk_image f $ (col $ z), col' $ (map $ z)); |
|
2434 |
|
2435 fun mk_goal f cols cols' = list_all_free Jzs (Library.foldr1 HOLogic.mk_conj |
|
2436 (map4 (mk_col_natural f) fs_Jmaps Jzs cols cols')); |
|
2437 |
|
2438 val goals = map3 mk_goal fs colss colss'; |
|
2439 |
|
2440 val ctss = |
|
2441 map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat]) goals; |
|
2442 |
|
2443 val thms = |
|
2444 map4 (fn goal => fn cts => fn rec_0s => fn rec_Sucs => |
|
2445 singleton (Proof_Context.export names_lthy lthy) |
|
2446 (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal) |
|
2447 (mk_col_natural_tac cts rec_0s rec_Sucs dtor_Jmap_thms set_mapss)) |
|
2448 |> Thm.close_derivation) |
|
2449 goals ctss hset_rec_0ss' hset_rec_Sucss'; |
|
2450 in |
|
2451 map (split_conj_thm o mk_specN n) thms |
|
2452 end; |
|
2453 |
|
2454 val col_bd_thmss = |
|
2455 let |
|
2456 fun mk_col_bd z col bd = mk_ordLeq (mk_card_of (col $ z)) bd; |
|
2457 |
|
2458 fun mk_goal bds cols = list_all_free Jzs (Library.foldr1 HOLogic.mk_conj |
|
2459 (map3 mk_col_bd Jzs cols bds)); |
|
2460 |
|
2461 val goals = map (mk_goal Jbds) colss; |
|
2462 |
|
2463 val ctss = map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat]) |
|
2464 (map (mk_goal (replicate n sbd)) colss); |
|
2465 |
|
2466 val thms = |
|
2467 map5 (fn j => fn goal => fn cts => fn rec_0s => fn rec_Sucs => |
|
2468 singleton (Proof_Context.export names_lthy lthy) |
|
2469 (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal) |
|
2470 (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jbd_defs THEN |
|
2471 mk_col_bd_tac m j cts rec_0s rec_Sucs sbd_Card_order sbd_Cinfinite set_sbdss)) |
|
2472 |> Thm.close_derivation) |
|
2473 ls goals ctss hset_rec_0ss' hset_rec_Sucss'; |
|
2474 in |
|
2475 map (split_conj_thm o mk_specN n) thms |
|
2476 end; |
|
2477 |
|
2478 val map_cong0_thms = |
|
2479 let |
|
2480 val cTs = map (SOME o certifyT lthy o |
|
2481 Term.typ_subst_atomic (passiveAs ~~ passiveBs) o TFree) coinduct_params; |
|
2482 |
|
2483 fun mk_prem z set f g y y' = |
|
2484 mk_Ball (set $ z) (Term.absfree y' (HOLogic.mk_eq (f $ y, g $ y))); |
|
2485 |
|
2486 fun mk_prems sets z = |
|
2487 Library.foldr1 HOLogic.mk_conj (map5 (mk_prem z) sets fs fs_copy ys ys') |
|
2488 |
|
2489 fun mk_map_cong0 sets z fmap gmap = |
|
2490 HOLogic.mk_imp (mk_prems sets z, HOLogic.mk_eq (fmap $ z, gmap $ z)); |
|
2491 |
|
2492 fun mk_coind_body sets (x, T) z fmap gmap y y_copy = |
|
2493 HOLogic.mk_conj |
|
2494 (HOLogic.mk_mem (z, HOLogic.mk_Collect (x, T, mk_prems sets z)), |
|
2495 HOLogic.mk_conj (HOLogic.mk_eq (y, fmap $ z), |
|
2496 HOLogic.mk_eq (y_copy, gmap $ z))) |
|
2497 |
|
2498 fun mk_cphi sets (z' as (x, T)) z fmap gmap y' y y'_copy y_copy = |
|
2499 HOLogic.mk_exists (x, T, mk_coind_body sets z' z fmap gmap y y_copy) |
|
2500 |> Term.absfree y'_copy |
|
2501 |> Term.absfree y' |
|
2502 |> certify lthy; |
|
2503 |
|
2504 val cphis = map9 mk_cphi |
|
2505 Jsetss_by_bnf Jzs' Jzs fs_Jmaps fs_copy_Jmaps Jys' Jys Jys'_copy Jys_copy; |
|
2506 |
|
2507 val coinduct = unfold_thms lthy Jset_defs |
|
2508 (Drule.instantiate' cTs (map SOME cphis) dtor_map_coinduct_thm); |
|
2509 |
|
2510 val goal = |
|
2511 HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj |
|
2512 (map4 mk_map_cong0 Jsetss_by_bnf Jzs fs_Jmaps fs_copy_Jmaps)); |
|
2513 |
|
2514 val thm = singleton (Proof_Context.export names_lthy lthy) |
|
2515 (Goal.prove_sorry lthy [] [] goal |
|
2516 (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN |
|
2517 mk_mcong_tac lthy m (rtac coinduct) map_comps dtor_Jmap_thms map_cong0s |
|
2518 set_mapss set_hset_thmss set_hset_hset_thmsss)) |
|
2519 |> Thm.close_derivation |
|
2520 in |
|
2521 split_conj_thm thm |
|
2522 end; |
|
2523 |
|
2524 val in_Jrels = map (fn def => trans OF [def, @{thm OO_Grp_alt}] RS @{thm predicate2_eqD}) |
|
2525 Jrel_unabs_defs; |
|
2526 |
|
2527 val fold_Jsets = fold_thms lthy Jset_unabs_defs; |
|
2528 val dtor_Jset_incl_thmss = map (map fold_Jsets) hset_dtor_incl_thmss; |
|
2529 val dtor_set_Jset_incl_thmsss = map (map (map fold_Jsets)) hset_hset_dtor_incl_thmsss; |
|
2530 val dtor_Jset_induct_thms = map fold_Jsets dtor_hset_induct_thms; |
|
2531 val Jwit_thmss = map (map fold_Jsets) wit_thmss; |
|
2532 |
|
2533 val Jrels = mk_Jrels passiveAs passiveBs; |
|
2534 val Jrelphis = map (fn rel => Term.list_comb (rel, Jphis)) Jrels; |
2700 val relphis = map (fn rel => Term.list_comb (rel, Jphis @ Jrelphis)) rels; |
2535 val relphis = map (fn rel => Term.list_comb (rel, Jphis @ Jrelphis)) rels; |
2701 val in_Jrels = map in_rel_of_bnf Jbnfs; |
2536 val Jrelpsi1s = map (fn rel => Term.list_comb (rel, Jpsi1s)) (mk_Jrels passiveAs passiveCs); |
2702 |
2537 val Jrelpsi2s = map (fn rel => Term.list_comb (rel, Jpsi2s)) (mk_Jrels passiveCs passiveBs); |
2703 val folded_dtor_map_thms = map fold_maps dtor_map_thms; |
2538 val Jrelpsi12s = map (fn rel => |
2704 val folded_dtor_map_o_thms = map fold_maps map_thms; |
2539 Term.list_comb (rel, map2 (curry mk_rel_compp) Jpsi1s Jpsi2s)) Jrels; |
2705 val folded_dtor_set_thmss = map (map fold_sets) dtor_set_thmss; |
|
2706 val folded_dtor_set_thmss' = transpose folded_dtor_set_thmss; |
|
2707 |
2540 |
2708 val dtor_Jrel_thms = |
2541 val dtor_Jrel_thms = |
2709 let |
2542 let |
2710 fun mk_goal Jz Jz' dtor dtor' Jrelphi relphi = fold_rev Logic.all (Jz :: Jz' :: Jphis) |
2543 fun mk_goal Jz Jz' dtor dtor' Jrelphi relphi = fold_rev Logic.all (Jz :: Jz' :: Jphis) |
2711 (mk_Trueprop_eq (Jrelphi $ Jz $ Jz', relphi $ (dtor $ Jz) $ (dtor' $ Jz'))); |
2544 (mk_Trueprop_eq (Jrelphi $ Jz $ Jz', relphi $ (dtor $ Jz) $ (dtor' $ Jz'))); |
2843 (fold_rev Logic.all (Jphis @ activeJphis @ zip_zs @ zips) |
2642 (fold_rev Logic.all (Jphis @ activeJphis @ zip_zs @ zips) |
2844 (Logic.list_implies (helper_prems, concl))) |
2643 (Logic.list_implies (helper_prems, concl))) |
2845 (mk_rel_coinduct_ind_tac m ks dtor_unfold_thms set_mapss j set_induct) |
2644 (mk_rel_coinduct_ind_tac m ks dtor_unfold_thms set_mapss j set_induct) |
2846 |> Thm.close_derivation |
2645 |> Thm.close_derivation |
2847 |> split_conj_thm) |
2646 |> split_conj_thm) |
2848 mk_helper_ind_concls ls dtor_set_induct_thms |
2647 mk_helper_ind_concls ls dtor_Jset_induct_thms |
2849 |> transpose; |
2648 |> transpose; |
2850 in |
2649 in |
2851 mk_rel_coinduct_tac in_rels in_Jrels |
2650 mk_rel_coinduct_tac in_rels in_Jrels |
2852 helper_ind_thmss helper_coind1_thms helper_coind2_thms |
2651 helper_ind_thmss helper_coind1_thms helper_coind2_thms |
2853 end; |
2652 end; |
2854 |
2653 |
2855 val Jrels = if m = 0 then map HOLogic.eq_const Ts |
|
2856 else map (mk_rel_of_bnf deads passiveAs passiveBs) Jbnfs; |
|
2857 val Jrel_coinduct_thm = |
2654 val Jrel_coinduct_thm = |
2858 mk_rel_xtor_co_induct_thm Greatest_FP rels activeJphis Jrels Jphis Jzs Jz's dtors dtor's |
2655 mk_rel_xtor_co_induct_thm Greatest_FP rels activeJphis Jrels Jphis Jzs Jz's dtors dtor's |
2859 Jrel_coinduct_tac lthy; |
2656 Jrel_coinduct_tac lthy; |
2860 |
2657 |
|
2658 val le_Jrel_OO_thm = |
|
2659 let |
|
2660 fun mk_le_Jrel_OO Jrelpsi1 Jrelpsi2 Jrelpsi12 = |
|
2661 mk_leq (mk_rel_compp (Jrelpsi1, Jrelpsi2)) Jrelpsi12; |
|
2662 val goals = map3 mk_le_Jrel_OO Jrelpsi1s Jrelpsi2s Jrelpsi12s; |
|
2663 |
|
2664 val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj goals); |
|
2665 in |
|
2666 singleton (Proof_Context.export names_lthy lthy) |
|
2667 (Goal.prove_sorry lthy [] [] goal |
|
2668 (K (mk_le_rel_OO_tac Jrel_coinduct_thm dtor_Jrel_thms rel_OOs))) |
|
2669 |> Thm.close_derivation |
|
2670 end; |
|
2671 |
|
2672 val timer = time (timer "helpers for BNF properties"); |
|
2673 |
|
2674 val map_id0_tacs = |
|
2675 map2 (K oo mk_map_id0_tac Jmap_thms) dtor_unfold_unique_thms unfold_dtor_thms; |
|
2676 val map_comp0_tacs = map (fn thm => K (rtac (thm RS sym) 1)) Jmap_comp0_thms; |
|
2677 val map_cong0_tacs = map (mk_map_cong0_tac m) map_cong0_thms; |
|
2678 val set_nat_tacss = |
|
2679 map2 (map2 (fn def => fn col => fn {context = ctxt, prems = _} => |
|
2680 unfold_thms_tac ctxt Jset_defs THEN mk_set_map0_tac def col)) |
|
2681 hset_defss (transpose col_natural_thmss); |
|
2682 |
|
2683 val Jbd_card_orders = map (fn def => fold_thms lthy [def] sbd_card_order) Jbd_defs; |
|
2684 val Jbd_Cinfinites = map (fn def => fold_thms lthy [def] sbd_Cinfinite) Jbd_defs; |
|
2685 |
|
2686 val bd_co_tacs = map (fn thm => K (rtac thm 1)) Jbd_card_orders; |
|
2687 val bd_cinf_tacs = map (fn thm => K (rtac (thm RS conjunct1) 1)) Jbd_Cinfinites; |
|
2688 |
|
2689 val set_bd_tacss = |
|
2690 map3 (fn Cinf => map2 (fn def => fn col => fn {context = ctxt, prems = _} => |
|
2691 unfold_thms_tac ctxt Jset_defs THEN mk_set_bd_tac Cinf def col)) |
|
2692 Jbd_Cinfinites hset_defss (transpose col_bd_thmss); |
|
2693 |
|
2694 val le_rel_OO_tacs = map (fn i => K (rtac (le_Jrel_OO_thm RS mk_conjunctN n i) 1)) ks; |
|
2695 |
|
2696 val rel_OO_Grp_tacs = map (fn def => K (rtac def 1)) Jrel_unabs_defs; |
|
2697 |
|
2698 val tacss = map9 zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_nat_tacss |
|
2699 bd_co_tacs bd_cinf_tacs set_bd_tacss le_rel_OO_tacs rel_OO_Grp_tacs; |
|
2700 |
|
2701 fun wit_tac thms {context = ctxt, prems = _} = unfold_thms_tac ctxt (flat Jwit_defss) THEN |
|
2702 mk_wit_tac n dtor_ctor_thms (flat dtor_Jset_thmss) (maps wit_thms_of_bnf bnfs) thms ctxt; |
|
2703 |
|
2704 val (Jbnfs, lthy) = |
|
2705 fold_map6 (fn tacs => fn map_b => fn rel_b => fn set_bs => fn Jwit_thms => fn consts => |
|
2706 fn lthy => |
|
2707 bnf_def Do_Inline (user_policy Note_Some) I tacs (wit_tac Jwit_thms) (SOME deads) |
|
2708 map_b rel_b set_bs consts lthy |
|
2709 |> register_bnf (Local_Theory.full_name lthy b)) |
|
2710 tacss map_bs rel_bs set_bss Jwit_thmss |
|
2711 ((((((bs ~~ Ts) ~~ Jmaps) ~~ Jsetss_by_bnf) ~~ Jbds) ~~ Jwitss) ~~ map SOME Jrels) |
|
2712 lthy; |
|
2713 |
|
2714 val timer = time (timer "registered new codatatypes as BNFs"); |
|
2715 |
|
2716 val ls' = if m = 1 then [0] else ls; |
|
2717 |
|
2718 val Jbnf_common_notes = |
|
2719 [(dtor_map_uniqueN, [dtor_Jmap_unique_thm])] @ |
|
2720 map2 (fn i => fn thm => (mk_dtor_set_inductN i, [thm])) ls' dtor_Jset_induct_thms |
|
2721 |> map (fn (thmN, thms) => |
|
2722 ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); |
|
2723 |
|
2724 val Jbnf_notes = |
|
2725 [(dtor_mapN, map single dtor_Jmap_thms), |
|
2726 (dtor_relN, map single dtor_Jrel_thms), |
|
2727 (dtor_set_inclN, dtor_Jset_incl_thmss), |
|
2728 (dtor_set_set_inclN, map flat dtor_set_Jset_incl_thmsss)] @ |
|
2729 map2 (fn i => fn thms => (mk_dtor_setN i, map single thms)) ls' dtor_Jset_thmss |
|
2730 |> maps (fn (thmN, thmss) => |
|
2731 map2 (fn b => fn thms => |
|
2732 ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) |
|
2733 bs thmss) |
|
2734 in |
|
2735 (timer, Jbnfs, (Jmap_thms, dtor_Jmap_thms), dtor_Jset_thmss', |
|
2736 dtor_Jrel_thms, Jrel_coinduct_thm, Jbnf_common_notes @ Jbnf_notes, lthy) |
|
2737 end; |
|
2738 |
|
2739 val dtor_unfold_o_Jmap_thms = mk_xtor_un_fold_o_map_thms Greatest_FP false m |
|
2740 dtor_unfold_unique_thm dtor_Jmap_o_thms (map (mk_pointfree lthy) dtor_unfold_thms) |
|
2741 sym_map_comps map_cong0s; |
|
2742 val dtor_corec_o_Jmap_thms = mk_xtor_un_fold_o_map_thms Greatest_FP true m |
|
2743 dtor_corec_unique_thm dtor_Jmap_o_thms (map (mk_pointfree lthy) dtor_corec_thms) |
|
2744 sym_map_comps map_cong0s; |
|
2745 |
2861 val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs; |
2746 val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs; |
|
2747 |
2862 val dtor_unfold_transfer_thms = |
2748 val dtor_unfold_transfer_thms = |
2863 mk_un_fold_transfer_thms Greatest_FP rels activephis Jrels Jphis |
2749 mk_un_fold_transfer_thms Greatest_FP rels activephis |
|
2750 (if m = 0 then map HOLogic.eq_const Ts |
|
2751 else map (mk_rel_of_bnf deads passiveAs passiveBs) Jbnfs) Jphis |
2864 (mk_unfolds passiveAs activeAs) (mk_unfolds passiveBs activeBs) |
2752 (mk_unfolds passiveAs activeAs) (mk_unfolds passiveBs activeBs) |
2865 (mk_unfold_transfer_tac m Jrel_coinduct_thm (map map_transfer_of_bnf bnfs) |
2753 (mk_unfold_transfer_tac m Jrel_coinduct_thm (map map_transfer_of_bnf bnfs) |
2866 dtor_unfold_thms) |
2754 dtor_unfold_thms) |
2867 lthy; |
2755 lthy; |
2868 |
2756 |