# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1271332544 -7200
# Node ID 8442d81496d5efb16149cb779113f2ffc6c4b67d
# Parent  0120da30673eb00fab0f144c804da1ca511fb2f8
alpha4_eqvt and alpha4_reflp

diff -r 0120da30673e -r 8442d81496d5 Nominal/Manual/Term4.thy
--- a/Nominal/Manual/Term4.thy	Thu Apr 15 12:27:36 2010 +0200
+++ b/Nominal/Manual/Term4.thy	Thu Apr 15 13:55:44 2010 +0200
@@ -66,10 +66,14 @@
 
 local_setup {*
 (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_eqvt_no}, []),
-  build_alpha_eqvts [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"},@{term "permute :: perm \<Rightarrow> rtrm4 list \<Rightarrow> rtrm4 list"}] @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] alpha4_inj_no} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} ctxt) ctxt))
+  build_alpha_eqvts [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] (fn _ => alpha_eqvt_tac @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] alpha4_inj_no} ctxt 1) ctxt) ctxt))
 *}
 lemmas alpha4_eqvt = alpha4_eqvt_no[simplified fix2]
 
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_reflp}, []),
+  build_alpha_refl [((0, @{term alpha_rtrm4}), 0), ((0, @{term alpha_rtrm4_list}), 0)] [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thms alpha4_inj_no} ctxt) ctxt)) *}
+thm alpha4_reflp
+
 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp_no}, []),
   (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_no} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha4_eqvt_no} ctxt)) ctxt)) *}
 lemmas alpha4_equivp = alpha4_equivp_no[simplified fix2]