--- a/QuotMain.thy	Wed Oct 14 16:23:32 2009 +0200
+++ b/QuotMain.thy	Wed Oct 14 16:23:49 2009 +0200
@@ -394,6 +394,13 @@
       in
         Const(@{const_name "All"}, at) $ lam_term
       end
+  | ((Const (@{const_name "All"}, at)) $ P) =>
+      let
+        val (_, [al, _]) = dest_Type (fastype_of P);
+        val ([x], lthy2) = Variable.variant_fixes [""] lthy;
+        val v = (Free (x, al));
+        val abs = Term.lambda_name (x, v) (P $ v);
+      in regularise ((Const (@{const_name "All"}, at)) $ abs) rty rel lthy2 end
   | ((Const (@{const_name "Ex"}, at)) $ (Abs (x, T, t))) =>
       if (needs_lift rty T) then let
         val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
@@ -418,6 +425,13 @@
       in
         Const(@{const_name "All"}, at) $ lam_term
       end
+  | ((Const (@{const_name "Ex"}, at)) $ P) =>
+      let
+        val (_, [al, _]) = dest_Type (fastype_of P);
+        val ([x], lthy2) = Variable.variant_fixes [""] lthy;
+        val v = (Free (x, al));
+        val abs = Term.lambda_name (x, v) (P $ v);
+      in regularise ((Const (@{const_name "Ex"}, at)) $ abs) rty rel lthy2 end
   | a $ b => (regularise a rty rel lthy) $ (regularise b rty rel lthy)
   | _ => trm
 
@@ -427,7 +441,8 @@
   cterm_of @{theory} (regularise @{term "\<lambda>x :: int. 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. P x"} @{typ "trm"} @{term "RR"} @{context});
-  cterm_of @{theory} (regularise @{term "\<exists>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context})
+  cterm_of @{theory} (regularise @{term "\<exists>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context});
+  cterm_of @{theory} (regularise @{term "All (P :: trm \<Rightarrow> bool)"} @{typ "trm"} @{term "RR"} @{context});
 *}
 
 
@@ -1127,8 +1142,18 @@
   done
 
 thm list.induct
+lemma list_induct2:
+  shows "(P []) \<Longrightarrow> (\<forall> a list. ((P list) \<longrightarrow> (P (a # list)))) \<Longrightarrow> \<forall>l :: 'a list. (P l)"
+  apply (rule allI)
+  apply (rule list.induct)
+  apply (assumption)
+  apply (auto)
+  done
 
-ML {* val li = Thm.freezeT (atomize_thm @{thm list.induct}) *}
+ML {* ObjectLogic.atomize (cprop_of @{thm list_induct2}) *}
+ML {* (atomize_thm @{thm list_induct2}) *}
+
+ML {* val li = Thm.freezeT (atomize_thm @{thm list_induct2}) *}
 
 (* TODO: the following 2 lemmas should go to quotscript.thy after all are done *)
 lemma RIGHT_RES_FORALL_REGULAR:
@@ -1147,41 +1172,18 @@
 
 prove {*
  Logic.mk_implies
-   ((regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context}),
-   (prop_of li)) *}
+   ((prop_of li),
+   (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context})) *}
   apply (simp only: equiv_res_forall[OF equiv_list_eq])
-  thm LEFT_RES_FORALL_REGULAR
-  apply (rule LEFT_RES_FORALL_REGULAR)
+  thm RIGHT_RES_FORALL_REGULAR
+  apply (rule RIGHT_RES_FORALL_REGULAR)
   prefer 2
   apply (assumption)
-  apply (erule thin_rl)
   apply (rule allI)
-  apply (rule conjI)
-  prefer 2
+  apply (rule impI)
   apply (rule impI)
-
-  apply (auto)
-  
-  apply (simp)
-  apply (thin_tac 1)
-.
-  apply (simp)
-
-  apply (unfold Ball_def)
-  apply (simp only: IN_RESPECTS)
-  apply (simp add: expand_fun_eq)
-
-
-  apply (tactic {* foo_tac' @{context} 1 *})
-  apply (atomize(full))
-  apply (simp)
-  prefer 2
-  apply (simp only: IN_RESPECTS)
-  apply (simp add:list_eq_refl)
-  apply (tactic {* foo_tac' @{context} 1 *})
-  prefer 2
-  apply (auto)
-  sorry
+  apply (assumption)
+  done
 
 ML {*
   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list.induct}))