--- a/QuotMain.thy	Thu Oct 15 10:25:23 2009 +0200
+++ b/QuotMain.thy	Thu Oct 15 11:17:27 2009 +0200
@@ -703,6 +703,19 @@
 apply (metis QUOT_TYPE_I_fset.R_trans QuotMain.card1_cons list_eq_refl mem_cons)
 done
 
+primrec
+  fold1
+where
+  "fold1 f (g :: 'a \<Rightarrow> 'b) (z :: 'b) [] = z"
+| "fold1 f g z (a # A) =
+     (if ((!u v. (f u v = f v u))
+      \<and> (!u v w. ((f u (f v w) = f (f u v) w))))
+     then (
+       if (a memb A) then (fold1 f g z A) else (f (g a) (fold1 f g z A))
+     ) else z)"
+
+thm fold1.simps
+
 lemma cons_preserves:
   fixes z
   assumes a: "xs \<approx> ys"
@@ -1175,6 +1188,16 @@
 thm card1_suc
 ML {* @{thm card1_suc_r} OF [li] *}
 
+ML {* val li = Thm.freezeT (atomize_thm @{thm fold1.simps(2)}) *}
+prove fold1_def_2_r: {*
+ Logic.mk_implies
+   ((prop_of li),
+   (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context})) *}
+  apply (simp add: equiv_res_forall[OF equiv_list_eq])
+  done
+
+ML {* @{thm fold1_def_2_r} OF [li] *}
+
 ML {*
   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list.induct}))
 *}