--- a/src/Doc/IsarImplementation/Integration.thy Sun Mar 02 19:15:23 2014 +0100
+++ b/src/Doc/IsarImplementation/Integration.thy Sun Mar 02 22:43:20 2014 +0100
@@ -48,7 +48,7 @@
text %mlref {*
\begin{mldecls}
@{index_ML_type Toplevel.state} \\
- @{index_ML Toplevel.UNDEF: "exn"} \\
+ @{index_ML_exception Toplevel.UNDEF} \\
@{index_ML Toplevel.is_toplevel: "Toplevel.state -> bool"} \\
@{index_ML Toplevel.theory_of: "Toplevel.state -> theory"} \\
@{index_ML Toplevel.proof_of: "Toplevel.state -> Proof.state"} \\
--- a/src/Doc/IsarImplementation/Logic.thy Sun Mar 02 19:15:23 2014 +0100
+++ b/src/Doc/IsarImplementation/Logic.thy Sun Mar 02 22:43:20 2014 +0100
@@ -696,7 +696,7 @@
abstract types @{ML_type ctyp} and @{ML_type cterm} are part of the
same inference kernel that is mainly responsible for @{ML_type thm}.
Thus syntactic operations on @{ML_type ctyp} and @{ML_type cterm}
- are located in the @{ML_struct Thm} module, even though theorems are
+ are located in the @{ML_structure Thm} module, even though theorems are
not yet involved at that stage.
\item @{ML Thm.ctyp_of}~@{text "thy \<tau>"} and @{ML
@@ -717,7 +717,7 @@
\item Type @{ML_type thm} represents proven propositions. This is
an abstract datatype that guarantees that its values have been
- constructed by basic principles of the @{ML_struct Thm} module.
+ constructed by basic principles of the @{ML_structure Thm} module.
Every @{ML_type thm} value refers its background theory,
cf.\ \secref{sec:context-theory}.
--- a/src/Doc/IsarImplementation/ML.thy Sun Mar 02 19:15:23 2014 +0100
+++ b/src/Doc/IsarImplementation/ML.thy Sun Mar 02 22:43:20 2014 +0100
@@ -1159,8 +1159,8 @@
\begin{mldecls}
@{index_ML try: "('a -> 'b) -> 'a -> 'b option"} \\
@{index_ML can: "('a -> 'b) -> 'a -> bool"} \\
- @{index_ML ERROR: "string -> exn"} \\
- @{index_ML Fail: "string -> exn"} \\
+ @{index_ML_exception ERROR: string} \\
+ @{index_ML_exception Fail: string} \\
@{index_ML Exn.is_interrupt: "exn -> bool"} \\
@{index_ML reraise: "exn -> 'a"} \\
@{index_ML ML_Compiler.exn_trace: "(unit -> 'a) -> 'a"} \\
@@ -1439,8 +1439,8 @@
Literal integers in ML text are forced to be of this one true
integer type --- adhoc overloading of SML97 is disabled.
- Structure @{ML_struct IntInf} of SML97 is obsolete and superseded by
- @{ML_struct Int}. Structure @{ML_struct Integer} in @{file
+ Structure @{ML_structure IntInf} of SML97 is obsolete and superseded by
+ @{ML_structure Int}. Structure @{ML_structure Integer} in @{file
"~~/src/Pure/General/integer.ML"} provides some additional
operations.
@@ -1487,7 +1487,7 @@
*}
text {* Apart from @{ML Option.map} most other operations defined in
- structure @{ML_struct Option} are alien to Isabelle/ML an never
+ structure @{ML_structure Option} are alien to Isabelle/ML an never
used. The operations shown above are defined in @{file
"~~/src/Pure/General/basics.ML"}. *}
--- a/src/Doc/IsarImplementation/Prelim.thy Sun Mar 02 19:15:23 2014 +0100
+++ b/src/Doc/IsarImplementation/Prelim.thy Sun Mar 02 22:43:20 2014 +0100
@@ -709,7 +709,7 @@
of declared type and term variable names. Projecting a proof
context down to a primitive name context is occasionally useful when
invoking lower-level operations. Regular management of ``fresh
- variables'' is done by suitable operations of structure @{ML_struct
+ variables'' is done by suitable operations of structure @{ML_structure
Variable}, which is also able to provide an official status of
``locally fixed variable'' within the logical environment (cf.\
\secref{sec:variables}).
--- a/src/Doc/IsarRef/Document_Preparation.thy Sun Mar 02 19:15:23 2014 +0100
+++ b/src/Doc/IsarRef/Document_Preparation.thy Sun Mar 02 22:43:20 2014 +0100
@@ -123,7 +123,8 @@
@{antiquotation_def ML} & : & @{text antiquotation} \\
@{antiquotation_def ML_op} & : & @{text antiquotation} \\
@{antiquotation_def ML_type} & : & @{text antiquotation} \\
- @{antiquotation_def ML_struct} & : & @{text antiquotation} \\
+ @{antiquotation_def ML_structure} & : & @{text antiquotation} \\
+ @{antiquotation_def ML_functor} & : & @{text antiquotation} \\
@{antiquotation_def "file"} & : & @{text antiquotation} \\
@{antiquotation_def "url"} & : & @{text antiquotation} \\
\end{matharray}
@@ -175,7 +176,8 @@
@@{antiquotation ML} options @{syntax name} |
@@{antiquotation ML_op} options @{syntax name} |
@@{antiquotation ML_type} options @{syntax name} |
- @@{antiquotation ML_struct} options @{syntax name} |
+ @@{antiquotation ML_structure} options @{syntax name} |
+ @@{antiquotation ML_functor} options @{syntax name} |
@@{antiquotation "file"} options @{syntax name} |
@@{antiquotation file_unchecked} options @{syntax name} |
@@{antiquotation url} options @{syntax name}
@@ -263,9 +265,9 @@
``@{text _}'' placeholders there.
\item @{text "@{ML s}"}, @{text "@{ML_op s}"}, @{text "@{ML_type
- s}"}, and @{text "@{ML_struct s}"} check text @{text s} as ML value,
- infix operator, type, and structure, respectively. The source is
- printed verbatim.
+ s}"}, @{text "@{ML_structure s}"}, and @{text "@{ML_functor s}"}
+ check text @{text s} as ML value, infix operator, type, structure,
+ and functor respectively. The source is printed verbatim.
\item @{text "@{file path}"} checks that @{text "path"} refers to a
file (or directory) and prints it verbatim.
--- a/src/Doc/IsarRef/Proof.thy Sun Mar 02 19:15:23 2014 +0100
+++ b/src/Doc/IsarRef/Proof.thy Sun Mar 02 22:43:20 2014 +0100
@@ -926,7 +926,7 @@
defines a proof method in the current theory. The given @{text
"text"} has to be an ML expression of type
@{ML_type "(Proof.context -> Proof.method) context_parser"}, cf.\
- basic parsers defined in structure @{ML_struct Args} and @{ML_struct
+ basic parsers defined in structure @{ML_structure Args} and @{ML_structure
Attrib}. There are also combinators like @{ML METHOD} and @{ML
SIMPLE_METHOD} to turn certain tactic forms into official proof
methods; the primed versions refer to tactics with explicit goal
--- a/src/Doc/IsarRef/Spec.thy Sun Mar 02 19:15:23 2014 +0100
+++ b/src/Doc/IsarRef/Spec.thy Sun Mar 02 22:43:20 2014 +0100
@@ -1059,7 +1059,7 @@
defines an attribute in the current theory. The given @{text
"text"} has to be an ML expression of type
@{ML_type "attribute context_parser"}, cf.\ basic parsers defined in
- structure @{ML_struct Args} and @{ML_struct Attrib}.
+ structure @{ML_structure Args} and @{ML_structure Attrib}.
In principle, attributes can operate both on a given theorem and the
implicit context, although in practice only one is modified and the
--- a/src/Doc/LaTeXsugar/Sugar.thy Sun Mar 02 19:15:23 2014 +0100
+++ b/src/Doc/LaTeXsugar/Sugar.thy Sun Mar 02 22:43:20 2014 +0100
@@ -398,7 +398,7 @@
Further use cases can be found in \S\ref{sec:yourself}.
If you are not afraid of ML, you may also define your own styles.
-Have a look at module @{ML_struct Term_Style}.
+Have a look at module @{ML_structure Term_Style}.
\section {Proofs}
--- a/src/Doc/antiquote_setup.ML Sun Mar 02 19:15:23 2014 +0100
+++ b/src/Doc/antiquote_setup.ML Sun Mar 02 22:43:20 2014 +0100
@@ -64,8 +64,8 @@
ml_toks "val _ = [NONE : (" @ toks1 @ ml_toks ") option, NONE : (" @
toks2 @ ml_toks ") option];";
-fun ml_exn (toks1, []) = ml_toks "fn _ => (" @ toks1 @ ml_toks " : exn);"
- | ml_exn (toks1, toks2) =
+fun ml_exception (toks1, []) = ml_toks "fn _ => (" @ toks1 @ ml_toks " : exn);"
+ | ml_exception (toks1, toks2) =
ml_toks "fn _ => (" @ toks1 @ ml_toks " : " @ toks2 @ ml_toks " -> exn);";
fun ml_structure (toks, _) =
@@ -121,8 +121,8 @@
index_ml @{binding index_ML} "" ml_val #>
index_ml @{binding index_ML_op} "infix" ml_op #>
index_ml @{binding index_ML_type} "type" ml_type #>
- index_ml @{binding index_ML_exn} "exception" ml_exn #>
- index_ml @{binding index_ML_struct} "structure" ml_structure #>
+ index_ml @{binding index_ML_exception} "exception" ml_exception #>
+ index_ml @{binding index_ML_structure} "structure" ml_structure #>
index_ml @{binding index_ML_functor} "functor" ml_functor;
end;
--- a/src/HOL/Decision_Procs/Cooper.thy Sun Mar 02 19:15:23 2014 +0100
+++ b/src/HOL/Decision_Procs/Cooper.thy Sun Mar 02 22:43:20 2014 +0100
@@ -25,7 +25,8 @@
| "num_size (CN n c a) = 4 + num_size a"
| "num_size (Mul c a) = 1 + num_size a"
-primrec Inum :: "int list \<Rightarrow> num \<Rightarrow> int" where
+primrec Inum :: "int list \<Rightarrow> num \<Rightarrow> int"
+where
"Inum bs (C c) = c"
| "Inum bs (Bound n) = bs!n"
| "Inum bs (CN n c a) = c * (bs!n) + (Inum bs a)"
@@ -267,15 +268,18 @@
| "isatom p = False"
lemma numsubst0_numbound0:
- assumes nb: "numbound0 t"
+ assumes "numbound0 t"
shows "numbound0 (numsubst0 t a)"
- using nb apply (induct a)
+ using assms
+ apply (induct a)
apply simp_all
- apply (case_tac nat, simp_all)
+ apply (case_tac nat)
+ apply simp_all
done
lemma subst0_bound0:
- assumes qf: "qfree p" and nb: "numbound0 t"
+ assumes qf: "qfree p"
+ and nb: "numbound0 t"
shows "bound0 (subst0 t p)"
using qf numsubst0_numbound0[OF nb] by (induct p) auto
@@ -356,22 +360,28 @@
assumes fqf: "\<forall>p. qfree p \<longrightarrow> qfree (f p)"
shows "\<forall>p. qfree p \<longrightarrow> qfree (DJ f p) "
proof clarify
- fix p assume qf: "qfree p"
- have th: "DJ f p = evaldjf f (disjuncts p)" by (simp add: DJ_def)
+ fix p
+ assume qf: "qfree p"
+ have th: "DJ f p = evaldjf f (disjuncts p)"
+ by (simp add: DJ_def)
from disjuncts_qf[OF qf] have "\<forall>q\<in> set (disjuncts p). qfree q" .
- with fqf have th':"\<forall>q\<in> set (disjuncts p). qfree (f q)" by blast
-
- from evaldjf_qf[OF th'] th show "qfree (DJ f p)" by simp
+ with fqf have th':"\<forall>q\<in> set (disjuncts p). qfree (f q)"
+ by blast
+ from evaldjf_qf[OF th'] th show "qfree (DJ f p)"
+ by simp
qed
lemma DJ_qe:
assumes qe: "\<forall>bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm bbs bs (qe p) = Ifm bbs bs (E p))"
shows "\<forall>bs p. qfree p \<longrightarrow> qfree (DJ qe p) \<and> (Ifm bbs bs ((DJ qe p)) = Ifm bbs bs (E p))"
proof clarify
- fix p :: fm and bs
+ fix p :: fm
+ fix bs
assume qf: "qfree p"
- from qe have qth: "\<forall>p. qfree p \<longrightarrow> qfree (qe p)" by blast
- from DJ_qf[OF qth] qf have qfth:"qfree (DJ qe p)" by auto
+ from qe have qth: "\<forall>p. qfree p \<longrightarrow> qfree (qe p)"
+ by blast
+ from DJ_qf[OF qth] qf have qfth:"qfree (DJ qe p)"
+ by auto
have "Ifm bbs bs (DJ qe p) = (\<exists>q\<in> set (disjuncts p). Ifm bbs bs (qe q))"
by (simp add: DJ_def evaldjf_ex)
also have "\<dots> = (\<exists>q \<in> set(disjuncts p). Ifm bbs bs (E q))"
@@ -399,9 +409,9 @@
fun lex_ns:: "nat list \<Rightarrow> nat list \<Rightarrow> bool"
where
- "lex_ns [] ms = True"
-| "lex_ns ns [] = False"
-| "lex_ns (n#ns) (m#ms) = (n<m \<or> ((n = m) \<and> lex_ns ns ms)) "
+ "lex_ns [] ms \<longleftrightarrow> True"
+| "lex_ns ns [] \<longleftrightarrow> False"
+| "lex_ns (n # ns) (m # ms) \<longleftrightarrow> n < m \<or> (n = m \<and> lex_ns ns ms)"
definition lex_bnd :: "num \<Rightarrow> num \<Rightarrow> bool"
where "lex_bnd t s = lex_ns (bnds t) (bnds s)"
@@ -440,10 +450,12 @@
lemma numadd: "Inum bs (numadd (t,s)) = Inum bs (Add t s)"
apply (induct t s rule: numadd.induct, simp_all add: Let_def)
- apply (case_tac "c1 + c2 = 0", case_tac "n1 \<le> n2", simp_all)
+ apply (case_tac "c1 + c2 = 0")
+ apply (case_tac "n1 \<le> n2")
+ apply simp_all
apply (case_tac "n1 = n2")
- apply(simp_all add: algebra_simps)
- apply(simp add: distrib_right[symmetric])
+ apply (simp_all add: algebra_simps)
+ apply (simp add: distrib_right[symmetric])
done
lemma numadd_nb: "numbound0 t \<Longrightarrow> numbound0 s \<Longrightarrow> numbound0 (numadd (t, s))"
@@ -452,7 +464,7 @@
fun nummul :: "int \<Rightarrow> num \<Rightarrow> num"
where
"nummul i (C j) = C (i * j)"
-| "nummul i (CN n c t) = CN n (c*i) (nummul i t)"
+| "nummul i (CN n c t) = CN n (c * i) (nummul i t)"
| "nummul i t = Mul i t"
lemma nummul: "Inum bs (nummul i t) = Inum bs (Mul i t)"
@@ -513,10 +525,14 @@
definition conj :: "fm \<Rightarrow> fm \<Rightarrow> fm"
where
- "conj p q = (if (p = F \<or> q=F) then F else if p=T then q else if q=T then p else And p q)"
+ "conj p q =
+ (if p = F \<or> q = F then F
+ else if p = T then q
+ else if q = T then p
+ else And p q)"
lemma conj: "Ifm bbs bs (conj p q) = Ifm bbs bs (And p q)"
- by (cases "p=F \<or> q=F", simp_all add: conj_def) (cases p, simp_all)
+ by (cases "p = F \<or> q = F", simp_all add: conj_def) (cases p, simp_all)
lemma conj_qf: "qfree p \<Longrightarrow> qfree q \<Longrightarrow> qfree (conj p q)"
using conj_def by auto
@@ -527,35 +543,42 @@
definition disj :: "fm \<Rightarrow> fm \<Rightarrow> fm"
where
"disj p q =
- (if (p = T \<or> q=T) then T else if p=F then q else if q=F then p else Or p q)"
+ (if p = T \<or> q = T then T
+ else if p = F then q
+ else if q = F then p
+ else Or p q)"
lemma disj: "Ifm bbs bs (disj p q) = Ifm bbs bs (Or p q)"
by (cases "p=T \<or> q=T", simp_all add: disj_def) (cases p, simp_all)
-lemma disj_qf: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (disj p q)"
+lemma disj_qf: "qfree p \<Longrightarrow> qfree q \<Longrightarrow> qfree (disj p q)"
using disj_def by auto
-lemma disj_nb: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (disj p q)"
+lemma disj_nb: "bound0 p \<Longrightarrow> bound0 q \<Longrightarrow> bound0 (disj p q)"
using disj_def by auto
definition imp :: "fm \<Rightarrow> fm \<Rightarrow> fm"
where
- "imp p q = (if (p = F \<or> q=T) then T else if p=T then q else if q=F then not p else Imp p q)"
+ "imp p q =
+ (if p = F \<or> q = T then T
+ else if p = T then q
+ else if q = F then not p
+ else Imp p q)"
lemma imp: "Ifm bbs bs (imp p q) = Ifm bbs bs (Imp p q)"
- by (cases "p=F \<or> q=T", simp_all add: imp_def, cases p) (simp_all add: not)
+ by (cases "p = F \<or> q = T", simp_all add: imp_def, cases p) (simp_all add: not)
lemma imp_qf: "qfree p \<Longrightarrow> qfree q \<Longrightarrow> qfree (imp p q)"
- using imp_def by (cases "p=F \<or> q=T",simp_all add: imp_def,cases p) (simp_all add: not_qf)
+ using imp_def by (cases "p = F \<or> q = T", simp_all add: imp_def, cases p) (simp_all add: not_qf)
lemma imp_nb: "bound0 p \<Longrightarrow> bound0 q \<Longrightarrow> bound0 (imp p q)"
- using imp_def by (cases "p=F \<or> q=T",simp_all add: imp_def,cases p) simp_all
+ using imp_def by (cases "p = F \<or> q = T", simp_all add: imp_def, cases p) simp_all
definition iff :: "fm \<Rightarrow> fm \<Rightarrow> fm"
where
"iff p q =
- (if (p = q) then T
- else if (p = not q \<or> not p = q) then F
+ (if p = q then T
+ else if p = not q \<or> not p = q then F
else if p = F then not q
else if q = F then not p
else if p = T then q
@@ -598,7 +621,7 @@
termination by (relation "measure fmsize") auto
lemma simpfm: "Ifm bbs bs (simpfm p) = Ifm bbs bs p"
-proof(induct p rule: simpfm.induct)
+proof (induct p rule: simpfm.induct)
case (6 a)
let ?sa = "simpnum a"
from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp
@@ -793,48 +816,70 @@
shows "\<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)
- case (1 c n a) thus ?case by auto
+ case (1 c n a)
+ then show ?case by auto
next
- case (2 m n a) thus ?case by (cases "m=0") auto
+ case (2 m n a)
+ then show ?case by (cases "m = 0") auto
next
case (3 m i a n a')
let ?j = "fst (zsplit0 a)"
let ?b = "snd (zsplit0 a)"
- have abj: "zsplit0 a = (?j,?b)" by simp
- {assume "m\<noteq>0"
- with 3(1)[OF abj] 3(2) have ?case by (auto simp add: Let_def split_def)}
+ have abj: "zsplit0 a = (?j, ?b)" by simp
+ {
+ assume "m \<noteq> 0"
+ with 3(1)[OF abj] 3(2) have ?case
+ by (auto simp add: Let_def split_def)
+ }
moreover
- {assume m0: "m =0"
+ {
+ assume m0: "m = 0"
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)" by simp
- also from th2 have "\<dots> = ?I x (CN 0 i (CN 0 ?j ?b))" by (simp add: distrib_right)
- finally have "?I x (CN 0 n a') = ?I x (CN 0 i a)" using th2 by simp
- with th2 th have ?case using m0 by blast}
-ultimately show ?case by blast
+ 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)"
+ by simp
+ also from th2 have "\<dots> = ?I x (CN 0 i (CN 0 ?j ?b))"
+ by (simp add: distrib_right)
+ finally have "?I x (CN 0 n a') = ?I x (CN 0 i a)"
+ using th2 by simp
+ with th2 th have ?case using m0
+ by blast
+ }
+ ultimately show ?case by blast
next
case (4 t n a)
let ?nt = "fst (zsplit0 t)"
let ?at = "snd (zsplit0 t)"
- have abj: "zsplit0 t = (?nt,?at)" by simp hence 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
- from th2[simplified] th[simplified] show ?case by simp
+ 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
+ from th2[simplified] th[simplified] show ?case
+ by simp
next
case (5 s t n a)
let ?ns = "fst (zsplit0 s)"
let ?as = "snd (zsplit0 s)"
let ?nt = "fst (zsplit0 t)"
let ?at = "snd (zsplit0 t)"
- have abjs: "zsplit0 s = (?ns,?as)" by simp
- moreover have abjt: "zsplit0 t = (?nt,?at)" by simp
- 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" 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)" by auto
- with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
- from abjs 5 have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast
+ have abjs: "zsplit0 s = (?ns, ?as)"
+ by simp
+ moreover have abjt: "zsplit0 t = (?nt, ?at)"
+ by simp
+ 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"
+ 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)"
+ by auto
+ with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at"
+ by blast
+ from abjs 5 have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as"
+ by blast
from th3[simplified] th2[simplified] th[simplified] show ?case
by (simp add: distrib_right)
next
@@ -843,29 +888,39 @@
let ?as = "snd (zsplit0 s)"
let ?nt = "fst (zsplit0 t)"
let ?at = "snd (zsplit0 t)"
- have abjs: "zsplit0 s = (?ns,?as)" by simp
- moreover have abjt: "zsplit0 t = (?nt,?at)" by simp
- 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" by blast
+ have abjs: "zsplit0 s = (?ns, ?as)"
+ by simp
+ moreover have abjt: "zsplit0 t = (?nt, ?at)"
+ by simp
+ 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"
+ 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)"
by auto
- with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
- from abjs 6 have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast
+ with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at"
+ by blast
+ from abjs 6 have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as"
+ by blast
from th3[simplified] th2[simplified] th[simplified] show ?case
by (simp add: left_diff_distrib)
next
case (7 i t n a)
let ?nt = "fst (zsplit0 t)"
let ?at = "snd (zsplit0 t)"
- have abj: "zsplit0 t = (?nt,?at)" by simp
- hence 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
- hence "?I x (Mul i t) = i * ?I x (CN 0 ?nt ?at)" by simp
- also have "\<dots> = ?I x (CN 0 (i*?nt) (Mul i ?at))" by (simp add: distrib_left)
- finally show ?case using th th2 by simp
+ have abj: "zsplit0 t = (?nt,?at)"
+ by simp
+ 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
+ then have "?I x (Mul i t) = i * ?I x (CN 0 ?nt ?at)"
+ by simp
+ also have "\<dots> = ?I x (CN 0 (i*?nt) (Mul i ?at))"
+ by (simp add: distrib_left)
+ finally show ?case using th th2
+ by simp
qed
consts iszlfm :: "fm \<Rightarrow> bool" -- {* Linearity test for fm *}
@@ -949,137 +1004,203 @@
case (5 a)
let ?c = "fst (zsplit0 a)"
let ?r = "snd (zsplit0 a)"
- have spl: "zsplit0 a = (?c,?r)" by simp
+ 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" by auto
+ 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
apply (auto simp add: Let_def split_def algebra_simps)
- apply (cases "?r", auto)
- apply (case_tac nat, auto)
+ apply (cases "?r")
+ apply auto
+ apply (case_tac nat)
+ apply auto
done
next
case (6 a)
let ?c = "fst (zsplit0 a)"
let ?r = "snd (zsplit0 a)"
- have spl: "zsplit0 a = (?c,?r)" by simp
+ 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" by auto
+ 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 6 Ia nb show ?case
apply (auto simp add: Let_def split_def algebra_simps)
- apply (cases "?r", auto)
- apply (case_tac nat, auto)
+ apply (cases "?r")
+ apply auto
+ apply (case_tac nat)
+ apply auto
done
next
case (7 a)
let ?c = "fst (zsplit0 a)"
let ?r = "snd (zsplit0 a)"
- have spl: "zsplit0 a = (?c,?r)" by simp
+ 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" by auto
+ 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 7 Ia nb show ?case
apply (auto simp add: Let_def split_def algebra_simps)
- apply (cases "?r", auto)
- apply (case_tac nat, auto)
+ apply (cases "?r")
+ apply auto
+ apply (case_tac nat)
+ apply auto
done
next
case (8 a)
let ?c = "fst (zsplit0 a)"
let ?r = "snd (zsplit0 a)"
- have spl: "zsplit0 a = (?c,?r)" by simp
+ 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" by auto
+ 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 8 Ia nb show ?case
+ from 8 Ia nb show ?case
apply (auto simp add: Let_def split_def algebra_simps)
- apply (cases "?r", auto)
- apply (case_tac nat, auto)
+ apply (cases "?r")
+ apply auto
+ apply (case_tac nat)
+ apply auto
done
next
case (9 a)
let ?c = "fst (zsplit0 a)"
let ?r = "snd (zsplit0 a)"
- have spl: "zsplit0 a = (?c,?r)" by simp
+ 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" by auto
+ 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 9 Ia nb show ?case
+ from 9 Ia nb show ?case
apply (auto simp add: Let_def split_def algebra_simps)
- apply (cases "?r", auto)
- apply (case_tac nat, auto)
+ apply (cases "?r")
+ apply auto
+ apply (case_tac nat)
+ apply auto
done
next
case (10 a)
let ?c = "fst (zsplit0 a)"
let ?r = "snd (zsplit0 a)"
- have spl: "zsplit0 a = (?c,?r)" by simp
+ 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" by auto
+ 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 10 Ia nb show ?case
+ from 10 Ia nb show ?case
apply (auto simp add: Let_def split_def algebra_simps)
- apply (cases "?r",auto)
- apply (case_tac nat, auto)
+ apply (cases "?r")
+ apply auto
+ apply (case_tac nat)
+ apply auto
done
next
case (11 j a)
let ?c = "fst (zsplit0 a)"
let ?r = "snd (zsplit0 a)"
- have spl: "zsplit0 a = (?c,?r)" by simp
+ 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" by auto
+ 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"
- 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
+ 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" hence z: "zlfm (Dvd j a) = (zlfm (Eq a))" by (simp add: Let_def)
- hence ?case using 11 `j = 0` by (simp del: zlfm.simps) }
+ {
+ assume "j = 0"
+ then have z: "zlfm (Dvd j a) = (zlfm (Eq a))"
+ by (simp add: Let_def)
+ then have ?case using 11 `j = 0`
+ by (simp del: zlfm.simps)
+ }
moreover
- {assume "?c=0" and "j\<noteq>0" hence ?case
+ {
+ assume "?c = 0" and "j \<noteq> 0"
+ then have ?case
using zsplit0_I[OF spl, where x="i" and bs="bs"]
apply (auto simp add: Let_def split_def algebra_simps)
- apply (cases "?r",auto)
- apply (case_tac nat, auto)
- done}
+ apply (cases "?r")
+ apply auto
+ apply (case_tac nat)
+ apply auto
+ done
+ }
moreover
- {assume cp: "?c > 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))"
+ {
+ assume cp: "?c > 0" and jnz: "j \<noteq> 0"
+ then have l: "?L (?l (Dvd j a))"
by (simp add: nb Let_def split_def)
- hence ?case using Ia cp jnz by (simp add: Let_def split_def)}
+ then have ?case
+ using Ia cp jnz by (simp add: Let_def split_def)
+ }
moreover
- {assume cn: "?c < 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))"
+ {
+ assume cn: "?c < 0" and jnz: "j \<noteq> 0"
+ then have l: "?L (?l (Dvd j a))"
by (simp add: nb Let_def split_def)
- hence ?case using Ia cn jnz dvd_minus_iff[of "abs j" "?c*i + ?N ?r" ]
- by (simp add: Let_def split_def) }
+ then have ?case
+ using Ia cn jnz dvd_minus_iff[of "abs j" "?c*i + ?N ?r"]
+ by (simp add: Let_def split_def)
+ }
ultimately show ?case by blast
next
case (12 j a)
let ?c = "fst (zsplit0 a)"
let ?r = "snd (zsplit0 a)"
- have spl: "zsplit0 a = (?c,?r)" by simp
+ 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" by auto
+ 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"
- 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
+ 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" hence z: "zlfm (NDvd j a) = (zlfm (NEq a))" by (simp add: Let_def)
- hence ?case using assms 12 `j = 0` by (simp del: zlfm.simps)}
+ {
+ assume "j = 0"
+ 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)
+ }
moreover
- {assume "?c=0" and "j\<noteq>0" hence ?case
+ {
+ assume "?c = 0" and "j \<noteq> 0"
+ then have ?case
using zsplit0_I[OF spl, where x="i" and bs="bs"]
apply (auto simp add: Let_def split_def algebra_simps)
- apply (cases "?r",auto)
- apply (case_tac nat, auto)
- done}
+ apply (cases "?r")
+ apply auto
+ apply (case_tac nat)
+ apply auto
+ done
+ }
moreover
- {assume cp: "?c > 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))"
+ {
+ assume cp: "?c > 0" and jnz: "j \<noteq> 0"
+ then have l: "?L (?l (Dvd j a))"
by (simp add: nb Let_def split_def)
- hence ?case using Ia cp jnz by (simp add: Let_def split_def) }
+ then have ?case using Ia cp jnz
+ by (simp add: Let_def split_def)
+ }
moreover
- {assume cn: "?c < 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))"
+ {
+ assume cn: "?c < 0" and jnz: "j \<noteq> 0"
+ then have l: "?L (?l (Dvd j a))"
by (simp add: nb Let_def split_def)
- hence ?case using Ia cn jnz dvd_minus_iff[of "abs j" "?c*i + ?N ?r"]
- by (simp add: Let_def split_def)}
+ then have ?case
+ using Ia cn jnz dvd_minus_iff[of "abs j" "?c*i + ?N ?r"]
+ by (simp add: Let_def split_def)
+ }
ultimately show ?case by blast
qed auto
@@ -1133,10 +1254,12 @@
shows "d_\<delta> p d'"
using lin ad d
proof (induct p rule: iszlfm.induct)
- case (9 i c e) thus ?case using d
+ case (9 i c e)
+ then show ?case using d
by (simp add: dvd_trans[of "i" "d" "d'"])
next
- case (10 i c e) thus ?case using d
+ case (10 i c e)
+ then show ?case using d
by (simp add: dvd_trans[of "i" "d" "d'"])
qed simp_all
@@ -1147,21 +1270,33 @@
proof (induct p rule: iszlfm.induct)
case (1 p q)
let ?d = "\<delta> (And p q)"
- from 1 lcm_pos_int have dp: "?d >0" by simp
- have d1: "\<delta> p dvd \<delta> (And p q)" using 1 by simp
- hence th: "d_\<delta> p ?d" using delta_mono 1(2,3) by(simp only: iszlfm.simps)
- have "\<delta> q dvd \<delta> (And p q)" using 1 by simp
- hence th': "d_\<delta> q ?d" using delta_mono 1 by(simp only: iszlfm.simps)
- from th th' dp show ?case by simp
+ from 1 lcm_pos_int have dp: "?d > 0"
+ by simp
+ have d1: "\<delta> p dvd \<delta> (And p q)"
+ using 1 by simp
+ then have th: "d_\<delta> p ?d"
+ using delta_mono 1(2,3) by (simp only: iszlfm.simps)
+ have "\<delta> q dvd \<delta> (And p q)"
+ using 1 by simp
+ then have th': "d_\<delta> q ?d"
+ using delta_mono 1 by (simp only: iszlfm.simps)
+ from th th' dp show ?case
+ by simp
next
case (2 p q)
let ?d = "\<delta> (And p q)"
- from 2 lcm_pos_int have dp: "?d >0" by simp
- have "\<delta> p dvd \<delta> (And p q)" using 2 by simp
- hence th: "d_\<delta> p ?d" using delta_mono 2 by(simp only: iszlfm.simps)
- have "\<delta> q dvd \<delta> (And p q)" using 2 by simp
- hence th': "d_\<delta> q ?d" using delta_mono 2 by(simp only: iszlfm.simps)
- from th th' dp show ?case by simp
+ from 2 lcm_pos_int have dp: "?d > 0"
+ by simp
+ have "\<delta> p dvd \<delta> (And p q)"
+ using 2 by simp
+ then have th: "d_\<delta> p ?d"
+ using delta_mono 2 by (simp only: iszlfm.simps)
+ have "\<delta> q dvd \<delta> (And p q)"
+ using 2 by simp
+ then have th': "d_\<delta> q ?d"
+ using delta_mono 2 by (simp only: iszlfm.simps)
+ from th th' dp show ?case
+ by simp
qed simp_all
@@ -1247,7 +1382,9 @@
text {* Lemmas for the correctness of @{text "\<sigma>_\<rho>"} *}
-lemma dvd1_eq1: "x >0 \<Longrightarrow> (x::int) dvd 1 = (x = 1)"
+lemma dvd1_eq1:
+ fixes x :: int
+ shows "x > 0 \<Longrightarrow> x dvd 1 \<longleftrightarrow> x = 1"
by simp
lemma minusinf_inf:
@@ -1257,25 +1394,32 @@
(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) thus ?case
+ case (1 p q)
+ then show ?case
by auto (rule_tac x="min z za" in exI,simp)
next
- case (2 p q) thus ?case
+ case (2 p q)
+ then show ?case
by auto (rule_tac x="min z za" in exI,simp)
next
- case (3 c e) hence c1: "c=1" and nb: "numbound0 e" by simp_all
+ case (3 c e)
+ then have c1: "c = 1" and nb: "numbound0 e"
+ by simp_all
fix a
- from 3 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"
+ from 3 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"
with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
- show "False" by simp
+ show False by simp
qed
- thus ?case by auto
+ then show ?case by auto
next
- case (4 c e) hence c1: "c=1" and nb: "numbound0 e" by simp_all
+ case (4 c e)
+ 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"
with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Sun Mar 02 19:15:23 2014 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Sun Mar 02 22:43:20 2014 +0100
@@ -325,7 +325,7 @@
ML_file "langford.ML"
method_setup dlo = {*
- Scan.succeed (SIMPLE_METHOD' o LangfordQE.dlo_tac)
+ Scan.succeed (SIMPLE_METHOD' o Langford.dlo_tac)
*} "Langford's algorithm for quantifier elimination in dense linear orders"
--- a/src/HOL/Decision_Procs/langford.ML Sun Mar 02 19:15:23 2014 +0100
+++ b/src/HOL/Decision_Procs/langford.ML Sun Mar 02 22:43:20 2014 +0100
@@ -2,13 +2,13 @@
Author: Amine Chaieb, TU Muenchen
*)
-signature LANGFORD_QE =
+signature LANGFORD =
sig
val dlo_tac : Proof.context -> int -> tactic
val dlo_conv : Proof.context -> cterm -> thm
end
-structure LangfordQE: LANGFORD_QE =
+structure Langford: LANGFORD =
struct
val dest_set =
@@ -21,7 +21,7 @@
fun prove_finite cT u =
let
- val [th0, th1] = map (instantiate' [SOME cT] []) @{thms "finite.intros"}
+ val [th0, th1] = map (instantiate' [SOME cT] []) @{thms finite.intros}
fun ins x th =
Thm.implies_elim
(instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg) (Thm.cprop_of th), SOME x] th1) th
@@ -33,176 +33,195 @@
(Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms ball_simps simp_thms})));
fun basic_dloqe ctxt stupid dlo_qeth dlo_qeth_nolb dlo_qeth_noub gather ep =
- case term_of ep of
- Const(@{const_name Ex},_)$_ =>
- let
- val p = Thm.dest_arg ep
- val ths =
- simplify (put_simpset HOL_basic_ss ctxt addsimps gather) (instantiate' [] [SOME p] stupid)
- val (L,U) =
- let
- val (_, q) = Thm.dest_abs NONE (Thm.dest_arg (Thm.rhs_of ths))
- in (Thm.dest_arg1 q |> Thm.dest_arg1, Thm.dest_arg q |> Thm.dest_arg1)
- end
- fun proveneF S =
- let val (a,A) = Thm.dest_comb S |>> Thm.dest_arg
- val cT = ctyp_of_term a
- val ne = instantiate' [SOME cT] [SOME a, SOME A]
- @{thm insert_not_empty}
- val f = prove_finite cT (dest_set S)
- in (ne, f) end
+ (case term_of ep of
+ Const (@{const_name Ex}, _) $ _ =>
+ let
+ val p = Thm.dest_arg ep
+ val ths =
+ simplify (put_simpset HOL_basic_ss ctxt addsimps gather)
+ (instantiate' [] [SOME p] stupid)
+ val (L, U) =
+ let val (_, q) = Thm.dest_abs NONE (Thm.dest_arg (Thm.rhs_of ths))
+ in (Thm.dest_arg1 q |> Thm.dest_arg1, Thm.dest_arg q |> Thm.dest_arg1) end
+ fun proveneF S =
+ let
+ val (a, A) = Thm.dest_comb S |>> Thm.dest_arg
+ val cT = ctyp_of_term a
+ val ne = instantiate' [SOME cT] [SOME a, SOME A] @{thm insert_not_empty}
+ val f = prove_finite cT (dest_set S)
+ in (ne, f) end
- val qe = case (term_of L, term_of U) of
- (Const (@{const_name Orderings.bot}, _),_) =>
- let
- val (neU,fU) = proveneF U
- in simp_rule ctxt (Thm.transitive ths (dlo_qeth_nolb OF [neU, fU])) end
- | (_,Const (@{const_name Orderings.bot}, _)) =>
- let
- val (neL,fL) = proveneF L
- in simp_rule ctxt (Thm.transitive ths (dlo_qeth_noub OF [neL, fL])) end
-
- | (_,_) =>
- let
- val (neL,fL) = proveneF L
- val (neU,fU) = proveneF U
- in simp_rule ctxt (Thm.transitive ths (dlo_qeth OF [neL, neU, fL, fU]))
- end
- in qe end
- | _ => error "dlo_qe : Not an existential formula";
+ val qe =
+ (case (term_of L, term_of U) of
+ (Const (@{const_name Orderings.bot}, _),_) =>
+ let val (neU, fU) = proveneF U
+ in simp_rule ctxt (Thm.transitive ths (dlo_qeth_nolb OF [neU, fU])) end
+ | (_, Const (@{const_name Orderings.bot}, _)) =>
+ let val (neL,fL) = proveneF L
+ in simp_rule ctxt (Thm.transitive ths (dlo_qeth_noub OF [neL, fL])) end
+ | _ =>
+ let
+ val (neL, fL) = proveneF L
+ val (neU, fU) = proveneF U
+ in simp_rule ctxt (Thm.transitive ths (dlo_qeth OF [neL, neU, fL, fU])) end)
+ in qe end
+ | _ => error "dlo_qe : Not an existential formula");
val all_conjuncts =
- let fun h acc ct =
- case term_of ct of
- @{term HOL.conj}$_$_ => h (h acc (Thm.dest_arg ct)) (Thm.dest_arg1 ct)
- | _ => ct::acc
-in h [] end;
+ let
+ fun h acc ct =
+ (case term_of ct of
+ @{term HOL.conj} $ _ $ _ => h (h acc (Thm.dest_arg ct)) (Thm.dest_arg1 ct)
+ | _ => ct :: acc)
+ in h [] end;
fun conjuncts ct =
- case term_of ct of
- @{term HOL.conj}$_$_ => (Thm.dest_arg1 ct)::(conjuncts (Thm.dest_arg ct))
-| _ => [ct];
+ (case term_of ct of
+ @{term HOL.conj} $ _ $ _ => Thm.dest_arg1 ct :: conjuncts (Thm.dest_arg ct)
+ | _ => [ct]);
-fun fold1 f = foldr1 (uncurry f);
+fun fold1 f = foldr1 (uncurry f); (* FIXME !? *)
-val list_conj = fold1 (fn c => fn c' => Thm.apply (Thm.apply @{cterm HOL.conj} c) c') ;
+val list_conj =
+ fold1 (fn c => fn c' => Thm.apply (Thm.apply @{cterm HOL.conj} c) c');
fun mk_conj_tab th =
- let fun h acc th =
- case prop_of th of
- @{term "Trueprop"}$(@{term HOL.conj}$p$q) =>
- h (h acc (th RS conjunct2)) (th RS conjunct1)
- | @{term "Trueprop"}$p => (p,th)::acc
-in fold (Termtab.insert Thm.eq_thm) (h [] th) Termtab.empty end;
+ let
+ fun h acc th =
+ (case prop_of th of
+ @{term "Trueprop"} $ (@{term HOL.conj} $ p $ q) =>
+ h (h acc (th RS conjunct2)) (th RS conjunct1)
+ | @{term "Trueprop"} $ p => (p, th) :: acc)
+ in fold (Termtab.insert Thm.eq_thm) (h [] th) Termtab.empty end;
fun is_conj (@{term HOL.conj}$_$_) = true
| is_conj _ = false;
fun prove_conj tab cjs =
- case cjs of
- [c] => if is_conj (term_of c) then prove_conj tab (conjuncts c) else tab c
- | c::cs => conjI OF [prove_conj tab [c], prove_conj tab cs];
+ (case cjs of
+ [c] =>
+ if is_conj (term_of c)
+ then prove_conj tab (conjuncts c)
+ else tab c
+ | c :: cs => conjI OF [prove_conj tab [c], prove_conj tab cs]);
fun conj_aci_rule eq =
- let
- val (l,r) = Thm.dest_equals eq
- fun tabl c = the (Termtab.lookup (mk_conj_tab (Thm.assume l)) (term_of c))
- fun tabr c = the (Termtab.lookup (mk_conj_tab (Thm.assume r)) (term_of c))
- val ll = Thm.dest_arg l
- val rr = Thm.dest_arg r
+ let
+ val (l, r) = Thm.dest_equals eq
+ fun tabl c = the (Termtab.lookup (mk_conj_tab (Thm.assume l)) (term_of c))
+ fun tabr c = the (Termtab.lookup (mk_conj_tab (Thm.assume r)) (term_of c))
+ val ll = Thm.dest_arg l
+ val rr = Thm.dest_arg r
+ val thl = prove_conj tabl (conjuncts rr) |> Drule.implies_intr_hyps
+ val thr = prove_conj tabr (conjuncts ll) |> Drule.implies_intr_hyps
+ val eqI = instantiate' [] [SOME ll, SOME rr] @{thm iffI}
+ in Thm.implies_elim (Thm.implies_elim eqI thl) thr |> mk_meta_eq end;
- val thl = prove_conj tabl (conjuncts rr)
- |> Drule.implies_intr_hyps
- val thr = prove_conj tabr (conjuncts ll)
- |> Drule.implies_intr_hyps
- val eqI = instantiate' [] [SOME ll, SOME rr] @{thm iffI}
- in Thm.implies_elim (Thm.implies_elim eqI thl) thr |> mk_meta_eq end;
+fun contains x ct =
+ member (op aconv) (Misc_Legacy.term_frees (term_of ct)) (term_of x);
-fun contains x ct = member (op aconv) (Misc_Legacy.term_frees (term_of ct)) (term_of x);
-
-fun is_eqx x eq = case term_of eq of
- Const(@{const_name HOL.eq},_)$l$r => l aconv term_of x orelse r aconv term_of x
- | _ => false ;
+fun is_eqx x eq =
+ (case term_of eq of
+ Const (@{const_name HOL.eq}, _) $ l $ r =>
+ l aconv term_of x orelse r aconv term_of x
+ | _ => false);
local
+
fun proc ctxt ct =
- case term_of ct of
- Const(@{const_name Ex},_)$Abs (xn,_,_) =>
- let
- val e = Thm.dest_fun ct
- val (x,p) = Thm.dest_abs (SOME xn) (Thm.dest_arg ct)
- val Pp = Thm.apply @{cterm "Trueprop"} p
- val (eqs,neqs) = List.partition (is_eqx x) (all_conjuncts p)
- in case eqs of
- [] =>
- let
- val (dx,ndx) = List.partition (contains x) neqs
- in case ndx of [] => NONE
- | _ =>
- conj_aci_rule (Thm.mk_binop @{cterm "op == :: prop => _"} Pp
- (Thm.apply @{cterm Trueprop} (list_conj (ndx @dx))))
- |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e
- |> Conv.fconv_rule (Conv.arg_conv
- (Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms ex_simps})))
- |> SOME
- end
- | _ => conj_aci_rule (Thm.mk_binop @{cterm "op == :: prop => _"} Pp
- (Thm.apply @{cterm Trueprop} (list_conj (eqs@neqs))))
- |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e
- |> Conv.fconv_rule (Conv.arg_conv
- (Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms ex_simps})))
- |> SOME
- end
- | _ => NONE;
-in val reduce_ex_simproc =
+ (case term_of ct of
+ Const (@{const_name Ex}, _) $ Abs (xn, _, _) =>
+ let
+ val e = Thm.dest_fun ct
+ val (x,p) = Thm.dest_abs (SOME xn) (Thm.dest_arg ct)
+ val Pp = Thm.apply @{cterm Trueprop} p
+ val (eqs,neqs) = List.partition (is_eqx x) (all_conjuncts p)
+ in
+ (case eqs of
+ [] =>
+ let
+ val (dx, ndx) = List.partition (contains x) neqs
+ in
+ case ndx of
+ [] => NONE
+ | _ =>
+ conj_aci_rule (Thm.mk_binop @{cterm "op \<equiv> :: prop => _"} Pp
+ (Thm.apply @{cterm Trueprop} (list_conj (ndx @ dx))))
+ |> Thm.abstract_rule xn x
+ |> Drule.arg_cong_rule e
+ |> Conv.fconv_rule
+ (Conv.arg_conv
+ (Simplifier.rewrite
+ (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms ex_simps})))
+ |> SOME
+ end
+ | _ =>
+ conj_aci_rule (Thm.mk_binop @{cterm "op \<equiv> :: prop => _"} Pp
+ (Thm.apply @{cterm Trueprop} (list_conj (eqs @ neqs))))
+ |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e
+ |> Conv.fconv_rule
+ (Conv.arg_conv
+ (Simplifier.rewrite
+ (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms ex_simps})))
+ |> SOME)
+ end
+ | _ => NONE);
+
+in
+
+val reduce_ex_simproc =
Simplifier.make_simproc
- {lhss = [@{cpat "EX x. ?P x"}] , name = "reduce_ex_simproc",
- proc = K proc, identifier = []}
+ {lhss = [@{cpat "\<exists>x. ?P x"}],
+ name = "reduce_ex_simproc",
+ proc = K proc,
+ identifier = []};
+
end;
fun raw_dlo_conv ctxt dlo_ss ({qe_bnds, qe_nolb, qe_noub, gst, gs, ...}: Langford_Data.entry) =
- let
- val ctxt' = put_simpset dlo_ss ctxt addsimps @{thms "dnf_simps"} addsimprocs [reduce_ex_simproc]
- val dnfex_conv = Simplifier.rewrite ctxt'
- val pcv =
- Simplifier.rewrite
- (put_simpset dlo_ss ctxt
- addsimps @{thms simp_thms ex_simps all_simps all_not_ex not_all ex_disj_distrib})
- in fn p =>
- Qelim.gen_qelim_conv pcv pcv dnfex_conv cons
- (Thm.add_cterm_frees p []) (K Thm.reflexive) (K Thm.reflexive)
- (K (basic_dloqe ctxt gst qe_bnds qe_nolb qe_noub gs)) p
- end;
-
+ let
+ val ctxt' =
+ Context_Position.set_visible false (put_simpset dlo_ss ctxt)
+ addsimps @{thms dnf_simps} addsimprocs [reduce_ex_simproc]
+ val dnfex_conv = Simplifier.rewrite ctxt'
+ val pcv =
+ Simplifier.rewrite
+ (put_simpset dlo_ss ctxt
+ addsimps @{thms simp_thms ex_simps all_simps all_not_ex not_all ex_disj_distrib})
+ in
+ fn p =>
+ Qelim.gen_qelim_conv pcv pcv dnfex_conv cons
+ (Thm.add_cterm_frees p []) (K Thm.reflexive) (K Thm.reflexive)
+ (K (basic_dloqe ctxt gst qe_bnds qe_nolb qe_noub gs)) p
+ end;
val grab_atom_bop =
- let
- fun h bounds tm =
- (case term_of tm of
- Const (@{const_name HOL.eq}, T) $ _ $ _ =>
- if domain_type T = HOLogic.boolT then find_args bounds tm
- else Thm.dest_fun2 tm
- | Const (@{const_name Not}, _) $ _ => h bounds (Thm.dest_arg tm)
- | Const (@{const_name All}, _) $ _ => find_body bounds (Thm.dest_arg tm)
- | Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
- | Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm)
- | Const (@{const_name HOL.conj}, _) $ _ $ _ => find_args bounds tm
- | Const (@{const_name HOL.disj}, _) $ _ $ _ => find_args bounds tm
- | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
- | Const ("==>", _) $ _ $ _ => find_args bounds tm
- | Const ("==", _) $ _ $ _ => find_args bounds tm
- | Const (@{const_name Trueprop}, _) $ _ => h bounds (Thm.dest_arg tm)
- | _ => Thm.dest_fun2 tm)
- and find_args bounds tm =
- (h bounds (Thm.dest_arg tm) handle CTERM _ => h bounds (Thm.dest_arg1 tm))
- and find_body bounds b =
- let val (_, b') = Thm.dest_abs (SOME (Name.bound bounds)) b
- in h (bounds + 1) b' end;
-in h end;
+ let
+ fun h bounds tm =
+ (case term_of tm of
+ Const (@{const_name HOL.eq}, T) $ _ $ _ =>
+ if domain_type T = HOLogic.boolT then find_args bounds tm
+ else Thm.dest_fun2 tm
+ | Const (@{const_name Not}, _) $ _ => h bounds (Thm.dest_arg tm)
+ | Const (@{const_name All}, _) $ _ => find_body bounds (Thm.dest_arg tm)
+ | Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
+ | Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm)
+ | Const (@{const_name HOL.conj}, _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name HOL.disj}, _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
+ | Const ("==>", _) $ _ $ _ => find_args bounds tm
+ | Const ("==", _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name Trueprop}, _) $ _ => h bounds (Thm.dest_arg tm)
+ | _ => Thm.dest_fun2 tm)
+ and find_args bounds tm =
+ (h bounds (Thm.dest_arg tm) handle CTERM _ => h bounds (Thm.dest_arg1 tm))
+ and find_body bounds b =
+ let val (_, b') = Thm.dest_abs (SOME (Name.bound bounds)) b
+ in h (bounds + 1) b' end;
+ in h end;
fun dlo_instance ctxt tm =
- (fst (Langford_Data.get ctxt),
- Langford_Data.match ctxt (grab_atom_bop 0 tm));
+ (fst (Langford_Data.get ctxt), Langford_Data.match ctxt (grab_atom_bop 0 tm));
fun dlo_conv ctxt tm =
(case dlo_instance ctxt tm of
@@ -210,28 +229,28 @@
| (ss, SOME instance) => raw_dlo_conv ctxt ss instance tm);
fun generalize_tac f = CSUBGOAL (fn (p, _) => PRIMITIVE (fn st =>
- let
- fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"}
- fun gen x t = Thm.apply (all (ctyp_of_term x)) (Thm.lambda x t)
- val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p)
- val p' = fold_rev gen ts p
- in Thm.implies_intr p' (Thm.implies_elim st (fold Thm.forall_elim ts (Thm.assume p'))) end));
-
+ let
+ fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"}
+ fun gen x t = Thm.apply (all (ctyp_of_term x)) (Thm.lambda x t)
+ val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p)
+ val p' = fold_rev gen ts p
+ in Thm.implies_intr p' (Thm.implies_elim st (fold Thm.forall_elim ts (Thm.assume p'))) end));
fun cfrees ats ct =
- let
- val ins = insert (op aconvc)
- fun h acc t =
- case (term_of t) of
- _$_$_ => if member (op aconvc) ats (Thm.dest_fun2 t)
- then ins (Thm.dest_arg t) (ins (Thm.dest_arg1 t) acc)
- else h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
- | _$_ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
- | Abs(_,_,_) => Thm.dest_abs NONE t ||> h acc |> uncurry (remove (op aconvc))
- | Free _ => if member (op aconvc) ats t then acc else ins t acc
- | Var _ => if member (op aconvc) ats t then acc else ins t acc
- | _ => acc
- in h [] ct end
+ let
+ val ins = insert (op aconvc)
+ fun h acc t =
+ (case (term_of t) of
+ _ $ _ $ _ =>
+ if member (op aconvc) ats (Thm.dest_fun2 t)
+ then ins (Thm.dest_arg t) (ins (Thm.dest_arg1 t) acc)
+ else h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
+ | _ $ _ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
+ | Abs _ => Thm.dest_abs NONE t ||> h acc |> uncurry (remove (op aconvc))
+ | Free _ => if member (op aconvc) ats t then acc else ins t acc
+ | Var _ => if member (op aconvc) ats t then acc else ins t acc
+ | _ => acc)
+ in h [] ct end
fun dlo_tac ctxt = CSUBGOAL (fn (p, i) =>
(case dlo_instance ctxt p of
--- a/src/HOL/ex/ML.thy Sun Mar 02 19:15:23 2014 +0100
+++ b/src/HOL/ex/ML.thy Sun Mar 02 22:43:20 2014 +0100
@@ -104,7 +104,7 @@
*}
text {*
- The @{ML_struct Par_List} module provides high-level combinators for
+ The @{ML_structure Par_List} module provides high-level combinators for
parallel list operations. *}
ML {* timeit (fn () => map (fn n => ackermann 3 n) (1 upto 10)) *}
--- a/src/Pure/General/completion.ML Sun Mar 02 19:15:23 2014 +0100
+++ b/src/Pure/General/completion.ML Sun Mar 02 22:43:20 2014 +0100
@@ -9,6 +9,7 @@
type T
val names: Position.T -> (string * string) list -> T
val none: T
+ val reported_text: T -> string
val report: T -> unit
end;
@@ -30,15 +31,17 @@
val none = names Position.none [];
-fun report completion =
+fun reported_text completion =
let val {pos, total, names} = dest completion in
if Position.is_reported pos andalso not (null names) then
let
val markup = Position.markup pos Markup.completion;
val body = (total, names) |>
let open XML.Encode in pair int (list (pair string string)) end;
- in Output.report (YXML.string_of (XML.Elem (markup, body))) end
- else ()
+ in YXML.string_of (XML.Elem (markup, body)) end
+ else ""
end;
+val report = Output.report o reported_text;
+
end;
--- a/src/Pure/General/name_space.ML Sun Mar 02 19:15:23 2014 +0100
+++ b/src/Pure/General/name_space.ML Sun Mar 02 22:43:20 2014 +0100
@@ -206,11 +206,12 @@
if Context_Position.is_visible_generic context andalso Position.is_reported pos
then
let
+ val x = Name.clean xname;
val Name_Space {kind = k, internals, ...} = space;
val ext = extern_shortest (Context.proof_of context) space;
val names =
Symtab.fold
- (fn (a, (b :: _, _)) => String.isPrefix xname a ? cons (ext b, Long_Name.implode [k, b])
+ (fn (a, (b :: _, _)) => String.isPrefix x a ? cons (ext b, Long_Name.implode [k, b])
| _ => I) internals []
|> sort_distinct (string_ord o pairself #1);
in Completion.names pos names end
@@ -451,8 +452,9 @@
(Context_Position.report_generic context pos (markup space name);
(name, x))
| NONE =>
- (Completion.report (completion context space (xname, pos));
- error (undefined (kind_of space) name ^ Position.here pos)))
+ error (undefined (kind_of space) name ^ Position.here pos ^
+ Markup.markup Markup.report
+ (Completion.reported_text (completion context space (xname, pos)))))
end;
fun get (space, tab) name =
--- a/src/Pure/Isar/proof_context.ML Sun Mar 02 19:15:23 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML Sun Mar 02 22:43:20 2014 +0100
@@ -377,11 +377,17 @@
fun read_class ctxt text =
let
val tsig = tsig_of ctxt;
- val (s, pos) = Symbol_Pos.source_content (Syntax.read_token text);
- val c = Type.cert_class tsig (Type.intern_class tsig s)
- handle TYPE (msg, _, _) => error (msg ^ Position.here pos);
- val _ = Context_Position.report ctxt pos (Name_Space.markup (Type.class_space tsig) c);
- in c end;
+ val class_space = Type.class_space tsig;
+
+ val (xname, pos) = Symbol_Pos.source_content (Syntax.read_token text);
+ 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))));
+ val _ = Context_Position.report ctxt pos (Name_Space.markup class_space name);
+ in name end;
(* types *)
@@ -435,26 +441,7 @@
in (xs ~~ Ts, ctxt') end;
-(* type and 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 =>
- Const (d, Consts.type_scheme (consts_of ctxt) d handle TYPE (msg, _, _) => err msg)
- | NONE => Consts.read_const consts (c, pos));
- val _ =
- if strict then ignore (Consts.the_const consts d) handle TYPE (msg, _, _) => err msg
- else ();
- val _ = Context_Position.report ctxt pos (Name_Space.markup (Consts.space_of consts) d);
- in t end;
-
-in
+(* type names *)
fun read_type_name ctxt strict text =
let
@@ -466,15 +453,13 @@
TFree (c, default_sort ctxt (c, ~1)))
else
let
- val d = intern_type ctxt c;
- val decl = Type.the_decl tsig (d, pos);
+ val (d, decl) = Type.check_decl (Context.Proof ctxt) tsig (c, pos);
fun err () = error ("Bad type name: " ^ quote d ^ Position.here pos);
val args =
(case decl of
Type.LogicalType n => n
| Type.Abbreviation (vs, _, _) => if strict then err () else length vs
| Type.Nonterminal => if strict then err () else 0);
- val _ = Context_Position.report ctxt pos (Name_Space.markup (Type.type_space tsig) d);
in Type (d, replicate args dummyT) end
end;
@@ -484,6 +469,30 @@
| T => error ("Not a type constructor: " ^ Syntax.string_of_typ ctxt T));
+(* 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;
+
+in
+
fun read_const_proper ctxt strict =
prep_const_proper ctxt strict o Symbol_Pos.source_content o Syntax.read_token;
--- a/src/Pure/ML/ml_compiler_polyml.ML Sun Mar 02 19:15:23 2014 +0100
+++ b/src/Pure/ML/ml_compiler_polyml.ML Sun Mar 02 22:43:20 2014 +0100
@@ -64,7 +64,7 @@
| reported loc (PolyML.PTopenedAt decl) =
cons (reported_entity Markup.ML_openN loc decl)
| reported loc (PolyML.PTstructureAt decl) =
- cons (reported_entity Markup.ML_structN loc decl)
+ cons (reported_entity Markup.ML_structureN loc decl)
| reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ())
| reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ())
| reported _ _ = I
--- a/src/Pure/PIDE/markup.ML Sun Mar 02 19:15:23 2014 +0100
+++ b/src/Pure/PIDE/markup.ML Sun Mar 02 22:43:20 2014 +0100
@@ -92,7 +92,7 @@
val ML_commentN: string val ML_comment: T
val ML_defN: string
val ML_openN: string
- val ML_structN: string
+ val ML_structureN: string
val ML_typingN: string val ML_typing: T
val antiquotedN: string val antiquoted: T
val antiquoteN: string val antiquote: T
@@ -391,7 +391,7 @@
val ML_defN = "ML_def";
val ML_openN = "ML_open";
-val ML_structN = "ML_struct";
+val ML_structureN = "ML_structure";
val (ML_typingN, ML_typing) = markup_elem "ML_typing";
--- a/src/Pure/PIDE/markup.scala Sun Mar 02 19:15:23 2014 +0100
+++ b/src/Pure/PIDE/markup.scala Sun Mar 02 22:43:20 2014 +0100
@@ -204,7 +204,7 @@
val ML_DEF = "ML_def"
val ML_OPEN = "ML_open"
- val ML_STRUCT = "ML_struct"
+ val ML_STRUCTURE = "ML_structure"
val ML_TYPING = "ML_typing"
--- a/src/Pure/Thy/thy_output.ML Sun Mar 02 19:15:23 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML Sun Mar 02 22:43:20 2014 +0100
@@ -661,7 +661,7 @@
(ml_text (Binding.name "ML") (ml_enclose "fn _ => (" ");") #>
ml_text (Binding.name "ML_op") (ml_enclose "fn _ => (op " ");") #>
ml_text (Binding.name "ML_type") (ml_enclose "val _ = NONE : (" ") option;") #>
- ml_text (Binding.name "ML_struct")
+ ml_text (Binding.name "ML_structure")
(ml_enclose "functor XXX() = struct structure XX = " " end;") #>
ml_text (Binding.name "ML_functor") (* FIXME formal treatment of functor name (!?) *)
--- a/src/Pure/consts.ML Sun Mar 02 19:15:23 2014 +0100
+++ b/src/Pure/consts.ML Sun Mar 02 22:43:20 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 read_const: T -> string * Position.T -> term
+ val check_const: Context.generic -> T -> xstring * Position.T -> term
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
@@ -141,11 +141,12 @@
| NONE => s);
-(* read_const *)
+(* check_const *)
-fun read_const consts (raw_c, pos) =
+fun check_const context consts (xname, pos) =
let
- val c = intern consts raw_c;
+ 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;
--- a/src/Pure/type.ML Sun Mar 02 19:15:23 2014 +0100
+++ b/src/Pure/type.ML Sun Mar 02 22:43:20 2014 +0100
@@ -52,6 +52,7 @@
val intern_type: tsig -> xstring -> string
val extern_type: Proof.context -> tsig -> string -> xstring
val is_logtype: tsig -> string -> bool
+ val check_decl: Context.generic -> tsig -> xstring * Position.T -> string * decl
val the_decl: tsig -> string * Position.T -> decl
val cert_typ_mode: mode -> tsig -> typ -> typ
val cert_typ: tsig -> typ -> typ
@@ -257,6 +258,8 @@
fun lookup_type (TSig {types = (_, types), ...}) = Symtab.lookup types;
+fun check_decl context (TSig {types, ...}) = Name_Space.check context types;
+
fun the_decl tsig (c, pos) =
(case lookup_type tsig c of
NONE => error (undecl_type c ^ Position.here pos)
--- a/src/Tools/jEdit/src/rendering.scala Sun Mar 02 19:15:23 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala Sun Mar 02 22:43:20 2014 +0100
@@ -359,7 +359,7 @@
case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _)))
if !props.exists(
{ case (Markup.KIND, Markup.ML_OPEN) => true
- case (Markup.KIND, Markup.ML_STRUCT) => true
+ case (Markup.KIND, Markup.ML_STRUCTURE) => true
case _ => false }) =>
val opt_link =