equal
deleted
inserted
replaced
54 rtac induct THEN_ALL_NEW |
54 rtac induct THEN_ALL_NEW |
55 simp_tac (HOL_basic_ss addsimps eq_iff) THEN_ALL_NEW |
55 simp_tac (HOL_basic_ss addsimps eq_iff) THEN_ALL_NEW |
56 split_conj_tac THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]} |
56 split_conj_tac THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]} |
57 THEN_ALL_NEW split_conj_tac THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps |
57 THEN_ALL_NEW split_conj_tac THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps |
58 @{thms alphas fresh_star_def fresh_zero_perm permute_zero ball_triv |
58 @{thms alphas fresh_star_def fresh_zero_perm permute_zero ball_triv |
59 add_0_left supp_zero_perm Int_empty_left split_conv}) |
59 add_0_left supp_zero_perm Int_empty_left split_conv prod_rel.simps}) |
60 *} |
60 *} |
61 |
61 |
62 ML {* |
62 ML {* |
63 fun build_alpha_refl fv_alphas_lst alphas induct eq_iff ctxt = |
63 fun build_alpha_refl fv_alphas_lst alphas induct eq_iff ctxt = |
64 let |
64 let |
289 in the type and chooses this supp_abs. Additionally single atoms are |
289 in the type and chooses this supp_abs. Additionally single atoms are |
290 treated properly. *) |
290 treated properly. *) |
291 ML {* |
291 ML {* |
292 fun choose_alpha_abs eqiff = |
292 fun choose_alpha_abs eqiff = |
293 let |
293 let |
294 fun exists_subterms f ts = true mem (map (exists_subterm f) ts); |
294 fun exists_subterms f ts = member (op =) (map (exists_subterm f) ts) true; |
295 val terms = map prop_of eqiff; |
295 val terms = map prop_of eqiff; |
296 fun check cname = exists_subterms (fn x => fst(dest_Const x) = cname handle _ => false) terms |
296 fun check cname = exists_subterms (fn x => fst(dest_Const x) = cname handle _ => false) terms |
297 val no = |
297 val no = |
298 if check @{const_name alpha_lst} then 2 else |
298 if check @{const_name alpha_lst} then 2 else |
299 if check @{const_name alpha_res} then 1 else |
299 if check @{const_name alpha_res} then 1 else |