equal
deleted
inserted
replaced
1112 |
1112 |
1113 (* my version of regularise *) |
1113 (* my version of regularise *) |
1114 (****************************) |
1114 (****************************) |
1115 |
1115 |
1116 (* some helper functions *) |
1116 (* some helper functions *) |
1117 ML {* |
1117 |
1118 fun mk_babs ty ty' = Const (@{const_name "Babs"}, (ty' --> @{typ bool}) --> ty --> ty) |
1118 |
|
1119 ML {* |
|
1120 fun mk_babs ty ty' = Const (@{const_name "Babs"}, [ty' --> @{typ bool}, ty] ---> ty) |
1119 fun mk_ball ty = Const (@{const_name "Ball"}, [ty, ty] ---> @{typ bool}) |
1121 fun mk_ball ty = Const (@{const_name "Ball"}, [ty, ty] ---> @{typ bool}) |
1120 fun mk_bex ty = Const (@{const_name "Bex"}, [ty, ty] ---> @{typ bool}) |
1122 fun mk_bex ty = Const (@{const_name "Bex"}, [ty, ty] ---> @{typ bool}) |
1121 fun mk_resp ty = Const (@{const_name Respects}, ([ty, ty] ---> @{typ bool}) --> ty --> @{typ bool}) |
1123 fun mk_resp ty = Const (@{const_name Respects}, [[ty, ty] ---> @{typ bool}, ty] ---> @{typ bool}) |
1122 *} |
1124 *} |
1123 |
1125 |
1124 (* applies f to the subterm of an abstractions, otherwise to the given term *) |
1126 (* applies f to the subterm of an abstractions, otherwise to the given term *) |
1125 ML {* |
1127 ML {* |
1126 fun apply_subt f trm = |
1128 fun apply_subt f trm = |
1177 ML {* |
1179 ML {* |
1178 cterm_of @{theory} (regularise @{term "\<exists>x::trm. P x"} @{typ "trm"} @{term "RR"} @{context}); |
1180 cterm_of @{theory} (regularise @{term "\<exists>x::trm. P x"} @{typ "trm"} @{term "RR"} @{context}); |
1179 cterm_of @{theory} (my_reg @{term "RR"} @{term "\<exists>x::trm. P x"}) |
1181 cterm_of @{theory} (my_reg @{term "RR"} @{term "\<exists>x::trm. P x"}) |
1180 *} |
1182 *} |
1181 |
1183 |
1182 (* my version is not eta-expanded *) |
1184 (* my version is not eta-expanded, but that should be OK *) |
1183 ML {* |
1185 ML {* |
1184 cterm_of @{theory} (regularise @{term "All (P::trm \<Rightarrow> bool)"} @{typ "trm"} @{term "RR"} @{context}); |
1186 cterm_of @{theory} (regularise @{term "All (P::trm \<Rightarrow> bool)"} @{typ "trm"} @{term "RR"} @{context}); |
1185 cterm_of @{theory} (my_reg @{term "RR"} @{term "All (P::trm \<Rightarrow> bool)"}) |
1187 cterm_of @{theory} (my_reg @{term "RR"} @{term "All (P::trm \<Rightarrow> bool)"}) |
1186 *} |
1188 *} |
1187 |
1189 |