merged
authorwenzelm
Fri Mar 07 20:50:02 2014 +0100 (2014-03-07)
changeset 55988ffe88d72afae
parent 55970 6d123f0ae358
parent 55987 52c22561996d
child 55989 55827fc7c0dd
merged
     1.1 --- a/src/HOL/Ctr_Sugar.thy	Fri Mar 07 15:52:56 2014 +0000
     1.2 +++ b/src/HOL/Ctr_Sugar.thy	Fri Mar 07 20:50:02 2014 +0100
     1.3 @@ -27,7 +27,6 @@
     1.4  declare [[coercion_args case_elem - +]]
     1.5  
     1.6  ML_file "Tools/Ctr_Sugar/case_translation.ML"
     1.7 -setup Case_Translation.setup
     1.8  
     1.9  lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y"
    1.10  by (erule iffI) (erule contrapos_pn)
     2.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Fri Mar 07 15:52:56 2014 +0000
     2.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Fri Mar 07 20:50:02 2014 +0100
     2.3 @@ -62,25 +62,25 @@
     2.4  
     2.5  primrec Ifm :: "bool list \<Rightarrow> int list \<Rightarrow> fm \<Rightarrow> bool"  -- {* Semantics of formulae (fm) *}
     2.6  where
     2.7 -  "Ifm bbs bs T = True"
     2.8 -| "Ifm bbs bs F = False"
     2.9 -| "Ifm bbs bs (Lt a) = (Inum bs a < 0)"
    2.10 -| "Ifm bbs bs (Gt a) = (Inum bs a > 0)"
    2.11 -| "Ifm bbs bs (Le a) = (Inum bs a \<le> 0)"
    2.12 -| "Ifm bbs bs (Ge a) = (Inum bs a \<ge> 0)"
    2.13 -| "Ifm bbs bs (Eq a) = (Inum bs a = 0)"
    2.14 -| "Ifm bbs bs (NEq a) = (Inum bs a \<noteq> 0)"
    2.15 -| "Ifm bbs bs (Dvd i b) = (i dvd Inum bs b)"
    2.16 -| "Ifm bbs bs (NDvd i b) = (\<not>(i dvd Inum bs b))"
    2.17 -| "Ifm bbs bs (NOT p) = (\<not> (Ifm bbs bs p))"
    2.18 -| "Ifm bbs bs (And p q) = (Ifm bbs bs p \<and> Ifm bbs bs q)"
    2.19 -| "Ifm bbs bs (Or p q) = (Ifm bbs bs p \<or> Ifm bbs bs q)"
    2.20 -| "Ifm bbs bs (Imp p q) = ((Ifm bbs bs p) \<longrightarrow> (Ifm bbs bs q))"
    2.21 -| "Ifm bbs bs (Iff p q) = (Ifm bbs bs p = Ifm bbs bs q)"
    2.22 -| "Ifm bbs bs (E p) = (\<exists>x. Ifm bbs (x#bs) p)"
    2.23 -| "Ifm bbs bs (A p) = (\<forall>x. Ifm bbs (x#bs) p)"
    2.24 -| "Ifm bbs bs (Closed n) = bbs!n"
    2.25 -| "Ifm bbs bs (NClosed n) = (\<not> bbs!n)"
    2.26 +  "Ifm bbs bs T \<longleftrightarrow> True"
    2.27 +| "Ifm bbs bs F \<longleftrightarrow> False"
    2.28 +| "Ifm bbs bs (Lt a) \<longleftrightarrow> Inum bs a < 0"
    2.29 +| "Ifm bbs bs (Gt a) \<longleftrightarrow> Inum bs a > 0"
    2.30 +| "Ifm bbs bs (Le a) \<longleftrightarrow> Inum bs a \<le> 0"
    2.31 +| "Ifm bbs bs (Ge a) \<longleftrightarrow> Inum bs a \<ge> 0"
    2.32 +| "Ifm bbs bs (Eq a) \<longleftrightarrow> Inum bs a = 0"
    2.33 +| "Ifm bbs bs (NEq a) \<longleftrightarrow> Inum bs a \<noteq> 0"
    2.34 +| "Ifm bbs bs (Dvd i b) \<longleftrightarrow> i dvd Inum bs b"
    2.35 +| "Ifm bbs bs (NDvd i b) \<longleftrightarrow> \<not> i dvd Inum bs b"
    2.36 +| "Ifm bbs bs (NOT p) \<longleftrightarrow> \<not> Ifm bbs bs p"
    2.37 +| "Ifm bbs bs (And p q) \<longleftrightarrow> Ifm bbs bs p \<and> Ifm bbs bs q"
    2.38 +| "Ifm bbs bs (Or p q) \<longleftrightarrow> Ifm bbs bs p \<or> Ifm bbs bs q"
    2.39 +| "Ifm bbs bs (Imp p q) \<longleftrightarrow> (Ifm bbs bs p \<longrightarrow> Ifm bbs bs q)"
    2.40 +| "Ifm bbs bs (Iff p q) \<longleftrightarrow> Ifm bbs bs p = Ifm bbs bs q"
    2.41 +| "Ifm bbs bs (E p) \<longleftrightarrow> (\<exists>x. Ifm bbs (x # bs) p)"
    2.42 +| "Ifm bbs bs (A p) \<longleftrightarrow> (\<forall>x. Ifm bbs (x # bs) p)"
    2.43 +| "Ifm bbs bs (Closed n) \<longleftrightarrow> bbs!n"
    2.44 +| "Ifm bbs bs (NClosed n) \<longleftrightarrow> \<not> bbs!n"
    2.45  
    2.46  consts prep :: "fm \<Rightarrow> fm"
    2.47  recdef prep "measure fmsize"
    2.48 @@ -129,44 +129,44 @@
    2.49  
    2.50  primrec numbound0 :: "num \<Rightarrow> bool"  -- {* a num is INDEPENDENT of Bound 0 *}
    2.51  where
    2.52 -  "numbound0 (C c) = True"
    2.53 -| "numbound0 (Bound n) = (n>0)"
    2.54 -| "numbound0 (CN n i a) = (n >0 \<and> numbound0 a)"
    2.55 -| "numbound0 (Neg a) = numbound0 a"
    2.56 -| "numbound0 (Add a b) = (numbound0 a \<and> numbound0 b)"
    2.57 -| "numbound0 (Sub a b) = (numbound0 a \<and> numbound0 b)"
    2.58 -| "numbound0 (Mul i a) = numbound0 a"
    2.59 +  "numbound0 (C c) \<longleftrightarrow> True"
    2.60 +| "numbound0 (Bound n) \<longleftrightarrow> n > 0"
    2.61 +| "numbound0 (CN n i a) \<longleftrightarrow> n > 0 \<and> numbound0 a"
    2.62 +| "numbound0 (Neg a) \<longleftrightarrow> numbound0 a"
    2.63 +| "numbound0 (Add a b) \<longleftrightarrow> numbound0 a \<and> numbound0 b"
    2.64 +| "numbound0 (Sub a b) \<longleftrightarrow> numbound0 a \<and> numbound0 b"
    2.65 +| "numbound0 (Mul i a) \<longleftrightarrow> numbound0 a"
    2.66  
    2.67  lemma numbound0_I:
    2.68    assumes nb: "numbound0 a"
    2.69 -  shows "Inum (b#bs) a = Inum (b'#bs) a"
    2.70 +  shows "Inum (b # bs) a = Inum (b' # bs) a"
    2.71    using nb by (induct a rule: num.induct) (auto simp add: gr0_conv_Suc)
    2.72  
    2.73  primrec bound0 :: "fm \<Rightarrow> bool" -- {* A Formula is independent of Bound 0 *}
    2.74  where
    2.75 -  "bound0 T = True"
    2.76 -| "bound0 F = True"
    2.77 -| "bound0 (Lt a) = numbound0 a"
    2.78 -| "bound0 (Le a) = numbound0 a"
    2.79 -| "bound0 (Gt a) = numbound0 a"
    2.80 -| "bound0 (Ge a) = numbound0 a"
    2.81 -| "bound0 (Eq a) = numbound0 a"
    2.82 -| "bound0 (NEq a) = numbound0 a"
    2.83 -| "bound0 (Dvd i a) = numbound0 a"
    2.84 -| "bound0 (NDvd i a) = numbound0 a"
    2.85 -| "bound0 (NOT p) = bound0 p"
    2.86 -| "bound0 (And p q) = (bound0 p \<and> bound0 q)"
    2.87 -| "bound0 (Or p q) = (bound0 p \<and> bound0 q)"
    2.88 -| "bound0 (Imp p q) = ((bound0 p) \<and> (bound0 q))"
    2.89 -| "bound0 (Iff p q) = (bound0 p \<and> bound0 q)"
    2.90 -| "bound0 (E p) = False"
    2.91 -| "bound0 (A p) = False"
    2.92 -| "bound0 (Closed P) = True"
    2.93 -| "bound0 (NClosed P) = True"
    2.94 +  "bound0 T \<longleftrightarrow> True"
    2.95 +| "bound0 F \<longleftrightarrow> True"
    2.96 +| "bound0 (Lt a) \<longleftrightarrow> numbound0 a"
    2.97 +| "bound0 (Le a) \<longleftrightarrow> numbound0 a"
    2.98 +| "bound0 (Gt a) \<longleftrightarrow> numbound0 a"
    2.99 +| "bound0 (Ge a) \<longleftrightarrow> numbound0 a"
   2.100 +| "bound0 (Eq a) \<longleftrightarrow> numbound0 a"
   2.101 +| "bound0 (NEq a) \<longleftrightarrow> numbound0 a"
   2.102 +| "bound0 (Dvd i a) \<longleftrightarrow> numbound0 a"
   2.103 +| "bound0 (NDvd i a) \<longleftrightarrow> numbound0 a"
   2.104 +| "bound0 (NOT p) \<longleftrightarrow> bound0 p"
   2.105 +| "bound0 (And p q) \<longleftrightarrow> bound0 p \<and> bound0 q"
   2.106 +| "bound0 (Or p q) \<longleftrightarrow> bound0 p \<and> bound0 q"
   2.107 +| "bound0 (Imp p q) \<longleftrightarrow> bound0 p \<and> bound0 q"
   2.108 +| "bound0 (Iff p q) \<longleftrightarrow> bound0 p \<and> bound0 q"
   2.109 +| "bound0 (E p) \<longleftrightarrow> False"
   2.110 +| "bound0 (A p) \<longleftrightarrow> False"
   2.111 +| "bound0 (Closed P) \<longleftrightarrow> True"
   2.112 +| "bound0 (NClosed P) \<longleftrightarrow> True"
   2.113  
   2.114  lemma bound0_I:
   2.115    assumes bp: "bound0 p"
   2.116 -  shows "Ifm bbs (b#bs) p = Ifm bbs (b'#bs) p"
   2.117 +  shows "Ifm bbs (b # bs) p = Ifm bbs (b' # bs) p"
   2.118    using bp numbound0_I[where b="b" and bs="bs" and b'="b'"]
   2.119    by (induct p rule: fm.induct) (auto simp add: gr0_conv_Suc)
   2.120  
   2.121 @@ -256,19 +256,19 @@
   2.122  
   2.123  fun isatom :: "fm \<Rightarrow> bool"  -- {* test for atomicity *}
   2.124  where
   2.125 -  "isatom T = True"
   2.126 -| "isatom F = True"
   2.127 -| "isatom (Lt a) = True"
   2.128 -| "isatom (Le a) = True"
   2.129 -| "isatom (Gt a) = True"
   2.130 -| "isatom (Ge a) = True"
   2.131 -| "isatom (Eq a) = True"
   2.132 -| "isatom (NEq a) = True"
   2.133 -| "isatom (Dvd i b) = True"
   2.134 -| "isatom (NDvd i b) = True"
   2.135 -| "isatom (Closed P) = True"
   2.136 -| "isatom (NClosed P) = True"
   2.137 -| "isatom p = False"
   2.138 +  "isatom T \<longleftrightarrow> True"
   2.139 +| "isatom F \<longleftrightarrow> True"
   2.140 +| "isatom (Lt a) \<longleftrightarrow> True"
   2.141 +| "isatom (Le a) \<longleftrightarrow> True"
   2.142 +| "isatom (Gt a) \<longleftrightarrow> True"
   2.143 +| "isatom (Ge a) \<longleftrightarrow> True"
   2.144 +| "isatom (Eq a) \<longleftrightarrow> True"
   2.145 +| "isatom (NEq a) \<longleftrightarrow> True"
   2.146 +| "isatom (Dvd i b) \<longleftrightarrow> True"
   2.147 +| "isatom (NDvd i b) \<longleftrightarrow> True"
   2.148 +| "isatom (Closed P) \<longleftrightarrow> True"
   2.149 +| "isatom (NClosed P) \<longleftrightarrow> True"
   2.150 +| "isatom p \<longleftrightarrow> False"
   2.151  
   2.152  lemma numsubst0_numbound0:
   2.153    assumes "numbound0 t"
   2.154 @@ -423,10 +423,10 @@
   2.155  
   2.156  consts numadd:: "num \<times> num \<Rightarrow> num"
   2.157  recdef numadd "measure (\<lambda>(t, s). num_size t + num_size s)"
   2.158 -  "numadd (CN n1 c1 r1 ,CN n2 c2 r2) =
   2.159 +  "numadd (CN n1 c1 r1, CN n2 c2 r2) =
   2.160      (if n1 = n2 then
   2.161 -      (let c = c1 + c2
   2.162 -       in if c = 0 then numadd (r1, r2) else CN n1 c (numadd (r1, r2)))
   2.163 +       let c = c1 + c2
   2.164 +       in if c = 0 then numadd (r1, r2) else CN n1 c (numadd (r1, r2))
   2.165       else if n1 \<le> n2 then CN n1 c1 (numadd (r1, Add (Mul c2 (Bound n2)) r2))
   2.166       else CN n2 c2 (numadd (Add (Mul c1 (Bound n1)) r1, r2)))"
   2.167    "numadd (CN n1 c1 r1, t) = CN n1 c1 (numadd (r1, t))"
   2.168 @@ -1108,8 +1108,8 @@
   2.169  
   2.170  lemma zlfm_I:
   2.171    assumes qfp: "qfree p"
   2.172 -  shows "(Ifm bbs (i # bs) (zlfm p) = Ifm bbs (i # bs) p) \<and> iszlfm (zlfm p)"
   2.173 -  (is "(?I (?l p) = ?I p) \<and> ?L (?l p)")
   2.174 +  shows "Ifm bbs (i # bs) (zlfm p) = Ifm bbs (i # bs) p \<and> iszlfm (zlfm p)"
   2.175 +  (is "?I (?l p) = ?I p \<and> ?L (?l p)")
   2.176    using qfp
   2.177  proof (induct p rule: zlfm.induct)
   2.178    case (5 a)
   2.179 @@ -2204,20 +2204,20 @@
   2.180      \<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)))"
   2.181    apply(rule iffI)
   2.182    prefer 2
   2.183 -  apply(drule minusinfinity)
   2.184 +  apply (drule minusinfinity)
   2.185    apply assumption+
   2.186 -  apply(fastforce)
   2.187 +  apply fastforce
   2.188    apply clarsimp
   2.189 -  apply(subgoal_tac "!!k. 0<=k \<Longrightarrow> !x. P x \<longrightarrow> P (x - k*D)")
   2.190 -  apply(frule_tac x = x and z=z in decr_lemma)
   2.191 -  apply(subgoal_tac "P1(x - (\<bar>x - z\<bar> + 1) * D)")
   2.192 +  apply (subgoal_tac "\<And>k. 0 \<le> k \<Longrightarrow> \<forall>x. P x \<longrightarrow> P (x - k * D)")
   2.193 +  apply (frule_tac x = x and z=z in decr_lemma)
   2.194 +  apply (subgoal_tac "P1 (x - (\<bar>x - z\<bar> + 1) * D)")
   2.195    prefer 2
   2.196 -  apply(subgoal_tac "0 <= (\<bar>x - z\<bar> + 1)")
   2.197 +  apply (subgoal_tac "0 \<le> \<bar>x - z\<bar> + 1")
   2.198    prefer 2 apply arith
   2.199     apply fastforce
   2.200 -  apply(drule (1)  periodic_finite_ex)
   2.201 +  apply (drule (1)  periodic_finite_ex)
   2.202    apply blast
   2.203 -  apply(blast dest:decr_mult_lemma)
   2.204 +  apply (blast dest: decr_mult_lemma)
   2.205    done
   2.206  
   2.207  theorem cp_thm:
   2.208 @@ -2297,7 +2297,7 @@
   2.209  proof -
   2.210    fix q B d
   2.211    assume qBd: "unit p = (q,B,d)"
   2.212 -  let ?thes = "((\<exists>x. Ifm bbs (x#bs) p) = (\<exists>x. Ifm bbs (x#bs) q)) \<and>
   2.213 +  let ?thes = "((\<exists>x. Ifm bbs (x#bs) p) \<longleftrightarrow> (\<exists>x. Ifm bbs (x#bs) q)) \<and>
   2.214      Inum (i#bs) ` set B = Inum (i#bs) ` set (\<beta> q) \<and>
   2.215      d_\<beta> q 1 \<and> d_\<delta> q d \<and> 0 < d \<and> iszlfm q \<and> (\<forall>b\<in> set B. numbound0 b)"
   2.216    let ?I = "\<lambda>x p. Ifm bbs (x#bs) p"
   2.217 @@ -2319,34 +2319,47 @@
   2.218    from lp' lp a_\<beta>[OF lp' dl lp] have lq:"iszlfm ?q" and uq: "d_\<beta> ?q 1"  by auto
   2.219    from \<delta>[OF lq] have dp:"?d >0" and dd: "d_\<delta> ?q ?d" by blast+
   2.220    let ?N = "\<lambda>t. Inum (i#bs) t"
   2.221 -  have "?N ` set ?B' = ((?N o simpnum) ` ?B)" by auto
   2.222 -  also have "\<dots> = ?N ` ?B" using simpnum_ci[where bs="i#bs"] by auto
   2.223 +  have "?N ` set ?B' = ((?N \<circ> simpnum) ` ?B)"
   2.224 +    by auto
   2.225 +  also have "\<dots> = ?N ` ?B"
   2.226 +    using simpnum_ci[where bs="i#bs"] by auto
   2.227    finally have BB': "?N ` set ?B' = ?N ` ?B" .
   2.228 -  have "?N ` set ?A' = ((?N o simpnum) ` ?A)" by auto
   2.229 -  also have "\<dots> = ?N ` ?A" using simpnum_ci[where bs="i#bs"] by auto
   2.230 +  have "?N ` set ?A' = ((?N \<circ> simpnum) ` ?A)"
   2.231 +    by auto
   2.232 +  also have "\<dots> = ?N ` ?A"
   2.233 +    using simpnum_ci[where bs="i#bs"] by auto
   2.234    finally have AA': "?N ` set ?A' = ?N ` ?A" .
   2.235    from \<beta>_numbound0[OF lq] have B_nb:"\<forall>b\<in> set ?B'. numbound0 b"
   2.236      by (simp add: simpnum_numbound0)
   2.237    from \<alpha>_l[OF lq] have A_nb: "\<forall>b\<in> set ?A'. numbound0 b"
   2.238      by (simp add: simpnum_numbound0)
   2.239 -    {assume "length ?B' \<le> length ?A'"
   2.240 -    then have q:"q=?q" and "B = ?B'" and d:"d = ?d"
   2.241 +  {
   2.242 +    assume "length ?B' \<le> length ?A'"
   2.243 +    then have q: "q = ?q" and "B = ?B'" and d: "d = ?d"
   2.244        using qBd by (auto simp add: Let_def unit_def)
   2.245 -    with BB' B_nb have b: "?N ` (set B) = ?N ` set (\<beta> q)"
   2.246 -      and bn: "\<forall>b\<in> set B. numbound0 b" by simp_all
   2.247 -  with pq_ex dp uq dd lq q d have ?thes by simp}
   2.248 +    with BB' B_nb
   2.249 +    have b: "?N ` (set B) = ?N ` set (\<beta> q)" and bn: "\<forall>b\<in> set B. numbound0 b"
   2.250 +      by simp_all
   2.251 +    with pq_ex dp uq dd lq q d have ?thes
   2.252 +      by simp
   2.253 +  }
   2.254    moreover
   2.255 -  {assume "\<not> (length ?B' \<le> length ?A')"
   2.256 +  {
   2.257 +    assume "\<not> (length ?B' \<le> length ?A')"
   2.258      then have q:"q=mirror ?q" and "B = ?A'" and d:"d = ?d"
   2.259        using qBd by (auto simp add: Let_def unit_def)
   2.260      with AA' mirror_\<alpha>_\<beta>[OF lq] A_nb have b:"?N ` (set B) = ?N ` set (\<beta> q)"
   2.261        and bn: "\<forall>b\<in> set B. numbound0 b" by simp_all
   2.262      from mirror_ex[OF lq] pq_ex q
   2.263 -    have pqm_eq:"(\<exists>(x::int). ?I x p) = (\<exists>(x::int). ?I x q)" by simp
   2.264 +    have pqm_eq:"(\<exists>(x::int). ?I x p) = (\<exists>(x::int). ?I x q)"
   2.265 +      by simp
   2.266      from lq uq q mirror_l[where p="?q"]
   2.267 -    have lq': "iszlfm q" and uq: "d_\<beta> q 1" by auto
   2.268 -    from \<delta>[OF lq'] mirror_\<delta>[OF lq] q d have dq:"d_\<delta> q d " by auto
   2.269 -    from pqm_eq b bn uq lq' dp dq q dp d have ?thes by simp
   2.270 +    have lq': "iszlfm q" and uq: "d_\<beta> q 1"
   2.271 +      by auto
   2.272 +    from \<delta>[OF lq'] mirror_\<delta>[OF lq] q d have dq: "d_\<delta> q d"
   2.273 +      by auto
   2.274 +    from pqm_eq b bn uq lq' dp dq q dp d have ?thes
   2.275 +      by simp
   2.276    }
   2.277    ultimately show ?thes by blast
   2.278  qed
   2.279 @@ -2354,7 +2367,8 @@
   2.280  
   2.281  text {* Cooper's Algorithm *}
   2.282  
   2.283 -definition cooper :: "fm \<Rightarrow> fm" where
   2.284 +definition cooper :: "fm \<Rightarrow> fm"
   2.285 +where
   2.286    "cooper p =
   2.287      (let
   2.288        (q, B, d) = unit p;
   2.289 @@ -2386,60 +2400,67 @@
   2.290    let ?Bjs = "[(b,j). b\<leftarrow>?B,j\<leftarrow>?js]"
   2.291    let ?qd = "evaldjf (\<lambda>(b,j). simpfm (subst0 (Add b (C j)) ?q)) ?Bjs"
   2.292    have qbf:"unit p = (?q,?B,?d)" by simp
   2.293 -  from unit[OF qf qbf] have pq_ex: "(\<exists>(x::int). ?I x p) = (\<exists>(x::int). ?I x ?q)" and
   2.294 -    B:"?N ` set ?B = ?N ` set (\<beta> ?q)" and
   2.295 -    uq:"d_\<beta> ?q 1" and dd: "d_\<delta> ?q ?d" and dp: "?d > 0" and
   2.296 -    lq: "iszlfm ?q" and
   2.297 -    Bn: "\<forall>b\<in> set ?B. numbound0 b" by auto
   2.298 +  from unit[OF qf qbf]
   2.299 +  have pq_ex: "(\<exists>(x::int). ?I x p) \<longleftrightarrow> (\<exists>(x::int). ?I x ?q)"
   2.300 +    and B: "?N ` set ?B = ?N ` set (\<beta> ?q)"
   2.301 +    and uq: "d_\<beta> ?q 1"
   2.302 +    and dd: "d_\<delta> ?q ?d"
   2.303 +    and dp: "?d > 0"
   2.304 +    and lq: "iszlfm ?q"
   2.305 +    and Bn: "\<forall>b\<in> set ?B. numbound0 b"
   2.306 +    by auto
   2.307    from zlin_qfree[OF lq] have qfq: "qfree ?q" .
   2.308    from simpfm_qf[OF minusinf_qfree[OF qfq]] have qfmq: "qfree ?smq" .
   2.309 -  have jsnb: "\<forall>j \<in> set ?js. numbound0 (C j)" by simp
   2.310 +  have jsnb: "\<forall>j \<in> set ?js. numbound0 (C j)"
   2.311 +    by simp
   2.312    then have "\<forall>j\<in> set ?js. bound0 (subst0 (C j) ?smq)"
   2.313      by (auto simp only: subst0_bound0[OF qfmq])
   2.314    then have th: "\<forall>j\<in> set ?js. bound0 (simpfm (subst0 (C j) ?smq))"
   2.315      by (auto simp add: simpfm_bound0)
   2.316 -  from evaldjf_bound0[OF th] have mdb: "bound0 ?md" by simp
   2.317 +  from evaldjf_bound0[OF th] have mdb: "bound0 ?md"
   2.318 +    by simp
   2.319    from Bn jsnb have "\<forall>(b,j) \<in> set ?Bjs. numbound0 (Add b (C j))"
   2.320      by simp
   2.321    then have "\<forall>(b,j) \<in> set ?Bjs. bound0 (subst0 (Add b (C j)) ?q)"
   2.322      using subst0_bound0[OF qfq] by blast
   2.323    then have "\<forall>(b,j) \<in> set ?Bjs. bound0 (simpfm (subst0 (Add b (C j)) ?q))"
   2.324 -    using simpfm_bound0  by blast
   2.325 +    using simpfm_bound0 by blast
   2.326    then have th': "\<forall>x \<in> set ?Bjs. bound0 ((\<lambda>(b,j). simpfm (subst0 (Add b (C j)) ?q)) x)"
   2.327      by auto
   2.328 -  from evaldjf_bound0 [OF th'] have qdb: "bound0 ?qd" by simp
   2.329 -  from mdb qdb
   2.330 -  have mdqdb: "bound0 (disj ?md ?qd)"
   2.331 -    unfolding disj_def by (cases "?md=T \<or> ?qd=T") simp_all
   2.332 +  from evaldjf_bound0 [OF th'] have qdb: "bound0 ?qd"
   2.333 +    by simp
   2.334 +  from mdb qdb have mdqdb: "bound0 (disj ?md ?qd)"
   2.335 +    unfolding disj_def by (cases "?md = T \<or> ?qd = T") simp_all
   2.336    from trans [OF pq_ex cp_thm'[OF lq uq dd dp,where i="i"]] B
   2.337 -  have "?lhs = (\<exists>j\<in> {1.. ?d}. ?I j ?mq \<or> (\<exists>b\<in> ?N ` set ?B. Ifm bbs ((b+ j)#bs) ?q))"
   2.338 +  have "?lhs \<longleftrightarrow> (\<exists>j \<in> {1.. ?d}. ?I j ?mq \<or> (\<exists>b \<in> ?N ` set ?B. Ifm bbs ((b + j) # bs) ?q))"
   2.339      by auto
   2.340 -  also have "\<dots> = (\<exists>j\<in> {1.. ?d}. ?I j ?mq \<or> (\<exists>b\<in> set ?B. Ifm bbs ((?N b+ j)#bs) ?q))"
   2.341 +  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))"
   2.342      by simp
   2.343 -  also have "\<dots> = ((\<exists>j\<in> {1.. ?d}. ?I j ?mq ) \<or>
   2.344 -      (\<exists>j\<in> {1.. ?d}. \<exists>b\<in> set ?B. Ifm bbs ((?N (Add b (C j)))#bs) ?q))"
   2.345 +  also have "\<dots> \<longleftrightarrow> (\<exists>j \<in> {1.. ?d}. ?I j ?mq ) \<or>
   2.346 +      (\<exists>j\<in> {1.. ?d}. \<exists>b \<in> set ?B. Ifm bbs ((?N (Add b (C j))) # bs) ?q)"
   2.347      by (simp only: Inum.simps) blast
   2.348 -  also have "\<dots> = ((\<exists>j\<in> {1.. ?d}. ?I j ?smq ) \<or>
   2.349 -      (\<exists>j\<in> {1.. ?d}. \<exists>b\<in> set ?B. Ifm bbs ((?N (Add b (C j)))#bs) ?q))"
   2.350 +  also have "\<dots> \<longleftrightarrow> (\<exists>j \<in> {1.. ?d}. ?I j ?smq) \<or>
   2.351 +      (\<exists>j \<in> {1.. ?d}. \<exists>b \<in> set ?B. Ifm bbs ((?N (Add b (C j))) # bs) ?q)"
   2.352      by (simp add: simpfm)
   2.353 -  also have "\<dots> = ((\<exists>j\<in> set ?js. (\<lambda>j. ?I i (simpfm (subst0 (C j) ?smq))) j) \<or>
   2.354 -      (\<exists>j\<in> set ?js. \<exists>b\<in> set ?B. Ifm bbs ((?N (Add b (C j)))#bs) ?q))"
   2.355 +  also have "\<dots> \<longleftrightarrow> (\<exists>j\<in> set ?js. (\<lambda>j. ?I i (simpfm (subst0 (C j) ?smq))) j) \<or>
   2.356 +      (\<exists>j\<in> set ?js. \<exists>b\<in> set ?B. Ifm bbs ((?N (Add b (C j)))#bs) ?q)"
   2.357      by (simp only: simpfm subst0_I[OF qfmq] set_upto) auto
   2.358 -  also have "\<dots> = (?I i (evaldjf (\<lambda>j. simpfm (subst0 (C j) ?smq)) ?js) \<or>
   2.359 -      (\<exists>j\<in> set ?js. \<exists>b\<in> set ?B. ?I i (subst0 (Add b (C j)) ?q)))"
   2.360 +  also have "\<dots> \<longleftrightarrow> ?I i (evaldjf (\<lambda>j. simpfm (subst0 (C j) ?smq)) ?js) \<or>
   2.361 +      (\<exists>j\<in> set ?js. \<exists>b\<in> set ?B. ?I i (subst0 (Add b (C j)) ?q))"
   2.362      by (simp only: evaldjf_ex subst0_I[OF qfq])
   2.363 -  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)))"
   2.364 +  also have "\<dots> \<longleftrightarrow> ?I i ?md \<or>
   2.365 +      (\<exists>(b,j) \<in> set ?Bjs. (\<lambda>(b,j). ?I i (simpfm (subst0 (Add b (C j)) ?q))) (b,j))"
   2.366      by (simp only: simpfm set_concat set_map concat_map_singleton UN_simps) blast
   2.367 -  also have "\<dots> = (?I i ?md \<or> (?I i (evaldjf (\<lambda>(b,j). simpfm (subst0 (Add b (C j)) ?q)) ?Bjs)))"
   2.368 +  also have "\<dots> \<longleftrightarrow> ?I i ?md \<or> ?I i (evaldjf (\<lambda>(b,j). simpfm (subst0 (Add b (C j)) ?q)) ?Bjs)"
   2.369      by (simp only: evaldjf_ex[where bs="i#bs" and f="\<lambda>(b,j). simpfm (subst0 (Add b (C j)) ?q)" and ps="?Bjs"])
   2.370        (auto simp add: split_def)
   2.371 -  finally have mdqd: "?lhs = (?I i ?md \<or> ?I i ?qd)"
   2.372 +  finally have mdqd: "?lhs \<longleftrightarrow> ?I i ?md \<or> ?I i ?qd"
   2.373      by simp
   2.374 -  also have "\<dots> = (?I i (disj ?md ?qd))"
   2.375 +  also have "\<dots> \<longleftrightarrow> ?I i (disj ?md ?qd)"
   2.376      by (simp add: disj)
   2.377 -  also have "\<dots> = (Ifm bbs bs (decr (disj ?md ?qd)))"
   2.378 +  also have "\<dots> \<longleftrightarrow> Ifm bbs bs (decr (disj ?md ?qd))"
   2.379      by (simp only: decr [OF mdqdb])
   2.380 -  finally have mdqd2: "?lhs = (Ifm bbs bs (decr (disj ?md ?qd)))" .
   2.381 +  finally have mdqd2: "?lhs \<longleftrightarrow> Ifm bbs bs (decr (disj ?md ?qd))" .
   2.382    {
   2.383      assume mdT: "?md = T"
   2.384      then have cT: "cooper p = T"
   2.385 @@ -2448,7 +2469,8 @@
   2.386        using mdqd by simp
   2.387      from mdT have "?rhs"
   2.388        by (simp add: cooper_def unit_def split_def)
   2.389 -    with lhs cT have ?thesis by simp
   2.390 +    with lhs cT have ?thesis
   2.391 +      by simp
   2.392    }
   2.393    moreover
   2.394    {
     3.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Fri Mar 07 15:52:56 2014 +0000
     3.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Fri Mar 07 20:50:02 2014 +0100
     3.3 @@ -12,22 +12,6 @@
     3.4  
     3.5  val cooper_ss = simpset_of @{context};
     3.6  
     3.7 -val nT = HOLogic.natT;
     3.8 -val comp_arith = @{thms simp_thms}
     3.9 -
    3.10 -val zdvd_int = @{thm zdvd_int};
    3.11 -val zdiff_int_split = @{thm zdiff_int_split};
    3.12 -val split_zdiv = @{thm split_zdiv};
    3.13 -val split_zmod = @{thm split_zmod};
    3.14 -val mod_div_equality' = @{thm mod_div_equality'};
    3.15 -val split_div' = @{thm split_div'};
    3.16 -val Suc_eq_plus1 = @{thm Suc_eq_plus1};
    3.17 -val mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
    3.18 -val mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
    3.19 -val mod_add_eq = @{thm mod_add_eq} RS sym;
    3.20 -val nat_div_add_eq = @{thm div_add1_eq} RS sym;
    3.21 -val int_div_add_eq = @{thm zdiv_zadd1_eq} RS sym;
    3.22 -
    3.23  fun prepare_for_linz q fm =
    3.24    let
    3.25      val ps = Logic.strip_params fm
    3.26 @@ -42,53 +26,51 @@
    3.27      val np = length ps
    3.28      val (fm',np) = List.foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
    3.29        (List.foldr HOLogic.mk_imp c rhs, np) ps
    3.30 -    val (vs, _) = List.partition (fn t => q orelse (type_of t) = nT)
    3.31 +    val (vs, _) = List.partition (fn t => q orelse (type_of t) = @{typ nat})
    3.32        (Misc_Legacy.term_frees fm' @ Misc_Legacy.term_vars fm');
    3.33      val fm2 = List.foldr mk_all2 fm' vs
    3.34    in (fm2, np + length vs, length rhs) end;
    3.35  
    3.36  (*Object quantifier to meta --*)
    3.37 -fun spec_step n th = if (n=0) then th else (spec_step (n-1) th) RS spec ;
    3.38 +fun spec_step n th = if n = 0 then th else (spec_step (n - 1) th) RS spec;
    3.39  
    3.40  (* object implication to meta---*)
    3.41 -fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp;
    3.42 +fun mp_step n th = if n = 0 then th else (mp_step (n - 1) th) RS mp;
    3.43  
    3.44  
    3.45  fun linz_tac ctxt q = Object_Logic.atomize_prems_tac ctxt THEN' SUBGOAL (fn (g, i) =>
    3.46    let
    3.47 -    val thy = Proof_Context.theory_of ctxt
    3.48 +    val thy = Proof_Context.theory_of ctxt;
    3.49      (* Transform the term*)
    3.50 -    val (t,np,nh) = prepare_for_linz q g
    3.51 +    val (t, np, nh) = prepare_for_linz q g;
    3.52      (* Some simpsets for dealing with mod div abs and nat*)
    3.53      val mod_div_simpset =
    3.54        put_simpset HOL_basic_ss ctxt
    3.55 -      addsimps [refl,mod_add_eq, mod_add_left_eq,
    3.56 -          mod_add_right_eq,
    3.57 -          nat_div_add_eq, int_div_add_eq,
    3.58 -          @{thm mod_self},
    3.59 -          @{thm div_by_0}, @{thm mod_by_0}, @{thm div_0}, @{thm mod_0},
    3.60 -          @{thm div_by_1}, @{thm mod_by_1}, @{thm div_1}, @{thm mod_1},
    3.61 -          Suc_eq_plus1]
    3.62 +      addsimps @{thms refl mod_add_eq [symmetric] mod_add_left_eq [symmetric]
    3.63 +          mod_add_right_eq [symmetric]
    3.64 +          div_add1_eq [symmetric] zdiv_zadd1_eq [symmetric]
    3.65 +          mod_self
    3.66 +          div_by_0 mod_by_0 div_0 mod_0
    3.67 +          div_by_1 mod_by_1 div_1 mod_1
    3.68 +          Suc_eq_plus1}
    3.69        addsimps @{thms add_ac}
    3.70        addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}]
    3.71      val simpset0 =
    3.72        put_simpset HOL_basic_ss ctxt
    3.73 -      addsimps [mod_div_equality', Suc_eq_plus1]
    3.74 -      addsimps comp_arith
    3.75 -      |> fold Splitter.add_split
    3.76 -          [split_zdiv, split_zmod, split_div', @{thm "split_min"}, @{thm "split_max"}]
    3.77 +      addsimps @{thms mod_div_equality' Suc_eq_plus1 simp_thms}
    3.78 +      |> fold Splitter.add_split @{thms split_zdiv split_zmod split_div' split_min split_max}
    3.79      (* Simp rules for changing (n::int) to int n *)
    3.80      val simpset1 =
    3.81        put_simpset HOL_basic_ss ctxt
    3.82 -      addsimps [zdvd_int] @ map (fn r => r RS sym)
    3.83 -        [@{thm int_numeral}, @{thm int_int_eq}, @{thm zle_int}, @{thm zless_int}, @{thm zadd_int}, @{thm zmult_int}]
    3.84 -      |> Splitter.add_split zdiff_int_split
    3.85 +      addsimps @{thms zdvd_int} @
    3.86 +        map (fn r => r RS sym) @{thms int_numeral int_int_eq zle_int zless_int zadd_int zmult_int}
    3.87 +      |> Splitter.add_split @{thm zdiff_int_split}
    3.88      (*simp rules for elimination of int n*)
    3.89  
    3.90      val simpset2 =
    3.91        put_simpset HOL_basic_ss ctxt
    3.92        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}]
    3.93 -      |> fold Simplifier.add_cong [@{thm conj_le_cong}, @{thm imp_le_cong}]
    3.94 +      |> fold Simplifier.add_cong @{thms conj_le_cong imp_le_cong}
    3.95      (* simp rules for elimination of abs *)
    3.96      val simpset3 = put_simpset HOL_basic_ss ctxt |> Splitter.add_split @{thm abs_split}
    3.97      val ct = cterm_of thy (HOLogic.mk_Trueprop t)
    3.98 @@ -100,14 +82,16 @@
    3.99        (Thm.trivial ct))
   3.100      fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
   3.101      (* The result of the quantifier elimination *)
   3.102 -    val (th, tac) = case (prop_of pre_thm) of
   3.103 +    val (th, tac) =
   3.104 +      (case (prop_of pre_thm) of
   3.105          Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
   3.106 -    let val pth = linzqe_oracle (cterm_of thy (Envir.eta_long [] t1))
   3.107 -    in
   3.108 -          ((pth RS iffD2) RS pre_thm,
   3.109 -            assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))
   3.110 -    end
   3.111 -      | _ => (pre_thm, assm_tac i)
   3.112 -  in rtac (((mp_step nh) o (spec_step np)) th) i THEN tac end);
   3.113 +          let
   3.114 +            val pth = linzqe_oracle (cterm_of thy (Envir.eta_long [] t1))
   3.115 +          in
   3.116 +            ((pth RS iffD2) RS pre_thm,
   3.117 +              assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))
   3.118 +          end
   3.119 +      | _ => (pre_thm, assm_tac i))
   3.120 +  in rtac (mp_step nh (spec_step np th)) i THEN tac end);
   3.121  
   3.122  end
     4.1 --- a/src/HOL/Num.thy	Fri Mar 07 15:52:56 2014 +0000
     4.2 +++ b/src/HOL/Num.thy	Fri Mar 07 20:50:02 2014 +0100
     4.3 @@ -285,14 +285,14 @@
     4.4      fun num_of_int n =
     4.5        if n > 0 then
     4.6          (case IntInf.quotRem (n, 2) of
     4.7 -          (0, 1) => Syntax.const @{const_name One}
     4.8 -        | (n, 0) => Syntax.const @{const_name Bit0} $ num_of_int n
     4.9 -        | (n, 1) => Syntax.const @{const_name Bit1} $ num_of_int n)
    4.10 +          (0, 1) => Syntax.const @{const_syntax One}
    4.11 +        | (n, 0) => Syntax.const @{const_syntax Bit0} $ num_of_int n
    4.12 +        | (n, 1) => Syntax.const @{const_syntax Bit1} $ num_of_int n)
    4.13        else raise Match
    4.14 -    val numeral = Syntax.const @{const_name numeral}
    4.15 -    val uminus = Syntax.const @{const_name uminus}
    4.16 -    val one = Syntax.const @{const_name Groups.one}
    4.17 -    val zero = Syntax.const @{const_name Groups.zero}
    4.18 +    val numeral = Syntax.const @{const_syntax numeral}
    4.19 +    val uminus = Syntax.const @{const_syntax uminus}
    4.20 +    val one = Syntax.const @{const_syntax Groups.one}
    4.21 +    val zero = Syntax.const @{const_syntax Groups.zero}
    4.22      fun numeral_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
    4.23            c $ numeral_tr [t] $ u
    4.24        | numeral_tr [Const (num, _)] =
    4.25 @@ -303,10 +303,10 @@
    4.26              if value > 0
    4.27              then numeral $ num_of_int value
    4.28              else if value = ~1 then uminus $ one
    4.29 -            else uminus $ (numeral $ num_of_int (~value))
    4.30 +            else uminus $ (numeral $ num_of_int (~ value))
    4.31            end
    4.32        | numeral_tr ts = raise TERM ("numeral_tr", ts);
    4.33 -  in [("_Numeral", K numeral_tr)] end
    4.34 +  in [(@{syntax_const "_Numeral"}, K numeral_tr)] end
    4.35  *}
    4.36  
    4.37  typed_print_translation {*
     5.1 --- a/src/HOL/ROOT	Fri Mar 07 15:52:56 2014 +0000
     5.2 +++ b/src/HOL/ROOT	Fri Mar 07 20:50:02 2014 +0100
     5.3 @@ -213,7 +213,6 @@
     5.4      Verification of imperative programs (verification conditions are generated
     5.5      automatically from pre/post conditions and loop invariants).
     5.6    *}
     5.7 -
     5.8    theories Hoare
     5.9    files "document/root.bib" "document/root.tex"
    5.10  
     6.1 --- a/src/HOL/Rat.thy	Fri Mar 07 15:52:56 2014 +0000
     6.2 +++ b/src/HOL/Rat.thy	Fri Mar 07 20:50:02 2014 +0100
     6.3 @@ -1155,12 +1155,16 @@
     6.4        let
     6.5          fun mk 1 = Syntax.const @{const_syntax Num.One}
     6.6            | mk i =
     6.7 -              let val (q, r) = Integer.div_mod i 2
     6.8 -              in HOLogic.mk_bit r $ (mk q) end;
     6.9 +              let
    6.10 +                val (q, r) = Integer.div_mod i 2;
    6.11 +                val bit = if r = 0 then @{const_syntax Num.Bit0} else @{const_syntax Num.Bit1};
    6.12 +              in Syntax.const bit $ (mk q) end;
    6.13        in
    6.14          if i = 0 then Syntax.const @{const_syntax Groups.zero}
    6.15          else if i > 0 then Syntax.const @{const_syntax Num.numeral} $ mk i
    6.16 -        else Syntax.const @{const_syntax Groups.uminus} $ (Syntax.const @{const_syntax Num.numeral} $ mk (~i))
    6.17 +        else
    6.18 +          Syntax.const @{const_syntax Groups.uminus} $
    6.19 +            (Syntax.const @{const_syntax Num.numeral} $ mk (~ i))
    6.20        end;
    6.21  
    6.22      fun mk_frac str =
    6.23 @@ -1181,6 +1185,7 @@
    6.24  lemma "123.456 = -111.111 + 200 + 30 + 4 + 5/10 + 6/100 + (7/1000::rat)"
    6.25    by simp
    6.26  
    6.27 +
    6.28  subsection {* Hiding implementation details *}
    6.29  
    6.30  hide_const (open) normalize positive
     7.1 --- a/src/HOL/Statespace/distinct_tree_prover.ML	Fri Mar 07 15:52:56 2014 +0000
     7.2 +++ b/src/HOL/Statespace/distinct_tree_prover.ML	Fri Mar 07 20:50:02 2014 +0100
     7.3 @@ -77,14 +77,6 @@
     7.4    | x => x);
     7.5  
     7.6  
     7.7 -fun index_tree (Const (@{const_name Tip}, _)) path tab = tab
     7.8 -  | index_tree (Const (@{const_name Node}, _) $ l $ x $ _ $ r) path tab =
     7.9 -      tab
    7.10 -      |> Termtab.update_new (x, path)
    7.11 -      |> index_tree l (path @ [Left])
    7.12 -      |> index_tree r (path @ [Right])
    7.13 -  | index_tree t _ _ = raise TERM ("index_tree: input not a tree", [t])
    7.14 -
    7.15  fun split_common_prefix xs [] = ([], xs, [])
    7.16    | split_common_prefix [] ys = ([], [], ys)
    7.17    | split_common_prefix (xs as (x :: xs')) (ys as (y :: ys')) =
    7.18 @@ -138,7 +130,6 @@
    7.19   *)
    7.20  fun naive_cterm_first_order_match (t, ct) env =
    7.21    let
    7.22 -    val thy = theory_of_cterm ct;
    7.23      fun mtch (env as (tyinsts, insts)) =
    7.24        fn (Var (ixn, T), ct) =>
    7.25            (case AList.lookup (op =) insts ixn of
     8.1 --- a/src/HOL/Statespace/state_fun.ML	Fri Mar 07 15:52:56 2014 +0000
     8.2 +++ b/src/HOL/Statespace/state_fun.ML	Fri Mar 07 20:50:02 2014 +0100
     8.3 @@ -174,7 +174,7 @@
     8.4    Simplifier.simproc_global @{theory} "update_simp" ["update d c n v s"]
     8.5      (fn ctxt => fn t =>
     8.6        (case t of
     8.7 -        ((upd as Const (@{const_name StateFun.update}, uT)) $ d $ c $ n $ v $ s) =>
     8.8 +        Const (@{const_name StateFun.update}, uT) $ _ $ _ $ _ $ _ $ _ =>
     8.9            let
    8.10              val (_ :: _ :: _ :: _ :: sT :: _) = binder_types uT;
    8.11                (*"('v => 'a1) => ('a2 => 'v) => 'n => ('a1 => 'a2) => ('n => 'v) => ('n => 'v)"*)
    8.12 @@ -208,7 +208,7 @@
    8.13                  * updates again, the optimised term is constructed.
    8.14                  *)
    8.15              fun mk_updterm already
    8.16 -                (t as ((upd as Const (@{const_name StateFun.update}, uT)) $ d $ c $ n $ v $ s)) =
    8.17 +                ((upd as Const (@{const_name StateFun.update}, uT)) $ d $ c $ n $ v $ s) =
    8.18                    let
    8.19                      fun rest already = mk_updterm already;
    8.20                      val (dT :: cT :: nT :: vT :: sT :: _) = binder_types uT;
    8.21 @@ -238,7 +238,8 @@
    8.22                                Const (@{const_name StateFun.update},
    8.23                                  d'T --> c'T --> nT --> vT' --> sT --> sT);
    8.24                            in
    8.25 -                            (upd $ d $ c $ n $ kb $ trm, upd' $ d' $ c' $ n $ f' $ trm', kv :: vars, comps', b)
    8.26 +                            (upd $ d $ c $ n $ kb $ trm, upd' $ d' $ c' $ n $ f' $ trm', kv :: vars,
    8.27 +                              comps', b)
    8.28                            end)
    8.29                    end
    8.30                | mk_updterm _ t = init_seed t;
     9.1 --- a/src/HOL/Statespace/state_space.ML	Fri Mar 07 15:52:56 2014 +0000
     9.2 +++ b/src/HOL/Statespace/state_space.ML	Fri Mar 07 20:50:02 2014 +0100
     9.3 @@ -78,16 +78,6 @@
     9.4  fun fold1' f [] x = x
     9.5    | fold1' f xs _ = fold1 f xs
     9.6  
     9.7 -fun sublist_idx eq xs ys =
     9.8 -  let
     9.9 -    fun sublist n xs ys =
    9.10 -         if is_prefix eq xs ys then SOME n
    9.11 -         else (case ys of [] => NONE
    9.12 -               | (y::ys') => sublist (n+1) xs ys')
    9.13 -  in sublist 0 xs ys end;
    9.14 -
    9.15 -fun is_sublist eq xs ys = is_some (sublist_idx eq xs ys);
    9.16 -
    9.17  fun sorted_subset eq [] ys = true
    9.18    | sorted_subset eq (x::xs) [] = false
    9.19    | sorted_subset eq (x::xs) (y::ys) = if eq (x,y) then sorted_subset eq xs ys
    9.20 @@ -118,13 +108,6 @@
    9.21       {declinfo=declinfo,distinctthm=distinctthm,silent=silent};
    9.22  
    9.23  
    9.24 -fun delete_declinfo n ctxt =
    9.25 -  let val {declinfo,distinctthm,silent} = NameSpaceData.get ctxt;
    9.26 -  in NameSpaceData.put
    9.27 -       (make_namespace_data (Termtab.delete_safe n declinfo) distinctthm silent) ctxt
    9.28 -  end;
    9.29 -
    9.30 -
    9.31  fun update_declinfo (n,v) ctxt =
    9.32    let val {declinfo,distinctthm,silent} = NameSpaceData.get ctxt;
    9.33    in NameSpaceData.put
    9.34 @@ -252,7 +235,6 @@
    9.35    let
    9.36      val all_comps = parent_comps @ new_comps;
    9.37      val vars = (map (fn n => (Binding.name n, NONE, NoSyn)) all_comps);
    9.38 -    val full_name = Sign.full_bname thy name;
    9.39      val dist_thm_name = distinct_compsN;
    9.40  
    9.41      val dist_thm_full_name = dist_thm_name;
    9.42 @@ -296,7 +278,7 @@
    9.43      |> interprete_parent name dist_thm_full_name parent_expr
    9.44    end;
    9.45  
    9.46 -fun encode_dot x = if x= #"." then #"_" else x;
    9.47 +fun encode_dot x = if x = #"." then #"_" else x;
    9.48  
    9.49  fun encode_type (TFree (s, _)) = s
    9.50    | encode_type (TVar ((s,i),_)) = "?" ^ s ^ string_of_int i
    9.51 @@ -309,23 +291,6 @@
    9.52  fun project_name T = projectN ^"_"^encode_type T;
    9.53  fun inject_name T = injectN ^"_"^encode_type T;
    9.54  
    9.55 -fun project_free T pT V = Free (project_name T, V --> pT);
    9.56 -fun inject_free T pT V = Free (inject_name T, pT --> V);
    9.57 -
    9.58 -fun get_name n = getN ^ "_" ^ n;
    9.59 -fun put_name n = putN ^ "_" ^ n;
    9.60 -fun get_const n T nT V = Free (get_name n, (nT --> V) --> T);
    9.61 -fun put_const n T nT V = Free (put_name n, T --> (nT --> V) --> (nT --> V));
    9.62 -
    9.63 -fun lookup_const T nT V =
    9.64 -  Const (@{const_name StateFun.lookup}, (V --> T) --> nT --> (nT --> V) --> T);
    9.65 -
    9.66 -fun update_const T nT V =
    9.67 -  Const (@{const_name StateFun.update},
    9.68 -    (V --> T) --> (T --> V) --> nT --> (T --> T) --> (nT --> V) --> (nT --> V));
    9.69 -
    9.70 -fun K_const T = Const (@{const_name K_statefun}, T --> T --> T);
    9.71 -
    9.72  
    9.73  fun add_declaration name decl thy =
    9.74    thy
    9.75 @@ -347,15 +312,12 @@
    9.76      val all_comps = rename renaming (parent_comps @ map (apsnd subst) components);
    9.77    in all_comps end;
    9.78  
    9.79 -fun take_upto i xs = List.take(xs,i) handle General.Subscript => xs;
    9.80 -
    9.81  fun statespace_definition state_type args name parents parent_comps components thy =
    9.82    let
    9.83      val full_name = Sign.full_bname thy name;
    9.84      val all_comps = parent_comps @ components;
    9.85  
    9.86      val components' = map (fn (n,T) => (n,(T,full_name))) components;
    9.87 -    val all_comps' = map (fn (n,T) => (n,(T,full_name))) all_comps;
    9.88  
    9.89      fun parent_expr (prefix, (_, n, rs)) =
    9.90        (suffix namespaceN n, (prefix, Expression.Positional rs));
    9.91 @@ -452,11 +414,6 @@
    9.92  
    9.93  (* prepare arguments *)
    9.94  
    9.95 -fun read_raw_parent ctxt raw_T =
    9.96 -  (case Proof_Context.read_typ_abbrev ctxt raw_T of
    9.97 -    Type (name, Ts) => (Ts, name)
    9.98 -  | T => error ("Bad parent statespace specification: " ^ Syntax.string_of_typ ctxt T));
    9.99 -
   9.100  fun read_typ ctxt raw_T env =
   9.101    let
   9.102      val ctxt' = fold (Variable.declare_typ o TFree) env ctxt;
   9.103 @@ -587,16 +544,15 @@
   9.104  (*** parse/print - translations ***)
   9.105  
   9.106  local
   9.107 +
   9.108  fun map_get_comp f ctxt (Free (name,_)) =
   9.109        (case (get_comp ctxt name) of
   9.110          SOME (T,_) => f T T dummyT
   9.111        | NONE => (Syntax.free "arbitrary"(*; error "context not ready"*)))
   9.112    | map_get_comp _ _ _ = Syntax.free "arbitrary";
   9.113  
   9.114 -val get_comp_projection = map_get_comp project_free;
   9.115 -val get_comp_injection  = map_get_comp inject_free;
   9.116 +fun name_of (Free (n,_)) = n;
   9.117  
   9.118 -fun name_of (Free (n,_)) = n;
   9.119  in
   9.120  
   9.121  fun gen_lookup_tr ctxt s n =
   9.122 @@ -624,7 +580,7 @@
   9.123            then Syntax.const "_statespace_lookup" $ s $ n
   9.124            else raise Match
   9.125        | NONE => raise Match)
   9.126 -  | lookup_tr' _ ts = raise Match;
   9.127 +  | lookup_tr' _ _ = raise Match;
   9.128  
   9.129  fun gen_update_tr id ctxt n v s =
   9.130    let
    10.1 --- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Fri Mar 07 15:52:56 2014 +0000
    10.2 +++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Fri Mar 07 20:50:02 2014 +0100
    10.3 @@ -21,7 +21,6 @@
    10.4    val strip_case: Proof.context -> bool -> term -> (term * (term * term) list) option
    10.5    val strip_case_full: Proof.context -> bool -> term -> term
    10.6    val show_cases: bool Config.T
    10.7 -  val setup: theory -> theory
    10.8    val register: term -> term list -> Context.generic -> Context.generic
    10.9  end;
   10.10  
   10.11 @@ -170,7 +169,7 @@
   10.12          fun dest_case2 (Const (@{syntax_const "_case2"}, _) $ t $ u) = t :: dest_case2 u
   10.13            | dest_case2 t = [t];
   10.14  
   10.15 -        val errt = if err then @{term True} else @{term False};
   10.16 +        val errt = Syntax.const (if err then @{const_syntax True} else @{const_syntax False});
   10.17        in
   10.18          Syntax.const @{const_syntax case_guard} $ errt $ t $
   10.19            (fold_rev
   10.20 @@ -180,7 +179,7 @@
   10.21        end
   10.22    | case_tr _ _ _ = case_error "case_tr";
   10.23  
   10.24 -val trfun_setup = Sign.parse_translation [(@{syntax_const "_case_syntax"}, case_tr true)];
   10.25 +val _ = Theory.setup (Sign.parse_translation [(@{syntax_const "_case_syntax"}, case_tr true)]);
   10.26  
   10.27  
   10.28  (* print translation *)
   10.29 @@ -207,7 +206,7 @@
   10.30        end
   10.31    | case_tr' _ = raise Match;
   10.32  
   10.33 -val trfun_setup' = Sign.print_translation [(@{const_syntax "case_guard"}, K case_tr')];
   10.34 +val _ = Theory.setup (Sign.print_translation [(@{const_syntax "case_guard"}, K case_tr')]);
   10.35  
   10.36  
   10.37  (* declarations *)
   10.38 @@ -229,6 +228,12 @@
   10.39      |> map_cases update_cases
   10.40    end;
   10.41  
   10.42 +val _ = Theory.setup
   10.43 +  (Attrib.setup @{binding case_translation}
   10.44 +    (Args.term -- Scan.repeat1 Args.term >>
   10.45 +      (fn (t, ts) => Thm.declaration_attribute (K (register t ts))))
   10.46 +    "declaration of case combinators and constructors");
   10.47 +
   10.48  
   10.49  (* (Un)check phases *)
   10.50  
   10.51 @@ -453,8 +458,7 @@
   10.52      map decode_case
   10.53    end;
   10.54  
   10.55 -val term_check_setup =
   10.56 -  Context.theory_map (Syntax_Phases.term_check 1 "case" check_case);
   10.57 +val _ = Context.>> (Syntax_Phases.term_check 1 "case" check_case);
   10.58  
   10.59  
   10.60  (* Pretty printing of nested case expressions *)
   10.61 @@ -595,21 +599,7 @@
   10.62    then map (fn t => if can Term.type_of t then strip_case_full ctxt true t else t) ts
   10.63    else ts;
   10.64  
   10.65 -val term_uncheck_setup =
   10.66 -  Context.theory_map (Syntax_Phases.term_uncheck 1 "case" uncheck_case);
   10.67 -
   10.68 -
   10.69 -(* theory setup *)
   10.70 -
   10.71 -val setup =
   10.72 -  trfun_setup #>
   10.73 -  trfun_setup' #>
   10.74 -  term_check_setup #>
   10.75 -  term_uncheck_setup #>
   10.76 -  Attrib.setup @{binding case_translation}
   10.77 -    (Args.term -- Scan.repeat1 Args.term >>
   10.78 -      (fn (t, ts) => Thm.declaration_attribute (K (register t ts))))
   10.79 -    "declaration of case combinators and constructors";
   10.80 +val _ = Context.>>  (Syntax_Phases.term_uncheck 1 "case" uncheck_case);
   10.81  
   10.82  
   10.83  (* outer syntax commands *)
    11.1 --- a/src/Pure/General/completion.ML	Fri Mar 07 15:52:56 2014 +0000
    11.2 +++ b/src/Pure/General/completion.ML	Fri Mar 07 20:50:02 2014 +0100
    11.3 @@ -7,7 +7,7 @@
    11.4  signature COMPLETION =
    11.5  sig
    11.6    type T
    11.7 -  val names: Position.T -> (string * string) list -> T
    11.8 +  val names: Position.T -> (string * (string * string)) list -> T
    11.9    val none: T
   11.10    val reported_text: T -> string
   11.11    val report: T -> unit
   11.12 @@ -17,7 +17,8 @@
   11.13  structure Completion: COMPLETION =
   11.14  struct
   11.15  
   11.16 -abstype T = Completion of {pos: Position.T, total: int, names: (string * string) list}
   11.17 +abstype T =
   11.18 +  Completion of {pos: Position.T, total: int, names: (string * (string * string)) list}
   11.19  with
   11.20  
   11.21  (* completion of names *)
   11.22 @@ -40,7 +41,7 @@
   11.23        let
   11.24          val markup = Position.markup pos Markup.completion;
   11.25          val body = (total, names) |>
   11.26 -          let open XML.Encode in pair int (list (pair string string)) end;
   11.27 +          let open XML.Encode in pair int (list (pair string (pair string string))) end;
   11.28        in YXML.string_of (XML.Elem (markup, body)) end
   11.29      else ""
   11.30    end;
    12.1 --- a/src/Pure/General/completion.scala	Fri Mar 07 15:52:56 2014 +0000
    12.2 +++ b/src/Pure/General/completion.scala	Fri Mar 07 20:50:02 2014 +0100
    12.3 @@ -21,11 +21,10 @@
    12.4      range: Text.Range,
    12.5      original: String,
    12.6      name: String,
    12.7 -    description: String,
    12.8 +    description: List[String],
    12.9      replacement: String,
   12.10      move: Int,
   12.11      immediate: Boolean)
   12.12 -  { override def toString: String = description }
   12.13  
   12.14    object Result
   12.15    {
   12.16 @@ -136,7 +135,7 @@
   12.17                val (total, names) =
   12.18                {
   12.19                  import XML.Decode._
   12.20 -                pair(int, list(pair(string, string)))(body)
   12.21 +                pair(int, list(pair(string, pair(string, string))))(body)
   12.22                }
   12.23                Some(Names(info.range, total, names))
   12.24              }
   12.25 @@ -148,21 +147,27 @@
   12.26      }
   12.27    }
   12.28  
   12.29 -  sealed case class Names(range: Text.Range, total: Int, names: List[(String, String)])
   12.30 +  sealed case class Names(
   12.31 +    range: Text.Range, total: Int, names: List[(String, (String, String))])
   12.32    {
   12.33      def no_completion: Boolean = total == 0 && names.isEmpty
   12.34  
   12.35      def complete(
   12.36        history: Completion.History,
   12.37 -      decode: Boolean,
   12.38 +      do_decode: Boolean,
   12.39        original: String): Option[Completion.Result] =
   12.40      {
   12.41 +      def decode(s: String): String = if (do_decode) Symbol.decode(s) else s
   12.42        val items =
   12.43          for {
   12.44 -          (xname, name) <- names
   12.45 -          xname1 = (if (decode) Symbol.decode(xname) else xname)
   12.46 +          (xname, (kind, name)) <- names
   12.47 +          xname1 = decode(xname)
   12.48            if xname1 != original
   12.49 -        } yield Item(range, original, name, xname1, xname1, 0, true)
   12.50 +          (full_name, descr_name) =
   12.51 +            if (kind == "") (name, quote(decode(name)))
   12.52 +            else (kind + "." + name, Library.plain_words(kind) + " " + quote(decode(name)))
   12.53 +          description = List(xname1, "(" + descr_name + ")")
   12.54 +        } yield Item(range, original, full_name, description, xname1, 0, true)
   12.55  
   12.56        if (items.isEmpty) None
   12.57        else Some(Result(range, original, names.length == 1, items.sorted(history.ordering)))
   12.58 @@ -252,24 +257,31 @@
   12.59  }
   12.60  
   12.61  final class Completion private(
   12.62 -  keywords: Set[String] = Set.empty,
   12.63 +  keywords: Map[String, Boolean] = Map.empty,
   12.64    words_lex: Scan.Lexicon = Scan.Lexicon.empty,
   12.65    words_map: Multi_Map[String, String] = Multi_Map.empty,
   12.66    abbrevs_lex: Scan.Lexicon = Scan.Lexicon.empty,
   12.67    abbrevs_map: Multi_Map[String, (String, String)] = Multi_Map.empty)
   12.68  {
   12.69 -  /* adding stuff */
   12.70 +  /* keywords */
   12.71  
   12.72 -  def + (keyword: String, replace: String): Completion =
   12.73 +  private def is_symbol(name: String): Boolean = Symbol.names.isDefinedAt(name)
   12.74 +  private def is_keyword(name: String): Boolean = !is_symbol(name) && keywords.isDefinedAt(name)
   12.75 +  private def is_keyword_template(name: String): Boolean = is_keyword(name) && keywords(name)
   12.76 +
   12.77 +  def + (keyword: String, template: String): Completion =
   12.78      new Completion(
   12.79 -      keywords + keyword,
   12.80 +      keywords + (keyword -> (keyword != template)),
   12.81        words_lex + keyword,
   12.82 -      words_map + (keyword -> replace),
   12.83 +      words_map + (keyword -> template),
   12.84        abbrevs_lex,
   12.85        abbrevs_map)
   12.86  
   12.87    def + (keyword: String): Completion = this + (keyword, keyword)
   12.88  
   12.89 +
   12.90 +  /* symbols with abbreviations */
   12.91 +
   12.92    private def add_symbols(): Completion =
   12.93    {
   12.94      val words =
   12.95 @@ -298,7 +310,7 @@
   12.96  
   12.97    def complete(
   12.98      history: Completion.History,
   12.99 -    decode: Boolean,
  12.100 +    do_decode: Boolean,
  12.101      explicit: Boolean,
  12.102      start: Text.Offset,
  12.103      text: CharSequence,
  12.104 @@ -306,6 +318,7 @@
  12.105      extend_word: Boolean,
  12.106      language_context: Completion.Language_Context): Option[Completion.Result] =
  12.107    {
  12.108 +    def decode(s: String): String = if (do_decode) Symbol.decode(s) else s
  12.109      val length = text.length
  12.110  
  12.111      val abbrevs_result =
  12.112 @@ -328,7 +341,8 @@
  12.113      }
  12.114  
  12.115      val words_result =
  12.116 -      abbrevs_result orElse {
  12.117 +      if (abbrevs_result.isDefined) None
  12.118 +      else {
  12.119          val end =
  12.120            if (extend_word) Completion.Word_Parsers.extend_word(text, caret)
  12.121            else caret
  12.122 @@ -344,7 +358,7 @@
  12.123              val completions =
  12.124                for {
  12.125                  s <- words_lex.completions(word)
  12.126 -                if (if (keywords(s)) language_context.is_outer else language_context.symbols)
  12.127 +                if (if (is_keyword(s)) language_context.is_outer else language_context.symbols)
  12.128                  r <- words_map.get_list(s)
  12.129                } yield r
  12.130              if (completions.isEmpty) None
  12.131 @@ -353,26 +367,43 @@
  12.132          }
  12.133        }
  12.134  
  12.135 -    words_result match {
  12.136 -      case Some(((word, cs), end)) =>
  12.137 -        val range = Text.Range(- word.length, 0) + end + start
  12.138 -        val ds = (if (decode) cs.map(Symbol.decode(_)) else cs).filter(_ != word)
  12.139 -        if (ds.isEmpty) None
  12.140 -        else {
  12.141 -          val immediate =
  12.142 -            !Completion.Word_Parsers.is_word(word) &&
  12.143 -            Character.codePointCount(word, 0, word.length) > 1
  12.144 -          val items =
  12.145 -            ds.map(s => {
  12.146 -              val (s1, s2) =
  12.147 -                space_explode(Completion.caret_indicator, s) match {
  12.148 -                  case List(s1, s2) => (s1, s2)
  12.149 -                  case _ => (s, "")
  12.150 -                }
  12.151 -              Completion.Item(range, word, s, s, s1 + s2, - s2.length, explicit || immediate)
  12.152 -            })
  12.153 -          Some(Completion.Result(range, word, cs.length == 1, items.sorted(history.ordering)))
  12.154 -        }
  12.155 +    (abbrevs_result orElse words_result) match {
  12.156 +      case Some(((original, completions0), end)) =>
  12.157 +        val completions1 = completions0.map(decode(_))
  12.158 +
  12.159 +        val range = Text.Range(- original.length, 0) + end + start
  12.160 +        val immediate =
  12.161 +          explicit ||
  12.162 +            (!Completion.Word_Parsers.is_word(original) &&
  12.163 +              Character.codePointCount(original, 0, original.length) > 1)
  12.164 +        val unique = completions0.length == 1
  12.165 +
  12.166 +        val items =
  12.167 +          for {
  12.168 +            (name0, name1) <- completions0 zip completions1
  12.169 +            if name1 != original
  12.170 +            (s1, s2) =
  12.171 +              space_explode(Completion.caret_indicator, name1) match {
  12.172 +                case List(s1, s2) => (s1, s2)
  12.173 +                case _ => (name1, "")
  12.174 +              }
  12.175 +            move = - s2.length
  12.176 +            description =
  12.177 +              if (is_symbol(name0)) {
  12.178 +                if (name0 == name1) List(name0)
  12.179 +                else List(name1, "(symbol " + quote(name0) + ")")
  12.180 +              }
  12.181 +              else if (move != 0 || is_keyword_template(name0))
  12.182 +                List(name1, "(template)")
  12.183 +              else if (is_keyword(name0))
  12.184 +                List(name1, "(keyword)")
  12.185 +              else List(name1)
  12.186 +          }
  12.187 +          yield Completion.Item(range, original, name1, description, s1 + s2, move, immediate)
  12.188 +
  12.189 +        if (items.isEmpty) None
  12.190 +        else Some(Completion.Result(range, original, unique, items.sorted(history.ordering)))
  12.191 +
  12.192        case None => None
  12.193      }
  12.194    }
    13.1 --- a/src/Pure/General/name_space.ML	Fri Mar 07 15:52:56 2014 +0000
    13.2 +++ b/src/Pure/General/name_space.ML	Fri Mar 07 20:50:02 2014 +0100
    13.3 @@ -208,11 +208,13 @@
    13.4    if Position.is_reported pos then
    13.5      let
    13.6        val x = Name.clean xname;
    13.7 -      val Name_Space {kind = k, internals, ...} = space;
    13.8 +      val Name_Space {kind, internals, ...} = space;
    13.9        val ext = extern_shortest (Context.proof_of context) space;
   13.10        val names =
   13.11          Symtab.fold
   13.12 -          (fn (a, (b :: _, _)) => String.isPrefix x a ? cons (ext b, Long_Name.implode [k, b])
   13.13 +          (fn (a, (name :: _, _)) =>
   13.14 +              if String.isPrefix x a andalso not (is_concealed space name)
   13.15 +              then cons (ext name, (kind, name)) else I
   13.16              | _ => I) internals []
   13.17          |> sort_distinct (string_ord o pairself #1);
   13.18      in Completion.names pos names end
    14.1 --- a/src/Pure/General/scan.scala	Fri Mar 07 15:52:56 2014 +0000
    14.2 +++ b/src/Pure/General/scan.scala	Fri Mar 07 20:50:02 2014 +0100
    14.3 @@ -7,6 +7,7 @@
    14.4  package isabelle
    14.5  
    14.6  
    14.7 +import scala.annotation.tailrec
    14.8  import scala.collection.{IndexedSeq, TraversableOnce}
    14.9  import scala.collection.immutable.PagedSeq
   14.10  import scala.util.parsing.input.{OffsetPosition, Position => InputPosition, Reader}
   14.11 @@ -323,14 +324,15 @@
   14.12      private def lookup(str: CharSequence): Option[(Boolean, Lexicon.Tree)] =
   14.13      {
   14.14        val len = str.length
   14.15 -      def look(tree: Lexicon.Tree, tip: Boolean, i: Int): Option[(Boolean, Lexicon.Tree)] =
   14.16 +      @tailrec def look(tree: Lexicon.Tree, tip: Boolean, i: Int): Option[(Boolean, Lexicon.Tree)] =
   14.17        {
   14.18          if (i < len) {
   14.19            tree.branches.get(str.charAt(i)) match {
   14.20              case Some((s, tr)) => look(tr, !s.isEmpty, i + 1)
   14.21              case None => None
   14.22            }
   14.23 -        } else Some(tip, tree)
   14.24 +        }
   14.25 +        else Some(tip, tree)
   14.26        }
   14.27        look(rep, false, 0)
   14.28      }
    15.1 --- a/src/Pure/Syntax/syntax_phases.ML	Fri Mar 07 15:52:56 2014 +0000
    15.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Fri Mar 07 20:50:02 2014 +0100
    15.3 @@ -228,6 +228,22 @@
    15.4        Proof_Context.check_const ctxt {proper = true, strict = false} (c, ps);
    15.5    in (c', reports) end;
    15.6  
    15.7 +local
    15.8 +
    15.9 +fun get_free ctxt x =
   15.10 +  let
   15.11 +    val fixed = Variable.lookup_fixed ctxt x;
   15.12 +    val is_const = can (decode_const ctxt) (x, []) orelse Long_Name.is_qualified x;
   15.13 +    val is_declared = is_some (Variable.def_type ctxt false (x, ~1));
   15.14 +  in
   15.15 +    if Variable.is_const ctxt x then NONE
   15.16 +    else if is_some fixed then fixed
   15.17 +    else if not is_const orelse is_declared then SOME x
   15.18 +    else NONE
   15.19 +  end;
   15.20 +
   15.21 +in
   15.22 +
   15.23  fun decode_term _ (result as (_: Position.report_text list, Exn.Exn _)) = result
   15.24    | decode_term ctxt (reports0, Exn.Res tm) =
   15.25        let
   15.26 @@ -235,24 +251,6 @@
   15.27          fun report ps = Position.store_reports reports ps;
   15.28          val append_reports = Position.append_reports reports;
   15.29  
   15.30 -        fun get_free x =
   15.31 -          let
   15.32 -            val fixed = Variable.lookup_fixed ctxt x;
   15.33 -            val is_const = can (decode_const ctxt) (x, []) orelse Long_Name.is_qualified x;
   15.34 -            val is_declared = is_some (Variable.def_type ctxt false (x, ~1));
   15.35 -          in
   15.36 -            if Variable.is_const ctxt x then NONE
   15.37 -            else if is_some fixed then fixed
   15.38 -            else if not is_const orelse is_declared then SOME x
   15.39 -            else NONE
   15.40 -          end;
   15.41 -
   15.42 -        fun the_const (a, ps) =
   15.43 -          let
   15.44 -            val (c, rs) = decode_const ctxt (a, ps);
   15.45 -            val _ = append_reports rs;
   15.46 -          in c end;
   15.47 -
   15.48          fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) =
   15.49                (case Term_Position.decode_position typ of
   15.50                  SOME (p, T) => Type.constraint T (decode (p :: ps) qs bs t)
   15.51 @@ -274,15 +272,20 @@
   15.52                    let
   15.53                      val c =
   15.54                        (case try Lexicon.unmark_const a of
   15.55 -                        SOME c => (report ps (markup_const ctxt) c; c)
   15.56 -                      | NONE => the_const (a, ps));
   15.57 +                        SOME c => c
   15.58 +                      | NONE => #1 (decode_const ctxt (a, [])));
   15.59 +                    val _ = report ps (markup_const ctxt) c;
   15.60                    in Const (c, T) end)
   15.61            | decode ps _ _ (Free (a, T)) =
   15.62                ((Name.reject_internal (a, ps) handle ERROR msg =>
   15.63                    error (msg ^ Proof_Context.consts_completion_message ctxt (a, ps)));
   15.64 -                (case get_free a of
   15.65 +                (case get_free ctxt a of
   15.66                    SOME x => (report ps (markup_free ctxt) x; Free (x, T))
   15.67 -                | NONE => Const (the_const (a, ps), T)))
   15.68 +                | NONE =>
   15.69 +                    let
   15.70 +                      val (c, rs) = decode_const ctxt (a, ps);
   15.71 +                      val _ = append_reports rs;
   15.72 +                    in Const (c, T) end))
   15.73            | decode ps _ _ (Var (xi, T)) = (report ps markup_var xi; Var (xi, T))
   15.74            | decode ps _ bs (t as Bound i) =
   15.75                (case try (nth bs) i of
   15.76 @@ -292,6 +295,8 @@
   15.77          val tm' = Exn.interruptible_capture (fn () => decode [] [] [] tm) ();
   15.78        in (! reports, tm') end;
   15.79  
   15.80 +end;
   15.81 +
   15.82  
   15.83  
   15.84  (** parse **)
   15.85 @@ -332,7 +337,7 @@
   15.86        else
   15.87          [cat_lines
   15.88            (("Ambiguous input" ^ Position.here (Position.reset_range pos) ^
   15.89 -            "\nproduces " ^ string_of_int len ^ " parse trees" ^
   15.90 +            " produces " ^ string_of_int len ^ " parse trees" ^
   15.91              (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
   15.92              map (Pretty.string_of o Pretty.item o single o Parser.pretty_parsetree)
   15.93                (take limit pts))];
   15.94 @@ -412,12 +417,11 @@
   15.95              report_result ctxt pos []
   15.96                [(reports', Exn.Exn (Exn.EXCEPTIONS (map ERROR ambig_msgs @ errs)))]
   15.97            else if checked_len = 1 then
   15.98 -            (if parsed_len > 1 andalso ambiguity_warning then
   15.99 +            (if not (null ambig_msgs) andalso ambiguity_warning then
  15.100                Context_Position.if_visible ctxt warning
  15.101                  (cat_lines (ambig_msgs @
  15.102 -                  ["Fortunately, only one parse tree is type correct" ^
  15.103 -                  Position.here (Position.reset_range pos) ^
  15.104 -                  ",\nbut you may still want to disambiguate your grammar or your input."]))
  15.105 +                  ["Fortunately, only one parse tree is well-formed and type-correct,\n\
  15.106 +                   \but you may still want to disambiguate your grammar or your input."]))
  15.107               else (); report_result ctxt pos [] results')
  15.108            else
  15.109              report_result ctxt pos []
    16.1 --- a/src/Pure/library.scala	Fri Mar 07 15:52:56 2014 +0000
    16.2 +++ b/src/Pure/library.scala	Fri Mar 07 20:50:02 2014 +0100
    16.3 @@ -97,6 +97,9 @@
    16.4      else ""
    16.5    }
    16.6  
    16.7 +  def plain_words(str: String): String =
    16.8 +    space_explode('_', str).mkString(" ")
    16.9 +
   16.10  
   16.11    /* strings */
   16.12  
    17.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Fri Mar 07 15:52:56 2014 +0000
    17.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Fri Mar 07 20:50:02 2014 +0100
    17.3 @@ -25,6 +25,22 @@
    17.4  
    17.5  object Completion_Popup
    17.6  {
    17.7 +  /** items with HTML rendering **/
    17.8 +
    17.9 +  private class Item(val item: Completion.Item)
   17.10 +  {
   17.11 +    private val html =
   17.12 +      item.description match {
   17.13 +        case a :: bs =>
   17.14 +          "<html><b>" + HTML.encode(a) + "</b>" +
   17.15 +            HTML.encode(bs.map(" " + _).mkString) + "</html>"
   17.16 +        case Nil => ""
   17.17 +      }
   17.18 +    override def toString: String = html
   17.19 +  }
   17.20 +
   17.21 +
   17.22 +
   17.23    /** jEdit text area **/
   17.24  
   17.25    object Text_Area
   17.26 @@ -210,8 +226,10 @@
   17.27              SwingUtilities.convertPoint(painter,
   17.28                loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered)
   17.29  
   17.30 +          val items = result.items.map(new Item(_))
   17.31            val completion =
   17.32 -            new Completion_Popup(Some((range, invalidate _)), layered, loc2, font, result.items) {
   17.33 +            new Completion_Popup(Some((range, invalidate _)), layered, loc2, font, items)
   17.34 +            {
   17.35                override def complete(item: Completion.Item) {
   17.36                  PIDE.completion_history.update(item)
   17.37                  insert(item)
   17.38 @@ -402,18 +420,19 @@
   17.39                val loc =
   17.40                  SwingUtilities.convertPoint(text_field, fm.stringWidth(text), fm.getHeight, layered)
   17.41  
   17.42 +              val items = result.items.map(new Item(_))
   17.43                val completion =
   17.44 -                new Completion_Popup(None, layered, loc, text_field.getFont, result.items)
   17.45 -              {
   17.46 -                override def complete(item: Completion.Item) {
   17.47 -                  PIDE.completion_history.update(item)
   17.48 -                  insert(item)
   17.49 +                new Completion_Popup(None, layered, loc, text_field.getFont, items)
   17.50 +                {
   17.51 +                  override def complete(item: Completion.Item) {
   17.52 +                    PIDE.completion_history.update(item)
   17.53 +                    insert(item)
   17.54 +                  }
   17.55 +                  override def propagate(evt: KeyEvent) {
   17.56 +                    if (!evt.isConsumed) text_field.processKeyEvent(evt)
   17.57 +                  }
   17.58 +                  override def refocus() { text_field.requestFocus }
   17.59                  }
   17.60 -                override def propagate(evt: KeyEvent) {
   17.61 -                  if (!evt.isConsumed) text_field.processKeyEvent(evt)
   17.62 -                }
   17.63 -                override def refocus() { text_field.requestFocus }
   17.64 -              }
   17.65                completion_popup = Some(completion)
   17.66                completion.show_popup()
   17.67  
   17.68 @@ -474,7 +493,7 @@
   17.69    layered: JLayeredPane,
   17.70    location: Point,
   17.71    font: Font,
   17.72 -  items: List[Completion.Item]) extends JPanel(new BorderLayout)
   17.73 +  items: List[Completion_Popup.Item]) extends JPanel(new BorderLayout)
   17.74  {
   17.75    completion =>
   17.76  
   17.77 @@ -508,7 +527,7 @@
   17.78    private def complete_selected(): Boolean =
   17.79    {
   17.80      list_view.selection.items.toList match {
   17.81 -      case item :: _ => complete(item); true
   17.82 +      case item :: _ => complete(item.item); true
   17.83        case _ => false
   17.84      }
   17.85    }
    18.1 --- a/src/Tools/jEdit/src/rendering.scala	Fri Mar 07 15:52:56 2014 +0000
    18.2 +++ b/src/Tools/jEdit/src/rendering.scala	Fri Mar 07 20:50:02 2014 +0100
    18.3 @@ -459,7 +459,7 @@
    18.4            case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) =>
    18.5              Some(Text.Info(r, (t1 + t2, info)))
    18.6            case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _))) =>
    18.7 -            val kind1 = space_explode('_', kind).mkString(" ")
    18.8 +            val kind1 = Library.plain_words(kind)
    18.9              val txt1 = kind1 + " " + quote(name)
   18.10              val t = prev.info._1
   18.11              val txt2 =