merged
authorhuffman
Tue, 09 Jun 2009 11:12:08 -0700
changeset 31538 16068eb224c0
parent 31524 8abf99ab669c (diff)
parent 31537 feec2711da4e (current diff)
child 31539 dc2662edd381
child 31558 e7a282113145
merged
src/HOL/Library/Convex_Euclidean_Space.thy
src/HOL/Library/Euclidean_Space.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Tue Jun 09 10:23:41 2009 -0700
+++ b/src/HOL/Decision_Procs/Approximation.thy	Tue Jun 09 11:12:08 2009 -0700
@@ -1152,6 +1152,7 @@
   else if 0 \<le> lx \<and> ux \<le> lpi      then (lb_cos prec ux, ub_cos prec lx)
   else if - lpi \<le> lx \<and> ux \<le> lpi  then (min (lb_cos prec (-lx)) (lb_cos prec ux), Float 1 0)
   else if 0 \<le> lx \<and> ux \<le> 2 * lpi  then (Float -1 0, max (ub_cos prec lx) (ub_cos prec (- (ux - 2 * lpi))))
+  else if -2 * lpi \<le> lx \<and> ux \<le> 0 then (Float -1 0, max (ub_cos prec (lx + 2 * lpi)) (ub_cos prec (-ux)))
                                  else (Float -1 0, Float 1 0))"
 
 lemma floor_int:
@@ -1354,9 +1355,51 @@
       finally show ?thesis unfolding u by (simp add: real_of_float_max)
     qed
     thus ?thesis unfolding l by auto
+  next case False note 4 = this show ?thesis
+  proof (cases "-2 * ?lpi \<le> ?lx \<and> ?ux \<le> 0")
+    case True note Cond = this with bnds 1 2 3 4
+    have l: "l = Float -1 0"
+      and u: "u = max (ub_cos prec (?lx + 2 * ?lpi)) (ub_cos prec (-?ux))"
+      by (auto simp add: bnds_cos_def Let_def)
+
+    have "cos x \<le> real u"
+    proof (cases "-pi < x - real k * 2 * pi")
+      case True hence "-pi \<le> x - real k * 2 * pi" by simp
+      from negative_ux[OF this Cond[THEN conjunct2]]
+      show ?thesis unfolding u by (simp add: real_of_float_max)
+    next
+      case False hence "x - real k * 2 * pi \<le> -pi" by simp
+      hence pi_x: "x - real k * 2 * pi + 2 * pi \<le> pi" by simp
+
+      have "-2 * pi \<le> real ?lx" using Cond lpi by (auto simp add: le_float_def)
+
+      hence "0 \<le> x - real k * 2 * pi + 2 * pi" using lx by simp
+
+      have lx_0: "0 \<le> real (?lx + 2 * ?lpi)"
+	using Cond lpi by (auto simp add: le_float_def)
+
+      from 1 and Cond have "\<not> -?lpi \<le> ?lx" by auto
+      hence "?lx + 2 * ?lpi \<le> ?lpi" by (auto simp add: le_float_def)
+      hence pi_lx: "real (?lx + 2 * ?lpi) \<le> pi"
+	using lpi[THEN le_imp_neg_le] by (auto simp add: le_float_def)
+
+      have lx_le_x: "real (?lx + 2 * ?lpi) \<le> x - real k * 2 * pi + 2 * pi"
+	using lx lpi by auto
+
+      have "cos x = cos (x + real (-k) * 2 * pi + real (1 :: int) * 2 * pi)"
+	unfolding cos_periodic_int ..
+      also have "\<dots> \<le> cos (real (?lx + 2 * ?lpi))"
+	using cos_monotone_0_pi'[OF lx_0 lx_le_x pi_x]
+	by (simp only: real_of_float_minus real_of_int_minus real_of_one
+	  number_of_Min real_diff_def mult_minus_left real_mult_1)
+      also have "\<dots> \<le> real (ub_cos prec (?lx + 2 * ?lpi))"
+	using lb_cos[OF lx_0 pi_lx] by simp
+      finally show ?thesis unfolding u by (simp add: real_of_float_max)
+    qed
+    thus ?thesis unfolding l by auto
   next
-    case False with bnds 1 2 3 show ?thesis by (auto simp add: bnds_cos_def Let_def)
-  qed qed qed qed
+    case False with bnds 1 2 3 4 show ?thesis by (auto simp add: bnds_cos_def Let_def)
+  qed qed qed qed qed
 qed
 
 section "Exponential function"
--- a/src/HOL/Library/Convex_Euclidean_Space.thy	Tue Jun 09 10:23:41 2009 -0700
+++ b/src/HOL/Library/Convex_Euclidean_Space.thy	Tue Jun 09 11:12:08 2009 -0700
@@ -50,9 +50,6 @@
         "setsum (\<lambda>y. if (x = y) then P y else Q y) s = setsum Q s"
   apply(rule_tac [!] setsum_cong2) using assms by auto
 
-lemma setsum_diff1'':assumes "finite A" "a \<in> A"
-  shows "setsum f (A - {a}) = setsum f A - (f a::'a::ring)" unfolding setsum_diff1'[OF assms] by auto
-
 lemma setsum_delta'': fixes s::"(real^'n) set" assumes "finite s"
   shows "(\<Sum>x\<in>s. (if y = x then f x else 0) *s x) = (if y\<in>s then (f y) *s y else 0)"
 proof-
@@ -64,34 +61,6 @@
 
 lemma if_smult:"(if P then x else (y::real)) *s v = (if P then x *s v else y *s v)" by auto
 
-lemma ex_bij_betw_nat_finite_1:
-  assumes "finite M"
-  shows "\<exists>h. bij_betw h {1 .. card M} M"
-proof-
-  obtain h where h:"bij_betw h {0..<card M} M" using ex_bij_betw_nat_finite[OF assms] by auto
-  let ?h = "h \<circ> (\<lambda>i. i - 1)"
-  have *:"(\<lambda>i. i - 1) ` {1..card M} = {0..<card M}" apply auto  unfolding image_iff apply(rule_tac x="Suc x" in bexI) by auto
-  hence "?h ` {1..card M} = h ` {0..<card M}" unfolding image_compose by auto 
-  hence "?h ` {1..card M} = M" unfolding image_compose using h unfolding * unfolding bij_betw_def by auto
-  moreover
-  have "inj_on (\<lambda>i. i - Suc 0) {Suc 0..card M}" unfolding inj_on_def by auto
-  hence "inj_on ?h {1..card M}" apply(rule_tac comp_inj_on) unfolding * using h[unfolded bij_betw_def] by auto
-  ultimately show ?thesis apply(rule_tac x="h \<circ> (\<lambda>i. i - 1)" in exI) unfolding o_def and bij_betw_def by auto
-qed
-
-lemma finite_subset_image:
-  assumes "B \<subseteq> f ` A" "finite B"
-  shows "\<exists>C\<subseteq>A. finite C \<and> B = f ` C"
-proof- from assms(1) have "\<forall>x\<in>B. \<exists>y\<in>A. x = f y" by auto
-  then obtain c where "\<forall>x\<in>B. c x \<in> A \<and> x = f (c x)"
-    using bchoice[of B "\<lambda>x y. y\<in>A \<and> x = f y"] by auto
-  thus ?thesis apply(rule_tac x="c ` B" in exI) using assms(2) by auto qed
-
-lemma inj_on_image_eq_iff: assumes "inj_on f (A \<union> B)"
-  shows "f ` A = f ` B \<longleftrightarrow> A = B"
-  using assms by(blast dest: inj_onD)
-
-
 lemma mem_interval_1: fixes x :: "real^1" shows
  "(x \<in> {a .. b} \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b)"
  "(x \<in> {a<..<b} \<longleftrightarrow> dest_vec1 a < dest_vec1 x \<and> dest_vec1 x < dest_vec1 b)"
@@ -559,7 +528,7 @@
   have "s \<noteq> {v}" using as(3,6) by auto
   thus "\<exists>x\<in>p. \<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p - {x} \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *s v) = x" 
     apply(rule_tac x=v in bexI, rule_tac x="s - {v}" in exI, rule_tac x="\<lambda>x. - (1 / u v) * u x" in exI)
-    unfolding vector_smult_assoc[THEN sym] and setsum_cmul unfolding setsum_right_distrib[THEN sym] and setsum_diff1''[OF as(1,5)] using as by auto
+    unfolding vector_smult_assoc[THEN sym] and setsum_cmul unfolding setsum_right_distrib[THEN sym] and setsum_diff1_ring[OF as(1,5)] using as by auto
 qed
 
 lemma affine_dependent_explicit_finite:
@@ -1682,7 +1651,7 @@
     apply(rule compact_imp_fip) apply(rule compact_frontier[OF compact_cball])
     defer apply(rule,rule,erule conjE) proof-
     fix f assume as:"f \<subseteq> ?k ` s" "finite f"
-    obtain c where c:"f = ?k ` c" "c\<subseteq>s" "finite c" using finite_subset_image[OF as] by auto
+    obtain c where c:"f = ?k ` c" "c\<subseteq>s" "finite c" using finite_subset_image[OF as(2,1)] by auto
     then obtain a b where ab:"a \<noteq> 0" "0 < b"  "\<forall>x\<in>convex hull c. b < a \<bullet> x"
       using separating_hyperplane_closed_0[OF convex_convex_hull, of c]
       using finite_imp_compact_convex_hull[OF c(3), THEN compact_imp_closed] and assms(2)
@@ -1867,7 +1836,7 @@
     have "m \<subseteq> X ` f" "p \<subseteq> X ` f" using mp(2) by auto
     then obtain g h where gh:"m = X ` g" "p = X ` h" "g \<subseteq> f" "h \<subseteq> f" unfolding subset_image_iff by auto 
     hence "f \<union> (g \<union> h) = f" by auto
-    hence f:"f = g \<union> h" using inj_on_image_eq_iff[of X f "g \<union> h"] and True
+    hence f:"f = g \<union> h" using inj_on_Un_image_eq_iff[of X f "g \<union> h"] and True
       unfolding mp(2)[unfolded image_Un[THEN sym] gh] by auto
     have *:"g \<inter> h = {}" using mp(1) unfolding gh using inj_on_image_Int[OF True gh(3,4)] by auto
     have "convex hull (X ` h) \<subseteq> \<Inter> g" "convex hull (X ` g) \<subseteq> \<Inter> h"
--- a/src/HOL/Library/Euclidean_Space.thy	Tue Jun 09 10:23:41 2009 -0700
+++ b/src/HOL/Library/Euclidean_Space.thy	Tue Jun 09 11:12:08 2009 -0700
@@ -1412,51 +1412,6 @@
 (* FIXME : Problem thm setsum_vmul[of _ "f:: 'a \<Rightarrow> real ^'n"]  ---
  Get rid of *s and use real_vector instead! Also prove that ^ creates a real_vector !! *)
 
-lemma setsum_add_split: assumes mn: "(m::nat) \<le> n + 1"
-  shows "setsum f {m..n + p} = setsum f {m..n} + setsum f {n + 1..n + p}"
-proof-
-  let ?A = "{m .. n}"
-  let ?B = "{n + 1 .. n + p}"
-  have eq: "{m .. n+p} = ?A \<union> ?B" using mn by auto
-  have d: "?A \<inter> ?B = {}" by auto
-  from setsum_Un_disjoint[of "?A" "?B" f] eq d show ?thesis by auto
-qed
-
-lemma setsum_natinterval_left:
-  assumes mn: "(m::nat) <= n"
-  shows "setsum f {m..n} = f m + setsum f {m + 1..n}"
-proof-
-  from mn have "{m .. n} = insert m {m+1 .. n}" by auto
-  then show ?thesis by auto
-qed
-
-lemma setsum_natinterval_difff:
-  fixes f:: "nat \<Rightarrow> ('a::ab_group_add)"
-  shows  "setsum (\<lambda>k. f k - f(k + 1)) {(m::nat) .. n} =
-          (if m <= n then f m - f(n + 1) else 0)"
-by (induct n, auto simp add: ring_simps not_le le_Suc_eq)
-
-lemmas setsum_restrict_set' = setsum_restrict_set[unfolded Int_def]
-
-lemma setsum_setsum_restrict:
-  "finite S \<Longrightarrow> finite T \<Longrightarrow> setsum (\<lambda>x. setsum (\<lambda>y. f x y) {y. y\<in> T \<and> R x y}) S = setsum (\<lambda>y. setsum (\<lambda>x. f x y) {x. x \<in> S \<and> R x y}) T"
-  apply (simp add: setsum_restrict_set'[unfolded mem_def] mem_def)
-  by (rule setsum_commute)
-
-lemma setsum_image_gen: assumes fS: "finite S"
-  shows "setsum g S = setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f ` S)"
-proof-
-  {fix x assume "x \<in> S" then have "{y. y\<in> f`S \<and> f x = y} = {f x}" by auto}
-  note th0 = this
-  have "setsum g S = setsum (\<lambda>x. setsum (\<lambda>y. g x) {y. y\<in> f`S \<and> f x = y}) S"
-    apply (rule setsum_cong2)
-    by (simp add: th0)
-  also have "\<dots> = setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f ` S)"
-    apply (rule setsum_setsum_restrict[OF fS])
-    by (rule finite_imageI[OF fS])
-  finally show ?thesis .
-qed
-
     (* FIXME: Here too need stupid finiteness assumption on T!!! *)
 lemma setsum_group:
   assumes fS: "finite S" and fT: "finite T" and fST: "f ` S \<subseteq> T"
--- a/src/HOL/Library/Sum_Of_Squares.thy	Tue Jun 09 10:23:41 2009 -0700
+++ b/src/HOL/Library/Sum_Of_Squares.thy	Tue Jun 09 11:12:08 2009 -0700
@@ -15,12 +15,10 @@
 
 *)
 
