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: |
119 lemma alpha_gen_atom_sym: |
120 assumes a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
120 assumes b: "\<exists>pi. (aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)" |
121 shows "\<exists>pi. (aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s) \<Longrightarrow> |
121 and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
122 \<exists>pi. (ab, s) \<approx>gen R f pi (aa, t)" |
122 shows "\<exists>pi. (ab, s) \<approx>gen R f pi (aa, t)" |
|
123 using b apply - |
123 apply(erule exE) |
124 apply(erule exE) |
124 apply(rule_tac x="- pi" in exI) |
125 apply(rule_tac x="- pi" in exI) |
125 apply(simp add: alpha_gen.simps) |
126 apply(simp add: alpha_gen.simps) |
126 apply(erule conjE)+ |
127 apply(erule conjE)+ |
127 apply(rule conjI) |
128 apply(rule conjI) |
130 apply simp |
131 apply simp |
131 apply(rule a) |
132 apply(rule a) |
132 apply assumption |
133 apply assumption |
133 done |
134 done |
134 |
135 |
135 |
136 prove alpha1_reflp_aux: {* fst (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}]) *} |
137 by (tactic {* |
137 apply (tactic {* |
138 |
138 (indtac @{thm rtrm1_bp.induct} ["x", "x"] THEN_ALL_NEW |
139 (indtac @{thm rtrm1_bp.induct} ["x", "x"] THEN_ALL_NEW |
139 asm_full_simp_tac (HOL_ss addsimps @{thms alpha1_inj}) THEN_ALL_NEW |
140 asm_full_simp_tac (HOL_ss addsimps @{thms alpha1_inj}) THEN_ALL_NEW |
140 TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW |
141 TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW |
141 rtac @{thm exI[of _ "0 :: perm"]} THEN_ALL_NEW |
142 (rtac @{thm exI[of _ "0 :: perm"]} THEN' |
142 asm_full_simp_tac (HOL_ss addsimps @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv}) |
143 asm_full_simp_tac (HOL_ss addsimps @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv})) |
143 ) 1 *}) |
144 ) 1 *}) |
144 apply (tactic {* |
145 |
|
146 prove alpha1_symp_aux: {* (fst o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}]) *} |
|
147 by (tactic {* |
145 (rtac @{thm alpha_rtrm1_alpha_bp.induct} THEN_ALL_NEW |
148 (rtac @{thm alpha_rtrm1_alpha_bp.induct} THEN_ALL_NEW |
146 asm_full_simp_tac (HOL_ss addsimps @{thms alpha1_inj}) THEN_ALL_NEW |
149 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 |
150 TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW |
148 (rtac @{thm alpha_gen_atom_sym} THEN' RANGE [ |
151 (etac @{thm alpha_gen_atom_sym} THEN' |
149 (asm_full_simp_tac (HOL_ss addsimps @{thms alpha1_eqvt})), atac |
152 asm_full_simp_tac (HOL_ss addsimps @{thms alpha1_eqvt}) |
150 ]) |
153 )) 1 *}) |
151 ) 1 *}) |
154 |
152 done |
155 prove alpha1_transp_aux: {* (snd o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}]) *} |
153 |
156 apply (rule alpha_rtrm1_alpha_bp.induct) |
154 lemma alpha1_reflp: |
157 apply simp_all |
155 "reflp alpha_rtrm1" |
158 apply (rule_tac [!] allI) |
156 "reflp alpha_bp" |
159 apply (rule_tac [!] impI) |
157 unfolding reflp_def |
160 apply (rotate_tac 4) |
|
161 apply (erule alpha_rtrm1.cases) |
|
162 apply (simp_all add: alpha1_inj) |
|
163 apply (rotate_tac 2) |
|
164 apply (erule alpha_rtrm1.cases) |
|
165 apply (simp_all add: alpha1_inj) |
|
166 thm alpha_gen_atom_trans |
|
167 (*apply (tactic {* |
|
168 (rtac @{thm alpha_rtrm1_alpha_bp.induct} THEN_ALL_NEW |
|
169 asm_full_simp_tac (HOL_ss addsimps @{thms alpha1_inj})) 1 *})*) |
|
170 sorry |
|
171 |
|
172 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))" |
|
173 by meson |
|
174 |
|
175 lemma alpha1_equivp: |
|
176 "equivp alpha_rtrm1" |
|
177 "equivp alpha_bp" |
|
178 unfolding equivp_reflp_symp_transp reflp_def |
158 apply (simp_all add: alpha1_reflp_aux) |
179 apply (simp_all add: alpha1_reflp_aux) |
159 done |
180 unfolding symp_def |
160 |
181 apply (simp_all add: alpha1_symp_aux) |
161 lemma alpha1_equivp: "equivp alpha_rtrm1" |
182 unfolding transp_def |
162 sorry |
183 apply (simp_all only: helper) |
163 |
184 apply (rule allI)+ |
|
185 apply (rule conjunct1[OF alpha1_transp_aux]) |
|
186 apply (rule allI)+ |
|
187 apply (rule conjunct2[OF alpha1_transp_aux]) |
|
188 done |
164 |
189 |
165 quotient_type trm1 = rtrm1 / alpha_rtrm1 |
190 quotient_type trm1 = rtrm1 / alpha_rtrm1 |
166 by (rule alpha1_equivp) |
191 by (rule alpha1_equivp(1)) |
167 |
192 |
168 local_setup {* |
193 local_setup {* |
169 (fn ctxt => ctxt |
194 (fn ctxt => ctxt |
170 |> snd o (Quotient_Def.quotient_lift_const ("Vr1", @{term rVr1})) |
195 |> snd o (Quotient_Def.quotient_lift_const ("Vr1", @{term rVr1})) |
171 |> snd o (Quotient_Def.quotient_lift_const ("Ap1", @{term rAp1})) |
196 |> snd o (Quotient_Def.quotient_lift_const ("Ap1", @{term rAp1})) |
302 apply(simp (no_asm) add: supp_def) |
327 apply(simp (no_asm) add: supp_def) |
303 apply(simp add: alpha1_INJ alpha_bp_eq) |
328 apply(simp add: alpha1_INJ alpha_bp_eq) |
304 apply(simp add: Abs_eq_iff) |
329 apply(simp add: Abs_eq_iff) |
305 apply(simp add: alpha_gen) |
330 apply(simp add: alpha_gen) |
306 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv) |
331 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv) |
307 apply(simp add: Collect_imp_eq Collect_neg_eq fresh_star_def helper) |
332 apply(simp add: Collect_imp_eq Collect_neg_eq fresh_star_def helper2) |
308 apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt) |
333 apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt) |
309 apply(simp (no_asm) add: supp_def eqvts) |
334 apply(simp (no_asm) add: supp_def eqvts) |
310 apply(fold supp_def) |
335 apply(fold supp_def) |
311 apply(simp add: supp_at_base) |
336 apply(simp add: supp_at_base) |
312 apply(simp (no_asm) add: supp_def Collect_imp_eq Collect_neg_eq) |
337 apply(simp (no_asm) add: supp_def Collect_imp_eq Collect_neg_eq) |