# HG changeset patch
# User wenzelm
# Date 1394221802 -3600
# Node ID ffe88d72afae57ce74440071cf6d8f50a8e594c8
# Parent  6d123f0ae358bd3b4375e4f6a529f5f231061b69# Parent  52c22561996dac4bd60bb6a6216431b4b5a6e072
merged

diff -r 6d123f0ae358 -r ffe88d72afae src/HOL/Ctr_Sugar.thy
--- a/src/HOL/Ctr_Sugar.thy	Fri Mar 07 15:52:56 2014 +0000
+++ b/src/HOL/Ctr_Sugar.thy	Fri Mar 07 20:50:02 2014 +0100
@@ -27,7 +27,6 @@
 declare [[coercion_args case_elem - +]]
 
 ML_file "Tools/Ctr_Sugar/case_translation.ML"
-setup Case_Translation.setup
 
 lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y"
 by (erule iffI) (erule contrapos_pn)
diff -r 6d123f0ae358 -r ffe88d72afae src/HOL/Decision_Procs/Cooper.thy
--- a/src/HOL/Decision_Procs/Cooper.thy	Fri Mar 07 15:52:56 2014 +0000
+++ b/src/HOL/Decision_Procs/Cooper.thy	Fri Mar 07 20:50:02 2014 +0100
@@ -62,25 +62,25 @@
 
 primrec Ifm :: "bool list \<Rightarrow> int list \<Rightarrow> fm \<Rightarrow> bool"  -- {* Semantics of formulae (fm) *}
 where
-  "Ifm bbs bs T = True"
-| "Ifm bbs bs F = False"
-| "Ifm bbs bs (Lt a) = (Inum bs a < 0)"
-| "Ifm bbs bs (Gt a) = (Inum bs a > 0)"
-| "Ifm bbs bs (Le a) = (Inum bs a \<le> 0)"
-| "Ifm bbs bs (Ge a) = (Inum bs a \<ge> 0)"
-| "Ifm bbs bs (Eq a) = (Inum bs a = 0)"
-| "Ifm bbs bs (NEq a) = (Inum bs a \<noteq> 0)"
-| "Ifm bbs bs (Dvd i b) = (i dvd Inum bs b)"
-| "Ifm bbs bs (NDvd i b) = (\<not>(i dvd Inum bs b))"
-| "Ifm bbs bs (NOT p) = (\<not> (Ifm bbs bs p))"
-| "Ifm bbs bs (And p q) = (Ifm bbs bs p \<and> Ifm bbs bs q)"
-| "Ifm bbs bs (Or p q) = (Ifm bbs bs p \<or> Ifm bbs bs q)"
-| "Ifm bbs bs (Imp p q) = ((Ifm bbs bs p) \<longrightarrow> (Ifm bbs bs q))"
-| "Ifm bbs bs (Iff p q) = (Ifm bbs bs p = Ifm bbs bs q)"
-| "Ifm bbs bs (E p) = (\<exists>x. Ifm bbs (x#bs) p)"
-| "Ifm bbs bs (A p) = (\<forall>x. Ifm bbs (x#bs) p)"
-| "Ifm bbs bs (Closed n) = bbs!n"
-| "Ifm bbs bs (NClosed n) = (\<not> bbs!n)"
+  "Ifm bbs bs T \<longleftrightarrow> True"
+| "Ifm bbs bs F \<longleftrightarrow> False"
+| "Ifm bbs bs (Lt a) \<longleftrightarrow> Inum bs a < 0"
+| "Ifm bbs bs (Gt a) \<longleftrightarrow> Inum bs a > 0"
+| "Ifm bbs bs (Le a) \<longleftrightarrow> Inum bs a \<le> 0"
+| "Ifm bbs bs (Ge a) \<longleftrightarrow> Inum bs a \<ge> 0"
+| "Ifm bbs bs (Eq a) \<longleftrightarrow> Inum bs a = 0"
+| "Ifm bbs bs (NEq a) \<longleftrightarrow> Inum bs a \<noteq> 0"
+| "Ifm bbs bs (Dvd i b) \<longleftrightarrow> i dvd Inum bs b"
+| "Ifm bbs bs (NDvd i b) \<longleftrightarrow> \<not> i dvd Inum bs b"
+| "Ifm bbs bs (NOT p) \<longleftrightarrow> \<not> Ifm bbs bs p"
+| "Ifm bbs bs (And p q) \<longleftrightarrow> Ifm bbs bs p \<and> Ifm bbs bs q"
+| "Ifm bbs bs (Or p q) \<longleftrightarrow> Ifm bbs bs p \<or> Ifm bbs bs q"
+| "Ifm bbs bs (Imp p q) \<longleftrightarrow> (Ifm bbs bs p \<longrightarrow> Ifm bbs bs q)"
+| "Ifm bbs bs (Iff p q) \<longleftrightarrow> Ifm bbs bs p = Ifm bbs bs q"
+| "Ifm bbs bs (E p) \<longleftrightarrow> (\<exists>x. Ifm bbs (x # bs) p)"
+| "Ifm bbs bs (A p) \<longleftrightarrow> (\<forall>x. Ifm bbs (x # bs) p)"
+| "Ifm bbs bs (Closed n) \<longleftrightarrow> bbs!n"
+| "Ifm bbs bs (NClosed n) \<longleftrightarrow> \<not> bbs!n"
 
 consts prep :: "fm \<Rightarrow> fm"
 recdef prep "measure fmsize"
@@ -129,44 +129,44 @@
 
 primrec numbound0 :: "num \<Rightarrow> bool"  -- {* a num is INDEPENDENT of Bound 0 *}
 where
-  "numbound0 (C c) = True"
-| "numbound0 (Bound n) = (n>0)"
-| "numbound0 (CN n i a) = (n >0 \<and> numbound0 a)"
-| "numbound0 (Neg a) = numbound0 a"
-| "numbound0 (Add a b) = (numbound0 a \<and> numbound0 b)"
-| "numbound0 (Sub a b) = (numbound0 a \<and> numbound0 b)"
-| "numbound0 (Mul i a) = numbound0 a"
+  "numbound0 (C c) \<longleftrightarrow> True"
+| "numbound0 (Bound n) \<longleftrightarrow> n > 0"
+| "numbound0 (CN n i a) \<longleftrightarrow> n > 0 \<and> numbound0 a"
+| "numbound0 (Neg a) \<longleftrightarrow> numbound0 a"
+| "numbound0 (Add a b) \<longleftrightarrow> numbound0 a \<and> numbound0 b"
+| "numbound0 (Sub a b) \<longleftrightarrow> numbound0 a \<and> numbound0 b"
+| "numbound0 (Mul i a) \<longleftrightarrow> numbound0 a"
 
 lemma numbound0_I:
   assumes nb: "numbound0 a"
-  shows "Inum (b#bs) a = Inum (b'#bs) a"
+  shows "Inum (b # bs) a = Inum (b' # bs) a"
   using nb by (induct a rule: num.induct) (auto simp add: gr0_conv_Suc)
 
 primrec bound0 :: "fm \<Rightarrow> bool" -- {* A Formula is independent of Bound 0 *}
 where
-  "bound0 T = True"
-| "bound0 F = True"
-| "bound0 (Lt a) = numbound0 a"
-| "bound0 (Le a) = numbound0 a"
-| "bound0 (Gt a) = numbound0 a"
-| "bound0 (Ge a) = numbound0 a"
-| "bound0 (Eq a) = numbound0 a"
-| "bound0 (NEq a) = numbound0 a"
-| "bound0 (Dvd i a) = numbound0 a"
-| "bound0 (NDvd i a) = numbound0 a"
-| "bound0 (NOT p) = bound0 p"
-| "bound0 (And p q) = (bound0 p \<and> bound0 q)"
-| "bound0 (Or p q) = (bound0 p \<and> bound0 q)"
-| "bound0 (Imp p q) = ((bound0 p) \<and> (bound0 q))"
-| "bound0 (Iff p q) = (bound0 p \<and> bound0 q)"
-| "bound0 (E p) = False"
-| "bound0 (A p) = False"
-| "bound0 (Closed P) = True"
-| "bound0 (NClosed P) = True"
+  "bound0 T \<longleftrightarrow> True"
+| "bound0 F \<longleftrightarrow> True"
+| "bound0 (Lt a) \<longleftrightarrow> numbound0 a"
+| "bound0 (Le a) \<longleftrightarrow> numbound0 a"
+| "bound0 (Gt a) \<longleftrightarrow> numbound0 a"
+| "bound0 (Ge a) \<longleftrightarrow> numbound0 a"
+| "bound0 (Eq a) \<longleftrightarrow> numbound0 a"
+| "bound0 (NEq a) \<longleftrightarrow> numbound0 a"
+| "bound0 (Dvd i a) \<longleftrightarrow> numbound0 a"
+| "bound0 (NDvd i a) \<longleftrightarrow> numbound0 a"
+| "bound0 (NOT p) \<longleftrightarrow> bound0 p"
+| "bound0 (And p q) \<longleftrightarrow> bound0 p \<and> bound0 q"
+| "bound0 (Or p q) \<longleftrightarrow> bound0 p \<and> bound0 q"
+| "bound0 (Imp p q) \<longleftrightarrow> bound0 p \<and> bound0 q"
+| "bound0 (Iff p q) \<longleftrightarrow> bound0 p \<and> bound0 q"
+| "bound0 (E p) \<longleftrightarrow> False"
+| "bound0 (A p) \<longleftrightarrow> False"
+| "bound0 (Closed P) \<longleftrightarrow> True"
+| "bound0 (NClosed P) \<longleftrightarrow> True"
 
 lemma bound0_I:
   assumes bp: "bound0 p"
