230 val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3c) = |
230 val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3c) = |
231 define_raw_fvs raw_dt_names raw_tys raw_cns_info raw_bn_info raw_bclauses |
231 define_raw_fvs raw_dt_names raw_tys raw_cns_info raw_bn_info raw_bclauses |
232 (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3b |
232 (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3b |
233 |
233 |
234 val _ = trace_msg (K "Defining alpha relations...") |
234 val _ = trace_msg (K "Defining alpha relations...") |
235 val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy4) = |
235 val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, alpha_result, lthy4) = |
236 define_raw_alpha raw_dt_names raw_tys raw_cns_info raw_bn_info raw_bclauses raw_fvs lthy3c |
236 define_raw_alpha raw_dt_names raw_tys raw_cns_info raw_bn_info raw_bclauses raw_fvs lthy3c |
237 |
237 |
238 val _ = tracing ("alpha_induct\n" ^ Syntax.string_of_term lthy3c (prop_of alpha_induct)) |
238 val _ = tracing ("alpha_induct\n" ^ Syntax.string_of_term lthy3c (prop_of alpha_induct)) |
239 val _ = tracing ("alpha_intros\n" ^ cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_intros)) |
239 val _ = tracing ("alpha_intros\n" ^ cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_intros)) |
240 |
240 |
241 val alpha_tys = map (domain_type o fastype_of) alpha_trms |
241 val alpha_tys = map (domain_type o fastype_of) alpha_trms |
242 |
242 |
243 val _ = trace_msg (K "Proving distinct theorems...") |
243 val _ = trace_msg (K "Proving distinct theorems...") |
244 val alpha_distincts = |
244 val alpha_distincts = |
245 raw_prove_alpha_distincts lthy4 alpha_cases raw_distinct_thms alpha_trms raw_dt_names |
245 raw_prove_alpha_distincts lthy4 alpha_result raw_distinct_thms raw_dt_names |
246 |
246 |
247 val _ = trace_msg (K "Proving eq-iff theorems...") |
247 val _ = trace_msg (K "Proving eq-iff theorems...") |
248 val alpha_eq_iff = |
248 val alpha_eq_iff = raw_prove_alpha_eq_iff lthy4 alpha_result raw_distinct_thms raw_inject_thms |
249 raw_prove_alpha_eq_iff lthy4 alpha_intros raw_distinct_thms raw_inject_thms alpha_cases |
|
250 |
249 |
251 val _ = trace_msg (K "Proving equivariance of bns, fvs, size and alpha...") |
250 val _ = trace_msg (K "Proving equivariance of bns, fvs, size and alpha...") |
252 val raw_bn_eqvt = |
251 val raw_bn_eqvt = |
253 raw_prove_eqvt raw_bns raw_bn_inducts (raw_bn_defs @ raw_perm_simps) lthy4 |
252 raw_prove_eqvt raw_bns raw_bn_inducts (raw_bn_defs @ raw_perm_simps) lthy4 |
254 |
253 |
271 Nominal_Eqvt.raw_equivariance (alpha_trms @ alpha_bn_trms) alpha_induct alpha_intros lthy5 |
270 Nominal_Eqvt.raw_equivariance (alpha_trms @ alpha_bn_trms) alpha_induct alpha_intros lthy5 |
272 |
271 |
273 val alpha_eqvt_norm = map (Nominal_ThmDecls.eqvt_transform lthy5) alpha_eqvt |
272 val alpha_eqvt_norm = map (Nominal_ThmDecls.eqvt_transform lthy5) alpha_eqvt |
274 |
273 |
275 val _ = trace_msg (K "Proving equivalence of alpha...") |
274 val _ = trace_msg (K "Proving equivalence of alpha...") |
276 val alpha_refl_thms = |
275 val alpha_refl_thms = raw_prove_refl lthy5 alpha_result raw_induct_thm |
277 raw_prove_refl alpha_trms alpha_bn_trms alpha_intros raw_induct_thm lthy5 |
276 val alpha_sym_thms = raw_prove_sym lthy5 alpha_result alpha_eqvt_norm |
278 |
277 val alpha_trans_thms = |
279 val alpha_sym_thms = |
278 raw_prove_trans lthy5 alpha_result (raw_distinct_thms @ raw_inject_thms) alpha_eqvt_norm |
280 raw_prove_sym (alpha_trms @ alpha_bn_trms) alpha_intros alpha_induct alpha_eqvt_norm lthy5 |
|
281 |
|
282 val alpha_trans_thms = |
|
283 raw_prove_trans (alpha_trms @ alpha_bn_trms) (raw_distinct_thms @ raw_inject_thms) |
|
284 alpha_intros alpha_induct alpha_cases alpha_eqvt_norm lthy5 |
|
285 |
279 |
286 val (alpha_equivp_thms, alpha_bn_equivp_thms) = |
280 val (alpha_equivp_thms, alpha_bn_equivp_thms) = |
287 raw_prove_equivp alpha_trms alpha_bn_trms alpha_refl_thms alpha_sym_thms |
281 raw_prove_equivp lthy5 alpha_result alpha_refl_thms alpha_sym_thms alpha_trans_thms |
288 alpha_trans_thms lthy5 |
|
289 |
282 |
290 val _ = trace_msg (K "Proving alpha implies bn...") |
283 val _ = trace_msg (K "Proving alpha implies bn...") |
291 val alpha_bn_imp_thms = |
284 val alpha_bn_imp_thms = |
292 raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy5 |
285 raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy5 |
293 |
286 |