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 lemma alpha_gen_atom_sym: |
|
120 assumes a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
|
121 shows "\<exists>pi. (aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s) \<Longrightarrow> |
|
122 \<exists>pi. (ab, s) \<approx>gen R f pi (aa, t)" |
|
123 apply(erule exE) |
|
124 apply(rule_tac x="- pi" in exI) |
|
125 apply(simp add: alpha_gen.simps) |
|
126 apply(erule conjE)+ |
|
127 apply(rule conjI) |
|
128 apply(simp add: fresh_star_def fresh_minus_perm) |
|
129 apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))") |
|
130 apply simp |
|
131 apply(rule a) |
|
132 apply assumption |
|
133 done |
|
134 |
|
135 |
119 prove alpha1_reflp_aux: {* (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}]) *} |
136 prove alpha1_reflp_aux: {* (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}]) *} |
120 apply (tactic {* |
137 apply (tactic {* |
121 (indtac @{thm rtrm1_bp.induct} ["x", "x"] THEN_ALL_NEW |
138 (indtac @{thm rtrm1_bp.induct} ["x", "x"] THEN_ALL_NEW |
122 asm_full_simp_tac (HOL_ss addsimps @{thms alpha1_inj}) THEN_ALL_NEW |
139 asm_full_simp_tac (HOL_ss addsimps @{thms alpha1_inj}) THEN_ALL_NEW |
123 TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW |
140 TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW |
124 rtac @{thm exI[of _ "0 :: perm"]} THEN_ALL_NEW |
141 rtac @{thm exI[of _ "0 :: perm"]} THEN_ALL_NEW |
125 asm_full_simp_tac (HOL_ss addsimps @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv}) |
142 asm_full_simp_tac (HOL_ss addsimps @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv}) |
|
143 ) 1 *}) |
|
144 apply (tactic {* |
|
145 (rtac @{thm alpha_rtrm1_alpha_bp.induct} THEN_ALL_NEW |
|
146 asm_full_simp_tac (HOL_ss addsimps @{thms alpha1_inj}) THEN_ALL_NEW |
|
147 TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW |
|
148 (rtac @{thm alpha_gen_atom_sym} THEN' RANGE [ |
|
149 (asm_full_simp_tac (HOL_ss addsimps @{thms alpha1_eqvt})), atac |
|
150 ]) |
126 ) 1 *}) |
151 ) 1 *}) |
127 done |
152 done |
128 |
153 |
129 lemma alpha1_reflp: |
154 lemma alpha1_reflp: |
130 "reflp alpha_rtrm1" |
155 "reflp alpha_rtrm1" |