--- a/IntEx.thy	Wed Nov 04 12:19:04 2009 +0100
+++ b/IntEx.thy	Wed Nov 04 13:33:13 2009 +0100
@@ -3,7 +3,7 @@
 begin
 
 fun
-  intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
+  intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50)
 where
   "intrel (x, y) (u, v) = (x + v = u + y)"
 
@@ -43,7 +43,6 @@
 
 term PLUS
 thm PLUS_def
-ML {* prop_of @{thm PLUS_def} *}
 
 fun
   my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
@@ -109,7 +108,7 @@
  "SIGN i = (if i = ZERO then ZERO else if (LESS ZERO i) then ONE else (NEG ONE))"
 
 lemma plus_sym_pre:
-  shows "intrel (my_plus a b) (my_plus b a)"
+  shows "my_plus a b \<approx> my_plus b a"
   apply(cases a)
   apply(cases b)
   apply(auto)
@@ -132,7 +131,7 @@
 ML {* lift_thm_my_int @{context} @{thm plus_sym_pre} *}
 
 lemma plus_assoc_pre:
-  shows "intrel (my_plus (my_plus i j) k) (my_plus i (my_plus j k))"
+  shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)"
   apply (cases i)
   apply (cases j)
   apply (cases k)
@@ -148,18 +147,18 @@
 
 
 
-
+lemma ho_tst: "foldl my_plus x [] = x"
+apply simp
+done
 
 text {* Below is the construction site code used if things do not work *}
 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int" *}
-ML {* val abs = findabs rty (prop_of (atomize_thm @{thm plus_sym_pre})) *}
-ML {* val simp_lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *}
-ML {* val defs_sym = add_lower_defs @{context} defs *}
 (* ML {* val consts = [@{const_name my_plus}] *}*)
 ML {* val consts = lookup_quot_consts defs *}
 ML {* val t_a = atomize_thm @{thm ho_tst} *}
-prove t_r: {* build_regularize_goal t_a rty rel @{context} *}
+
+(*prove t_r: {* build_regularize_goal t_a rty rel @{context} *}
 ML_prf {*   fun tac ctxt =
       (ObjectLogic.full_atomize_tac) THEN'
      REPEAT_ALL_NEW (FIRST' [
@@ -177,16 +176,51 @@
 apply (atomize(full))
 apply (tactic {* tac @{context} 1 *})
 apply (auto)
-sorry
-(*ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *}*)
-ML {* val t_t = Toplevel.program (fn () => repabs @{context} @{thm t_r} consts rty qty quot rel_refl trans2 rsp_thms) *}
+done
+ML {* val t_r = @{thm t_r} OF [t_a] *}*)
+ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *}
+ML {*
+  val rt = build_repabs_term @{context} t_r consts rty qty
+  val rg = Logic.mk_equals ((Thm.prop_of t_r), rt);
+*}
+
+lemma foldl_rsp:
+  "((IntEx.intrel ===> IntEx.intrel ===> IntEx.intrel) ===>
+           IntEx.intrel ===> op = ===> IntEx.intrel)
+           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 (simp only:)
+  apply (rule list.induct)
+  apply (simp)
+  apply (simp only: foldl.simps)
+  sorry
+
+ML {* val rsp_thms = @{thm foldl_rsp} :: rsp_thms *}
+prove t_t: rg
+apply(atomize(full))
+ML_prf {* fun r_mk_comb_tac_int lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *}
+apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_int @{context}) 1 *})
+done
+ML {* val t_t = @{thm Pure.equal_elim_rule1} OF [@{thm t_t},t_r] *}
+ML {* val abs = findabs rty (prop_of t_a) *}
+ML {* val aps = findaps rty (prop_of t_a); *}
+ML {* val simp_lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *}
+
+(*ML {* val t_t = Toplevel.program (fn () => repabs @{context} @{thm t_r} consts rty qty quot rel_refl trans2 rsp_thms) *}*)
 ML {* val (alls, exs) = findallex rty qty (prop_of t_a) *}
 ML {* val allthms = map (make_allex_prs_thm @{context} quot @{thm FORALL_PRS}) alls *}
 ML {* val t_a = MetaSimplifier.rewrite_rule (allthms) t_t *}
 ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_a *}
+ML {* val defs_sym = add_lower_defs @{context} defs *}
 ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_l *}
 ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *}
 ML {* ObjectLogic.rulify t_r *}
-
-thm FORALL_PRS
-