118 |
118 |
119 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_equivp}, []), |
119 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_equivp}, []), |
120 (build_equivps [@{term alpha_rtrm1}, @{term alpha_bp}] @{thm rtrm1_bp.induct} @{thm alpha_rtrm1_alpha_bp.induct} @{thms rtrm1.inject bp.inject} @{thms alpha1_inj} @{thms rtrm1.distinct bp.distinct} @{thms alpha_rtrm1.cases alpha_bp.cases} @{thms alpha1_eqvt} ctxt)) ctxt)) *} |
120 (build_equivps [@{term alpha_rtrm1}, @{term alpha_bp}] @{thm rtrm1_bp.induct} @{thm alpha_rtrm1_alpha_bp.induct} @{thms rtrm1.inject bp.inject} @{thms alpha1_inj} @{thms rtrm1.distinct bp.distinct} @{thms alpha_rtrm1.cases alpha_bp.cases} @{thms alpha1_eqvt} ctxt)) ctxt)) *} |
121 thm alpha1_equivp |
121 thm alpha1_equivp |
122 |
122 |
123 (*prove alpha1_reflp_aux: {* fst (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *} |
|
124 by (tactic {* reflp_tac @{thm rtrm1_bp.induct} @{thms alpha1_inj} 1 *}) |
|
125 |
|
126 prove alpha1_symp_aux: {* (fst o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *} |
|
127 by (tactic {* symp_tac @{thm alpha_rtrm1_alpha_bp.induct} @{thms alpha1_inj} @{thms alpha1_eqvt} 1 *}) |
|
128 |
|
129 prove alpha1_transp_aux: {* (snd o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *} |
|
130 by (tactic {* transp_tac @{thm alpha_rtrm1_alpha_bp.induct} @{thms alpha1_inj} @{thms rtrm1.inject bp.inject} @{thms rtrm1.distinct bp.distinct} @{thms alpha_rtrm1.cases alpha_bp.cases} @{thms alpha1_eqvt} 1 *}) |
|
131 |
|
132 lemma alpha1_equivp: |
|
133 "equivp alpha_rtrm1" |
|
134 "equivp alpha_bp" |
|
135 apply (tactic {* |
|
136 (simp_tac (HOL_ss addsimps @{thms equivp_reflp_symp_transp reflp_def symp_def}) |
|
137 THEN' rtac @{thm conjI} THEN' rtac @{thm allI} THEN' |
|
138 resolve_tac (HOLogic.conj_elims @{thm alpha1_reflp_aux}) |
|
139 THEN' rtac @{thm conjI} THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' |
|
140 resolve_tac (HOLogic.conj_elims @{thm alpha1_symp_aux}) THEN' rtac @{thm transp_aux} |
|
141 THEN' resolve_tac (HOLogic.conj_elims @{thm alpha1_transp_aux}) |
|
142 ) |
|
143 1 *}) |
|
144 done*) |
|
145 |
|
146 quotient_type trm1 = rtrm1 / alpha_rtrm1 |
123 quotient_type trm1 = rtrm1 / alpha_rtrm1 |
147 by (rule alpha1_equivp(1)) |
124 by (rule alpha1_equivp(1)) |
148 |
125 |
149 local_setup {* |
126 local_setup {* |
150 (fn ctxt => ctxt |
127 (fn ctxt => ctxt |
225 done |
202 done |
226 |
203 |
227 lemma bp_supp: "finite (supp (bp :: bp))" |
204 lemma bp_supp: "finite (supp (bp :: bp))" |
228 apply (induct bp) |
205 apply (induct bp) |
229 apply(simp_all add: supp_def) |
206 apply(simp_all add: supp_def) |
230 apply (fold supp_def) |
207 apply(simp add: supp_at_base supp_def[symmetric]) |
231 apply (simp add: supp_at_base) |
208 apply(simp add: Collect_imp_eq Collect_neg_eq[symmetric] supp_def) |
232 apply(simp add: Collect_imp_eq) |
|
233 apply(simp add: Collect_neg_eq[symmetric]) |
|
234 apply (fold supp_def) |
|
235 apply (simp) |
|
236 done |
209 done |
237 |
210 |
238 instance trm1 :: fs |
211 instance trm1 :: fs |
239 apply default |
212 apply default |
240 apply(induct_tac x rule: trm1_bp_inducts(1)) |
213 apply(induct_tac x rule: trm1_bp_inducts(1)) |
457 lemma alpha4_eqvt: |
430 lemma alpha4_eqvt: |
458 "t \<approx>4 s \<Longrightarrow> (pi \<bullet> t) \<approx>4 (pi \<bullet> s)" |
431 "t \<approx>4 s \<Longrightarrow> (pi \<bullet> t) \<approx>4 (pi \<bullet> s)" |
459 "a \<approx>4l b \<Longrightarrow> (pi \<bullet> a) \<approx>4l (pi \<bullet> b)" |
432 "a \<approx>4l b \<Longrightarrow> (pi \<bullet> a) \<approx>4l (pi \<bullet> b)" |
460 sorry |
433 sorry |
461 |
434 |
462 (* |
|
463 prove alpha4_transp_aux: {* (snd o snd) (build_alpha_refl_gl [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] ("x","y","z")) *} |
|
464 apply (tactic {* |
|
465 transp_tac @{thm rtrm4.induct} @{thms alpha4_inj} @{thms rtrm4.inject list.inject} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha1_eqvt} 1 *}) |
|
466 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp}, []), |
435 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp}, []), |
467 (build_equivps [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject list.inject} @{thms alpha4_inj} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases list.cases} @{thms alpha4_eqvt} ctxt)) ctxt)) *} |
436 (build_equivps [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject list.inject} @{thms alpha4_inj} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha4_eqvt} ctxt)) ctxt)) *} |
468 *) |
437 thm alpha4_equivp |
469 |
|
470 |
|
471 |
|
472 |
|
473 lemma alpha4_equivp: "equivp alpha_rtrm4" sorry |
|
474 lemma alpha4list_equivp: "equivp alpha_rtrm4_list" sorry |
|
475 |
438 |
476 quotient_type |
439 quotient_type |
477 qrtrm4 = rtrm4 / alpha_rtrm4 and |
440 qrtrm4 = rtrm4 / alpha_rtrm4 and |
478 qrtrm4list = "rtrm4 list" / alpha_rtrm4_list |
441 qrtrm4list = "rtrm4 list" / alpha_rtrm4_list |
479 by (simp_all add: alpha4_equivp alpha4list_equivp) |
442 by (simp_all add: alpha4_equivp) |
480 |
443 |
481 |
444 |
482 datatype rtrm5 = |
445 datatype rtrm5 = |
483 rVr5 "name" |
446 rVr5 "name" |
484 | rAp5 "rtrm5" "rtrm5" |
447 | rAp5 "rtrm5" "rtrm5" |