56 apply default |
56 apply default |
57 apply (simp_all only:rperm_zero_ok rperm_plus_ok) |
57 apply (simp_all only:rperm_zero_ok rperm_plus_ok) |
58 done |
58 done |
59 |
59 |
60 end |
60 end |
|
61 |
|
62 (* |
|
63 setup {* snd o define_raw_perms ["kind", "ty", "trm"] ["LFex.kind", "LFex.ty", "LFex.trm"] *} |
|
64 local_setup {* |
|
65 snd o define_fv_alpha "LFex.kind" |
|
66 [[ [], [[], [(NONE, 1)], [(NONE, 1)]] ], |
|
67 [ [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]] ], |
|
68 [ [[]], [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]]]] *} |
|
69 notation |
|
70 alpha_kind ("_ \<approx>ki _" [100, 100] 100) |
|
71 and alpha_ty ("_ \<approx>ty _" [100, 100] 100) |
|
72 and alpha_trm ("_ \<approx>tr _" [100, 100] 100) |
|
73 thm fv_kind_fv_ty_fv_trm.simps alpha_kind_alpha_ty_alpha_trm.intros |
|
74 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alphas_inj}, []), (build_alpha_inj @{thms alpha_kind_alpha_ty_alpha_trm.intros} @{thms kind.distinct ty.distinct trm.distinct kind.inject ty.inject trm.inject} @{thms alpha_kind.cases alpha_ty.cases alpha_trm.cases} ctxt)) ctxt)) *} |
|
75 thm alphas_inj |
|
76 |
|
77 lemma alphas_eqvt: |
|
78 "t1 \<approx>ki s1 \<Longrightarrow> (pi \<bullet> t1) \<approx>ki (pi \<bullet> s1)" |
|
79 "t2 \<approx>ty s2 \<Longrightarrow> (pi \<bullet> t2) \<approx>ty (pi \<bullet> s2)" |
|
80 "t3 \<approx>tr s3 \<Longrightarrow> (pi \<bullet> t3) \<approx>tr (pi \<bullet> s3)" |
|
81 sorry |
|
82 |
|
83 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alphas_equivp}, []), |
|
84 (build_equivps [@{term alpha_kind}, @{term alpha_ty}, @{term alpha_trm}] |
|
85 @{thm kind_ty_trm.induct} @{thm alpha_kind_alpha_ty_alpha_trm.induct} |
|
86 @{thms kind.inject ty.inject trm.inject} @{thms alphas_inj} |
|
87 @{thms kind.distinct ty.distinct trm.distinct} |
|
88 @{thms alpha_kind.cases alpha_ty.cases alpha_trm.cases} |
|
89 @{thms alphas_eqvt} ctxt)) ctxt)) *} |
|
90 thm alphas_equivp |
|
91 *) |
61 |
92 |
62 primrec |
93 primrec |
63 rfv_kind :: "kind \<Rightarrow> atom set" |
94 rfv_kind :: "kind \<Rightarrow> atom set" |
64 and rfv_ty :: "ty \<Rightarrow> atom set" |
95 and rfv_ty :: "ty \<Rightarrow> atom set" |
65 and rfv_trm :: "trm \<Rightarrow> atom set" |
96 and rfv_trm :: "trm \<Rightarrow> atom set" |