133 fun symp_tac induct inj = |
133 fun symp_tac induct inj = |
134 rtac induct THEN_ALL_NEW |
134 rtac induct THEN_ALL_NEW |
135 asm_full_simp_tac (HOL_ss addsimps inj) 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 |
136 TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW |
137 (etac @{thm alpha_gen_compose_sym} THEN' |
137 (etac @{thm alpha_gen_compose_sym} THEN' |
138 asm_full_simp_tac (HOL_ss addsimps @{thms alpha1_eqvt})) |
138 eresolve_tac @{thms alpha1_eqvt}) |
139 *} |
139 *} |
140 |
140 |
141 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}]) *} |
142 by (tactic {* symp_tac @{thm alpha_rtrm1_alpha_bp.induct} @{thms alpha1_inj} 1 *}) |
142 by (tactic {* symp_tac @{thm alpha_rtrm1_alpha_bp.induct} @{thms alpha1_inj} 1 *}) |
143 |
143 |
144 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}]) *} |
145 apply (rule alpha_rtrm1_alpha_bp.induct) |
145 apply (tactic {* |
146 apply simp_all |
146 (rtac @{thm alpha_rtrm1_alpha_bp.induct} THEN_ALL_NEW |
147 apply (rule_tac [!] allI) |
147 (rtac allI THEN' rtac impI THEN' rotate_tac (~1) THEN' |
148 apply (rule_tac [!] impI) |
148 eresolve_tac @{thms alpha_rtrm1.cases alpha_bp.cases}) THEN_ALL_NEW |
149 apply (rotate_tac 4) |
149 ( |
150 apply (erule alpha_rtrm1.cases) |
150 asm_full_simp_tac (HOL_ss addsimps @{thms alpha1_inj rtrm1.distinct rtrm1.inject bp.distinct bp.inject}) THEN' |
151 apply (simp_all add: alpha1_inj) |
151 TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW |
152 apply (rotate_tac 2) |
152 (etac @{thm alpha_gen_compose_trans} THEN' RANGE [atac, eresolve_tac @{thms alpha1_eqvt}]) |
153 apply (erule alpha_rtrm1.cases) |
153 ) |
154 apply (simp_all add: alpha1_inj) |
154 ) 1 *}) |
155 apply (erule alpha_gen_compose_trans) |
155 done |
156 (*apply (tactic {* |
|
157 (rtac @{thm alpha_rtrm1_alpha_bp.induct} THEN_ALL_NEW |
|
158 asm_full_simp_tac (HOL_ss addsimps @{thms alpha1_inj})) 1 *})*) |
|
159 sorry |
|
160 |
156 |
161 lemma helper: "(\<forall>x y z. R x y \<and> R y z \<longrightarrow> R x z) = (\<forall>xa ya. R xa ya \<longrightarrow> (\<forall>z. R ya z \<longrightarrow> R xa z))" |
157 lemma helper: "(\<forall>x y z. R x y \<and> R y z \<longrightarrow> R x z) = (\<forall>xa ya. R xa ya \<longrightarrow> (\<forall>z. R ya z \<longrightarrow> R xa z))" |
162 by meson |
158 by meson |
163 |
159 |
164 lemma alpha1_equivp: |
160 lemma alpha1_equivp: |