-
 method_setup sos = {* Scan.succeed (SIMPLE_METHOD' o Sos.sos_tac) *} 
   "Prove universal problems over the reals using sums of squares"
 
 text{* Tests -- commented since they work only when csdp is installed -- see above *}
-
 (*
 lemma "(3::real) * x + 7 * a < 4 & 3 < 2 * x \<Longrightarrow> a < 0" by sos
 
@@ -59,8 +57,8 @@
 (* ------------------------------------------------------------------------- *)
 (*
 lemma "2 <= (x::real) & x <= 4 & 2 <= y & y <= 4 & 2 <= z & z <= 4 --> 12 <= 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z)" by sos
+*)
 
-*)
 (* ------------------------------------------------------------------------- *)
 (* Inequality from sci.math (see "Leon-Sotelo, por favor").                  *)
 (* ------------------------------------------------------------------------- *)
--- a/src/HOL/Library/sum_of_squares.ML	Tue Jun 09 10:23:41 2009 -0700
+++ b/src/HOL/Library/sum_of_squares.ML	Tue Jun 09 11:12:08 2009 -0700
@@ -1619,8 +1619,44 @@
 | _ => ([],ct)
 
 fun core_sos_conv ctxt t = Drule.arg_cong_rule @{cterm Trueprop} (real_sos ctxt (Thm.dest_arg t) RS @{thm Eq_TrueI})
+
+val known_sos_constants = 
+  [@{term "op ==>"}, @{term "Trueprop"}, 
+   @{term "op -->"}, @{term "op &"}, @{term "op |"}, 
+   @{term "Not"}, @{term "op = :: bool => _"}, 
+   @{term "All :: (real => _) => _"}, @{term "Ex :: (real => _) => _"}, 
+   @{term "op = :: real => _"}, @{term "op < :: real => _"}, 
+   @{term "op <= :: real => _"}, 
+   @{term "op + :: real => _"}, @{term "op - :: real => _"}, 
+   @{term "op * :: real => _"}, @{term "uminus :: real => _"}, 
+   @{term "op / :: real => _"}, @{term "inverse :: real => _"},
+   @{term "op ^ :: real => _"}, @{term "abs :: real => _"}, 
+   @{term "min :: real => _"}, @{term "max :: real => _"},
+   @{term "0::real"}, @{term "1::real"}, @{term "number_of :: int => real"},
+   @{term "number_of :: int => nat"},
+   @{term "Int.Bit0"}, @{term "Int.Bit1"}, 
+   @{term "Int.Pls"}, @{term "Int.Min"}];
+
+fun check_sos kcts ct = 
+ let
+  val t = term_of ct
+  val _ = if not (null (Term.add_tfrees t []) 
+                  andalso null (Term.add_tvars t [])) 
+          then error "SOS: not sos. Additional type varables" else ()
+  val fs = Term.add_frees t []
+  val _ = if exists (fn ((_,T)) => not (T = @{typ "real"})) fs 
+          then error "SOS: not sos. Variables with type not real" else ()
+  val vs = Term.add_vars t []
+  val _ = if exists (fn ((_,T)) => not (T = @{typ "real"})) fs 
+          then error "SOS: not sos. Variables with type not real" else ()
+  val ukcs = subtract (fn (t,p) => Const p aconv t) kcts (Term.add_consts t [])
+  val _ = if  null ukcs then () 
+              else error ("SOSO: Unknown constants in Subgoal:" ^ commas (map fst ukcs))
+in () end
+
 fun core_sos_tac ctxt = CSUBGOAL (fn (ct, i) => 
-  let val (avs, p) = strip_all ct
+  let val _ = check_sos known_sos_constants ct
+      val (avs, p) = strip_all ct
       val th = standard (fold_rev forall_intr avs (real_sos ctxt (Thm.dest_arg p)))
   in rtac th i end);
 
@@ -1662,4 +1698,4 @@
 fun sos_tac ctxt = ObjectLogic.full_atomize_tac THEN' elim_denom_tac ctxt THEN' core_sos_tac ctxt
 
 
-end;
\ No newline at end of file
+end;
--- a/src/HOL/SetInterval.thy	Tue Jun 09 10:23:41 2009 -0700
+++ b/src/HOL/SetInterval.thy	Tue Jun 09 11:12:08 2009 -0700
@@ -859,6 +859,43 @@
           (if m <= n then f m - f(n + 1) else 0)"
 by (induct n, auto simp add: algebra_simps not_le le_Suc_eq)
 
+lemmas setsum_restrict_set' = setsum_restrict_set[unfolded Int_def]
+
+lemma setsum_setsum_restrict:
+  "finite S \<Longrightarrow> finite T \<Longrightarrow> setsum (\<lambda>x. setsum (\<lambda>y. f x y) {y. y\<in> T \<and> R x y}) S = setsum (\<lambda>y. setsum (\<lambda>x. f x y) {x. x \<in> S \<and> R x y}) T"
+  by (simp add: setsum_restrict_set'[unfolded mem_def] mem_def)
+     (rule setsum_commute)
+
+lemma setsum_image_gen: assumes fS: "finite S"
+  shows "setsum g S = setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f ` S)"
+proof-
+  { fix x assume "x \<in> S" then have "{y. y\<in> f`S \<and> f x = y} = {f x}" by auto }
+  hence "setsum g S = setsum (\<lambda>x. setsum (\<lambda>y. g x) {y. y\<in> f`S \<and> f x = y}) S"
+    by simp
+  also have "\<dots> = setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f ` S)"
+    by (rule setsum_setsum_restrict[OF fS finite_imageI[OF fS]])
+  finally show ?thesis .
+qed
+
+lemma setsum_multicount_gen:
+  assumes "finite s" "finite t" "\<forall>j\<in>t. (card {i\<in>s. R i j} = k j)"
+  shows "setsum (\<lambda>i. (card {j\<in>t. R i j})) s = setsum k t" (is "?l = ?r")
+proof-
+  have "?l = setsum (\<lambda>i. setsum (\<lambda>x.1) {j\<in>t. R i j}) s" by auto
+  also have "\<dots> = ?r" unfolding setsum_setsum_restrict[OF assms(1-2)]
+    using assms(3) by auto
+  finally show ?thesis .
+qed
+
+lemma setsum_multicount:
+  assumes "finite S" "finite T" "\<forall>j\<in>T. (card {i\<in>S. R i j} = k)"
+  shows "setsum (\<lambda>i. card {j\<in>T. R i j}) S = k * card T" (is "?l = ?r")
+proof-
+  have "?l = setsum (\<lambda>i. k) T" by(rule setsum_multicount_gen)(auto simp:assms)
+  also have "\<dots> = ?r" by(simp add: setsum_constant mult_commute)
+  finally show ?thesis by auto
+qed
+
 
 subsection{* Shifting bounds *}
 
--- a/src/HOL/Tools/int_arith.ML	Tue Jun 09 10:23:41 2009 -0700
+++ b/src/HOL/Tools/int_arith.ML	Tue Jun 09 11:12:08 2009 -0700
@@ -87,6 +87,12 @@
 val global_setup = Simplifier.map_simpset
   (fn simpset => simpset addsimprocs [fast_int_arith_simproc]);
 
+
+fun number_of thy T n =
+  if not (Sign.of_sort thy (T, @{sort number}))
+  then raise CTERM ("number_of", [])
+  else Numeral.mk_cnumber (Thm.ctyp_of thy T) n
+
 val setup =
   Lin_Arith.add_inj_thms [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
   #> Lin_Arith.add_lessD @{thm zless_imp_add1_zle}
@@ -95,6 +101,7 @@
   #> Lin_Arith.add_simprocs (Numeral_Simprocs.assoc_fold_simproc :: zero_one_idom_simproc
       :: Numeral_Simprocs.combine_numerals
       :: Numeral_Simprocs.cancel_numerals)
+  #> Lin_Arith.set_number_of number_of
   #> Lin_Arith.add_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT)
   #> Lin_Arith.add_discrete_type @{type_name Int.int}
 
--- a/src/HOL/Tools/lin_arith.ML	Tue Jun 09 10:23:41 2009 -0700
+++ b/src/HOL/Tools/lin_arith.ML	Tue Jun 09 11:12:08 2009 -0700
@@ -16,6 +16,8 @@
   val add_simprocs: simproc list -> Context.generic -> Context.generic
   val add_inj_const: string * typ -> Context.generic -> Context.generic
   val add_discrete_type: string -> Context.generic -> Context.generic
+  val set_number_of: (theory -> typ -> int -> cterm) -> Context.generic ->
+    Context.generic
   val setup: Context.generic -> Context.generic
   val global_setup: theory -> theory
   val split_limit: int Config.T
@@ -36,6 +38,7 @@
 val conjI = conjI;
 val notI = notI;
 val sym = sym;
+val trueI = TrueI;
 val not_lessD = @{thm linorder_not_less} RS iffD1;
 val not_leD = @{thm linorder_not_le} RS iffD1;
 
@@ -274,7 +277,6 @@
   | domain_is_nat (_ $ (Const ("Not", _) $ (Const (_, T) $ _ $ _))) = nT T
   | domain_is_nat _                                                 = false;
 
-val mk_number = HOLogic.mk_number;
 
 (*---------------------------------------------------------------------------*)
 (* the following code performs splitting of certain constants (e.g. min,     *)
@@ -752,23 +754,30 @@
 
 val map_data = Fast_Arith.map_data;
 
-fun map_inj_thms f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =
+fun map_inj_thms f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} =
   {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = f inj_thms,
-    lessD = lessD, neqE = neqE, simpset = simpset};
+    lessD = lessD, neqE = neqE, simpset = simpset, number_of = number_of};
 
-fun map_lessD f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =
+fun map_lessD f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} =
   {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms,
-    lessD = f lessD, neqE = neqE, simpset = simpset};
+    lessD = f lessD, neqE = neqE, simpset = simpset, number_of = number_of};
 
-fun map_simpset f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =
+fun map_simpset f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} =
   {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms,
-    lessD = lessD, neqE = neqE, simpset = f simpset};
+    lessD = lessD, neqE = neqE, simpset = f simpset, number_of = number_of};
+
+fun map_number_of f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} =
+  {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms,
+    lessD = lessD, neqE = neqE, simpset = simpset, number_of = f number_of};
 
 fun add_inj_thms thms = Fast_Arith.map_data (map_inj_thms (append thms));
 fun add_lessD thm = Fast_Arith.map_data (map_lessD (fn thms => thms @ [thm]));
 fun add_simps thms = Fast_Arith.map_data (map_simpset (fn simpset => simpset addsimps thms));
 fun add_simprocs procs = Fast_Arith.map_data (map_simpset (fn simpset => simpset addsimprocs procs));
 
+fun set_number_of f = Fast_Arith.map_data (map_number_of (K (serial (), f)))
+
+
 fun simple_tac ctxt = Fast_Arith.lin_arith_tac ctxt false;
 val lin_arith_tac = Fast_Arith.lin_arith_tac;
 val trace = Fast_Arith.trace;
@@ -778,13 +787,16 @@
    Most of the work is done by the cancel tactics. *)
 
 val init_arith_data =
-  Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, ...} =>
+  Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, number_of, ...} =>
    {add_mono_thms = @{thms add_mono_thms_ordered_semiring} @ @{thms add_mono_thms_ordered_field} @ add_mono_thms,
-    mult_mono_thms = @{thm mult_strict_left_mono} :: @{thm mult_left_mono} :: mult_mono_thms,
+    mult_mono_thms = @{thm mult_strict_left_mono} :: @{thm mult_left_mono} ::
+      @{lemma "a = b ==> c*a = c*b" by (rule arg_cong)} :: mult_mono_thms,
     inj_thms = inj_thms,
     lessD = lessD @ [@{thm "Suc_leI"}],
     neqE = [@{thm linorder_neqE_nat}, @{thm linorder_neqE_ordered_idom}],
     simpset = HOL_basic_ss
+      addsimps @{thms ring_distribs}
+      addsimps [@{thm if_True}, @{thm if_False}]
       addsimps
        [@{thm "monoid_add_class.add_0_left"},
         @{thm "monoid_add_class.add_0_right"},
@@ -795,7 +807,8 @@
       addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]
        (*abel_cancel helps it work in abstract algebraic domains*)
       addsimprocs Nat_Arith.nat_cancel_sums_add
-      addcongs [if_weak_cong]}) #>
+      addcongs [if_weak_cong],
+    number_of = number_of}) #>
   add_discrete_type @{type_name nat};
 
 fun add_arith_facts ss =
--- a/src/HOL/ex/Predicate_Compile_ex.thy	Tue Jun 09 10:23:41 2009 -0700
+++ b/src/HOL/ex/Predicate_Compile_ex.thy	Tue Jun 09 11:12:08 2009 -0700
@@ -7,9 +7,13 @@
   | "even n \<Longrightarrow> odd (Suc n)"
   | "odd n \<Longrightarrow> even (Suc n)"
 
+
+(*
 code_pred even
   using assms by (rule even.cases)
-
+*)
+setup {* Predicate_Compile.add_equations @{const_name even} *}
+thm odd.equation
 thm even.equation
 
 values "{x. even 2}"
@@ -22,8 +26,20 @@
     append_Nil: "append [] xs xs"
   | append_Cons: "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
 
+inductive rev
+where
+"rev [] []"
+| "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys"
+
+setup {* Predicate_Compile.add_equations @{const_name rev} *}
+
+thm rev.equation
+thm append.equation
+
+(*
 code_pred append
   using assms by (rule append.cases)
+*)
 
 thm append.equation
 
@@ -38,17 +54,22 @@
   | "f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) (x # ys) zs"
   | "\<not> f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) ys (x # zs)"
 
+setup {* Predicate_Compile.add_equations @{const_name partition} *}
+(*
 code_pred partition
   using assms by (rule partition.cases)
+*)
 
 thm partition.equation
 
 (*FIXME values 10 "{(ys, zs). partition (\<lambda>n. n mod 2 = 0)
   [0, Suc 0, 2, 3, 4, 5, 6, 7] ys zs}"*)
 
-
+setup {* Predicate_Compile.add_equations @{const_name tranclp} *}
+(*
 code_pred tranclp
   using assms by (rule tranclp.cases)
+*)
 
 thm tranclp.equation
 
@@ -56,13 +77,17 @@
     "succ 0 1"
   | "succ m n \<Longrightarrow> succ (Suc m) (Suc n)"
 
+setup {* Predicate_Compile.add_equations @{const_name succ} *} 
+(*
 code_pred succ
   using assms by (rule succ.cases)
-
+*)
 thm succ.equation
 
+(*
 values 20 "{n. tranclp succ 10 n}"
 values "{n. tranclp succ n 10}"
 values 20 "{(n, m). tranclp succ n m}"
+*)
 
 end
