# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1255433827 -7200
# Node ID 133af7260a1233b62be2690cace8f5d77ab22774
# Parent  dbffc6477c089085b814c911db0645b03767767d
Regularizing HOL all.

diff -r dbffc6477c08 -r 133af7260a12 QuotMain.thy
--- a/QuotMain.thy	Tue Oct 13 11:38:35 2009 +0200
+++ b/QuotMain.thy	Tue Oct 13 13:37:07 2009 +0200
@@ -320,17 +320,20 @@
         | _ => Const (@{const_name "op ="}, ty --> ty --> @{typ bool}))
 *}
 
-definition
-  "(x : p) ==> (Babs p m x = m x)"
-
-print_theorems
-thm Babs_def
-ML {* type_of @{term Babs } *}
-ML {* type_of @{term Ball } *}
 ML {*
   cterm_of @{theory} (tyRel @{typ "trm \<Rightarrow> bool"} @{typ "trm"} @{term "RR"} @{context})
 *}
-ML {* type_of @{term Respects } *}
+
+definition
+  "(x : p) \<Longrightarrow> (Babs p m x = m x)"
+
+print_theorems
+
+thm Ball_def
+
+definition
+  "BAll A P \<equiv> (\<And>x. x \<in> A \<Longrightarrow> P x)"
+thm BAll_def
 
 ML {*
 (* trm \<Rightarrow> new_trm *)
@@ -348,7 +351,7 @@
         val res_term = respects $ sub_res_term;
         val ty = fastype_of trm;
         val rabs = Const (@{const_name Babs}, (fastype_of res_term) --> ty --> ty);
-        val rabs_term = (rabs $ respects) $ lam_term;
+        val rabs_term = (rabs $ res_term) $ lam_term;
       in
         rabs_term
       end else let
@@ -359,24 +362,48 @@
       in
         Term.lambda_name (x, v) rec_term
       end
+  | ((Const (@{const_name "All"}, _)) $ (Abs (x, T, t))) =>
+      if T = rty then let
+        val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
+        val v = Free (x', rty);
+        val t' = subst_bound (v, t);
+        val rec_term = regularise t' rty rel lthy2;
+        val lam_term = Term.lambda_name (x, v) rec_term;
+        val sub_res_term = tyRel T rty rel lthy;
+        val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool});
+        val res_term = respects $ sub_res_term;
+        val ty = fastype_of lam_term;
+        val rall = Const (@{const_name Ball}, (fastype_of res_term) --> ty --> @{typ bool});
+        val rall_term = (rall $ res_term) $ lam_term;
+      in
+        rall_term
+      end else let
+        val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
+        val v = Free (x', rty);
+        val t' = subst_bound (v, t);
+        val rec_term = regularise t' rty rel lthy2;
+      in
+        Term.lambda_name (x, v) rec_term
+      end
   | _ => trm
 
 *}
-
-term "Babs (Respects (RR)) (\<lambda>x :: trm. x)"
+term "Ball"
+term "Ball (Respects (RR)) (\<lambda>x :: trm. true)"
 
-(*
 ML {*
-  Toplevel.program (fn () =>
-  cterm_of @{theory} (regularise @{term "\<lambda>x :: trm. x"} @{typ "trm"} @{term "RR"} @{context})
-  )
+  cterm_of @{theory} (regularise @{term "\<lambda>x :: trm. x"} @{typ "trm"} @{term "RR"} @{context});
+  cterm_of @{theory} (regularise @{term "\<forall>x :: trm. true"} @{typ "trm"} @{term "RR"} @{context})
 *}
 
-fun prove_reg trm \<Rightarrow> thm (we might need some facts to do this)
+(*fun prove_reg trm \<Rightarrow> thm (we might need some facts to do this)
   trm == new_trm
 *)
 
+thm list.induct
+
 text {* produces the definition for a lifted constant *}
+
 ML {*
 fun get_const_def nconst oconst rty qty lthy =
 let