--- a/IntEx.thy	Wed Dec 02 14:37:21 2009 +0100
+++ b/IntEx.thy	Wed Dec 02 17:15:36 2009 +0100
@@ -151,9 +151,6 @@
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 prefer 2
 apply(tactic {* clean_tac @{context} [quot] defs 1 *})
-apply(simp add: id_def)
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
@@ -190,7 +187,6 @@
 lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)"
 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
-apply(simp)
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 apply(tactic {* clean_tac @{context} [quot] defs 1 *})
 done
@@ -199,35 +195,88 @@
 apply simp
 done
 
-(* FIXME/TODO: is this a respectfulness theorem? Does not look like one. *)
-lemma map_prs: 
-  "map REP_my_int (map ABS_my_int x) = x"
+
+lemma foldr_prs:
+  assumes a: "QUOTIENT R1 abs1 rep1"
+  and     b: "QUOTIENT R2 abs2 rep2"
+  shows "abs2 (foldr ((abs1 ---> abs2 ---> rep2) f) (map rep1 l) (rep2 e)) = foldr f l e"
+apply (induct l)
+apply (simp add: QUOTIENT_ABS_REP[OF b])
+apply (simp add: QUOTIENT_ABS_REP[OF a] QUOTIENT_ABS_REP[OF b])
+done
+
+lemma foldl_prs:
+  assumes a: "QUOTIENT R1 abs1 rep1"
+  and     b: "QUOTIENT R2 abs2 rep2"
+  shows "abs1 (foldl ((abs1 ---> abs2 ---> rep1) f) (rep1 e) (map rep2 l)) = foldl f e l"
+apply (induct l arbitrary:e)
+apply (simp add: QUOTIENT_ABS_REP[OF a])
+apply (simp add: QUOTIENT_ABS_REP[OF a] QUOTIENT_ABS_REP[OF b])
+done
+
+lemma map_prs:
+  assumes a: "QUOTIENT R1 abs1 rep1"
+  and     b: "QUOTIENT R2 abs2 rep2"
+  shows "(map abs2) (map ((abs1 ---> rep2) f) (map rep1 l)) = map f l"
+apply (induct l)
+apply (simp)
+apply (simp add: QUOTIENT_ABS_REP[OF a] QUOTIENT_ABS_REP[OF b])
+done
+
+
+(* Removed unneeded assumption: "QUOTIENT R abs1 rep1" *)
+lemma nil_prs:
+  shows "map abs1 [] = []"
+by simp
+
+lemma cons_prs:
+  assumes a: "QUOTIENT R1 abs1 rep1"
+  shows "(map abs1) ((rep1 h) # (map rep1 t)) = h # t"
+  apply (induct t)
+by (simp_all add: QUOTIENT_ABS_REP[OF a])
+
+lemma cons_rsp[quot_rsp]:
+  "(op \<approx> ===> LIST_REL op \<approx> ===> LIST_REL op \<approx>) op # op #"
+by simp
+
+(* I believe it's true. *)
+lemma foldl_rsp[quot_rsp]:
+  "((op \<approx> ===> op \<approx> ===> op \<approx>) ===> op \<approx> ===> LIST_REL op \<approx> ===> op \<approx>) foldl foldl"
+apply (simp only: FUN_REL.simps)
+apply (rule allI)
+apply (rule allI)
+apply (rule impI)
+apply (rule allI)
+apply (rule allI)
+apply (rule impI)
+apply (rule allI)
+apply (rule allI)
+apply (rule impI)
+apply (induct_tac xb yb rule:list_induct2) (* To finish I need to give it: arbitrary:xa ya *)
 sorry
 
-lemma foldl_prs[quot_rsp]: 
-  "((op \<approx> ===> op \<approx> ===> op \<approx>) ===> op \<approx> ===> op = ===> op \<approx>) foldl foldl"
-sorry
+lemma nil_listrel_rsp[quot_rsp]:
+  "(LIST_REL R) [] []"
+by simp
 
 lemma "foldl PLUS x [] = x"
 apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
-apply(simp add: map_prs)
-apply(simp only: map_prs)
-apply(tactic {* clean_tac @{context} [quot] defs 1 *})
-sorry
-
-(*
-  FIXME: All below is your construction code; mostly commented out as it
-  does not work.
-*)
-
-lemma "PLUS (PLUS i j) k = PLUS i (PLUS j k)"
-apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *})
-apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
-apply(simp)
-apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) 
+apply(simp only: foldl_prs[OF QUOTIENT_my_int QUOTIENT_my_int])
+apply(simp only: nil_prs)
 apply(tactic {* clean_tac @{context} [quot] defs 1 *})
 done
 
+lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)"
+sorry
 
+lemma "foldl PLUS x (h # t) = PLUS h (foldl PLUS x t)"
+apply(tactic {* procedure_tac @{context} @{thm ho_tst2} 1 *})
+apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
+apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(simp only: foldl_prs[OF QUOTIENT_my_int QUOTIENT_my_int])
+apply(simp only: cons_prs[OF QUOTIENT_my_int])
+apply(tactic {* clean_tac @{context} [quot] defs 1 *})
+done
+