\ No newline at end of file
--- a/src/HOL/ex/predicate_compile.ML	Tue Jun 09 10:23:41 2009 -0700
+++ b/src/HOL/ex/predicate_compile.ML	Tue Jun 09 11:12:08 2009 -0700
@@ -7,21 +7,24 @@
 signature PREDICATE_COMPILE =
 sig
   type mode = int list option list * int list
-  val prove_equation: string -> mode option -> theory -> theory
-  val intro_rule: theory -> string -> mode -> thm
-  val elim_rule: theory -> string -> mode -> thm
-  val strip_intro_concl: term -> int -> term * (term list * term list)
-  val modename_of: theory -> string -> mode -> string
+  val add_equations_of: string list -> theory -> theory
+  val register_predicate : (thm list * thm * int) -> theory -> theory
+  val predfun_intro_of: theory -> string -> mode -> thm
+  val predfun_elim_of: theory -> string -> mode -> thm
+  val strip_intro_concl: int -> term -> term * (term list * term list)
+  val predfun_name_of: theory -> string -> mode -> string
+  val all_preds_of : theory -> string list
   val modes_of: theory -> string -> mode list
-  val pred_intros: theory -> string -> thm list
-  val get_nparams: theory -> string -> int
+  val intros_of: theory -> string -> thm list
+  val nparams_of: theory -> string -> int
   val setup: theory -> theory
   val code_pred: string -> Proof.context -> Proof.state
   val code_pred_cmd: string -> Proof.context -> Proof.state
-  val print_alternative_rules: theory -> theory (*FIXME diagnostic command?*)
+(*  val print_alternative_rules: theory -> theory (*FIXME diagnostic command?*) *)
   val do_proofs: bool ref
   val analyze_compr: theory -> term -> term
   val eval_ref: (unit -> term Predicate.pred) option ref
+  val add_equations : string -> theory -> theory
 end;
 
 structure Predicate_Compile : PREDICATE_COMPILE =
@@ -31,8 +34,6 @@
 
 (* debug stuff *)
 
-fun makestring _ = "?";   (* FIXME dummy *)
-
 fun tracing s = (if ! Toplevel.debug then Output.tracing s else ());
 
 fun print_tac s = (if ! Toplevel.debug then Tactical.print_tac s else Seq.single);
@@ -40,6 +41,12 @@
 
 val do_proofs = ref true;
 
+fun mycheat_tac thy i st =
+  (Tactic.rtac (SkipProof.make_thm thy (Var (("A", 0), propT))) i) st
+
+(* reference to preprocessing of InductiveSet package *)
+
+val ind_set_codegen_preproc = InductiveSetPackage.codegen_preproc;
 
 (** fundamentals **)
 
@@ -54,6 +61,10 @@
 fun mk_tupleT [] = HOLogic.unitT
   | mk_tupleT Ts = foldr1 HOLogic.mk_prodT Ts;
 
+fun dest_tupleT (Type (@{type_name Product_Type.unit}, [])) = []
+  | dest_tupleT (Type (@{type_name "*"}, [T1, T2])) = T1 :: (dest_tupleT T2)
+  | dest_tupleT t = [t]
+
 fun mk_tuple [] = HOLogic.unit
   | mk_tuple ts = foldr1 HOLogic.mk_prod ts;
 
@@ -61,9 +72,9 @@
   | dest_tuple (Const (@{const_name Pair}, _) $ t1 $ t2) = t1 :: (dest_tuple t2)
   | dest_tuple t = [t]
 
-fun mk_pred_enumT T = Type ("Predicate.pred", [T])
+fun mk_pred_enumT T = Type (@{type_name "Predicate.pred"}, [T])
 
-fun dest_pred_enumT (Type ("Predicate.pred", [T])) = T
+fun dest_pred_enumT (Type (@{type_name "Predicate.pred"}, [T])) = T
   | dest_pred_enumT T = raise TYPE ("dest_pred_enumT", [T], []);
 
 fun mk_Enum f =
@@ -98,120 +109,163 @@
 fun mk_not_pred t = let val T = mk_pred_enumT HOLogic.unitT
   in Const (@{const_name Predicate.not_pred}, T --> T) $ t end
 
+(* destruction of intro rules *)
+
+(* FIXME: look for other place where this functionality was used before *)
+fun strip_intro_concl nparams intro = let
+  val _ $ u = Logic.strip_imp_concl intro
+  val (pred, all_args) = strip_comb u
+  val (params, args) = chop nparams all_args
+in (pred, (params, args)) end
 
 (* data structures *)
 
-type mode = int list option list * int list;
+type mode = int list option list * int list; (*pmode FIMXE*)
+
+fun string_of_mode (iss, is) = space_implode " -> " (map
+  (fn NONE => "X"
+    | SOME js => enclose "[" "]" (commas (map string_of_int js)))
+       (iss @ [SOME is]));
+
+fun print_modes modes = Output.tracing ("Inferred modes:\n" ^
+  cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map
+    string_of_mode ms)) modes));
 
-val mode_ord = prod_ord (list_ord (option_ord (list_ord int_ord))) (list_ord int_ord);
+datatype predfun_data = PredfunData of {
+  name : string,
+  definition : thm,
+  intro : thm,
+  elim : thm
+};
+
+fun rep_predfun_data (PredfunData data) = data;
+fun mk_predfun_data (name, definition, intro, elim) =
+  PredfunData {name = name, definition = definition, intro = intro, elim = elim}
 
-structure PredModetab = TableFun(
-  type key = string * mode
-  val ord = prod_ord fast_string_ord mode_ord
-);
+datatype pred_data = PredData of {
+  intros : thm list,
+  elim : thm option,
+  nparams : int,
+  functions : (mode * predfun_data) list
+};
 
