--- a/NEWS Thu Mar 06 17:55:39 2014 +0100
+++ b/NEWS Thu Mar 06 22:15:01 2014 +0100
@@ -40,6 +40,13 @@
completion for ML source, but within ML strings, comments,
antiquotations.
+* Semantic completions may get extended by appending a suffix of
+underscores to an already recognized name, e.g. "foo_" to complete
+"foo" or "foobar" if these are known in the context. The special
+identifier "__" serves as a wild-card in this respect: it completes to
+the full collection of names from the name space (truncated according
+to the system option "completion_limit").
+
* Document panel: simplied interaction where every single mouse click
(re)opens document via desktop environment or as jEdit buffer.
--- a/src/Doc/ProgProve/LaTeXsugar.thy Thu Mar 06 17:55:39 2014 +0100
+++ b/src/Doc/ProgProve/LaTeXsugar.thy Thu Mar 06 22:15:01 2014 +0100
@@ -46,7 +46,7 @@
setup{*
let
fun pretty ctxt c =
- let val tc = Proof_Context.read_const_proper ctxt false c
+ let val tc = Proof_Context.read_const ctxt {proper = true, strict = false} c
in Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::",
Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]
end
--- a/src/HOL/Decision_Procs/Cooper.thy Thu Mar 06 17:55:39 2014 +0100
+++ b/src/HOL/Decision_Procs/Cooper.thy Thu Mar 06 22:15:01 2014 +0100
@@ -881,9 +881,9 @@
assumes qe_inv: "\<forall>bs p. qfree p \<longrightarrow> qfree (qe p) \<and> Ifm bbs bs (qe p) = Ifm bbs bs (E p)"
shows "\<And>bs. qfree (qelim p qe) \<and> Ifm bbs bs (qelim p qe) = Ifm bbs bs p"
using qe_inv DJ_qe[OF qe_inv]
- by(induct p rule: qelim.induct)
- (auto simp add: not disj conj iff imp not_qf disj_qf conj_qf imp_qf iff_qf
- simpfm simpfm_qf simp del: simpfm.simps)
+ by (induct p rule: qelim.induct)
+ (auto simp add: not disj conj iff imp not_qf disj_qf conj_qf imp_qf iff_qf
+ simpfm simpfm_qf simp del: simpfm.simps)
text {* Linearity for fm where Bound 0 ranges over @{text "\<int>"} *}
@@ -908,7 +908,7 @@
| "zsplit0 (Mul i a) = (let (i', a') = zsplit0 a in (i*i', Mul i a'))"
lemma zsplit0_I:
- shows "\<And>n a. zsplit0 t = (n, a) \<Longrightarrow>
+ "\<And>n a. zsplit0 t = (n, a) \<Longrightarrow>
(Inum ((x::int) # bs) (CN 0 n a) = Inum (x # bs) t) \<and> numbound0 a"
(is "\<And>n a. ?S t = (n,a) \<Longrightarrow> (?I x (CN 0 n a) = ?I x t) \<and> ?N a")
proof (induct t rule: zsplit0.induct)
@@ -930,11 +930,11 @@
moreover
{
assume m0: "m = 0"
- with abj have th: "a'=?b \<and> n=i+?j" using 3
- by (simp add: Let_def split_def)
+ with abj have th: "a' = ?b \<and> n = i + ?j"
+ using 3 by (simp add: Let_def split_def)
from abj 3 m0 have th2: "(?I x (CN 0 ?j ?b) = ?I x a) \<and> ?N ?b"
by blast
- from th have "?I x (CN 0 n a') = ?I x (CN 0 (i+?j) ?b)"
+ from th have "?I x (CN 0 n a') = ?I x (CN 0 (i + ?j) ?b)"
by simp
also from th2 have "\<dots> = ?I x (CN 0 i (CN 0 ?j ?b))"
by (simp add: distrib_right)
@@ -948,8 +948,9 @@
case (4 t n a)
let ?nt = "fst (zsplit0 t)"
let ?at = "snd (zsplit0 t)"
- have abj: "zsplit0 t = (?nt,?at)" by simp
- then have th: "a=Neg ?at \<and> n=-?nt"
+ have abj: "zsplit0 t = (?nt, ?at)"
+ by simp
+ then have th: "a = Neg ?at \<and> n = - ?nt"
using 4 by (simp add: Let_def split_def)
from abj 4 have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at"
by blast
@@ -965,9 +966,9 @@
by simp
moreover have abjt: "zsplit0 t = (?nt, ?at)"
by simp
- ultimately have th: "a=Add ?as ?at \<and> n=?ns + ?nt"
+ ultimately have th: "a = Add ?as ?at \<and> n = ?ns + ?nt"
using 5 by (simp add: Let_def split_def)
- from abjs[symmetric] have bluddy: "\<exists>x y. (x,y) = zsplit0 s"
+ from abjs[symmetric] have bluddy: "\<exists>x y. (x, y) = zsplit0 s"
by blast
from 5 have "(\<exists>x y. (x, y) = zsplit0 s) \<longrightarrow>
(\<forall>xa xb. zsplit0 t = (xa, xb) \<longrightarrow> Inum (x # bs) (CN 0 xa xb) = Inum (x # bs) t \<and> numbound0 xb)"
@@ -988,9 +989,9 @@
by simp
moreover have abjt: "zsplit0 t = (?nt, ?at)"
by simp
- ultimately have th: "a=Sub ?as ?at \<and> n=?ns - ?nt"
+ ultimately have th: "a = Sub ?as ?at \<and> n = ?ns - ?nt"
using 6 by (simp add: Let_def split_def)
- from abjs[symmetric] have bluddy: "\<exists>x y. (x,y) = zsplit0 s"
+ from abjs[symmetric] have bluddy: "\<exists>x y. (x, y) = zsplit0 s"
by blast
from 6 have "(\<exists>x y. (x,y) = zsplit0 s) \<longrightarrow>
(\<forall>xa xb. zsplit0 t = (xa, xb) \<longrightarrow> Inum (x # bs) (CN 0 xa xb) = Inum (x # bs) t \<and> numbound0 xb)"
@@ -1007,7 +1008,7 @@
let ?at = "snd (zsplit0 t)"
have abj: "zsplit0 t = (?nt,?at)"
by simp
- then have th: "a=Mul i ?at \<and> n=i*?nt"
+ then have th: "a = Mul i ?at \<and> n = i * ?nt"
using 7 by (simp add: Let_def split_def)
from abj 7 have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at"
by blast
@@ -1042,34 +1043,50 @@
"zlfm (Or p q) = Or (zlfm p) (zlfm q)"
"zlfm (Imp p q) = Or (zlfm (NOT p)) (zlfm q)"
"zlfm (Iff p q) = Or (And (zlfm p) (zlfm q)) (And (zlfm (NOT p)) (zlfm (NOT q)))"
- "zlfm (Lt a) = (let (c,r) = zsplit0 a in
- if c=0 then Lt r else
- if c>0 then (Lt (CN 0 c r)) else (Gt (CN 0 (- c) (Neg r))))"
- "zlfm (Le a) = (let (c,r) = zsplit0 a in
- if c=0 then Le r else
- if c>0 then (Le (CN 0 c r)) else (Ge (CN 0 (- c) (Neg r))))"
- "zlfm (Gt a) = (let (c,r) = zsplit0 a in
- if c=0 then Gt r else
- if c>0 then (Gt (CN 0 c r)) else (Lt (CN 0 (- c) (Neg r))))"
- "zlfm (Ge a) = (let (c,r) = zsplit0 a in
- if c=0 then Ge r else
- if c>0 then (Ge (CN 0 c r)) else (Le (CN 0 (- c) (Neg r))))"
- "zlfm (Eq a) = (let (c,r) = zsplit0 a in
- if c=0 then Eq r else
- if c>0 then (Eq (CN 0 c r)) else (Eq (CN 0 (- c) (Neg r))))"
- "zlfm (NEq a) = (let (c,r) = zsplit0 a in
- if c=0 then NEq r else
- if c>0 then (NEq (CN 0 c r)) else (NEq (CN 0 (- c) (Neg r))))"
- "zlfm (Dvd i a) = (if i=0 then zlfm (Eq a)
- else (let (c,r) = zsplit0 a in
- if c=0 then (Dvd (abs i) r) else
- if c>0 then (Dvd (abs i) (CN 0 c r))
- else (Dvd (abs i) (CN 0 (- c) (Neg r)))))"
- "zlfm (NDvd i a) = (if i=0 then zlfm (NEq a)
- else (let (c,r) = zsplit0 a in
- if c=0 then (NDvd (abs i) r) else
- if c>0 then (NDvd (abs i) (CN 0 c r))
- else (NDvd (abs i) (CN 0 (- c) (Neg r)))))"
+ "zlfm (Lt a) =
+ (let (c, r) = zsplit0 a in
+ if c = 0 then Lt r else
+ if c > 0 then (Lt (CN 0 c r))
+ else Gt (CN 0 (- c) (Neg r)))"
+ "zlfm (Le a) =
+ (let (c, r) = zsplit0 a in
+ if c = 0 then Le r
+ else if c > 0 then Le (CN 0 c r)
+ else Ge (CN 0 (- c) (Neg r)))"
+ "zlfm (Gt a) =
+ (let (c, r) = zsplit0 a in
+ if c = 0 then Gt r else
+ if c > 0 then Gt (CN 0 c r)
+ else Lt (CN 0 (- c) (Neg r)))"
+ "zlfm (Ge a) =
+ (let (c, r) = zsplit0 a in
+ if c = 0 then Ge r
+ else if c > 0 then Ge (CN 0 c r)
+ else Le (CN 0 (- c) (Neg r)))"
+ "zlfm (Eq a) =
+ (let (c, r) = zsplit0 a in
+ if c = 0 then Eq r
+ else if c > 0 then Eq (CN 0 c r)
+ else Eq (CN 0 (- c) (Neg r)))"
+ "zlfm (NEq a) =
+ (let (c, r) = zsplit0 a in
+ if c = 0 then NEq r
+ else if c > 0 then NEq (CN 0 c r)
+ else NEq (CN 0 (- c) (Neg r)))"
+ "zlfm (Dvd i a) =
+ (if i = 0 then zlfm (Eq a)
+ else
+ let (c, r) = zsplit0 a in
+ if c = 0 then Dvd (abs i) r
+ else if c > 0 then Dvd (abs i) (CN 0 c r)
+ else Dvd (abs i) (CN 0 (- c) (Neg r)))"
+ "zlfm (NDvd i a) =
+ (if i = 0 then zlfm (NEq a)
+ else
+ let (c, r) = zsplit0 a in
+ if c = 0 then NDvd (abs i) r
+ else if c > 0 then NDvd (abs i) (CN 0 c r)
+ else NDvd (abs i) (CN 0 (- c) (Neg r)))"
"zlfm (NOT (And p q)) = Or (zlfm (NOT p)) (zlfm (NOT q))"
"zlfm (NOT (Or p q)) = And (zlfm (NOT p)) (zlfm (NOT q))"
"zlfm (NOT (Imp p q)) = And (zlfm p) (zlfm (NOT q))"
@@ -1091,7 +1108,7 @@
lemma zlfm_I:
assumes qfp: "qfree p"
- shows "(Ifm bbs (i#bs) (zlfm p) = Ifm bbs (i# bs) p) \<and> iszlfm (zlfm 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)
@@ -1101,10 +1118,10 @@
have spl: "zsplit0 a = (?c, ?r)"
by simp
from zsplit0_I[OF spl, where x="i" and bs="bs"]
- have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
+ have Ia: "Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
by auto
- let ?N = "\<lambda>t. Inum (i#bs) t"
- from 5 Ia nb show ?case
+ let ?N = "\<lambda>t. Inum (i # bs) t"
+ from 5 Ia nb show ?case
apply (auto simp add: Let_def split_def algebra_simps)
apply (cases "?r")
apply auto
@@ -1118,9 +1135,9 @@
have spl: "zsplit0 a = (?c, ?r)"
by simp
from zsplit0_I[OF spl, where x="i" and bs="bs"]
- have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
+ have Ia: "Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
by auto
- let ?N = "\<lambda>t. Inum (i#bs) t"
+ let ?N = "\<lambda>t. Inum (i # bs) t"
from 6 Ia nb show ?case
apply (auto simp add: Let_def split_def algebra_simps)
apply (cases "?r")
@@ -1137,7 +1154,7 @@
from zsplit0_I[OF spl, where x="i" and bs="bs"]
have Ia: "Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
by auto
- let ?N = "\<lambda>t. Inum (i#bs) t"
+ let ?N = "\<lambda>t. Inum (i # bs) t"
from 7 Ia nb show ?case
apply (auto simp add: Let_def split_def algebra_simps)
apply (cases "?r")
@@ -1152,9 +1169,9 @@
have spl: "zsplit0 a = (?c, ?r)"
by simp
from zsplit0_I[OF spl, where x="i" and bs="bs"]
- have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
+ have Ia: "Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
by auto
- let ?N = "\<lambda>t. Inum (i#bs) t"
+ let ?N = "\<lambda>t. Inum (i # bs) t"
from 8 Ia nb show ?case
apply (auto simp add: Let_def split_def algebra_simps)
apply (cases "?r")
@@ -1171,7 +1188,7 @@
from zsplit0_I[OF spl, where x="i" and bs="bs"]
have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
by auto
- let ?N = "\<lambda>t. Inum (i#bs) t"
+ let ?N = "\<lambda>t. Inum (i # bs) t"
from 9 Ia nb show ?case
apply (auto simp add: Let_def split_def algebra_simps)
apply (cases "?r")
@@ -1188,7 +1205,7 @@
from zsplit0_I[OF spl, where x="i" and bs="bs"]
have Ia: "Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
by auto
- let ?N = "\<lambda>t. Inum (i#bs) t"
+ let ?N = "\<lambda>t. Inum (i # bs) t"
from 10 Ia nb show ?case
apply (auto simp add: Let_def split_def algebra_simps)
apply (cases "?r")
@@ -1255,13 +1272,13 @@
from zsplit0_I[OF spl, where x="i" and bs="bs"]
have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
by auto
- let ?N = "\<lambda>t. Inum (i#bs) t"
+ let ?N = "\<lambda>t. Inum (i # bs) t"
have "j = 0 \<or> (j \<noteq> 0 \<and> ?c = 0) \<or> (j \<noteq> 0 \<and> ?c > 0) \<or> (j \<noteq> 0 \<and> ?c < 0)"
by arith
moreover
{
assume "j = 0"
- then have z: "zlfm (NDvd j a) = (zlfm (NEq a))"
+ then have z: "zlfm (NDvd j a) = zlfm (NEq a)"
by (simp add: Let_def)
then have ?case
using assms 12 `j = 0` by (simp del: zlfm.simps)
@@ -1484,17 +1501,17 @@
lemma minusinf_inf:
assumes linp: "iszlfm p"
and u: "d_\<beta> p 1"
- shows "\<exists>(z::int). \<forall>x < z. Ifm bbs (x#bs) (minusinf p) = Ifm bbs (x#bs) p"
+ shows "\<exists>z::int. \<forall>x < z. Ifm bbs (x # bs) (minusinf p) = Ifm bbs (x # bs) p"
(is "?P p" is "\<exists>(z::int). \<forall>x < z. ?I x (?M p) = ?I x p")
using linp u
proof (induct p rule: minusinf.induct)
case (1 p q)
then show ?case
- by auto (rule_tac x="min z za" in exI, simp)
+ by auto (rule_tac x = "min z za" in exI, simp)
next
case (2 p q)
then show ?case
- by auto (rule_tac x="min z za" in exI, simp)
+ by auto (rule_tac x = "min z za" in exI, simp)
next
case (3 c e)
then have c1: "c = 1" and nb: "numbound0 e"
@@ -1513,10 +1530,10 @@
then have c1: "c = 1" and nb: "numbound0 e"
by simp_all
fix a
- from 4 have "\<forall>x < (- Inum (a#bs) e). c*x + Inum (x#bs) e \<noteq> 0"
+ from 4 have "\<forall>x < (- Inum (a # bs) e). c * x + Inum (x # bs) e \<noteq> 0"
proof clarsimp
fix x
- assume "x < (- Inum (a#bs) e)" and"x + Inum (x # bs) e = 0"
+ assume "x < (- Inum (a # bs) e)" and "x + Inum (x # bs) e = 0"
with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
show "False" by simp
qed
@@ -1526,10 +1543,10 @@
then have c1: "c = 1" and nb: "numbound0 e"
by simp_all
fix a
- from 5 have "\<forall>x<(- Inum (a#bs) e). c*x + Inum (x#bs) e < 0"
+ from 5 have "\<forall>x<(- Inum (a # bs) e). c*x + Inum (x # bs) e < 0"
proof clarsimp
fix x
- assume "x < (- Inum (a#bs) e)"
+ assume "x < (- Inum (a # bs) e)"
with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
show "x + Inum (x # bs) e < 0"
by simp
@@ -1540,12 +1557,12 @@
then have c1: "c = 1" and nb: "numbound0 e"
by simp_all
fix a
- from 6 have "\<forall>x<(- Inum (a#bs) e). c*x + Inum (x#bs) e \<le> 0"
+ from 6 have "\<forall>x<(- Inum (a # bs) e). c * x + Inum (x # bs) e \<le> 0"
proof clarsimp
fix x
- assume "x < (- Inum (a#bs) e)"
+ assume "x < (- Inum (a # bs) e)"
with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
- show "x + Inum (x#bs) e \<le> 0" by simp
+ show "x + Inum (x # bs) e \<le> 0" by simp
qed
then show ?case by auto
next
@@ -1553,10 +1570,10 @@
then have c1: "c = 1" and nb: "numbound0 e"
by simp_all
fix a
- from 7 have "\<forall>x<(- Inum (a#bs) e). \<not> (c*x + Inum (x#bs) e > 0)"
+ from 7 have "\<forall>x<(- Inum (a # bs) e). \<not> (c * x + Inum (x # bs) e > 0)"
proof clarsimp
fix x
- assume "x < (- Inum (a#bs) e)" and"x + Inum (x#bs) e > 0"
+ assume "x < - Inum (a # bs) e" and "x + Inum (x # bs) e > 0"
with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
show False by simp
qed
@@ -1596,23 +1613,23 @@
(is "?ri dvd ?rc*?rx - ?rc*(?rk*?rd) + ?I x e" is "?ri dvd ?rt")
then have "\<exists>l::int. ?rt = i * l"
by (simp add: dvd_def)
- then have "\<exists>l::int. c*x+ ?I x e = i * l + c * (k * i * di)"
+ then have "\<exists>l::int. c * x + ?I x e = i * l + c * (k * i * di)"
by (simp add: algebra_simps di_def)
- then have "\<exists>l::int. c*x+ ?I x e = i*(l + c * k * di)"
+ then have "\<exists>l::int. c * x + ?I x e = i* (l + c * k * di)"
by (simp add: algebra_simps)
then have "\<exists>l::int. c * x + ?I x e = i * l"
by blast
then show "i dvd c * x + Inum (x # bs) e"
by (simp add: dvd_def)
next
- assume "i dvd c*x + Inum (x # bs) e" (is "?ri dvd ?rc * ?rx + ?e")
+ assume "i dvd c * x + Inum (x # bs) e" (is "?ri dvd ?rc * ?rx + ?e")
then have "\<exists>l::int. c * x + ?e = i * l"
by (simp add: dvd_def)
then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * l - c * (k * d)"
by simp
then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * l - c * (k * i * di)"
by (simp add: di_def)
- then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * ((l - c * k * di))"
+ then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * (l - c * k * di)"
by (simp add: algebra_simps)
then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * l"
by blast
@@ -1660,7 +1677,7 @@
lemma mirror_\<alpha>_\<beta>:
assumes lp: "iszlfm p"
- shows "(Inum (i#bs)) ` set (\<alpha> p) = (Inum (i#bs)) ` set (\<beta> (mirror p))"
+ shows "Inum (i # bs) ` set (\<alpha> p) = Inum (i # bs) ` set (\<beta> (mirror p))"
using lp by (induct p rule: mirror.induct) auto
lemma mirror:
@@ -1669,27 +1686,30 @@
using lp
proof (induct p rule: iszlfm.induct)
case (9 j c e)
- then have nb: "numbound0 e" by simp
- have "Ifm bbs (x#bs) (mirror (Dvd j (CN 0 c e))) = (j dvd c*x - Inum (x#bs) e)"
+ then have nb: "numbound0 e"
+ by simp
+ have "Ifm bbs (x # bs) (mirror (Dvd j (CN 0 c e))) \<longleftrightarrow> j dvd c * x - Inum (x # bs) e"
(is "_ = (j dvd c*x - ?e)") by simp
- also have "\<dots> = (j dvd (- (c*x - ?e)))"
+ also have "\<dots> \<longleftrightarrow> j dvd (- (c * x - ?e))"
by (simp only: dvd_minus_iff)
- also have "\<dots> = (j dvd (c* (- x)) + ?e)"
+ also have "\<dots> \<longleftrightarrow> j dvd (c * (- x)) + ?e"
by (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] add_ac minus_add_distrib)
(simp add: algebra_simps)
- also have "\<dots> = Ifm bbs ((- x)#bs) (Dvd j (CN 0 c e))"
+ also have "\<dots> = Ifm bbs ((- x) # bs) (Dvd j (CN 0 c e))"
using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"] by simp
finally show ?case .
next
- case (10 j c e) then have nb: "numbound0 e" by simp
- have "Ifm bbs (x#bs) (mirror (Dvd j (CN 0 c e))) = (j dvd c*x - Inum (x#bs) e)"
- (is "_ = (j dvd c*x - ?e)") by simp
- also have "\<dots> = (j dvd (- (c*x - ?e)))"
+ case (10 j c e)
+ then have nb: "numbound0 e"
+ by simp
+ have "Ifm bbs (x # bs) (mirror (Dvd j (CN 0 c e))) \<longleftrightarrow> j dvd c * x - Inum (x # bs) e"
+ (is "_ = (j dvd c * x - ?e)") by simp
+ also have "\<dots> \<longleftrightarrow> j dvd (- (c * x - ?e))"
by (simp only: dvd_minus_iff)
- also have "\<dots> = (j dvd (c* (- x)) + ?e)"
+ also have "\<dots> \<longleftrightarrow> j dvd (c * (- x)) + ?e"
by (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] add_ac minus_add_distrib)
(simp add: algebra_simps)
- also have "\<dots> = Ifm bbs ((- x)#bs) (Dvd j (CN 0 c e))"
+ also have "\<dots> \<longleftrightarrow> Ifm bbs ((- x) # bs) (Dvd j (CN 0 c e))"
using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"] by simp
finally show ?case by simp
qed (auto simp add: numbound0_I[where bs="bs" and b="x" and b'="- x"] gr0_conv_Suc)
@@ -1702,7 +1722,7 @@
lemma \<beta>_numbound0:
assumes lp: "iszlfm p"
- shows "\<forall>b\<in> set (\<beta> p). numbound0 b"
+ shows "\<forall>b \<in> set (\<beta> p). numbound0 b"
using lp by (induct p rule: \<beta>.induct) auto
lemma d_\<beta>_mono:
@@ -1724,29 +1744,37 @@
using linp
proof (induct p rule: iszlfm.induct)
case (1 p q)
- from 1 have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp
- from 1 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp
+ from 1 have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)"
+ by simp
+ from 1 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)"
+ by simp
from 1 d_\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"]
- d_\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"]
- dl1 dl2 show ?case by (auto simp add: lcm_pos_int)
+ d_\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"]
+ dl1 dl2
+ show ?case
+ by (auto simp add: lcm_pos_int)
next
case (2 p q)
- from 2 have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp
- from 2 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp
+ from 2 have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)"
+ by simp
+ from 2 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)"
+ by simp
from 2 d_\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"]
- d_\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"]
- dl1 dl2 show ?case by (auto simp add: lcm_pos_int)
+ d_\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"]
+ dl1 dl2
+ show ?case
+ by (auto simp add: lcm_pos_int)
qed (auto simp add: lcm_pos_int)
lemma a_\<beta>:
assumes linp: "iszlfm p"
and d: "d_\<beta> p l"
and lp: "l > 0"
- shows "iszlfm (a_\<beta> p l) \<and> d_\<beta> (a_\<beta> p l) 1 \<and> (Ifm bbs (l*x #bs) (a_\<beta> p l) = Ifm bbs (x#bs) p)"
+ shows "iszlfm (a_\<beta> p l) \<and> d_\<beta> (a_\<beta> p l) 1 \<and> Ifm bbs (l * x # bs) (a_\<beta> p l) = Ifm bbs (x # bs) p"
using linp d
proof (induct p rule: iszlfm.induct)
case (5 c e)
- then have cp: "c>0" and be: "numbound0 e" and d': "c dvd l"
+ then have cp: "c > 0" and be: "numbound0 e" and d': "c dvd l"
by simp_all
from lp cp have clel: "c \<le> l"
by (simp add: zdvd_imp_le [OF d' lp])
@@ -1760,15 +1788,17 @@
using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
then have cl: "c * (l div c) =l"
using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp
- then have "(l*x + (l div c) * Inum (x # bs) e < 0) =
+ then have "(l * x + (l div c) * Inum (x # bs) e < 0) \<longleftrightarrow>
((c * (l div c)) * x + (l div c) * Inum (x # bs) e < 0)"
by simp
- also have "\<dots> = ((l div c) * (c*x + Inum (x # bs) e) < (l div c) * 0)"
+ also have "\<dots> \<longleftrightarrow> (l div c) * (c*x + Inum (x # bs) e) < (l div c) * 0"
by (simp add: algebra_simps)
- also have "\<dots> = (c*x + Inum (x # bs) e < 0)"
- using mult_less_0_iff [where a="(l div c)" and b="c*x + Inum (x # bs) e"] ldcp by simp
+ also have "\<dots> \<longleftrightarrow> c * x + Inum (x # bs) e < 0"
+ using mult_less_0_iff [where a="(l div c)" and b="c*x + Inum (x # bs) e"] ldcp
+ by simp
finally show ?case
- using numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"] be by simp
+ using numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"] be
+ by simp
next
case (6 c e)
then have cp: "c > 0" and be: "numbound0 e" and d': "c dvd l"
@@ -1777,20 +1807,20 @@
by (simp add: zdvd_imp_le [OF d' lp])
from cp have cnz: "c \<noteq> 0"
by simp
- have "c div c\<le> l div c"
+ have "c div c \<le> l div c"
by (simp add: zdiv_mono1[OF clel cp])
then have ldcp:"0 < l div c"
by (simp add: div_self[OF cnz])
- have "c * (l div c) = c* (l div c) + l mod c"
+ have "c * (l div c) = c * (l div c) + l mod c"
using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
then have cl: "c * (l div c) = l"
using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp
- then have "(l*x + (l div c) * Inum (x# bs) e \<le> 0) =
- ((c * (l div c)) * x + (l div c) * Inum (x # bs) e \<le> 0)"
+ then have "l * x + (l div c) * Inum (x # bs) e \<le> 0 \<longleftrightarrow>
+ (c * (l div c)) * x + (l div c) * Inum (x # bs) e \<le> 0"
by simp
- also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) \<le> ((l div c)) * 0)"
+ also have "\<dots> \<longleftrightarrow> (l div c) * (c * x + Inum (x # bs) e) \<le> (l div c) * 0"
by (simp add: algebra_simps)
- also have "\<dots> = (c*x + Inum (x # bs) e \<le> 0)"
+ also have "\<dots> \<longleftrightarrow> c * x + Inum (x # bs) e \<le> 0"
using mult_le_0_iff [where a="(l div c)" and b="c*x + Inum (x # bs) e"] ldcp by simp
finally show ?case
using numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"] be by simp
@@ -1804,18 +1834,18 @@
by simp
have "c div c \<le> l div c"
by (simp add: zdiv_mono1[OF clel cp])
- then have ldcp:"0 < l div c"
+ then have ldcp: "0 < l div c"
by (simp add: div_self[OF cnz])
- have "c * (l div c) = c* (l div c) + l mod c"
+ have "c * (l div c) = c * (l div c) + l mod c"
using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
- then have cl:"c * (l div c) = l"
+ then have cl: "c * (l div c) = l"
using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp
- then have "(l * x + (l div c) * Inum (x # bs) e > 0) =
- ((c * (l div c)) * x + (l div c) * Inum (x # bs) e > 0)"
+ then have "l * x + (l div c) * Inum (x # bs) e > 0 \<longleftrightarrow>
+ (c * (l div c)) * x + (l div c) * Inum (x # bs) e > 0"
by simp
- also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) > ((l div c)) * 0)"
+ also have "\<dots> \<longleftrightarrow> (l div c) * (c * x + Inum (x # bs) e) > (l div c) * 0"
by (simp add: algebra_simps)
- also have "\<dots> = (c * x + Inum (x # bs) e > 0)"
+ also have "\<dots> \<longleftrightarrow> c * x + Inum (x # bs) e > 0"
using zero_less_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp
by simp
finally show ?case
@@ -1833,17 +1863,17 @@
by (simp add: zdiv_mono1[OF clel cp])
then have ldcp: "0 < l div c"
by (simp add: div_self[OF cnz])
- have "c * (l div c) = c* (l div c) + l mod c"
+ have "c * (l div c) = c * (l div c) + l mod c"
using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
then have cl: "c * (l div c) =l"
using zmod_zdiv_equality[where a="l" and b="c", symmetric]
by simp
- then have "(l*x + (l div c)* Inum (x # bs) e \<ge> 0) =
- ((c*(l div c))*x + (l div c)* Inum (x # bs) e \<ge> 0)"
+ then have "l * x + (l div c) * Inum (x # bs) e \<ge> 0 \<longleftrightarrow>
+ (c * (l div c)) * x + (l div c) * Inum (x # bs) e \<ge> 0"
by simp
- also have "\<dots> = ((l div c)*(c*x + Inum (x # bs) e) \<ge> ((l div c)) * 0)"
+ also have "\<dots> \<longleftrightarrow> (l div c) * (c * x + Inum (x # bs) e) \<ge> (l div c) * 0"
by (simp add: algebra_simps)
- also have "\<dots> = (c*x + Inum (x # bs) e \<ge> 0)"
+ also have "\<dots> \<longleftrightarrow> c * x + Inum (x # bs) e \<ge> 0"
using ldcp zero_le_mult_iff [where a="l div c" and b="c*x + Inum (x # bs) e"]
by simp
finally show ?case
@@ -1861,16 +1891,16 @@
by (simp add: zdiv_mono1[OF clel cp])
then have ldcp:"0 < l div c"
by (simp add: div_self[OF cnz])
- have "c * (l div c) = c* (l div c) + l mod c"
+ have "c * (l div c) = c * (l div c) + l mod c"
using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
then have cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
by simp
- then have "(l * x + (l div c) * Inum (x # bs) e = 0) =
- ((c * (l div c)) * x + (l div c) * Inum (x # bs) e = 0)"
+ then have "l * x + (l div c) * Inum (x # bs) e = 0 \<longleftrightarrow>
+ (c * (l div c)) * x + (l div c) * Inum (x # bs) e = 0"
by simp
- also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) = ((l div c)) * 0)"
+ also have "\<dots> \<longleftrightarrow> (l div c) * (c * x + Inum (x # bs) e) = ((l div c)) * 0"
by (simp add: algebra_simps)
- also have "\<dots> = (c * x + Inum (x # bs) e = 0)"
+ also have "\<dots> \<longleftrightarrow> c * x + Inum (x # bs) e = 0"
using mult_eq_0_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp
by simp
finally show ?case
@@ -1888,11 +1918,11 @@
by (simp add: zdiv_mono1[OF clel cp])
then have ldcp:"0 < l div c"
by (simp add: div_self[OF cnz])
- have "c * (l div c) = c* (l div c) + l mod c"
+ have "c * (l div c) = c * (l div c) + l mod c"
using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
then have cl: "c * (l div c) = l"
using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp
- then have "(l * x + (l div c) * Inum (x # bs) e \<noteq> 0) \<longleftrightarrow>
+ then have "l * x + (l div c) * Inum (x # bs) e \<noteq> 0 \<longleftrightarrow>
(c * (l div c)) * x + (l div c) * Inum (x # bs) e \<noteq> 0"
by simp
also have "\<dots> \<longleftrightarrow> (l div c) * (c * x + Inum (x # bs) e) \<noteq> (l div c) * 0"
@@ -1914,14 +1944,14 @@
by (simp add: zdiv_mono1[OF clel cp])
then have ldcp:"0 < l div c"
by (simp add: div_self[OF cnz])
- have "c * (l div c) = c* (l div c) + l mod c"
+ have "c * (l div c) = c * (l div c) + l mod c"
using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
then have cl: "c * (l div c) = l"
using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp
then have "(\<exists>k::int. l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) \<longleftrightarrow>
- (\<exists>(k::int). (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)"
+ (\<exists>k::int. (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)"
by simp
- also have "\<dots> \<longleftrightarrow> (\<exists>(k::int). (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c) * 0)"
+ also have "\<dots> \<longleftrightarrow> (\<exists>k::int. (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c) * 0)"
by (simp add: algebra_simps)
also
fix k
@@ -1958,10 +1988,10 @@
by (simp add: algebra_simps)
also
fix k
- have "\<dots> = (\<exists>k::int. c * x + Inum (x # bs) e - j * k = 0)"
+ have "\<dots> \<longleftrightarrow> (\<exists>k::int. c * x + Inum (x # bs) e - j * k = 0)"
using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e - j * k"] ldcp
by simp
- also have "\<dots> = (\<exists>k::int. c * x + Inum (x # bs) e = j * k)"
+ also have "\<dots> \<longleftrightarrow> (\<exists>k::int. c * x + Inum (x # bs) e = j * k)"
by simp
finally show ?case
using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be
@@ -1988,15 +2018,15 @@
and u: "d_\<beta> p 1"
and d: "d_\<delta> p d"
and dp: "d > 0"
- and nob: "\<not>(\<exists>(j::int) \<in> {1 .. d}. \<exists>b\<in> (Inum (a#bs)) ` set(\<beta> p). x = b + j)"
- and p: "Ifm bbs (x#bs) p" (is "?P x")
+ and nob: "\<not> (\<exists>j::int \<in> {1 .. d}. \<exists>b \<in> Inum (a # bs) ` set (\<beta> p). x = b + j)"
+ and p: "Ifm bbs (x # bs) p" (is "?P x")
shows "?P (x - d)"
using lp u d dp nob p
proof (induct p rule: iszlfm.induct)
case (5 c e)
then have c1: "c = 1" and bn: "numbound0 e"
by simp_all
- with dp p c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] 5
+ with dp p c1 numbound0_I[OF bn,where b = "(x - d)" and b' = "x" and bs = "bs"] 5
show ?case by simp
next
case (6 c e)
@@ -2006,29 +2036,30 @@
show ?case by simp
next
case (7 c e)
- then have p: "Ifm bbs (x #bs) (Gt (CN 0 c e))" and c1: "c=1" and bn: "numbound0 e"
+ then have p: "Ifm bbs (x # bs) (Gt (CN 0 c e))" and c1: "c=1" and bn: "numbound0 e"
by simp_all
let ?e = "Inum (x # bs) e"
{
- assume "(x-d) +?e > 0"
+ assume "(x - d) + ?e > 0"
then have ?case
using c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] by simp
}
moreover
{
- assume H: "\<not> (x-d) + ?e > 0"
- let ?v="Neg e"
- have vb: "?v \<in> set (\<beta> (Gt (CN 0 c e)))" by simp
+ assume H: "\<not> (x - d) + ?e > 0"
+ let ?v = "Neg e"
+ have vb: "?v \<in> set (\<beta> (Gt (CN 0 c e)))"
+ by simp
from 7(5)[simplified simp_thms Inum.simps \<beta>.simps set_simps bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]]
- have nob: "\<not> (\<exists>j\<in> {1 ..d}. x = - ?e + j)"
+ have nob: "\<not> (\<exists>j\<in> {1 ..d}. x = - ?e + j)"
by auto
from H p have "x + ?e > 0 \<and> x + ?e \<le> d"
by (simp add: c1)
then have "x + ?e \<ge> 1 \<and> x + ?e \<le> d"
by simp
- then have "\<exists>(j::int) \<in> {1 .. d}. j = x + ?e"
+ then have "\<exists>j::int \<in> {1 .. d}. j = x + ?e"
by simp
- then have "\<exists>(j::int) \<in> {1 .. d}. x = (- ?e + j)"
+ then have "\<exists>j::int \<in> {1 .. d}. x = (- ?e + j)"
by (simp add: algebra_simps)
with nob have ?case
by auto
@@ -2059,9 +2090,9 @@
by (simp add: c1)
then have "x + ?e +1 \<ge> 1 \<and> x + ?e + 1 \<le> d"
by simp
- then have "\<exists>(j::int) \<in> {1 .. d}. j = x + ?e + 1"
+ then have "\<exists>j::int \<in> {1 .. d}. j = x + ?e + 1"
by simp
- then have "\<exists>(j::int) \<in> {1 .. d}. x= - ?e - 1 + j"
+ then have "\<exists>j::int \<in> {1 .. d}. x= - ?e - 1 + j"
by (simp add: algebra_simps)
with nob have ?case
by simp
@@ -2072,35 +2103,38 @@
case (3 c e)
then
have p: "Ifm bbs (x #bs) (Eq (CN 0 c e))" (is "?p x")
- and c1: "c=1"
+ and c1: "c = 1"
and bn: "numbound0 e"
by simp_all
let ?e = "Inum (x # bs) e"
let ?v="(Sub (C -1) e)"
have vb: "?v \<in> set (\<beta> (Eq (CN 0 c e)))"
by simp
- from p have "x= - ?e" by (simp add: c1) with 3(5) show ?case
+ from p have "x= - ?e"
+ by (simp add: c1) with 3(5)
+ show ?case
using dp
by simp (erule ballE[where x="1"],
simp_all add:algebra_simps numbound0_I[OF bn,where b="x"and b'="a"and bs="bs"])
next
case (4 c e)
then
- have p: "Ifm bbs (x #bs) (NEq (CN 0 c e))" (is "?p x")
+ have p: "Ifm bbs (x # bs) (NEq (CN 0 c e))" (is "?p x")
and c1: "c = 1"
and bn: "numbound0 e"
by simp_all
let ?e = "Inum (x # bs) e"
let ?v="Neg e"
- have vb: "?v \<in> set (\<beta> (NEq (CN 0 c e)))" by simp
+ have vb: "?v \<in> set (\<beta> (NEq (CN 0 c e)))"
+ by simp
{
assume "x - d + Inum (((x -d)) # bs) e \<noteq> 0"
then have ?case by (simp add: c1)
}
moreover
{
- assume H: "x - d + Inum (((x -d)) # bs) e = 0"
- then have "x = - Inum (((x -d)) # bs) e + d"
+ assume H: "x - d + Inum ((x - d) # bs) e = 0"
+ then have "x = - Inum ((x - d) # bs) e + d"
by simp
then have "x = - Inum (a # bs) e + d"
by (simp add: numbound0_I[OF bn,where b="x - d"and b'="a"and bs="bs"])
@@ -2119,9 +2153,9 @@
let ?e = "Inum (x # bs) e"
from 9 have id: "j dvd d"
by simp
- from c1 have "?p x = (j dvd (x + ?e))"
+ from c1 have "?p x \<longleftrightarrow> j dvd (x + ?e)"
by simp
- also have "\<dots> = (j dvd x - d + ?e)"
+ also have "\<dots> \<longleftrightarrow> j dvd x - d + ?e"
using zdvd_period[OF id, where x="x" and c="-1" and t="?e"]
by simp
finally show ?case
@@ -2130,16 +2164,16 @@
next
case (10 j c e)
then
- have p: "Ifm bbs (x #bs) (NDvd j (CN 0 c e))" (is "?p x")
+ have p: "Ifm bbs (x # bs) (NDvd j (CN 0 c e))" (is "?p x")
and c1: "c = 1"
and bn: "numbound0 e"
by simp_all
let ?e = "Inum (x # bs) e"
from 10 have id: "j dvd d"
by simp
- from c1 have "?p x = (\<not> j dvd (x + ?e))"
+ from c1 have "?p x \<longleftrightarrow> \<not> j dvd (x + ?e)"
by simp
- also have "\<dots> = (\<not> j dvd x - d + ?e)"
+ also have "\<dots> \<longleftrightarrow> \<not> j dvd x - d + ?e"
using zdvd_period[OF id, where x="x" and c="-1" and t="?e"]
by simp
finally show ?case
@@ -2152,13 +2186,13 @@
and u: "d_\<beta> p 1"
and d: "d_\<delta> p d"
and dp: "d > 0"
- shows "\<forall>x. \<not> (\<exists>(j::int) \<in> {1 .. d}. \<exists>b\<in> set(\<beta> p). Ifm bbs ((Inum (a#bs) b + j) #bs) p) \<longrightarrow>
- Ifm bbs (x#bs) p \<longrightarrow> Ifm bbs ((x - d)#bs) p" (is "\<forall>x. ?b \<longrightarrow> ?P x \<longrightarrow> ?P (x - d)")
+ shows "\<forall>x. \<not> (\<exists>j::int \<in> {1 .. d}. \<exists>b \<in> set(\<beta> p). Ifm bbs ((Inum (a#bs) b + j) #bs) p) \<longrightarrow>
+ Ifm bbs (x # bs) p \<longrightarrow> Ifm bbs ((x - d) # bs) p" (is "\<forall>x. ?b \<longrightarrow> ?P x \<longrightarrow> ?P (x - d)")
proof clarify
fix x
assume nb: "?b"
and px: "?P x"
- then have nb2: "\<not>(\<exists>(j::int) \<in> {1 .. d}. \<exists>b\<in> (Inum (a#bs)) ` set(\<beta> p). x = b + j)"
+ then have nb2: "\<not> (\<exists>j::int \<in> {1 .. d}. \<exists>b \<in> Inum (a # bs) ` set (\<beta> p). x = b + j)"
by auto
from \<beta>[OF lp u d dp nb2 px] show "?P (x -d )" .
qed
@@ -2191,16 +2225,18 @@
and u: "d_\<beta> p 1"
and d: "d_\<delta> p d"
and dp: "d > 0"
- shows "(\<exists>(x::int). Ifm bbs (x #bs) p) = (\<exists>j\<in> {1.. d}. Ifm bbs (j #bs) (minusinf p) \<or> (\<exists>b \<in> set (\<beta> p). Ifm bbs ((Inum (i#bs) b + j) #bs) p))"
+ shows "(\<exists>(x::int). Ifm bbs (x # bs) p) \<longleftrightarrow>
+ (\<exists>j \<in> {1.. d}. Ifm bbs (j # bs) (minusinf p) \<or>
+ (\<exists>b \<in> set (\<beta> p). Ifm bbs ((Inum (i # bs) b + j) # bs) p))"
(is "(\<exists>(x::int). ?P (x)) = (\<exists>j\<in> ?D. ?M j \<or> (\<exists>b\<in> ?B. ?P (?I b + j)))")
proof -
from minusinf_inf[OF lp u]
- have th: "\<exists>(z::int). \<forall>x<z. ?P (x) = ?M x"
+ have th: "\<exists>z::int. \<forall>x<z. ?P (x) = ?M x"
by blast
- let ?B' = "{?I b | b. b\<in> ?B}"
- have BB': "(\<exists>j\<in>?D. \<exists>b\<in> ?B. ?P (?I b +j)) = (\<exists>j \<in> ?D. \<exists>b \<in> ?B'. ?P (b + j))"
+ let ?B' = "{?I b | b. b \<in> ?B}"
+ have BB': "(\<exists>j\<in>?D. \<exists>b \<in> ?B. ?P (?I b + j)) \<longleftrightarrow> (\<exists>j \<in> ?D. \<exists>b \<in> ?B'. ?P (b + j))"
by auto
- then have th2: "\<forall>x. \<not> (\<exists>j \<in> ?D. \<exists>b \<in> ?B'. ?P ((b + j))) \<longrightarrow> ?P (x) \<longrightarrow> ?P ((x - d))"
+ then have th2: "\<forall>x. \<not> (\<exists>j \<in> ?D. \<exists>b \<in> ?B'. ?P (b + j)) \<longrightarrow> ?P x \<longrightarrow> ?P (x - d)"
using \<beta>'[OF lp u d dp, where a="i" and bbs = "bbs"] by blast
from minusinf_repeats[OF d lp]
have th3: "\<forall>x k. ?M x = ?M (x-k*d)"
@@ -2214,31 +2250,50 @@
assumes lp: "iszlfm p"
shows "(\<exists>x. Ifm bbs (x#bs) (mirror p)) = (\<exists>x. Ifm bbs (x#bs) p)"
(is "(\<exists>x. ?I x ?mp) = (\<exists>x. ?I x p)")
-proof(auto)
- fix x assume "?I x ?mp" then have "?I (- x) p" using mirror[OF lp] by blast
- then show "\<exists>x. ?I x p" by blast
+proof auto
+ fix x
+ assume "?I x ?mp"
+ then have "?I (- x) p"
+ using mirror[OF lp] by blast
+ then show "\<exists>x. ?I x p"
+ by blast
next
- fix x assume "?I x p" then have "?I (- x) ?mp"
+ fix x
+ assume "?I x p"
+ then have "?I (- x) ?mp"
using mirror[OF lp, where x="- x", symmetric] by auto
- then show "\<exists>x. ?I x ?mp" by blast
+ then show "\<exists>x. ?I x ?mp"
+ by blast
qed
-
lemma cp_thm':
assumes lp: "iszlfm p"
- and up: "d_\<beta> p 1" and dd: "d_\<delta> p d" and dp: "d > 0"
- shows "(\<exists>x. Ifm bbs (x#bs) p) = ((\<exists>j\<in> {1 .. d}. Ifm bbs (j#bs) (minusinf p)) \<or> (\<exists>j\<in> {1.. d}. \<exists>b\<in> (Inum (i#bs)) ` set (\<beta> p). Ifm bbs ((b+j)#bs) p))"
+ and up: "d_\<beta> p 1"
+ and dd: "d_\<delta> p d"
+ and dp: "d > 0"
+ shows "(\<exists>x. Ifm bbs (x # bs) p) \<longleftrightarrow>
+ ((\<exists>j\<in> {1 .. d}. Ifm bbs (j#bs) (minusinf p)) \<or>
+ (\<exists>j\<in> {1.. d}. \<exists>b\<in> (Inum (i#bs)) ` set (\<beta> p). Ifm bbs ((b + j) # bs) p))"
using cp_thm[OF lp up dd dp,where i="i"] by auto
definition unit :: "fm \<Rightarrow> fm \<times> num list \<times> int"
where
- "unit p = (let p' = zlfm p ; l = \<zeta> p' ; q = And (Dvd l (CN 0 1 (C 0))) (a_\<beta> p' l); d = \<delta> q;
- B = remdups (map simpnum (\<beta> q)) ; a = remdups (map simpnum (\<alpha> q))
- in if length B \<le> length a then (q,B,d) else (mirror q, a,d))"
+ "unit p =
+ (let
+ p' = zlfm p;
+ l = \<zeta> p';
+ q = And (Dvd l (CN 0 1 (C 0))) (a_\<beta> p' l);
+ d = \<delta> q;
+ B = remdups (map simpnum (\<beta> q));
+ a = remdups (map simpnum (\<alpha> q))
+ in if length B \<le> length a then (q, B, d) else (mirror q, a, d))"
lemma unit:
assumes qf: "qfree p"
- shows "\<And>q B d. unit p = (q,B,d) \<Longrightarrow> ((\<exists>x. Ifm bbs (x#bs) p) = (\<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> d >0 \<and> iszlfm q \<and> (\<forall>b\<in> set B. numbound0 b)"
+ shows "\<And>q B d. unit p = (q, B, d) \<Longrightarrow>
+ ((\<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> d > 0 \<and>
+ iszlfm q \<and> (\<forall>b\<in> set B. numbound0 b)"
proof -
fix q B d
assume qBd: "unit p = (q,B,d)"
--- a/src/HOL/Library/LaTeXsugar.thy Thu Mar 06 17:55:39 2014 +0100
+++ b/src/HOL/Library/LaTeXsugar.thy Thu Mar 06 22:15:01 2014 +0100
@@ -100,7 +100,7 @@
setup{*
let
fun pretty ctxt c =
- let val tc = Proof_Context.read_const_proper ctxt false c
+ let val tc = Proof_Context.read_const ctxt {proper = true, strict = false} c
in Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::",
Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]
end
--- a/src/HOL/Nominal/nominal_fresh_fun.ML Thu Mar 06 17:55:39 2014 +0100
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML Thu Mar 06 22:15:01 2014 +0100
@@ -185,7 +185,7 @@
(Scan.succeed false);
fun setup_generate_fresh x =
- (Args.goal_spec -- Args.type_name true >>
+ (Args.goal_spec -- Args.type_name {proper = true, strict = true} >>
(fn (quant, s) => K (SIMPLE_METHOD'' quant (generate_fresh_tac s)))) x;
fun setup_fresh_fun_simp x =
--- a/src/HOL/Nominal/nominal_induct.ML Thu Mar 06 17:55:39 2014 +0100
+++ b/src/HOL/Nominal/nominal_induct.ML Thu Mar 06 22:15:01 2014 +0100
@@ -63,7 +63,7 @@
let
val tune =
if internal then Name.internal
- else fn x => the_default x (try Name.dest_internal x);
+ else perhaps (try Name.dest_internal);
val n = length xs;
fun rename prem =
let
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Thu Mar 06 17:55:39 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Thu Mar 06 22:15:01 2014 +0100
@@ -33,7 +33,8 @@
error ("{" ^ commas ss ^ "} is not a complete set of mutually recursive new-style datatypes");
val fpT_names =
- map (fst o dest_Type o Proof_Context.read_type_name_proper lthy false) raw_fpT_names;
+ map (fst o dest_Type o Proof_Context.read_type_name lthy {proper = true, strict = false})
+ raw_fpT_names;
fun lfp_sugar_of s =
(case fp_sugar_of lthy s of
--- a/src/HOL/Tools/Datatype/datatype_data.ML Thu Mar 06 17:55:39 2014 +0100
+++ b/src/HOL/Tools/Datatype/datatype_data.ML Thu Mar 06 22:15:01 2014 +0100
@@ -234,7 +234,7 @@
(** document antiquotation **)
val antiq_setup =
- Thy_Output.antiquotation @{binding datatype} (Args.type_name true)
+ Thy_Output.antiquotation @{binding datatype} (Args.type_name {proper = true, strict = true})
(fn {source = src, context = ctxt, ...} => fn dtco =>
let
val thy = Proof_Context.theory_of ctxt;
--- a/src/HOL/Tools/Datatype/rep_datatype.ML Thu Mar 06 17:55:39 2014 +0100
+++ b/src/HOL/Tools/Datatype/rep_datatype.ML Thu Mar 06 22:15:01 2014 +0100
@@ -534,10 +534,11 @@
(drop (length dt_names) inducts);
val ctxt = Proof_Context.init_global thy9;
- val case_combs = map (Proof_Context.read_const ctxt false dummyT) case_names;
+ val case_combs =
+ map (Proof_Context.read_const ctxt {proper = true, strict = true}) case_names;
val constrss = map (fn (dtname, {descr, index, ...}) =>
- map (Proof_Context.read_const ctxt false dummyT o fst)
- (#3 (the (AList.lookup op = descr index)))) dt_infos
+ map (Proof_Context.read_const ctxt {proper = true, strict = true} o fst)
+ (#3 (the (AList.lookup op = descr index)))) dt_infos;
in
thy9
|> Global_Theory.note_thmss ""
--- a/src/HOL/Tools/Quickcheck/abstract_generators.ML Thu Mar 06 17:55:39 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/abstract_generators.ML Thu Mar 06 22:15:01 2014 +0100
@@ -61,8 +61,10 @@
val quickcheck_generator = gen_quickcheck_generator (K I) (K I)
-val quickcheck_generator_cmd = gen_quickcheck_generator
- (fn ctxt => fst o dest_Type o Proof_Context.read_type_name_proper ctxt false) Syntax.read_term
+val quickcheck_generator_cmd =
+ gen_quickcheck_generator
+ (fn ctxt => fst o dest_Type o Proof_Context.read_type_name ctxt {proper = true, strict = true})
+ Syntax.read_term
val _ =
Outer_Syntax.command @{command_spec "quickcheck_generator"}
--- a/src/HOL/Tools/Quotient/quotient_info.ML Thu Mar 06 17:55:39 2014 +0100
+++ b/src/HOL/Tools/Quotient/quotient_info.ML Thu Mar 06 22:15:01 2014 +0100
@@ -71,8 +71,9 @@
val quotmaps_attribute_setup =
Attrib.setup @{binding mapQ3}
- ((Args.type_name true --| Scan.lift @{keyword "="}) --
- (Scan.lift @{keyword "("} |-- Args.const_proper true --| Scan.lift @{keyword ","} --
+ ((Args.type_name {proper = true, strict = true} --| Scan.lift @{keyword "="}) --
+ (Scan.lift @{keyword "("} |--
+ Args.const {proper = true, strict = true} --| Scan.lift @{keyword ","} --
Attrib.thm --| Scan.lift @{keyword ")"}) >>
(fn (tyname, (relname, qthm)) =>
let val minfo = {relmap = relname, quot_thm = qthm}
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Thu Mar 06 17:55:39 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Thu Mar 06 22:15:01 2014 +0100
@@ -430,7 +430,7 @@
| NONE => [ax])
fun external_frees t =
- [] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst)
+ [] |> Term.add_frees t |> filter_out (Name.is_internal o fst)
fun maybe_instantiate_inducts ctxt hyp_ts concl_t =
if Config.get ctxt instantiate_inducts then
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Mar 06 17:55:39 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Mar 06 22:15:01 2014 +0100
@@ -144,7 +144,7 @@
val do_preplay = preplay_timeout <> Time.zeroTime
val compress_isar = if isar_proofs = NONE andalso do_preplay then 1000.0 else compress_isar
- val is_fixed = Variable.is_declared ctxt orf can Name.dest_skolem
+ val is_fixed = Variable.is_declared ctxt orf Name.is_skolem
fun skolems_of t = Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev
fun get_role keep_role ((num, _), role, t, rule, _) =
--- a/src/HOL/Tools/coinduction.ML Thu Mar 06 17:55:39 2014 +0100
+++ b/src/HOL/Tools/coinduction.ML Thu Mar 06 22:15:01 2014 +0100
@@ -129,9 +129,9 @@
| NONE => error ("No rule for " ^ k ^ " " ^ quote name))))));
fun rule get_type get_pred =
- named_rule Induct.typeN (Args.type_name false) get_type ||
- named_rule Induct.predN (Args.const false) get_pred ||
- named_rule Induct.setN (Args.const false) get_pred ||
+ named_rule Induct.typeN (Args.type_name {proper = false, strict = false}) get_type ||
+ named_rule Induct.predN (Args.const {proper = false, strict = false}) get_pred ||
+ named_rule Induct.setN (Args.const {proper = false, strict = false}) get_pred ||
Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms;
val coinduct_rule = rule Induct.lookup_coinductT Induct.lookup_coinductP >> single_rule;
--- a/src/HOL/Tools/inductive_realizer.ML Thu Mar 06 17:55:39 2014 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Thu Mar 06 22:15:01 2014 +0100
@@ -515,7 +515,8 @@
val setup =
Attrib.setup @{binding ind_realizer}
((Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
- Scan.option (Scan.lift (Args.colon) |-- Scan.repeat1 (Args.const true)))) >> rlz_attrib)
+ Scan.option (Scan.lift (Args.colon) |--
+ Scan.repeat1 (Args.const {proper = true, strict = true})))) >> rlz_attrib)
"add realizers for inductive set";
end;
--- a/src/Pure/General/name_space.ML Thu Mar 06 17:55:39 2014 +0100
+++ b/src/Pure/General/name_space.ML Thu Mar 06 22:15:01 2014 +0100
@@ -56,7 +56,7 @@
val declare: Context.generic -> bool -> binding -> T -> string * T
type 'a table = T * 'a Symtab.table
val check_reports: Context.generic -> 'a table ->
- xstring * Position.T -> (string * Position.report list) * 'a
+ xstring * Position.T list -> (string * Position.report list) * 'a
val check: Context.generic -> 'a table -> xstring * Position.T -> string * 'a
val get: 'a table -> string -> 'a
val define: Context.generic -> bool -> binding * 'a -> 'a table -> string * 'a table
@@ -205,7 +205,7 @@
(* completion *)
fun completion context space (xname, pos) =
- if Context_Position.is_reported_generic context pos then
+ if Position.is_reported pos then
let
val x = Name.clean xname;
val Name_Space {kind = k, internals, ...} = space;
@@ -322,6 +322,8 @@
fun transform_binding (Naming {conceal = true, ...}) = Binding.conceal
| transform_binding _ = I;
+val bad_specs = ["", "??", "__"];
+
fun name_spec (naming as Naming {path, ...}) raw_binding =
let
val binding = transform_binding naming raw_binding;
@@ -332,7 +334,7 @@
val spec2 = if name = "" then [] else [(name, true)];
val spec = spec1 @ spec2;
val _ =
- exists (fn (a, _) => a = "" orelse a = "??" orelse exists_string (fn s => s = "\"") a) spec
+ exists (fn (a, _) => member (op =) bad_specs a orelse exists_string (fn s => s = "\"") a) spec
andalso err_bad binding;
in (concealed, if null spec2 then [] else spec) end;
@@ -446,24 +448,27 @@
type 'a table = T * 'a Symtab.table;
-fun check_reports context (space, tab) (xname, pos) =
+fun check_reports context (space, tab) (xname, ps) =
let val name = intern space xname in
(case Symtab.lookup tab name of
SOME x =>
let
val reports =
- if Context_Position.is_reported_generic context pos
- then [(pos, markup space name)] else [];
+ filter (Context_Position.is_reported_generic context) ps
+ |> map (fn pos => (pos, markup space name));
in ((name, reports), x) end
| NONE =>
- error (undefined (kind_of space) name ^ Position.here pos ^
- Markup.markup Markup.report
- (Completion.reported_text (completion context space (xname, pos)))))
+ let
+ val completions = map (fn pos => completion context space (xname, pos)) ps;
+ in
+ error (undefined (kind_of space) name ^ Position.here_list ps ^
+ Markup.markup_report (implode (map Completion.reported_text completions)))
+ end)
end;
-fun check context table arg =
+fun check context table (xname, pos) =
let
- val ((name, reports), x) = check_reports context table arg;
+ val ((name, reports), x) = check_reports context table (xname, [pos]);
val _ = Position.reports reports;
in (name, x) end;
--- a/src/Pure/General/position.ML Thu Mar 06 17:55:39 2014 +0100
+++ b/src/Pure/General/position.ML Thu Mar 06 22:15:01 2014 +0100
@@ -43,6 +43,7 @@
val reports: report list -> unit
val store_reports: report_text list Unsynchronized.ref ->
T list -> ('a -> Markup.T list) -> 'a -> unit
+ val append_reports: report_text list Unsynchronized.ref -> report list -> unit
val here: T -> string
val here_list: T list -> string
type range = T * T
@@ -182,6 +183,9 @@
let val ms = markup x
in Unsynchronized.change r (fold (fn p => fold (fn m => cons ((p, m), "")) ms) ps) end;
+fun append_reports (r: report_text list Unsynchronized.ref) reports =
+ Unsynchronized.change r (append (map (rpair "") reports));
+
(* here: inlined formal markup *)
--- a/src/Pure/Isar/args.ML Thu Mar 06 17:55:39 2014 +0100
+++ b/src/Pure/Isar/args.ML Thu Mar 06 22:15:01 2014 +0100
@@ -56,9 +56,8 @@
val term_pattern: term context_parser
val term_abbrev: term context_parser
val prop: term context_parser
- val type_name: bool -> string context_parser
- val const: bool -> string context_parser
- val const_proper: bool -> string context_parser
+ val type_name: {proper: bool, strict: bool} -> string context_parser
+ val const: {proper: bool, strict: bool} -> string context_parser
val goal_spec: ((int -> tactic) -> tactic) context_parser
val parse: Token.T list parser
val parse1: (string -> bool) -> Token.T list parser
@@ -208,18 +207,14 @@
(* type and constant names *)
-fun type_name strict =
- Scan.peek (fn ctxt => named_typ (Proof_Context.read_type_name (Context.proof_of ctxt) strict))
+fun type_name flags =
+ Scan.peek (fn ctxt => named_typ (Proof_Context.read_type_name (Context.proof_of ctxt) flags))
>> (fn Type (c, _) => c | TFree (a, _) => a | _ => "");
-fun const strict =
- Scan.peek (fn ctxt => named_term (Proof_Context.read_const (Context.proof_of ctxt) strict dummyT))
+fun const flags =
+ Scan.peek (fn ctxt => named_term (Proof_Context.read_const (Context.proof_of ctxt) flags))
>> (fn Const (c, _) => c | Free (x, _) => x | _ => "");
-fun const_proper strict =
- Scan.peek (fn ctxt => named_term (Proof_Context.read_const_proper (Context.proof_of ctxt) strict))
- >> (fn Const (c, _) => c | _ => "");
-
(* improper method arguments *)
@@ -304,7 +299,7 @@
| (_, (_, args2)) =>
error ("Bad arguments for " ^ kind ^ " " ^ quote s ^ Position.here pos ^
(if null args2 then "" else ":\n " ^ space_implode " " (map Token.print args2)) ^
- Markup.markup Markup.report (reported_text ())))
+ Markup.markup_report (reported_text ())))
end;
fun context_syntax kind scan src =
--- a/src/Pure/Isar/proof.ML Thu Mar 06 17:55:39 2014 +0100
+++ b/src/Pure/Isar/proof.ML Thu Mar 06 22:15:01 2014 +0100
@@ -575,13 +575,17 @@
#> map_context (fn ctxt => ctxt |> Proof_Context.notation true mode (map (prep_arg ctxt) args))
#> reset_facts;
+fun read_arg ctxt (c, mx) =
+ (case Proof_Context.read_const ctxt {proper = false, strict = false} c of
+ Free (x, _) =>
+ let val T = Proof_Context.infer_type ctxt (x, Mixfix.mixfixT mx)
+ in (Free (x, T), mx) end
+ | t => (t, mx));
+
in
val write = gen_write (K I);
-
-val write_cmd =
- gen_write (fn ctxt => fn (c, mx) =>
- (Proof_Context.read_const ctxt false (Mixfix.mixfixT mx) c, mx));
+val write_cmd = gen_write read_arg;
end;
--- a/src/Pure/Isar/proof_context.ML Thu Mar 06 17:55:39 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML Thu Mar 06 22:15:01 2014 +0100
@@ -68,21 +68,19 @@
val infer_type: Proof.context -> string * typ -> typ
val inferred_param: string -> Proof.context -> typ * Proof.context
val inferred_fixes: Proof.context -> (string * typ) list * Proof.context
- val check_type_name: Proof.context -> bool ->
- xstring * Position.T -> typ * Position.report list
- val check_type_name_proper: Proof.context -> bool ->
+ val check_type_name: Proof.context -> {proper: bool, strict: bool} ->
xstring * Position.T -> typ * Position.report list
- val read_type_name: Proof.context -> bool -> string -> typ
- val read_type_name_proper: Proof.context -> bool -> string -> typ
- val read_const_proper: Proof.context -> bool -> string -> term
- val read_const: Proof.context -> bool -> typ -> string -> term
+ val read_type_name: Proof.context -> {proper: bool, strict: bool} -> string -> typ
+ val consts_completion_message: Proof.context -> xstring * Position.T list -> string
+ val check_const: Proof.context -> {proper: bool, strict: bool} ->
+ xstring * Position.T list -> term * Position.report list
+ val read_const: Proof.context -> {proper: bool, strict: bool} -> string -> term
val read_arity: Proof.context -> xstring * string list * string -> arity
val cert_arity: Proof.context -> arity -> arity
val allow_dummies: Proof.context -> Proof.context
val prepare_sortsT: Proof.context -> typ list -> string * typ list
val prepare_sorts: Proof.context -> term list -> string * term list
val check_tfree: Proof.context -> string * sort -> string * sort
- val intern_skolem: Proof.context -> string -> string option
val read_term_pattern: Proof.context -> string -> term
val read_term_schematic: Proof.context -> string -> term
val read_term_abbrev: Proof.context -> string -> term
@@ -387,9 +385,8 @@
val name = Type.cert_class tsig (Type.intern_class tsig xname)
handle TYPE (msg, _, _) =>
error (msg ^ Position.here pos ^
- Markup.markup Markup.report
- (Completion.reported_text
- (Name_Space.completion (Context.Proof ctxt) class_space (xname, pos))));
+ Markup.markup_report (Completion.reported_text
+ (Name_Space.completion (Context.Proof ctxt) class_space (xname, pos))));
val reports =
if Context_Position.is_reported ctxt pos
then [(pos, Name_Space.markup class_space name)] else [];
@@ -422,19 +419,6 @@
-(** prepare variables **)
-
-(* check Skolem constants *)
-
-fun no_skolem internal x =
- if can Name.dest_skolem x then
- error ("Illegal reference to internal Skolem constant: " ^ quote x)
- else if not internal andalso can Name.dest_internal x then
- error ("Illegal reference to internal variable: " ^ quote x)
- else x;
-
-
-
(** prepare terms and propositions **)
(* inferred types of parameters *)
@@ -455,13 +439,15 @@
(* type names *)
-fun check_type_name ctxt strict (c, pos) =
+fun check_type_name ctxt {proper, strict} (c, pos) =
if Lexicon.is_tid c then
- let
- val reports =
- if Context_Position.is_reported ctxt pos
- then [(pos, Markup.tfree)] else [];
- in (TFree (c, default_sort ctxt (c, ~1)), reports) end
+ if proper then error ("Not a type constructor: " ^ c ^ Position.here pos)
+ else
+ let
+ val reports =
+ if Context_Position.is_reported ctxt pos
+ then [(pos, Markup.tfree)] else [];
+ in (TFree (c, default_sort ctxt (c, ~1)), reports) end
else
let
val ((d, reports), decl) = Type.check_decl (Context.Proof ctxt) (tsig_of ctxt) (c, pos);
@@ -473,59 +459,61 @@
| Type.Nonterminal => if strict then err () else 0);
in (Type (d, replicate args dummyT), reports) end;
-fun check_type_name_proper ctxt strict arg =
- (case check_type_name ctxt strict arg of
- res as (Type _, _) => res
- | (T, _) => error ("Not a type constructor: " ^ Syntax.string_of_typ ctxt T));
-
-fun read_type_name ctxt strict =
- Syntax.read_token #> Symbol_Pos.source_content #> check_type_name ctxt strict #> #1;
-
-fun read_type_name_proper ctxt strict =
- Syntax.read_token #> Symbol_Pos.source_content #> check_type_name_proper ctxt strict #> #1;
+fun read_type_name ctxt flags text =
+ let
+ val (T, reports) =
+ check_type_name ctxt flags (Symbol_Pos.source_content (Syntax.read_token text));
+ val _ = Position.reports reports;
+ in T end;
(* constant names *)
-local
-
-fun prep_const_proper ctxt strict (c, pos) =
- let
- fun err msg = error (msg ^ Position.here pos);
- val consts = consts_of ctxt;
- val t as Const (d, _) =
- (case Variable.lookup_const ctxt c of
- SOME d =>
- let
- val T = Consts.type_scheme (consts_of ctxt) d handle TYPE (msg, _, _) => err msg;
- val _ = Context_Position.report ctxt pos (Name_Space.markup (Consts.space_of consts) d);
- in Const (d, T) end
- | NONE => Consts.check_const (Context.Proof ctxt) consts (c, pos));
- val _ =
- if strict
- then ignore (Consts.the_const consts d) handle TYPE (msg, _, _) => err msg
- else ();
- in t end;
+fun consts_completion_message ctxt (c, ps) =
+ ps |> map (fn pos =>
+ Name_Space.completion (Context.Proof ctxt) (Consts.space_of (consts_of ctxt)) (c, pos)
+ |> Completion.reported_text)
+ |> implode
+ |> Markup.markup_report;
-in
-
-fun read_const_proper ctxt strict =
- prep_const_proper ctxt strict o Symbol_Pos.source_content o Syntax.read_token;
-
-fun read_const ctxt strict ty text =
+fun check_const ctxt {proper, strict} (c, ps) =
let
- val (c, pos) = Symbol_Pos.source_content (Syntax.read_token text);
- val _ = no_skolem false c;
- in
- (case (Variable.lookup_fixed ctxt c, Variable.is_const ctxt c) of
- (SOME x, false) =>
- (Context_Position.report ctxt pos
- (Markup.name x (if can Name.dest_skolem x then Markup.skolem else Markup.free));
- Free (x, infer_type ctxt (x, ty)))
- | _ => prep_const_proper ctxt strict (c, pos))
- end;
+ val _ =
+ Name.reject_internal (c, ps) handle ERROR msg =>
+ error (msg ^ consts_completion_message ctxt (c, ps));
+ fun err msg = error (msg ^ Position.here_list ps);
+ val consts = consts_of ctxt;
+ val fixed = if proper then NONE else Variable.lookup_fixed ctxt c;
+ val (t, reports) =
+ (case (fixed, Variable.lookup_const ctxt c) of
+ (SOME x, NONE) =>
+ let
+ val reports = ps
+ |> filter (Context_Position.is_reported ctxt)
+ |> map (fn pos =>
+ (pos, Markup.name x (if Name.is_skolem x then Markup.skolem else Markup.free)));
+ in (Free (x, infer_type ctxt (x, dummyT)), reports) end
+ | (_, SOME d) =>
+ let
+ val T = Consts.type_scheme consts d handle TYPE (msg, _, _) => err msg;
+ val reports = ps
+ |> filter (Context_Position.is_reported ctxt)
+ |> map (fn pos => (pos, Name_Space.markup (Consts.space_of consts) d));
+ in (Const (d, T), reports) end
+ | _ => Consts.check_const (Context.Proof ctxt) consts (c, ps));
+ val _ =
+ (case (strict, t) of
+ (true, Const (d, _)) =>
+ (ignore (Consts.the_const consts d) handle TYPE (msg, _, _) => err msg)
+ | _ => ());
+ in (t, reports) end;
-end;
+fun read_const ctxt flags text =
+ let
+ val (xname, pos) = Symbol_Pos.source_content (Syntax.read_token text);
+ val (t, reports) = check_const ctxt flags (xname, [pos]);
+ val _ = Position.reports reports;
+ in t end;
(* type arities *)
@@ -539,29 +527,14 @@
in
val read_arity =
- prep_arity (fn ctxt => #1 o dest_Type o read_type_name_proper ctxt true) Syntax.read_sort;
+ prep_arity (fn ctxt => #1 o dest_Type o read_type_name ctxt {proper = true, strict = true})
+ Syntax.read_sort;
val cert_arity = prep_arity (K I) (Type.cert_sort o tsig_of);
end;
-(* skolem variables *)
-
-fun intern_skolem ctxt x =
- let
- val _ = no_skolem false x;
- val sko = Variable.lookup_fixed ctxt x;
- val is_const = can (read_const_proper ctxt false) 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 sko then sko
- else if not is_const orelse is_declared then SOME x
- else NONE
- end;
-
-
(* read_term *)
fun read_term_mode mode ctxt = Syntax.read_term (set_mode mode ctxt);
@@ -1033,8 +1006,10 @@
fold_map (fn (b, raw_T, mx) => fn ctxt =>
let
val x = Variable.check_name b;
- val _ = Symbol_Pos.is_identifier (no_skolem internal x) orelse
- error ("Illegal variable name: " ^ Binding.print b);
+ val check_name = if internal then Name.reject_skolem else Name.reject_internal;
+ val _ =
+ if can check_name (x, []) andalso Symbol_Pos.is_identifier x then ()
+ else error ("Bad name: " ^ Binding.print b);
fun cond_tvars T =
if internal then T
@@ -1375,7 +1350,7 @@
if x = x' then Pretty.str x
else Pretty.block [Pretty.str x, Pretty.str " =", Pretty.brk 1, prt_term (Syntax.free x')];
val fixes =
- filter_out ((can Name.dest_internal orf member (op =) structs) o #1)
+ filter_out ((Name.is_internal orf member (op =) structs) o #1)
(Variable.dest_fixes ctxt);
val prt_fixes =
if null fixes then []
--- a/src/Pure/Isar/specification.ML Thu Mar 06 17:55:39 2014 +0100
+++ b/src/Pure/Isar/specification.ML Thu Mar 06 22:15:01 2014 +0100
@@ -276,10 +276,12 @@
in
val type_notation = gen_type_notation (K I);
-val type_notation_cmd = gen_type_notation (fn ctxt => Proof_Context.read_type_name ctxt false);
+val type_notation_cmd =
+ gen_type_notation (fn ctxt => Proof_Context.read_type_name ctxt {proper = true, strict = false});
val notation = gen_notation (K I);
-val notation_cmd = gen_notation (fn ctxt => Proof_Context.read_const ctxt false dummyT);
+val notation_cmd =
+ gen_notation (fn ctxt => Proof_Context.read_const ctxt {proper = false, strict = false});
end;
--- a/src/Pure/ML/ml_antiquote.ML Thu Mar 06 17:55:39 2014 +0100
+++ b/src/Pure/ML/ml_antiquote.ML Thu Mar 06 22:15:01 2014 +0100
@@ -127,7 +127,7 @@
fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax)
>> (fn (ctxt, (s, pos)) =>
let
- val Type (c, _) = Proof_Context.read_type_name_proper ctxt false s;
+ val Type (c, _) = Proof_Context.read_type_name ctxt {proper = true, strict = false} s;
val decl = Type.the_decl (Proof_Context.tsig_of ctxt) (c, pos);
val res =
(case try check (c, decl) of
@@ -151,7 +151,7 @@
fun const_name check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax)
>> (fn (ctxt, (s, pos)) =>
let
- val Const (c, _) = Proof_Context.read_const_proper ctxt false s;
+ val Const (c, _) = Proof_Context.read_const ctxt {proper = true, strict = false} s;
val res = check (Proof_Context.consts_of ctxt, c)
handle TYPE (msg, _, _) => error (msg ^ Position.here pos);
in ML_Syntax.print_string res end);
@@ -175,7 +175,8 @@
(Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
>> (fn ((ctxt, raw_c), Ts) =>
let
- val Const (c, _) = Proof_Context.read_const_proper ctxt true raw_c;
+ val Const (c, _) =
+ Proof_Context.read_const ctxt {proper = true, strict = true} raw_c;
val consts = Proof_Context.consts_of ctxt;
val n = length (Consts.typargs consts (c, Consts.type_scheme consts c));
val _ = length Ts <> n andalso
--- a/src/Pure/PIDE/markup.ML Thu Mar 06 17:55:39 2014 +0100
+++ b/src/Pure/PIDE/markup.ML Thu Mar 06 22:15:01 2014 +0100
@@ -189,6 +189,7 @@
val enclose: T -> Output.output -> Output.output
val markup: T -> string -> string
val markup_only: T -> string
+ val markup_report: string -> string
end;
structure Markup: MARKUP =
@@ -602,4 +603,7 @@
fun markup_only m = markup m "";
+fun markup_report "" = ""
+ | markup_report txt = markup report txt;
+
end;
--- a/src/Pure/Syntax/lexicon.ML Thu Mar 06 17:55:39 2014 +0100
+++ b/src/Pure/Syntax/lexicon.ML Thu Mar 06 22:15:01 2014 +0100
@@ -261,8 +261,8 @@
fun tokenize lex xids syms =
let
val scan_xid =
- if xids then $$$ "_" @@@ scan_id || scan_id
- else scan_id;
+ (if xids then $$$ "_" @@@ scan_id || scan_id else scan_id) ||
+ $$$ "_" @@@ $$$ "_";
val scan_num = scan_hex || scan_bin || scan_int;
--- a/src/Pure/Syntax/syntax_phases.ML Thu Mar 06 17:55:39 2014 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML Thu Mar 06 22:15:01 2014 +0100
@@ -51,7 +51,7 @@
[Name_Space.markup (Consts.space_of (Proof_Context.consts_of ctxt)) c];
fun markup_free ctxt x =
- [if can Name.dest_skolem x then Markup.skolem else Markup.free] @
+ [if Name.is_skolem x then Markup.skolem else Markup.free] @
(if Variable.is_body ctxt orelse Variable.is_fixed ctxt x
then [Variable.markup_fixed ctxt x]
else []);
@@ -140,6 +140,7 @@
let
val reports = Unsynchronized.ref ([]: Position.report_text list);
fun report pos = Position.store_reports reports [pos];
+ val append_reports = Position.append_reports reports;
fun trans a args =
(case trf a of
@@ -164,14 +165,15 @@
let
val pos = Lexicon.pos_of_token tok;
val (c, rs) = Proof_Context.check_class ctxt (Lexicon.str_of_token tok, pos);
- val _ = Unsynchronized.change reports (append (map (rpair "") rs));
+ val _ = append_reports rs;
in [Ast.Constant (Lexicon.mark_class c)] end
| asts_of (Parser.Node ("_type_name", [Parser.Tip tok])) =
let
val pos = Lexicon.pos_of_token tok;
val (Type (c, _), rs) =
- Proof_Context.check_type_name_proper ctxt false (Lexicon.str_of_token tok, pos);
- val _ = Unsynchronized.change reports (append (map (rpair "") rs));
+ Proof_Context.check_type_name ctxt {proper = true, strict = false}
+ (Lexicon.str_of_token tok, pos);
+ val _ = append_reports rs;
in [Ast.Constant (Lexicon.mark_type c)] end
| asts_of (Parser.Node ("_position", [Parser.Tip tok])) = asts_of_position "_constrain" tok
| asts_of (Parser.Node ("_position_sort", [Parser.Tip tok])) = asts_of_position "_ofsort" tok
@@ -220,16 +222,36 @@
(* decode_term -- transform parse tree into raw term *)
+fun decode_const ctxt (c, ps) =
+ let
+ val (Const (c', _), reports) =
+ Proof_Context.check_const ctxt {proper = true, strict = false} (c, ps);
+ in (c', reports) end;
+
fun decode_term _ (result as (_: Position.report_text list, Exn.Exn _)) = result
| decode_term ctxt (reports0, Exn.Res tm) =
let
- fun get_const a =
- ((true, #1 (Term.dest_Const (Proof_Context.read_const_proper ctxt false a)))
- handle ERROR _ => (false, Consts.intern (Proof_Context.consts_of ctxt) a));
- val get_free = Proof_Context.intern_skolem ctxt;
-
val reports = Unsynchronized.ref reports0;
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
@@ -252,18 +274,15 @@
let
val c =
(case try Lexicon.unmark_const a of
- SOME c => c
- | NONE => snd (get_const a));
- val _ = report ps (markup_const ctxt) c;
+ SOME c => (report ps (markup_const ctxt) c; c)
+ | NONE => the_const (a, ps));
in Const (c, T) end)
| decode ps _ _ (Free (a, T)) =
- (case (get_free a, get_const a) of
- (SOME x, _) => (report ps (markup_free ctxt) x; Free (x, T))
- | (_, (true, c)) => (report ps (markup_const ctxt) c; Const (c, T))
- | (_, (false, c)) =>
- if Long_Name.is_qualified c
- then (report ps (markup_const ctxt) c; Const (c, T))
- else (report ps (markup_free ctxt) c; Free (c, T)))
+ ((Name.reject_internal (a, ps) handle ERROR msg =>
+ error (msg ^ Proof_Context.consts_completion_message ctxt (a, ps)));
+ (case get_free a of
+ SOME x => (report ps (markup_free ctxt) x; Free (x, T))
+ | NONE => Const (the_const (a, ps), T)))
| 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
@@ -304,8 +323,7 @@
val pts = Syntax.parse syn root (filter Lexicon.is_proper toks)
handle ERROR msg =>
- error (msg ^
- implode (map (Markup.markup Markup.report o Lexicon.reported_token_range ctxt) toks));
+ error (msg ^ Markup.markup_report (implode (map (Lexicon.reported_token_range ctxt) toks)));
val len = length pts;
val limit = Config.get ctxt Syntax.ambiguity_limit;
@@ -337,7 +355,7 @@
fun parse_failed ctxt pos msg kind =
cat_error msg ("Failed to parse " ^ kind ^
- Markup.markup Markup.report (Context_Position.reported_text ctxt pos Markup.bad ""));
+ Markup.markup_report (Context_Position.reported_text ctxt pos Markup.bad ""));
fun parse_sort ctxt =
Syntax.parse_token ctxt Term_XML.Decode.sort Markup.language_sort
@@ -664,7 +682,7 @@
if Variable.is_fixed ctxt x orelse Syntax.is_pretty_global ctxt
then Markup.fixed x else Markup.intensify;
in
- if can Name.dest_skolem x
+ if Name.is_skolem x
then ([m, Markup.skolem], Variable.revert_fixed ctxt x)
else ([m, Markup.free], x)
end;
@@ -793,16 +811,15 @@
(* authentic syntax *)
-fun const_ast_tr intern ctxt [Ast.Variable c] =
+fun const_ast_tr intern ctxt asts =
+ (case asts of
+ [Ast.Appl [Ast.Constant "_constrain", Ast.Variable c, T as Ast.Variable p]] =>
let
- val Const (c', _) = Proof_Context.read_const_proper ctxt false c;
+ val pos = the_default Position.none (Term_Position.decode p);
+ val (c', _) = decode_const ctxt (c, [pos]);
val d = if intern then Lexicon.mark_const c' else c;
- in Ast.Constant d end
- | const_ast_tr intern ctxt [Ast.Appl [Ast.Constant "_constrain", x, T as Ast.Variable pos]] =
- (Ast.Appl [Ast.Constant "_constrain", const_ast_tr intern ctxt [x], T]
- handle ERROR msg =>
- error (msg ^ Position.here (the_default Position.none (Term_Position.decode pos))))
- | const_ast_tr _ _ asts = raise Ast.AST ("const_ast_tr", asts);
+ in Ast.Appl [Ast.Constant "_constrain", Ast.Constant d, T] end
+ | _ => raise Ast.AST ("const_ast_tr", asts));
(* setup translations *)
--- a/src/Pure/Syntax/syntax_trans.ML Thu Mar 06 17:55:39 2014 +0100
+++ b/src/Pure/Syntax/syntax_trans.ML Thu Mar 06 22:15:01 2014 +0100
@@ -124,7 +124,7 @@
| lambda_ast_tr asts = raise Ast.AST ("lambda_ast_tr", asts);
fun absfree_proper (x, T) t =
- if can Name.dest_internal x
+ if Name.is_internal x
then error ("Illegal internal variable in abstraction: " ^ quote x)
else absfree (x, T) t;
@@ -316,7 +316,7 @@
val body = body_of tm;
val rev_new_vars = Term.rename_wrt_term body vars;
fun subst (x, T) b =
- if can Name.dest_internal x andalso not (Term.is_dependent b)
+ if Name.is_internal x andalso not (Term.is_dependent b)
then (Const ("_idtdummy", T), incr_boundvars ~1 b)
else (mark_bound_abs (x, T), Term.subst_bound (mark_bound_body (x, T), b));
val (rev_vars', body') = fold_map subst rev_new_vars body;
--- a/src/Pure/Thy/thy_output.ML Thu Mar 06 17:55:39 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML Thu Mar 06 22:15:01 2014 +0100
@@ -515,7 +515,7 @@
Pretty.str o Proof_Context.extern_class ctxt o Proof_Context.read_class ctxt;
fun pretty_type ctxt s =
- let val Type (name, _) = Proof_Context.read_type_name_proper ctxt false s
+ let val Type (name, _) = Proof_Context.read_type_name ctxt {proper = true, strict = false} s
in Pretty.str (Proof_Context.extern_type ctxt name) end;
fun pretty_prf full ctxt = Proof_Syntax.pretty_proof_of ctxt full;
@@ -573,7 +573,7 @@
basic_entity (Binding.name "term") (Term_Style.parse -- Args.term) pretty_term_style #>
basic_entity (Binding.name "term_type") (Term_Style.parse -- Args.term) pretty_term_typ #>
basic_entity (Binding.name "typeof") (Term_Style.parse -- Args.term) pretty_term_typeof #>
- basic_entity (Binding.name "const") (Args.const_proper false) pretty_const #>
+ basic_entity (Binding.name "const") (Args.const {proper = true, strict = false}) pretty_const #>
basic_entity (Binding.name "abbrev") (Scan.lift Args.name_inner_syntax) pretty_abbrev #>
basic_entity (Binding.name "typ") Args.typ_abbrev Syntax.pretty_typ #>
basic_entity (Binding.name "class") (Scan.lift Args.name_inner_syntax) pretty_class #>
--- a/src/Pure/consts.ML Thu Mar 06 17:55:39 2014 +0100
+++ b/src/Pure/consts.ML Thu Mar 06 22:15:01 2014 +0100
@@ -25,7 +25,7 @@
val extern: Proof.context -> T -> string -> xstring
val intern_syntax: T -> xstring -> string
val extern_syntax: Proof.context -> T -> string -> xstring
- val check_const: Context.generic -> T -> xstring * Position.T -> term
+ val check_const: Context.generic -> T -> xstring * Position.T list -> term * Position.report list
val certify: Context.pretty -> Type.tsig -> bool -> T -> term -> term (*exception TYPE*)
val typargs: T -> string * typ -> typ list
val instance: T -> string * typ list -> typ
@@ -143,12 +143,12 @@
(* check_const *)
-fun check_const context consts (xname, pos) =
+fun check_const context consts (xname, ps) =
let
val Consts {decls, ...} = consts;
- val (c, _) = Name_Space.check context decls (xname, pos);
- val T = type_scheme consts c handle TYPE (msg, _, _) => error (msg ^ Position.here pos);
- in Const (c, T) end;
+ val ((c, reports), _) = Name_Space.check_reports context decls (xname, ps);
+ val T = type_scheme consts c handle TYPE (msg, _, _) => error (msg ^ Position.here_list ps);
+ in (Const (c, T), reports) end;
(* certify *)
--- a/src/Pure/name.ML Thu Mar 06 17:55:39 2014 +0100
+++ b/src/Pure/name.ML Thu Mar 06 22:15:01 2014 +0100
@@ -13,8 +13,12 @@
val is_bound: string -> bool
val internal: string -> string
val dest_internal: string -> string
+ val is_internal: string -> bool
+ val reject_internal: string * Position.T list -> unit
val skolem: string -> string
val dest_skolem: string -> string
+ val is_skolem: string -> bool
+ val reject_skolem: string * Position.T list -> unit
val clean_index: string * int -> string * int
val clean: string -> string
type context
@@ -59,13 +63,19 @@
val is_bound = String.isPrefix ":";
-(* internal names *)
+(* internal names -- NB: internal subsumes skolem *)
val internal = suffix "_";
val dest_internal = unsuffix "_";
+val is_internal = String.isSuffix "_";
+fun reject_internal (x, ps) =
+ if is_internal x then error ("Bad name: " ^ quote x ^ Position.here_list ps) else ();
val skolem = suffix "__";
val dest_skolem = unsuffix "__";
+val is_skolem = String.isSuffix "__";
+fun reject_skolem (x, ps) =
+ if is_skolem x then error ("Bad name: " ^ quote x ^ Position.here_list ps) else ();
fun clean_index (x, i) =
(case try dest_internal x of
--- a/src/Pure/type.ML Thu Mar 06 17:55:39 2014 +0100
+++ b/src/Pure/type.ML Thu Mar 06 22:15:01 2014 +0100
@@ -259,7 +259,8 @@
fun lookup_type (TSig {types = (_, types), ...}) = Symtab.lookup types;
-fun check_decl context (TSig {types, ...}) = Name_Space.check_reports context types;
+fun check_decl context (TSig {types, ...}) (c, pos) =
+ Name_Space.check_reports context types (c, [pos]);
fun the_decl tsig (c, pos) =
(case lookup_type tsig c of
--- a/src/Pure/variable.ML Thu Mar 06 17:55:39 2014 +0100
+++ b/src/Pure/variable.ML Thu Mar 06 22:15:01 2014 +0100
@@ -399,7 +399,7 @@
fun add_fixes_binding bs ctxt =
let
val _ =
- (case filter (can Name.dest_skolem o Binding.name_of) bs of
+ (case filter (Name.is_skolem o Binding.name_of) bs of
[] => ()
| bads => error ("Illegal internal Skolem constant(s): " ^ commas (map Binding.print bads)));
val _ =
@@ -417,7 +417,7 @@
fun variant_fixes raw_xs ctxt =
let
val names = names_of ctxt;
- val xs = map (fn x => Name.clean x |> can Name.dest_internal x ? Name.internal) raw_xs;
+ val xs = map (fn x => Name.clean x |> Name.is_internal x ? Name.internal) raw_xs;
val (xs', names') = fold_map Name.variant xs names |>> (is_body ctxt ? map Name.skolem);
in ctxt |> new_fixes names' xs xs' (replicate (length xs) Position.none) end;
--- a/src/Tools/Code/code_target.ML Thu Mar 06 17:55:39 2014 +0100
+++ b/src/Tools/Code/code_target.ML Thu Mar 06 22:15:01 2014 +0100
@@ -97,8 +97,8 @@
else error ("No such type constructor: " ^ quote tyco);
in tyco end;
-fun read_tyco ctxt = #1 o dest_Type
- o Proof_Context.read_type_name_proper ctxt true;
+fun read_tyco ctxt =
+ #1 o dest_Type o Proof_Context.read_type_name ctxt {proper = true, strict = true};
fun cert_class ctxt class =
let
--- a/src/Tools/adhoc_overloading.ML Thu Mar 06 17:55:39 2014 +0100
+++ b/src/Tools/adhoc_overloading.ML Thu Mar 06 22:15:01 2014 +0100
@@ -220,7 +220,8 @@
fun adhoc_overloading_cmd add raw_args lthy =
let
- fun const_name ctxt = fst o dest_Const o Proof_Context.read_const ctxt false dummyT;
+ fun const_name ctxt =
+ fst o dest_Const o Proof_Context.read_const ctxt {proper = false, strict = false}; (* FIXME {proper = true, strict = true} (!?) *)
fun read_term ctxt = singleton (Variable.polymorphic ctxt) o Syntax.read_term ctxt;
val args =
raw_args
--- a/src/Tools/induct.ML Thu Mar 06 17:55:39 2014 +0100
+++ b/src/Tools/induct.ML Thu Mar 06 22:15:01 2014 +0100
@@ -361,9 +361,9 @@
Scan.lift (Args.$$$ k) >> K "";
fun attrib add_type add_pred del =
- spec typeN (Args.type_name false) >> add_type ||
- spec predN (Args.const false) >> add_pred ||
- spec setN (Args.const false) >> add_pred ||
+ spec typeN (Args.type_name {proper = false, strict = false}) >> add_type ||
+ spec predN (Args.const {proper = false, strict = false}) >> add_pred ||
+ spec setN (Args.const {proper = false, strict = false}) >> add_pred ||
Scan.lift Args.del >> K del;
in
@@ -883,9 +883,9 @@
| NONE => error ("No rule for " ^ k ^ " " ^ quote name))))));
fun rule get_type get_pred =
- named_rule typeN (Args.type_name false) get_type ||
- named_rule predN (Args.const false) get_pred ||
- named_rule setN (Args.const false) get_pred ||
+ named_rule typeN (Args.type_name {proper = false, strict = false}) get_type ||
+ named_rule predN (Args.const {proper = false, strict = false}) get_pred ||
+ named_rule setN (Args.const {proper = false, strict = false}) get_pred ||
Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms;
val cases_rule = rule lookup_casesT lookup_casesP >> single_rule;
--- a/src/Tools/subtyping.ML Thu Mar 06 17:55:39 2014 +0100
+++ b/src/Tools/subtyping.ML Thu Mar 06 22:15:01 2014 +0100
@@ -1105,7 +1105,7 @@
(Args.term >> (fn t => Thm.declaration_attribute (K (add_type_map t))))
"declaration of new map functions" #>
Attrib.setup @{binding coercion_args}
- (Args.const false -- Scan.lift (Scan.repeat1 parse_coerce_args) >>
+ (Args.const {proper = false, strict = false} -- Scan.lift (Scan.repeat1 parse_coerce_args) >>
(fn spec => Thm.declaration_attribute (K (map_coerce_args (Symtab.update spec)))))
"declaration of new constants with coercion-invariant arguments";