148 lemma fv_rtrm1_rsp:

   148 prove fv_rtrm1_rsp': {*

   149   shows "t \<approx>1 s \<Longrightarrow> fv_rtrm1 t = fv_rtrm1 s"

   149  (@{term Trueprop} $ (Quotient_Term.equiv_relation_chk @{context} (fastype_of @{term fv_rtrm1}, fastype_of @{term fv_trm1}) $ @{term fv_rtrm1} $ @{term fv_rtrm1})) *}

   150   apply(induct rule: alpha_rtrm1_alpha_bp.inducts(1))

   150 by (tactic {*

   151   apply(simp_all add: alpha_gen.simps alpha_bp_eq)

   151   (rtac @{thm fun_rel_id} THEN'

   152   done

   152   eresolve_tac @{thms alpha_rtrm1_alpha_bp.inducts} THEN_ALL_NEW

   153   asm_full_simp_tac (HOL_ss addsimps @{thms alpha_gen fv_rtrm1_fv_bp.simps})) 1 *})

   154 

   155 

   156 lemmas fv_rtrm1_rsp = apply_rsp'[OF fv_rtrm1_rsp']

   157 

   158 (* We need this since 'prove' doesn't support attributes *)

   159 lemma [quot_respect]: "(alpha_rtrm1 ===> op =) fv_rtrm1 fv_rtrm1"

   160   by (rule fv_rtrm1_rsp')

   161 

   162 ML {*

   163 fun contr_rsp_tac inj rsp equivps =

   164 let

   165   val reflps = map (fn x => @{thm equivp_reflp} OF [x]) equivps

   166 in

   167   REPEAT o rtac @{thm fun_rel_id} THEN'

   168   simp_tac (HOL_ss addsimps inj) THEN'

   169   (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)) THEN_ALL_NEW

   170   (asm_simp_tac HOL_ss THEN_ALL_NEW (

   171    rtac @{thm exI[of _ "0 :: perm"]} THEN'

   172    asm_full_simp_tac (HOL_ss addsimps (rsp @ reflps @

   173      @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv}))

   174   ))

   175 end

   176 *}

   159 apply (simp_all only: fun_rel_def alpha1_inj alpha_bp_eq)

   183 apply (tactic {* contr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1 *})+

   160 apply (clarify)

   184 done

   161 apply (clarify)

   185 

   162 apply (clarify)

   163 apply (auto)

   164 apply (rule_tac [!] x="0" in exI)

   165 apply (simp_all add: alpha_gen fresh_star_def fresh_zero_perm fv_rtrm1_rsp)

   166 done

   167 

   168 lemma [quot_respect]:

   169   "(op = ===> alpha_rtrm1 ===> alpha_rtrm1) permute permute"

   170   by (simp add: alpha1_eqvt)

   171 

   172 lemma [quot_respect]:

   173   "(alpha_rtrm1 ===> op =) fv_rtrm1 fv_rtrm1"

   174   by (simp add: fv_rtrm1_rsp)