--- 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)
--- 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
{
--- 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
--- 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 {*
--- 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"
--- 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
--- 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
--- 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;
--- 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
--- 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 *)
--- 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;
--- 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
}
}
--- 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
--- 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)
}
--- 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 []
--- 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 */
--- 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
}
}
--- 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 =