-
-(*FIXME scrap boilerplate*)
-
-structure IndCodegenData = TheoryDataFun
+fun rep_pred_data (PredData data) = data;
+fun mk_pred_data ((intros, elim, nparams), functions) =
+  PredData {intros = intros, elim = elim, nparams = nparams, functions = functions}
+fun map_pred_data f (PredData {intros, elim, nparams, functions}) =
+  mk_pred_data (f ((intros, elim, nparams), functions))
+  
+fun eq_option eq (NONE, NONE) = true
+  | eq_option eq (SOME x, SOME y) = eq (x, y)
+  | eq_option eq _ = false
+  
+fun eq_pred_data (PredData d1, PredData d2) = 
+  eq_list (Thm.eq_thm) (#intros d1, #intros d2) andalso
+  eq_option (Thm.eq_thm) (#elim d1, #elim d2) andalso
+  #nparams d1 = #nparams d2
+  
+structure PredData = TheoryDataFun
 (
-  type T = {names : string PredModetab.table,
-            modes : mode list Symtab.table,
-            function_defs : Thm.thm Symtab.table,
-            function_intros : Thm.thm Symtab.table,
-            function_elims : Thm.thm Symtab.table,
-            intro_rules : Thm.thm list Symtab.table,
-            elim_rules : Thm.thm Symtab.table,
-            nparams : int Symtab.table
-           }; (*FIXME: better group tables according to key*)
-      (* names: map from inductive predicate and mode to function name (string).
-         modes: map from inductive predicates to modes
-         function_defs: map from function name to definition
-         function_intros: map from function name to intro rule
-         function_elims: map from function name to elim rule
-         intro_rules: map from inductive predicate to alternative intro rules
-         elim_rules: map from inductive predicate to alternative elimination rule
-         nparams: map from const name to number of parameters (* assuming there exist intro and elimination rules *) 
-       *)
-  val empty = {names = PredModetab.empty,
-               modes = Symtab.empty,
-               function_defs = Symtab.empty,
-               function_intros = Symtab.empty,
-               function_elims = Symtab.empty,
-               intro_rules = Symtab.empty,
-               elim_rules = Symtab.empty,
-               nparams = Symtab.empty};
+  type T = pred_data Graph.T;
+  val empty = Graph.empty;
   val copy = I;
   val extend = I;
-  fun merge _ (r : T * T) = {names = PredModetab.merge (op =) (pairself #names r),
-                   modes = Symtab.merge (op =) (pairself #modes r),
-                   function_defs = Symtab.merge Thm.eq_thm (pairself #function_defs r),
-                   function_intros = Symtab.merge Thm.eq_thm (pairself #function_intros r),
-                   function_elims = Symtab.merge Thm.eq_thm (pairself #function_elims r),
-                   intro_rules = Symtab.merge ((forall Thm.eq_thm) o (op ~~)) (pairself #intro_rules r),
-                   elim_rules = Symtab.merge Thm.eq_thm (pairself #elim_rules r),
-                   nparams = Symtab.merge (op =) (pairself #nparams r)};
+  fun merge _ = Graph.merge eq_pred_data;
 );
 
-  fun map_names f thy = IndCodegenData.map
-    (fn x => {names = f (#names x), modes = #modes x, function_defs = #function_defs x,
-            function_intros = #function_intros x, function_elims = #function_elims x,
-            intro_rules = #intro_rules x, elim_rules = #elim_rules x,
-            nparams = #nparams x}) thy
+(* queries *)
+
+val lookup_pred_data = try rep_pred_data oo Graph.get_node o PredData.get; 
+
+fun the_pred_data thy name = case lookup_pred_data thy name
+ of NONE => error ("No such predicate " ^ quote name)  
+  | SOME data => data;
+
+val is_pred = is_some oo lookup_pred_data 
 
-  fun map_modes f thy = IndCodegenData.map
-    (fn x => {names = #names x, modes = f (#modes x), function_defs = #function_defs x,
-            function_intros = #function_intros x, function_elims = #function_elims x,
-            intro_rules = #intro_rules x, elim_rules = #elim_rules x,
-            nparams = #nparams x}) thy
+val all_preds_of = Graph.keys o PredData.get
+
+val intros_of = #intros oo the_pred_data
+
+fun the_elim_of thy name = case #elim (the_pred_data thy name)
+ of NONE => error ("No elimination rule for predicate " ^ quote name)
+  | SOME thm => thm 
+  
+val has_elim = is_some o #elim oo the_pred_data;
+
+val nparams_of = #nparams oo the_pred_data
 
-  fun map_function_defs f thy = IndCodegenData.map
-    (fn x => {names = #names x, modes = #modes x, function_defs = f (#function_defs x),
-            function_intros = #function_intros x, function_elims = #function_elims x,
-            intro_rules = #intro_rules x, elim_rules = #elim_rules x,
-            nparams = #nparams x}) thy 
-  
-  fun map_function_elims f thy = IndCodegenData.map
-    (fn x => {names = #names x, modes = #modes x, function_defs = #function_defs x,
-            function_intros = #function_intros x, function_elims = f (#function_elims x),
-            intro_rules = #intro_rules x, elim_rules = #elim_rules x,
-            nparams = #nparams x}) thy
+val modes_of = (map fst) o #functions oo the_pred_data
+
+fun all_modes_of thy = map (fn name => (name, modes_of thy name)) (all_preds_of thy) 
+
+val is_compiled = not o null o #functions oo the_pred_data
+
+fun lookup_predfun_data thy name mode =
+  Option.map rep_predfun_data (AList.lookup (op =)
+  (#functions (the_pred_data thy name)) mode)
 
-  fun map_function_intros f thy = IndCodegenData.map
-    (fn x => {names = #names x, modes = #modes x, function_defs = #function_defs x,
-            function_intros = f (#function_intros x), function_elims = #function_elims x,
-            intro_rules = #intro_rules x, elim_rules = #elim_rules x,
-            nparams = #nparams x}) thy
+fun the_predfun_data thy name mode = case lookup_predfun_data thy name mode
+ of NONE => error ("No such mode" ^ string_of_mode mode)
+  | SOME data => data;
+
+val predfun_name_of = #name ooo the_predfun_data
+
+val predfun_definition_of = #definition ooo the_predfun_data
+
+val predfun_intro_of = #intro ooo the_predfun_data
+
+val predfun_elim_of = #elim ooo the_predfun_data
+
 
-  fun map_intro_rules f thy = IndCodegenData.map
-    (fn x => {names = #names x, modes = #modes x, function_defs = #function_defs x,
-            function_intros = #function_intros x, function_elims = #function_elims x,
-            intro_rules = f (#intro_rules x), elim_rules = #elim_rules x,
-            nparams = #nparams x}) thy 
-  
-  fun map_elim_rules f thy = IndCodegenData.map
-    (fn x => {names = #names x, modes = #modes x, function_defs = #function_defs x,
-            function_intros = #function_intros x, function_elims = #function_elims x,
-            intro_rules = #intro_rules x, elim_rules = f (#elim_rules x),
-            nparams = #nparams x}) thy
+(* replaces print_alternative_rules *)
+(* TODO:
+fun print_alternative_rules thy = let
+    val d = IndCodegenData.get thy
+    val preds = (Symtab.keys (#intro_rules d)) union (Symtab.keys (#elim_rules d))
+    val _ = tracing ("preds: " ^ (makestring preds))
+    fun print pred = let
+      val _ = tracing ("predicate: " ^ pred)
+      val _ = tracing ("introrules: ")
+      val _ = fold (fn thm => fn u => tracing (makestring thm))
+        (rev (Symtab.lookup_list (#intro_rules d) pred)) ()
+      val _ = tracing ("casesrule: ")
+      val _ = tracing (makestring (Symtab.lookup (#elim_rules d) pred))
+    in () end
+    val _ = map print preds
+ in thy end;
+*)
+
+(* updaters *)
+
+fun add_predfun name mode data = let
+    val add = apsnd (cons (mode, mk_predfun_data data))
+  in PredData.map (Graph.map_node name (map_pred_data add)) end
 
-  fun map_nparams f thy = IndCodegenData.map
-    (fn x => {names = #names x, modes = #modes x, function_defs = #function_defs x,
-            function_intros = #function_intros x, function_elims = #function_elims x,
-            intro_rules = #intro_rules x, elim_rules = #elim_rules x,
-            nparams = f (#nparams x)}) thy
+fun add_intro thm = let
+   val (name, _) = dest_Const (fst (strip_intro_concl 0 (prop_of thm)))
+   fun set (intros, elim, nparams) = (thm::intros, elim, nparams)  
+  in PredData.map (Graph.map_node name (map_pred_data (apfst set))) end
+
+fun set_elim thm = let
+    val (name, _) = dest_Const (fst 
+      (strip_comb (HOLogic.dest_Trueprop (hd (prems_of thm)))))
+    fun set (intros, _, nparams) = (intros, SOME thm, nparams)  
+  in PredData.map (Graph.map_node name (map_pred_data (apfst set))) end
 
-(* removes first subgoal *)
-fun mycheat_tac thy i st =
-  (Tactic.rtac (SkipProof.make_thm thy (Var (("A", 0), propT))) i) st
-
-(* Lightweight mode analysis **********************************************)
+fun set_nparams name nparams = let
+    fun set (intros, elim, _ ) = (intros, elim, nparams) 
+  in PredData.map (Graph.map_node name (map_pred_data (apfst set))) end
 
-(**************************************************************************)
-(* source code from old code generator ************************************)
+fun register_predicate (intros, elim, nparams) = let
+    val (name, _) = dest_Const (fst (strip_intro_concl nparams (prop_of (hd intros))))
+    fun set _ = (intros, SOME elim, nparams)
+  in PredData.map (Graph.new_node (name, mk_pred_data ((intros, SOME elim, nparams), []))) end
 
-(**** check if a term contains only constructor functions ****)
+  
+(* Mode analysis *)
 
+(*** check if a term contains only constructor functions ***)
 fun is_constrt thy =
   let
     val cnstrs = flat (maps
@@ -225,23 +279,11 @@
       | _ => false)
   in check end;
 
-(**** check if a type is an equality type (i.e. doesn't contain fun)
-  FIXME this is only an approximation ****)
-
+(*** check if a type is an equality type (i.e. doesn't contain fun)
+  FIXME this is only an approximation ***)
 fun is_eqT (Type (s, Ts)) = s <> "fun" andalso forall is_eqT Ts
   | is_eqT _ = true;
 
-(**** mode inference ****)
-
-fun string_of_mode (iss, is) = space_implode " -> " (map
-  (fn NONE => "X"
-    | SOME js => enclose "[" "]" (commas (map string_of_int js)))
-       (iss @ [SOME is]));
-
-fun print_modes modes = tracing ("Inferred modes:\n" ^
-  cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map
-    string_of_mode ms)) modes));
-
 fun term_vs tm = fold_aterms (fn Free (x, T) => cons x | _ => I) tm [];
 val terms_vs = distinct (op =) o maps term_vs;
 
@@ -265,16 +307,52 @@
        let val is = subsets (i+1) j
        in merge (map (fn ks => i::ks) is) is end
      else [[]];
-
+     
+(* FIXME: should be in library - map_prod *)
 fun cprod ([], ys) = []
   | cprod (x :: xs, ys) = map (pair x) ys @ cprod (xs, ys);
 
 fun cprods xss = foldr (map op :: o cprod) [[]] xss;
 
 datatype hmode = Mode of mode * int list * hmode option list; (*FIXME don't understand
-  why there is another mode type!?*)
+  why there is another mode type tmode !?*)
 
-fun modes_of_term modes t =
+  
+(*TODO: cleanup function and put together with modes_of_term *)
+fun modes_of_param default modes t = let
+    val (vs, t') = strip_abs t
+    val b = length vs
+    fun mk_modes name args = Option.map (maps (fn (m as (iss, is)) =>
+        let
+          val (args1, args2) =
+            if length args < length iss then
+              error ("Too few arguments for inductive predicate " ^ name)
+            else chop (length iss) args;
+          val k = length args2;
+          val perm = map (fn i => (find_index_eq (Bound (b - i)) args2) + 1)
+            (1 upto b)  
+          val partial_mode = (1 upto k) \\ perm
+        in
+          if not (partial_mode subset is) then [] else
+          let
+            val is' = 
+            (fold_index (fn (i, j) => if j mem is then cons (i + 1) else I) perm [])
+            |> fold (fn i => if i > k then cons (i - k + b) else I) is
+              
+           val res = map (fn x => Mode (m, is', x)) (cprods (map
+            (fn (NONE, _) => [NONE]
+              | (SOME js, arg) => map SOME (filter
+                  (fn Mode (_, js', _) => js=js') (modes_of_term modes arg)))
+                    (iss ~~ args1)))
+          in res end
+        end)) (AList.lookup op = modes name)
+  in case strip_comb t' of
+    (Const (name, _), args) => the_default default (mk_modes name args)
+    | (Var ((name, _), _), args) => the (mk_modes name args)
+    | (Free (name, _), args) => the (mk_modes name args)
+    | _ => default end
+  
+and modes_of_term modes t =
   let
     val ks = 1 upto length (binder_types (fastype_of t));
     val default = [Mode (([], ks), ks, [])];
@@ -301,6 +379,7 @@
       (Const (name, _), args) => the_default default (mk_modes name args)
     | (Var ((name, _), _), args) => the (mk_modes name args)
     | (Free (name, _), args) => the (mk_modes name args)
+    | (Abs _, []) => modes_of_param default modes t 
     | _ => default)
   end
 
@@ -376,10 +455,7 @@
       subsets 1 k))) arities);
 
 
-(*****************************************************************************************)
-(**** end of old source code *************************************************************)
-(*****************************************************************************************)
-(**** term construction ****)
+(* term construction *)
 
 (* for simple modes (e.g. parameters) only: better call it param_funT *)
 (* or even better: remove it and only use funT'_of - some modifications to funT'_of necessary *) 
@@ -400,22 +476,22 @@
 
 
 fun mk_v (names, vs) s T = (case AList.lookup (op =) vs s of
-      NONE => ((names, (s, [])::vs), Free (s, T))
+      NONE => (Free (s, T), (names, (s, [])::vs))
     | SOME xs =>
         let
           val s' = Name.variant names s;
           val v = Free (s', T)
         in
-          ((s'::names, AList.update (op =) (s, v::xs) vs), v)
+          (v, (s'::names, AList.update (op =) (s, v::xs) vs))
         end);
 
-fun distinct_v (nvs, Free (s, T)) = mk_v nvs s T
-  | distinct_v (nvs, t $ u) =
+fun distinct_v (Free (s, T)) nvs = mk_v nvs s T
+  | distinct_v (t $ u) nvs =
       let
-        val (nvs', t') = distinct_v (nvs, t);
-        val (nvs'', u') = distinct_v (nvs', u);
-      in (nvs'', t' $ u') end
-  | distinct_v x = x;
+        val (t', nvs') = distinct_v t nvs;
+        val (u', nvs'') = distinct_v u nvs';
+      in (t' $ u', nvs'') end
+  | distinct_v x nvs = (x, nvs);
 
 fun compile_match thy eqs eqs' out_ts success_t =
   let 
@@ -439,15 +515,6 @@
        (v', mk_empty U')]))
   end;
 
-fun modename_of thy name mode = let
-    val v = (PredModetab.lookup (#names (IndCodegenData.get thy)) (name, mode))
-  in if (is_some v) then the v (*FIXME use case here*)
-     else error ("fun modename_of - definition not found: name: " ^ name ^ " mode: " ^  (makestring mode))
-  end
-
-fun modes_of thy =
-  these o Symtab.lookup ((#modes o IndCodegenData.get) thy);
-
 (*FIXME function can be removed*)
 fun mk_funcomp f t =
   let
@@ -459,20 +526,58 @@
     fold_rev lambda vs (f (list_comb (t, vs)))
   end;
 
-fun compile_param thy modes (NONE, t) = t
-  | compile_param thy modes (m as SOME (Mode ((iss, is'), is, ms)), t) = let
-    val (f, args) = strip_comb t
-    val (params, args') = chop (length ms) args
-    val params' = map (compile_param thy modes) (ms ~~ params)
-    val f' = case f of
+
+
+fun compile_param_ext thy modes (NONE, t) = t
+  | compile_param_ext thy modes (m as SOME (Mode ((iss, is'), is, ms)), t) =
+      let
+        val (vs, u) = strip_abs t
+        val (ivs, ovs) = get_args is vs    
+        val (f, args) = strip_comb u
+        val (params, args') = chop (length ms) args
+        val (inargs, outargs) = get_args is' args'
+        val b = length vs
+        val perm = map (fn i => (find_index_eq (Bound (b - i)) args') + 1) (1 upto b)
+        val outp_perm =
+          snd (get_args is perm)
+          |> map (fn i => i - length (filter (fn x => x < i) is'))
+        val names = [] (* TODO *)
+        val out_names = Name.variant_list names (replicate (length outargs) "x")
+        val f' = case f of
+            Const (name, T) =>
+              if AList.defined op = modes name then
+                Const (predfun_name_of thy name (iss, is'), funT'_of (iss, is') T)
+              else error "compile param: Not an inductive predicate with correct mode"
+          | Free (name, T) => Free (name, funT_of T (SOME is'))
+        val outTs = dest_tupleT (dest_pred_enumT (body_type (fastype_of f')))
+        val out_vs = map Free (out_names ~~ outTs)
+        val params' = map (compile_param thy modes) (ms ~~ params)
+        val f_app = list_comb (f', params' @ inargs)
+        val single_t = (mk_single (mk_tuple (map (fn i => nth out_vs (i - 1)) outp_perm)))
+        val match_t = compile_match thy [] [] out_vs single_t
+      in list_abs (ivs,
+        mk_bind (f_app, match_t))
+      end
+  | compile_param_ext _ _ _ = error "compile params"
+
+and compile_param thy modes (NONE, t) = t
+ | compile_param thy modes (m as SOME (Mode ((iss, is'), is, ms)), t) =
+   (case t of
+     Abs _ => compile_param_ext thy modes (m, t)
+   |  _ => let
+     val (f, args) = strip_comb t
+     val (params, args') = chop (length ms) args
+     val params' = map (compile_param thy modes) (ms ~~ params)
+     val f' = case f of
         Const (name, T) =>
           if AList.defined op = modes name then
-            Const (modename_of thy name (iss, is'), funT'_of (iss, is') T)
+             Const (predfun_name_of thy name (iss, is'), funT'_of (iss, is') T)
           else error "compile param: Not an inductive predicate with correct mode"
       | Free (name, T) => Free (name, funT_of T (SOME is'))
-    in list_comb (f', params' @ args') end
-  | compile_param _ _ _ = error "compile params"
-
+   in list_comb (f', params' @ args') end)
+ | compile_param _ _ _ = error "compile params"
+  
+  
 fun compile_expr thy modes (SOME (Mode (mode, is, ms)), t) =
       (case strip_comb t of
          (Const (name, T), params) =>
@@ -481,8 +586,7 @@
                val (Ts, Us) = get_args is
                  (curry Library.drop (length ms) (fst (strip_type T)))
                val params' = map (compile_param thy modes) (ms ~~ params)
-               val mode_id = modename_of thy name mode
-             in list_comb (Const (mode_id, ((map fastype_of params') @ Ts) --->
+             in list_comb (Const (predfun_name_of thy name mode, ((map fastype_of params') @ Ts) --->
                mk_pred_enumT (mk_tupleT Us)), params')
              end
            else error "not a valid inductive expression"
@@ -499,25 +603,25 @@
     val modes' = modes @ List.mapPartial
       (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)]))
         (param_vs ~~ iss);
-    fun check_constrt ((names, eqs), t) =
-      if is_constrt thy t then ((names, eqs), t) else
+    fun check_constrt t (names, eqs) =
+      if is_constrt thy t then (t, (names, eqs)) else
         let
           val s = Name.variant names "x";
           val v = Free (s, fastype_of t)
-        in ((s::names, HOLogic.mk_eq (v, t)::eqs), v) end;
+        in (v, (s::names, HOLogic.mk_eq (v, t)::eqs)) end;
 
     val (in_ts, out_ts) = get_args is ts;
-    val ((all_vs', eqs), in_ts') =
-      (*FIXME*) Library.foldl_map check_constrt ((all_vs, []), in_ts);
+    val (in_ts', (all_vs', eqs)) =
+      fold_map check_constrt in_ts (all_vs, []);
 
     fun compile_prems out_ts' vs names [] =
           let
-            val ((names', eqs'), out_ts'') =
-              (*FIXME*) Library.foldl_map check_constrt ((names, []), out_ts');
-            val (nvs, out_ts''') = (*FIXME*) Library.foldl_map distinct_v
-              ((names', map (rpair []) vs), out_ts'');
+            val (out_ts'', (names', eqs')) =
+              fold_map check_constrt out_ts' (names, []);
+            val (out_ts''', (names'', constr_vs)) = fold_map distinct_v
+              out_ts'' (names', map (rpair []) vs);
           in
-            compile_match thy (snd nvs) (eqs @ eqs') out_ts'''
+            compile_match thy constr_vs (eqs @ eqs') out_ts'''
               (mk_single (mk_tuple out_ts))
           end
       | compile_prems out_ts vs names ps =
@@ -526,16 +630,16 @@
             val SOME (p, mode as SOME (Mode (_, js, _))) =
               select_mode_prem thy modes' vs' ps
             val ps' = filter_out (equal p) ps
-            val ((names', eqs), out_ts') =
-              (*FIXME*) Library.foldl_map check_constrt ((names, []), out_ts)
-            val (nvs, out_ts'') = (*FIXME*) Library.foldl_map distinct_v
-              ((names', map (rpair []) vs), out_ts')
+            val (out_ts', (names', eqs)) =
+              fold_map check_constrt out_ts (names, [])
+            val (out_ts'', (names'', constr_vs')) = fold_map distinct_v
+              out_ts' ((names', map (rpair []) vs))
             val (compiled_clause, rest) = case p of
                Prem (us, t) =>
                  let
                    val (in_ts, out_ts''') = get_args js us;
                    val u = list_comb (compile_expr thy modes (mode, t), in_ts)
-                   val rest = compile_prems out_ts''' vs' (fst nvs) ps'
+                   val rest = compile_prems out_ts''' vs' names'' ps'
                  in
                    (u, rest)
                  end
@@ -543,18 +647,18 @@
                  let
                    val (in_ts, out_ts''') = get_args js us
                    val u = list_comb (compile_expr thy modes (mode, t), in_ts)
-                   val rest = compile_prems out_ts''' vs' (fst nvs) ps'
+                   val rest = compile_prems out_ts''' vs' names'' ps'
                  in
                    (mk_not_pred u, rest)
                  end
              | Sidecond t =>
                  let
-                   val rest = compile_prems [] vs' (fst nvs) ps';
+                   val rest = compile_prems [] vs' names'' ps';
                  in
                    (mk_if_predenum t, rest)
                  end
           in
-            compile_match thy (snd nvs) eqs out_ts'' 
+            compile_match thy constr_vs' eqs out_ts'' 
               (mk_bind (compiled_clause, rest))
           end
     val prem_t = compile_prems in_ts' param_vs all_vs' ps;
@@ -574,7 +678,7 @@
     val cl_ts =
       map (fn cl => compile_clause thy
         all_vs param_vs modes mode cl (mk_tuple xs)) cls;
-    val mode_id = modename_of thy s mode
+    val mode_id = predfun_name_of thy s mode
   in
     HOLogic.mk_Trueprop (HOLogic.mk_eq
       (list_comb (Const (mode_id, (Ts1' @ Us1) --->
@@ -588,26 +692,13 @@
     map (compile_pred thy all_vs param_vs modes s T cls)
       ((the o AList.lookup (op =) modes) s)) preds;
 
-(* end of term construction ******************************************************)
 
 (* special setup for simpset *)                  
 val HOL_basic_ss' = HOL_basic_ss setSolver 
   (mk_solver "all_tac_solver" (fn _ => fn _ => all_tac))
 
 
-(* misc: constructing and proving tupleE rules ***********************************)
-
-
-(* Creating definitions of functional programs 
-   and proving intro and elim rules **********************************************) 
-
-fun is_ind_pred thy c = 
-  (can (InductivePackage.the_inductive (ProofContext.init thy)) c) orelse
-  (c mem_string (Symtab.keys (#intro_rules (IndCodegenData.get thy))))
-
-fun get_name_of_ind_calls_of_clauses thy preds intrs =
-    fold Term.add_consts intrs [] |> map fst
-    |> filter_out (member (op =) preds) |> filter (is_ind_pred thy)
+(* Definition of executable functions and their intro and elim rules *)
 
 fun print_arities arities = tracing ("Arities:\n" ^
   cat_lines (map (fn (s, (ks, k)) => s ^ ": " ^
@@ -628,7 +719,7 @@
   (t, argnames @ names)
 end;
 
-fun create_intro_rule nparams mode defthm mode_id funT pred thy =
+fun create_intro_elim_rule nparams mode defthm mode_id funT pred thy =
 let
   val Ts = binder_types (fastype_of pred)
   val funtrm = Const (mode_id, funT)
@@ -654,11 +745,8 @@
   val P = HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT));
   val elimtrm = Logic.list_implies ([funpropE, Logic.mk_implies (predprop, P)], P)
   val elimthm = Goal.prove (ProofContext.init thy) (argnames @ ["y", "P"]) [] elimtrm (fn {...} => unfolddef_tac)
-in
-  map_function_intros (Symtab.update_new (mode_id, introthm)) thy
-  |> map_function_elims (Symtab.update_new (mode_id, elimthm))
-  |> PureThy.store_thm (Binding.name (Long_Name.base_name mode_id ^ "I"), introthm) |> snd
-  |> PureThy.store_thm (Binding.name (Long_Name.base_name mode_id ^ "E"), elimthm)  |> snd
+in 
+  (introthm, elimthm)
 end;
 
 fun create_definitions preds nparams (name, modes) thy =
@@ -694,12 +782,13 @@
       val mode_id = Sign.full_bname thy (Long_Name.base_name mode_id)
       val lhs = list_comb (Const (mode_id, funT), xparams @ xins)
       val def = Logic.mk_equals (lhs, predterm)
-      val ([defthm], thy') = thy |>
+      val ([definition], thy') = thy |>
         Sign.add_consts_i [(Binding.name (Long_Name.base_name mode_id), funT, NoSyn)] |>
         PureThy.add_defs false [((Binding.name (Long_Name.base_name mode_id ^ "_def"), def), [])]
-      in thy' |> map_names (PredModetab.update_new ((name, mode), mode_id))
-           |> map_function_defs (Symtab.update_new (mode_id, defthm))
-           |> create_intro_rule nparams mode defthm mode_id funT (Const (name, T))
+      val (intro, elim) = create_intro_elim_rule nparams mode definition mode_id funT (Const (name, T)) thy'
+      in thy' |> add_predfun name mode (mode_id, definition, intro, elim)
+        |> PureThy.store_thm (Binding.name (Long_Name.base_name mode_id ^ "I"), intro) |> snd
+        |> PureThy.store_thm (Binding.name (Long_Name.base_name mode_id ^ "E"), elim)  |> snd
       end;
   in
     fold create_definition modes thy
@@ -708,29 +797,6 @@
 (**************************************************************************************)
 (* Proving equivalence of term *)
 
-
-fun intro_rule thy pred mode = modename_of thy pred mode
-    |> Symtab.lookup (#function_intros (IndCodegenData.get thy)) |> the
-
-fun elim_rule thy pred mode = modename_of thy pred mode
-    |> Symtab.lookup (#function_elims (IndCodegenData.get thy)) |> the
-
-fun pred_intros thy predname = let
-    fun is_intro_of pred intro = let
-      val const = fst (strip_comb (HOLogic.dest_Trueprop (concl_of intro)))
-    in (fst (dest_Const const) = pred) end;
-    val d = IndCodegenData.get thy
-  in
-    if (Symtab.defined (#intro_rules d) predname) then
-      rev (Symtab.lookup_list (#intro_rules d) predname)
-    else
-      InductivePackage.the_inductive (ProofContext.init thy) predname
-      |> snd |> #intrs |> filter (is_intro_of predname)
-  end
-
-fun function_definition thy pred mode =
-  modename_of thy pred mode |> Symtab.lookup (#function_defs (IndCodegenData.get thy)) |> the
-
 fun is_Type (Type _) = true
   | is_Type _ = false
 
@@ -793,11 +859,12 @@
     val (params, _) = chop (length ms) args
     val f_tac = case f of
         Const (name, T) => simp_tac (HOL_basic_ss addsimps 
-           @{thm eval_pred}::function_definition thy name mode::[]) 1
+           (@{thm eval_pred}::(predfun_definition_of thy name mode)::
+           @{thm "Product_Type.split_conv"}::[])) 1
       | Free _ => all_tac
+      | Abs _ => error "TODO: implement here"
   in  
     print_tac "before simplification in prove_args:"
-    THEN debug_tac ("mode" ^ (makestring mode))
     THEN f_tac
     THEN print_tac "after simplification in prove_args"
     (* work with parameter arguments *)
@@ -809,25 +876,19 @@
   (case strip_comb t of
     (Const (name, T), args) =>
       if AList.defined op = modes name then (let
-          val introrule = intro_rule thy name mode
+          val introrule = predfun_intro_of thy name mode
           (*val (in_args, out_args) = get_args is us
           val (pred, rargs) = strip_comb (HOLogic.dest_Trueprop
             (hd (Logic.strip_imp_prems (prop_of introrule))))
           val nparams = length ms (* get_nparams thy (fst (dest_Const pred)) *)
           val (_, args) = chop nparams rargs
-          val _ = tracing ("args: " ^ (makestring args))
           val subst = map (pairself (cterm_of thy)) (args ~~ us)
-          val _ = tracing ("subst: " ^ (makestring subst))
           val inst_introrule = Drule.cterm_instantiate subst introrule*)
          (* the next line is old and probably wrong *)
           val (args1, args2) = chop (length ms) args
-          val _ = tracing ("premposition: " ^ (makestring premposition))
         in
         rtac @{thm bindI} 1
         THEN print_tac "before intro rule:"
-        THEN debug_tac ("mode" ^ (makestring mode))
-        THEN debug_tac (makestring introrule)
-        THEN debug_tac ("premposition: " ^ (makestring premposition))
         (* for the right assumption in first position *)
         THEN rotate_tac premposition 1
         THEN rtac introrule 1
@@ -854,9 +915,8 @@
   val simprules = @{thm "unit.cases"} :: @{thm "prod.cases"} :: (flat (map get_case_rewrite out_ts))
 (* replace TRY by determining if it necessary - are there equations when calling compile match? *)
 in
-  print_tac ("before prove_match rewriting: simprules = " ^ (makestring simprules))
    (* make this simpset better! *)
-  THEN asm_simp_tac (HOL_basic_ss' addsimps simprules) 1
+  asm_simp_tac (HOL_basic_ss' addsimps simprules) 1
   THEN print_tac "after prove_match:"
   THEN (DETERM (TRY (EqSubst.eqsubst_tac (ProofContext.init thy) [0] [@{thm "HOL.if_P"}] 1
          THEN (REPEAT_DETERM (rtac @{thm conjI} 1 THEN (SOLVED (asm_simp_tac HOL_basic_ss 1))))
@@ -866,26 +926,22 @@
 
 (* corresponds to compile_fun -- maybe call that also compile_sidecond? *)
 
-fun prove_sidecond thy modes t = let
-  val _ = tracing ("prove_sidecond:" ^ (makestring t))
-  fun preds_of t nameTs = case strip_comb t of 
-    (f as Const (name, T), args) =>
-      if AList.defined (op =) modes name then (name, T) :: nameTs
-        else fold preds_of args nameTs
-    | _ => nameTs
-  val preds = preds_of t []
-  
-  val _ = tracing ("preds: " ^ (makestring preds))
-  val defs = map
-    (fn (pred, T) => function_definition thy pred ([], (1 upto (length (binder_types T)))))
-      preds
-  val _ = tracing ("defs: " ^ (makestring defs))
-in 
-   (* remove not_False_eq_True when simpset in prove_match is better *)
-   simp_tac (HOL_basic_ss addsimps @{thm not_False_eq_True} :: @{thm eval_pred} :: defs) 1 
-   (* need better control here! *)
-   THEN print_tac "after sidecond simplification"
-   end
+fun prove_sidecond thy modes t =
+  let
+    fun preds_of t nameTs = case strip_comb t of 
+      (f as Const (name, T), args) =>
+        if AList.defined (op =) modes name then (name, T) :: nameTs
+          else fold preds_of args nameTs
+      | _ => nameTs
+    val preds = preds_of t []
+    val defs = map
+      (fn (pred, T) => predfun_definition_of thy pred ([], (1 upto (length (binder_types T)))))
+        preds
+  in 
+    (* remove not_False_eq_True when simpset in prove_match is better *)
+    simp_tac (HOL_basic_ss addsimps @{thm not_False_eq_True} :: @{thm eval_pred} :: defs) 1 
+    (* need better control here! *)
+  end
 
 fun prove_clause thy nargs all_vs param_vs modes (iss, is) (ts, ps) = let
   val modes' = modes @ List.mapPartial
@@ -932,13 +988,10 @@
             val name = (case strip_comb t of (Const (c, _), _) => SOME c | _ => NONE)
             val (_, params) = strip_comb t
           in
-            print_tac "before negated clause:"
-            THEN rtac @{thm bindI} 1
+            rtac @{thm bindI} 1
             THEN (if (is_some name) then
-                simp_tac (HOL_basic_ss addsimps [function_definition thy (the name) (iss, js)]) 1
+                simp_tac (HOL_basic_ss addsimps [predfun_definition_of thy (the name) (iss, js)]) 1
                 THEN rtac @{thm not_predI} 1
-                THEN print_tac "after neg. intro rule"
-                THEN print_tac ("t = " ^ (makestring t))
                 (* FIXME: work with parameter arguments *)
                 THEN (EVERY (map (prove_param thy modes) (param_modes ~~ params)))
               else
@@ -967,43 +1020,17 @@
   | select_sup _ 1 = [rtac @{thm supI1}]
   | select_sup n i = (rtac @{thm supI2})::(select_sup (n - 1) (i - 1));
 
-(* FIXME: This function relies on the derivation of an induction rule *)
-fun get_nparams thy s = let
-    val _ = tracing ("get_nparams: " ^ s)
-  in
-  if Symtab.defined (#nparams (IndCodegenData.get thy)) s then
-    the (Symtab.lookup (#nparams (IndCodegenData.get thy)) s) 
-  else
-    case try (InductivePackage.the_inductive (ProofContext.init thy)) s of
-      SOME info => info |> snd |> #raw_induct |> Thm.unvarify
-        |> InductivePackage.params_of |> length
-    | NONE => 0 (* default value *)
-  end
-
-val ind_set_codegen_preproc = InductiveSetPackage.codegen_preproc;
-
-fun pred_elim thy predname =
-  if (Symtab.defined (#elim_rules (IndCodegenData.get thy)) predname) then
-    the (Symtab.lookup (#elim_rules (IndCodegenData.get thy)) predname)
-  else
-    (let
-      val ind_result = InductivePackage.the_inductive (ProofContext.init thy) predname
-      val index = find_index (fn s => s = predname) (#names (fst ind_result))
-    in nth (#elims (snd ind_result)) index end)
-
 fun prove_one_direction thy all_vs param_vs modes clauses ((pred, T), mode) = let
-  val elim_rule = the (Symtab.lookup (#function_elims (IndCodegenData.get thy)) (modename_of thy pred mode))
 (*  val ind_result = InductivePackage.the_inductive (ProofContext.init thy) pred
   val index = find_index (fn s => s = pred) (#names (fst ind_result))
   val (_, T) = dest_Const (nth (#preds (snd ind_result)) index) *)
-  val nargs = length (binder_types T) - get_nparams thy pred
+  val nargs = length (binder_types T) - nparams_of thy pred
   val pred_case_rule = singleton (ind_set_codegen_preproc thy)
-    (preprocess_elim thy nargs (pred_elim thy pred))
+    (preprocess_elim thy nargs (the_elim_of thy pred))
   (* FIXME preprocessor |> Simplifier.full_simplify (HOL_basic_ss addsimps [@ {thm Predicate.memb_code}])*)
-  val _ = tracing ("pred_case_rule " ^ (makestring pred_case_rule))
 in
   REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"}))
-  THEN etac elim_rule 1
+  THEN etac (predfun_elim_of thy pred mode) 1
   THEN etac pred_case_rule 1
   THEN (EVERY (map
          (fn i => EVERY' (select_sup (length clauses) i) i) 
@@ -1027,8 +1054,7 @@
           | _ => PureThy.get_thms thy (((fst o dest_Type o fastype_of) t) ^ ".split_asm")
         val (_, ts) = strip_comb t
       in
-        print_tac ("splitting with t = " ^ (makestring t))
-        THEN (Splitter.split_asm_tac split_rules 1)
+        (Splitter.split_asm_tac split_rules 1)
 (*        THEN (Simplifier.asm_full_simp_tac HOL_basic_ss 1)
           THEN (DETERM (TRY (etac @{thm Pair_inject} 1))) *)
         THEN (REPEAT_DETERM_N (num_of_constrs - 1) (etac @{thm botE} 1 ORELSE etac @{thm botE} 2))
@@ -1049,11 +1075,11 @@
     val (params, _) = chop (length ms) args
     val f_tac = case f of
         Const (name, T) => full_simp_tac (HOL_basic_ss addsimps 
-           @{thm eval_pred}::function_definition thy name mode::[]) 1
+           (@{thm eval_pred}::(predfun_definition_of thy name mode)
+           :: @{thm "Product_Type.split_conv"}::[])) 1
       | Free _ => all_tac
   in  
     print_tac "before simplification in prove_args:"
-    THEN debug_tac ("function : " ^ (makestring f) ^ " - mode" ^ (makestring mode))
     THEN f_tac
     THEN print_tac "after simplification in prove_args"
     (* work with parameter arguments *)
@@ -1066,23 +1092,21 @@
       if AList.defined op = modes name then
         etac @{thm bindE} 1
         THEN (REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"})))
-        THEN (etac (elim_rule thy name mode) 1)
+        THEN (etac (predfun_elim_of thy name mode) 1)
         THEN (EVERY (map (prove_param2 thy modes) (ms ~~ args)))
       else error "Prove expr2 if case not implemented"
     | _ => etac @{thm bindE} 1)
   | prove_expr2 _ _ _ = error "Prove expr2 not implemented"
 
 fun prove_sidecond2 thy modes t = let
-  val _ = tracing ("prove_sidecond:" ^ (makestring t))
   fun preds_of t nameTs = case strip_comb t of 
     (f as Const (name, T), args) =>
       if AList.defined (op =) modes name then (name, T) :: nameTs
         else fold preds_of args nameTs
     | _ => nameTs
   val preds = preds_of t []
-  val _ = tracing ("preds: " ^ (makestring preds))
   val defs = map
-    (fn (pred, T) => function_definition thy pred ([], (1 upto (length (binder_types T)))))
+    (fn (pred, T) => predfun_definition_of thy pred ([], (1 upto (length (binder_types T)))))
       preds
   in
    (* only simplify the one assumption *)
@@ -1101,7 +1125,7 @@
           val s = Name.variant names "x";
           val v = Free (s, fastype_of t)
         in ((s::names, HOLogic.mk_eq (v, t)::eqs), v) end;
-  val pred_intro_rule = nth (pred_intros thy pred) (i - 1)
+  val pred_intro_rule = nth (intros_of thy pred) (i - 1)
     |> preprocess_intro thy
     |> (fn thm => hd (ind_set_codegen_preproc thy [thm]))
     (* FIXME preprocess |> Simplifier.full_simplify (HOL_basic_ss addsimps [@ {thm Predicate.memb_code}]) *)
@@ -1146,7 +1170,7 @@
             print_tac "before neg prem 2"
             THEN etac @{thm bindE} 1
             THEN (if is_some name then
-                full_simp_tac (HOL_basic_ss addsimps [function_definition thy (the name) (iss, js)]) 1 
+                full_simp_tac (HOL_basic_ss addsimps [predfun_definition_of thy (the name) (iss, js)]) 1 
                 THEN etac @{thm not_predE} 1
                 THEN (EVERY (map (prove_param2 thy modes) (param_modes ~~ params)))
               else
@@ -1180,7 +1204,7 @@
 in
   (DETERM (TRY (rtac @{thm unit.induct} 1)))
    THEN (REPEAT_DETERM (CHANGED (rewtac @{thm split_paired_all})))
-   THEN (rtac (intro_rule thy pred mode) 1)
+   THEN (rtac (predfun_intro_of thy pred mode) 1)
    THEN (EVERY (map prove_clause (clauses ~~ (1 upto (length clauses)))))
 end;
 
@@ -1202,25 +1226,6 @@
 fun prove_preds thy all_vs param_vs modes clauses pmts =
   map (prove_pred thy all_vs param_vs modes clauses) pmts
 
-(* look for other place where this functionality was used before *)
-fun strip_intro_concl intro nparams = let
-  val _ $ u = Logic.strip_imp_concl intro
-  val (pred, all_args) = strip_comb u
-  val (params, args) = chop nparams all_args
-in (pred, (params, args)) end
-
-(* setup for alternative introduction and elimination rules *)
-
-fun add_intro_thm thm thy = let
-   val (pred, _) = dest_Const (fst (strip_intro_concl (prop_of thm) 0))
- in map_intro_rules (Symtab.insert_list Thm.eq_thm (pred, thm)) thy end
-
-fun add_elim_thm thm thy = let
-    val (pred, _) = dest_Const (fst 
-      (strip_comb (HOLogic.dest_Trueprop (hd (prems_of thm)))))
-  in map_elim_rules (Symtab.update (pred, thm)) thy end
-
-
 (* special case: inductive predicate with no clauses *)
 fun noclause (predname, T) thy = let
   val Ts = binder_types T
@@ -1231,137 +1236,110 @@
   val intro_t = Logic.mk_implies (@{prop False}, clausehd)
   val P = HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT))
   val elim_t = Logic.list_implies ([clausehd, Logic.mk_implies (@{prop False}, P)], P)
-  val intro_thm = Goal.prove (ProofContext.init thy) names [] intro_t
+  val intro = Goal.prove (ProofContext.init thy) names [] intro_t
         (fn {...} => etac @{thm FalseE} 1)
-  val elim_thm = Goal.prove (ProofContext.init thy) ("P" :: names) [] elim_t
-        (fn {...} => etac (pred_elim thy predname) 1) 
+  val elim = Goal.prove (ProofContext.init thy) ("P" :: names) [] elim_t
+        (fn {...} => etac (the_elim_of thy predname) 1) 
 in
-  add_intro_thm intro_thm thy
-  |> add_elim_thm elim_thm
+  add_intro intro thy
+  |> set_elim elim
 end
 
-(*************************************************************************************)
-(* main function *********************************************************************)
-(*************************************************************************************)
-
-fun prove_equation ind_name mode thy =
-let
-  val _ = tracing ("starting prove_equation' with " ^ ind_name)
-  val (prednames, preds) = 
-    case (try (InductivePackage.the_inductive (ProofContext.init thy)) ind_name) of
-      SOME info => let val preds = info |> snd |> #preds
-        in (map (fst o dest_Const) preds, map ((apsnd Logic.unvarifyT) o dest_Const) preds) end
-    | NONE => let
-        val pred = Symtab.lookup (#intro_rules (IndCodegenData.get thy)) ind_name
-          |> the |> hd |> prop_of
-          |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop |> strip_comb
-          |> fst |>  dest_Const |> apsnd Logic.unvarifyT
-       in ([ind_name], [pred]) end
-  val thy' = fold (fn pred as (predname, T) => fn thy =>
-    if null (pred_intros thy predname) then noclause pred thy else thy) preds thy
-  val intrs = map (preprocess_intro thy') (maps (pred_intros thy') prednames)
-    |> ind_set_codegen_preproc thy' (*FIXME preprocessor
-    |> map (Simplifier.full_simplify (HOL_basic_ss addsimps [@ {thm Predicate.memb_code}]))*)
-    |> map (Logic.unvarify o prop_of)
-  val _ = tracing ("preprocessed intro rules:" ^ (makestring (map (cterm_of thy') intrs)))
-  val name_of_calls = get_name_of_ind_calls_of_clauses thy' prednames intrs 
-  val _ = tracing ("calling preds: " ^ makestring name_of_calls)
-  val _ = tracing "starting recursive compilations"
-  fun rec_call name thy = 
-    (*FIXME use member instead of infix mem*)
-    if not (name mem (Symtab.keys (#modes (IndCodegenData.get thy)))) then
-      prove_equation name NONE thy else thy
-  val thy'' = fold rec_call name_of_calls thy'
-  val _ = tracing "returning from recursive calls"
-  val _ = tracing "starting mode inference"
-  val extra_modes = Symtab.dest (#modes (IndCodegenData.get thy''))
-  val nparams = get_nparams thy'' ind_name
-  val _ $ u = Logic.strip_imp_concl (hd intrs);
-  val params = List.take (snd (strip_comb u), nparams);
-  val param_vs = maps term_vs params
-  val all_vs = terms_vs intrs
-  fun dest_prem t =
+fun prepare_intrs thy prednames =
+  let
+    val intrs = map (preprocess_intro thy) (maps (intros_of thy) prednames)
+      |> ind_set_codegen_preproc thy (*FIXME preprocessor
+      |> map (Simplifier.full_simplify (HOL_basic_ss addsimps [@ {thm Predicate.memb_code}]))*)
+      |> map (Logic.unvarify o prop_of)
+    val nparams = nparams_of thy (hd prednames)
+    val preds = distinct (op =) (map (dest_Const o fst o (strip_intro_concl nparams)) intrs)
+    val extra_modes = all_modes_of thy |> filter_out (fn (name, _) => member (op =) prednames name)
+    val _ $ u = Logic.strip_imp_concl (hd intrs);
+    val params = List.take (snd (strip_comb u), nparams);
+    val param_vs = maps term_vs params
+    val all_vs = terms_vs intrs
+    fun dest_prem t =
       (case strip_comb t of
         (v as Free _, ts) => if v mem params then Prem (ts, v) else Sidecond t
       | (c as Const (@{const_name Not}, _), [t]) => (case dest_prem t of
           Prem (ts, t) => Negprem (ts, t)
-        | Negprem _ => error ("Double negation not allowed in premise: " ^ (makestring (c $ t))) 
+        | Negprem _ => error ("Double negation not allowed in premise: " ^ (Syntax.string_of_term_global thy (c $ t))) 
         | Sidecond t => Sidecond (c $ t))
       | (c as Const (s, _), ts) =>
-        if is_ind_pred thy'' s then
-          let val (ts1, ts2) = chop (get_nparams thy'' s) ts
+        if is_pred thy s then
+          let val (ts1, ts2) = chop (nparams_of thy s) ts
           in Prem (ts2, list_comb (c, ts1)) end
         else Sidecond t
       | _ => Sidecond t)
-  fun add_clause intr (clauses, arities) =
-  let
-    val _ $ t = Logic.strip_imp_concl intr;
-    val (Const (name, T), ts) = strip_comb t;
-    val (ts1, ts2) = chop nparams ts;
-    val prems = map (dest_prem o HOLogic.dest_Trueprop) (Logic.strip_imp_prems intr);
-    val (Ts, Us) = chop nparams (binder_types T)
-  in
-    (AList.update op = (name, these (AList.lookup op = clauses name) @
-      [(ts2, prems)]) clauses,
-     AList.update op = (name, (map (fn U => (case strip_type U of
+    fun add_clause intr (clauses, arities) =
+    let
+      val _ $ t = Logic.strip_imp_concl intr;
+      val (Const (name, T), ts) = strip_comb t;
+      val (ts1, ts2) = chop nparams ts;
+      val prems = map (dest_prem o HOLogic.dest_Trueprop) (Logic.strip_imp_prems intr);
+      val (Ts, Us) = chop nparams (binder_types T)
+    in
+      (AList.update op = (name, these (AList.lookup op = clauses name) @
+        [(ts2, prems)]) clauses,
+       AList.update op = (name, (map (fn U => (case strip_type U of
                  (Rs as _ :: _, Type ("bool", [])) => SOME (length Rs)
                | _ => NONE)) Ts,
              length Us)) arities)
-  end;
-  val (clauses, arities) = fold add_clause intrs ([], []);
-  val modes = infer_modes thy'' extra_modes arities param_vs clauses
-  val _ = print_arities arities;
-  val _ = print_modes modes;
-  val modes = if (is_some mode) then AList.update (op =) (ind_name, [the mode]) modes else modes
-  val _ = print_modes modes
-  val thy''' = fold (create_definitions preds nparams) modes thy''
-    |> map_modes (fold Symtab.update_new modes)
+    end;
+    val (clauses, arities) = fold add_clause intrs ([], []);
+  in (preds, nparams, all_vs, param_vs, extra_modes, clauses, arities) end;
+
+fun arrange kvs =
+  let
+    fun add (key, value) table =
+      AList.update op = (key, these (AList.lookup op = table key) @ [value]) table
+  in fold add kvs [] end;
+        
+(* main function *)
+
+fun add_equations_of prednames thy =
+let
+  val _ = tracing ("starting add_equations with " ^ commas prednames ^ "...")
+  (* null clause handling *)
+  (*
+  val thy' = fold (fn pred as (predname, T) => fn thy =>
+    if null (intros_of thy predname) then noclause pred thy else thy) preds thy
+    *)
+  val (preds, nparams, all_vs, param_vs, extra_modes, clauses, arities) =
+    prepare_intrs thy prednames
+  val _ = tracing "Infering modes..."
+  val modes = infer_modes thy extra_modes arities param_vs clauses
+  val _ = tracing "Defining executable functions..."
+  val thy' = fold (create_definitions preds nparams) modes thy
   val clauses' = map (fn (s, cls) => (s, (the (AList.lookup (op =) preds s), cls))) clauses
-  val _ = tracing "compiling predicates..."
-  val ts = compile_preds thy''' all_vs param_vs (extra_modes @ modes) clauses'
-  val _ = tracing "returned term from compile_preds"
-  val pred_mode = maps (fn (s, (T, _)) => map (pair (s, T)) ((the o AList.lookup (op =) modes) s)) clauses'
-  val _ = tracing "starting proof"
-  val result_thms = prove_preds thy''' all_vs param_vs (extra_modes @ modes) clauses (pred_mode ~~ (flat ts))
-  val (_, thy'''') = yield_singleton PureThy.add_thmss
-    ((Binding.qualify true (Long_Name.base_name ind_name) (Binding.name "equation"), result_thms),
-      [Attrib.attribute_i thy''' Code.add_default_eqn_attrib]) thy'''
+  val _ = tracing "Compiling equations..."
+  val ts = compile_preds thy' all_vs param_vs (extra_modes @ modes) clauses'
+  val pred_mode =
+    maps (fn (s, (T, _)) => map (pair (s, T)) ((the o AList.lookup (op =) modes) s)) clauses' 
+  val _ = tracing "Proving equations..."
+  val result_thms =
+    prove_preds thy' all_vs param_vs (extra_modes @ modes) clauses (pred_mode ~~ (flat ts))
+  val thy'' = fold (fn (name, result_thms) => fn thy => snd (PureThy.add_thmss
+    [((Binding.qualify true (Long_Name.base_name name) (Binding.name "equation"), result_thms),
+      [Attrib.attribute_i thy Code.add_default_eqn_attrib])] thy))
+    (arrange ((map (fn ((name, _), _) => name) pred_mode) ~~ result_thms)) thy'
 in
-  thy''''
+  thy''
 end
 
-fun set_nparams (pred, nparams) thy = map_nparams (Symtab.update (pred, nparams)) thy
-
-fun print_alternative_rules thy = let
-    val d = IndCodegenData.get thy
-    val preds = (Symtab.keys (#intro_rules d)) union (Symtab.keys (#elim_rules d))
-    val _ = tracing ("preds: " ^ (makestring preds))
-    fun print pred = let
-      val _ = tracing ("predicate: " ^ pred)
-      val _ = tracing ("introrules: ")
-      val _ = fold (fn thm => fn u => tracing (makestring thm))
-        (rev (Symtab.lookup_list (#intro_rules d) pred)) ()
-      val _ = tracing ("casesrule: ")
-      val _ = tracing (makestring (Symtab.lookup (#elim_rules d) pred))
-    in () end
-    val _ = map print preds
- in thy end; 
-
-
 (* generation of case rules from user-given introduction rules *)
 
 fun mk_casesrule introrules nparams ctxt =
   let
     val intros = map prop_of introrules
-    val (pred, (params, args)) = strip_intro_concl (hd intros) nparams
+    val (pred, (params, args)) = strip_intro_concl nparams (hd intros)
     val ([propname], ctxt1) = Variable.variant_fixes ["thesis"] ctxt
     val prop = HOLogic.mk_Trueprop (Free (propname, HOLogic.boolT))
     val (argnames, ctxt2) = Variable.variant_fixes
       (map (fn i => "a" ^ string_of_int i) (1 upto (length args))) ctxt1
-    val argvs = map Free (argnames ~~ (map fastype_of args))
-      (*FIXME map2*)
+    val argvs = map2 (curry Free) argnames (map fastype_of args)
     fun mk_case intro = let
-        val (_, (_, args)) = strip_intro_concl intro nparams
+        val (_, (_, args)) = strip_intro_concl nparams intro
         val prems = Logic.strip_imp_prems intro
         val eqprems = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (argvs ~~ args)
         val frees = (fold o fold_aterms)
@@ -1376,6 +1354,46 @@
               ctxt2
   in (pred, prop, ctxt3) end;
 
+(* code dependency graph *)
+  
+fun fetch_pred_data thy name =
+  case try (InductivePackage.the_inductive (ProofContext.init thy)) name of
+    SOME (info as (_, result)) => 
+      let
+        fun is_intro_of intro =
+          let
+            val (const, _) = strip_comb (HOLogic.dest_Trueprop (concl_of intro))
+          in (fst (dest_Const const) = name) end;
+        val intros =  filter is_intro_of (#intrs result)
+        val elim = nth (#elims result) (find_index (fn s => s = name) (#names (fst info)))
+        val nparams = length (InductivePackage.params_of (#raw_induct result))
+      in mk_pred_data ((intros, SOME elim, nparams), []) end
+  | NONE => error ("No such predicate: " ^ quote name)
+
+fun dependencies_of (thy : theory) name =
+  let
+    fun is_inductive_predicate thy name =
+      is_some (try (InductivePackage.the_inductive (ProofContext.init thy)) name)
+    val data = fetch_pred_data thy name
+    val intros = map Thm.prop_of (#intros (rep_pred_data data))
+    val keys = fold Term.add_consts intros [] |> map fst
+    |> filter (is_inductive_predicate thy)
+  in
+    (data, keys)
+  end;
+
+fun add_equations name thy =
+  let
+    val thy' = PredData.map (Graph.extend (dependencies_of thy) [name]) thy;
+    (*val preds = Graph.all_preds (PredData.get thy') [name] |> filter_out (has_elim thy') *)
+    fun strong_conn_of gr keys =
+      Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr)
+    val scc = strong_conn_of (PredData.get thy') [name]
+    val thy'' = fold_rev
+      (fn preds => fn thy =>
+        if forall (null o modes_of thy) preds then add_equations_of preds thy else thy)
+      scc thy'
+  in thy'' end
 
 (** user interface **)
 
@@ -1383,26 +1401,47 @@
 
 fun attrib f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
 
-val add_elim_attrib = attrib add_elim_thm;
+(*
+val add_elim_attrib = attrib set_elim;
+*)
 
+
+(* TODO: make TheoryDataFun to GenericDataFun & remove duplication of local theory and theory *)
+(* TODO: must create state to prove multiple cases *)
 fun generic_code_pred prep_const raw_const lthy =
   let
-    val thy = ProofContext.theory_of lthy
+    val thy = (ProofContext.theory_of lthy)
     val const = prep_const thy raw_const
-    val nparams = get_nparams thy const
-    val intro_rules = pred_intros thy const
-    val (((tfrees, frees), fact), lthy') =
-      Variable.import_thms true intro_rules lthy;
-    val (pred, prop, lthy'') = mk_casesrule fact nparams lthy'
-    val (predname, _) = dest_Const pred
-    fun after_qed [[th]] lthy'' =
-      lthy''
+    val lthy' = lthy
+    val thy' = PredData.map (Graph.extend (dependencies_of thy) [const]) thy
+    val preds = Graph.all_preds (PredData.get thy') [const] |> filter_out (has_elim thy')
+    val _ = Output.tracing ("preds: " ^ commas preds)
+    (*
+    fun mk_elim pred =
+      let
+        val nparams = nparams_of thy pred 
+        val intros = intros_of thy pred
+        val (((tfrees, frees), fact), lthy'') =
+          Variable.import_thms true intros lthy';
+        val (pred, prop, lthy''') = mk_casesrule fact nparams lthy''
+      in (pred, prop, lthy''') end;
+      
+        val (predname, _) = dest_Const pred
+    *)
+    val nparams = nparams_of thy' const
+    val intros = intros_of thy' const
+    val (((tfrees, frees), fact), lthy'') =
+      Variable.import_thms true intros lthy';
+    val (pred, prop, lthy''') = mk_casesrule fact nparams lthy''
+    val (predname, _) = dest_Const pred  
+    fun after_qed [[th]] lthy''' =
+      lthy'''
       |> LocalTheory.note Thm.generatedK
-           ((Binding.empty, [Attrib.internal (K add_elim_attrib)]), [th])
+           ((Binding.empty, []), [th])
       |> snd
-      |> LocalTheory.theory (prove_equation predname NONE)
+      |> LocalTheory.theory (add_equations_of [predname])
   in
-    Proof.theorem_i NONE after_qed [[(prop, [])]] lthy''
+    Proof.theorem_i NONE after_qed [[(prop, [])]] lthy'''
   end;
 
 structure P = OuterParse
@@ -1412,14 +1451,15 @@
 val code_pred = generic_code_pred (K I);
 val code_pred_cmd = generic_code_pred Code.read_const
 
-val setup =
-  Attrib.setup @{binding code_ind_intros} (Scan.succeed (attrib add_intro_thm))
-    "adding alternative introduction rules for code generation of inductive predicates" #>
-  Attrib.setup @{binding code_ind_cases} (Scan.succeed add_elim_attrib)
+val setup = PredData.put (Graph.empty) #>
+  Attrib.setup @{binding code_pred_intros} (Scan.succeed (attrib add_intro))
+    "adding alternative introduction rules for code generation of inductive predicates"
+(*  Attrib.setup @{binding code_ind_cases} (Scan.succeed add_elim_attrib)
     "adding alternative elimination rules for code generation of inductive predicates";
+    *)
   (*FIXME name discrepancy in attribs and ML code*)
   (*FIXME intros should be better named intro*)
-  (*FIXME why distinguished atribute for cases?*)
+  (*FIXME why distinguished attribute for cases?*)
 
 val _ = OuterSyntax.local_theory_to_proof "code_pred"
   "prove equations for predicate specified by intro/elim rules"
@@ -1443,21 +1483,20 @@
     val (body, Ts, fp) = HOLogic.strip_split split;
       (*FIXME former order of tuple positions must be restored*)
     val (pred as Const (name, T), all_args) = strip_comb body
-    val (params, args) = chop (get_nparams thy name) all_args
+    val (params, args) = chop (nparams_of thy name) all_args
     val user_mode = map_filter I (map_index
       (fn (i, t) => case t of Bound j => if j < length Ts then NONE
         else SOME (i+1) | _ => SOME (i+1)) args) (*FIXME dangling bounds should not occur*)
     val (inargs, _) = get_args user_mode args;
-    val all_modes = Symtab.dest (#modes (IndCodegenData.get thy));
     val modes = filter (fn Mode (_, is, _) => is = user_mode)
-      (modes_of_term all_modes (list_comb (pred, params)));
+      (modes_of_term (all_modes_of thy) (list_comb (pred, params)));
     val m = case modes
      of [] => error ("No mode possible for comprehension "
                 ^ Syntax.string_of_term_global thy t_compr)
       | [m] => m
       | m :: _ :: _ => (warning ("Multiple modes possible for comprehension "
                 ^ Syntax.string_of_term_global thy t_compr); m);
-    val t_eval = list_comb (compile_expr thy all_modes (SOME m, list_comb (pred, params)),
+    val t_eval = list_comb (compile_expr thy (all_modes_of thy) (SOME m, list_comb (pred, params)),
       inargs)
   in t_eval end;
 
--- a/src/Provers/Arith/fast_lin_arith.ML	Tue Jun 09 10:23:41 2009 -0700
+++ b/src/Provers/Arith/fast_lin_arith.ML	Tue Jun 09 11:12:08 2009 -0700
@@ -1,6 +1,6 @@
 (*  Title:      Provers/Arith/fast_lin_arith.ML
     ID:         $Id$
-    Author:     Tobias Nipkow and Tjark Weber
+    Author:     Tobias Nipkow and Tjark Weber and Sascha Boehme
 
 A generic linear arithmetic package.  It provides two tactics
 (cut_lin_arith_tac, lin_arith_tac) and a simplification procedure
@@ -21,6 +21,7 @@
   val not_lessD   : thm  (* ~(m < n) ==> n <= m *)
   val not_leD     : thm  (* ~(m <= n) ==> n < m *)
   val sym         : thm  (* x = y ==> y = x *)
+  val trueI       : thm  (* True *)
   val mk_Eq       : thm -> thm
   val atomize     : thm -> thm list
   val mk_Trueprop : term -> term
@@ -56,7 +57,6 @@
 
   (*preprocessing, performed on the goal -- must do the same as 'pre_decomp':*)
   val pre_tac: Proof.context -> int -> tactic
-  val mk_number: typ -> int -> term
 
   (*the limit on the number of ~= allowed; because each ~= is split
     into two cases, this can lead to an explosion*)
@@ -90,9 +90,11 @@
   val lin_arith_tac: Proof.context -> bool -> int -> tactic
   val lin_arith_simproc: simpset -> term -> thm option
   val map_data: ({add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
-                 lessD: thm list, neqE: thm list, simpset: Simplifier.simpset}
+                 lessD: thm list, neqE: thm list, simpset: Simplifier.simpset,
+                 number_of : serial * (theory -> typ -> int -> cterm)}
                  -> {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
-                     lessD: thm list, neqE: thm list, simpset: Simplifier.simpset})
+                     lessD: thm list, neqE: thm list, simpset: Simplifier.simpset,
+                     number_of : serial * (theory -> typ -> int -> cterm)})
                 -> Context.generic -> Context.generic
   val trace: bool ref
   val warning_count: int ref;
@@ -105,6 +107,8 @@
 
 (** theory data **)
 
+fun no_number_of _ _ _ = raise CTERM ("number_of", [])
+
 structure Data = GenericDataFun
 (
   type T =
@@ -113,22 +117,27 @@
     inj_thms: thm list,
     lessD: thm list,
     neqE: thm list,
-    simpset: Simplifier.simpset};
+    simpset: Simplifier.simpset,
+    number_of : serial * (theory -> typ -> int -> cterm)};
 
   val empty = {add_mono_thms = [], mult_mono_thms = [], inj_thms = [],
-               lessD = [], neqE = [], simpset = Simplifier.empty_ss};
+               lessD = [], neqE = [], simpset = Simplifier.empty_ss,
+               number_of = (serial (), no_number_of) };
   val extend = I;
   fun merge _
     ({add_mono_thms= add_mono_thms1, mult_mono_thms= mult_mono_thms1, inj_thms= inj_thms1,
-      lessD = lessD1, neqE=neqE1, simpset = simpset1},
+      lessD = lessD1, neqE=neqE1, simpset = simpset1,
+      number_of = (number_of1 as (s1, _))},
      {add_mono_thms= add_mono_thms2, mult_mono_thms= mult_mono_thms2, inj_thms= inj_thms2,
-      lessD = lessD2, neqE=neqE2, simpset = simpset2}) =
+      lessD = lessD2, neqE=neqE2, simpset = simpset2,
+      number_of = (number_of2 as (s2, _))}) =
     {add_mono_thms = Thm.merge_thms (add_mono_thms1, add_mono_thms2),
      mult_mono_thms = Thm.merge_thms (mult_mono_thms1, mult_mono_thms2),
      inj_thms = Thm.merge_thms (inj_thms1, inj_thms2),
      lessD = Thm.merge_thms (lessD1, lessD2),
      neqE = Thm.merge_thms (neqE1, neqE2),
-     simpset = Simplifier.merge_ss (simpset1, simpset2)};
+     simpset = Simplifier.merge_ss (simpset1, simpset2),
+     number_of = if s1 > s2 then number_of1 else number_of2};
 );
 
 val map_data = Data.map;
@@ -154,7 +163,6 @@
                 | NotLeD of injust
                 | NotLeDD of injust
                 | Multiplied of int * injust
-                | Multiplied2 of int * injust
                 | Added of injust * injust;
 
 datatype lineq = Lineq of int * lineq_type * int list * injust;
@@ -320,7 +328,7 @@
         else (m1,m2)
       val (p1,p2) = if ty1=Eq andalso ty2=Eq andalso (n1 = ~1 orelse n2 = ~1)
                     then (~n1,~n2) else (n1,n2)
-  in add_ineq (multiply_ineq n1 i1) (multiply_ineq n2 i2) end;
+  in add_ineq (multiply_ineq p1 i1) (multiply_ineq p2 i2) end;
 
 (* ------------------------------------------------------------------------- *)
 (* The main refutation-finding code.                                         *)
@@ -328,7 +336,7 @@
 
 fun is_trivial (Lineq(_,_,l,_)) = forall (fn i => i=0) l;
 
-fun is_answer (ans as Lineq(k,ty,l,_)) =
+fun is_contradictory (ans as Lineq(k,ty,l,_)) =
   case ty  of Eq => k <> 0 | Le => k > 0 | Lt => k >= 0;
 
 fun calc_blowup l =
@@ -347,13 +355,10 @@
 (* blowup (number of consequences generated) and eliminates it.              *)
 (* ------------------------------------------------------------------------- *)
 
-fun allpairs f xs ys =
-  maps (fn x => map (fn y => f x y) ys) xs;
-
 fun extract_first p =
-  let fun extract xs (y::ys) = if p y then (SOME y,xs@ys)
-                               else extract (y::xs) ys
-        | extract xs []      = (NONE,xs)
+  let
+    fun extract xs (y::ys) = if p y then (y, xs @ ys) else extract (y::xs) ys
+      | extract xs [] = raise Empty
   in extract [] end;
 
 fun print_ineqs ineqs =
@@ -368,10 +373,10 @@
 datatype result = Success of injust | Failure of history;
 
 fun elim (ineqs, hist) =
-  let val dummy = print_ineqs ineqs
+  let val _ = print_ineqs ineqs
       val (triv, nontriv) = List.partition is_trivial ineqs in
   if not (null triv)
-  then case Library.find_first is_answer triv of
+  then case Library.find_first is_contradictory triv of
          NONE => elim (nontriv, hist)
        | SOME(Lineq(_,_,_,j)) => Success j
   else
@@ -379,11 +384,12 @@
   else
   let val (eqs, noneqs) = List.partition (fn (Lineq(_,ty,_,_)) => ty=Eq) nontriv in
   if not (null eqs) then
-     let val clist = Library.foldl (fn (cs,Lineq(_,_,l,_)) => l union cs) ([],eqs)
-         val sclist = sort (fn (x,y) => int_ord (abs x, abs y))
-                           (List.filter (fn i => i<>0) clist)
-         val c = hd sclist
-         val (SOME(eq as Lineq(_,_,ceq,_)),othereqs) =
+     let val c =
+           fold (fn Lineq(_,_,l,_) => fn cs => l union cs) eqs []
+           |> filter (fn i => i <> 0)
+           |> sort (int_ord o pairself abs)
+           |> hd
+         val (eq as Lineq(_,_,ceq,_),othereqs) =
                extract_first (fn Lineq(_,_,l,_) => c mem l) eqs
          val v = find_index_eq c ceq
          val (ioth,roth) = List.partition (fn (Lineq(_,_,l,_)) => nth l v = 0)
@@ -402,7 +408,7 @@
      let val (c,v) = hd(sort (fn (x,y) => int_ord(fst(x),fst(y))) nziblows)
          val (no,yes) = List.partition (fn (Lineq(_,_,l,_)) => nth l v = 0) ineqs
          val (pos,neg) = List.partition(fn (Lineq(_,_,l,_)) => nth l v > 0) yes
-     in elim(no @ allpairs (elim_var v) pos neg, (v,nontriv)::hist) end
+     in elim(no @ map_product (elim_var v) pos neg, (v,nontriv)::hist) end
   end
   end
   end;
@@ -427,11 +433,12 @@
 val union_bterm = curry (gen_union
   (fn ((b:bool, t), (b', t')) => b = b' andalso Pattern.aeconv (t, t')));
 
-(* FIXME OPTIMIZE!!!! (partly done already)
-   Addition/Multiplication need i*t representation rather than t+t+...
-   Get rid of Mulitplied(2). For Nat LA_Data.mk_number should return Suc^n
-   because Numerals are not known early enough.
+fun add_atoms (lhs, _, _, rhs, _, _) =
+  union_term (map fst lhs) o union_term (map fst rhs);
 
+fun atoms_of ds = fold add_atoms ds [];
+
+(*
 Simplification may detect a contradiction 'prematurely' due to type
 information: n+1 <= 0 is simplified to False and does not need to be crossed
 with 0 <= n.
@@ -444,58 +451,77 @@
   let
     val ctxt = Simplifier.the_context ss;
     val thy = ProofContext.theory_of ctxt;
-    val {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset, ...} = get_data ctxt;
+    val {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset,
+      number_of = (_, num_of), ...} = get_data ctxt;
     val simpset' = Simplifier.inherit_context ss simpset;
-    val atoms = Library.foldl (fn (ats, (lhs,_,_,rhs,_,_)) =>
-                            union_term (map fst lhs) (union_term (map fst rhs) ats))
-                        ([], List.mapPartial (fn thm => if Thm.no_prems thm
-                                              then LA_Data.decomp ctxt (Thm.concl_of thm)
-                                              else NONE) asms)
+    fun only_concl f thm =
+      if Thm.no_prems thm then f (Thm.concl_of thm) else NONE;
+    val atoms = atoms_of (map_filter (only_concl (LA_Data.decomp ctxt)) asms);
+
+    fun use_first rules thm =
+      get_first (fn th => SOME (thm RS th) handle THM _ => NONE) rules
+
+    fun add2 thm1 thm2 =
+      use_first add_mono_thms (thm1 RS (thm2 RS LA_Logic.conjI));
+    fun try_add thms thm = get_first (fn th => add2 th thm) thms;
 
-      fun add2 thm1 thm2 =
-        let val conj = thm1 RS (thm2 RS LA_Logic.conjI)
-        in get_first (fn th => SOME(conj RS th) handle THM _ => NONE) add_mono_thms
-        end;
-      fun try_add [] _ = NONE
-        | try_add (thm1::thm1s) thm2 = case add2 thm1 thm2 of
-             NONE => try_add thm1s thm2 | some => some;
+    fun add_thms thm1 thm2 =
+      (case add2 thm1 thm2 of
+        NONE =>
+          (case try_add ([thm1] RL inj_thms) thm2 of
+            NONE =>
+              (the (try_add ([thm2] RL inj_thms) thm1)
+                handle Option =>
+                  (trace_thm "" thm1; trace_thm "" thm2;
+                   sys_error "Linear arithmetic: failed to add thms"))
+          | SOME thm => thm)
+      | SOME thm => thm);
+
+    fun mult_by_add n thm =
+      let fun mul i th = if i = 1 then th else mul (i - 1) (add_thms thm th)
+      in mul n thm end;
 
-      fun addthms thm1 thm2 =
-        case add2 thm1 thm2 of
-          NONE => (case try_add ([thm1] RL inj_thms) thm2 of
-                     NONE => ( the (try_add ([thm2] RL inj_thms) thm1)
-                               handle Option =>
-                               (trace_thm "" thm1; trace_thm "" thm2;
-                                sys_error "Linear arithmetic: failed to add thms")
-                             )
-                   | SOME thm => thm)
-        | SOME thm => thm;
-
-      fun multn(n,thm) =
-        let fun mul(i,th) = if i=1 then th else mul(i-1, addthms thm th)
-        in if n < 0 then mul(~n,thm) RS LA_Logic.sym else mul(n,thm) end;
+    val rewr = Simplifier.rewrite simpset';
+    val rewrite_concl = Conv.fconv_rule (Conv.concl_conv ~1 (Conv.arg_conv
+      (Conv.binop_conv rewr)));
+    fun discharge_prem thm = if Thm.nprems_of thm = 0 then thm else
+      let val cv = Conv.arg1_conv (Conv.arg_conv rewr)
+      in Thm.implies_elim (Conv.fconv_rule cv thm) LA_Logic.trueI end
 
-      fun multn2(n,thm) =
-        let val SOME(mth) =
-              get_first (fn th => SOME(thm RS th) handle THM _ => NONE) mult_mono_thms
-            fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (Thm.theory_of_thm th) var;
-            val cv = cvar(mth, hd(prems_of mth));
-            val ct = cterm_of thy (LA_Data.mk_number (#T (rep_cterm cv)) n)
-        in instantiate ([],[(cv,ct)]) mth end
+    fun mult n thm =
+      (case use_first mult_mono_thms thm of
+        NONE => mult_by_add n thm
+      | SOME mth =>
+          let
+            val cv = mth |> Thm.cprop_of |> Drule.strip_imp_concl
+              |> Thm.dest_arg |> Thm.dest_arg1 |> Thm.dest_arg1
+            val T = #T (Thm.rep_cterm cv)
+          in
+            mth
+            |> Thm.instantiate ([], [(cv, num_of thy T n)])
+            |> rewrite_concl
+            |> discharge_prem
+            handle CTERM _ => mult_by_add n thm
+                 | THM _ => mult_by_add n thm
+          end);
 
-      fun simp thm =
-        let val thm' = trace_thm "Simplified:" (full_simplify simpset' thm)
-        in if LA_Logic.is_False thm' then raise FalseE thm' else thm' end
+    fun mult_thm (n, thm) =
+      if n = ~1 then thm RS LA_Logic.sym
+      else if n < 0 then mult (~n) thm RS LA_Logic.sym
+      else mult n thm;
+
+    fun simp thm =
+      let val thm' = trace_thm "Simplified:" (full_simplify simpset' thm)
+      in if LA_Logic.is_False thm' then raise FalseE thm' else thm' end;
 
-      fun mk (Asm i) = trace_thm ("Asm " ^ string_of_int i) (nth asms i)
-        | mk (Nat i) = trace_thm ("Nat " ^ string_of_int i) (LA_Logic.mk_nat_thm thy (nth atoms i))
-        | mk (LessD j)            = trace_thm "L" (hd ([mk j] RL lessD))
-        | mk (NotLeD j)           = trace_thm "NLe" (mk j RS LA_Logic.not_leD)
-        | mk (NotLeDD j)          = trace_thm "NLeD" (hd ([mk j RS LA_Logic.not_leD] RL lessD))
-        | mk (NotLessD j)         = trace_thm "NL" (mk j RS LA_Logic.not_lessD)
-        | mk (Added (j1, j2))     = simp (trace_thm "+" (addthms (mk j1) (mk j2)))
-        | mk (Multiplied (n, j))  = (trace_msg ("*" ^ string_of_int n); trace_thm "*" (multn (n, mk j)))
-        | mk (Multiplied2 (n, j)) = simp (trace_msg ("**" ^ string_of_int n); trace_thm "**" (multn2 (n, mk j)))
+    fun mk (Asm i) = trace_thm ("Asm " ^ string_of_int i) (nth asms i)
+      | mk (Nat i) = trace_thm ("Nat " ^ string_of_int i) (LA_Logic.mk_nat_thm thy (nth atoms i))
+      | mk (LessD j)            = trace_thm "L" (hd ([mk j] RL lessD))
+      | mk (NotLeD j)           = trace_thm "NLe" (mk j RS LA_Logic.not_leD)
+      | mk (NotLeDD j)          = trace_thm "NLeD" (hd ([mk j RS LA_Logic.not_leD] RL lessD))
+      | mk (NotLessD j)         = trace_thm "NL" (mk j RS LA_Logic.not_lessD)
+      | mk (Added (j1, j2))     = simp (trace_thm "+" (add_thms (mk j1) (mk j2)))
+      | mk (Multiplied (n, j))  = (trace_msg ("*" ^ string_of_int n); trace_thm "*" (mult_thm (n, mk j)))
 
   in
     let
@@ -542,7 +568,7 @@
       val diff = map2 (curry (op -)) rhsa lhsa
       val c = i-j
       val just = Asm k
-      fun lineq(c,le,cs,j) = Lineq(c,le,cs, if m=1 then j else Multiplied2(m,j))
+      fun lineq(c,le,cs,j) = Lineq(c,le,cs, if m=1 then j else Multiplied(m,j))
   in case rel of
       "<="   => lineq(c,Le,diff,just)
      | "~<=" => if discrete
@@ -676,9 +702,6 @@
   result
 end;
 
-fun add_atoms (ats : term list, ((lhs,_,_,rhs,_,_) : LA_Data.decomp, _)) : term list =
-    union_term (map fst lhs) (union_term (map fst rhs) ats);
-
 fun add_datoms (dats : (bool * term) list, ((lhs,_,_,rhs,_,d) : LA_Data.decomp, _)) :
   (bool * term) list =
   union_bterm (map (pair d o fst) lhs) (union_bterm (map (pair d o fst) rhs) dats);
@@ -691,7 +714,7 @@
   let
     fun refute ((Ts, initems : (LA_Data.decomp * int) list) :: initemss) (js: injust list) =
           let
-            val atoms = Library.foldl add_atoms ([], initems)
+            val atoms = atoms_of (map fst initems)
             val n = length atoms
             val mkleq = mklineq n atoms
             val ixs = 0 upto (n - 1)
--- a/src/Pure/General/graph.ML	Tue Jun 09 10:23:41 2009 -0700
+++ b/src/Pure/General/graph.ML	Tue Jun 09 11:12:08 2009 -0700
@@ -48,6 +48,8 @@
   val topological_order: 'a T -> key list
   val add_edge_trans_acyclic: key * key -> 'a T -> 'a T               (*exception CYCLES*)
   val merge_trans_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T   (*exception CYCLES*)
+  val extend: (key -> 'a * key list) -> key list -> 'a T -> 'a T
+  val make: (key -> 'a * key list) -> key list -> 'a T
 end;
 
 functor GraphFun(Key: KEY): GRAPH =
@@ -275,6 +277,25 @@
   |> fold add_edge_trans_acyclic (diff_edges G1 G2)
   |> fold add_edge_trans_acyclic (diff_edges G2 G1);
 
+  
+(* constructing graphs *)
+
+fun extend explore =
+  let
+    fun contains_node gr key = member eq_key (keys gr) key
+    fun extend' key gr =
+      let
+        val (node, preds) = explore key
+      in
+        gr |> (not (contains_node gr key)) ?
+          (new_node (key, node)
+          #> fold extend' preds
+          #> fold (add_edge o (pair key)) preds)
+      end
+  in fold extend' end
+
+fun make explore keys = extend explore keys empty
+
 
 (*final declarations of this structure!*)
 val fold = fold_graph;