# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1255530212 -7200
# Node ID ec29be471518fd6094ee044ee7f2ccfd9d09804a
# Parent  56ad69873907f6b02a14586434ffea5f947b685d
Manually regularized list_induct2

diff -r 56ad69873907 -r ec29be471518 QuotMain.thy
--- 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)
diff -r 56ad69873907 -r ec29be471518 QuotScript.thy
--- a/QuotScript.thy	Wed Oct 14 12:05:39 2009 +0200
+++ b/QuotScript.thy	Wed Oct 14 16:23:32 2009 +0200
@@ -98,6 +98,11 @@
 by metis
 
 fun
+  prod_rel
+where
+  "prod_rel r1 r2 = (\<lambda>(a,b) (c,d). r1 a c \<and> r2 b d)"
+
+fun
   fun_map 
 where
   "fun_map f g h x = g (h (f x))"
@@ -398,4 +403,16 @@
 using a1 a2 unfolding o_def expand_fun_eq
 by (auto)
 
-end
\ No newline at end of file
+lemma equiv_res_forall:
+  fixes P :: "'a \<Rightarrow> bool"
+  assumes a: "EQUIV E"
+  shows "Ball (Respects E) P = (All P)"
+  using a by (metis EQUIV_def IN_RESPECTS a)
+
+lemma equiv_res_exists:
+  fixes P :: "'a \<Rightarrow> bool"
+  assumes a: "EQUIV E"
+  shows "Bex (Respects E) P = (Ex P)"
+  using a by (metis EQUIV_def IN_RESPECTS a)
+
+end