nominal2: comparison Nominal/Term5.thy

equal deleted inserted replaced

-:2c37f5a8c747
+:7b8f570b2450
 done
 local_setup {* snd o Local_Theory.note ((@{binding alpha_dis}, []), (flat (map (distinct_rel @{context} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases}) [(@{thms rtrm5.distinct}, @{term alpha_rtrm5}), (@{thms rlts.distinct}, @{term alpha_rlts}), (@{thms rlts.distinct}, @{term alpha_rbv5})]))) *}
 print_theorems
-local_setup {* snd o Local_Theory.note ((@{binding alpha_bn_rsp}, []), prove_alpha_bn_rsp [@{term alpha_rtrm5}, @{term alpha_rlts}] @{thms alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts} @{thms alpha5_inj alpha_dis} @{thms alpha5_equivp} @{context} (@{term alpha_rbv5}, 1)) *}
+local_setup {* snd o Local_Theory.note ((@{binding alpha_bn_rsp}, []), prove_alpha_bn_rsp [@{term alpha_rtrm5}, @{term alpha_rlts}] @{thms alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts} @{thms rtrm5.exhaust rlts.exhaust} @{thms alpha5_inj alpha_dis} @{thms alpha5_equivp} @{context} (@{term alpha_rbv5}, 1)) *}
 thm alpha_bn_rsp
 lemma [quot_respect]:
 "(alpha_rlts ===> op =) fv_rlts fv_rlts"
 "(alpha_rtrm5 ===> op =) fv_rtrm5 fv_rtrm5"
 apply (clarify)
 apply (rule_tac x="0" in exI)
 apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
 done
 lemma
 shows "(alpha_rlts ===> op =) rbv5 rbv5"
 by (simp add: bv_list_rsp)
 lemmas trm5_lts_inducts = rtrm5_rlts.inducts[quot_lifted]