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 prove alpha1_reflp_aux: {* (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}]) *} |
|
120 apply (tactic {* |
|
121 (indtac @{thm rtrm1_bp.induct} ["x", "x"] THEN_ALL_NEW |
|
122 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 |
|
124 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}) |
|
126 ) 1 *}) |
|
127 done |
|
128 |
|
129 lemma alpha1_reflp: |
|
130 "reflp alpha_rtrm1" |
|
131 "reflp alpha_bp" |
|
132 unfolding reflp_def |
|
133 apply (simp_all add: alpha1_reflp_aux) |
|
134 done |
|
135 |
119 lemma alpha1_equivp: "equivp alpha_rtrm1" |
136 lemma alpha1_equivp: "equivp alpha_rtrm1" |
120 sorry |
137 sorry |
|
138 |
121 |
139 |
122 quotient_type trm1 = rtrm1 / alpha_rtrm1 |
140 quotient_type trm1 = rtrm1 / alpha_rtrm1 |
123 by (rule alpha1_equivp) |
141 by (rule alpha1_equivp) |
124 |
142 |
125 local_setup {* |
143 local_setup {* |