# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1255994242 -7200
# Node ID 0842a38dcf01024e29225a930ec7c8ff1add8dc4
# Parent  8e8ba210f0f7d3779ee1bd24e70c5b5fa9464798
my version of regularise (still needs to be completed)

diff -r 8e8ba210f0f7 -r 0842a38dcf01 QuotMain.thy
--- a/QuotMain.thy	Tue Oct 20 00:12:05 2009 +0200
+++ b/QuotMain.thy	Tue Oct 20 01:17:22 2009 +0200
@@ -1110,6 +1110,78 @@
   cterm_of @{theory} (regularise @{term "All (P :: trm \<Rightarrow> bool)"} @{typ "trm"} @{term "RR"} @{context});
 *}
 
+(* my version of regularise *)
+(****************************)
+
+(* some helper functions *)
+ML {*
+fun mk_babs ty ty' = Const (@{const_name "Babs"}, (ty' --> @{typ bool}) --> ty --> ty)
+fun mk_ball ty = Const (@{const_name "Ball"}, [ty, ty] ---> @{typ bool})
+fun mk_bex ty = Const (@{const_name "Bex"}, [ty, ty] ---> @{typ bool})
+fun mk_resp ty = Const (@{const_name Respects}, ([ty, ty] ---> @{typ bool}) --> ty --> @{typ bool})
+*}
+
+(* applies f to the subterm of an abstractions, otherwise to the given term *)
+ML {*
+fun apply_subt f trm =
+  case trm of
+    Abs (x, T, t) => Abs (x, T, f t)
+  | _ => f trm
+*}
+
+(* FIXME: assumes always the typ is qty! *)
+ML {*
+fun my_reg rel trm =
+  case trm of
+    Abs (x, T, t) =>
+       let 
+          val ty1 = fastype_of trm
+       in
+         (mk_babs ty1 T) $ (mk_resp T $ rel) $ (apply_subt (my_reg rel) trm)    
+       end
+  | Const (@{const_name "All"}, U) $ t =>
+       let 
+          val ty1 = fastype_of t
+          val ty2 = domain_type ty1
+       in
+         (mk_ball ty1) $ (mk_resp ty2 $ rel) $ (apply_subt (my_reg rel) t)      
+       end
+  | Const (@{const_name "Ex"}, U) $ t =>
+       let 
+          val ty1 = fastype_of t
+          val ty2 = domain_type ty1
+       in
+         (mk_bex ty1) $ (mk_resp ty2 $ rel) $ (apply_subt (my_reg rel) t)    
+       end
+  | _ => trm
+*}
+
+ML {*  
+  cterm_of @{theory} (regularise @{term "\<lambda>x::trm. x"} @{typ "trm"} @{term "RR"} @{context});
+  cterm_of @{theory} (my_reg @{term "RR"} @{term "\<lambda>x::trm. x"})
+*}
+
+ML {*  
+  cterm_of @{theory} (regularise @{term "\<forall>(x::trm) (y::trm). P x y"} @{typ "trm"} @{term "RR"} @{context});
+  cterm_of @{theory} (my_reg @{term "RR"} @{term "\<forall>(x::trm) (y::trm). P x y"})
+*}
+
+ML {*  
+  cterm_of @{theory} (regularise @{term "\<forall>x::trm. P x"} @{typ "trm"} @{term "RR"} @{context});
+  cterm_of @{theory} (my_reg @{term "RR"} @{term "\<forall>x::trm. P x"})
+*}
+
+ML {*  
+  cterm_of @{theory} (regularise @{term "\<exists>x::trm. P x"} @{typ "trm"} @{term "RR"} @{context});
+  cterm_of @{theory} (my_reg @{term "RR"} @{term "\<exists>x::trm. P x"})
+*}
+
+(* my version is not eta-expanded *)
+ML {*  
+  cterm_of @{theory} (regularise @{term "All (P::trm \<Rightarrow> bool)"} @{typ "trm"} @{term "RR"} @{context});
+  cterm_of @{theory} (my_reg @{term "RR"} @{term "All (P::trm \<Rightarrow> bool)"})
+*}
+
 ML {*
 fun atomize_thm thm =
 let