-  shows "Ifm bbs (b#bs) p = Ifm bbs (b'#bs) p"
+  shows "Ifm bbs (b # bs) p = Ifm bbs (b' # bs) p"
   using bp numbound0_I[where b="b" and bs="bs" and b'="b'"]
   by (induct p rule: fm.induct) (auto simp add: gr0_conv_Suc)
 
@@ -256,19 +256,19 @@
 
 fun isatom :: "fm \<Rightarrow> bool"  -- {* test for atomicity *}
 where
-  "isatom T = True"
-| "isatom F = True"
-| "isatom (Lt a) = True"
-| "isatom (Le a) = True"
-| "isatom (Gt a) = True"
-| "isatom (Ge a) = True"
-| "isatom (Eq a) = True"
-| "isatom (NEq a) = True"
-| "isatom (Dvd i b) = True"
-| "isatom (NDvd i b) = True"
-| "isatom (Closed P) = True"
-| "isatom (NClosed P) = True"
-| "isatom p = False"
+  "isatom T \<longleftrightarrow> True"
+| "isatom F \<longleftrightarrow> True"
+| "isatom (Lt a) \<longleftrightarrow> True"
+| "isatom (Le a) \<longleftrightarrow> True"
+| "isatom (Gt a) \<longleftrightarrow> True"
+| "isatom (Ge a) \<longleftrightarrow> True"
+| "isatom (Eq a) \<longleftrightarrow> True"
+| "isatom (NEq a) \<longleftrightarrow> True"
+| "isatom (Dvd i b) \<longleftrightarrow> True"
+| "isatom (NDvd i b) \<longleftrightarrow> True"
+| "isatom (Closed P) \<longleftrightarrow> True"
+| "isatom (NClosed P) \<longleftrightarrow> True"
+| "isatom p \<longleftrightarrow> False"
 
 lemma numsubst0_numbound0:
   assumes "numbound0 t"
@@ -423,10 +423,10 @@
 
 consts numadd:: "num \<times> num \<Rightarrow> num"
 recdef numadd "measure (\<lambda>(t, s). num_size t + num_size s)"
-  "numadd (CN n1 c1 r1 ,CN n2 c2 r2) =
+  "numadd (CN n1 c1 r1, CN n2 c2 r2) =
     (if n1 = n2 then
-      (let c = c1 + c2
-       in if c = 0 then numadd (r1, r2) else CN n1 c (numadd (r1, r2)))
+       let c = c1 + c2
+       in if c = 0 then numadd (r1, r2) else CN n1 c (numadd (r1, r2))
      else if n1 \<le> n2 then CN n1 c1 (numadd (r1, Add (Mul c2 (Bound n2)) r2))
      else CN n2 c2 (numadd (Add (Mul c1 (Bound n1)) r1, r2)))"
   "numadd (CN n1 c1 r1, t) = CN n1 c1 (numadd (r1, t))"
@@ -1108,8 +1108,8 @@
 
 lemma zlfm_I:
   assumes qfp: "qfree p"
-  shows "(Ifm bbs (i # bs) (zlfm p) = Ifm bbs (i # bs) p) \<and> iszlfm (zlfm p)"
-  (is "(?I (?l p) = ?I p) \<and> ?L (?l p)")
+  shows "Ifm bbs (i # bs) (zlfm p) = Ifm bbs (i # bs) p \<and> iszlfm (zlfm p)"
+  (is "?I (?l p) = ?I p \<and> ?L (?l p)")
   using qfp
 proof (induct p rule: zlfm.induct)
   case (5 a)
@@ -2204,20 +2204,20 @@
     \<Longrightarrow> (\<exists>(x::int). P x) = ((\<exists>(j::int) \<in> {1..D}. P1 j) \<or> (\<exists>(j::int) \<in> {1..D}. \<exists>(b::int) \<in> B. P (b + j)))"
   apply(rule iffI)
   prefer 2
-  apply(drule minusinfinity)
+  apply (drule minusinfinity)
   apply assumption+
-  apply(fastforce)
+  apply fastforce
   apply clarsimp
-  apply(subgoal_tac "!!k. 0<=k \<Longrightarrow> !x. P x \<longrightarrow> P (x - k*D)")
-  apply(frule_tac x = x and z=z in decr_lemma)
-  apply(subgoal_tac "P1(x - (\<bar>x - z\<bar> + 1) * D)")
+  apply (subgoal_tac "\<And>k. 0 \<le> k \<Longrightarrow> \<forall>x. P x \<longrightarrow> P (x - k * D)")
+  apply (frule_tac x = x and z=z in decr_lemma)
+  apply (subgoal_tac "P1 (x - (\<bar>x - z\<bar> + 1) * D)")
   prefer 2
-  apply(subgoal_tac "0 <= (\<bar>x - z\<bar> + 1)")
+  apply (subgoal_tac "0 \<le> \<bar>x - z\<bar> + 1")
   prefer 2 apply arith
    apply fastforce
-  apply(drule (1)  periodic_finite_ex)
+  apply (drule (1)  periodic_finite_ex)
   apply blast
-  apply(blast dest:decr_mult_lemma)
+  apply (blast dest: decr_mult_lemma)
   done
 
 theorem cp_thm:
@@ -2297,7 +2297,7 @@
 proof -
   fix q B d
   assume qBd: "unit p = (q,B,d)"
-  let ?thes = "((\<exists>x. Ifm bbs (x#bs) p) = (\<exists>x. Ifm bbs (x#bs) q)) \<and>
+  let ?thes = "((\<exists>x. Ifm bbs (x#bs) p) \<longleftrightarrow> (\<exists>x. Ifm bbs (x#bs) q)) \<and>
     Inum (i#bs) ` set B = Inum (i#bs) ` set (\<beta> q) \<and>
     d_\<beta> q 1 \<and> d_\<delta> q d \<and> 0 < d \<and> iszlfm q \<and> (\<forall>b\<in> set B. numbound0 b)"
   let ?I = "\<lambda>x p. Ifm bbs (x#bs) p"
@@ -2319,34 +2319,47 @@
   from lp' lp a_\<beta>[OF lp' dl lp] have lq:"iszlfm ?q" and uq: "d_\<beta> ?q 1"  by auto
   from \<delta>[OF lq] have dp:"?d >0" and dd: "d_\<delta> ?q ?d" by blast+
   let ?N = "\<lambda>t. Inum (i#bs) t"
-  have "?N ` set ?B' = ((?N o simpnum) ` ?B)" by auto
-  also have "\<dots> = ?N ` ?B" using simpnum_ci[where bs="i#bs"] by auto
+  have "?N ` set ?B' = ((?N \<circ> simpnum) ` ?B)"
+    by auto
+  also have "\<dots> = ?N ` ?B"
+    using simpnum_ci[where bs="i#bs"] by auto
   finally have BB': "?N ` set ?B' = ?N ` ?B" .
-  have "?N ` set ?A' = ((?N o simpnum) ` ?A)" by auto
-  also have "\<dots> = ?N ` ?A" using simpnum_ci[where bs="i#bs"] by auto
+  have "?N ` set ?A' = ((?N \<circ> simpnum) ` ?A)"
+    by auto
+  also have "\<dots> = ?N ` ?A"
+    using simpnum_ci[where bs="i#bs"] by auto
   finally have AA': "?N ` set ?A' = ?N ` ?A" .
   from \<beta>_numbound0[OF lq] have B_nb:"\<forall>b\<in> set ?B'. numbound0 b"
     by (simp add: simpnum_numbound0)
   from \<alpha>_l[OF lq] have A_nb: "\<forall>b\<in> set ?A'. numbound0 b"
     by (simp add: simpnum_numbound0)
-    {assume "length ?B' \<le> length ?A'"
-    then have q:"q=?q" and "B = ?B'" and d:"d = ?d"
+  {
+    assume "length ?B' \<le> length ?A'"
+    then have q: "q = ?q" and "B = ?B'" and d: "d = ?d"
       using qBd by (auto simp add: Let_def unit_def)
-    with BB' B_nb have b: "?N ` (set B) = ?N ` set (\<beta> q)"
-      and bn: "\<forall>b\<in> set B. numbound0 b" by simp_all
-  with pq_ex dp uq dd lq q d have ?thes by simp}
+    with BB' B_nb
+    have b: "?N ` (set B) = ?N ` set (\<beta> q)" and bn: "\<forall>b\<in> set B. numbound0 b"
+      by simp_all
+    with pq_ex dp uq dd lq q d have ?thes
+      by simp
+  }
   moreover
-  {assume "\<not> (length ?B' \<le> length ?A')"
+  {
+    assume "\<not> (length ?B' \<le> length ?A')"
     then have q:"q=mirror ?q" and "B = ?A'" and d:"d = ?d"
       using qBd by (auto simp add: Let_def unit_def)
     with AA' mirror_\<alpha>_\<beta>[OF lq] A_nb have b:"?N ` (set B) = ?N ` set (\<beta> q)"
       and bn: "\<forall>b\<in> set B. numbound0 b" by simp_all
     from mirror_ex[OF lq] pq_ex q
-    have pqm_eq:"(\<exists>(x::int). ?I x p) = (\<exists>(x::int). ?I x q)" by simp
+    have pqm_eq:"(\<exists>(x::int). ?I x p) = (\<exists>(x::int). ?I x q)"
+      by simp
     from lq uq q mirror_l[where p="?q"]
-    have lq': "iszlfm q" and uq: "d_\<beta> q 1" by auto
-    from \<delta>[OF lq'] mirror_\<delta>[OF lq] q d have dq:"d_\<delta> q d " by auto
-    from pqm_eq b bn uq lq' dp dq q dp d have ?thes by simp
+    have lq': "iszlfm q" and uq: "d_\<beta> q 1"
+      by auto
+    from \<delta>[OF lq'] mirror_\<delta>[OF lq] q d have dq: "d_\<delta> q d"
+      by auto
+    from pqm_eq b bn uq lq' dp dq q dp d have ?thes
+      by simp
   }
   ultimately show ?thes by blast
 qed
@@ -2354,7 +2367,8 @@
 
 text {* Cooper's Algorithm *}
 
-definition cooper :: "fm \<Rightarrow> fm" where
+definition cooper :: "fm \<Rightarrow> fm"
+where
   "cooper p =
     (let
       (q, B, d) = unit p;
@@ -2386,60 +2400,67 @@
   let ?Bjs = "[(b,j). b\<leftarrow>?B,j\<leftarrow>?js]"
   let ?qd = "evaldjf (\<lambda>(b,j). simpfm (subst0 (Add b (C j)) ?q)) ?Bjs"
   have qbf:"unit p = (?q,?B,?d)" by simp
-  from unit[OF qf qbf] have pq_ex: "(\<exists>(x::int). ?I x p) = (\<exists>(x::int). ?I x ?q)" and
-    B:"?N ` set ?B = ?N ` set (\<beta> ?q)" and
-    uq:"d_\<beta> ?q 1" and dd: "d_\<delta> ?q ?d" and dp: "?d > 0" and
-    lq: "iszlfm ?q" and
-    Bn: "\<forall>b\<in> set ?B. numbound0 b" by auto
+  from unit[OF qf qbf]
+  have pq_ex: "(\<exists>(x::int). ?I x p) \<longleftrightarrow> (\<exists>(x::int). ?I x ?q)"
+    and B: "?N ` set ?B = ?N ` set (\<beta> ?q)"
+    and uq: "d_\<beta> ?q 1"
+    and dd: "d_\<delta> ?q ?d"
+    and dp: "?d > 0"
+    and lq: "iszlfm ?q"
+    and Bn: "\<forall>b\<in> set ?B. numbound0 b"
+    by auto
   from zlin_qfree[OF lq] have qfq: "qfree ?q" .
   from simpfm_qf[OF minusinf_qfree[OF qfq]] have qfmq: "qfree ?smq" .
-  have jsnb: "\<forall>j \<in> set ?js. numbound0 (C j)" by simp
+  have jsnb: "\<forall>j \<in> set ?js. numbound0 (C j)"
+    by simp
   then have "\<forall>j\<in> set ?js. bound0 (subst0 (C j) ?smq)"
     by (auto simp only: subst0_bound0[OF qfmq])
   then have th: "\<forall>j\<in> set ?js. bound0 (simpfm (subst0 (C j) ?smq))"
     by (auto simp add: simpfm_bound0)
-  from evaldjf_bound0[OF th] have mdb: "bound0 ?md" by simp
+  from evaldjf_bound0[OF th] have mdb: "bound0 ?md"
+    by simp
   from Bn jsnb have "\<forall>(b,j) \<in> set ?Bjs. numbound0 (Add b (C j))"
     by simp
   then have "\<forall>(b,j) \<in> set ?Bjs. bound0 (subst0 (Add b (C j)) ?q)"
     using subst0_bound0[OF qfq] by blast
   then have "\<forall>(b,j) \<in> set ?Bjs. bound0 (simpfm (subst0 (Add b (C j)) ?q))"
-    using simpfm_bound0  by blast
+    using simpfm_bound0 by blast
   then have th': "\<forall>x \<in> set ?Bjs. bound0 ((\<lambda>(b,j). simpfm (subst0 (Add b (C j)) ?q)) x)"
     by auto
-  from evaldjf_bound0 [OF th'] have qdb: "bound0 ?qd" by simp
-  from mdb qdb
-  have mdqdb: "bound0 (disj ?md ?qd)"
-    unfolding disj_def by (cases "?md=T \<or> ?qd=T") simp_all
+  from evaldjf_bound0 [OF th'] have qdb: "bound0 ?qd"
+    by simp
+  from mdb qdb have mdqdb: "bound0 (disj ?md ?qd)"
+    unfolding disj_def by (cases "?md = T \<or> ?qd = T") simp_all
   from trans [OF pq_ex cp_thm'[OF lq uq dd dp,where i="i"]] B
-  have "?lhs = (\<exists>j\<in> {1.. ?d}. ?I j ?mq \<or> (\<exists>b\<in> ?N ` set ?B. Ifm bbs ((b+ j)#bs) ?q))"
+  have "?lhs \<longleftrightarrow> (\<exists>j \<in> {1.. ?d}. ?I j ?mq \<or> (\<exists>b \<in> ?N ` set ?B. Ifm bbs ((b + j) # bs) ?q))"
     by auto
-  also have "\<dots> = (\<exists>j\<in> {1.. ?d}. ?I j ?mq \<or> (\<exists>b\<in> set ?B. Ifm bbs ((?N b+ j)#bs) ?q))"
+  also have "\<dots> \<longleftrightarrow> (\<exists>j \<in> {1.. ?d}. ?I j ?mq \<or> (\<exists>b \<in> set ?B. Ifm bbs ((?N b + j) # bs) ?q))"
     by simp
-  also have "\<dots> = ((\<exists>j\<in> {1.. ?d}. ?I j ?mq ) \<or>
-      (\<exists>j\<in> {1.. ?d}. \<exists>b\<in> set ?B. Ifm bbs ((?N (Add b (C j)))#bs) ?q))"
+  also have "\<dots> \<longleftrightarrow> (\<exists>j \<in> {1.. ?d}. ?I j ?mq ) \<or>
+      (\<exists>j\<in> {1.. ?d}. \<exists>b \<in> set ?B. Ifm bbs ((?N (Add b (C j))) # bs) ?q)"
     by (simp only: Inum.simps) blast
-  also have "\<dots> = ((\<exists>j\<in> {1.. ?d}. ?I j ?smq ) \<or>
-      (\<exists>j\<in> {1.. ?d}. \<exists>b\<in> set ?B. Ifm bbs ((?N (Add b (C j)))#bs) ?q))"
+  also have "\<dots> \<longleftrightarrow> (\<exists>j \<in> {1.. ?d}. ?I j ?smq) \<or>
+      (\<exists>j \<in> {1.. ?d}. \<exists>b \<in> set ?B. Ifm bbs ((?N (Add b (C j))) # bs) ?q)"
     by (simp add: simpfm)
-  also have "\<dots> = ((\<exists>j\<in> set ?js. (\<lambda>j. ?I i (simpfm (subst0 (C j) ?smq))) j) \<or>
-      (\<exists>j\<in> set ?js. \<exists>b\<in> set ?B. Ifm bbs ((?N (Add b (C j)))#bs) ?q))"
+  also have "\<dots> \<longleftrightarrow> (\<exists>j\<in> set ?js. (\<lambda>j. ?I i (simpfm (subst0 (C j) ?smq))) j) \<or>
+      (\<exists>j\<in> set ?js. \<exists>b\<in> set ?B. Ifm bbs ((?N (Add b (C j)))#bs) ?q)"
     by (simp only: simpfm subst0_I[OF qfmq] set_upto) auto
-  also have "\<dots> = (?I i (evaldjf (\<lambda>j. simpfm (subst0 (C j) ?smq)) ?js) \<or>
-      (\<exists>j\<in> set ?js. \<exists>b\<in> set ?B. ?I i (subst0 (Add b (C j)) ?q)))"
+  also have "\<dots> \<longleftrightarrow> ?I i (evaldjf (\<lambda>j. simpfm (subst0 (C j) ?smq)) ?js) \<or>
+      (\<exists>j\<in> set ?js. \<exists>b\<in> set ?B. ?I i (subst0 (Add b (C j)) ?q))"
     by (simp only: evaldjf_ex subst0_I[OF qfq])
-  also have "\<dots>= (?I i ?md \<or> (\<exists>(b,j) \<in> set ?Bjs. (\<lambda>(b,j). ?I i (simpfm (subst0 (Add b (C j)) ?q))) (b,j)))"
+  also have "\<dots> \<longleftrightarrow> ?I i ?md \<or>
+      (\<exists>(b,j) \<in> set ?Bjs. (\<lambda>(b,j). ?I i (simpfm (subst0 (Add b (C j)) ?q))) (b,j))"
     by (simp only: simpfm set_concat set_map concat_map_singleton UN_simps) blast
-  also have "\<dots> = (?I i ?md \<or> (?I i (evaldjf (\<lambda>(b,j). simpfm (subst0 (Add b (C j)) ?q)) ?Bjs)))"
+  also have "\<dots> \<longleftrightarrow> ?I i ?md \<or> ?I i (evaldjf (\<lambda>(b,j). simpfm (subst0 (Add b (C j)) ?q)) ?Bjs)"
     by (simp only: evaldjf_ex[where bs="i#bs" and f="\<lambda>(b,j). simpfm (subst0 (Add b (C j)) ?q)" and ps="?Bjs"])
       (auto simp add: split_def)
-  finally have mdqd: "?lhs = (?I i ?md \<or> ?I i ?qd)"
+  finally have mdqd: "?lhs \<longleftrightarrow> ?I i ?md \<or> ?I i ?qd"
     by simp
-  also have "\<dots> = (?I i (disj ?md ?qd))"
+  also have "\<dots> \<longleftrightarrow> ?I i (disj ?md ?qd)"
     by (simp add: disj)
-  also have "\<dots> = (Ifm bbs bs (decr (disj ?md ?qd)))"
+  also have "\<dots> \<longleftrightarrow> Ifm bbs bs (decr (disj ?md ?qd))"
     by (simp only: decr [OF mdqdb])
-  finally have mdqd2: "?lhs = (Ifm bbs bs (decr (disj ?md ?qd)))" .
+  finally have mdqd2: "?lhs \<longleftrightarrow> Ifm bbs bs (decr (disj ?md ?qd))" .
   {
     assume mdT: "?md = T"
     then have cT: "cooper p = T"
@@ -2448,7 +2469,8 @@
       using mdqd by simp
     from mdT have "?rhs"
       by (simp add: cooper_def unit_def split_def)
-    with lhs cT have ?thesis by simp
+    with lhs cT have ?thesis
+      by simp
   }
   moreover
   {
diff -r 6d123f0ae358 -r ffe88d72afae src/HOL/Decision_Procs/cooper_tac.ML
--- a/src/HOL/Decision_Procs/cooper_tac.ML	Fri Mar 07 15:52:56 2014 +0000
+++ b/src/HOL/Decision_Procs/cooper_tac.ML	Fri Mar 07 20:50:02 2014 +0100
@@ -12,22 +12,6 @@
 
 val cooper_ss = simpset_of @{context};
 
-val nT = HOLogic.natT;
-val comp_arith = @{thms simp_thms}
-
-val zdvd_int = @{thm zdvd_int};
-val zdiff_int_split = @{thm zdiff_int_split};
-val split_zdiv = @{thm split_zdiv};
-val split_zmod = @{thm split_zmod};
-val mod_div_equality' = @{thm mod_div_equality'};
-val split_div' = @{thm split_div'};
-val Suc_eq_plus1 = @{thm Suc_eq_plus1};
-val mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
-val mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
-val mod_add_eq = @{thm mod_add_eq} RS sym;
-val nat_div_add_eq = @{thm div_add1_eq} RS sym;
-val int_div_add_eq = @{thm zdiv_zadd1_eq} RS sym;
-
 fun prepare_for_linz q fm =
   let
     val ps = Logic.strip_params fm
@@ -42,53 +26,51 @@
     val np = length ps
     val (fm',np) = List.foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
       (List.foldr HOLogic.mk_imp c rhs, np) ps
-    val (vs, _) = List.partition (fn t => q orelse (type_of t) = nT)
+    val (vs, _) = List.partition (fn t => q orelse (type_of t) = @{typ nat})
       (Misc_Legacy.term_frees fm' @ Misc_Legacy.term_vars fm');
     val fm2 = List.foldr mk_all2 fm' vs
   in (fm2, np + length vs, length rhs) end;
 
 (*Object quantifier to meta --*)
-fun spec_step n th = if (n=0) then th else (spec_step (n-1) th) RS spec ;
+fun spec_step n th = if n = 0 then th else (spec_step (n - 1) th) RS spec;
 
 (* object implication to meta---*)
-fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp;
+fun mp_step n th = if n = 0 then th else (mp_step (n - 1) th) RS mp;
 
 
 fun linz_tac ctxt q = Object_Logic.atomize_prems_tac ctxt THEN' SUBGOAL (fn (g, i) =>
   let
-    val thy = Proof_Context.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt;
     (* Transform the term*)
-    val (t,np,nh) = prepare_for_linz q g
+    val (t, np, nh) = prepare_for_linz q g;
     (* Some simpsets for dealing with mod div abs and nat*)
     val mod_div_simpset =
       put_simpset HOL_basic_ss ctxt
-      addsimps [refl,mod_add_eq, mod_add_left_eq,
-          mod_add_right_eq,
-          nat_div_add_eq, int_div_add_eq,
-          @{thm mod_self},
-          @{thm div_by_0}, @{thm mod_by_0}, @{thm div_0}, @{thm mod_0},
-          @{thm div_by_1}, @{thm mod_by_1}, @{thm div_1}, @{thm mod_1},
-          Suc_eq_plus1]
+      addsimps @{thms refl mod_add_eq [symmetric] mod_add_left_eq [symmetric]
+          mod_add_right_eq [symmetric]
+          div_add1_eq [symmetric] zdiv_zadd1_eq [symmetric]
+          mod_self
+          div_by_0 mod_by_0 div_0 mod_0
+          div_by_1 mod_by_1 div_1 mod_1
+          Suc_eq_plus1}
       addsimps @{thms add_ac}
       addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}]
     val simpset0 =
       put_simpset HOL_basic_ss ctxt
-      addsimps [mod_div_equality', Suc_eq_plus1]
-      addsimps comp_arith
-      |> fold Splitter.add_split
-          [split_zdiv, split_zmod, split_div', @{thm "split_min"}, @{thm "split_max"}]
+      addsimps @{thms mod_div_equality' Suc_eq_plus1 simp_thms}
+      |> fold Splitter.add_split @{thms split_zdiv split_zmod split_div' split_min split_max}
     (* Simp rules for changing (n::int) to int n *)
     val simpset1 =
       put_simpset HOL_basic_ss ctxt
-      addsimps [zdvd_int] @ map (fn r => r RS sym)
-        [@{thm int_numeral}, @{thm int_int_eq}, @{thm zle_int}, @{thm zless_int}, @{thm zadd_int}, @{thm zmult_int}]
-      |> Splitter.add_split zdiff_int_split
+      addsimps @{thms zdvd_int} @
+        map (fn r => r RS sym) @{thms int_numeral int_int_eq zle_int zless_int zadd_int zmult_int}
+      |> Splitter.add_split @{thm zdiff_int_split}
     (*simp rules for elimination of int n*)
 
     val simpset2 =
       put_simpset HOL_basic_ss ctxt
       addsimps [@{thm nat_0_le}, @{thm all_nat}, @{thm ex_nat}, @{thm zero_le_numeral}, @{thm order_refl}(* FIXME: necessary? *), @{thm int_0}, @{thm int_1}]
-      |> fold Simplifier.add_cong [@{thm conj_le_cong}, @{thm imp_le_cong}]
+      |> fold Simplifier.add_cong @{thms conj_le_cong imp_le_cong}
     (* simp rules for elimination of abs *)
     val simpset3 = put_simpset HOL_basic_ss ctxt |> Splitter.add_split @{thm abs_split}
     val ct = cterm_of thy (HOLogic.mk_Trueprop t)
@@ -100,14 +82,16 @@
       (Thm.trivial ct))
     fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
     (* The result of the quantifier elimination *)
-    val (th, tac) = case (prop_of pre_thm) of
+    val (th, tac) =
+      (case (prop_of pre_thm) of
         Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
-    let val pth = linzqe_oracle (cterm_of thy (Envir.eta_long [] t1))
-    in
-          ((pth RS iffD2) RS pre_thm,
-            assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))
-    end
-      | _ => (pre_thm, assm_tac i)
-  in rtac (((mp_step nh) o (spec_step np)) th) i THEN tac end);
+          let
+            val pth = linzqe_oracle (cterm_of thy (Envir.eta_long [] t1))
+          in
+            ((pth RS iffD2) RS pre_thm,
+              assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))
+          end
+      | _ => (pre_thm, assm_tac i))
+  in rtac (mp_step nh (spec_step np th)) i THEN tac end);
 
 end
diff -r 6d123f0ae358 -r ffe88d72afae src/HOL/Num.thy
--- a/src/HOL/Num.thy	Fri Mar 07 15:52:56 2014 +0000
+++ b/src/HOL/Num.thy	Fri Mar 07 20:50:02 2014 +0100
@@ -285,14 +285,14 @@
     fun num_of_int n =
       if n > 0 then
         (case IntInf.quotRem (n, 2) of
-          (0, 1) => Syntax.const @{const_name One}
-        | (n, 0) => Syntax.const @{const_name Bit0} $ num_of_int n
-        | (n, 1) => Syntax.const @{const_name Bit1} $ num_of_int n)
+          (0, 1) => Syntax.const @{const_syntax One}
+        | (n, 0) => Syntax.const @{const_syntax Bit0} $ num_of_int n
+        | (n, 1) => Syntax.const @{const_syntax Bit1} $ num_of_int n)
       else raise Match
-    val numeral = Syntax.const @{const_name numeral}
-    val uminus = Syntax.const @{const_name uminus}
-    val one = Syntax.const @{const_name Groups.one}
-    val zero = Syntax.const @{const_name Groups.zero}
+    val numeral = Syntax.const @{const_syntax numeral}
+    val uminus = Syntax.const @{const_syntax uminus}
+    val one = Syntax.const @{const_syntax Groups.one}
+    val zero = Syntax.const @{const_syntax Groups.zero}
     fun numeral_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
           c $ numeral_tr [t] $ u
       | numeral_tr [Const (num, _)] =
@@ -303,10 +303,10 @@
             if value > 0
             then numeral $ num_of_int value
             else if value = ~1 then uminus $ one
-            else uminus $ (numeral $ num_of_int (~value))
+            else uminus $ (numeral $ num_of_int (~ value))
           end
       | numeral_tr ts = raise TERM ("numeral_tr", ts);
-  in [("_Numeral", K numeral_tr)] end
+  in [(@{syntax_const "_Numeral"}, K numeral_tr)] end
 *}
 
 typed_print_translation {*
diff -r 6d123f0ae358 -r ffe88d72afae src/HOL/ROOT
--- a/src/HOL/ROOT	Fri Mar 07 15:52:56 2014 +0000
+++ b/src/HOL/ROOT	Fri Mar 07 20:50:02 2014 +0100
@@ -213,7 +213,6 @@
     Verification of imperative programs (verification conditions are generated
     automatically from pre/post conditions and loop invariants).
   *}
-
   theories Hoare
   files "document/root.bib" "document/root.tex"
 
diff -r 6d123f0ae358 -r ffe88d72afae src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Fri Mar 07 15:52:56 2014 +0000
+++ b/src/HOL/Rat.thy	Fri Mar 07 20:50:02 2014 +0100
@@ -1155,12 +1155,16 @@
       let
         fun mk 1 = Syntax.const @{const_syntax Num.One}
           | mk i =
-              let val (q, r) = Integer.div_mod i 2
-              in HOLogic.mk_bit r $ (mk q) end;
+              let
+                val (q, r) = Integer.div_mod i 2;
+                val bit = if r = 0 then @{const_syntax Num.Bit0} else @{const_syntax Num.Bit1};
+              in Syntax.const bit $ (mk q) end;
       in
         if i = 0 then Syntax.const @{const_syntax Groups.zero}
         else if i > 0 then Syntax.const @{const_syntax Num.numeral} $ mk i
-        else Syntax.const @{const_syntax Groups.uminus} $ (Syntax.const @{const_syntax Num.numeral} $ mk (~i))
+        else
+          Syntax.const @{const_syntax Groups.uminus} $
+            (Syntax.const @{const_syntax Num.numeral} $ mk (~ i))
       end;
 
     fun mk_frac str =
@@ -1181,6 +1185,7 @@
 lemma "123.456 = -111.111 + 200 + 30 + 4 + 5/10 + 6/100 + (7/1000::rat)"
   by simp
 
+
 subsection {* Hiding implementation details *}
 
 hide_const (open) normalize positive
diff -r 6d123f0ae358 -r ffe88d72afae src/HOL/Statespace/distinct_tree_prover.ML
--- a/src/HOL/Statespace/distinct_tree_prover.ML	Fri Mar 07 15:52:56 2014 +0000
+++ b/src/HOL/Statespace/distinct_tree_prover.ML	Fri Mar 07 20:50:02 2014 +0100
@@ -77,14 +77,6 @@
   | x => x);
 
 
-fun index_tree (Const (@{const_name Tip}, _)) path tab = tab
-  | index_tree (Const (@{const_name Node}, _) $ l $ x $ _ $ r) path tab =
-      tab
-      |> Termtab.update_new (x, path)
-      |> index_tree l (path @ [Left])
-      |> index_tree r (path @ [Right])
-  | index_tree t _ _ = raise TERM ("index_tree: input not a tree", [t])
-
 fun split_common_prefix xs [] = ([], xs, [])
   | split_common_prefix [] ys = ([], [], ys)
   | split_common_prefix (xs as (x :: xs')) (ys as (y :: ys')) =
@@ -138,7 +130,6 @@
  *)
 fun naive_cterm_first_order_match (t, ct) env =
   let
-    val thy = theory_of_cterm ct;
     fun mtch (env as (tyinsts, insts)) =
       fn (Var (ixn, T), ct) =>
           (case AList.lookup (op =) insts ixn of
diff -r 6d123f0ae358 -r ffe88d72afae src/HOL/Statespace/state_fun.ML
--- a/src/HOL/Statespace/state_fun.ML	Fri Mar 07 15:52:56 2014 +0000
+++ b/src/HOL/Statespace/state_fun.ML	Fri Mar 07 20:50:02 2014 +0100
@@ -174,7 +174,7 @@
   Simplifier.simproc_global @{theory} "update_simp" ["update d c n v s"]
     (fn ctxt => fn t =>
       (case t of
-        ((upd as Const (@{const_name StateFun.update}, uT)) $ d $ c $ n $ v $ s) =>
+        Const (@{const_name StateFun.update}, uT) $ _ $ _ $ _ $ _ $ _ =>
           let
             val (_ :: _ :: _ :: _ :: sT :: _) = binder_types uT;
               (*"('v => 'a1) => ('a2 => 'v) => 'n => ('a1 => 'a2) => ('n => 'v) => ('n => 'v)"*)
@@ -208,7 +208,7 @@
                 * updates again, the optimised term is constructed.
                 *)
             fun mk_updterm already
-                (t as ((upd as Const (@{const_name StateFun.update}, uT)) $ d $ c $ n $ v $ s)) =
+                ((upd as Const (@{const_name StateFun.update}, uT)) $ d $ c $ n $ v $ s) =
                   let
                     fun rest already = mk_updterm already;
                     val (dT :: cT :: nT :: vT :: sT :: _) = binder_types uT;
@@ -238,7 +238,8 @@
                               Const (@{const_name StateFun.update},
                                 d'T --> c'T --> nT --> vT' --> sT --> sT);
                           in
-                            (upd $ d $ c $ n $ kb $ trm, upd' $ d' $ c' $ n $ f' $ trm', kv :: vars, comps', b)
+                            (upd $ d $ c $ n $ kb $ trm, upd' $ d' $ c' $ n $ f' $ trm', kv :: vars,
+                              comps', b)
                           end)
                   end
               | mk_updterm _ t = init_seed t;
diff -r 6d123f0ae358 -r ffe88d72afae src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Fri Mar 07 15:52:56 2014 +0000
+++ b/src/HOL/Statespace/state_space.ML	Fri Mar 07 20:50:02 2014 +0100
@@ -78,16 +78,6 @@
 fun fold1' f [] x = x
   | fold1' f xs _ = fold1 f xs
 
-fun sublist_idx eq xs ys =
-  let
-    fun sublist n xs ys =
-         if is_prefix eq xs ys then SOME n
-         else (case ys of [] => NONE
-               | (y::ys') => sublist (n+1) xs ys')
-  in sublist 0 xs ys end;
-
-fun is_sublist eq xs ys = is_some (sublist_idx eq xs ys);
-
 fun sorted_subset eq [] ys = true
   | sorted_subset eq (x::xs) [] = false
   | sorted_subset eq (x::xs) (y::ys) = if eq (x,y) then sorted_subset eq xs ys
@@ -118,13 +108,6 @@
      {declinfo=declinfo,distinctthm=distinctthm,silent=silent};
 
 
-fun delete_declinfo n ctxt =
-  let val {declinfo,distinctthm,silent} = NameSpaceData.get ctxt;
-  in NameSpaceData.put
-       (make_namespace_data (Termtab.delete_safe n declinfo) distinctthm silent) ctxt
-  end;
-
-
 fun update_declinfo (n,v) ctxt =
   let val {declinfo,distinctthm,silent} = NameSpaceData.get ctxt;
   in NameSpaceData.put
@@ -252,7 +235,6 @@
   let
     val all_comps = parent_comps @ new_comps;
     val vars = (map (fn n => (Binding.name n, NONE, NoSyn)) all_comps);
-    val full_name = Sign.full_bname thy name;
     val dist_thm_name = distinct_compsN;
 
     val dist_thm_full_name = dist_thm_name;
@@ -296,7 +278,7 @@
     |> interprete_parent name dist_thm_full_name parent_expr
   end;
 
-fun encode_dot x = if x= #"." then #"_" else x;
+fun encode_dot x = if x = #"." then #"_" else x;
 
 fun encode_type (TFree (s, _)) = s
   | encode_type (TVar ((s,i),_)) = "?" ^ s ^ string_of_int i
@@ -309,23 +291,6 @@
 fun project_name T = projectN ^"_"^encode_type T;
 fun inject_name T = injectN ^"_"^encode_type T;
 
-fun project_free T pT V = Free (project_name T, V --> pT);
-fun inject_free T pT V = Free (inject_name T, pT --> V);
-
-fun get_name n = getN ^ "_" ^ n;
-fun put_name n = putN ^ "_" ^ n;
-fun get_const n T nT V = Free (get_name n, (nT --> V) --> T);
-fun put_const n T nT V = Free (put_name n, T --> (nT --> V) --> (nT --> V));
-
-fun lookup_const T nT V =
-  Const (@{const_name StateFun.lookup}, (V --> T) --> nT --> (nT --> V) --> T);
-
-fun update_const T nT V =
-  Const (@{const_name StateFun.update},
-    (V --> T) --> (T --> V) --> nT --> (T --> T) --> (nT --> V) --> (nT --> V));
-
-fun K_const T = Const (@{const_name K_statefun}, T --> T --> T);
-
 
 fun add_declaration name decl thy =
   thy
@@ -347,15 +312,12 @@
     val all_comps = rename renaming (parent_comps @ map (apsnd subst) components);
   in all_comps end;
 
-fun take_upto i xs = List.take(xs,i) handle General.Subscript => xs;
-
 fun statespace_definition state_type args name parents parent_comps components thy =
   let
     val full_name = Sign.full_bname thy name;
     val all_comps = parent_comps @ components;
 
     val components' = map (fn (n,T) => (n,(T,full_name))) components;
-    val all_comps' = map (fn (n,T) => (n,(T,full_name))) all_comps;
 
     fun parent_expr (prefix, (_, n, rs)) =
       (suffix namespaceN n, (prefix, Expression.Positional rs));
@@ -452,11 +414,6 @@
 
 (* prepare arguments *)
 
-fun read_raw_parent ctxt raw_T =
-  (case Proof_Context.read_typ_abbrev ctxt raw_T of
-    Type (name, Ts) => (Ts, name)
-  | T => error ("Bad parent statespace specification: " ^ Syntax.string_of_typ ctxt T));
-
 fun read_typ ctxt raw_T env =
   let
     val ctxt' = fold (Variable.declare_typ o TFree) env ctxt;
@@ -587,16 +544,15 @@
 (*** parse/print - translations ***)
 
 local
+
 fun map_get_comp f ctxt (Free (name,_)) =
       (case (get_comp ctxt name) of
         SOME (T,_) => f T T dummyT
       | NONE => (Syntax.free "arbitrary"(*; error "context not ready"*)))
   | map_get_comp _ _ _ = Syntax.free "arbitrary";
 
-val get_comp_projection = map_get_comp project_free;
-val get_comp_injection  = map_get_comp inject_free;
+fun name_of (Free (n,_)) = n;
 
-fun name_of (Free (n,_)) = n;
 in
 
 fun gen_lookup_tr ctxt s n =
@@ -624,7 +580,7 @@
           then Syntax.const "_statespace_lookup" $ s $ n
           else raise Match
       | NONE => raise Match)
-  | lookup_tr' _ ts = raise Match;
+  | lookup_tr' _ _ = raise Match;
 
 fun gen_update_tr id ctxt n v s =
   let
diff -r 6d123f0ae358 -r ffe88d72afae src/HOL/Tools/Ctr_Sugar/case_translation.ML
--- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Fri Mar 07 15:52:56 2014 +0000
+++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Fri Mar 07 20:50:02 2014 +0100
@@ -21,7 +21,6 @@
   val strip_case: Proof.context -> bool -> term -> (term * (term * term) list) option
   val strip_case_full: Proof.context -> bool -> term -> term
   val show_cases: bool Config.T
-  val setup: theory -> theory
   val register: term -> term list -> Context.generic -> Context.generic
 end;
 
@@ -170,7 +169,7 @@
         fun dest_case2 (Const (@{syntax_const "_case2"}, _) $ t $ u) = t :: dest_case2 u
           | dest_case2 t = [t];
 
-        val errt = if err then @{term True} else @{term False};
+        val errt = Syntax.const (if err then @{const_syntax True} else @{const_syntax False});
       in
         Syntax.const @{const_syntax case_guard} $ errt $ t $
           (fold_rev
@@ -180,7 +179,7 @@
       end
   | case_tr _ _ _ = case_error "case_tr";
 
-val trfun_setup = Sign.parse_translation [(@{syntax_const "_case_syntax"}, case_tr true)];
+val _ = Theory.setup (Sign.parse_translation [(@{syntax_const "_case_syntax"}, case_tr true)]);
 
 
 (* print translation *)
@@ -207,7 +206,7 @@
       end
   | case_tr' _ = raise Match;
 
-val trfun_setup' = Sign.print_translation [(@{const_syntax "case_guard"}, K case_tr')];
+val _ = Theory.setup (Sign.print_translation [(@{const_syntax "case_guard"}, K case_tr')]);
 
 
 (* declarations *)
@@ -229,6 +228,12 @@
     |> map_cases update_cases
   end;
 
+val _ = Theory.setup
+  (Attrib.setup @{binding case_translation}
+    (Args.term -- Scan.repeat1 Args.term >>
+      (fn (t, ts) => Thm.declaration_attribute (K (register t ts))))
+    "declaration of case combinators and constructors");
+
 
 (* (Un)check phases *)
 
@@ -453,8 +458,7 @@
     map decode_case
   end;
 
-val term_check_setup =
-  Context.theory_map (Syntax_Phases.term_check 1 "case" check_case);
+val _ = Context.>> (Syntax_Phases.term_check 1 "case" check_case);
 
 
 (* Pretty printing of nested case expressions *)
@@ -595,21 +599,7 @@
   then map (fn t => if can Term.type_of t then strip_case_full ctxt true t else t) ts
   else ts;
 
-val term_uncheck_setup =
-  Context.theory_map (Syntax_Phases.term_uncheck 1 "case" uncheck_case);
-
-
-(* theory setup *)
-
-val setup =
-  trfun_setup #>
-  trfun_setup' #>
-  term_check_setup #>
-  term_uncheck_setup #>
-  Attrib.setup @{binding case_translation}
-    (Args.term -- Scan.repeat1 Args.term >>
-      (fn (t, ts) => Thm.declaration_attribute (K (register t ts))))
-    "declaration of case combinators and constructors";
+val _ = Context.>>  (Syntax_Phases.term_uncheck 1 "case" uncheck_case);
 
 
 (* outer syntax commands *)
diff -r 6d123f0ae358 -r ffe88d72afae src/Pure/General/completion.ML
--- a/src/Pure/General/completion.ML	Fri Mar 07 15:52:56 2014 +0000
+++ b/src/Pure/General/completion.ML	Fri Mar 07 20:50:02 2014 +0100
@@ -7,7 +7,7 @@
 signature COMPLETION =
 sig
   type T
-  val names: Position.T -> (string * string) list -> T
+  val names: Position.T -> (string * (string * string)) list -> T
   val none: T
   val reported_text: T -> string
   val report: T -> unit
@@ -17,7 +17,8 @@
 structure Completion: COMPLETION =
 struct
 
-abstype T = Completion of {pos: Position.T, total: int, names: (string * string) list}
+abstype T =
+  Completion of {pos: Position.T, total: int, names: (string * (string * string)) list}
 with
 
 (* completion of names *)
@@ -40,7 +41,7 @@
       let
         val markup = Position.markup pos Markup.completion;
         val body = (total, names) |>
-          let open XML.Encode in pair int (list (pair string string)) end;
+          let open XML.Encode in pair int (list (pair string (pair string string))) end;
       in YXML.string_of (XML.Elem (markup, body)) end
     else ""
   end;
diff -r 6d123f0ae358 -r ffe88d72afae src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Fri Mar 07 15:52:56 2014 +0000
+++ b/src/Pure/General/completion.scala	Fri Mar 07 20:50:02 2014 +0100
@@ -21,11 +21,10 @@
     range: Text.Range,
     original: String,
     name: String,
-    description: String,
+    description: List[String],
     replacement: String,
     move: Int,
     immediate: Boolean)
-  { override def toString: String = description }
 
   object Result
   {
@@ -136,7 +135,7 @@
               val (total, names) =
               {
                 import XML.Decode._
-                pair(int, list(pair(string, string)))(body)
+                pair(int, list(pair(string, pair(string, string))))(body)
               }
               Some(Names(info.range, total, names))
             }
@@ -148,21 +147,27 @@
     }
   }
 
-  sealed case class Names(range: Text.Range, total: Int, names: List[(String, String)])
+  sealed case class Names(
+    range: Text.Range, total: Int, names: List[(String, (String, String))])
   {
     def no_completion: Boolean = total == 0 && names.isEmpty
 
     def complete(
       history: Completion.History,
-      decode: Boolean,
+      do_decode: Boolean,
       original: String): Option[Completion.Result] =
     {
+      def decode(s: String): String = if (do_decode) Symbol.decode(s) else s
       val items =
         for {
-          (xname, name) <- names
-          xname1 = (if (decode) Symbol.decode(xname) else xname)
+          (xname, (kind, name)) <- names
+          xname1 = decode(xname)
           if xname1 != original
-        } yield Item(range, original, name, xname1, xname1, 0, true)
+          (full_name, descr_name) =
+            if (kind == "") (name, quote(decode(name)))
+            else (kind + "." + name, Library.plain_words(kind) + " " + quote(decode(name)))
+          description = List(xname1, "(" + descr_name + ")")
+        } yield Item(range, original, full_name, description, xname1, 0, true)
 
       if (items.isEmpty) None
       else Some(Result(range, original, names.length == 1, items.sorted(history.ordering)))
@@ -252,24 +257,31 @@
 }
 
 final class Completion private(
-  keywords: Set[String] = Set.empty,
+  keywords: Map[String, Boolean] = Map.empty,
   words_lex: Scan.Lexicon = Scan.Lexicon.empty,
   words_map: Multi_Map[String, String] = Multi_Map.empty,
   abbrevs_lex: Scan.Lexicon = Scan.Lexicon.empty,
   abbrevs_map: Multi_Map[String, (String, String)] = Multi_Map.empty)
 {
-  /* adding stuff */
+  /* keywords */
 
-  def + (keyword: String, replace: String): Completion =
+  private def is_symbol(name: String): Boolean = Symbol.names.isDefinedAt(name)
+  private def is_keyword(name: String): Boolean = !is_symbol(name) && keywords.isDefinedAt(name)
+  private def is_keyword_template(name: String): Boolean = is_keyword(name) && keywords(name)
+
+  def + (keyword: String, template: String): Completion =
     new Completion(
-      keywords + keyword,
+      keywords + (keyword -> (keyword != template)),
       words_lex + keyword,
-      words_map + (keyword -> replace),
+      words_map + (keyword -> template),
       abbrevs_lex,
       abbrevs_map)
 
   def + (keyword: String): Completion = this + (keyword, keyword)
 
+
+  /* symbols with abbreviations */
+
   private def add_symbols(): Completion =
   {
     val words =
@@ -298,7 +310,7 @@
 
   def complete(
     history: Completion.History,
-    decode: Boolean,
+    do_decode: Boolean,
     explicit: Boolean,
     start: Text.Offset,
     text: CharSequence,
@@ -306,6 +318,7 @@
     extend_word: Boolean,
     language_context: Completion.Language_Context): Option[Completion.Result] =
   {
+    def decode(s: String): String = if (do_decode) Symbol.decode(s) else s
     val length = text.length
 
     val abbrevs_result =
@@ -328,7 +341,8 @@
     }
 
     val words_result =
-      abbrevs_result orElse {
+      if (abbrevs_result.isDefined) None
+      else {
         val end =
           if (extend_word) Completion.Word_Parsers.extend_word(text, caret)
           else caret
@@ -344,7 +358,7 @@
             val completions =
               for {
                 s <- words_lex.completions(word)
-                if (if (keywords(s)) language_context.is_outer else language_context.symbols)
+                if (if (is_keyword(s)) language_context.is_outer else language_context.symbols)
                 r <- words_map.get_list(s)
               } yield r
             if (completions.isEmpty) None
@@ -353,26 +367,43 @@
         }
       }
 
-    words_result match {
-      case Some(((word, cs), end)) =>
-        val range = Text.Range(- word.length, 0) + end + start
-        val ds = (if (decode) cs.map(Symbol.decode(_)) else cs).filter(_ != word)
-        if (ds.isEmpty) None
-        else {
-          val immediate =
-            !Completion.Word_Parsers.is_word(word) &&
-            Character.codePointCount(word, 0, word.length) > 1
-          val items =
-            ds.map(s => {
-              val (s1, s2) =
-                space_explode(Completion.caret_indicator, s) match {
-                  case List(s1, s2) => (s1, s2)
-                  case _ => (s, "")
-                }
-              Completion.Item(range, word, s, s, s1 + s2, - s2.length, explicit || immediate)
-            })
-          Some(Completion.Result(range, word, cs.length == 1, items.sorted(history.ordering)))
-        }
+    (abbrevs_result orElse words_result) match {
+      case Some(((original, completions0), end)) =>
+        val completions1 = completions0.map(decode(_))
+
+        val range = Text.Range(- original.length, 0) + end + start
+        val immediate =
+          explicit ||
+            (!Completion.Word_Parsers.is_word(original) &&
+              Character.codePointCount(original, 0, original.length) > 1)
+        val unique = completions0.length == 1
+
+        val items =
+          for {
+            (name0, name1) <- completions0 zip completions1
+            if name1 != original
+            (s1, s2) =
+              space_explode(Completion.caret_indicator, name1) match {
+                case List(s1, s2) => (s1, s2)
+                case _ => (name1, "")
+              }
+            move = - s2.length
+            description =
+              if (is_symbol(name0)) {
+                if (name0 == name1) List(name0)
+                else List(name1, "(symbol " + quote(name0) + ")")
+              }
+              else if (move != 0 || is_keyword_template(name0))
+                List(name1, "(template)")
+              else if (is_keyword(name0))
+                List(name1, "(keyword)")
+              else List(name1)
+          }
+          yield Completion.Item(range, original, name1, description, s1 + s2, move, immediate)
+
+        if (items.isEmpty) None
+        else Some(Completion.Result(range, original, unique, items.sorted(history.ordering)))
+
       case None => None
     }
   }
diff -r 6d123f0ae358 -r ffe88d72afae src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Fri Mar 07 15:52:56 2014 +0000
+++ b/src/Pure/General/name_space.ML	Fri Mar 07 20:50:02 2014 +0100
@@ -208,11 +208,13 @@
   if Position.is_reported pos then
     let
       val x = Name.clean xname;
-      val Name_Space {kind = k, internals, ...} = space;
+      val Name_Space {kind, internals, ...} = space;
       val ext = extern_shortest (Context.proof_of context) space;
       val names =
         Symtab.fold
-          (fn (a, (b :: _, _)) => String.isPrefix x a ? cons (ext b, Long_Name.implode [k, b])
+          (fn (a, (name :: _, _)) =>
+              if String.isPrefix x a andalso not (is_concealed space name)
+              then cons (ext name, (kind, name)) else I
             | _ => I) internals []
         |> sort_distinct (string_ord o pairself #1);
     in Completion.names pos names end
diff -r 6d123f0ae358 -r ffe88d72afae src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Fri Mar 07 15:52:56 2014 +0000
+++ b/src/Pure/General/scan.scala	Fri Mar 07 20:50:02 2014 +0100
@@ -7,6 +7,7 @@
 package isabelle
 
 
+import scala.annotation.tailrec
 import scala.collection.{IndexedSeq, TraversableOnce}
 import scala.collection.immutable.PagedSeq
 import scala.util.parsing.input.{OffsetPosition, Position => InputPosition, Reader}
@@ -323,14 +324,15 @@
     private def lookup(str: CharSequence): Option[(Boolean, Lexicon.Tree)] =
     {
       val len = str.length
-      def look(tree: Lexicon.Tree, tip: Boolean, i: Int): Option[(Boolean, Lexicon.Tree)] =
+      @tailrec def look(tree: Lexicon.Tree, tip: Boolean, i: Int): Option[(Boolean, Lexicon.Tree)] =
       {
         if (i < len) {
           tree.branches.get(str.charAt(i)) match {
             case Some((s, tr)) => look(tr, !s.isEmpty, i + 1)
             case None => None
           }
-        } else Some(tip, tree)
+        }
+        else Some(tip, tree)
       }
       look(rep, false, 0)
     }
diff -r 6d123f0ae358 -r ffe88d72afae src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Fri Mar 07 15:52:56 2014 +0000
+++ b/src/Pure/Syntax/syntax_phases.ML	Fri Mar 07 20:50:02 2014 +0100
@@ -228,6 +228,22 @@
       Proof_Context.check_const ctxt {proper = true, strict = false} (c, ps);
   in (c', reports) end;
 
+local
+
+fun get_free ctxt x =
+  let
+    val fixed = Variable.lookup_fixed ctxt x;
+    val is_const = can (decode_const ctxt) (x, []) orelse Long_Name.is_qualified x;
+    val is_declared = is_some (Variable.def_type ctxt false (x, ~1));
+  in
+    if Variable.is_const ctxt x then NONE
+    else if is_some fixed then fixed
+    else if not is_const orelse is_declared then SOME x
+    else NONE
+  end;
+
+in
+
 fun decode_term _ (result as (_: Position.report_text list, Exn.Exn _)) = result
   | decode_term ctxt (reports0, Exn.Res tm) =
       let
@@ -235,24 +251,6 @@
         fun report ps = Position.store_reports reports ps;
         val append_reports = Position.append_reports reports;
 
-        fun get_free x =
-          let
-            val fixed = Variable.lookup_fixed ctxt x;
-            val is_const = can (decode_const ctxt) (x, []) orelse Long_Name.is_qualified x;
-            val is_declared = is_some (Variable.def_type ctxt false (x, ~1));
-          in
-            if Variable.is_const ctxt x then NONE
-            else if is_some fixed then fixed
-            else if not is_const orelse is_declared then SOME x
-            else NONE
-          end;
-
-        fun the_const (a, ps) =
-          let
-            val (c, rs) = decode_const ctxt (a, ps);
-            val _ = append_reports rs;
-          in c end;
-
         fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) =
               (case Term_Position.decode_position typ of
                 SOME (p, T) => Type.constraint T (decode (p :: ps) qs bs t)
@@ -274,15 +272,20 @@
                   let
                     val c =
                       (case try Lexicon.unmark_const a of
-                        SOME c => (report ps (markup_const ctxt) c; c)
-                      | NONE => the_const (a, ps));
+                        SOME c => c
+                      | NONE => #1 (decode_const ctxt (a, [])));
+                    val _ = report ps (markup_const ctxt) c;
                   in Const (c, T) end)
           | decode ps _ _ (Free (a, T)) =
               ((Name.reject_internal (a, ps) handle ERROR msg =>
                   error (msg ^ Proof_Context.consts_completion_message ctxt (a, ps)));
-                (case get_free a of
+                (case get_free ctxt a of
                   SOME x => (report ps (markup_free ctxt) x; Free (x, T))
-                | NONE => Const (the_const (a, ps), T)))
+                | NONE =>
+                    let
+                      val (c, rs) = decode_const ctxt (a, ps);
+                      val _ = append_reports rs;
+                    in Const (c, T) end))
           | decode ps _ _ (Var (xi, T)) = (report ps markup_var xi; Var (xi, T))
           | decode ps _ bs (t as Bound i) =
               (case try (nth bs) i of
@@ -292,6 +295,8 @@
         val tm' = Exn.interruptible_capture (fn () => decode [] [] [] tm) ();
       in (! reports, tm') end;
 
+end;
+
 
 
 (** parse **)
@@ -332,7 +337,7 @@
       else
         [cat_lines
           (("Ambiguous input" ^ Position.here (Position.reset_range pos) ^
-            "\nproduces " ^ string_of_int len ^ " parse trees" ^
+            " produces " ^ string_of_int len ^ " parse trees" ^
             (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
             map (Pretty.string_of o Pretty.item o single o Parser.pretty_parsetree)
               (take limit pts))];
@@ -412,12 +417,11 @@
             report_result ctxt pos []
               [(reports', Exn.Exn (Exn.EXCEPTIONS (map ERROR ambig_msgs @ errs)))]
           else if checked_len = 1 then
-            (if parsed_len > 1 andalso ambiguity_warning then
+            (if not (null ambig_msgs) andalso ambiguity_warning then
               Context_Position.if_visible ctxt warning
                 (cat_lines (ambig_msgs @
-                  ["Fortunately, only one parse tree is type correct" ^
-                  Position.here (Position.reset_range pos) ^
-                  ",\nbut you may still want to disambiguate your grammar or your input."]))
+                  ["Fortunately, only one parse tree is well-formed and type-correct,\n\
+                   \but you may still want to disambiguate your grammar or your input."]))
              else (); report_result ctxt pos [] results')
           else
             report_result ctxt pos []
diff -r 6d123f0ae358 -r ffe88d72afae src/Pure/library.scala
--- a/src/Pure/library.scala	Fri Mar 07 15:52:56 2014 +0000
+++ b/src/Pure/library.scala	Fri Mar 07 20:50:02 2014 +0100
@@ -97,6 +97,9 @@
     else ""
   }
 
+  def plain_words(str: String): String =
+    space_explode('_', str).mkString(" ")
+
 
   /* strings */
 
diff -r 6d123f0ae358 -r ffe88d72afae src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Fri Mar 07 15:52:56 2014 +0000
+++ b/src/Tools/jEdit/src/completion_popup.scala	Fri Mar 07 20:50:02 2014 +0100
@@ -25,6 +25,22 @@
 
 object Completion_Popup
 {
+  /** items with HTML rendering **/
+
+  private class Item(val item: Completion.Item)
+  {
+    private val html =
+      item.description match {
+        case a :: bs =>
+          "<html><b>" + HTML.encode(a) + "</b>" +
+            HTML.encode(bs.map(" " + _).mkString) + "</html>"
+        case Nil => ""
+      }
+    override def toString: String = html
+  }
+
+
+
   /** jEdit text area **/
 
   object Text_Area
@@ -210,8 +226,10 @@
             SwingUtilities.convertPoint(painter,
               loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered)
 
+          val items = result.items.map(new Item(_))
           val completion =
-            new Completion_Popup(Some((range, invalidate _)), layered, loc2, font, result.items) {
+            new Completion_Popup(Some((range, invalidate _)), layered, loc2, font, items)
+            {
               override def complete(item: Completion.Item) {
                 PIDE.completion_history.update(item)
                 insert(item)
@@ -402,18 +420,19 @@
               val loc =
                 SwingUtilities.convertPoint(text_field, fm.stringWidth(text), fm.getHeight, layered)
 
+              val items = result.items.map(new Item(_))
               val completion =
-                new Completion_Popup(None, layered, loc, text_field.getFont, result.items)
-              {
-                override def complete(item: Completion.Item) {
-                  PIDE.completion_history.update(item)
-                  insert(item)
+                new Completion_Popup(None, layered, loc, text_field.getFont, items)
+                {
+                  override def complete(item: Completion.Item) {
+                    PIDE.completion_history.update(item)
+                    insert(item)
+                  }
+                  override def propagate(evt: KeyEvent) {
+                    if (!evt.isConsumed) text_field.processKeyEvent(evt)
+                  }
+                  override def refocus() { text_field.requestFocus }
                 }
-                override def propagate(evt: KeyEvent) {
-                  if (!evt.isConsumed) text_field.processKeyEvent(evt)
-                }
-                override def refocus() { text_field.requestFocus }
-              }
               completion_popup = Some(completion)
               completion.show_popup()
 
@@ -474,7 +493,7 @@
   layered: JLayeredPane,
   location: Point,
   font: Font,
-  items: List[Completion.Item]) extends JPanel(new BorderLayout)
+  items: List[Completion_Popup.Item]) extends JPanel(new BorderLayout)
 {
   completion =>
 
@@ -508,7 +527,7 @@
   private def complete_selected(): Boolean =
   {
     list_view.selection.items.toList match {
-      case item :: _ => complete(item); true
+      case item :: _ => complete(item.item); true
       case _ => false
     }
   }
diff -r 6d123f0ae358 -r ffe88d72afae src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Fri Mar 07 15:52:56 2014 +0000
+++ b/src/Tools/jEdit/src/rendering.scala	Fri Mar 07 20:50:02 2014 +0100
@@ -459,7 +459,7 @@
           case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) =>
             Some(Text.Info(r, (t1 + t2, info)))
           case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _))) =>
-            val kind1 = space_explode('_', kind).mkString(" ")
+            val kind1 = Library.plain_words(kind)
             val txt1 = kind1 + " " + quote(name)
             val t = prev.info._1
             val txt2 =