114 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
114 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
115 apply(simp add: atom_eqvt fv_rtrm1_eqvt Diff_eqvt bv1_eqvt) |
115 apply(simp add: atom_eqvt fv_rtrm1_eqvt Diff_eqvt bv1_eqvt) |
116 apply(simp add: permute_eqvt[symmetric]) |
116 apply(simp add: permute_eqvt[symmetric]) |
117 done |
117 done |
118 |
118 |
119 prove alpha1_reflp_aux: {* fst (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}]) *} |
119 ML {* |
120 by (tactic {* |
120 fun reflp_tac induct inj = |
121 |
121 rtac induct THEN_ALL_NEW |
122 (indtac @{thm rtrm1_bp.induct} ["x", "x"] THEN_ALL_NEW |
122 asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW |
123 asm_full_simp_tac (HOL_ss addsimps @{thms alpha1_inj}) THEN_ALL_NEW |
|
124 TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW |
123 TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW |
125 (rtac @{thm exI[of _ "0 :: perm"]} THEN' |
124 (rtac @{thm exI[of _ "0 :: perm"]} THEN' |
126 asm_full_simp_tac (HOL_ss addsimps @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv})) |
125 asm_full_simp_tac (HOL_ss addsimps |
127 ) 1 *}) |
126 @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv})) |
|
127 *} |
|
128 |
|
129 prove alpha1_reflp_aux: {* fst (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}]) *} |
|
130 by (tactic {* reflp_tac @{thm rtrm1_bp.induct} @{thms alpha1_inj} 1 *}) |
|
131 |
|
132 ML {* |
|
133 fun symp_tac induct inj = |
|
134 rtac induct THEN_ALL_NEW |
|
135 asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW |
|
136 TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW |
|
137 (etac @{thm alpha_gen_compose_sym} THEN' |
|
138 asm_full_simp_tac (HOL_ss addsimps @{thms alpha1_eqvt})) |
|
139 *} |
128 |
140 |
129 prove alpha1_symp_aux: {* (fst o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}]) *} |
141 prove alpha1_symp_aux: {* (fst o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}]) *} |
130 by (tactic {* |
142 by (tactic {* symp_tac @{thm alpha_rtrm1_alpha_bp.induct} @{thms alpha1_inj} 1 *}) |
131 (rtac @{thm alpha_rtrm1_alpha_bp.induct} THEN_ALL_NEW |
|
132 asm_full_simp_tac (HOL_ss addsimps @{thms alpha1_inj}) THEN_ALL_NEW |
|
133 TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW |
|
134 (etac @{thm alpha_gen_compose_sym} THEN' |
|
135 asm_full_simp_tac (HOL_ss addsimps @{thms alpha1_eqvt}) |
|
136 )) 1 *}) |
|
137 |
143 |
138 prove alpha1_transp_aux: {* (snd o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}]) *} |
144 prove alpha1_transp_aux: {* (snd o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}]) *} |
139 apply (rule alpha_rtrm1_alpha_bp.induct) |
145 apply (rule alpha_rtrm1_alpha_bp.induct) |
140 apply simp_all |
146 apply simp_all |
141 apply (rule_tac [!] allI) |
147 apply (rule_tac [!] allI) |