70 notation |
70 notation |
71 alpha_rkind ("_ \<approx>ki _" [100, 100] 100) |
71 alpha_rkind ("_ \<approx>ki _" [100, 100] 100) |
72 and alpha_rty ("_ \<approx>ty _" [100, 100] 100) |
72 and alpha_rty ("_ \<approx>ty _" [100, 100] 100) |
73 and alpha_rtrm ("_ \<approx>tr _" [100, 100] 100) |
73 and alpha_rtrm ("_ \<approx>tr _" [100, 100] 100) |
74 thm fv_rkind_fv_rty_fv_rtrm.simps alpha_rkind_alpha_rty_alpha_rtrm.intros |
74 thm fv_rkind_fv_rty_fv_rtrm.simps alpha_rkind_alpha_rty_alpha_rtrm.intros |
75 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alphas_inj}, []), (build_alpha_inj @{thms alpha_rkind_alpha_rty_alpha_rtrm.intros} @{thms rkind.distinct rty.distinct rtrm.distinct rkind.inject rty.inject rtrm.inject} @{thms alpha_rkind.cases alpha_rty.cases alpha_rtrm.cases} ctxt)) ctxt)) *} |
75 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha_rkind_alpha_rty_alpha_rtrm_inj}, []), (build_alpha_inj @{thms alpha_rkind_alpha_rty_alpha_rtrm.intros} @{thms rkind.distinct rty.distinct rtrm.distinct rkind.inject rty.inject rtrm.inject} @{thms alpha_rkind.cases alpha_rty.cases alpha_rtrm.cases} ctxt)) ctxt)) *} |
76 thm alphas_inj |
76 thm alpha_rkind_alpha_rty_alpha_rtrm_inj |
77 |
77 |
78 lemma alphas_eqvt: |
78 lemma alpha_eqvt: |
79 "t1 \<approx>ki s1 \<Longrightarrow> (pi \<bullet> t1) \<approx>ki (pi \<bullet> s1)" |
79 "t1 \<approx>ki s1 \<Longrightarrow> (pi \<bullet> t1) \<approx>ki (pi \<bullet> s1)" |
80 "t2 \<approx>rty s2 \<Longrightarrow> (pi \<bullet> t2) \<approx>rty (pi \<bullet> s2)" |
80 "t2 \<approx>ty s2 \<Longrightarrow> (pi \<bullet> t2) \<approx>ty (pi \<bullet> s2)" |
81 "t3 \<approx>tr s3 \<Longrightarrow> (pi \<bullet> t3) \<approx>tr (pi \<bullet> s3)" |
81 "t3 \<approx>tr s3 \<Longrightarrow> (pi \<bullet> t3) \<approx>tr (pi \<bullet> s3)" |
82 sorry |
82 sorry |
83 |
83 |
84 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alphas_equivp}, []), |
84 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha_equivps}, []), |
85 (build_equivps [@{term alpha_rkind}, @{term alpha_rty}, @{term alpha_rtrm}] |
85 (build_equivps [@{term alpha_rkind}, @{term alpha_rty}, @{term alpha_rtrm}] |
86 @{thm rkind_rty_rtrm.induct} @{thm alpha_rkind_alpha_rty_alpha_rtrm.induct} |
86 @{thm rkind_rty_rtrm.induct} @{thm alpha_rkind_alpha_rty_alpha_rtrm.induct} |
87 @{thms rkind.inject rty.inject rtrm.inject} @{thms alphas_inj} |
87 @{thms rkind.inject rty.inject rtrm.inject} @{thms alpha_rkind_alpha_rty_alpha_rtrm_inj} |
88 @{thms rkind.distinct rty.distinct rtrm.distinct} |
88 @{thms rkind.distinct rty.distinct rtrm.distinct} |
89 @{thms alpha_rkind.cases alpha_rty.cases alpha_rtrm.cases} |
89 @{thms alpha_rkind.cases alpha_rty.cases alpha_rtrm.cases} |
90 @{thms alphas_eqvt} ctxt)) ctxt)) *} |
90 @{thms alpha_eqvt} ctxt)) ctxt)) *} |
91 thm alphas_equivp |
91 thm alpha_equivps |
92 *) |
92 *) |
93 |
93 |
94 primrec |
94 primrec |
95 fv_rkind :: "rkind \<Rightarrow> atom set" |
95 fv_rkind :: "rkind \<Rightarrow> atom set" |
96 and fv_rty :: "rty \<Rightarrow> atom set" |
96 and fv_rty :: "rty \<Rightarrow> atom set" |