equal
deleted
inserted
replaced
40 |
40 |
41 local_setup {* snd o define_raw_alpha dtinfo [] bl [@{term fv_rtrm4}, @{term fv_rtrm4_list}] *} |
41 local_setup {* snd o define_raw_alpha dtinfo [] bl [@{term fv_rtrm4}, @{term fv_rtrm4_list}] *} |
42 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_rel_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases} ctxt)) ctxt)) *} |
42 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_rel_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases} ctxt)) ctxt)) *} |
43 lemmas alpha_inj = alpha4_inj(1-3) |
43 lemmas alpha_inj = alpha4_inj(1-3) |
44 |
44 |
45 lemma alpha_fix: "alpha_rtrm4_list = list_rel alpha_rtrm4" |
45 lemma alpha_fix: "alpha_rtrm4_list = list_all2 alpha_rtrm4" |
46 apply (rule ext)+ |
46 apply (rule ext)+ |
47 apply (induct_tac x xa rule: list_induct2') |
47 apply (induct_tac x xa rule: list_induct2') |
48 apply (simp_all add: alpha_rtrm4_alpha_rtrm4_list.intros) |
48 apply (simp_all add: alpha_rtrm4_alpha_rtrm4_list.intros) |
49 apply clarify apply (erule alpha_rtrm4_list.cases) apply(simp_all) |
49 apply clarify apply (erule alpha_rtrm4_list.cases) apply(simp_all) |
50 apply clarify apply (erule alpha_rtrm4_list.cases) apply(simp_all) |
50 apply clarify apply (erule alpha_rtrm4_list.cases) apply(simp_all) |
103 (fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp alpha4_equivp} 1) *} |
103 (fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp alpha4_equivp} 1) *} |
104 local_setup {* snd o prove_const_rsp [] @{binding rLm4_rsp} [@{term rLm4}] |
104 local_setup {* snd o prove_const_rsp [] @{binding rLm4_rsp} [@{term rLm4}] |
105 (fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp alpha4_equivp} 1) *} |
105 (fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp alpha4_equivp} 1) *} |
106 |
106 |
107 lemma [quot_respect]: |
107 lemma [quot_respect]: |
108 "(alpha_rtrm4 ===> list_rel alpha_rtrm4 ===> alpha_rtrm4) rAp4 rAp4" |
108 "(alpha_rtrm4 ===> list_all2 alpha_rtrm4 ===> alpha_rtrm4) rAp4 rAp4" |
109 by (simp add: alpha_inj_fixed) |
109 by (simp add: alpha_inj_fixed) |
110 |
110 |
111 local_setup {* snd o prove_const_rsp [] @{binding permute_rtrm4_rsp} |
111 local_setup {* snd o prove_const_rsp [] @{binding permute_rtrm4_rsp} |
112 [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"}] |
112 [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"}] |
113 (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha4_eqvt}) 1) *} |
113 (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha4_eqvt}) 1) *} |
124 apply simp |
124 apply simp |
125 apply simp |
125 apply simp |
126 apply (simp add: meta_eq_to_obj_eq[OF permute_trm4_def,simplified expand_fun_eq,simplified]) |
126 apply (simp add: meta_eq_to_obj_eq[OF permute_trm4_def,simplified expand_fun_eq,simplified]) |
127 done |
127 done |
128 |
128 |
129 lemma [quot_respect]: "(op = ===> list_rel alpha_rtrm4 ===> list_rel alpha_rtrm4) permute permute" |
129 lemma [quot_respect]: "(op = ===> list_all2 alpha_rtrm4 ===> list_all2 alpha_rtrm4) permute permute" |
130 apply simp |
130 apply simp |
131 apply (rule allI)+ |
131 apply (rule allI)+ |
132 apply (induct_tac xa y rule: list_induct2') |
132 apply (induct_tac xa y rule: list_induct2') |
133 apply simp_all |
133 apply simp_all |
134 apply clarify |
134 apply clarify |