equal
deleted
inserted
replaced
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 b: "\<exists>pi. (aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)" |
|
121 and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
|
122 shows "\<exists>pi. (ab, s) \<approx>gen R f pi (aa, t)" |
|
123 using b apply - |
|
124 apply(erule exE) |
|
125 apply(rule_tac x="- pi" in exI) |
|
126 apply(simp add: alpha_gen.simps) |
|
127 apply(erule conjE)+ |
|
128 apply(rule conjI) |
|
129 apply(simp add: fresh_star_def fresh_minus_perm) |
|
130 apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))") |
|
131 apply simp |
|
132 apply(rule a) |
|
133 apply assumption |
|
134 done |
|
135 |
|
136 prove alpha1_reflp_aux: {* fst (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}]) *} |
119 prove alpha1_reflp_aux: {* fst (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}]) *} |
137 by (tactic {* |
120 by (tactic {* |
138 |
121 |
139 (indtac @{thm rtrm1_bp.induct} ["x", "x"] THEN_ALL_NEW |
122 (indtac @{thm rtrm1_bp.induct} ["x", "x"] THEN_ALL_NEW |
140 asm_full_simp_tac (HOL_ss addsimps @{thms alpha1_inj}) THEN_ALL_NEW |
123 asm_full_simp_tac (HOL_ss addsimps @{thms alpha1_inj}) THEN_ALL_NEW |
146 prove alpha1_symp_aux: {* (fst o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}]) *} |
129 prove alpha1_symp_aux: {* (fst o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}]) *} |
147 by (tactic {* |
130 by (tactic {* |
148 (rtac @{thm alpha_rtrm1_alpha_bp.induct} THEN_ALL_NEW |
131 (rtac @{thm alpha_rtrm1_alpha_bp.induct} THEN_ALL_NEW |
149 asm_full_simp_tac (HOL_ss addsimps @{thms alpha1_inj}) THEN_ALL_NEW |
132 asm_full_simp_tac (HOL_ss addsimps @{thms alpha1_inj}) THEN_ALL_NEW |
150 TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW |
133 TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW |
151 (etac @{thm alpha_gen_atom_sym} THEN' |
134 (etac @{thm alpha_gen_compose_sym} THEN' |
152 asm_full_simp_tac (HOL_ss addsimps @{thms alpha1_eqvt}) |
135 asm_full_simp_tac (HOL_ss addsimps @{thms alpha1_eqvt}) |
153 )) 1 *}) |
136 )) 1 *}) |
154 |
137 |
155 prove alpha1_transp_aux: {* (snd o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}]) *} |
138 prove alpha1_transp_aux: {* (snd o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}]) *} |
156 apply (rule alpha_rtrm1_alpha_bp.induct) |
139 apply (rule alpha_rtrm1_alpha_bp.induct) |
161 apply (erule alpha_rtrm1.cases) |
144 apply (erule alpha_rtrm1.cases) |
162 apply (simp_all add: alpha1_inj) |
145 apply (simp_all add: alpha1_inj) |
163 apply (rotate_tac 2) |
146 apply (rotate_tac 2) |
164 apply (erule alpha_rtrm1.cases) |
147 apply (erule alpha_rtrm1.cases) |
165 apply (simp_all add: alpha1_inj) |
148 apply (simp_all add: alpha1_inj) |
166 thm alpha_gen_atom_trans |
149 apply (erule alpha_gen_compose_trans) |
167 (*apply (tactic {* |
150 (*apply (tactic {* |
168 (rtac @{thm alpha_rtrm1_alpha_bp.induct} THEN_ALL_NEW |
151 (rtac @{thm alpha_rtrm1_alpha_bp.induct} THEN_ALL_NEW |
169 asm_full_simp_tac (HOL_ss addsimps @{thms alpha1_inj})) 1 *})*) |
152 asm_full_simp_tac (HOL_ss addsimps @{thms alpha1_inj})) 1 *})*) |
170 sorry |
153 sorry |
171 |
154 |