--- a/QuotMain.thy	Wed Oct 14 12:05:39 2009 +0200
+++ b/QuotMain.thy	Wed Oct 14 16:23:32 2009 +0200
@@ -242,8 +242,8 @@
 
 (* mapfuns for some standard types *)
 setup {*
-  update @{type_name "list"} {mapfun = @{const_name "map"},      relfun = @{const_name "LIST_REL"}} #> 
-  update @{type_name "*"}    {mapfun = @{const_name "prod_fun"}, relfun = "???"} #> 
+  update @{type_name "list"} {mapfun = @{const_name "map"},      relfun = @{const_name "LIST_REL"}} #>
+  update @{type_name "*"}    {mapfun = @{const_name "prod_fun"}, relfun = @{const_name "prod_rel"}} #>
   update @{type_name "fun"}  {mapfun = @{const_name "fun_map"},  relfun = @{const_name "FUN_REL"}}
 *}
 
@@ -1130,15 +1130,51 @@
 
 ML {* val li = Thm.freezeT (atomize_thm @{thm list.induct}) *}
 
+(* TODO: the following 2 lemmas should go to quotscript.thy after all are done *)
+lemma RIGHT_RES_FORALL_REGULAR:
+  assumes a: "!x :: 'a. (R x --> P x --> Q x)"
+  shows "All P ==> Ball R Q"
+  using a
+  apply (metis COMBC_def Collect_def Collect_mem_eq a)
+  done
+
+lemma LEFT_RES_FORALL_REGULAR:
+  assumes a: "!x. (R x \<and> (Q x --> P x))"
+  shows "Ball R Q ==> All P"
+  using a
+  apply (metis COMBC_def Collect_def Collect_mem_eq a)
+  done
+
 prove {*
- Logic.mk_equals
+ Logic.mk_implies
    ((regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context}),
    (prop_of li)) *}
-  apply (atomize(full))
+  apply (simp only: equiv_res_forall[OF equiv_list_eq])
+  thm LEFT_RES_FORALL_REGULAR
+  apply (rule LEFT_RES_FORALL_REGULAR)
+  prefer 2
+  apply (assumption)
+  apply (erule thin_rl)
+  apply (rule allI)
+  apply (rule conjI)
+  prefer 2
+  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 (simp only: IN_RESPECTS)
-  apply (simp_all add: expand_fun_eq)
+  apply (atomize(full))
+  apply (simp)
   prefer 2
   apply (simp only: IN_RESPECTS)
   apply (simp add:list_eq_refl)