18 | App "rtrm" "rtrm" |
18 | App "rtrm" "rtrm" |
19 | Lam "rty" "name" "rtrm" |
19 | Lam "rty" "name" "rtrm" |
20 |
20 |
21 |
21 |
22 setup {* snd o define_raw_perms ["rkind", "rty", "rtrm"] ["LFex.rkind", "LFex.rty", "LFex.rtrm"] *} |
22 setup {* snd o define_raw_perms ["rkind", "rty", "rtrm"] ["LFex.rkind", "LFex.rty", "LFex.rtrm"] *} |
|
23 print_theorems |
23 |
24 |
24 local_setup {* |
25 local_setup {* |
25 snd o define_fv_alpha "LFex.rkind" |
26 snd o define_fv_alpha "LFex.rkind" |
26 [[ [], [[], [(NONE, 1)], [(NONE, 1)]] ], |
27 [[ [], [[], [(NONE, 1)], [(NONE, 1)]] ], |
27 [ [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]] ], |
28 [ [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]] ], |
115 lemmas kind_ty_trm_induct = rkind_rty_rtrm.induct[quot_lifted] |
116 lemmas kind_ty_trm_induct = rkind_rty_rtrm.induct[quot_lifted] |
116 |
117 |
117 thm rkind_rty_rtrm.inducts |
118 thm rkind_rty_rtrm.inducts |
118 lemmas kind_ty_trm_inducts = rkind_rty_rtrm.inducts[quot_lifted] |
119 lemmas kind_ty_trm_inducts = rkind_rty_rtrm.inducts[quot_lifted] |
119 |
120 |
120 instantiation kind and ty and trm :: pt |
121 setup {* define_lifted_perms ["LFex.kind", "LFex.ty", "LFex.trm"] |
121 begin |
122 [("permute_kind", @{term "permute :: perm \<Rightarrow> rkind \<Rightarrow> rkind"}), |
122 |
123 ("permute_ty", @{term "permute :: perm \<Rightarrow> rty \<Rightarrow> rty"}), |
123 quotient_definition |
124 ("permute_trm", @{term "permute :: perm \<Rightarrow> rtrm \<Rightarrow> rtrm"})] |
124 "permute_kind :: perm \<Rightarrow> kind \<Rightarrow> kind" |
125 @{thms permute_rkind_permute_rty_permute_rtrm_zero permute_rkind_permute_rty_permute_rtrm_append} *} |
125 is |
|
126 "permute :: perm \<Rightarrow> rkind \<Rightarrow> rkind" |
|
127 |
|
128 quotient_definition |
|
129 "permute_ty :: perm \<Rightarrow> ty \<Rightarrow> ty" |
|
130 is |
|
131 "permute :: perm \<Rightarrow> rty \<Rightarrow> rty" |
|
132 |
|
133 quotient_definition |
|
134 "permute_trm :: perm \<Rightarrow> trm \<Rightarrow> trm" |
|
135 is |
|
136 "permute :: perm \<Rightarrow> rtrm \<Rightarrow> rtrm" |
|
137 |
|
138 instance by default (simp_all add: |
|
139 permute_rkind_permute_rty_permute_rtrm_zero[quot_lifted] |
|
140 permute_rkind_permute_rty_permute_rtrm_append[quot_lifted]) |
|
141 |
|
142 end |
|
143 |
126 |
144 (* |
127 (* |
145 Lifts, but slow and not needed?. |
128 Lifts, but slow and not needed?. |
146 lemmas alpha_kind_alpha_ty_alpha_trm_induct = alpha_rkind_alpha_rty_alpha_rtrm.induct[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
129 lemmas alpha_kind_alpha_ty_alpha_trm_induct = alpha_rkind_alpha_rty_alpha_rtrm.induct[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
147 *) |
130 *) |