1111 *}

  1112 

  1113 (* my version of regularise *)

  1114 (****************************)

  1115 

  1116 (* some helper functions *)

  1117 ML {*

  1118 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})

  1120 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})

  1122 *}

  1123 

  1124 (* applies f to the subterm of an abstractions, otherwise to the given term *)

  1125 ML {*

  1126 fun apply_subt f trm =

  1127   case trm of

  1128     Abs (x, T, t) => Abs (x, T, f t)

  1129   | _ => f trm

  1130 *}

  1131 

  1132 (* FIXME: assumes always the typ is qty! *)

  1133 ML {*

  1134 fun my_reg rel trm =

  1135   case trm of

  1136     Abs (x, T, t) =>

  1137        let 

  1138           val ty1 = fastype_of trm

  1139        in

  1140          (mk_babs ty1 T) $ (mk_resp T $ rel) $ (apply_subt (my_reg rel) trm)    

  1141        end

  1142   | Const (@{const_name "All"}, U) $ t =>

  1143        let 

  1144           val ty1 = fastype_of t

  1145           val ty2 = domain_type ty1

  1146        in

  1147          (mk_ball ty1) $ (mk_resp ty2 $ rel) $ (apply_subt (my_reg rel) t)      

  1148        end

  1149   | Const (@{const_name "Ex"}, U) $ t =>

  1150        let 

  1151           val ty1 = fastype_of t

  1152           val ty2 = domain_type ty1

  1153        in

  1154          (mk_bex ty1) $ (mk_resp ty2 $ rel) $ (apply_subt (my_reg rel) t)    

  1155        end

  1156   | _ => trm

  1157 *}

  1158 

  1159 ML {*  

  1160   cterm_of @{theory} (regularise @{term "\<lambda>x::trm. x"} @{typ "trm"} @{term "RR"} @{context});

  1161   cterm_of @{theory} (my_reg @{term "RR"} @{term "\<lambda>x::trm. x"})

  1162 *}

  1163 

  1164 ML {*  

  1165   cterm_of @{theory} (regularise @{term "\<forall>(x::trm) (y::trm). P x y"} @{typ "trm"} @{term "RR"} @{context});

  1166   cterm_of @{theory} (my_reg @{term "RR"} @{term "\<forall>(x::trm) (y::trm). P x y"})

  1167 *}

  1168 

  1169 ML {*  

  1170   cterm_of @{theory} (regularise @{term "\<forall>x::trm. P x"} @{typ "trm"} @{term "RR"} @{context});

  1171   cterm_of @{theory} (my_reg @{term "RR"} @{term "\<forall>x::trm. P x"})

  1172 *}

  1173 

  1174 ML {*  

  1175   cterm_of @{theory} (regularise @{term "\<exists>x::trm. P x"} @{typ "trm"} @{term "RR"} @{context});

  1176   cterm_of @{theory} (my_reg @{term "RR"} @{term "\<exists>x::trm. P x"})

  1177 *}

  1178 

  1179 (* my version is not eta-expanded *)

  1180 ML {*  

  1181   cterm_of @{theory} (regularise @{term "All (P::trm \<Rightarrow> bool)"} @{typ "trm"} @{term "RR"} @{context});

  1182   cterm_of @{theory} (my_reg @{term "RR"} @{term "All (P::trm \<Rightarrow> bool)"})