# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1255449714 -7200
# Node ID 9220c51e5155f5e9e20dc7eedf58d95c9a3ebfc9
# Parent  133af7260a1233b62be2690cace8f5d77ab22774
atomize_thm and meta_quantify.

diff -r 133af7260a12 -r 9220c51e5155 QuotMain.thy
--- a/QuotMain.thy	Tue Oct 13 13:37:07 2009 +0200
+++ b/QuotMain.thy	Tue Oct 13 18:01:54 2009 +0200
@@ -327,13 +327,9 @@
 definition
   "(x : p) \<Longrightarrow> (Babs p m x = m x)"
 
-print_theorems
-
-thm Ball_def
+(*definition BAll :: "('a \<Rightarrow> prop) \<Rightarrow> ('a \<Rightarrow> prop) \<Rightarrow> prop" where
+  "BAll (R :: 'a \<Rightarrow> prop) (P :: 'a \<Rightarrow> prop) \<equiv> (\<And>x. (PROP R x \<Longrightarrow> PROP P x))"*)
 
-definition
-  "BAll A P \<equiv> (\<And>x. x \<in> A \<Longrightarrow> P x)"
-thm BAll_def
 
 ML {*
 (* trm \<Rightarrow> new_trm *)
@@ -385,22 +381,63 @@
       in
         Term.lambda_name (x, v) rec_term
       end
+  | ((Const (@{const_name "Ex"}, _)) $ (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 Bex}, (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 "Ball"
-term "Ball (Respects (RR)) (\<lambda>x :: trm. true)"
 
 ML {*
   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})
+  cterm_of @{theory} (regularise @{term "\<forall>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context});
+  cterm_of @{theory} (regularise @{term "\<exists>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context})
+*}
+
+
+term Respects
+
+ML {*
+fun atomize_thm t =
+  MetaSimplifier.rewrite_rule [ObjectLogic.atomize (cterm_of @{theory} (prop_of t))] t
 *}
 
+ML {*
+fun meta_quantify t =
+  let
+    val vars = Term.add_vars (prop_of t) [];
+    val cvars = map (fn x => cterm_of @{theory} (Var x)) vars
+  in
+    fold forall_intr cvars t
+  end
+*}
+
+ML {* atomize_thm (meta_quantify @{thm list.induct}) *}
+
 (*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 *}
 
@@ -1079,6 +1116,14 @@
 
 thm list.induct
 
+ML {* val li = atomize_thm (meta_quantify @{thm list.induct}) *}
+
+ML {* (* Doesn't recognize that 'a list = '?a list *)
+  cterm_of @{theory} (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context})
+*}
+
+
+
 ML {*
   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list.induct}))
 *}